src/HOL/ex/ReflectionEx.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39246 9e58f0499f57
child 47108 2a1953f0d20d
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
haftmann@29650
     1
(*  Title:      HOL/ex/ReflectionEx.thy
wenzelm@20319
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@20319
     3
*)
wenzelm@20319
     4
wenzelm@20319
     5
header {* Examples for generic reflection and reification *}
haftmann@29650
     6
wenzelm@20319
     7
theory ReflectionEx
wenzelm@41413
     8
imports "~~/src/HOL/Library/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{* 
wenzelm@28866
    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
haftmann@39246
    49
primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool" where
chaieb@23624
    50
  "Ifm (At n) vs = vs!n"
haftmann@39246
    51
| "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
haftmann@39246
    52
| "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
haftmann@39246
    53
| "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
haftmann@39246
    54
| "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
haftmann@39246
    55
| "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
wenzelm@20319
    56
chaieb@23547
    57
lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
chaieb@23547
    58
apply (reify Ifm.simps)
chaieb@23547
    59
oops
chaieb@23547
    60
chaieb@23547
    61
  text{* Method @{text reify} maps a bool to an fm. For this it needs the 
chaieb@23547
    62
  semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
chaieb@23547
    63
chaieb@23547
    64
chaieb@23547
    65
  (* You can also just pick up a subterm to reify \<dots> *)
chaieb@23547
    66
lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
chaieb@23547
    67
apply (reify Ifm.simps ("((~ D) & (~ F))"))
chaieb@23547
    68
oops
chaieb@23547
    69
chaieb@23547
    70
  text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
krauss@35419
    71
primrec fmsize :: "fm \<Rightarrow> nat" where
wenzelm@20319
    72
  "fmsize (At n) = 1"
krauss@35419
    73
| "fmsize (NOT p) = 1 + fmsize p"
krauss@35419
    74
| "fmsize (And p q) = 1 + fmsize p + fmsize q"
krauss@35419
    75
| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
krauss@35419
    76
| "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
krauss@35419
    77
| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
krauss@35419
    78
krauss@35419
    79
lemma [measure_function]: "is_measure fmsize" ..
wenzelm@20319
    80
krauss@35419
    81
fun nnf :: "fm \<Rightarrow> fm"
krauss@35419
    82
where
wenzelm@20319
    83
  "nnf (At n) = At n"
krauss@35419
    84
| "nnf (And p q) = And (nnf p) (nnf q)"
krauss@35419
    85
| "nnf (Or p q) = Or (nnf p) (nnf q)"
krauss@35419
    86
| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
krauss@35419
    87
| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
krauss@35419
    88
| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
krauss@35419
    89
| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
krauss@35419
    90
| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
krauss@35419
    91
| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
krauss@35419
    92
| "nnf (NOT (NOT p)) = nnf p"
krauss@35419
    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. *}
krauss@35419
   116
primrec num_size :: "num \<Rightarrow> nat" 
krauss@35419
   117
where
wenzelm@20319
   118
  "num_size (C c) = 1"
krauss@35419
   119
| "num_size (Var n) = 1"
krauss@35419
   120
| "num_size (Add a b) = 1 + num_size a + num_size b"
krauss@35419
   121
| "num_size (Mul c a) = 1 + num_size a"
krauss@35419
   122
| "num_size (CN n c a) = 4 + num_size a "
wenzelm@20319
   123
chaieb@20337
   124
  text{* The semantics of num *}
krauss@35419
   125
primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
krauss@35419
   126
where
chaieb@23624
   127
  Inum_C  : "Inum (C i) vs = i"
krauss@35419
   128
| Inum_Var: "Inum (Var n) vs = vs!n"
krauss@35419
   129
| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
krauss@35419
   130
| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
krauss@35419
   131
| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
wenzelm@20319
   132
chaieb@23650
   133
wenzelm@28866
   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
wenzelm@28866
   140
  text{* So let's leave the @{text "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
wenzelm@28866
   153
  text{* That was fine, so let's try another 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
wenzelm@28866
   158
  text{* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "number_of"} \dots\ 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} *}
krauss@35419
   171
fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
krauss@35419
   172
where
krauss@35419
   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
krauss@35419
   176
  in (if c=0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
krauss@35419
   177
  else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2))) 
krauss@35419
   178
  else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
krauss@35419
   179
| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"  
krauss@35419
   180
| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)" 
krauss@35419
   181
| "lin_add (C b1) (C b2) = C (b1+b2)"
krauss@35419
   182
| "lin_add a b = Add a b"
krauss@35419
   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@29667
   186
by (case_tac "n1 = n2", simp_all add: algebra_simps)
wenzelm@20319
   187
krauss@35419
   188
fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
krauss@35419
   189
where
krauss@35419
   190
  "lin_mul (C j) i = C (i*j)"
