src/HOL/ex/ReflectionEx.thy

     ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
 header {* Examples for generic reflection and reification *}
-
 theory ReflectionEx
 imports Reflection
 begin
 
 text{* This theory presents two methods: reify and reflection *}

 The method reflection uses @{text reify} and has a very similar signature: @{text "reflection corr_thm eqs (t)"}. Here again @{text eqs} and @{text "(t)"} are as described above and @{text corr_thm} is a thorem proving @{term "I vs (f t) = I vs t"}. We assume that @{text I} is the interpretation and @{text f} is some useful and executable simplification of type @{text "tau \<Rightarrow> tau"}. The method @{text reflection} applies reification and hence the theorem @{term "t = I xs s"} and hence using @{text corr_thm} derives @{term "t = I xs (f s)"}. It then uses normalization by evaluation to prove @{term "f s = s'"} which almost finishes the proof of @{term "t = t'"} where @{term "I xs s' = t'"}.
 *}
 
 text{* Example 1 : Propositional formulae and NNF.*}
 text{* The type @{text fm} represents simple propositional formulae: *}
+
+datatype form = TrueF | FalseF | Less nat nat |
+                And form form | Or form form | Neg form | ExQ form
+
+fun interp :: "('a::ord) list \<Rightarrow> form \<Rightarrow> bool" where
+"interp e TrueF = True" |
+"interp e FalseF = False" |
+"interp e (Less i j) = (e!i < e!j)" |
+"interp e (And f1 f2) = (interp e f1 & interp e f2)" |
+"interp e (Or f1 f2) = (interp e f1 | interp e f2)" |
+"interp e (Neg f) = (~ interp e f)" |
+"interp e (ExQ f) = (EX x. interp (x#e) f)"
+
+lemmas interp_reify_eqs = interp.simps[where ?'b = int]
+declare interp_reify_eqs(1)[reify add: interp_reify_eqs]
+
+lemma "EX x::int. y < x & x < z"
+  apply reify
+oops
 
 datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
 
 consts Ifm :: "bool list \<Rightarrow> fm \<Rightarrow> bool"
 primrec

   "Ifm vs (Or p q) = (Ifm vs p \<or> Ifm vs q)"
   "Ifm vs (Imp p q) = (Ifm vs p \<longrightarrow> Ifm vs q)"
   "Ifm vs (Iff p q) = (Ifm vs p = Ifm vs q)"
   "Ifm vs (NOT p) = (\<not> (Ifm vs p))"
 
+lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
+apply (reify Ifm.simps)
+oops
+
+  text{* Method @{text reify} maps a bool to an fm. For this it needs the 
+  semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
+
+
+  (* You can also just pick up a subterm to reify \<dots> *)
+lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
+apply (reify Ifm.simps ("((~ D) & (~ F))"))
+oops
+
+  text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
 consts fmsize :: "fm \<Rightarrow> nat"
 primrec
   "fmsize (At n) = 1"
   "fmsize (NOT p) = 1 + fmsize p"
   "fmsize (And p q) = 1 + fmsize p + fmsize q"
   "fmsize (Or p q) = 1 + fmsize p + fmsize q"
   "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
   "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
 
-
-
-  text{* Method @{text reify} maps a bool to an fm. For this it needs the 
-  semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
-lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
-apply (reify Ifm.simps)
-oops
-
-  (* You can also just pick up a subterm to reify \<dots> *)
-lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
-apply (reify Ifm.simps ("((~ D) & (~ F))"))
-oops
-
-  text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
 consts nnf :: "fm \<Rightarrow> fm"
 recdef nnf "measure fmsize"
   "nnf (At n) = At n"
   "nnf (And p q) = And (nnf p) (nnf q)"
   "nnf (Or p q) = Or (nnf p) (nnf q)"

   "Isgn vs (And p q) = (Isgn vs p \<and> Isgn vs q)"
   "Isgn vs (Or p q) = (Isgn vs p \<or> Isgn vs q)"
 
 lemmas eqs = Isgn.simps Iprod.simps
 
-lemma "(x::int)^4 * y * z * y^2 * z^23 > 0"
+lemma "(x::'a::{ordered_idom, recpower})^4 * y * z * y^2 * z^23 > 0"
   apply (reify eqs)
   oops
 
-
 end