src/HOL/ex/ReflectionEx.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29668 33ba3faeaa0e child 31021 53642251a04f permissions -rw-r--r--
1 (*  Title:      HOL/ex/ReflectionEx.thy
2     Author:     Amine Chaieb, TU Muenchen
3 *)
5 header {* Examples for generic reflection and reification *}
7 theory ReflectionEx
8 imports Reflection
9 begin
11 text{* This theory presents two methods: reify and reflection *}
13 text{*
14 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
15 In order to implement a simplification on terms of type 'a we often need its structure.
16 Traditionnaly such simplifications are written in ML, proofs are synthesized.
17 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.
19 NB: All the interpretations supported by @{text reify} must have the type @{text "'b list \<Rightarrow> tau \<Rightarrow> 'a"}.
20 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.
22 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'"}.
23 *}
25 text{* Example 1 : Propositional formulae and NNF.*}
26 text{* The type @{text fm} represents simple propositional formulae: *}
28 datatype form = TrueF | FalseF | Less nat nat |
29                 And form form | Or form form | Neg form | ExQ form
31 fun interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool" where
32 "interp TrueF e = True" |
33 "interp FalseF e = False" |
34 "interp (Less i j) e = (e!i < e!j)" |
35 "interp (And f1 f2) e = (interp f1 e & interp f2 e)" |
36 "interp (Or f1 f2) e = (interp f1 e | interp f2 e)" |
37 "interp (Neg f) e = (~ interp f e)" |
38 "interp (ExQ f) e = (EX x. interp f (x#e))"
40 lemmas interp_reify_eqs = interp.simps
41 declare interp_reify_eqs[reify]
43 lemma "EX x. x < y & x < z"
44   apply (reify )
45   oops
47 datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
49 consts Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
50 primrec
51   "Ifm (At n) vs = vs!n"
52   "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
53   "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
54   "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
55   "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
56   "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
58 lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
59 apply (reify Ifm.simps)
60 oops
62   text{* Method @{text reify} maps a bool to an fm. For this it needs the
63   semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
66   (* You can also just pick up a subterm to reify \<dots> *)
67 lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
68 apply (reify Ifm.simps ("((~ D) & (~ F))"))
69 oops
71   text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
72 consts fmsize :: "fm \<Rightarrow> nat"
73 primrec
74   "fmsize (At n) = 1"
75   "fmsize (NOT p) = 1 + fmsize p"
76   "fmsize (And p q) = 1 + fmsize p + fmsize q"
77   "fmsize (Or p q) = 1 + fmsize p + fmsize q"
78   "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
79   "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
81 consts nnf :: "fm \<Rightarrow> fm"
82 recdef nnf "measure fmsize"
83   "nnf (At n) = At n"
84   "nnf (And p q) = And (nnf p) (nnf q)"
85   "nnf (Or p q) = Or (nnf p) (nnf q)"
86   "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
87   "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
88   "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
89   "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
90   "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
91   "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
92   "nnf (NOT (NOT p)) = nnf p"
93   "nnf (NOT p) = NOT p"
95   text{* The correctness theorem of nnf: it preserves the semantics of fm *}
96 lemma nnf[reflection]: "Ifm (nnf p) vs = Ifm p vs"
97   by (induct p rule: nnf.induct) auto
99   text{* Now let's perform NNF using our @{term nnf} function defined above. First to the whole subgoal. *}
100 lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
101 apply (reflection Ifm.simps)
102 oops
104   text{* Now we specify on which subterm it should be applied*}
105 lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
106 apply (reflection Ifm.simps only: "(B | C \<and> (B \<longrightarrow> A | D))")
107 oops
110   (* Example 2 : Simple arithmetic formulae *)
112   text{* The type @{text num} reflects linear expressions over natural number *}
113 datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
115 text{* This is just technical to make recursive definitions easier. *}
116 consts num_size :: "num \<Rightarrow> nat"
117 primrec
118   "num_size (C c) = 1"
119   "num_size (Var n) = 1"
120   "num_size (Add a b) = 1 + num_size a + num_size b"
121   "num_size (Mul c a) = 1 + num_size a"
122   "num_size (CN n c a) = 4 + num_size a "
124   text{* The semantics of num *}
125 consts Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
126 primrec
127   Inum_C  : "Inum (C i) vs = i"
128   Inum_Var: "Inum (Var n) vs = vs!n"
129   Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
130   Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
131   Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
134   text{* Let's reify some nat expressions \dots *}
135 lemma "4 * (2*x + (y::nat)) + f a \<noteq> 0"
136   apply (reify Inum.simps ("4 * (2*x + (y::nat)) + f a"))
137 oops
138 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.*}
140   text{* So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots*}
141 lemma "4 * (2*x + (y::nat)) \<noteq> 0"
142   apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2*x + (y::nat))"))
143 oops
144 text{* Hmmm let's specialize @{text Inum_C} with numerals.*}
146 lemma Inum_number: "Inum (C (number_of t)) vs = number_of t" by simp
147 lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
149   text{* Second attempt *}
150 lemma "1 * (2*x + (y::nat)) \<noteq> 0"
151   apply (reify Inum_eqs ("1 * (2*x + (y::nat))"))
152 oops
153   text{* That was fine, so let's try another one \dots *}
155 lemma "1 * (2* x + (y::nat) + 0 + 1) \<noteq> 0"
156   apply (reify Inum_eqs ("1 * (2*x + (y::nat) + 0 + 1)"))
157 oops
158   text{* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "number_of"} \dots\ thing. The same for 1. So let's add those equations too *}
160 lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
161   by simp+
163 lemmas Inum_eqs'= Inum_eqs Inum_01
165 text{* Third attempt: *}
167 lemma "1 * (2*x + (y::nat) + 0 + 1) \<noteq> 0"
168   apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)"))
169 oops
170 text{* Okay, let's try reflection. Some simplifications on num follow. You can skim until the main theorem @{text linum} *}
171 consts lin_add :: "num \<times> num \<Rightarrow> num"
172 recdef lin_add "measure (\<lambda>(x,y). ((size x) + (size y)))"
173   "lin_add (CN n1 c1 r1,CN n2 c2 r2) =
174   (if n1=n2 then
175   (let c = c1 + c2
176   in (if c=0 then lin_add(r1,r2) else CN n1 c (lin_add (r1,r2))))
177   else if n1 \<le> n2 then (CN n1 c1 (lin_add (r1,CN n2 c2 r2)))
178   else (CN n2 c2 (lin_add (CN n1 c1 r1,r2))))"
179   "lin_add (CN n1 c1 r1,t) = CN n1 c1 (lin_add (r1, t))"
180   "lin_add (t,CN n2 c2 r2) = CN n2 c2 (lin_add (t,r2))"
181   "lin_add (C b1, C b2) = C (b1+b2)"
185 apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
186 by (case_tac "n1 = n2", simp_all add: algebra_simps)
188 consts lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
189 recdef lin_mul "measure size "
190   "lin_mul (C j) = (\<lambda> i. C (i*j))"
191   "lin_mul (CN n c a) = (\<lambda> i. if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
192   "lin_mul t = (\<lambda> i. Mul i t)"
194 lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
195 by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: algebra_simps)
197 consts linum:: "num \<Rightarrow> num"
198 recdef linum "measure num_size"
199   "linum (C b) = C b"
200   "linum (Var n) = CN n 1 (C 0)"
202   "linum (Mul c t) = lin_mul (linum t) c"
203   "linum (CN n c t) = lin_add (linum (Mul c (Var n)),linum t)"
205 lemma linum[reflection] : "Inum (linum t) bs = Inum t bs"
208   text{* Now we can use linum to simplify nat terms using reflection *}
209 lemma "(Suc (Suc 1)) * (x + (Suc 1)*y) = 3*x + 6*y"
210  apply (reflection Inum_eqs' only: "(Suc (Suc 1)) * (x + (Suc 1)*y)")
211 oops
213   text{* Let's lift this to formulae and see what happens *}
215 datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num |
216   Conj aform aform | Disj aform aform | NEG aform | T | F
217 consts linaformsize:: "aform \<Rightarrow> nat"
218 recdef linaformsize "measure size"
219   "linaformsize T = 1"
220   "linaformsize F = 1"
221   "linaformsize (Lt a b) = 1"
222   "linaformsize (Ge a b) = 1"
223   "linaformsize (Eq a b) = 1"
224   "linaformsize (NEq a b) = 1"
225   "linaformsize (NEG p) = 2 + linaformsize p"
226   "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
227   "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
230 consts is_aform :: "aform => nat list => bool"
231 primrec
232   "is_aform T vs = True"
233   "is_aform F vs = False"
234   "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
235   "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
236   "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
237   "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
238   "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
239   "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
240   "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
242   text{* Let's reify and do reflection *}
243 lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
244  apply (reify Inum_eqs' is_aform.simps)
245 oops
247 text{* Note that reification handles several interpretations at the same time*}
248 lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
249  apply (reflection Inum_eqs' is_aform.simps only:"x + x + 1")
250 oops
252   text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
253 consts linaform:: "aform \<Rightarrow> aform"
254 recdef linaform "measure linaformsize"
255   "linaform (Lt s t) = Lt (linum s) (linum t)"
256   "linaform (Eq s t) = Eq (linum s) (linum t)"
257   "linaform (Ge s t) = Ge (linum s) (linum t)"
258   "linaform (NEq s t) = NEq (linum s) (linum t)"
259   "linaform (Conj p q) = Conj (linaform p) (linaform q)"
260   "linaform (Disj p q) = Disj (linaform p) (linaform q)"
261   "linaform (NEG T) = F"
262   "linaform (NEG F) = T"
263   "linaform (NEG (Lt a b)) = Ge a b"
264   "linaform (NEG (Ge a b)) = Lt a b"
265   "linaform (NEG (Eq a b)) = NEq a b"
266   "linaform (NEG (NEq a b)) = Eq a b"
267   "linaform (NEG (NEG p)) = linaform p"
268   "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
269   "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
270   "linaform p = p"
272 lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
273   by (induct p rule: linaform.induct) (auto simp add: linum)
275 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)"
276    apply (reflection Inum_eqs' is_aform.simps rules: linaform)
277 oops
279 declare linaform[reflection]
280 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)"
281    apply (reflection Inum_eqs' is_aform.simps)
282 oops
284 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 *}
285 datatype rb = BC bool| BAnd rb rb | BOr rb rb
286 consts Irb :: "rb \<Rightarrow> bool"
287 primrec
288   "Irb (BC p) = p"
289   "Irb (BAnd s t) = (Irb s \<and> Irb t)"
290   "Irb (BOr s t) = (Irb s \<or> Irb t)"
292 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)"
293 apply (reify Irb.simps)
294 oops
297 datatype rint = IC int| IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint
298 consts Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
299 primrec
300 Irint_Var: "Irint (IVar n) vs = vs!n"
301 Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
302 Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
303 Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
304 Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
305 Irint_C: "Irint (IC i) vs = i"
306 lemma Irint_C0: "Irint (IC 0) vs = 0"
307   by simp
308 lemma Irint_C1: "Irint (IC 1) vs = 1"
309   by simp
310 lemma Irint_Cnumberof: "Irint (IC (number_of x)) vs = number_of x"
311   by simp
312 lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumberof
313 lemma "(3::int) * x + y*y - 9 + (- z) = 0"
314   apply (reify Irint_simps ("(3::int) * x + y*y - 9 + (- z)"))
315   oops
316 datatype rlist = LVar nat| LEmpty| LCons rint rlist | LAppend rlist rlist
317 consts Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> (int list)"
318 primrec
319   "Irlist (LEmpty) is vs = []"
320   "Irlist (LVar n) is vs = vs!n"
321   "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))"
322   "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)"
323 lemma "[(1::int)] = []"
324   apply (reify Irlist.simps Irint_simps ("[1]:: int list"))
325   oops
327 lemma "([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs = [y*y - z - 9 + (3::int) * x]"
328   apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs"))
329   oops
331 datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist
332 consts Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> nat"
333 primrec
334 Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
335 Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
336 Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
337 Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
338 Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
339 Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
340 Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
341 Irnat_C: "Irnat (NC i) is ls vs = i"
342 lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
343 by simp
344 lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
345 by simp
346 lemma Irnat_Cnumberof: "Irnat (NC (number_of x)) is ls vs = number_of x"
347 by simp
348 lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
349   Irnat_C0 Irnat_C1 Irnat_Cnumberof
350 lemma "(Suc n) * length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs) = length xs"
351   apply (reify Irnat_simps Irlist.simps Irint_simps ("(Suc n) *length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs)"))
352   oops
353 datatype rifm = RT | RF | RVar nat
354   | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
355   |RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
356   | RNEX rifm | RIEX rifm| RLEX rifm | RNALL rifm | RIALL rifm| RLALL rifm
357   | RBEX rifm | RBALL rifm
359 consts Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
360 primrec
361 "Irifm RT ps is ls ns = True"
362 "Irifm RF ps is ls ns = False"
363 "Irifm (RVar n) ps is ls ns = ps!n"
364 "Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)"
365 "Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)"
366 "Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)"
367 "Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \<and> Irifm q ps is ls ns)"
368 "Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \<or> Irifm q ps is ls ns)"
369 "Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns)"
370 "Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)"
371 "Irifm (RNEX p) ps is ls ns =  (\<exists>x. Irifm p ps is ls (x#ns))"
372 "Irifm (RIEX p) ps is ls ns =  (\<exists>x. Irifm p ps (x#is) ls ns)"
373 "Irifm (RLEX p) ps is ls ns =  (\<exists>x. Irifm p ps is (x#ls) ns)"
374 "Irifm (RBEX p) ps is ls ns =  (\<exists>x. Irifm p (x#ps) is ls ns)"
375 "Irifm (RNALL p) ps is ls ns = (\<forall>x. Irifm p ps is ls (x#ns))"
376 "Irifm (RIALL p) ps is ls ns = (\<forall>x. Irifm p ps (x#is) ls ns)"
377 "Irifm (RLALL p) ps is ls ns = (\<forall>x. Irifm p ps is (x#ls) ns)"
378 "Irifm (RBALL p) ps is ls ns = (\<forall>x. Irifm p (x#ps) is ls ns)"
380 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)"
381   apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
382 oops
385   (* An example for equations containing type variables *)
386 datatype prod = Zero | One | Var nat | Mul prod prod
387   | Pw prod nat | PNM nat nat prod
388 consts Iprod :: " prod \<Rightarrow> ('a::{ordered_idom,recpower}) list \<Rightarrow>'a"
389 primrec
390   "Iprod Zero vs = 0"
391   "Iprod One vs = 1"
392   "Iprod (Var n) vs = vs!n"
393   "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
394   "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
395   "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
396 consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
397 datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
398   | Or sgn sgn | And sgn sgn
400 consts Isgn :: " sgn \<Rightarrow> ('a::{ordered_idom, recpower}) list \<Rightarrow>bool"
401 primrec
402   "Isgn Tr vs = True"
403   "Isgn F vs = False"
404   "Isgn (ZeroEq t) vs = (Iprod t vs = 0)"
405   "Isgn (NZeroEq t) vs = (Iprod t vs \<noteq> 0)"
406   "Isgn (Pos t) vs = (Iprod t vs > 0)"
407   "Isgn (Neg t) vs = (Iprod t vs < 0)"
408   "Isgn (And p q) vs = (Isgn p vs \<and> Isgn q vs)"
409   "Isgn (Or p q) vs = (Isgn p vs \<or> Isgn q vs)"
411 lemmas eqs = Isgn.simps Iprod.simps
413 lemma "(x::'a::{ordered_idom, recpower})^4 * y * z * y^2 * z^23 > 0"
414   apply (reify eqs)
415   oops
417 end