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