src/HOL/ex/ReflectionEx.thy
 author huffman Sun Mar 25 20:15:39 2012 +0200 (2012-03-25) changeset 47108 2a1953f0d20d parent 41413 64cd30d6b0b8 permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
```     1 (*  Title:      HOL/ex/ReflectionEx.thy
```
```     2     Author:     Amine Chaieb, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Examples for generic reflection and reification *}
```
```     6
```
```     7 theory ReflectionEx
```
```     8 imports "~~/src/HOL/Library/Reflection"
```
```     9 begin
```
```    10
```
```    11 text{* This theory presents two methods: reify and reflection *}
```
```    12
```
```    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.
```
```    18
```
```    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.
```
```    21
```
```    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 *}
```
```    24
```
```    25 text{* Example 1 : Propositional formulae and NNF.*}
```
```    26 text{* The type @{text fm} represents simple propositional formulae: *}
```
```    27
```
```    28 datatype form = TrueF | FalseF | Less nat nat |
```
```    29                 And form form | Or form form | Neg form | ExQ form
```
```    30
```
```    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))"
```
```    39
```
```    40 lemmas interp_reify_eqs = interp.simps
```
```    41 declare interp_reify_eqs[reify]
```
```    42
```
```    43 lemma "EX x. x < y & x < z"
```
```    44   apply (reify )
```
```    45   oops
```
```    46
```
```    47 datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
```
```    48
```
```    49 primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool" where
```
```    50   "Ifm (At n) vs = vs!n"
```
```    51 | "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
```
```    52 | "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
```
```    53 | "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
```
```    54 | "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
```
```    55 | "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
```
```    56
```
```    57 lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
```
```    58 apply (reify Ifm.simps)
```
```    59 oops
```
```    60
```
```    61   text{* Method @{text reify} maps a bool to an fm. For this it needs the
```
```    62   semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
```
```    63
```
```    64
```
```    65   (* You can also just pick up a subterm to reify \<dots> *)
```
```    66 lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
```
```    67 apply (reify Ifm.simps ("((~ D) & (~ F))"))
```
```    68 oops
```
```    69
```
```    70   text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
```
```    71 primrec fmsize :: "fm \<Rightarrow> nat" where
```
```    72   "fmsize (At n) = 1"
```
```    73 | "fmsize (NOT p) = 1 + fmsize p"
```
```    74 | "fmsize (And p q) = 1 + fmsize p + fmsize q"
```
```    75 | "fmsize (Or p q) = 1 + fmsize p + fmsize q"
```
```    76 | "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
```
```    77 | "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
```
```    78
```
```    79 lemma [measure_function]: "is_measure fmsize" ..
```
```    80
```
```    81 fun nnf :: "fm \<Rightarrow> fm"
```
```    82 where
```
```    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"
```
```    94
```
```    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
```
```    98
```
```    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
```
```   103
```
```   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
```
```   108
```
```   109
```
```   110   (* Example 2 : Simple arithmetic formulae *)
```
```   111
```
```   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
```
```   114
```
```   115 text{* This is just technical to make recursive definitions easier. *}
```
```   116 primrec num_size :: "num \<Rightarrow> nat"
```
```   117 where
```
```   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 "
```
```   123
```
```   124   text{* The semantics of num *}
```
```   125 primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
```
```   126 where
```
```   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 "
```
```   132
```
```   133
```
```   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.*}
```
```   139
```
```   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.*}
```
```   145
```
```   146 lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
```
```   147 lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
```
```   148
```
```   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 *}
```
```   154
```
```   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 "numeral"} \dots\ thing. The same for 1. So let's add those equations too *}
```
```   159
```
```   160 lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
```
```   161   by simp+
```
```   162
```
```   163 lemmas Inum_eqs'= Inum_eqs Inum_01
```
```   164
```
```   165 text{* Third attempt: *}
```
```   166
```
```   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 fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
```
```   172 where
```
```   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)"
```
```   182 | "lin_add a b = Add a b"
```
```   183 lemma lin_add: "Inum (lin_add t s) bs = Inum (Add t s) bs"
```
```   184 apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
```
```   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)
```
```   187
```
```   188 fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
```
```   189 where
```
```   190   "lin_mul (C j) i = C (i*j)"
```
```   191 | "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
```
```   192 | "lin_mul t i = (Mul i t)"
```
```   193
```
```   194 lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
```
```   195 by (induct t i rule: lin_mul.induct, auto simp add: algebra_simps)
```
```   196
```
```   197 lemma [measure_function]: "is_measure num_size" ..
```
```   198
```
```   199 fun linum:: "num \<Rightarrow> num"
```
```   200 where
```
```   201   "linum (C b) = C b"
```
```   202 | "linum (Var n) = CN n 1 (C 0)"
```
```   203 | "linum (Add t s) = lin_add (linum t) (linum s)"
```
```   204 | "linum (Mul c t) = lin_mul (linum t) c"
```
```   205 | "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
```
```   206
```
```   207 lemma linum[reflection] : "Inum (linum t) bs = Inum t bs"
```
```   208 by (induct t rule: linum.induct, simp_all add: lin_mul lin_add)
```
```   209
```
```   210   text{* Now we can use linum to simplify nat terms using reflection *}
```
```   211 lemma "(Suc (Suc 1)) * (x + (Suc 1)*y) = 3*x + 6*y"
```
```   212  apply (reflection Inum_eqs' only: "(Suc (Suc 1)) * (x + (Suc 1)*y)")
```
```   213 oops
```
```   214
```
```   215   text{* Let's lift this to formulae and see what happens *}
```
```   216
```
```   217 datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num |
```
```   218   Conj aform aform | Disj aform aform | NEG aform | T | F
```
```   219
```
```   220 primrec linaformsize:: "aform \<Rightarrow> nat"
```
```   221 where
```
```   222   "linaformsize T = 1"
```
```   223 | "linaformsize F = 1"
```
```   224 | "linaformsize (Lt a b) = 1"
```
```   225 | "linaformsize (Ge a b) = 1"
```
```   226 | "linaformsize (Eq a b) = 1"
```
```   227 | "linaformsize (NEq a b) = 1"
```
```   228 | "linaformsize (NEG p) = 2 + linaformsize p"
```
```   229 | "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
```
```   230 | "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
```
```   231
```
```   232 lemma [measure_function]: "is_measure linaformsize" ..
```
```   233
```
```   234 primrec is_aform :: "aform => nat list => bool"
```
```   235 where
```
```   236   "is_aform T vs = True"
```
```   237 | "is_aform F vs = False"
```
```   238 | "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
```
```   239 | "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
```
```   240 | "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
```
```   241 | "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
```
```   242 | "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
```
```   243 | "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
```
```   244 | "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
```
```   245
```
```   246   text{* Let's reify and do reflection *}
```
```   247 lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
```
```   248  apply (reify Inum_eqs' is_aform.simps)
```
```   249 oops
```
```   250
```
```   251 text{* Note that reification handles several interpretations at the same time*}
```
```   252 lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
```
```   253  apply (reflection Inum_eqs' is_aform.simps only:"x + x + 1")
```
```   254 oops
```
```   255
```
```   256   text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
```
```   257
```
```   258 fun linaform:: "aform \<Rightarrow> aform"
```
```   259 where
```
```   260   "linaform (Lt s t) = Lt (linum s) (linum t)"
```
```   261 | "linaform (Eq s t) = Eq (linum s) (linum t)"
```
```   262 | "linaform (Ge s t) = Ge (linum s) (linum t)"
```
```   263 | "linaform (NEq s t) = NEq (linum s) (linum t)"
```
```   264 | "linaform (Conj p q) = Conj (linaform p) (linaform q)"
```
```   265 | "linaform (Disj p q) = Disj (linaform p) (linaform q)"
```
```   266 | "linaform (NEG T) = F"
```
```   267 | "linaform (NEG F) = T"
```
```   268 | "linaform (NEG (Lt a b)) = Ge a b"
```
```   269 | "linaform (NEG (Ge a b)) = Lt a b"
```
```   270 | "linaform (NEG (Eq a b)) = NEq a b"
```
```   271 | "linaform (NEG (NEq a b)) = Eq a b"
```
```   272 | "linaform (NEG (NEG p)) = linaform p"
```
```   273 | "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
```
```   274 | "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
```
```   275 | "linaform p = p"
```
```   276
```
```   277 lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
```
```   278   by (induct p rule: linaform.induct) (auto simp add: linum)
```
```   279
```
```   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 rules: linaform)
```
```   282 oops
```
```   283
```
```   284 declare linaform[reflection]
```
```   285 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)"
```
```   286    apply (reflection Inum_eqs' is_aform.simps)
```
```   287 oops
```
```   288
```
```   289 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 *}
```
```   290 datatype rb = BC bool| BAnd rb rb | BOr rb rb
```
```   291 primrec Irb :: "rb \<Rightarrow> bool"
```
```   292 where
```
```   293   "Irb (BC p) = p"
```
```   294 | "Irb (BAnd s t) = (Irb s \<and> Irb t)"
```
```   295 | "Irb (BOr s t) = (Irb s \<or> Irb t)"
```
```   296
```
```   297 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)"
```
```   298 apply (reify Irb.simps)
```
```   299 oops
```
```   300
```
```   301
```
```   302 datatype rint = IC int| IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint
```
```   303 primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
```
```   304 where
```
```   305   Irint_Var: "Irint (IVar n) vs = vs!n"
```
```   306 | Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
```
```   307 | Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
```
```   308 | Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
```
```   309 | Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
```
```   310 | Irint_C: "Irint (IC i) vs = i"
```
```   311 lemma Irint_C0: "Irint (IC 0) vs = 0"
```
```   312   by simp
```
```   313 lemma Irint_C1: "Irint (IC 1) vs = 1"
```
```   314   by simp
```
```   315 lemma Irint_Cnumeral: "Irint (IC (numeral x)) vs = numeral x"
```
```   316   by simp
```
```   317 lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumeral
```
```   318 lemma "(3::int) * x + y*y - 9 + (- z) = 0"
```
```   319   apply (reify Irint_simps ("(3::int) * x + y*y - 9 + (- z)"))
```
```   320   oops
```
```   321 datatype rlist = LVar nat| LEmpty| LCons rint rlist | LAppend rlist rlist
```
```   322 primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> (int list)"
```
```   323 where
```
```   324   "Irlist (LEmpty) is vs = []"
```
```   325 | "Irlist (LVar n) is vs = vs!n"
```
```   326 | "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))"
```
```   327 | "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)"
```
```   328 lemma "[(1::int)] = []"
```
```   329   apply (reify Irlist.simps Irint_simps (":: int list"))
```
```   330   oops
```
```   331
```
```   332 lemma "([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs = [y*y - z - 9 + (3::int) * x]"
```
```   333   apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs"))
```
```   334   oops
```
```   335
```
```   336 datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist
```
```   337 primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> nat"
```
```   338 where
```
```   339   Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
```
```   340 | Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
```
```   341 | Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
```
```   342 | Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
```
```   343 | Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
```
```   344 | Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
```
```   345 | Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
```
```   346 | Irnat_C: "Irnat (NC i) is ls vs = i"
```
```   347 lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
```
```   348 by simp
```
```   349 lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
```
```   350 by simp
```
```   351 lemma Irnat_Cnumeral: "Irnat (NC (numeral x)) is ls vs = numeral x"
```
```   352 by simp
```
```   353 lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
```
```   354   Irnat_C0 Irnat_C1 Irnat_Cnumeral
```
```   355 lemma "(Suc n) * length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs) = length xs"
```
```   356   apply (reify Irnat_simps Irlist.simps Irint_simps ("(Suc n) *length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs)"))
```
```   357   oops
```
```   358 datatype rifm = RT | RF | RVar nat
```
```   359   | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
```
```   360   |RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
```
```   361   | RNEX rifm | RIEX rifm| RLEX rifm | RNALL rifm | RIALL rifm| RLALL rifm
```
```   362   | RBEX rifm | RBALL rifm
```
```   363
```
```   364 primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
```
```   365 where
```
```   366   "Irifm RT ps is ls ns = True"
```
```   367 | "Irifm RF ps is ls ns = False"
```
```   368 | "Irifm (RVar n) ps is ls ns = ps!n"
```
```   369 | "Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)"
```
```   370 | "Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)"
```
```   371 | "Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)"
```
```   372 | "Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \<and> Irifm q ps is ls ns)"
```
```   373 | "Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \<or> Irifm q ps is ls ns)"
```
```   374 | "Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns)"
```
```   375 | "Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)"
```
```   376 | "Irifm (RNEX p) ps is ls ns =  (\<exists>x. Irifm p ps is ls (x#ns))"
```
```   377 | "Irifm (RIEX p) ps is ls ns =  (\<exists>x. Irifm p ps (x#is) ls ns)"
```
```   378 | "Irifm (RLEX p) ps is ls ns =  (\<exists>x. Irifm p ps is (x#ls) ns)"
```
```   379 | "Irifm (RBEX p) ps is ls ns =  (\<exists>x. Irifm p (x#ps) is ls ns)"
```
```   380 | "Irifm (RNALL p) ps is ls ns = (\<forall>x. Irifm p ps is ls (x#ns))"
```
```   381 | "Irifm (RIALL p) ps is ls ns = (\<forall>x. Irifm p ps (x#is) ls ns)"
```
```   382 | "Irifm (RLALL p) ps is ls ns = (\<forall>x. Irifm p ps is (x#ls) ns)"
```
```   383 | "Irifm (RBALL p) ps is ls ns = (\<forall>x. Irifm p (x#ps) is ls ns)"
```
```   384
```
```   385 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)"
```
```   386   apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
```
```   387 oops
```
```   388
```
```   389
```
```   390 (* An example for equations containing type variables *)
```
```   391 datatype prod = Zero | One | Var nat | Mul prod prod
```
```   392   | Pw prod nat | PNM nat nat prod
```
```   393 primrec Iprod :: " prod \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>'a"
```
```   394 where
```
```   395   "Iprod Zero vs = 0"
```
```   396 | "Iprod One vs = 1"
```
```   397 | "Iprod (Var n) vs = vs!n"
```
```   398 | "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
```
```   399 | "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
```
```   400 | "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
```
```   401
```
```   402 datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
```
```   403   | Or sgn sgn | And sgn sgn
```
```   404
```
```   405 primrec Isgn :: " sgn \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>bool"
```
```   406 where
```
```   407   "Isgn Tr vs = True"
```
```   408 | "Isgn F vs = False"
```
```   409 | "Isgn (ZeroEq t) vs = (Iprod t vs = 0)"
```
```   410 | "Isgn (NZeroEq t) vs = (Iprod t vs \<noteq> 0)"
```
```   411 | "Isgn (Pos t) vs = (Iprod t vs > 0)"
```
```   412 | "Isgn (Neg t) vs = (Iprod t vs < 0)"
```
```   413 | "Isgn (And p q) vs = (Isgn p vs \<and> Isgn q vs)"
```
```   414 | "Isgn (Or p q) vs = (Isgn p vs \<or> Isgn q vs)"
```
```   415
```
```   416 lemmas eqs = Isgn.simps Iprod.simps
```
```   417
```
```   418 lemma "(x::'a::{linordered_idom})^4 * y * z * y^2 * z^23 > 0"
```
```   419   apply (reify eqs)
```
```   420   oops
```
```   421
```
```   422 end
```