krauss@35419
   191
| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
krauss@35419
   192
| "lin_mul t i = (Mul i t)"
wenzelm@20319
   193
chaieb@23624
   194
lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
krauss@35419
   195
by (induct t i rule: lin_mul.induct, auto simp add: algebra_simps)
wenzelm@20319
   196
krauss@35419
   197
lemma [measure_function]: "is_measure num_size" ..
krauss@35419
   198
krauss@35419
   199
fun linum:: "num \<Rightarrow> num"
krauss@35419
   200
where
wenzelm@20319
   201
  "linum (C b) = C b"
krauss@35419
   202
| "linum (Var n) = CN n 1 (C 0)"
krauss@35419
   203
| "linum (Add t s) = lin_add (linum t) (linum s)"
krauss@35419
   204
| "linum (Mul c t) = lin_mul (linum t) c"
krauss@35419
   205
| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
wenzelm@20319
   206
chaieb@23650
   207
lemma linum[reflection] : "Inum (linum t) bs = Inum t bs"
wenzelm@20319
   208
by (induct t rule: linum.induct, simp_all add: lin_mul lin_add)
wenzelm@20319
   209
chaieb@20337
   210
  text{* Now we can use linum to simplify nat terms using reflection *}
chaieb@20337
   211
lemma "(Suc (Suc 1)) * (x + (Suc 1)*y) = 3*x + 6*y"
chaieb@23650
   212
 apply (reflection Inum_eqs' only: "(Suc (Suc 1)) * (x + (Suc 1)*y)") 
wenzelm@20319
   213
oops
wenzelm@20319
   214
chaieb@20337
   215
  text{* Let's lift this to formulae and see what happens *}
wenzelm@20319
   216
wenzelm@20319
   217
datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
wenzelm@20319
   218
  Conj aform aform | Disj aform aform | NEG aform | T | F
krauss@35419
   219
krauss@35419
   220
primrec linaformsize:: "aform \<Rightarrow> nat"
krauss@35419
   221
where
wenzelm@20319
   222
  "linaformsize T = 1"
krauss@35419
   223
| "linaformsize F = 1"
krauss@35419
   224
| "linaformsize (Lt a b) = 1"
krauss@35419
   225
| "linaformsize (Ge a b) = 1"
krauss@35419
   226
| "linaformsize (Eq a b) = 1"
krauss@35419
   227
| "linaformsize (NEq a b) = 1"
krauss@35419
   228
| "linaformsize (NEG p) = 2 + linaformsize p"
krauss@35419
   229
| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
krauss@35419
   230
| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
wenzelm@20319
   231
krauss@35419
   232
lemma [measure_function]: "is_measure linaformsize" ..
wenzelm@20319
   233
krauss@35419
   234
primrec is_aform :: "aform => nat list => bool"
krauss@35419
   235
where
wenzelm@28866
   236
  "is_aform T vs = True"
krauss@35419
   237
| "is_aform F vs = False"
krauss@35419
   238
| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
krauss@35419
   239
| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
krauss@35419
   240
| "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
krauss@35419
   241
| "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
krauss@35419
   242
| "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
krauss@35419
   243
| "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
krauss@35419
   244
| "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
wenzelm@20319
   245
chaieb@20564
   246
  text{* Let's reify and do reflection *}
wenzelm@20319
   247
lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
wenzelm@28866
   248
 apply (reify Inum_eqs' is_aform.simps) 
wenzelm@20319
   249
oops
wenzelm@20319
   250
chaieb@20337
   251
text{* Note that reification handles several interpretations at the same time*}
wenzelm@20319
   252
lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
wenzelm@28866
   253
 apply (reflection Inum_eqs' is_aform.simps only:"x + x + 1") 
wenzelm@20319
   254
oops
wenzelm@20319
   255
chaieb@20337
   256
  text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
krauss@35419
   257
krauss@35419
   258
fun linaform:: "aform \<Rightarrow> aform"
krauss@35419
   259
where
wenzelm@20319
   260
  "linaform (Lt s t) = Lt (linum s) (linum t)"
krauss@35419
   261
| "linaform (Eq s t) = Eq (linum s) (linum t)"
krauss@35419
   262
| "linaform (Ge s t) = Ge (linum s) (linum t)"
krauss@35419
   263
| "linaform (NEq s t) = NEq (linum s) (linum t)"
krauss@35419
   264
| "linaform (Conj p q) = Conj (linaform p) (linaform q)"
krauss@35419
   265
| "linaform (Disj p q) = Disj (linaform p) (linaform q)"
krauss@35419
   266
| "linaform (NEG T) = F"
krauss@35419
   267
| "linaform (NEG F) = T"
krauss@35419
   268
| "linaform (NEG (Lt a b)) = Ge a b"
krauss@35419
   269
| "linaform (NEG (Ge a b)) = Lt a b"
krauss@35419
   270
| "linaform (NEG (Eq a b)) = NEq a b"
krauss@35419
   271
| "linaform (NEG (NEq a b)) = Eq a b"
krauss@35419
   272
| "linaform (NEG (NEG p)) = linaform p"
krauss@35419
   273
| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
krauss@35419
   274
| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
krauss@35419
   275
| "linaform p = p"
wenzelm@20319
   276
wenzelm@28866
   277
lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
wenzelm@28866
   278
  by (induct p rule: linaform.induct) (auto simp add: linum)
wenzelm@20319
   279
wenzelm@20319
   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)"
wenzelm@28866
   281
   apply (reflection Inum_eqs' is_aform.simps rules: linaform)  
chaieb@23650
   282
oops
chaieb@23650
   283
chaieb@23650
   284
declare linaform[reflection]
chaieb@23650
   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)"
wenzelm@28866
   286
   apply (reflection Inum_eqs' is_aform.simps)
chaieb@20564
   287
oops
chaieb@20564
   288
chaieb@20564
   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 *}
chaieb@20564
   290
datatype rb = BC bool| BAnd rb rb | BOr rb rb
krauss@35419
   291
primrec Irb :: "rb \<Rightarrow> bool"
krauss@35419
   292
where
chaieb@23650
   293
  "Irb (BC p) = p"
krauss@35419
   294
| "Irb (BAnd s t) = (Irb s \<and> Irb t)"
krauss@35419
   295
| "Irb (BOr s t) = (Irb s \<or> Irb t)"
chaieb@20564
   296
chaieb@20564
   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)"
chaieb@20564
   298
apply (reify Irb.simps)
wenzelm@20319
   299
oops
wenzelm@20319
   300
chaieb@23650
   301
chaieb@20564
   302
datatype rint = IC int| IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint
krauss@35419
   303
primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
krauss@35419
   304
where
krauss@35419
   305
  Irint_Var: "Irint (IVar n) vs = vs!n"
krauss@35419
   306
| Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
krauss@35419
   307
| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
krauss@35419
   308
| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
krauss@35419
   309
| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
krauss@35419
   310
| Irint_C: "Irint (IC i) vs = i"
chaieb@23624
   311
lemma Irint_C0: "Irint (IC 0) vs = 0"
chaieb@20564
   312
  by simp
chaieb@23624
   313
lemma Irint_C1: "Irint (IC 1) vs = 1"
chaieb@20564
   314
  by simp
chaieb@23624
   315
lemma Irint_Cnumberof: "Irint (IC (number_of x)) vs = number_of x"
chaieb@20564
   316
  by simp
chaieb@20564
   317
lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumberof 
chaieb@20564
   318
lemma "(3::int) * x + y*y - 9 + (- z) = 0"
chaieb@20564
   319
  apply (reify Irint_simps ("(3::int) * x + y*y - 9 + (- z)"))
chaieb@20564
   320
  oops
chaieb@20564
   321
datatype rlist = LVar nat| LEmpty| LCons rint rlist | LAppend rlist rlist
krauss@35419
   322
primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> (int list)"
krauss@35419
   323
where
chaieb@23624
   324
  "Irlist (LEmpty) is vs = []"
krauss@35419
   325
| "Irlist (LVar n) is vs = vs!n"
krauss@35419
   326
| "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))"
krauss@35419
   327
| "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)"
chaieb@20564
   328
lemma "[(1::int)] = []"
chaieb@20564
   329
  apply (reify Irlist.simps Irint_simps ("[1]:: int list"))
chaieb@20564
   330
  oops
chaieb@20374
   331
chaieb@20564
   332
lemma "([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs = [y*y - z - 9 + (3::int) * x]"
chaieb@20564
   333
  apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs"))
chaieb@20564
   334
  oops
chaieb@20374
   335
chaieb@20564
   336
datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist
krauss@35419
   337
primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> nat"
krauss@35419
   338
where
krauss@35419
   339
  Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
krauss@35419
   340
| Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
krauss@35419
   341
| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
krauss@35419
   342
| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
krauss@35419
   343
| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
krauss@35419
   344
| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
krauss@35419
   345
| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
krauss@35419
   346
| Irnat_C: "Irnat (NC i) is ls vs = i"
chaieb@23624
   347
lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
chaieb@20564
   348
by simp
chaieb@23624
   349
lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
chaieb@20564
   350
by simp
chaieb@23624
   351
lemma Irnat_Cnumberof: "Irnat (NC (number_of x)) is ls vs = number_of x"
chaieb@20564
   352
by simp
chaieb@20564
   353
lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
chaieb@20564
   354
  Irnat_C0 Irnat_C1 Irnat_Cnumberof
chaieb@20564
   355
lemma "(Suc n) * length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs) = length xs"
chaieb@20564
   356
  apply (reify Irnat_simps Irlist.simps Irint_simps ("(Suc n) *length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs)"))
chaieb@20564
   357
  oops
chaieb@20564
   358
datatype rifm = RT | RF | RVar nat
chaieb@20564
   359
  | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
chaieb@20564
   360
  |RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
chaieb@20564
   361
  | RNEX rifm | RIEX rifm| RLEX rifm | RNALL rifm | RIALL rifm| RLALL rifm
chaieb@20564
   362
  | RBEX rifm | RBALL rifm
chaieb@23624
   363
krauss@35419
   364
primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
krauss@35419
   365
where
krauss@35419
   366
  "Irifm RT ps is ls ns = True"
krauss@35419
   367
| "Irifm RF ps is ls ns = False"
krauss@35419
   368
| "Irifm (RVar n) ps is ls ns = ps!n"
krauss@35419
   369
| "Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)"
krauss@35419
   370
| "Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)"
krauss@35419
   371
| "Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)"
krauss@35419
   372
| "Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \<and> Irifm q ps is ls ns)"
krauss@35419
   373
| "Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \<or> Irifm q ps is ls ns)"
krauss@35419
   374
| "Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns)"
krauss@35419
   375
| "Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)"
krauss@35419
   376
| "Irifm (RNEX p) ps is ls ns =  (\<exists>x. Irifm p ps is ls (x#ns))"
krauss@35419
   377
| "Irifm (RIEX p) ps is ls ns =  (\<exists>x. Irifm p ps (x#is) ls ns)"
krauss@35419
   378
| "Irifm (RLEX p) ps is ls ns =  (\<exists>x. Irifm p ps is (x#ls) ns)"
krauss@35419
   379
| "Irifm (RBEX p) ps is ls ns =  (\<exists>x. Irifm p (x#ps) is ls ns)"
krauss@35419
   380
| "Irifm (RNALL p) ps is ls ns = (\<forall>x. Irifm p ps is ls (x#ns))"
krauss@35419
   381
| "Irifm (RIALL p) ps is ls ns = (\<forall>x. Irifm p ps (x#is) ls ns)"
krauss@35419
   382
| "Irifm (RLALL p) ps is ls ns = (\<forall>x. Irifm p ps is (x#ls) ns)"
krauss@35419
   383
| "Irifm (RBALL p) ps is ls ns = (\<forall>x. Irifm p (x#ps) is ls ns)"
chaieb@20374
   384
chaieb@20564
   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)"
chaieb@20564
   386
  apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
chaieb@20374
   387
oops
chaieb@20374
   388
chaieb@22199
   389
wenzelm@32960
   390
(* An example for equations containing type variables *)
chaieb@22199
   391
datatype prod = Zero | One | Var nat | Mul prod prod 
chaieb@22199
   392
  | Pw prod nat | PNM nat nat prod
krauss@35419
   393
primrec Iprod :: " prod \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>'a" 
krauss@35419
   394
where
chaieb@23624
   395
  "Iprod Zero vs = 0"
krauss@35419
   396
| "Iprod One vs = 1"
krauss@35419
   397
| "Iprod (Var n) vs = vs!n"
krauss@35419
   398
| "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
krauss@35419
   399
| "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
krauss@35419
   400
| "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
haftmann@39246
   401
chaieb@22199
   402
datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
chaieb@22199
   403
  | Or sgn sgn | And sgn sgn
chaieb@22199
   404
krauss@35419
   405
primrec Isgn :: " sgn \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>bool"
krauss@35419
   406
where 
chaieb@23624
   407
  "Isgn Tr vs = True"
krauss@35419
   408
| "Isgn F vs = False"
krauss@35419
   409
| "Isgn (ZeroEq t) vs = (Iprod t vs = 0)"
krauss@35419
   410
| "Isgn (NZeroEq t) vs = (Iprod t vs \<noteq> 0)"
krauss@35419
   411
| "Isgn (Pos t) vs = (Iprod t vs > 0)"
krauss@35419
   412
| "Isgn (Neg t) vs = (Iprod t vs < 0)"
krauss@35419
   413
| "Isgn (And p q) vs = (Isgn p vs \<and> Isgn q vs)"
krauss@35419
   414
| "Isgn (Or p q) vs = (Isgn p vs \<or> Isgn q vs)"
chaieb@22199
   415
chaieb@22199
   416
lemmas eqs = Isgn.simps Iprod.simps
chaieb@22199
   417
haftmann@35028
   418
lemma "(x::'a::{linordered_idom})^4 * y * z * y^2 * z^23 > 0"
chaieb@22199
   419
  apply (reify eqs)
chaieb@22199
   420
  oops
chaieb@22199
   421
wenzelm@20319
   422
end