src/HOL/ex/ReflectionEx.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 47108 2a1953f0d20d
permissions -rw-r--r--
introduce order topology
     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 ("[1]:: 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