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