# HG changeset patch
# User chaieb
# Date 1183477798 -7200
# Node ID cb1203d8897c09fb44f7effc5576d7ff751f1e78
# Parent  c8a1bd9585a086bcbbce286c3fe0e118a99fb566
More examples

diff -r c8a1bd9585a0 -r cb1203d8897c src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Tue Jul 03 17:49:55 2007 +0200
+++ b/src/HOL/ex/ReflectionEx.thy	Tue Jul 03 17:49:58 2007 +0200
@@ -4,7 +4,6 @@
 *)
 
 header {* Examples for generic reflection and reification *}
-
 theory ReflectionEx
 imports Reflection
 begin
@@ -26,6 +25,25 @@
 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"
@@ -37,6 +55,20 @@
   "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"
@@ -46,20 +78,6 @@
   "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"
@@ -384,9 +402,8 @@
 
 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