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