src/HOL/ex/Reflection_Examples.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61343 5b5656a63bd6
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/ex/Reflection_Examples.thy
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 section {* Examples for generic reflection and reification *}
     6 
     7 theory Reflection_Examples
     8 imports Complex_Main "~~/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 @{text \<sigma>}, the structure of which is not recongnisable
    15 on the theory level.  This is the case of @{typ bool}, arithmetical terms such as @{typ int},
    16 @{typ real} etc \dots  In order to implement a simplification on terms of type @{text \<sigma>} we
    17 often need its structure.  Traditionnaly such simplifications are written in ML,
    18 proofs are synthesized.
    19 
    20 An other strategy is to declare an HOL datatype @{text \<tau>} and an HOL function (the
    21 interpretation) that maps elements of @{text \<tau>} to elements of @{text \<sigma>}.
    22 
    23 The functionality of @{text reify} then is, given a term @{text t} of type @{text \<sigma>},
    24 to compute a term @{text s} of type @{text \<tau>}.  For this it needs equations for the
    25 interpretation.
    26 
    27 N.B: All the interpretations supported by @{text reify} must have the type
    28 @{text "'a list \<Rightarrow> \<tau> \<Rightarrow> \<sigma>"}.  The method @{text reify} can also be told which subterm
    29 of the current subgoal should be reified.  The general call for @{text reify} is
    30 @{text "reify eqs (t)"}, where @{text eqs} are the defining equations of the interpretation
    31 and @{text "(t)"} is an optional parameter which specifies the subterm to which reification
    32 should be applied to.  If @{text "(t)"} is abscent, @{text reify} tries to reify the whole
    33 subgoal.
    34 
    35 The method @{text reflection} uses @{text reify} and has a very similar signature:
    36 @{text "reflection corr_thm eqs (t)"}.  Here again @{text eqs} and @{text "(t)"}
    37 are as described above and @{text corr_thm} is a theorem proving
    38 @{prop "I vs (f t) = I vs t"}.  We assume that @{text I} is the interpretation
    39 and @{text f} is some useful and executable simplification of type @{text "\<tau> \<Rightarrow> \<tau>"}.
    40 The method @{text reflection} applies reification and hence the theorem @{prop "t = I xs s"}
    41 and hence using @{text corr_thm} derives @{prop "t = I xs (f s)"}.  It then uses
    42 normalization by equational rewriting to prove @{prop "f s = s'"} which almost finishes
    43 the proof of @{prop "t = t'"} where @{prop "I xs s' = t'"}.
    44 *}
    45 
    46 text {* Example 1 : Propositional formulae and NNF. *}
    47 text {* The type @{text fm} represents simple propositional formulae: *}
    48 
    49 datatype form = TrueF | FalseF | Less nat nat
    50   | And form form | Or form form | Neg form | ExQ form
    51 
    52 primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
    53 where
    54   "interp TrueF vs \<longleftrightarrow> True"
    55 | "interp FalseF vs \<longleftrightarrow> False"
    56 | "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
    57 | "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
    58 | "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
    59 | "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
    60 | "interp (ExQ f) vs \<longleftrightarrow> (\<exists>v. interp f (v # vs))"
    61 
    62 lemmas interp_reify_eqs = interp.simps
    63 declare interp_reify_eqs [reify]
    64 
    65 lemma "\<exists>x. x < y \<and> x < z"
    66   apply reify
    67   oops
    68 
    69 datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
    70 
    71 primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
    72 where
    73   "Ifm (At n) vs \<longleftrightarrow> vs ! n"
    74 | "Ifm (And p q) vs \<longleftrightarrow> Ifm p vs \<and> Ifm q vs"
    75 | "Ifm (Or p q) vs \<longleftrightarrow> Ifm p vs \<or> Ifm q vs"
    76 | "Ifm (Imp p q) vs \<longleftrightarrow> Ifm p vs \<longrightarrow> Ifm q vs"
    77 | "Ifm (Iff p q) vs \<longleftrightarrow> Ifm p vs = Ifm q vs"
    78 | "Ifm (NOT p) vs \<longleftrightarrow> \<not> Ifm p vs"
    79 
    80 lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
    81   apply (reify Ifm.simps)
    82 oops
    83 
    84 text {* Method @{text reify} maps a @{typ bool} to an @{typ fm}.  For this it needs the 
    85 semantics of @{text fm}, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
    86 
    87 text {* You can also just pick up a subterm to reify. *}
    88 lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
    89   apply (reify Ifm.simps ("((\<not> D) \<and> (\<not> F))"))
    90 oops
    91 
    92 text {* Let's perform NNF. This is a version that tends to generate disjunctions *}
    93 primrec fmsize :: "fm \<Rightarrow> nat"
    94 where
    95   "fmsize (At n) = 1"
    96 | "fmsize (NOT p) = 1 + fmsize p"
    97 | "fmsize (And p q) = 1 + fmsize p + fmsize q"
    98 | "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    99 | "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
   100 | "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
   101 
   102 lemma [measure_function]: "is_measure fmsize" ..
   103 
   104 fun nnf :: "fm \<Rightarrow> fm"
   105 where
   106   "nnf (At n) = At n"
   107 | "nnf (And p q) = And (nnf p) (nnf q)"
   108 | "nnf (Or p q) = Or (nnf p) (nnf q)"
   109 | "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
   110 | "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
   111 | "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
   112 | "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
   113 | "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
   114 | "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
   115 | "nnf (NOT (NOT p)) = nnf p"
   116 | "nnf (NOT p) = NOT p"
   117 
   118 text {* The correctness theorem of @{const nnf}: it preserves the semantics of @{typ fm} *}
   119 lemma nnf [reflection]:
   120   "Ifm (nnf p) vs = Ifm p vs"
   121   by (induct p rule: nnf.induct) auto
   122 
   123 text {* Now let's perform NNF using our @{const nnf} function defined above.  First to the
   124   whole subgoal. *}
   125 lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
   126   apply (reflection Ifm.simps)
   127 oops
   128 
   129 text {* Now we specify on which subterm it should be applied *}
   130 lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
   131   apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)")
   132 oops
   133 
   134 
   135 text {* Example 2: Simple arithmetic formulae *}
   136 
   137 text {* The type @{text num} reflects linear expressions over natural number *}
   138 datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
   139 
   140 text {* This is just technical to make recursive definitions easier. *}
   141 primrec num_size :: "num \<Rightarrow> nat" 
   142 where
   143   "num_size (C c) = 1"
   144 | "num_size (Var n) = 1"
   145 | "num_size (Add a b) = 1 + num_size a + num_size b"
   146 | "num_size (Mul c a) = 1 + num_size a"
   147 | "num_size (CN n c a) = 4 + num_size a "
   148 
   149 lemma [measure_function]: "is_measure num_size" ..
   150 
   151 text {* The semantics of num *}
   152 primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
   153 where
   154   Inum_C  : "Inum (C i) vs = i"
   155 | Inum_Var: "Inum (Var n) vs = vs!n"
   156 | Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
   157 | Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
   158 | Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
   159 
   160 text {* Let's reify some nat expressions \dots *}
   161 lemma "4 * (2 * x + (y::nat)) + f a \<noteq> 0"
   162   apply (reify Inum.simps ("4 * (2 * x + (y::nat)) + f a"))
   163 oops
   164 text {* We're in a bad situation! @{text x}, @{text y} and @{text f} have been recongnized
   165 as constants, which is correct but does not correspond to our intuition of the constructor C.
   166 It should encapsulate constants, i.e. numbers, i.e. numerals. *}
   167 
   168 text {* So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots*}
   169 lemma "4 * (2 * x + (y::nat)) \<noteq> 0"
   170   apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2 * x + (y::nat))"))
   171 oops
   172 text {* Hm, let's specialize @{text Inum_C} with numerals.*}
   173 
   174 lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
   175 lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
   176 
   177 text {* Second attempt *}
   178 lemma "1 * (2 * x + (y::nat)) \<noteq> 0"
   179   apply (reify Inum_eqs ("1 * (2 * x + (y::nat))"))
   180 oops
   181 
   182 text{* That was fine, so let's try another one \dots *}
   183 
   184 lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
   185   apply (reify Inum_eqs ("1 * (2 * x + (y::nat) + 0 + 1)"))
   186 oops
   187 
   188 text {* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "numeral"} \dots\ thing.
   189 The same for 1. So let's add those equations, too. *}
   190 
   191 lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
   192   by simp_all
   193 
   194 lemmas Inum_eqs'= Inum_eqs Inum_01
   195 
   196 text{* Third attempt: *}
   197 
   198 lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
   199   apply (reify Inum_eqs' ("1 * (2 * x + (y::nat) + 0 + 1)"))
   200 oops
   201 
   202 text {* Okay, let's try reflection. Some simplifications on @{typ num} follow. You can
   203   skim until the main theorem @{text linum}. *}
   204   
   205 fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
   206 where
   207   "lin_add (CN n1 c1 r1) (CN n2 c2 r2) =
   208     (if n1 = n2 then 
   209       (let c = c1 + c2
   210        in (if c = 0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
   211      else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2))) 
   212      else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
   213 | "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"  
   214 | "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)" 
   215 | "lin_add (C b1) (C b2) = C (b1 + b2)"
   216 | "lin_add a b = Add a b"
   217 
   218 lemma lin_add:
   219   "Inum (lin_add t s) bs = Inum (Add t s) bs"
   220   apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
   221   apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   222   apply (case_tac "n1 = n2", simp_all add: algebra_simps)
   223   done
   224 
   225 fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
   226 where
   227   "lin_mul (C j) i = C (i * j)"
   228 | "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i * c) (lin_mul a i))"
   229 | "lin_mul t i = (Mul i t)"
   230 
   231 lemma lin_mul:
   232   "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
   233   by (induct t i rule: lin_mul.induct) (auto simp add: algebra_simps)
   234 
   235 fun linum:: "num \<Rightarrow> num"
   236 where
   237   "linum (C b) = C b"
   238 | "linum (Var n) = CN n 1 (C 0)"
   239 | "linum (Add t s) = lin_add (linum t) (linum s)"
   240 | "linum (Mul c t) = lin_mul (linum t) c"
   241 | "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
   242 
   243 lemma linum [reflection]:
   244   "Inum (linum t) bs = Inum t bs"
   245   by (induct t rule: linum.induct) (simp_all add: lin_mul lin_add)
   246 
   247 text {* Now we can use linum to simplify nat terms using reflection *}
   248 
   249 lemma "Suc (Suc 1) * (x + Suc 1 * y) = 3 * x + 6 * y"
   250   apply (reflection Inum_eqs' only: "Suc (Suc 1) * (x + Suc 1 * y)")
   251 oops
   252 
   253 text {* Let's lift this to formulae and see what happens *}
   254 
   255 datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   256   Conj aform aform | Disj aform aform | NEG aform | T | F
   257 
   258 primrec linaformsize:: "aform \<Rightarrow> nat"
   259 where
   260   "linaformsize T = 1"
   261 | "linaformsize F = 1"
   262 | "linaformsize (Lt a b) = 1"
   263 | "linaformsize (Ge a b) = 1"
   264 | "linaformsize (Eq a b) = 1"
   265 | "linaformsize (NEq a b) = 1"
   266 | "linaformsize (NEG p) = 2 + linaformsize p"
   267 | "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
   268 | "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
   269 
   270 lemma [measure_function]: "is_measure linaformsize" ..
   271 
   272 primrec is_aform :: "aform => nat list => bool"
   273 where
   274   "is_aform T vs = True"
   275 | "is_aform F vs = False"
   276 | "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
   277 | "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
   278 | "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
   279 | "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
   280 | "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
   281 | "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
   282 | "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
   283 
   284 text{* Let's reify and do reflection *}
   285 lemma "(3::nat) * x + t < 0 \<and> (2 * x + y \<noteq> 17)"
   286   apply (reify Inum_eqs' is_aform.simps) 
   287 oops
   288 
   289 text {* Note that reification handles several interpretations at the same time*}
   290 lemma "(3::nat) * x + t < 0 \<and> x * x + t * x + 3 + 1 = z * t * 4 * z \<or> x + x + 1 < 0"
   291   apply (reflection Inum_eqs' is_aform.simps only: "x + x + 1") 
   292 oops
   293 
   294 text {* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
   295 
   296 fun linaform:: "aform \<Rightarrow> aform"
   297 where
   298   "linaform (Lt s t) = Lt (linum s) (linum t)"
   299 | "linaform (Eq s t) = Eq (linum s) (linum t)"
   300 | "linaform (Ge s t) = Ge (linum s) (linum t)"
   301 | "linaform (NEq s t) = NEq (linum s) (linum t)"
   302 | "linaform (Conj p q) = Conj (linaform p) (linaform q)"
   303 | "linaform (Disj p q) = Disj (linaform p) (linaform q)"
   304 | "linaform (NEG T) = F"
   305 | "linaform (NEG F) = T"
   306 | "linaform (NEG (Lt a b)) = Ge a b"
   307 | "linaform (NEG (Ge a b)) = Lt a b"
   308 | "linaform (NEG (Eq a b)) = NEq a b"
   309 | "linaform (NEG (NEq a b)) = Eq a b"
   310 | "linaform (NEG (NEG p)) = linaform p"
   311 | "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
   312 | "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
   313 | "linaform p = p"
   314 
   315 lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
   316   by (induct p rule: linaform.induct) (auto simp add: linum)
   317 
   318 lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
   319   (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
   320   apply (reflection Inum_eqs' is_aform.simps rules: linaform)  
   321 oops
   322 
   323 declare linaform [reflection]
   324 
   325 lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
   326   (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
   327   apply (reflection Inum_eqs' is_aform.simps)
   328 oops
   329 
   330 text {* We now give an example where interpretaions have zero or more than only
   331   one envornement of different types and show that automatic reification also deals with
   332   bindings *}
   333   
   334 datatype rb = BC bool | BAnd rb rb | BOr rb rb
   335 
   336 primrec Irb :: "rb \<Rightarrow> bool"
   337 where
   338   "Irb (BC p) \<longleftrightarrow> p"
   339 | "Irb (BAnd s t) \<longleftrightarrow> Irb s \<and> Irb t"
   340 | "Irb (BOr s t) \<longleftrightarrow> Irb s \<or> Irb t"
   341 
   342 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)"
   343   apply (reify Irb.simps)
   344 oops
   345 
   346 datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
   347   | INeg rint | ISub rint rint
   348 
   349 primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
   350 where
   351   Irint_Var: "Irint (IVar n) vs = vs ! n"
   352 | Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
   353 | Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
   354 | Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
   355 | Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
   356 | Irint_C: "Irint (IC i) vs = i"
   357 
   358 lemma Irint_C0: "Irint (IC 0) vs = 0"
   359   by simp
   360 
   361 lemma Irint_C1: "Irint (IC 1) vs = 1"
   362   by simp
   363 
   364 lemma Irint_Cnumeral: "Irint (IC (numeral x)) vs = numeral x"
   365   by simp
   366 
   367 lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumeral
   368 
   369 lemma "(3::int) * x + y * y - 9 + (- z) = 0"
   370   apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
   371   oops
   372 
   373 datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
   374 
   375 primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
   376 where
   377   "Irlist (LEmpty) is vs = []"
   378 | "Irlist (LVar n) is vs = vs ! n"
   379 | "Irlist (LCons i t) is vs = Irint i is # Irlist t is vs"
   380 | "Irlist (LAppend s t) is vs = Irlist s is vs @ Irlist t is vs"
   381 
   382 lemma "[(1::int)] = []"
   383   apply (reify Irlist.simps Irint_simps ("[1] :: int list"))
   384   oops
   385 
   386 lemma "([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs = [y * y - z - 9 + (3::int) * x]"
   387   apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
   388   oops
   389 
   390 datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
   391   | NNeg rnat | NSub rnat rnat | Nlgth rlist
   392 
   393 primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
   394 where
   395   Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
   396 | Irnat_Var: "Irnat (NVar n) is ls vs = vs ! n"
   397 | Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
   398 | Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
   399 | Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
   400 | Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
   401 | Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
   402 | Irnat_C: "Irnat (NC i) is ls vs = i"
   403 
   404 lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
   405   by simp
   406 
   407 lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
   408   by simp
   409 
   410 lemma Irnat_Cnumeral: "Irnat (NC (numeral x)) is ls vs = numeral x"
   411   by simp
   412 
   413 lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
   414   Irnat_C0 Irnat_C1 Irnat_Cnumeral
   415 
   416 lemma "Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs) = length xs"
   417   apply (reify Irnat_simps Irlist.simps Irint_simps
   418      ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
   419   oops
   420 
   421 datatype rifm = RT | RF | RVar nat
   422   | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
   423   | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
   424   | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
   425   | RBEX rifm | RBALL rifm
   426 
   427 primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
   428 where
   429   "Irifm RT ps is ls ns \<longleftrightarrow> True"
   430 | "Irifm RF ps is ls ns \<longleftrightarrow> False"
   431 | "Irifm (RVar n) ps is ls ns \<longleftrightarrow> ps ! n"
   432 | "Irifm (RNLT s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns < Irnat t is ls ns"
   433 | "Irifm (RNILT s t) ps is ls ns \<longleftrightarrow> int (Irnat s is ls ns) < Irint t is"
   434 | "Irifm (RNEQ s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns = Irnat t is ls ns"
   435 | "Irifm (RAnd p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<and> Irifm q ps is ls ns"
   436 | "Irifm (ROr p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<or> Irifm q ps is ls ns"
   437 | "Irifm (RImp p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns"
   438 | "Irifm (RIff p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns = Irifm q ps is ls ns"
   439 | "Irifm (RNEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is ls (x # ns))"
   440 | "Irifm (RIEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps (x # is) ls ns)"
   441 | "Irifm (RLEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is (x # ls) ns)"
   442 | "Irifm (RBEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p (x # ps) is ls ns)"
   443 | "Irifm (RNALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is ls (x#ns))"
   444 | "Irifm (RIALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps (x # is) ls ns)"
   445 | "Irifm (RLALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is (x#ls) ns)"
   446 | "Irifm (RBALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p (x # ps) is ls ns)"
   447 
   448 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)"
   449   apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
   450 oops
   451 
   452 text {* An example for equations containing type variables *}
   453 
   454 datatype prod = Zero | One | Var nat | Mul prod prod 
   455   | Pw prod nat | PNM nat nat prod
   456 
   457 primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
   458 where
   459   "Iprod Zero vs = 0"
   460 | "Iprod One vs = 1"
   461 | "Iprod (Var n) vs = vs ! n"
   462 | "Iprod (Mul a b) vs = Iprod a vs * Iprod b vs"
   463 | "Iprod (Pw a n) vs = Iprod a vs ^ n"
   464 | "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
   465 
   466 datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   467   | Or sgn sgn | And sgn sgn
   468 
   469 primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
   470 where 
   471   "Isgn Tr vs \<longleftrightarrow> True"
   472 | "Isgn F vs \<longleftrightarrow> False"
   473 | "Isgn (ZeroEq t) vs \<longleftrightarrow> Iprod t vs = 0"
   474 | "Isgn (NZeroEq t) vs \<longleftrightarrow> Iprod t vs \<noteq> 0"
   475 | "Isgn (Pos t) vs \<longleftrightarrow> Iprod t vs > 0"
   476 | "Isgn (Neg t) vs \<longleftrightarrow> Iprod t vs < 0"
   477 | "Isgn (And p q) vs \<longleftrightarrow> Isgn p vs \<and> Isgn q vs"
   478 | "Isgn (Or p q) vs \<longleftrightarrow> Isgn p vs \<or> Isgn q vs"
   479 
   480 lemmas eqs = Isgn.simps Iprod.simps
   481 
   482 lemma "(x::'a::{linordered_idom}) ^ 4 * y * z * y ^ 2 * z ^ 23 > 0"
   483   apply (reify eqs)
   484   oops
   485 
   486 end
   487