tuned, particulary name
authorhaftmann
Wed Feb 13 13:38:52 2013 +0100 (2013-02-13)
changeset 510939d7aa2bb097b
parent 51092 5e6398b48030
child 51094 84b03c49c223
tuned, particulary name
src/HOL/ROOT
src/HOL/ex/ReflectionEx.thy
src/HOL/ex/Reflection_Examples.thy
     1.1 --- a/src/HOL/ROOT	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/HOL/ROOT	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -446,7 +446,7 @@
     1.4      Termination
     1.5      Coherent
     1.6      PresburgerEx
     1.7 -    ReflectionEx
     1.8 +    Reflection_Examples
     1.9      Sqrt
    1.10      Sqrt_Script
    1.11      Transfer_Ex
     2.1 --- a/src/HOL/ex/ReflectionEx.thy	Wed Feb 13 13:38:52 2013 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,422 +0,0 @@
     2.4 -(*  Title:      HOL/ex/ReflectionEx.thy
     2.5 -    Author:     Amine Chaieb, TU Muenchen
     2.6 -*)
     2.7 -
     2.8 -header {* Examples for generic reflection and reification *}
     2.9 -
    2.10 -theory ReflectionEx
    2.11 -imports "~~/src/HOL/Library/Reflection"
    2.12 -begin
    2.13 -
    2.14 -text{* This theory presents two methods: reify and reflection *}
    2.15 -
    2.16 -text{* 
    2.17 -Consider an HOL type 'a, the structure of which is not recongnisable on the theory level. This is the case of bool, arithmetical terms such as int, real etc \dots
    2.18 -In order to implement a simplification on terms of type 'a we often need its structure.
    2.19 -Traditionnaly such simplifications are written in ML, proofs are synthesized.
    2.20 -An other strategy is to declare an HOL-datatype tau and an HOL function (the interpretation) that maps elements of tau to elements of 'a. The functionality of @{text reify} is to compute a term s::tau, which is the representant of t. For this it needs equations for the interpretation.
    2.21 -
    2.22 -NB: All the interpretations supported by @{text reify} must have the type @{text "'b list \<Rightarrow> tau \<Rightarrow> 'a"}.
    2.23 -The method @{text reify} can also be told which subterm of the current subgoal should be reified. The general call for @{text reify} is: @{text "reify eqs (t)"}, where @{text eqs} are the defining equations of the interpretation and @{text "(t)"} is an optional parameter which specifies the subterm to which reification should be applied to. If @{text "(t)"} is abscent, @{text reify} tries to reify the whole subgoal.
    2.24 -
    2.25 -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'"}.
    2.26 -*}
    2.27 -
    2.28 -text{* Example 1 : Propositional formulae and NNF.*}
    2.29 -text{* The type @{text fm} represents simple propositional formulae: *}
    2.30 -
    2.31 -datatype form = TrueF | FalseF | Less nat nat |
    2.32 -                And form form | Or form form | Neg form | ExQ form
    2.33 -
    2.34 -fun interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool" where
    2.35 -"interp TrueF e = True" |
    2.36 -"interp FalseF e = False" |
    2.37 -"interp (Less i j) e = (e!i < e!j)" |
    2.38 -"interp (And f1 f2) e = (interp f1 e & interp f2 e)" |
    2.39 -"interp (Or f1 f2) e = (interp f1 e | interp f2 e)" |
    2.40 -"interp (Neg f) e = (~ interp f e)" |
    2.41 -"interp (ExQ f) e = (EX x. interp f (x#e))"
    2.42 -
    2.43 -lemmas interp_reify_eqs = interp.simps
    2.44 -declare interp_reify_eqs[reify]
    2.45 -
    2.46 -lemma "EX x. x < y & x < z"
    2.47 -  apply (reify )
    2.48 -  oops
    2.49 -
    2.50 -datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
    2.51 -
    2.52 -primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool" where
    2.53 -  "Ifm (At n) vs = vs!n"
    2.54 -| "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
    2.55 -| "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
    2.56 -| "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
    2.57 -| "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
    2.58 -| "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
    2.59 -
    2.60 -lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
    2.61 -apply (reify Ifm.simps)
    2.62 -oops
    2.63 -
    2.64 -  text{* Method @{text reify} maps a bool to an fm. For this it needs the 
    2.65 -  semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
    2.66 -
    2.67 -
    2.68 -  (* You can also just pick up a subterm to reify \<dots> *)
    2.69 -lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
    2.70 -apply (reify Ifm.simps ("((~ D) & (~ F))"))
    2.71 -oops
    2.72 -
    2.73 -  text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
    2.74 -primrec fmsize :: "fm \<Rightarrow> nat" where
    2.75 -  "fmsize (At n) = 1"
    2.76 -| "fmsize (NOT p) = 1 + fmsize p"
    2.77 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    2.78 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    2.79 -| "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
    2.80 -| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
    2.81 -
    2.82 -lemma [measure_function]: "is_measure fmsize" ..
    2.83 -
    2.84 -fun nnf :: "fm \<Rightarrow> fm"
    2.85 -where
    2.86 -  "nnf (At n) = At n"
    2.87 -| "nnf (And p q) = And (nnf p) (nnf q)"
    2.88 -| "nnf (Or p q) = Or (nnf p) (nnf q)"
    2.89 -| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
    2.90 -| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
    2.91 -| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
    2.92 -| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
    2.93 -| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
    2.94 -| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
    2.95 -| "nnf (NOT (NOT p)) = nnf p"
    2.96 -| "nnf (NOT p) = NOT p"
    2.97 -
    2.98 -  text{* The correctness theorem of nnf: it preserves the semantics of fm *}
    2.99 -lemma nnf[reflection]: "Ifm (nnf p) vs = Ifm p vs"
   2.100 -  by (induct p rule: nnf.induct) auto
   2.101 -
   2.102 -  text{* Now let's perform NNF using our @{term nnf} function defined above. First to the whole subgoal. *}
   2.103 -lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
   2.104 -apply (reflection Ifm.simps)
   2.105 -oops
   2.106 -
   2.107 -  text{* Now we specify on which subterm it should be applied*}
   2.108 -lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
   2.109 -apply (reflection Ifm.simps only: "(B | C \<and> (B \<longrightarrow> A | D))")
   2.110 -oops
   2.111 -
   2.112 -
   2.113 -  (* Example 2 : Simple arithmetic formulae *)
   2.114 -
   2.115 -  text{* The type @{text num} reflects linear expressions over natural number *}
   2.116 -datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
   2.117 -
   2.118 -text{* This is just technical to make recursive definitions easier. *}
   2.119 -primrec num_size :: "num \<Rightarrow> nat" 
   2.120 -where
   2.121 -  "num_size (C c) = 1"
   2.122 -| "num_size (Var n) = 1"
   2.123 -| "num_size (Add a b) = 1 + num_size a + num_size b"
   2.124 -| "num_size (Mul c a) = 1 + num_size a"
   2.125 -| "num_size (CN n c a) = 4 + num_size a "
   2.126 -
   2.127 -  text{* The semantics of num *}
   2.128 -primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
   2.129 -where
   2.130 -  Inum_C  : "Inum (C i) vs = i"
   2.131 -| Inum_Var: "Inum (Var n) vs = vs!n"
   2.132 -| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
   2.133 -| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
   2.134 -| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
   2.135 -
   2.136 -
   2.137 -  text{* Let's reify some nat expressions \dots *}
   2.138 -lemma "4 * (2*x + (y::nat)) + f a \<noteq> 0"
   2.139 -  apply (reify Inum.simps ("4 * (2*x + (y::nat)) + f a"))
   2.140 -oops
   2.141 -text{* We're in a bad situation!! x, y and f a have been recongnized as a constants, which is correct but does not correspond to our intuition of the constructor C. It should encapsulate constants, i.e. numbers, i.e. numerals.*}
   2.142 -
   2.143 -  text{* So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots*}
   2.144 -lemma "4 * (2*x + (y::nat)) \<noteq> 0"
   2.145 -  apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2*x + (y::nat))"))
   2.146 -oops
   2.147 -text{* Hmmm let's specialize @{text Inum_C} with numerals.*}
   2.148 -
   2.149 -lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
   2.150 -lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
   2.151 -
   2.152 -  text{* Second attempt *}
   2.153 -lemma "1 * (2*x + (y::nat)) \<noteq> 0"
   2.154 -  apply (reify Inum_eqs ("1 * (2*x + (y::nat))"))
   2.155 -oops
   2.156 -  text{* That was fine, so let's try another one \dots *}
   2.157 -
   2.158 -lemma "1 * (2* x + (y::nat) + 0 + 1) \<noteq> 0"
   2.159 -  apply (reify Inum_eqs ("1 * (2*x + (y::nat) + 0 + 1)"))
   2.160 -oops
   2.161 -  text{* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "numeral"} \dots\ thing. The same for 1. So let's add those equations too *}
   2.162 -
   2.163 -lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
   2.164 -  by simp+
   2.165 -
   2.166 -lemmas Inum_eqs'= Inum_eqs Inum_01
   2.167 -
   2.168 -text{* Third attempt: *}
   2.169 -
   2.170 -lemma "1 * (2*x + (y::nat) + 0 + 1) \<noteq> 0"
   2.171 -  apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)"))
   2.172 -oops
   2.173 -text{* Okay, let's try reflection. Some simplifications on num follow. You can skim until the main theorem @{text linum} *}
   2.174 -fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
   2.175 -where
   2.176 -  "lin_add (CN n1 c1 r1) (CN n2 c2 r2) =
   2.177 -  (if n1=n2 then 
   2.178 -  (let c = c1 + c2
   2.179 -  in (if c=0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
   2.180 -  else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2))) 
   2.181 -  else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
   2.182 -| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"  
   2.183 -| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)" 
   2.184 -| "lin_add (C b1) (C b2) = C (b1+b2)"
   2.185 -| "lin_add a b = Add a b"
   2.186 -lemma lin_add: "Inum (lin_add t s) bs = Inum (Add t s) bs"
   2.187 -apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
   2.188 -apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   2.189 -by (case_tac "n1 = n2", simp_all add: algebra_simps)
   2.190 -
   2.191 -fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
   2.192 -where
   2.193 -  "lin_mul (C j) i = C (i*j)"
   2.194 -| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
   2.195 -| "lin_mul t i = (Mul i t)"
   2.196 -
   2.197 -lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
   2.198 -by (induct t i rule: lin_mul.induct, auto simp add: algebra_simps)
   2.199 -
   2.200 -lemma [measure_function]: "is_measure num_size" ..
   2.201 -
   2.202 -fun linum:: "num \<Rightarrow> num"
   2.203 -where
   2.204 -  "linum (C b) = C b"
   2.205 -| "linum (Var n) = CN n 1 (C 0)"
   2.206 -| "linum (Add t s) = lin_add (linum t) (linum s)"
   2.207 -| "linum (Mul c t) = lin_mul (linum t) c"
   2.208 -| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
   2.209 -
   2.210 -lemma linum[reflection] : "Inum (linum t) bs = Inum t bs"
   2.211 -by (induct t rule: linum.induct, simp_all add: lin_mul lin_add)
   2.212 -
   2.213 -  text{* Now we can use linum to simplify nat terms using reflection *}
   2.214 -lemma "(Suc (Suc 1)) * (x + (Suc 1)*y) = 3*x + 6*y"
   2.215 - apply (reflection Inum_eqs' only: "(Suc (Suc 1)) * (x + (Suc 1)*y)") 
   2.216 -oops
   2.217 -
   2.218 -  text{* Let's lift this to formulae and see what happens *}
   2.219 -
   2.220 -datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   2.221 -  Conj aform aform | Disj aform aform | NEG aform | T | F
   2.222 -
   2.223 -primrec linaformsize:: "aform \<Rightarrow> nat"
   2.224 -where
   2.225 -  "linaformsize T = 1"
   2.226 -| "linaformsize F = 1"
   2.227 -| "linaformsize (Lt a b) = 1"
   2.228 -| "linaformsize (Ge a b) = 1"
   2.229 -| "linaformsize (Eq a b) = 1"
   2.230 -| "linaformsize (NEq a b) = 1"
   2.231 -| "linaformsize (NEG p) = 2 + linaformsize p"
   2.232 -| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
   2.233 -| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
   2.234 -
   2.235 -lemma [measure_function]: "is_measure linaformsize" ..
   2.236 -
   2.237 -primrec is_aform :: "aform => nat list => bool"
   2.238 -where
   2.239 -  "is_aform T vs = True"
   2.240 -| "is_aform F vs = False"
   2.241 -| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
   2.242 -| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
   2.243 -| "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
   2.244 -| "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
   2.245 -| "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
   2.246 -| "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
   2.247 -| "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
   2.248 -
   2.249 -  text{* Let's reify and do reflection *}
   2.250 -lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
   2.251 - apply (reify Inum_eqs' is_aform.simps) 
   2.252 -oops
   2.253 -
   2.254 -text{* Note that reification handles several interpretations at the same time*}
   2.255 -lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
   2.256 - apply (reflection Inum_eqs' is_aform.simps only:"x + x + 1") 
   2.257 -oops
   2.258 -
   2.259 -  text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
   2.260 -
   2.261 -fun linaform:: "aform \<Rightarrow> aform"
   2.262 -where
   2.263 -  "linaform (Lt s t) = Lt (linum s) (linum t)"
   2.264 -| "linaform (Eq s t) = Eq (linum s) (linum t)"
   2.265 -| "linaform (Ge s t) = Ge (linum s) (linum t)"
   2.266 -| "linaform (NEq s t) = NEq (linum s) (linum t)"
   2.267 -| "linaform (Conj p q) = Conj (linaform p) (linaform q)"
   2.268 -| "linaform (Disj p q) = Disj (linaform p) (linaform q)"
   2.269 -| "linaform (NEG T) = F"
   2.270 -| "linaform (NEG F) = T"
   2.271 -| "linaform (NEG (Lt a b)) = Ge a b"
   2.272 -| "linaform (NEG (Ge a b)) = Lt a b"
   2.273 -| "linaform (NEG (Eq a b)) = NEq a b"
   2.274 -| "linaform (NEG (NEq a b)) = Eq a b"
   2.275 -| "linaform (NEG (NEG p)) = linaform p"
   2.276 -| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
   2.277 -| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
   2.278 -| "linaform p = p"
   2.279 -
   2.280 -lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
   2.281 -  by (induct p rule: linaform.induct) (auto simp add: linum)
   2.282 -
   2.283 -lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0  + Suc 0< 0)"
   2.284 -   apply (reflection Inum_eqs' is_aform.simps rules: linaform)  
   2.285 -oops
   2.286 -
   2.287 -declare linaform[reflection]
   2.288 -lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0  + Suc 0< 0)"
   2.289 -   apply (reflection Inum_eqs' is_aform.simps)
   2.290 -oops
   2.291 -
   2.292 -text{* We now give an example where Interpretaions have 0 or more than only one envornement of different types and show that automatic reification also deals with binding *}
   2.293 -datatype rb = BC bool| BAnd rb rb | BOr rb rb
   2.294 -primrec Irb :: "rb \<Rightarrow> bool"
   2.295 -where
   2.296 -  "Irb (BC p) = p"
   2.297 -| "Irb (BAnd s t) = (Irb s \<and> Irb t)"
   2.298 -| "Irb (BOr s t) = (Irb s \<or> Irb t)"
   2.299 -
   2.300 -lemma "A \<and> (B \<or> D \<and> B) \<and> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B)"
   2.301 -apply (reify Irb.simps)
   2.302 -oops
   2.303 -
   2.304 -
   2.305 -datatype rint = IC int| IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint
   2.306 -primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
   2.307 -where
   2.308 -  Irint_Var: "Irint (IVar n) vs = vs!n"
   2.309 -| Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
   2.310 -| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
   2.311 -| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
   2.312 -| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
   2.313 -| Irint_C: "Irint (IC i) vs = i"
   2.314 -lemma Irint_C0: "Irint (IC 0) vs = 0"
   2.315 -  by simp
   2.316 -lemma Irint_C1: "Irint (IC 1) vs = 1"
   2.317 -  by simp
   2.318 -lemma Irint_Cnumeral: "Irint (IC (numeral x)) vs = numeral x"
   2.319 -  by simp
   2.320 -lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumeral
   2.321 -lemma "(3::int) * x + y*y - 9 + (- z) = 0"
   2.322 -  apply (reify Irint_simps ("(3::int) * x + y*y - 9 + (- z)"))
   2.323 -  oops
   2.324 -datatype rlist = LVar nat| LEmpty| LCons rint rlist | LAppend rlist rlist
   2.325 -primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> (int list)"
   2.326 -where
   2.327 -  "Irlist (LEmpty) is vs = []"
   2.328 -| "Irlist (LVar n) is vs = vs!n"
   2.329 -| "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))"
   2.330 -| "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)"
   2.331 -lemma "[(1::int)] = []"
   2.332 -  apply (reify Irlist.simps Irint_simps ("[1]:: int list"))
   2.333 -  oops
   2.334 -
   2.335 -lemma "([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs = [y*y - z - 9 + (3::int) * x]"
   2.336 -  apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs"))
   2.337 -  oops
   2.338 -
   2.339 -datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist
   2.340 -primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> nat"
   2.341 -where
   2.342 -  Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
   2.343 -| Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
   2.344 -| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
   2.345 -| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
   2.346 -| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
   2.347 -| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
   2.348 -| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
   2.349 -| Irnat_C: "Irnat (NC i) is ls vs = i"
   2.350 -lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
   2.351 -by simp
   2.352 -lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
   2.353 -by simp
   2.354 -lemma Irnat_Cnumeral: "Irnat (NC (numeral x)) is ls vs = numeral x"
   2.355 -by simp
   2.356 -lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
   2.357 -  Irnat_C0 Irnat_C1 Irnat_Cnumeral
   2.358 -lemma "(Suc n) * length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs) = length xs"
   2.359 -  apply (reify Irnat_simps Irlist.simps Irint_simps ("(Suc n) *length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs)"))
   2.360 -  oops
   2.361 -datatype rifm = RT | RF | RVar nat
   2.362 -  | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
   2.363 -  |RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
   2.364 -  | RNEX rifm | RIEX rifm| RLEX rifm | RNALL rifm | RIALL rifm| RLALL rifm
   2.365 -  | RBEX rifm | RBALL rifm
   2.366 -
   2.367 -primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
   2.368 -where
   2.369 -  "Irifm RT ps is ls ns = True"
   2.370 -| "Irifm RF ps is ls ns = False"
   2.371 -| "Irifm (RVar n) ps is ls ns = ps!n"
   2.372 -| "Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)"
   2.373 -| "Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)"
   2.374 -| "Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)"
   2.375 -| "Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \<and> Irifm q ps is ls ns)"
   2.376 -| "Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \<or> Irifm q ps is ls ns)"
   2.377 -| "Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns)"
   2.378 -| "Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)"
   2.379 -| "Irifm (RNEX p) ps is ls ns =  (\<exists>x. Irifm p ps is ls (x#ns))"
   2.380 -| "Irifm (RIEX p) ps is ls ns =  (\<exists>x. Irifm p ps (x#is) ls ns)"
   2.381 -| "Irifm (RLEX p) ps is ls ns =  (\<exists>x. Irifm p ps is (x#ls) ns)"
   2.382 -| "Irifm (RBEX p) ps is ls ns =  (\<exists>x. Irifm p (x#ps) is ls ns)"
   2.383 -| "Irifm (RNALL p) ps is ls ns = (\<forall>x. Irifm p ps is ls (x#ns))"
   2.384 -| "Irifm (RIALL p) ps is ls ns = (\<forall>x. Irifm p ps (x#is) ls ns)"
   2.385 -| "Irifm (RLALL p) ps is ls ns = (\<forall>x. Irifm p ps is (x#ls) ns)"
   2.386 -| "Irifm (RBALL p) ps is ls ns = (\<forall>x. Irifm p (x#ps) is ls ns)"
   2.387 -
   2.388 -lemma " \<forall>x. \<exists>n. ((Suc n) * length (([(3::int) * x + (f t)*y - 9 + (- z)] @ []) @ xs) = length xs) \<and> m < 5*n - length (xs @ [2,3,4,x*z + 8 - y]) \<longrightarrow> (\<exists>p. \<forall>q. p \<and> q \<longrightarrow> r)"
   2.389 -  apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
   2.390 -oops
   2.391 -
   2.392 -
   2.393 -(* An example for equations containing type variables *)
   2.394 -datatype prod = Zero | One | Var nat | Mul prod prod 
   2.395 -  | Pw prod nat | PNM nat nat prod
   2.396 -primrec Iprod :: " prod \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>'a" 
   2.397 -where
   2.398 -  "Iprod Zero vs = 0"
   2.399 -| "Iprod One vs = 1"
   2.400 -| "Iprod (Var n) vs = vs!n"
   2.401 -| "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
   2.402 -| "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
   2.403 -| "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
   2.404 -
   2.405 -datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   2.406 -  | Or sgn sgn | And sgn sgn
   2.407 -
   2.408 -primrec Isgn :: " sgn \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>bool"
   2.409 -where 
   2.410 -  "Isgn Tr vs = True"
   2.411 -| "Isgn F vs = False"
   2.412 -| "Isgn (ZeroEq t) vs = (Iprod t vs = 0)"
   2.413 -| "Isgn (NZeroEq t) vs = (Iprod t vs \<noteq> 0)"
   2.414 -| "Isgn (Pos t) vs = (Iprod t vs > 0)"
   2.415 -| "Isgn (Neg t) vs = (Iprod t vs < 0)"
   2.416 -| "Isgn (And p q) vs = (Isgn p vs \<and> Isgn q vs)"
   2.417 -| "Isgn (Or p q) vs = (Isgn p vs \<or> Isgn q vs)"
   2.418 -
   2.419 -lemmas eqs = Isgn.simps Iprod.simps
   2.420 -
   2.421 -lemma "(x::'a::{linordered_idom})^4 * y * z * y^2 * z^23 > 0"
   2.422 -  apply (reify eqs)
   2.423 -  oops
   2.424 -
   2.425 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Reflection_Examples.thy	Wed Feb 13 13:38:52 2013 +0100
     3.3 @@ -0,0 +1,488 @@
     3.4 +(*  Title:      HOL/ex/Reflection_Ex.thy
     3.5 +    Author:     Amine Chaieb, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +header {* Examples for generic reflection and reification *}
     3.9 +
    3.10 +theory Reflection_Examples
    3.11 +imports Complex_Main "~~/src/HOL/Library/Reflection"
    3.12 +begin
    3.13 +
    3.14 +text {* This theory presents two methods: reify and reflection *}
    3.15 +
    3.16 +text {* 
    3.17 +Consider an HOL type @{text \<sigma>}, the structure of which is not recongnisable
    3.18 +on the theory level.  This is the case of @{typ bool}, arithmetical terms such as @{typ int},
    3.19 +@{typ real} etc \dots  In order to implement a simplification on terms of type @{text \<sigma>} we
    3.20 +often need its structure.  Traditionnaly such simplifications are written in ML,
    3.21 +proofs are synthesized.
    3.22 +
    3.23 +An other strategy is to declare an HOL-datatype @{text \<tau>} and an HOL function (the
    3.24 +interpretation) that maps elements of @{text \<tau>} to elements of @{text \<sigma>}.
    3.25 +
    3.26 +The functionality of @{text reify} then is, given a term @{text t} of type @{text \<sigma>},
    3.27 +to compute a term @{text s} of type @{text \<tau>}.  For this it needs equations for the
    3.28 +interpretation.
    3.29 +
    3.30 +N.B: All the interpretations supported by @{text reify} must have the type
    3.31 +@{text "'a list \<Rightarrow> \<tau> \<Rightarrow> \<sigma>"}.  The method @{text reify} can also be told which subterm
    3.32 +of the current subgoal should be reified.  The general call for @{text reify} is
    3.33 +@{text "reify eqs (t)"}, where @{text eqs} are the defining equations of the interpretation
    3.34 +and @{text "(t)"} is an optional parameter which specifies the subterm to which reification
    3.35 +should be applied to.  If @{text "(t)"} is abscent, @{text reify} tries to reify the whole
    3.36 +subgoal.
    3.37 +
    3.38 +The method @{text reflection} uses @{text reify} and has a very similar signature:
    3.39 +@{text "reflection corr_thm eqs (t)"}.  Here again @{text eqs} and @{text "(t)"}
    3.40 +are as described above and @{text corr_thm} is a theorem proving
    3.41 +@{prop "I vs (f t) = I vs t"}.  We assume that @{text I} is the interpretation
    3.42 +and @{text f} is some useful and executable simplification of type @{text "\<tau> \<Rightarrow> \<tau>"}.
    3.43 +The method @{text reflection} applies reification and hence the theorem @{prop "t = I xs s"}
    3.44 +and hence using @{text corr_thm} derives @{prop "t = I xs (f s)"}.  It then uses
    3.45 +normalization by equational rewriting to prove @{prop "f s = s'"} which almost finishes
    3.46 +the proof of @{prop "t = t'"} where @{prop "I xs s' = t'"}.
    3.47 +*}
    3.48 +
    3.49 +text {* Example 1 : Propositional formulae and NNF. *}
    3.50 +text {* The type @{text fm} represents simple propositional formulae: *}
    3.51 +
    3.52 +datatype form = TrueF | FalseF | Less nat nat
    3.53 +  | And form form | Or form form | Neg form | ExQ form
    3.54 +
    3.55 +primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
    3.56 +where
    3.57 +  "interp TrueF vs \<longleftrightarrow> True"
    3.58 +| "interp FalseF vs \<longleftrightarrow> False"
    3.59 +| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
    3.60 +| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
    3.61 +| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
    3.62 +| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
    3.63 +| "interp (ExQ f) vs \<longleftrightarrow> (\<exists>v. interp f (v # vs))"
    3.64 +
    3.65 +lemmas interp_reify_eqs = interp.simps
    3.66 +declare interp_reify_eqs [reify]
    3.67 +
    3.68 +lemma "\<exists>x. x < y \<and> x < z"
    3.69 +  apply reify
    3.70 +  oops
    3.71 +
    3.72 +datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
    3.73 +
    3.74 +primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
    3.75 +where
    3.76 +  "Ifm (At n) vs \<longleftrightarrow> vs ! n"
    3.77 +| "Ifm (And p q) vs \<longleftrightarrow> Ifm p vs \<and> Ifm q vs"
    3.78 +| "Ifm (Or p q) vs \<longleftrightarrow> Ifm p vs \<or> Ifm q vs"
    3.79 +| "Ifm (Imp p q) vs \<longleftrightarrow> Ifm p vs \<longrightarrow> Ifm q vs"
    3.80 +| "Ifm (Iff p q) vs \<longleftrightarrow> Ifm p vs = Ifm q vs"
    3.81 +| "Ifm (NOT p) vs \<longleftrightarrow> \<not> Ifm p vs"
    3.82 +
    3.83 +lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
    3.84 +  apply (reify Ifm.simps)
    3.85 +oops
    3.86 +
    3.87 +text {* Method @{text reify} maps a @{typ bool} to an @{typ fm}.  For this it needs the 
    3.88 +semantics of @{text fm}, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
    3.89 +
    3.90 +text {* You can also just pick up a subterm to reify. *}
    3.91 +lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
    3.92 +  apply (reify Ifm.simps ("((\<not> D) \<and> (\<not> F))"))
    3.93 +oops
    3.94 +
    3.95 +text {* Let's perform NNF. This is a version that tends to generate disjunctions *}
    3.96 +primrec fmsize :: "fm \<Rightarrow> nat"
    3.97 +where
    3.98 +  "fmsize (At n) = 1"
    3.99 +| "fmsize (NOT p) = 1 + fmsize p"
   3.100 +| "fmsize (And p q) = 1 + fmsize p + fmsize q"
   3.101 +| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
   3.102 +| "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
   3.103 +| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
   3.104 +
   3.105 +lemma [measure_function]: "is_measure fmsize" ..
   3.106 +
   3.107 +fun nnf :: "fm \<Rightarrow> fm"
   3.108 +where
   3.109 +  "nnf (At n) = At n"
   3.110 +| "nnf (And p q) = And (nnf p) (nnf q)"
   3.111 +| "nnf (Or p q) = Or (nnf p) (nnf q)"
   3.112 +| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
   3.113 +| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
   3.114 +| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
   3.115 +| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
   3.116 +| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
   3.117 +| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
   3.118 +| "nnf (NOT (NOT p)) = nnf p"
   3.119 +| "nnf (NOT p) = NOT p"
   3.120 +
   3.121 +text {* The correctness theorem of @{const nnf}: it preserves the semantics of @{typ fm} *}
   3.122 +lemma nnf [reflection]:
   3.123 +  "Ifm (nnf p) vs = Ifm p vs"
   3.124 +  by (induct p rule: nnf.induct) auto
   3.125 +
   3.126 +text {* Now let's perform NNF using our @{const nnf} function defined above.  First to the
   3.127 +  whole subgoal. *}
   3.128 +lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
   3.129 +  apply (reflection Ifm.simps)
   3.130 +oops
   3.131 +
   3.132 +text {* Now we specify on which subterm it should be applied *}
   3.133 +lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
   3.134 +  apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)")
   3.135 +  apply code_simp
   3.136 +oops
   3.137 +
   3.138 +
   3.139 +text {* Example 2: Simple arithmetic formulae *}
   3.140 +
   3.141 +text {* The type @{text num} reflects linear expressions over natural number *}
   3.142 +datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
   3.143 +
   3.144 +text {* This is just technical to make recursive definitions easier. *}
   3.145 +primrec num_size :: "num \<Rightarrow> nat" 
   3.146 +where
   3.147 +  "num_size (C c) = 1"
   3.148 +| "num_size (Var n) = 1"
   3.149 +| "num_size (Add a b) = 1 + num_size a + num_size b"
   3.150 +| "num_size (Mul c a) = 1 + num_size a"
   3.151 +| "num_size (CN n c a) = 4 + num_size a "
   3.152 +
   3.153 +lemma [measure_function]: "is_measure num_size" ..
   3.154 +
   3.155 +text {* The semantics of num *}
   3.156 +primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
   3.157 +where
   3.158 +  Inum_C  : "Inum (C i) vs = i"
   3.159 +| Inum_Var: "Inum (Var n) vs = vs!n"
   3.160 +| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
   3.161 +| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
   3.162 +| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
   3.163 +
   3.164 +text {* Let's reify some nat expressions \dots *}
   3.165 +lemma "4 * (2 * x + (y::nat)) + f a \<noteq> 0"
   3.166 +  apply (reify Inum.simps ("4 * (2 * x + (y::nat)) + f a"))
   3.167 +oops
   3.168 +text {* We're in a bad situation! @{text x}, @{text y} and @{text f} have been recongnized
   3.169 +as constants, which is correct but does not correspond to our intuition of the constructor C.
   3.170 +It should encapsulate constants, i.e. numbers, i.e. numerals. *}
   3.171 +
   3.172 +text {* So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots*}
   3.173 +lemma "4 * (2 * x + (y::nat)) \<noteq> 0"
   3.174 +  apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2 * x + (y::nat))"))
   3.175 +oops
   3.176 +text {* Hm, let's specialize @{text Inum_C} with numerals.*}
   3.177 +
   3.178 +lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
   3.179 +lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
   3.180 +
   3.181 +text {* Second attempt *}
   3.182 +lemma "1 * (2 * x + (y::nat)) \<noteq> 0"
   3.183 +  apply (reify Inum_eqs ("1 * (2 * x + (y::nat))"))
   3.184 +oops
   3.185 +
   3.186 +text{* That was fine, so let's try another one \dots *}
   3.187 +
   3.188 +lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
   3.189 +  apply (reify Inum_eqs ("1 * (2 * x + (y::nat) + 0 + 1)"))
   3.190 +oops
   3.191 +
   3.192 +text {* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "numeral"} \dots\ thing.
   3.193 +The same for 1. So let's add those equations, too. *}
   3.194 +
   3.195 +lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
   3.196 +  by simp_all
   3.197 +
   3.198 +lemmas Inum_eqs'= Inum_eqs Inum_01
   3.199 +
   3.200 +text{* Third attempt: *}
   3.201 +
   3.202 +lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
   3.203 +  apply (reify Inum_eqs' ("1 * (2 * x + (y::nat) + 0 + 1)"))
   3.204 +oops
   3.205 +
   3.206 +text {* Okay, let's try reflection. Some simplifications on @{typ num} follow. You can
   3.207 +  skim until the main theorem @{text linum}. *}
   3.208 +  
   3.209 +fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
   3.210 +where
   3.211 +  "lin_add (CN n1 c1 r1) (CN n2 c2 r2) =
   3.212 +    (if n1 = n2 then 
   3.213 +      (let c = c1 + c2
   3.214 +       in (if c = 0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
   3.215 +     else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2))) 
   3.216 +     else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
   3.217 +| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"  
   3.218 +| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)" 
   3.219 +| "lin_add (C b1) (C b2) = C (b1 + b2)"
   3.220 +| "lin_add a b = Add a b"
   3.221 +
   3.222 +lemma lin_add:
   3.223 +  "Inum (lin_add t s) bs = Inum (Add t s) bs"
   3.224 +  apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
   3.225 +  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   3.226 +  apply (case_tac "n1 = n2", simp_all add: algebra_simps)
   3.227 +  done
   3.228 +
   3.229 +fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
   3.230 +where
   3.231 +  "lin_mul (C j) i = C (i * j)"
   3.232 +| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i * c) (lin_mul a i))"
   3.233 +| "lin_mul t i = (Mul i t)"
   3.234 +
   3.235 +lemma lin_mul:
   3.236 +  "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
   3.237 +  by (induct t i rule: lin_mul.induct) (auto simp add: algebra_simps)
   3.238 +
   3.239 +fun linum:: "num \<Rightarrow> num"
   3.240 +where
   3.241 +  "linum (C b) = C b"
   3.242 +| "linum (Var n) = CN n 1 (C 0)"
   3.243 +| "linum (Add t s) = lin_add (linum t) (linum s)"
   3.244 +| "linum (Mul c t) = lin_mul (linum t) c"
   3.245 +| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
   3.246 +
   3.247 +lemma linum [reflection]:
   3.248 +  "Inum (linum t) bs = Inum t bs"
   3.249 +  by (induct t rule: linum.induct) (simp_all add: lin_mul lin_add)
   3.250 +
   3.251 +text {* Now we can use linum to simplify nat terms using reflection *}
   3.252 +
   3.253 +lemma "Suc (Suc 1) * (x + Suc 1 * y) = 3 * x + 6 * y"
   3.254 +  apply (reflection Inum_eqs' only: "Suc (Suc 1) * (x + Suc 1 * y)")
   3.255 +oops
   3.256 +
   3.257 +text {* Let's lift this to formulae and see what happens *}
   3.258 +
   3.259 +datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   3.260 +  Conj aform aform | Disj aform aform | NEG aform | T | F
   3.261 +
   3.262 +primrec linaformsize:: "aform \<Rightarrow> nat"
   3.263 +where
   3.264 +  "linaformsize T = 1"
   3.265 +| "linaformsize F = 1"
   3.266 +| "linaformsize (Lt a b) = 1"
   3.267 +| "linaformsize (Ge a b) = 1"
   3.268 +| "linaformsize (Eq a b) = 1"
   3.269 +| "linaformsize (NEq a b) = 1"
   3.270 +| "linaformsize (NEG p) = 2 + linaformsize p"
   3.271 +| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
   3.272 +| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
   3.273 +
   3.274 +lemma [measure_function]: "is_measure linaformsize" ..
   3.275 +
   3.276 +primrec is_aform :: "aform => nat list => bool"
   3.277 +where
   3.278 +  "is_aform T vs = True"
   3.279 +| "is_aform F vs = False"
   3.280 +| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
   3.281 +| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
   3.282 +| "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
   3.283 +| "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
   3.284 +| "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
   3.285 +| "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
   3.286 +| "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
   3.287 +
   3.288 +text{* Let's reify and do reflection *}
   3.289 +lemma "(3::nat) * x + t < 0 \<and> (2 * x + y \<noteq> 17)"
   3.290 +  apply (reify Inum_eqs' is_aform.simps) 
   3.291 +oops
   3.292 +
   3.293 +text {* Note that reification handles several interpretations at the same time*}
   3.294 +lemma "(3::nat) * x + t < 0 \<and> x * x + t * x + 3 + 1 = z * t * 4 * z \<or> x + x + 1 < 0"
   3.295 +  apply (reflection Inum_eqs' is_aform.simps only: "x + x + 1") 
   3.296 +oops
   3.297 +
   3.298 +text {* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
   3.299 +
   3.300 +fun linaform:: "aform \<Rightarrow> aform"
   3.301 +where
   3.302 +  "linaform (Lt s t) = Lt (linum s) (linum t)"
   3.303 +| "linaform (Eq s t) = Eq (linum s) (linum t)"
   3.304 +| "linaform (Ge s t) = Ge (linum s) (linum t)"
   3.305 +| "linaform (NEq s t) = NEq (linum s) (linum t)"
   3.306 +| "linaform (Conj p q) = Conj (linaform p) (linaform q)"
   3.307 +| "linaform (Disj p q) = Disj (linaform p) (linaform q)"
   3.308 +| "linaform (NEG T) = F"
   3.309 +| "linaform (NEG F) = T"
   3.310 +| "linaform (NEG (Lt a b)) = Ge a b"
   3.311 +| "linaform (NEG (Ge a b)) = Lt a b"
   3.312 +| "linaform (NEG (Eq a b)) = NEq a b"
   3.313 +| "linaform (NEG (NEq a b)) = Eq a b"
   3.314 +| "linaform (NEG (NEG p)) = linaform p"
   3.315 +| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
   3.316 +| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
   3.317 +| "linaform p = p"
   3.318 +
   3.319 +lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
   3.320 +  by (induct p rule: linaform.induct) (auto simp add: linum)
   3.321 +
   3.322 +lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
   3.323 +  (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
   3.324 +  apply (reflection Inum_eqs' is_aform.simps rules: linaform)  
   3.325 +oops
   3.326 +
   3.327 +declare linaform [reflection]
   3.328 +
   3.329 +lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
   3.330 +  (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
   3.331 +  apply (reflection Inum_eqs' is_aform.simps)
   3.332 +oops
   3.333 +
   3.334 +text {* We now give an example where interpretaions have zero or more than only
   3.335 +  one envornement of different types and show that automatic reification also deals with
   3.336 +  bindings *}
   3.337 +  
   3.338 +datatype rb = BC bool | BAnd rb rb | BOr rb rb
   3.339 +
   3.340 +primrec Irb :: "rb \<Rightarrow> bool"
   3.341 +where
   3.342 +  "Irb (BC p) \<longleftrightarrow> p"
   3.343 +| "Irb (BAnd s t) \<longleftrightarrow> Irb s \<and> Irb t"
   3.344 +| "Irb (BOr s t) \<longleftrightarrow> Irb s \<or> Irb t"
   3.345 +
   3.346 +lemma "A \<and> (B \<or> D \<and> B) \<and> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B)"
   3.347 +  apply (reify Irb.simps)
   3.348 +oops
   3.349 +
   3.350 +datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
   3.351 +  | INeg rint | ISub rint rint
   3.352 +
   3.353 +primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
   3.354 +where
   3.355 +  Irint_Var: "Irint (IVar n) vs = vs ! n"
   3.356 +| Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
   3.357 +| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
   3.358 +| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
   3.359 +| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
   3.360 +| Irint_C: "Irint (IC i) vs = i"
   3.361 +
   3.362 +lemma Irint_C0: "Irint (IC 0) vs = 0"
   3.363 +  by simp
   3.364 +
   3.365 +lemma Irint_C1: "Irint (IC 1) vs = 1"
   3.366 +  by simp
   3.367 +
   3.368 +lemma Irint_Cnumeral: "Irint (IC (numeral x)) vs = numeral x"
   3.369 +  by simp
   3.370 +
   3.371 +lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumeral
   3.372 +
   3.373 +lemma "(3::int) * x + y * y - 9 + (- z) = 0"
   3.374 +  apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
   3.375 +  oops
   3.376 +
   3.377 +datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
   3.378 +
   3.379 +primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
   3.380 +where
   3.381 +  "Irlist (LEmpty) is vs = []"
   3.382 +| "Irlist (LVar n) is vs = vs ! n"
   3.383 +| "Irlist (LCons i t) is vs = Irint i is # Irlist t is vs"
   3.384 +| "Irlist (LAppend s t) is vs = Irlist s is vs @ Irlist t is vs"
   3.385 +
   3.386 +lemma "[(1::int)] = []"
   3.387 +  apply (reify Irlist.simps Irint_simps ("[1] :: int list"))
   3.388 +  oops
   3.389 +
   3.390 +lemma "([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs = [y * y - z - 9 + (3::int) * x]"
   3.391 +  apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
   3.392 +  oops
   3.393 +
   3.394 +datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
   3.395 +  | NNeg rnat | NSub rnat rnat | Nlgth rlist
   3.396 +
   3.397 +primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
   3.398 +where
   3.399 +  Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
   3.400 +| Irnat_Var: "Irnat (NVar n) is ls vs = vs ! n"
   3.401 +| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
   3.402 +| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
   3.403 +| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
   3.404 +| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
   3.405 +| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
   3.406 +| Irnat_C: "Irnat (NC i) is ls vs = i"
   3.407 +
   3.408 +lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
   3.409 +  by simp
   3.410 +
   3.411 +lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
   3.412 +  by simp
   3.413 +
   3.414 +lemma Irnat_Cnumeral: "Irnat (NC (numeral x)) is ls vs = numeral x"
   3.415 +  by simp
   3.416 +
   3.417 +lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
   3.418 +  Irnat_C0 Irnat_C1 Irnat_Cnumeral
   3.419 +
   3.420 +lemma "Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs) = length xs"
   3.421 +  apply (reify Irnat_simps Irlist.simps Irint_simps
   3.422 +     ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
   3.423 +  oops
   3.424 +
   3.425 +datatype rifm = RT | RF | RVar nat
   3.426 +  | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
   3.427 +  | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
   3.428 +  | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
   3.429 +  | RBEX rifm | RBALL rifm
   3.430 +
   3.431 +primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
   3.432 +where
   3.433 +  "Irifm RT ps is ls ns \<longleftrightarrow> True"
   3.434 +| "Irifm RF ps is ls ns \<longleftrightarrow> False"
   3.435 +| "Irifm (RVar n) ps is ls ns \<longleftrightarrow> ps ! n"
   3.436 +| "Irifm (RNLT s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns < Irnat t is ls ns"
   3.437 +| "Irifm (RNILT s t) ps is ls ns \<longleftrightarrow> int (Irnat s is ls ns) < Irint t is"
   3.438 +| "Irifm (RNEQ s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns = Irnat t is ls ns"
   3.439 +| "Irifm (RAnd p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<and> Irifm q ps is ls ns"
   3.440 +| "Irifm (ROr p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<or> Irifm q ps is ls ns"
   3.441 +| "Irifm (RImp p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns"
   3.442 +| "Irifm (RIff p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns = Irifm q ps is ls ns"
   3.443 +| "Irifm (RNEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is ls (x # ns))"
   3.444 +| "Irifm (RIEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps (x # is) ls ns)"
   3.445 +| "Irifm (RLEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is (x # ls) ns)"
   3.446 +| "Irifm (RBEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p (x # ps) is ls ns)"
   3.447 +| "Irifm (RNALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is ls (x#ns))"
   3.448 +| "Irifm (RIALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps (x # is) ls ns)"
   3.449 +| "Irifm (RLALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is (x#ls) ns)"
   3.450 +| "Irifm (RBALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p (x # ps) is ls ns)"
   3.451 +
   3.452 +lemma " \<forall>x. \<exists>n. ((Suc n) * length (([(3::int) * x + f t * y - 9 + (- z)] @ []) @ xs) = length xs) \<and> m < 5*n - length (xs @ [2,3,4,x*z + 8 - y]) \<longrightarrow> (\<exists>p. \<forall>q. p \<and> q \<longrightarrow> r)"
   3.453 +  apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
   3.454 +oops
   3.455 +
   3.456 +text {* An example for equations containing type variables *}
   3.457 +
   3.458 +datatype prod = Zero | One | Var nat | Mul prod prod 
   3.459 +  | Pw prod nat | PNM nat nat prod
   3.460 +
   3.461 +primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
   3.462 +where
   3.463 +  "Iprod Zero vs = 0"
   3.464 +| "Iprod One vs = 1"
   3.465 +| "Iprod (Var n) vs = vs ! n"
   3.466 +| "Iprod (Mul a b) vs = Iprod a vs * Iprod b vs"
   3.467 +| "Iprod (Pw a n) vs = Iprod a vs ^ n"
   3.468 +| "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
   3.469 +
   3.470 +datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   3.471 +  | Or sgn sgn | And sgn sgn
   3.472 +
   3.473 +primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
   3.474 +where 
   3.475 +  "Isgn Tr vs \<longleftrightarrow> True"
   3.476 +| "Isgn F vs \<longleftrightarrow> False"
   3.477 +| "Isgn (ZeroEq t) vs \<longleftrightarrow> Iprod t vs = 0"
   3.478 +| "Isgn (NZeroEq t) vs \<longleftrightarrow> Iprod t vs \<noteq> 0"
   3.479 +| "Isgn (Pos t) vs \<longleftrightarrow> Iprod t vs > 0"
   3.480 +| "Isgn (Neg t) vs \<longleftrightarrow> Iprod t vs < 0"
   3.481 +| "Isgn (And p q) vs \<longleftrightarrow> Isgn p vs \<and> Isgn q vs"
   3.482 +| "Isgn (Or p q) vs \<longleftrightarrow> Isgn p vs \<or> Isgn q vs"
   3.483 +
   3.484 +lemmas eqs = Isgn.simps Iprod.simps
   3.485 +
   3.486 +lemma "(x::'a::{linordered_idom}) ^ 4 * y * z * y ^ 2 * z ^ 23 > 0"
   3.487 +  apply (reify eqs)
   3.488 +  oops
   3.489 +
   3.490 +end
   3.491 +