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