Theory Example

(*
    Author:   Salomon Sickert
    License:  BSD
*)

section ‹Example›

theory Example
imports
  "../LTL" "../Rewriting" "HOL-Library.Code_Target_Numeral"
begin

― ‹The included parser always returns a @{typ "String.literal ltlc"}. If a different labelling
  is needed one can use @{const map_ltlc} to relabel the leafs. In our example we prepend a
  string to each atom.›

definition rewrite :: "String.literal ltlc ⇒ String.literal ltlc"
where
  "rewrite ≡ ltln_to_ltlc o rewrite_iter_slow o ltlc_to_ltln o (map_ltlc (λs. String.implode ''prop('' + s + String.implode '')''))"

― ‹Export rewriting engine (and also constructors)›

export_code true⇩c Iff_ltlc rewrite in SML file_prefix ‹rewrite_example›

end