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 ("[1]:: 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