|
1 (* Title: HOL/Reflection/Ferrack.thy |
|
2 Author: Amine Chaieb |
|
3 *) |
|
4 |
|
5 theory Ferrack |
|
6 imports Complex_Main Dense_Linear_Order Efficient_Nat |
|
7 uses ("ferrack_tac.ML") |
|
8 begin |
|
9 |
|
10 section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *} |
|
11 |
|
12 (*********************************************************************************) |
|
13 (* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *) |
|
14 (*********************************************************************************) |
|
15 |
|
16 consts alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" |
|
17 primrec |
|
18 "alluopairs [] = []" |
|
19 "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)" |
|
20 |
|
21 lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}" |
|
22 by (induct xs, auto) |
|
23 |
|
24 lemma alluopairs_set: |
|
25 "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) " |
|
26 by (induct xs, auto) |
|
27 |
|
28 lemma alluopairs_ex: |
|
29 assumes Pc: "\<forall> x y. P x y = P y x" |
|
30 shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)" |
|
31 proof |
|
32 assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" |
|
33 then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y" by blast |
|
34 from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" |
|
35 by auto |
|
36 next |
|
37 assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y" |
|
38 then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+ |
|
39 from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast |
|
40 with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast |
|
41 qed |
|
42 |
|
43 lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)" |
|
44 using Nat.gr0_conv_Suc |
|
45 by clarsimp |
|
46 |
|
47 lemma filter_length: "length (List.filter P xs) < Suc (length xs)" |
|
48 apply (induct xs, auto) done |
|
49 |
|
50 consts remdps:: "'a list \<Rightarrow> 'a list" |
|
51 |
|
52 recdef remdps "measure size" |
|
53 "remdps [] = []" |
|
54 "remdps (x#xs) = (x#(remdps (List.filter (\<lambda> y. y \<noteq> x) xs)))" |
|
55 (hints simp add: filter_length[rule_format]) |
|
56 |
|
57 lemma remdps_set[simp]: "set (remdps xs) = set xs" |
|
58 by (induct xs rule: remdps.induct, auto) |
|
59 |
|
60 |
|
61 |
|
62 (*********************************************************************************) |
|
63 (**** SHADOW SYNTAX AND SEMANTICS ****) |
|
64 (*********************************************************************************) |
|
65 |
|
66 datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num |
|
67 | Mul int num |
|
68 |
|
69 (* A size for num to make inductive proofs simpler*) |
|
70 consts num_size :: "num \<Rightarrow> nat" |
|
71 primrec |
|
72 "num_size (C c) = 1" |
|
73 "num_size (Bound n) = 1" |
|
74 "num_size (Neg a) = 1 + num_size a" |
|
75 "num_size (Add a b) = 1 + num_size a + num_size b" |
|
76 "num_size (Sub a b) = 3 + num_size a + num_size b" |
|
77 "num_size (Mul c a) = 1 + num_size a" |
|
78 "num_size (CN n c a) = 3 + num_size a " |
|
79 |
|
80 (* Semantics of numeral terms (num) *) |
|
81 consts Inum :: "real list \<Rightarrow> num \<Rightarrow> real" |
|
82 primrec |
|
83 "Inum bs (C c) = (real c)" |
|
84 "Inum bs (Bound n) = bs!n" |
|
85 "Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)" |
|
86 "Inum bs (Neg a) = -(Inum bs a)" |
|
87 "Inum bs (Add a b) = Inum bs a + Inum bs b" |
|
88 "Inum bs (Sub a b) = Inum bs a - Inum bs b" |
|
89 "Inum bs (Mul c a) = (real c) * Inum bs a" |
|
90 (* FORMULAE *) |
|
91 datatype fm = |
|
92 T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| |
|
93 NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm |
|
94 |
|
95 |
|
96 (* A size for fm *) |
|
97 consts fmsize :: "fm \<Rightarrow> nat" |
|
98 recdef fmsize "measure size" |
|
99 "fmsize (NOT p) = 1 + fmsize p" |
|
100 "fmsize (And p q) = 1 + fmsize p + fmsize q" |
|
101 "fmsize (Or p q) = 1 + fmsize p + fmsize q" |
|
102 "fmsize (Imp p q) = 3 + fmsize p + fmsize q" |
|
103 "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" |
|
104 "fmsize (E p) = 1 + fmsize p" |
|
105 "fmsize (A p) = 4+ fmsize p" |
|
106 "fmsize p = 1" |
|
107 (* several lemmas about fmsize *) |
|
108 lemma fmsize_pos: "fmsize p > 0" |
|
109 by (induct p rule: fmsize.induct) simp_all |
|
110 |
|
111 (* Semantics of formulae (fm) *) |
|
112 consts Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool" |
|
113 primrec |
|
114 "Ifm bs T = True" |
|
115 "Ifm bs F = False" |
|
116 "Ifm bs (Lt a) = (Inum bs a < 0)" |
|
117 "Ifm bs (Gt a) = (Inum bs a > 0)" |
|
118 "Ifm bs (Le a) = (Inum bs a \<le> 0)" |
|
119 "Ifm bs (Ge a) = (Inum bs a \<ge> 0)" |
|
120 "Ifm bs (Eq a) = (Inum bs a = 0)" |
|
121 "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)" |
|
122 "Ifm bs (NOT p) = (\<not> (Ifm bs p))" |
|
123 "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)" |
|
124 "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)" |
|
125 "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))" |
|
126 "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)" |
|
127 "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)" |
|
128 "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)" |
|
129 |
|
130 lemma IfmLeSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Le (Sub s t)) = (s' \<le> t')" |
|
131 apply simp |
|
132 done |
|
133 |
|
134 lemma IfmLtSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Lt (Sub s t)) = (s' < t')" |
|
135 apply simp |
|
136 done |
|
137 lemma IfmEqSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Eq (Sub s t)) = (s' = t')" |
|
138 apply simp |
|
139 done |
|
140 lemma IfmNOT: " (Ifm bs p = P) \<Longrightarrow> (Ifm bs (NOT p) = (\<not>P))" |
|
141 apply simp |
|
142 done |
|
143 lemma IfmAnd: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (And p q) = (P \<and> Q))" |
|
144 apply simp |
|
145 done |
|
146 lemma IfmOr: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Or p q) = (P \<or> Q))" |
|
147 apply simp |
|
148 done |
|
149 lemma IfmImp: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Imp p q) = (P \<longrightarrow> Q))" |
|
150 apply simp |
|
151 done |
|
152 lemma IfmIff: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Iff p q) = (P = Q))" |
|
153 apply simp |
|
154 done |
|
155 |
|
156 lemma IfmE: " (!! x. Ifm (x#bs) p = P x) \<Longrightarrow> (Ifm bs (E p) = (\<exists>x. P x))" |
|
157 apply simp |
|
158 done |
|
159 lemma IfmA: " (!! x. Ifm (x#bs) p = P x) \<Longrightarrow> (Ifm bs (A p) = (\<forall>x. P x))" |
|
160 apply simp |
|
161 done |
|
162 |
|
163 consts not:: "fm \<Rightarrow> fm" |
|
164 recdef not "measure size" |
|
165 "not (NOT p) = p" |
|
166 "not T = F" |
|
167 "not F = T" |
|
168 "not p = NOT p" |
|
169 lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)" |
|
170 by (cases p) auto |
|
171 |
|
172 constdefs conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
|
173 "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else |
|
174 if p = q then p else And p q)" |
|
175 lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)" |
|
176 by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all) |
|
177 |
|
178 constdefs disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
|
179 "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p |
|
180 else if p=q then p else Or p q)" |
|
181 |
|
182 lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)" |
|
183 by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) |
|
184 |
|
185 constdefs imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
|
186 "imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p |
|
187 else Imp p q)" |
|
188 lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)" |
|
189 by (cases "p=F \<or> q=T",simp_all add: imp_def) |
|
190 |
|
191 constdefs iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
|
192 "iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else |
|
193 if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else |
|
194 Iff p q)" |
|
195 lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)" |
|
196 by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) |
|
197 |
|
198 lemma conj_simps: |
|
199 "conj F Q = F" |
|
200 "conj P F = F" |
|
201 "conj T Q = Q" |
|
202 "conj P T = P" |
|
203 "conj P P = P" |
|
204 "P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> conj P Q = And P Q" |
|
205 by (simp_all add: conj_def) |
|
206 |
|
207 lemma disj_simps: |
|
208 "disj T Q = T" |
|
209 "disj P T = T" |
|
210 "disj F Q = Q" |
|
211 "disj P F = P" |
|
212 "disj P P = P" |
|
213 "P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> disj P Q = Or P Q" |
|
214 by (simp_all add: disj_def) |
|
215 lemma imp_simps: |
|
216 "imp F Q = T" |
|
217 "imp P T = T" |
|
218 "imp T Q = Q" |
|
219 "imp P F = not P" |
|
220 "imp P P = T" |
|
221 "P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> imp P Q = Imp P Q" |
|
222 by (simp_all add: imp_def) |
|
223 lemma trivNOT: "p \<noteq> NOT p" "NOT p \<noteq> p" |
|
224 apply (induct p, auto) |
|
225 done |
|
226 |
|
227 lemma iff_simps: |
|
228 "iff p p = T" |
|
229 "iff p (NOT p) = F" |
|
230 "iff (NOT p) p = F" |
|
231 "iff p F = not p" |
|
232 "iff F p = not p" |
|
233 "p \<noteq> NOT T \<Longrightarrow> iff T p = p" |
|
234 "p\<noteq> NOT T \<Longrightarrow> iff p T = p" |
|
235 "p\<noteq>q \<Longrightarrow> p\<noteq> NOT q \<Longrightarrow> q\<noteq> NOT p \<Longrightarrow> p\<noteq> F \<Longrightarrow> q\<noteq> F \<Longrightarrow> p \<noteq> T \<Longrightarrow> q \<noteq> T \<Longrightarrow> iff p q = Iff p q" |
|
236 using trivNOT |
|
237 by (simp_all add: iff_def, cases p, auto) |
|
238 (* Quantifier freeness *) |
|
239 consts qfree:: "fm \<Rightarrow> bool" |
|
240 recdef qfree "measure size" |
|
241 "qfree (E p) = False" |
|
242 "qfree (A p) = False" |
|
243 "qfree (NOT p) = qfree p" |
|
244 "qfree (And p q) = (qfree p \<and> qfree q)" |
|
245 "qfree (Or p q) = (qfree p \<and> qfree q)" |
|
246 "qfree (Imp p q) = (qfree p \<and> qfree q)" |
|
247 "qfree (Iff p q) = (qfree p \<and> qfree q)" |
|
248 "qfree p = True" |
|
249 |
|
250 (* Boundedness and substitution *) |
|
251 consts |
|
252 numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) |
|
253 bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) |
|
254 primrec |
|
255 "numbound0 (C c) = True" |
|
256 "numbound0 (Bound n) = (n>0)" |
|
257 "numbound0 (CN n c a) = (n\<noteq>0 \<and> numbound0 a)" |
|
258 "numbound0 (Neg a) = numbound0 a" |
|
259 "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)" |
|
260 "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" |
|
261 "numbound0 (Mul i a) = numbound0 a" |
|
262 lemma numbound0_I: |
|
263 assumes nb: "numbound0 a" |
|
264 shows "Inum (b#bs) a = Inum (b'#bs) a" |
|
265 using nb |
|
266 by (induct a rule: numbound0.induct,auto simp add: nth_pos2) |
|
267 |
|
268 primrec |
|
269 "bound0 T = True" |
|
270 "bound0 F = True" |
|
271 "bound0 (Lt a) = numbound0 a" |
|
272 "bound0 (Le a) = numbound0 a" |
|
273 "bound0 (Gt a) = numbound0 a" |
|
274 "bound0 (Ge a) = numbound0 a" |
|
275 "bound0 (Eq a) = numbound0 a" |
|
276 "bound0 (NEq a) = numbound0 a" |
|
277 "bound0 (NOT p) = bound0 p" |
|
278 "bound0 (And p q) = (bound0 p \<and> bound0 q)" |
|
279 "bound0 (Or p q) = (bound0 p \<and> bound0 q)" |
|
280 "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))" |
|
281 "bound0 (Iff p q) = (bound0 p \<and> bound0 q)" |
|
282 "bound0 (E p) = False" |
|
283 "bound0 (A p) = False" |
|
284 |
|
285 lemma bound0_I: |
|
286 assumes bp: "bound0 p" |
|
287 shows "Ifm (b#bs) p = Ifm (b'#bs) p" |
|
288 using bp numbound0_I[where b="b" and bs="bs" and b'="b'"] |
|
289 by (induct p rule: bound0.induct) (auto simp add: nth_pos2) |
|
290 |
|
291 lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" |
|
292 by (cases p, auto) |
|
293 lemma not_bn[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" |
|
294 by (cases p, auto) |
|
295 |
|
296 |
|
297 lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)" |
|
298 using conj_def by auto |
|
299 lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)" |
|
300 using conj_def by auto |
|
301 |
|
302 lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)" |
|
303 using disj_def by auto |
|
304 lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)" |
|
305 using disj_def by auto |
|
306 |
|
307 lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)" |
|
308 using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) |
|
309 lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)" |
|
310 using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) |
|
311 |
|
312 lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)" |
|
313 by (unfold iff_def,cases "p=q", auto) |
|
314 lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)" |
|
315 using iff_def by (unfold iff_def,cases "p=q", auto) |
|
316 |
|
317 consts |
|
318 decrnum:: "num \<Rightarrow> num" |
|
319 decr :: "fm \<Rightarrow> fm" |
|
320 |
|
321 recdef decrnum "measure size" |
|
322 "decrnum (Bound n) = Bound (n - 1)" |
|
323 "decrnum (Neg a) = Neg (decrnum a)" |
|
324 "decrnum (Add a b) = Add (decrnum a) (decrnum b)" |
|
325 "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)" |
|
326 "decrnum (Mul c a) = Mul c (decrnum a)" |
|
327 "decrnum (CN n c a) = CN (n - 1) c (decrnum a)" |
|
328 "decrnum a = a" |
|
329 |
|
330 recdef decr "measure size" |
|
331 "decr (Lt a) = Lt (decrnum a)" |
|
332 "decr (Le a) = Le (decrnum a)" |
|
333 "decr (Gt a) = Gt (decrnum a)" |
|
334 "decr (Ge a) = Ge (decrnum a)" |
|
335 "decr (Eq a) = Eq (decrnum a)" |
|
336 "decr (NEq a) = NEq (decrnum a)" |
|
337 "decr (NOT p) = NOT (decr p)" |
|
338 "decr (And p q) = conj (decr p) (decr q)" |
|
339 "decr (Or p q) = disj (decr p) (decr q)" |
|
340 "decr (Imp p q) = imp (decr p) (decr q)" |
|
341 "decr (Iff p q) = iff (decr p) (decr q)" |
|
342 "decr p = p" |
|
343 |
|
344 lemma decrnum: assumes nb: "numbound0 t" |
|
345 shows "Inum (x#bs) t = Inum bs (decrnum t)" |
|
346 using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2) |
|
347 |
|
348 lemma decr: assumes nb: "bound0 p" |
|
349 shows "Ifm (x#bs) p = Ifm bs (decr p)" |
|
350 using nb |
|
351 by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum) |
|
352 |
|
353 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)" |
|
354 by (induct p, simp_all) |
|
355 |
|
356 consts |
|
357 isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) |
|
358 recdef isatom "measure size" |
|
359 "isatom T = True" |
|
360 "isatom F = True" |
|
361 "isatom (Lt a) = True" |
|
362 "isatom (Le a) = True" |
|
363 "isatom (Gt a) = True" |
|
364 "isatom (Ge a) = True" |
|
365 "isatom (Eq a) = True" |
|
366 "isatom (NEq a) = True" |
|
367 "isatom p = False" |
|
368 |
|
369 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" |
|
370 by (induct p, simp_all) |
|
371 |
|
372 constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" |
|
373 "djf f p q \<equiv> (if q=T then T else if q=F then f p else |
|
374 (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))" |
|
375 constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" |
|
376 "evaldjf f ps \<equiv> foldr (djf f) ps F" |
|
377 |
|
378 lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)" |
|
379 by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) |
|
380 (cases "f p", simp_all add: Let_def djf_def) |
|
381 |
|
382 |
|
383 lemma djf_simps: |
|
384 "djf f p T = T" |
|
385 "djf f p F = f p" |
|
386 "q\<noteq>T \<Longrightarrow> q\<noteq>F \<Longrightarrow> djf f p q = (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q)" |
|
387 by (simp_all add: djf_def) |
|
388 |
|
389 lemma evaldjf_ex: "Ifm bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bs (f p))" |
|
390 by(induct ps, simp_all add: evaldjf_def djf_Or) |
|
391 |
|
392 lemma evaldjf_bound0: |
|
393 assumes nb: "\<forall> x\<in> set xs. bound0 (f x)" |
|
394 shows "bound0 (evaldjf f xs)" |
|
395 using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) |
|
396 |
|
397 lemma evaldjf_qf: |
|
398 assumes nb: "\<forall> x\<in> set xs. qfree (f x)" |
|
399 shows "qfree (evaldjf f xs)" |
|
400 using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) |
|
401 |
|
402 consts disjuncts :: "fm \<Rightarrow> fm list" |
|
403 recdef disjuncts "measure size" |
|
404 "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" |
|
405 "disjuncts F = []" |
|
406 "disjuncts p = [p]" |
|
407 |
|
408 lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p" |
|
409 by(induct p rule: disjuncts.induct, auto) |
|
410 |
|
411 lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q" |
|
412 proof- |
|
413 assume nb: "bound0 p" |
|
414 hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto) |
|
415 thus ?thesis by (simp only: list_all_iff) |
|
416 qed |
|
417 |
|
418 lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q" |
|
419 proof- |
|
420 assume qf: "qfree p" |
|
421 hence "list_all qfree (disjuncts p)" |
|
422 by (induct p rule: disjuncts.induct, auto) |
|
423 thus ?thesis by (simp only: list_all_iff) |
|
424 qed |
|
425 |
|
426 constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" |
|
427 "DJ f p \<equiv> evaldjf f (disjuncts p)" |
|
428 |
|
429 lemma DJ: assumes fdj: "\<forall> p q. Ifm bs (f (Or p q)) = Ifm bs (Or (f p) (f q))" |
|
430 and fF: "f F = F" |
|
431 shows "Ifm bs (DJ f p) = Ifm bs (f p)" |
|
432 proof- |
|
433 have "Ifm bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bs (f q))" |
|
434 by (simp add: DJ_def evaldjf_ex) |
|
435 also have "\<dots> = Ifm bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto) |
|
436 finally show ?thesis . |
|
437 qed |
|
438 |
|
439 lemma DJ_qf: assumes |
|
440 fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)" |
|
441 shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) " |
|
442 proof(clarify) |
|
443 fix p assume qf: "qfree p" |
|
444 have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def) |
|
445 from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" . |
|
446 with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast |
|
447 |
|
448 from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp |
|
449 qed |
|
450 |
|
451 lemma DJ_qe: assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))" |
|
452 shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bs ((DJ qe p)) = Ifm bs (E p))" |
|
453 proof(clarify) |
|
454 fix p::fm and bs |
|
455 assume qf: "qfree p" |
|
456 from qe have qth: "\<forall> p. qfree p \<longrightarrow> qfree (qe p)" by blast |
|
457 from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto |
|
458 have "Ifm bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm bs (qe q))" |
|
459 by (simp add: DJ_def evaldjf_ex) |
|
460 also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bs (E q))" using qe disjuncts_qf[OF qf] by auto |
|
461 also have "\<dots> = Ifm bs (E p)" by (induct p rule: disjuncts.induct, auto) |
|
462 finally show "qfree (DJ qe p) \<and> Ifm bs (DJ qe p) = Ifm bs (E p)" using qfth by blast |
|
463 qed |
|
464 (* Simplification *) |
|
465 consts |
|
466 numgcd :: "num \<Rightarrow> int" |
|
467 numgcdh:: "num \<Rightarrow> int \<Rightarrow> int" |
|
468 reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num" |
|
469 reducecoeff :: "num \<Rightarrow> num" |
|
470 dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" |
|
471 consts maxcoeff:: "num \<Rightarrow> int" |
|
472 recdef maxcoeff "measure size" |
|
473 "maxcoeff (C i) = abs i" |
|
474 "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)" |
|
475 "maxcoeff t = 1" |
|
476 |
|
477 lemma maxcoeff_pos: "maxcoeff t \<ge> 0" |
|
478 by (induct t rule: maxcoeff.induct, auto) |
|
479 |
|
480 recdef numgcdh "measure size" |
|
481 "numgcdh (C i) = (\<lambda>g. zgcd i g)" |
|
482 "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))" |
|
483 "numgcdh t = (\<lambda>g. 1)" |
|
484 defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)" |
|
485 |
|
486 recdef reducecoeffh "measure size" |
|
487 "reducecoeffh (C i) = (\<lambda> g. C (i div g))" |
|
488 "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))" |
|
489 "reducecoeffh t = (\<lambda>g. t)" |
|
490 |
|
491 defs reducecoeff_def: "reducecoeff t \<equiv> |
|
492 (let g = numgcd t in |
|
493 if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)" |
|
494 |
|
495 recdef dvdnumcoeff "measure size" |
|
496 "dvdnumcoeff (C i) = (\<lambda> g. g dvd i)" |
|
497 "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))" |
|
498 "dvdnumcoeff t = (\<lambda>g. False)" |
|
499 |
|
500 lemma dvdnumcoeff_trans: |
|
501 assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'" |
|
502 shows "dvdnumcoeff t g" |
|
503 using dgt' gdg |
|
504 by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg]) |
|
505 |
|
506 declare zdvd_trans [trans add] |
|
507 |
|
508 lemma natabs0: "(nat (abs x) = 0) = (x = 0)" |
|
509 by arith |
|
510 |
|
511 lemma numgcd0: |
|
512 assumes g0: "numgcd t = 0" |
|
513 shows "Inum bs t = 0" |
|
514 using g0[simplified numgcd_def] |
|
515 by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos) |
|
516 |
|
517 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0" |
|
518 using gp |
|
519 by (induct t rule: numgcdh.induct, auto simp add: zgcd_def) |
|
520 |
|
521 lemma numgcd_pos: "numgcd t \<ge>0" |
|
522 by (simp add: numgcd_def numgcdh_pos maxcoeff_pos) |
|
523 |
|
524 lemma reducecoeffh: |
|
525 assumes gt: "dvdnumcoeff t g" and gp: "g > 0" |
|
526 shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t" |
|
527 using gt |
|
528 proof(induct t rule: reducecoeffh.induct) |
|
529 case (1 i) hence gd: "g dvd i" by simp |
|
530 from gp have gnz: "g \<noteq> 0" by simp |
|
531 from prems show ?case by (simp add: real_of_int_div[OF gnz gd]) |
|
532 next |
|
533 case (2 n c t) hence gd: "g dvd c" by simp |
|
534 from gp have gnz: "g \<noteq> 0" by simp |
|
535 from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) |
|
536 qed (auto simp add: numgcd_def gp) |
|
537 consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" |
|
538 recdef ismaxcoeff "measure size" |
|
539 "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)" |
|
540 "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))" |
|
541 "ismaxcoeff t = (\<lambda>x. True)" |
|
542 |
|
543 lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'" |
|
544 by (induct t rule: ismaxcoeff.induct, auto) |
|
545 |
|
546 lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)" |
|
547 proof (induct t rule: maxcoeff.induct) |
|
548 case (2 n c t) |
|
549 hence H:"ismaxcoeff t (maxcoeff t)" . |
|
550 have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2) |
|
551 from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1) |
|
552 qed simp_all |
|
553 |
|
554 lemma zgcd_gt1: "zgcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))" |
|
555 apply (cases "abs i = 0", simp_all add: zgcd_def) |
|
556 apply (cases "abs j = 0", simp_all) |
|
557 apply (cases "abs i = 1", simp_all) |
|
558 apply (cases "abs j = 1", simp_all) |
|
559 apply auto |
|
560 done |
|
561 lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0" |
|
562 by (induct t rule: numgcdh.induct, auto simp add:zgcd0) |
|
563 |
|
564 lemma dvdnumcoeff_aux: |
|
565 assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1" |
|
566 shows "dvdnumcoeff t (numgcdh t m)" |
|
567 using prems |
|
568 proof(induct t rule: numgcdh.induct) |
|
569 case (2 n c t) |
|
570 let ?g = "numgcdh t m" |
|
571 from prems have th:"zgcd c ?g > 1" by simp |
|
572 from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] |
|
573 have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp |
|
574 moreover {assume "abs c > 1" and gp: "?g > 1" with prems |
|
575 have th: "dvdnumcoeff t ?g" by simp |
|
576 have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2) |
|
577 from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)} |
|
578 moreover {assume "abs c = 0 \<and> ?g > 1" |
|
579 with prems have th: "dvdnumcoeff t ?g" by simp |
|
580 have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2) |
|
581 from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1) |
|
582 hence ?case by simp } |
|
583 moreover {assume "abs c > 1" and g0:"?g = 0" |
|
584 from numgcdh0[OF g0] have "m=0". with prems have ?case by simp } |
|
585 ultimately show ?case by blast |
|
586 qed(auto simp add: zgcd_zdvd1) |
|
587 |
|
588 lemma dvdnumcoeff_aux2: |
|
589 assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0" |
|
590 using prems |
|
591 proof (simp add: numgcd_def) |
|
592 let ?mc = "maxcoeff t" |
|
593 let ?g = "numgcdh t ?mc" |
|
594 have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff) |
|
595 have th2: "?mc \<ge> 0" by (rule maxcoeff_pos) |
|
596 assume H: "numgcdh t ?mc > 1" |
|
597 from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . |
|
598 qed |
|
599 |
|
600 lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t" |
|
601 proof- |
|
602 let ?g = "numgcd t" |
|
603 have "?g \<ge> 0" by (simp add: numgcd_pos) |
|
604 hence "?g = 0 \<or> ?g = 1 \<or> ?g > 1" by auto |
|
605 moreover {assume "?g = 0" hence ?thesis by (simp add: numgcd0)} |
|
606 moreover {assume "?g = 1" hence ?thesis by (simp add: reducecoeff_def)} |
|
607 moreover { assume g1:"?g > 1" |
|
608 from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" and g0: "?g > 0" by blast+ |
|
609 from reducecoeffh[OF th1 g0, where bs="bs"] g1 have ?thesis |
|
610 by (simp add: reducecoeff_def Let_def)} |
|
611 ultimately show ?thesis by blast |
|
612 qed |
|
613 |
|
614 lemma reducecoeffh_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeffh t g)" |
|
615 by (induct t rule: reducecoeffh.induct, auto) |
|
616 |
|
617 lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)" |
|
618 using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def) |
|
619 |
|
620 consts |
|
621 simpnum:: "num \<Rightarrow> num" |
|
622 numadd:: "num \<times> num \<Rightarrow> num" |
|
623 nummul:: "num \<Rightarrow> int \<Rightarrow> num" |
|
624 recdef numadd "measure (\<lambda> (t,s). size t + size s)" |
|
625 "numadd (CN n1 c1 r1,CN n2 c2 r2) = |
|
626 (if n1=n2 then |
|
627 (let c = c1 + c2 |
|
628 in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2)))) |
|
629 else if n1 \<le> n2 then (CN n1 c1 (numadd (r1,CN n2 c2 r2))) |
|
630 else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))" |
|
631 "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))" |
|
632 "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" |
|
633 "numadd (C b1, C b2) = C (b1+b2)" |
|
634 "numadd (a,b) = Add a b" |
|
635 |
|
636 lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" |
|
637 apply (induct t s rule: numadd.induct, simp_all add: Let_def) |
|
638 apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all) |
|
639 apply (case_tac "n1 = n2", simp_all add: algebra_simps) |
|
640 by (simp only: left_distrib[symmetric],simp) |
|
641 |
|
642 lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))" |
|
643 by (induct t s rule: numadd.induct, auto simp add: Let_def) |
|
644 |
|
645 recdef nummul "measure size" |
|
646 "nummul (C j) = (\<lambda> i. C (i*j))" |
|
647 "nummul (CN n c a) = (\<lambda> i. CN n (i*c) (nummul a i))" |
|
648 "nummul t = (\<lambda> i. Mul i t)" |
|
649 |
|
650 lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)" |
|
651 by (induct t rule: nummul.induct, auto simp add: algebra_simps) |
|
652 |
|
653 lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)" |
|
654 by (induct t rule: nummul.induct, auto ) |
|
655 |
|
656 constdefs numneg :: "num \<Rightarrow> num" |
|
657 "numneg t \<equiv> nummul t (- 1)" |
|
658 |
|
659 constdefs numsub :: "num \<Rightarrow> num \<Rightarrow> num" |
|
660 "numsub s t \<equiv> (if s = t then C 0 else numadd (s,numneg t))" |
|
661 |
|
662 lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)" |
|
663 using numneg_def by simp |
|
664 |
|
665 lemma numneg_nb[simp]: "numbound0 t \<Longrightarrow> numbound0 (numneg t)" |
|
666 using numneg_def by simp |
|
667 |
|
668 lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)" |
|
669 using numsub_def by simp |
|
670 |
|
671 lemma numsub_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)" |
|
672 using numsub_def by simp |
|
673 |
|
674 recdef simpnum "measure size" |
|
675 "simpnum (C j) = C j" |
|
676 "simpnum (Bound n) = CN n 1 (C 0)" |
|
677 "simpnum (Neg t) = numneg (simpnum t)" |
|
678 "simpnum (Add t s) = numadd (simpnum t,simpnum s)" |
|
679 "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)" |
|
680 "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)" |
|
681 "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0),simpnum t))" |
|
682 |
|
683 lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t" |
|
684 by (induct t rule: simpnum.induct, auto simp add: numneg numadd numsub nummul) |
|
685 |
|
686 lemma simpnum_numbound0[simp]: |
|
687 "numbound0 t \<Longrightarrow> numbound0 (simpnum t)" |
|
688 by (induct t rule: simpnum.induct, auto) |
|
689 |
|
690 consts nozerocoeff:: "num \<Rightarrow> bool" |
|
691 recdef nozerocoeff "measure size" |
|
692 "nozerocoeff (C c) = True" |
|
693 "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)" |
|
694 "nozerocoeff t = True" |
|
695 |
|
696 lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))" |
|
697 by (induct a b rule: numadd.induct,auto simp add: Let_def) |
|
698 |
|
699 lemma nummul_nz : "\<And> i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)" |
|
700 by (induct a rule: nummul.induct,auto simp add: Let_def numadd_nz) |
|
701 |
|
702 lemma numneg_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff (numneg a)" |
|
703 by (simp add: numneg_def nummul_nz) |
|
704 |
|
705 lemma numsub_nz: "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numsub a b)" |
|
706 by (simp add: numsub_def numneg_nz numadd_nz) |
|
707 |
|
708 lemma simpnum_nz: "nozerocoeff (simpnum t)" |
|
709 by(induct t rule: simpnum.induct, auto simp add: numadd_nz numneg_nz numsub_nz nummul_nz) |
|
710 |
|
711 lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0" |
|
712 proof (induct t rule: maxcoeff.induct) |
|
713 case (2 n c t) |
|
714 hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ |
|
715 have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) |
|
716 with cnz have "max (abs c) (maxcoeff t) > 0" by arith |
|
717 with prems show ?case by simp |
|
718 qed auto |
|
719 |
|
720 lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" |
|
721 proof- |
|
722 from g0 have th:"numgcdh t (maxcoeff t) = 0" by (simp add: numgcd_def) |
|
723 from numgcdh0[OF th] have th:"maxcoeff t = 0" . |
|
724 from maxcoeff_nz[OF nz th] show ?thesis . |
|
725 qed |
|
726 |
|
727 constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int" |
|
728 "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else |
|
729 (let t' = simpnum t ; g = numgcd t' in |
|
730 if g > 1 then (let g' = zgcd n g in |
|
731 if g' = 1 then (t',n) |
|
732 else (reducecoeffh t' g', n div g')) |
|
733 else (t',n))))" |
|
734 |
|
735 lemma simp_num_pair_ci: |
|
736 shows "((\<lambda> (t,n). Inum bs t / real n) (simp_num_pair (t,n))) = ((\<lambda> (t,n). Inum bs t / real n) (t,n))" |
|
737 (is "?lhs = ?rhs") |
|
738 proof- |
|
739 let ?t' = "simpnum t" |
|
740 let ?g = "numgcd ?t'" |
|
741 let ?g' = "zgcd n ?g" |
|
742 {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)} |
|
743 moreover |
|
744 { assume nnz: "n \<noteq> 0" |
|
745 {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)} |
|
746 moreover |
|
747 {assume g1:"?g>1" hence g0: "?g > 0" by simp |
|
748 from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp |
|
749 hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith |
|
750 hence "?g'= 1 \<or> ?g' > 1" by arith |
|
751 moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)} |
|
752 moreover {assume g'1:"?g'>1" |
|
753 from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" .. |
|
754 let ?tt = "reducecoeffh ?t' ?g'" |
|
755 let ?t = "Inum bs ?tt" |
|
756 have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2) |
|
757 have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) |
|
758 have gpdgp: "?g' dvd ?g'" by simp |
|
759 from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] |
|
760 have th2:"real ?g' * ?t = Inum bs ?t'" by simp |
|
761 from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) |
|
762 also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp |
|
763 also have "\<dots> = (Inum bs ?t' / real n)" |
|
764 using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp |
|
765 finally have "?lhs = Inum bs t / real n" by (simp add: simpnum_ci) |
|
766 then have ?thesis using prems by (simp add: simp_num_pair_def)} |
|
767 ultimately have ?thesis by blast} |
|
768 ultimately have ?thesis by blast} |
|
769 ultimately show ?thesis by blast |
|
770 qed |
|
771 |
|
772 lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" |
|
773 shows "numbound0 t' \<and> n' >0" |
|
774 proof- |
|
775 let ?t' = "simpnum t" |
|
776 let ?g = "numgcd ?t'" |
|
777 let ?g' = "zgcd n ?g" |
|
778 {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)} |
|
779 moreover |
|
780 { assume nnz: "n \<noteq> 0" |
|
781 {assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} |
|
782 moreover |
|
783 {assume g1:"?g>1" hence g0: "?g > 0" by simp |
|
784 from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp |
|
785 hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith |
|
786 hence "?g'= 1 \<or> ?g' > 1" by arith |
|
787 moreover {assume "?g'=1" hence ?thesis using prems |
|
788 by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} |
|
789 moreover {assume g'1:"?g'>1" |
|
790 have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2) |
|
791 have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) |
|
792 have gpdgp: "?g' dvd ?g'" by simp |
|
793 from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" . |
|
794 from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] |
|
795 have "n div ?g' >0" by simp |
|
796 hence ?thesis using prems |
|
797 by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)} |
|
798 ultimately have ?thesis by blast} |
|
799 ultimately have ?thesis by blast} |
|
800 ultimately show ?thesis by blast |
|
801 qed |
|
802 |
|
803 consts simpfm :: "fm \<Rightarrow> fm" |
|
804 recdef simpfm "measure fmsize" |
|
805 "simpfm (And p q) = conj (simpfm p) (simpfm q)" |
|
806 "simpfm (Or p q) = disj (simpfm p) (simpfm q)" |
|
807 "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" |
|
808 "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" |
|
809 "simpfm (NOT p) = not (simpfm p)" |
|
810 "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F |
|
811 | _ \<Rightarrow> Lt a')" |
|
812 "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0) then T else F | _ \<Rightarrow> Le a')" |
|
813 "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F | _ \<Rightarrow> Gt a')" |
|
814 "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F | _ \<Rightarrow> Ge a')" |
|
815 "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq a')" |
|
816 "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq a')" |
|
817 "simpfm p = p" |
|
818 lemma simpfm: "Ifm bs (simpfm p) = Ifm bs p" |
|
819 proof(induct p rule: simpfm.induct) |
|
820 case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
821 {fix v assume "?sa = C v" hence ?case using sa by simp } |
|
822 moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa |
|
823 by (cases ?sa, simp_all add: Let_def)} |
|
824 ultimately show ?case by blast |
|
825 next |
|
826 case (7 a) let ?sa = "simpnum a" |
|
827 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
828 {fix v assume "?sa = C v" hence ?case using sa by simp } |
|
829 moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa |
|
830 by (cases ?sa, simp_all add: Let_def)} |
|
831 ultimately show ?case by blast |
|
832 next |
|
833 case (8 a) let ?sa = "simpnum a" |
|
834 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
835 {fix v assume "?sa = C v" hence ?case using sa by simp } |
|
836 moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa |
|
837 by (cases ?sa, simp_all add: Let_def)} |
|
838 ultimately show ?case by blast |
|
839 next |
|
840 case (9 a) let ?sa = "simpnum a" |
|
841 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
842 {fix v assume "?sa = C v" hence ?case using sa by simp } |
|
843 moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa |
|
844 by (cases ?sa, simp_all add: Let_def)} |
|
845 ultimately show ?case by blast |
|
846 next |
|
847 case (10 a) let ?sa = "simpnum a" |
|
848 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
849 {fix v assume "?sa = C v" hence ?case using sa by simp } |
|
850 moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa |
|
851 by (cases ?sa, simp_all add: Let_def)} |
|
852 ultimately show ?case by blast |
|
853 next |
|
854 case (11 a) let ?sa = "simpnum a" |
|
855 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
856 {fix v assume "?sa = C v" hence ?case using sa by simp } |
|
857 moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa |
|
858 by (cases ?sa, simp_all add: Let_def)} |
|
859 ultimately show ?case by blast |
|
860 qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not) |
|
861 |
|
862 |
|
863 lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)" |
|
864 proof(induct p rule: simpfm.induct) |
|
865 case (6 a) hence nb: "numbound0 a" by simp |
|
866 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
867 thus ?case by (cases "simpnum a", auto simp add: Let_def) |
|
868 next |
|
869 case (7 a) hence nb: "numbound0 a" by simp |
|
870 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
871 thus ?case by (cases "simpnum a", auto simp add: Let_def) |
|
872 next |
|
873 case (8 a) hence nb: "numbound0 a" by simp |
|
874 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
875 thus ?case by (cases "simpnum a", auto simp add: Let_def) |
|
876 next |
|
877 case (9 a) hence nb: "numbound0 a" by simp |
|
878 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
879 thus ?case by (cases "simpnum a", auto simp add: Let_def) |
|
880 next |
|
881 case (10 a) hence nb: "numbound0 a" by simp |
|
882 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
883 thus ?case by (cases "simpnum a", auto simp add: Let_def) |
|
884 next |
|
885 case (11 a) hence nb: "numbound0 a" by simp |
|
886 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
887 thus ?case by (cases "simpnum a", auto simp add: Let_def) |
|
888 qed(auto simp add: disj_def imp_def iff_def conj_def not_bn) |
|
889 |
|
890 lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)" |
|
891 by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) |
|
892 (case_tac "simpnum a",auto)+ |
|
893 |
|
894 consts prep :: "fm \<Rightarrow> fm" |
|
895 recdef prep "measure fmsize" |
|
896 "prep (E T) = T" |
|
897 "prep (E F) = F" |
|
898 "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))" |
|
899 "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))" |
|
900 "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" |
|
901 "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))" |
|
902 "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))" |
|
903 "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" |
|
904 "prep (E p) = E (prep p)" |
|
905 "prep (A (And p q)) = conj (prep (A p)) (prep (A q))" |
|
906 "prep (A p) = prep (NOT (E (NOT p)))" |
|
907 "prep (NOT (NOT p)) = prep p" |
|
908 "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))" |
|
909 "prep (NOT (A p)) = prep (E (NOT p))" |
|
910 "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))" |
|
911 "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))" |
|
912 "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))" |
|
913 "prep (NOT p) = not (prep p)" |
|
914 "prep (Or p q) = disj (prep p) (prep q)" |
|
915 "prep (And p q) = conj (prep p) (prep q)" |
|
916 "prep (Imp p q) = prep (Or (NOT p) q)" |
|
917 "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))" |
|
918 "prep p = p" |
|
919 (hints simp add: fmsize_pos) |
|
920 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p" |
|
921 by (induct p rule: prep.induct, auto) |
|
922 |
|
923 (* Generic quantifier elimination *) |
|
924 consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" |
|
925 recdef qelim "measure fmsize" |
|
926 "qelim (E p) = (\<lambda> qe. DJ qe (qelim p qe))" |
|
927 "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))" |
|
928 "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))" |
|
929 "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" |
|
930 "qelim (Or p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" |
|
931 "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))" |
|
932 "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))" |
|
933 "qelim p = (\<lambda> y. simpfm p)" |
|
934 |
|
935 lemma qelim_ci: |
|
936 assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))" |
|
937 shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)" |
|
938 using qe_inv DJ_qe[OF qe_inv] |
|
939 by(induct p rule: qelim.induct) |
|
940 (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf |
|
941 simpfm simpfm_qf simp del: simpfm.simps) |
|
942 |
|
943 consts |
|
944 plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*) |
|
945 minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*) |
|
946 recdef minusinf "measure size" |
|
947 "minusinf (And p q) = conj (minusinf p) (minusinf q)" |
|
948 "minusinf (Or p q) = disj (minusinf p) (minusinf q)" |
|
949 "minusinf (Eq (CN 0 c e)) = F" |
|
950 "minusinf (NEq (CN 0 c e)) = T" |
|
951 "minusinf (Lt (CN 0 c e)) = T" |
|
952 "minusinf (Le (CN 0 c e)) = T" |
|
953 "minusinf (Gt (CN 0 c e)) = F" |
|
954 "minusinf (Ge (CN 0 c e)) = F" |
|
955 "minusinf p = p" |
|
956 |
|
957 recdef plusinf "measure size" |
|
958 "plusinf (And p q) = conj (plusinf p) (plusinf q)" |
|
959 "plusinf (Or p q) = disj (plusinf p) (plusinf q)" |
|
960 "plusinf (Eq (CN 0 c e)) = F" |
|
961 "plusinf (NEq (CN 0 c e)) = T" |
|
962 "plusinf (Lt (CN 0 c e)) = F" |
|
963 "plusinf (Le (CN 0 c e)) = F" |
|
964 "plusinf (Gt (CN 0 c e)) = T" |
|
965 "plusinf (Ge (CN 0 c e)) = T" |
|
966 "plusinf p = p" |
|
967 |
|
968 consts |
|
969 isrlfm :: "fm \<Rightarrow> bool" (* Linearity test for fm *) |
|
970 recdef isrlfm "measure size" |
|
971 "isrlfm (And p q) = (isrlfm p \<and> isrlfm q)" |
|
972 "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)" |
|
973 "isrlfm (Eq (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
|
974 "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
|
975 "isrlfm (Lt (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
|
976 "isrlfm (Le (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
|
977 "isrlfm (Gt (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
|
978 "isrlfm (Ge (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
|
979 "isrlfm p = (isatom p \<and> (bound0 p))" |
|
980 |
|
981 (* splits the bounded from the unbounded part*) |
|
982 consts rsplit0 :: "num \<Rightarrow> int \<times> num" |
|
983 recdef rsplit0 "measure num_size" |
|
984 "rsplit0 (Bound 0) = (1,C 0)" |
|
985 "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a ; (cb,tb) = rsplit0 b |
|
986 in (ca+cb, Add ta tb))" |
|
987 "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))" |
|
988 "rsplit0 (Neg a) = (let (c,t) = rsplit0 a in (-c,Neg t))" |
|
989 "rsplit0 (Mul c a) = (let (ca,ta) = rsplit0 a in (c*ca,Mul c ta))" |
|
990 "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c+ca,ta))" |
|
991 "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca,CN n c ta))" |
|
992 "rsplit0 t = (0,t)" |
|
993 lemma rsplit0: |
|
994 shows "Inum bs ((split (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))" |
|
995 proof (induct t rule: rsplit0.induct) |
|
996 case (2 a b) |
|
997 let ?sa = "rsplit0 a" let ?sb = "rsplit0 b" |
|
998 let ?ca = "fst ?sa" let ?cb = "fst ?sb" |
|
999 let ?ta = "snd ?sa" let ?tb = "snd ?sb" |
|
1000 from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))" |
|
1001 by(cases "rsplit0 a",auto simp add: Let_def split_def) |
|
1002 have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = |
|
1003 Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)" |
|
1004 by (simp add: Let_def split_def algebra_simps) |
|
1005 also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a", simp_all) |
|
1006 finally show ?case using nb by simp |
|
1007 qed(auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric]) |
|
1008 |
|
1009 (* Linearize a formula*) |
|
1010 definition |
|
1011 lt :: "int \<Rightarrow> num \<Rightarrow> fm" |
|
1012 where |
|
1013 "lt c t = (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t)) |
|
1014 else (Gt (CN 0 (-c) (Neg t))))" |
|
1015 |
|
1016 definition |
|
1017 le :: "int \<Rightarrow> num \<Rightarrow> fm" |
|
1018 where |
|
1019 "le c t = (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t)) |
|
1020 else (Ge (CN 0 (-c) (Neg t))))" |
|
1021 |
|
1022 definition |
|
1023 gt :: "int \<Rightarrow> num \<Rightarrow> fm" |
|
1024 where |
|
1025 "gt c t = (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t)) |
|
1026 else (Lt (CN 0 (-c) (Neg t))))" |
|
1027 |
|
1028 definition |
|
1029 ge :: "int \<Rightarrow> num \<Rightarrow> fm" |
|
1030 where |
|
1031 "ge c t = (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t)) |
|
1032 else (Le (CN 0 (-c) (Neg t))))" |
|
1033 |
|
1034 definition |
|
1035 eq :: "int \<Rightarrow> num \<Rightarrow> fm" |
|
1036 where |
|
1037 "eq c t = (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t)) |
|
1038 else (Eq (CN 0 (-c) (Neg t))))" |
|
1039 |
|
1040 definition |
|
1041 neq :: "int \<Rightarrow> num \<Rightarrow> fm" |
|
1042 where |
|
1043 "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t)) |
|
1044 else (NEq (CN 0 (-c) (Neg t))))" |
|
1045 |
|
1046 lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))" |
|
1047 using rsplit0[where bs = "bs" and t="t"] |
|
1048 by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,case_tac "nat",auto) |
|
1049 |
|
1050 lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) = Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))" |
|
1051 using rsplit0[where bs = "bs" and t="t"] |
|
1052 by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) |
|
1053 |
|
1054 lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) = Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))" |
|
1055 using rsplit0[where bs = "bs" and t="t"] |
|
1056 by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) |
|
1057 |
|
1058 lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) = Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))" |
|
1059 using rsplit0[where bs = "bs" and t="t"] |
|
1060 by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) |
|
1061 |
|
1062 lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) = Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))" |
|
1063 using rsplit0[where bs = "bs" and t="t"] |
|
1064 by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) |
|
1065 |
|
1066 lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) = Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))" |
|
1067 using rsplit0[where bs = "bs" and t="t"] |
|
1068 by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) |
|
1069 |
|
1070 lemma conj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)" |
|
1071 by (auto simp add: conj_def) |
|
1072 lemma disj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)" |
|
1073 by (auto simp add: disj_def) |
|
1074 |
|
1075 consts rlfm :: "fm \<Rightarrow> fm" |
|
1076 recdef rlfm "measure fmsize" |
|
1077 "rlfm (And p q) = conj (rlfm p) (rlfm q)" |
|
1078 "rlfm (Or p q) = disj (rlfm p) (rlfm q)" |
|
1079 "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)" |
|
1080 "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))" |
|
1081 "rlfm (Lt a) = split lt (rsplit0 a)" |
|
1082 "rlfm (Le a) = split le (rsplit0 a)" |
|
1083 "rlfm (Gt a) = split gt (rsplit0 a)" |
|
1084 "rlfm (Ge a) = split ge (rsplit0 a)" |
|
1085 "rlfm (Eq a) = split eq (rsplit0 a)" |
|
1086 "rlfm (NEq a) = split neq (rsplit0 a)" |
|
1087 "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))" |
|
1088 "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))" |
|
1089 "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))" |
|
1090 "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))" |
|
1091 "rlfm (NOT (NOT p)) = rlfm p" |
|
1092 "rlfm (NOT T) = F" |
|
1093 "rlfm (NOT F) = T" |
|
1094 "rlfm (NOT (Lt a)) = rlfm (Ge a)" |
|
1095 "rlfm (NOT (Le a)) = rlfm (Gt a)" |
|
1096 "rlfm (NOT (Gt a)) = rlfm (Le a)" |
|
1097 "rlfm (NOT (Ge a)) = rlfm (Lt a)" |
|
1098 "rlfm (NOT (Eq a)) = rlfm (NEq a)" |
|
1099 "rlfm (NOT (NEq a)) = rlfm (Eq a)" |
|
1100 "rlfm p = p" (hints simp add: fmsize_pos) |
|
1101 |
|
1102 lemma rlfm_I: |
|
1103 assumes qfp: "qfree p" |
|
1104 shows "(Ifm bs (rlfm p) = Ifm bs p) \<and> isrlfm (rlfm p)" |
|
1105 using qfp |
|
1106 by (induct p rule: rlfm.induct, auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin) |
|
1107 |
|
1108 (* Operations needed for Ferrante and Rackoff *) |
|
1109 lemma rminusinf_inf: |
|
1110 assumes lp: "isrlfm p" |
|
1111 shows "\<exists> z. \<forall> x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\<exists> z. \<forall> x. ?P z x p") |
|
1112 using lp |
|
1113 proof (induct p rule: minusinf.induct) |
|
1114 case (1 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto |
|
1115 next |
|
1116 case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto |
|
1117 next |
|
1118 case (3 c e) |
|
1119 from prems have nb: "numbound0 e" by simp |
|
1120 from prems have cp: "real c > 0" by simp |
|
1121 fix a |
|
1122 let ?e="Inum (a#bs) e" |
|
1123 let ?z = "(- ?e) / real c" |
|
1124 {fix x |
|
1125 assume xz: "x < ?z" |
|
1126 hence "(real c * x < - ?e)" |
|
1127 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) |
|
1128 hence "real c * x + ?e < 0" by arith |
|
1129 hence "real c * x + ?e \<noteq> 0" by simp |
|
1130 with xz have "?P ?z x (Eq (CN 0 c e))" |
|
1131 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1132 hence "\<forall> x < ?z. ?P ?z x (Eq (CN 0 c e))" by simp |
|
1133 thus ?case by blast |
|
1134 next |
|
1135 case (4 c e) |
|
1136 from prems have nb: "numbound0 e" by simp |
|
1137 from prems have cp: "real c > 0" by simp |
|
1138 fix a |
|
1139 let ?e="Inum (a#bs) e" |
|
1140 let ?z = "(- ?e) / real c" |
|
1141 {fix x |
|
1142 assume xz: "x < ?z" |
|
1143 hence "(real c * x < - ?e)" |
|
1144 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) |
|
1145 hence "real c * x + ?e < 0" by arith |
|
1146 hence "real c * x + ?e \<noteq> 0" by simp |
|
1147 with xz have "?P ?z x (NEq (CN 0 c e))" |
|
1148 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1149 hence "\<forall> x < ?z. ?P ?z x (NEq (CN 0 c e))" by simp |
|
1150 thus ?case by blast |
|
1151 next |
|
1152 case (5 c e) |
|
1153 from prems have nb: "numbound0 e" by simp |
|
1154 from prems have cp: "real c > 0" by simp |
|
1155 fix a |
|
1156 let ?e="Inum (a#bs) e" |
|
1157 let ?z = "(- ?e) / real c" |
|
1158 {fix x |
|
1159 assume xz: "x < ?z" |
|
1160 hence "(real c * x < - ?e)" |
|
1161 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) |
|
1162 hence "real c * x + ?e < 0" by arith |
|
1163 with xz have "?P ?z x (Lt (CN 0 c e))" |
|
1164 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1165 hence "\<forall> x < ?z. ?P ?z x (Lt (CN 0 c e))" by simp |
|
1166 thus ?case by blast |
|
1167 next |
|
1168 case (6 c e) |
|
1169 from prems have nb: "numbound0 e" by simp |
|
1170 from prems have cp: "real c > 0" by simp |
|
1171 fix a |
|
1172 let ?e="Inum (a#bs) e" |
|
1173 let ?z = "(- ?e) / real c" |
|
1174 {fix x |
|
1175 assume xz: "x < ?z" |
|
1176 hence "(real c * x < - ?e)" |
|
1177 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) |
|
1178 hence "real c * x + ?e < 0" by arith |
|
1179 with xz have "?P ?z x (Le (CN 0 c e))" |
|
1180 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1181 hence "\<forall> x < ?z. ?P ?z x (Le (CN 0 c e))" by simp |
|
1182 thus ?case by blast |
|
1183 next |
|
1184 case (7 c e) |
|
1185 from prems have nb: "numbound0 e" by simp |
|
1186 from prems have cp: "real c > 0" by simp |
|
1187 fix a |
|
1188 let ?e="Inum (a#bs) e" |
|
1189 let ?z = "(- ?e) / real c" |
|
1190 {fix x |
|
1191 assume xz: "x < ?z" |
|
1192 hence "(real c * x < - ?e)" |
|
1193 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) |
|
1194 hence "real c * x + ?e < 0" by arith |
|
1195 with xz have "?P ?z x (Gt (CN 0 c e))" |
|
1196 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1197 hence "\<forall> x < ?z. ?P ?z x (Gt (CN 0 c e))" by simp |
|
1198 thus ?case by blast |
|
1199 next |
|
1200 case (8 c e) |
|
1201 from prems have nb: "numbound0 e" by simp |
|
1202 from prems have cp: "real c > 0" by simp |
|
1203 fix a |
|
1204 let ?e="Inum (a#bs) e" |
|
1205 let ?z = "(- ?e) / real c" |
|
1206 {fix x |
|
1207 assume xz: "x < ?z" |
|
1208 hence "(real c * x < - ?e)" |
|
1209 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) |
|
1210 hence "real c * x + ?e < 0" by arith |
|
1211 with xz have "?P ?z x (Ge (CN 0 c e))" |
|
1212 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1213 hence "\<forall> x < ?z. ?P ?z x (Ge (CN 0 c e))" by simp |
|
1214 thus ?case by blast |
|
1215 qed simp_all |
|
1216 |
|
1217 lemma rplusinf_inf: |
|
1218 assumes lp: "isrlfm p" |
|
1219 shows "\<exists> z. \<forall> x > z. Ifm (x#bs) (plusinf p) = Ifm (x#bs) p" (is "\<exists> z. \<forall> x. ?P z x p") |
|
1220 using lp |
|
1221 proof (induct p rule: isrlfm.induct) |
|
1222 case (1 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto |
|
1223 next |
|
1224 case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto |
|
1225 next |
|
1226 case (3 c e) |
|
1227 from prems have nb: "numbound0 e" by simp |
|
1228 from prems have cp: "real c > 0" by simp |
|
1229 fix a |
|
1230 let ?e="Inum (a#bs) e" |
|
1231 let ?z = "(- ?e) / real c" |
|
1232 {fix x |
|
1233 assume xz: "x > ?z" |
|
1234 with mult_strict_right_mono [OF xz cp] cp |
|
1235 have "(real c * x > - ?e)" by (simp add: mult_ac) |
|
1236 hence "real c * x + ?e > 0" by arith |
|
1237 hence "real c * x + ?e \<noteq> 0" by simp |
|
1238 with xz have "?P ?z x (Eq (CN 0 c e))" |
|
1239 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1240 hence "\<forall> x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp |
|
1241 thus ?case by blast |
|
1242 next |
|
1243 case (4 c e) |
|
1244 from prems have nb: "numbound0 e" by simp |
|
1245 from prems have cp: "real c > 0" by simp |
|
1246 fix a |
|
1247 let ?e="Inum (a#bs) e" |
|
1248 let ?z = "(- ?e) / real c" |
|
1249 {fix x |
|
1250 assume xz: "x > ?z" |
|
1251 with mult_strict_right_mono [OF xz cp] cp |
|
1252 have "(real c * x > - ?e)" by (simp add: mult_ac) |
|
1253 hence "real c * x + ?e > 0" by arith |
|
1254 hence "real c * x + ?e \<noteq> 0" by simp |
|
1255 with xz have "?P ?z x (NEq (CN 0 c e))" |
|
1256 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1257 hence "\<forall> x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp |
|
1258 thus ?case by blast |
|
1259 next |
|
1260 case (5 c e) |
|
1261 from prems have nb: "numbound0 e" by simp |
|
1262 from prems have cp: "real c > 0" by simp |
|
1263 fix a |
|
1264 let ?e="Inum (a#bs) e" |
|
1265 let ?z = "(- ?e) / real c" |
|
1266 {fix x |
|
1267 assume xz: "x > ?z" |
|
1268 with mult_strict_right_mono [OF xz cp] cp |
|
1269 have "(real c * x > - ?e)" by (simp add: mult_ac) |
|
1270 hence "real c * x + ?e > 0" by arith |
|
1271 with xz have "?P ?z x (Lt (CN 0 c e))" |
|
1272 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1273 hence "\<forall> x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp |
|
1274 thus ?case by blast |
|
1275 next |
|
1276 case (6 c e) |
|
1277 from prems have nb: "numbound0 e" by simp |
|
1278 from prems have cp: "real c > 0" by simp |
|
1279 fix a |
|
1280 let ?e="Inum (a#bs) e" |
|
1281 let ?z = "(- ?e) / real c" |
|
1282 {fix x |
|
1283 assume xz: "x > ?z" |
|
1284 with mult_strict_right_mono [OF xz cp] cp |
|
1285 have "(real c * x > - ?e)" by (simp add: mult_ac) |
|
1286 hence "real c * x + ?e > 0" by arith |
|
1287 with xz have "?P ?z x (Le (CN 0 c e))" |
|
1288 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1289 hence "\<forall> x > ?z. ?P ?z x (Le (CN 0 c e))" by simp |
|
1290 thus ?case by blast |
|
1291 next |
|
1292 case (7 c e) |
|
1293 from prems have nb: "numbound0 e" by simp |
|
1294 from prems have cp: "real c > 0" by simp |
|
1295 fix a |
|
1296 let ?e="Inum (a#bs) e" |
|
1297 let ?z = "(- ?e) / real c" |
|
1298 {fix x |
|
1299 assume xz: "x > ?z" |
|
1300 with mult_strict_right_mono [OF xz cp] cp |
|
1301 have "(real c * x > - ?e)" by (simp add: mult_ac) |
|
1302 hence "real c * x + ?e > 0" by arith |
|
1303 with xz have "?P ?z x (Gt (CN 0 c e))" |
|
1304 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1305 hence "\<forall> x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp |
|
1306 thus ?case by blast |
|
1307 next |
|
1308 case (8 c e) |
|
1309 from prems have nb: "numbound0 e" by simp |
|
1310 from prems have cp: "real c > 0" by simp |
|
1311 fix a |
|
1312 let ?e="Inum (a#bs) e" |
|
1313 let ?z = "(- ?e) / real c" |
|
1314 {fix x |
|
1315 assume xz: "x > ?z" |
|
1316 with mult_strict_right_mono [OF xz cp] cp |
|
1317 have "(real c * x > - ?e)" by (simp add: mult_ac) |
|
1318 hence "real c * x + ?e > 0" by arith |
|
1319 with xz have "?P ?z x (Ge (CN 0 c e))" |
|
1320 using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } |
|
1321 hence "\<forall> x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp |
|
1322 thus ?case by blast |
|
1323 qed simp_all |
|
1324 |
|
1325 lemma rminusinf_bound0: |
|
1326 assumes lp: "isrlfm p" |
|
1327 shows "bound0 (minusinf p)" |
|
1328 using lp |
|
1329 by (induct p rule: minusinf.induct) simp_all |
|
1330 |
|
1331 lemma rplusinf_bound0: |
|
1332 assumes lp: "isrlfm p" |
|
1333 shows "bound0 (plusinf p)" |
|
1334 using lp |
|
1335 by (induct p rule: plusinf.induct) simp_all |
|
1336 |
|
1337 lemma rminusinf_ex: |
|
1338 assumes lp: "isrlfm p" |
|
1339 and ex: "Ifm (a#bs) (minusinf p)" |
|
1340 shows "\<exists> x. Ifm (x#bs) p" |
|
1341 proof- |
|
1342 from bound0_I [OF rminusinf_bound0[OF lp], where b="a" and bs ="bs"] ex |
|
1343 have th: "\<forall> x. Ifm (x#bs) (minusinf p)" by auto |
|
1344 from rminusinf_inf[OF lp, where bs="bs"] |
|
1345 obtain z where z_def: "\<forall>x<z. Ifm (x # bs) (minusinf p) = Ifm (x # bs) p" by blast |
|
1346 from th have "Ifm ((z - 1)#bs) (minusinf p)" by simp |
|
1347 moreover have "z - 1 < z" by simp |
|
1348 ultimately show ?thesis using z_def by auto |
|
1349 qed |
|
1350 |
|
1351 lemma rplusinf_ex: |
|
1352 assumes lp: "isrlfm p" |
|
1353 and ex: "Ifm (a#bs) (plusinf p)" |
|
1354 shows "\<exists> x. Ifm (x#bs) p" |
|
1355 proof- |
|
1356 from bound0_I [OF rplusinf_bound0[OF lp], where b="a" and bs ="bs"] ex |
|
1357 have th: "\<forall> x. Ifm (x#bs) (plusinf p)" by auto |
|
1358 from rplusinf_inf[OF lp, where bs="bs"] |
|
1359 obtain z where z_def: "\<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p" by blast |
|
1360 from th have "Ifm ((z + 1)#bs) (plusinf p)" by simp |
|
1361 moreover have "z + 1 > z" by simp |
|
1362 ultimately show ?thesis using z_def by auto |
|
1363 qed |
|
1364 |
|
1365 consts |
|
1366 uset:: "fm \<Rightarrow> (num \<times> int) list" |
|
1367 usubst :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm " |
|
1368 recdef uset "measure size" |
|
1369 "uset (And p q) = (uset p @ uset q)" |
|
1370 "uset (Or p q) = (uset p @ uset q)" |
|
1371 "uset (Eq (CN 0 c e)) = [(Neg e,c)]" |
|
1372 "uset (NEq (CN 0 c e)) = [(Neg e,c)]" |
|
1373 "uset (Lt (CN 0 c e)) = [(Neg e,c)]" |
|
1374 "uset (Le (CN 0 c e)) = [(Neg e,c)]" |
|
1375 "uset (Gt (CN 0 c e)) = [(Neg e,c)]" |
|
1376 "uset (Ge (CN 0 c e)) = [(Neg e,c)]" |
|
1377 "uset p = []" |
|
1378 recdef usubst "measure size" |
|
1379 "usubst (And p q) = (\<lambda> (t,n). And (usubst p (t,n)) (usubst q (t,n)))" |
|
1380 "usubst (Or p q) = (\<lambda> (t,n). Or (usubst p (t,n)) (usubst q (t,n)))" |
|
1381 "usubst (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))" |
|
1382 "usubst (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))" |
|
1383 "usubst (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))" |
|
1384 "usubst (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))" |
|
1385 "usubst (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))" |
|
1386 "usubst (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))" |
|
1387 "usubst p = (\<lambda> (t,n). p)" |
|
1388 |
|
1389 lemma usubst_I: assumes lp: "isrlfm p" |
|
1390 and np: "real n > 0" and nbt: "numbound0 t" |
|
1391 shows "(Ifm (x#bs) (usubst p (t,n)) = Ifm (((Inum (x#bs) t)/(real n))#bs) p) \<and> bound0 (usubst p (t,n))" (is "(?I x (usubst p (t,n)) = ?I ?u p) \<and> ?B p" is "(_ = ?I (?t/?n) p) \<and> _" is "(_ = ?I (?N x t /_) p) \<and> _") |
|
1392 using lp |
|
1393 proof(induct p rule: usubst.induct) |
|
1394 case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ |
|
1395 have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)" |
|
1396 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
|
1397 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" |
|
1398 by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" |
|
1399 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
|
1400 also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)" |
|
1401 using np by simp |
|
1402 finally show ?case using nbt nb by (simp add: algebra_simps) |
|
1403 next |
|
1404 case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ |
|
1405 have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)" |
|
1406 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
|
1407 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)" |
|
1408 by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" |
|
1409 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
|
1410 also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)" |
|
1411 using np by simp |
|
1412 finally show ?case using nbt nb by (simp add: algebra_simps) |
|
1413 next |
|
1414 case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ |
|
1415 have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" |
|
1416 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
|
1417 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" |
|
1418 by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" |
|
1419 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
|
1420 also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)" |
|
1421 using np by simp |
|
1422 finally show ?case using nbt nb by (simp add: algebra_simps) |
|
1423 next |
|
1424 case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ |
|
1425 have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)" |
|
1426 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
|
1427 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)" |
|
1428 by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" |
|
1429 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
|
1430 also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)" |
|
1431 using np by simp |
|
1432 finally show ?case using nbt nb by (simp add: algebra_simps) |
|
1433 next |
|
1434 case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ |
|
1435 from np have np: "real n \<noteq> 0" by simp |
|
1436 have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)" |
|
1437 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
|
1438 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)" |
|
1439 by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" |
|
1440 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
|
1441 also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)" |
|
1442 using np by simp |
|
1443 finally show ?case using nbt nb by (simp add: algebra_simps) |
|
1444 next |
|
1445 case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ |
|
1446 from np have np: "real n \<noteq> 0" by simp |
|
1447 have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)" |
|
1448 using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp |
|
1449 also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)" |
|
1450 by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" |
|
1451 and b="0", simplified divide_zero_left]) (simp only: algebra_simps) |
|
1452 also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)" |
|
1453 using np by simp |
|
1454 finally show ?case using nbt nb by (simp add: algebra_simps) |
|
1455 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2) |
|
1456 |
|
1457 lemma uset_l: |
|
1458 assumes lp: "isrlfm p" |
|
1459 shows "\<forall> (t,k) \<in> set (uset p). numbound0 t \<and> k >0" |
|
1460 using lp |
|
1461 by(induct p rule: uset.induct,auto) |
|
1462 |
|
1463 lemma rminusinf_uset: |
|
1464 assumes lp: "isrlfm p" |
|
1465 and nmi: "\<not> (Ifm (a#bs) (minusinf p))" (is "\<not> (Ifm (a#bs) (?M p))") |
|
1466 and ex: "Ifm (x#bs) p" (is "?I x p") |
|
1467 shows "\<exists> (s,m) \<in> set (uset p). x \<ge> Inum (a#bs) s / real m" (is "\<exists> (s,m) \<in> ?U p. x \<ge> ?N a s / real m") |
|
1468 proof- |
|
1469 have "\<exists> (s,m) \<in> set (uset p). real m * x \<ge> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<ge> ?N a s") |
|
1470 using lp nmi ex |
|
1471 by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2) |
|
1472 then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<ge> ?N a s" by blast |
|
1473 from uset_l[OF lp] smU have mp: "real m > 0" by auto |
|
1474 from pos_divide_le_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<ge> ?N a s / real m" |
|
1475 by (auto simp add: mult_commute) |
|
1476 thus ?thesis using smU by auto |
|
1477 qed |
|
1478 |
|
1479 lemma rplusinf_uset: |
|
1480 assumes lp: "isrlfm p" |
|
1481 and nmi: "\<not> (Ifm (a#bs) (plusinf p))" (is "\<not> (Ifm (a#bs) (?M p))") |
|
1482 and ex: "Ifm (x#bs) p" (is "?I x p") |
|
1483 shows "\<exists> (s,m) \<in> set (uset p). x \<le> Inum (a#bs) s / real m" (is "\<exists> (s,m) \<in> ?U p. x \<le> ?N a s / real m") |
|
1484 proof- |
|
1485 have "\<exists> (s,m) \<in> set (uset p). real m * x \<le> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<le> ?N a s") |
|
1486 using lp nmi ex |
|
1487 by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2) |
|
1488 then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<le> ?N a s" by blast |
|
1489 from uset_l[OF lp] smU have mp: "real m > 0" by auto |
|
1490 from pos_le_divide_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<le> ?N a s / real m" |
|
1491 by (auto simp add: mult_commute) |
|
1492 thus ?thesis using smU by auto |
|
1493 qed |
|
1494 |
|
1495 lemma lin_dense: |
|
1496 assumes lp: "isrlfm p" |
|
1497 and noS: "\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> (\<lambda> (t,n). Inum (x#bs) t / real n) ` set (uset p)" |
|
1498 (is "\<forall> t. _ \<and> _ \<longrightarrow> t \<notin> (\<lambda> (t,n). ?N x t / real n ) ` (?U p)") |
|
1499 and lx: "l < x" and xu:"x < u" and px:" Ifm (x#bs) p" |
|
1500 and ly: "l < y" and yu: "y < u" |
|
1501 shows "Ifm (y#bs) p" |
|
1502 using lp px noS |
|
1503 proof (induct p rule: isrlfm.induct) |
|
1504 case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ |
|
1505 from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) |
|
1506 hence pxc: "x < (- ?N x e) / real c" |
|
1507 by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) |
|
1508 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto |
|
1509 with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto |
|
1510 hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto |
|
1511 moreover {assume y: "y < (-?N x e)/ real c" |
|
1512 hence "y * real c < - ?N x e" |
|
1513 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
|
1514 hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) |
|
1515 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} |
|
1516 moreover {assume y: "y > (- ?N x e) / real c" |
|
1517 with yu have eu: "u > (- ?N x e) / real c" by auto |
|
1518 with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) |
|
1519 with lx pxc have "False" by auto |
|
1520 hence ?case by simp } |
|
1521 ultimately show ?case by blast |
|
1522 next |
|
1523 case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + |
|
1524 from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) |
|
1525 hence pxc: "x \<le> (- ?N x e) / real c" |
|
1526 by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) |
|
1527 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto |
|
1528 with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto |
|
1529 hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto |
|
1530 moreover {assume y: "y < (-?N x e)/ real c" |
|
1531 hence "y * real c < - ?N x e" |
|
1532 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
|
1533 hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) |
|
1534 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} |
|
1535 moreover {assume y: "y > (- ?N x e) / real c" |
|
1536 with yu have eu: "u > (- ?N x e) / real c" by auto |
|
1537 with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) |
|
1538 with lx pxc have "False" by auto |
|
1539 hence ?case by simp } |
|
1540 ultimately show ?case by blast |
|
1541 next |
|
1542 case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ |
|
1543 from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) |
|
1544 hence pxc: "x > (- ?N x e) / real c" |
|
1545 by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) |
|
1546 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto |
|
1547 with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto |
|
1548 hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto |
|
1549 moreover {assume y: "y > (-?N x e)/ real c" |
|
1550 hence "y * real c > - ?N x e" |
|
1551 by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
|
1552 hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) |
|
1553 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} |
|
1554 moreover {assume y: "y < (- ?N x e) / real c" |
|
1555 with ly have eu: "l < (- ?N x e) / real c" by auto |
|
1556 with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) |
|
1557 with xu pxc have "False" by auto |
|
1558 hence ?case by simp } |
|
1559 ultimately show ?case by blast |
|
1560 next |
|
1561 case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ |
|
1562 from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) |
|
1563 hence pxc: "x \<ge> (- ?N x e) / real c" |
|
1564 by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) |
|
1565 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto |
|
1566 with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto |
|
1567 hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto |
|
1568 moreover {assume y: "y > (-?N x e)/ real c" |
|
1569 hence "y * real c > - ?N x e" |
|
1570 by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
|
1571 hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) |
|
1572 hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} |
|
1573 moreover {assume y: "y < (- ?N x e) / real c" |
|
1574 with ly have eu: "l < (- ?N x e) / real c" by auto |
|
1575 with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) |
|
1576 with xu pxc have "False" by auto |
|
1577 hence ?case by simp } |
|
1578 ultimately show ?case by blast |
|
1579 next |
|
1580 case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ |
|
1581 from cp have cnz: "real c \<noteq> 0" by simp |
|
1582 from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) |
|
1583 hence pxc: "x = (- ?N x e) / real c" |
|
1584 by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) |
|
1585 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto |
|
1586 with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto |
|
1587 with pxc show ?case by simp |
|
1588 next |
|
1589 case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ |
|
1590 from cp have cnz: "real c \<noteq> 0" by simp |
|
1591 from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto |
|
1592 with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto |
|
1593 hence "y* real c \<noteq> -?N x e" |
|
1594 by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp |
|
1595 hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) |
|
1596 thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] |
|
1597 by (simp add: algebra_simps) |
|
1598 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"]) |
|
1599 |
|
1600 lemma finite_set_intervals: |
|
1601 assumes px: "P (x::real)" |
|
1602 and lx: "l \<le> x" and xu: "x \<le> u" |
|
1603 and linS: "l\<in> S" and uinS: "u \<in> S" |
|
1604 and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u" |
|
1605 shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x" |
|
1606 proof- |
|
1607 let ?Mx = "{y. y\<in> S \<and> y \<le> x}" |
|
1608 let ?xM = "{y. y\<in> S \<and> x \<le> y}" |
|
1609 let ?a = "Max ?Mx" |
|
1610 let ?b = "Min ?xM" |
|
1611 have MxS: "?Mx \<subseteq> S" by blast |
|
1612 hence fMx: "finite ?Mx" using fS finite_subset by auto |
|
1613 from lx linS have linMx: "l \<in> ?Mx" by blast |
|
1614 hence Mxne: "?Mx \<noteq> {}" by blast |
|
1615 have xMS: "?xM \<subseteq> S" by blast |
|
1616 hence fxM: "finite ?xM" using fS finite_subset by auto |
|
1617 from xu uinS have linxM: "u \<in> ?xM" by blast |
|
1618 hence xMne: "?xM \<noteq> {}" by blast |
|
1619 have ax:"?a \<le> x" using Mxne fMx by auto |
|
1620 have xb:"x \<le> ?b" using xMne fxM by auto |
|
1621 have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast |
|
1622 have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast |
|
1623 have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S" |
|
1624 proof(clarsimp) |
|
1625 fix y |
|
1626 assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S" |
|
1627 from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by auto |
|
1628 moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp} |
|
1629 moreover {assume "y \<in> ?xM" hence "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp} |
|
1630 ultimately show "False" by blast |
|
1631 qed |
|
1632 from ainS binS noy ax xb px show ?thesis by blast |
|
1633 qed |
|
1634 |
|
1635 lemma finite_set_intervals2: |
|
1636 assumes px: "P (x::real)" |
|
1637 and lx: "l \<le> x" and xu: "x \<le> u" |
|
1638 and linS: "l\<in> S" and uinS: "u \<in> S" |
|
1639 and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u" |
|
1640 shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)" |
|
1641 proof- |
|
1642 from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] |
|
1643 obtain a and b where |
|
1644 as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto |
|
1645 from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto |
|
1646 thus ?thesis using px as bs noS by blast |
|
1647 qed |
|
1648 |
|
1649 lemma rinf_uset: |
|
1650 assumes lp: "isrlfm p" |
|
1651 and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))") |
|
1652 and npi: "\<not> (Ifm (x#bs) (plusinf p))" (is "\<not> (Ifm (x#bs) (?P p))") |
|
1653 and ex: "\<exists> x. Ifm (x#bs) p" (is "\<exists> x. ?I x p") |
|
1654 shows "\<exists> (l,n) \<in> set (uset p). \<exists> (s,m) \<in> set (uset p). ?I ((Inum (x#bs) l / real n + Inum (x#bs) s / real m) / 2) p" |
|
1655 proof- |
|
1656 let ?N = "\<lambda> x t. Inum (x#bs) t" |
|
1657 let ?U = "set (uset p)" |
|
1658 from ex obtain a where pa: "?I a p" by blast |
|
1659 from bound0_I[OF rminusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] nmi |
|
1660 have nmi': "\<not> (?I a (?M p))" by simp |
|
1661 from bound0_I[OF rplusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] npi |
|
1662 have npi': "\<not> (?I a (?P p))" by simp |
|
1663 have "\<exists> (l,n) \<in> set (uset p). \<exists> (s,m) \<in> set (uset p). ?I ((?N a l/real n + ?N a s /real m) / 2) p" |
|
1664 proof- |
|
1665 let ?M = "(\<lambda> (t,c). ?N a t / real c) ` ?U" |
|
1666 have fM: "finite ?M" by auto |
|
1667 from rminusinf_uset[OF lp nmi pa] rplusinf_uset[OF lp npi pa] |
|
1668 have "\<exists> (l,n) \<in> set (uset p). \<exists> (s,m) \<in> set (uset p). a \<le> ?N x l / real n \<and> a \<ge> ?N x s / real m" by blast |
|
1669 then obtain "t" "n" "s" "m" where |
|
1670 tnU: "(t,n) \<in> ?U" and smU: "(s,m) \<in> ?U" |
|
1671 and xs1: "a \<le> ?N x s / real m" and tx1: "a \<ge> ?N x t / real n" by blast |
|
1672 from uset_l[OF lp] tnU smU numbound0_I[where bs="bs" and b="x" and b'="a"] xs1 tx1 have xs: "a \<le> ?N a s / real m" and tx: "a \<ge> ?N a t / real n" by auto |
|
1673 from tnU have Mne: "?M \<noteq> {}" by auto |
|
1674 hence Une: "?U \<noteq> {}" by simp |
|
1675 let ?l = "Min ?M" |
|
1676 let ?u = "Max ?M" |
|
1677 have linM: "?l \<in> ?M" using fM Mne by simp |
|
1678 have uinM: "?u \<in> ?M" using fM Mne by simp |
|
1679 have tnM: "?N a t / real n \<in> ?M" using tnU by auto |
|
1680 have smM: "?N a s / real m \<in> ?M" using smU by auto |
|
1681 have lM: "\<forall> t\<in> ?M. ?l \<le> t" using Mne fM by auto |
|
1682 have Mu: "\<forall> t\<in> ?M. t \<le> ?u" using Mne fM by auto |
|
1683 have "?l \<le> ?N a t / real n" using tnM Mne by simp hence lx: "?l \<le> a" using tx by simp |
|
1684 have "?N a s / real m \<le> ?u" using smM Mne by simp hence xu: "a \<le> ?u" using xs by simp |
|
1685 from finite_set_intervals2[where P="\<lambda> x. ?I x p",OF pa lx xu linM uinM fM lM Mu] |
|
1686 have "(\<exists> s\<in> ?M. ?I s p) \<or> |
|
1687 (\<exists> t1\<in> ?M. \<exists> t2 \<in> ?M. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p)" . |
|
1688 moreover { fix u assume um: "u\<in> ?M" and pu: "?I u p" |
|
1689 hence "\<exists> (tu,nu) \<in> ?U. u = ?N a tu / real nu" by auto |
|
1690 then obtain "tu" "nu" where tuU: "(tu,nu) \<in> ?U" and tuu:"u= ?N a tu / real nu" by blast |
|
1691 have "(u + u) / 2 = u" by auto with pu tuu |
|
1692 have "?I (((?N a tu / real nu) + (?N a tu / real nu)) / 2) p" by simp |
|
1693 with tuU have ?thesis by blast} |
|
1694 moreover{ |
|
1695 assume "\<exists> t1\<in> ?M. \<exists> t2 \<in> ?M. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p" |
|
1696 then obtain t1 and t2 where t1M: "t1 \<in> ?M" and t2M: "t2\<in> ?M" |
|
1697 and noM: "\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M" and t1x: "t1 < a" and xt2: "a < t2" and px: "?I a p" |
|
1698 by blast |
|
1699 from t1M have "\<exists> (t1u,t1n) \<in> ?U. t1 = ?N a t1u / real t1n" by auto |
|
1700 then obtain "t1u" "t1n" where t1uU: "(t1u,t1n) \<in> ?U" and t1u: "t1 = ?N a t1u / real t1n" by blast |
|
1701 from t2M have "\<exists> (t2u,t2n) \<in> ?U. t2 = ?N a t2u / real t2n" by auto |
|
1702 then obtain "t2u" "t2n" where t2uU: "(t2u,t2n) \<in> ?U" and t2u: "t2 = ?N a t2u / real t2n" by blast |
|
1703 from t1x xt2 have t1t2: "t1 < t2" by simp |
|
1704 let ?u = "(t1 + t2) / 2" |
|
1705 from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto |
|
1706 from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" . |
|
1707 with t1uU t2uU t1u t2u have ?thesis by blast} |
|
1708 ultimately show ?thesis by blast |
|
1709 qed |
|
1710 then obtain "l" "n" "s" "m" where lnU: "(l,n) \<in> ?U" and smU:"(s,m) \<in> ?U" |
|
1711 and pu: "?I ((?N a l / real n + ?N a s / real m) / 2) p" by blast |
|
1712 from lnU smU uset_l[OF lp] have nbl: "numbound0 l" and nbs: "numbound0 s" by auto |
|
1713 from numbound0_I[OF nbl, where bs="bs" and b="a" and b'="x"] |
|
1714 numbound0_I[OF nbs, where bs="bs" and b="a" and b'="x"] pu |
|
1715 have "?I ((?N x l / real n + ?N x s / real m) / 2) p" by simp |
|
1716 with lnU smU |
|
1717 show ?thesis by auto |
|
1718 qed |
|
1719 (* The Ferrante - Rackoff Theorem *) |
|
1720 |
|
1721 theorem fr_eq: |
|
1722 assumes lp: "isrlfm p" |
|
1723 shows "(\<exists> x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \<or> (Ifm (x#bs) (plusinf p)) \<or> (\<exists> (t,n) \<in> set (uset p). \<exists> (s,m) \<in> set (uset p). Ifm ((((Inum (x#bs) t)/ real n + (Inum (x#bs) s) / real m) /2)#bs) p))" |
|
1724 (is "(\<exists> x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D") |
|
1725 proof |
|
1726 assume px: "\<exists> x. ?I x p" |
|
1727 have "?M \<or> ?P \<or> (\<not> ?M \<and> \<not> ?P)" by blast |
|
1728 moreover {assume "?M \<or> ?P" hence "?D" by blast} |
|
1729 moreover {assume nmi: "\<not> ?M" and npi: "\<not> ?P" |
|
1730 from rinf_uset[OF lp nmi npi] have "?F" using px by blast hence "?D" by blast} |
|
1731 ultimately show "?D" by blast |
|
1732 next |
|
1733 assume "?D" |
|
1734 moreover {assume m:"?M" from rminusinf_ex[OF lp m] have "?E" .} |
|
1735 moreover {assume p: "?P" from rplusinf_ex[OF lp p] have "?E" . } |
|
1736 moreover {assume f:"?F" hence "?E" by blast} |
|
1737 ultimately show "?E" by blast |
|
1738 qed |
|
1739 |
|
1740 |
|
1741 lemma fr_equsubst: |
|
1742 assumes lp: "isrlfm p" |
|
1743 shows "(\<exists> x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \<or> (Ifm (x#bs) (plusinf p)) \<or> (\<exists> (t,k) \<in> set (uset p). \<exists> (s,l) \<in> set (uset p). Ifm (x#bs) (usubst p (Add(Mul l t) (Mul k s) , 2*k*l))))" |
|
1744 (is "(\<exists> x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D") |
|
1745 proof |
|
1746 assume px: "\<exists> x. ?I x p" |
|
1747 have "?M \<or> ?P \<or> (\<not> ?M \<and> \<not> ?P)" by blast |
|
1748 moreover {assume "?M \<or> ?P" hence "?D" by blast} |
|
1749 moreover {assume nmi: "\<not> ?M" and npi: "\<not> ?P" |
|
1750 let ?f ="\<lambda> (t,n). Inum (x#bs) t / real n" |
|
1751 let ?N = "\<lambda> t. Inum (x#bs) t" |
|
1752 {fix t n s m assume "(t,n)\<in> set (uset p)" and "(s,m) \<in> set (uset p)" |
|
1753 with uset_l[OF lp] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0" |
|
1754 by auto |
|
1755 let ?st = "Add (Mul m t) (Mul n s)" |
|
1756 from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" |
|
1757 by (simp add: mult_commute) |
|
1758 from tnb snb have st_nb: "numbound0 ?st" by simp |
|
1759 have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" |
|
1760 using mnp mp np by (simp add: algebra_simps add_divide_distrib) |
|
1761 from usubst_I[OF lp mnp st_nb, where x="x" and bs="bs"] |
|
1762 have "?I x (usubst p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])} |
|
1763 with rinf_uset[OF lp nmi npi px] have "?F" by blast hence "?D" by blast} |
|
1764 ultimately show "?D" by blast |
|
1765 next |
|
1766 assume "?D" |
|
1767 moreover {assume m:"?M" from rminusinf_ex[OF lp m] have "?E" .} |
|
1768 moreover {assume p: "?P" from rplusinf_ex[OF lp p] have "?E" . } |
|
1769 moreover {fix t k s l assume "(t,k) \<in> set (uset p)" and "(s,l) \<in> set (uset p)" |
|
1770 and px:"?I x (usubst p (Add (Mul l t) (Mul k s), 2*k*l))" |
|
1771 with uset_l[OF lp] have tnb: "numbound0 t" and np:"real k > 0" and snb: "numbound0 s" and mp:"real l > 0" by auto |
|
1772 let ?st = "Add (Mul l t) (Mul k s)" |
|
1773 from mult_pos_pos[OF np mp] have mnp: "real (2*k*l) > 0" |
|
1774 by (simp add: mult_commute) |
|
1775 from tnb snb have st_nb: "numbound0 ?st" by simp |
|
1776 from usubst_I[OF lp mnp st_nb, where bs="bs"] px have "?E" by auto} |
|
1777 ultimately show "?E" by blast |
|
1778 qed |
|
1779 |
|
1780 |
|
1781 (* Implement the right hand side of Ferrante and Rackoff's Theorem. *) |
|
1782 constdefs ferrack:: "fm \<Rightarrow> fm" |
|
1783 "ferrack p \<equiv> (let p' = rlfm (simpfm p); mp = minusinf p'; pp = plusinf p' |
|
1784 in if (mp = T \<or> pp = T) then T else |
|
1785 (let U = remdps(map simp_num_pair |
|
1786 (map (\<lambda> ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)) |
|
1787 (alluopairs (uset p')))) |
|
1788 in decr (disj mp (disj pp (evaldjf (simpfm o (usubst p')) U)))))" |
|
1789 |
|
1790 lemma uset_cong_aux: |
|
1791 assumes Ul: "\<forall> (t,n) \<in> set U. numbound0 t \<and> n >0" |
|
1792 shows "((\<lambda> (t,n). Inum (x#bs) t /real n) ` (set (map (\<lambda> ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)) (alluopairs U)))) = ((\<lambda> ((t,n),(s,m)). (Inum (x#bs) t /real n + Inum (x#bs) s /real m)/2) ` (set U \<times> set U))" |
|
1793 (is "?lhs = ?rhs") |
|
1794 proof(auto) |
|
1795 fix t n s m |
|
1796 assume "((t,n),(s,m)) \<in> set (alluopairs U)" |
|
1797 hence th: "((t,n),(s,m)) \<in> (set U \<times> set U)" |
|
1798 using alluopairs_set1[where xs="U"] by blast |
|
1799 let ?N = "\<lambda> t. Inum (x#bs) t" |
|
1800 let ?st= "Add (Mul m t) (Mul n s)" |
|
1801 from Ul th have mnz: "m \<noteq> 0" by auto |
|
1802 from Ul th have nnz: "n \<noteq> 0" by auto |
|
1803 have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" |
|
1804 using mnz nnz by (simp add: algebra_simps add_divide_distrib) |
|
1805 |
|
1806 thus "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) / |
|
1807 (2 * real n * real m) |
|
1808 \<in> (\<lambda>((t, n), s, m). |
|
1809 (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` |
|
1810 (set U \<times> set U)"using mnz nnz th |
|
1811 apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def) |
|
1812 by (rule_tac x="(s,m)" in bexI,simp_all) |
|
1813 (rule_tac x="(t,n)" in bexI,simp_all) |
|
1814 next |
|
1815 fix t n s m |
|
1816 assume tnU: "(t,n) \<in> set U" and smU:"(s,m) \<in> set U" |
|
1817 let ?N = "\<lambda> t. Inum (x#bs) t" |
|
1818 let ?st= "Add (Mul m t) (Mul n s)" |
|
1819 from Ul smU have mnz: "m \<noteq> 0" by auto |
|
1820 from Ul tnU have nnz: "n \<noteq> 0" by auto |
|
1821 have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" |
|
1822 using mnz nnz by (simp add: algebra_simps add_divide_distrib) |
|
1823 let ?P = "\<lambda> (t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" |
|
1824 have Pc:"\<forall> a b. ?P a b = ?P b a" |
|
1825 by auto |
|
1826 from Ul alluopairs_set1 have Up:"\<forall> ((t,n),(s,m)) \<in> set (alluopairs U). n \<noteq> 0 \<and> m \<noteq> 0" by blast |
|
1827 from alluopairs_ex[OF Pc, where xs="U"] tnU smU |
|
1828 have th':"\<exists> ((t',n'),(s',m')) \<in> set (alluopairs U). ?P (t',n') (s',m')" |
|
1829 by blast |
|
1830 then obtain t' n' s' m' where ts'_U: "((t',n'),(s',m')) \<in> set (alluopairs U)" |
|
1831 and Pts': "?P (t',n') (s',m')" by blast |
|
1832 from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 0" by auto |
|
1833 let ?st' = "Add (Mul m' t') (Mul n' s')" |
|
1834 have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')" |
|
1835 using mnz' nnz' by (simp add: algebra_simps add_divide_distrib) |
|
1836 from Pts' have |
|
1837 "(Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" by simp |
|
1838 also have "\<dots> = ((\<lambda>(t, n). Inum (x # bs) t / real n) ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st') |
|
1839 finally show "(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2 |
|
1840 \<in> (\<lambda>(t, n). Inum (x # bs) t / real n) ` |
|
1841 (\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ` |
|
1842 set (alluopairs U)" |
|
1843 using ts'_U by blast |
|
1844 qed |
|
1845 |
|
1846 lemma uset_cong: |
|
1847 assumes lp: "isrlfm p" |
|
1848 and UU': "((\<lambda> (t,n). Inum (x#bs) t /real n) ` U') = ((\<lambda> ((t,n),(s,m)). (Inum (x#bs) t /real n + Inum (x#bs) s /real m)/2) ` (U \<times> U))" (is "?f ` U' = ?g ` (U\<times>U)") |
|
1849 and U: "\<forall> (t,n) \<in> U. numbound0 t \<and> n > 0" |
|
1850 and U': "\<forall> (t,n) \<in> U'. numbound0 t \<and> n > 0" |
|
1851 shows "(\<exists> (t,n) \<in> U. \<exists> (s,m) \<in> U. Ifm (x#bs) (usubst p (Add (Mul m t) (Mul n s),2*n*m))) = (\<exists> (t,n) \<in> U'. Ifm (x#bs) (usubst p (t,n)))" |
|
1852 (is "?lhs = ?rhs") |
|
1853 proof |
|
1854 assume ?lhs |
|
1855 then obtain t n s m where tnU: "(t,n) \<in> U" and smU:"(s,m) \<in> U" and |
|
1856 Pst: "Ifm (x#bs) (usubst p (Add (Mul m t) (Mul n s),2*n*m))" by blast |
|
1857 let ?N = "\<lambda> t. Inum (x#bs) t" |
|
1858 from tnU smU U have tnb: "numbound0 t" and np: "n > 0" |
|
1859 and snb: "numbound0 s" and mp:"m > 0" by auto |
|
1860 let ?st= "Add (Mul m t) (Mul n s)" |
|
1861 from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" |
|
1862 by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) |
|
1863 from tnb snb have stnb: "numbound0 ?st" by simp |
|
1864 have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" |
|
1865 using mp np by (simp add: algebra_simps add_divide_distrib) |
|
1866 from tnU smU UU' have "?g ((t,n),(s,m)) \<in> ?f ` U'" by blast |
|
1867 hence "\<exists> (t',n') \<in> U'. ?g ((t,n),(s,m)) = ?f (t',n')" |
|
1868 by auto (rule_tac x="(a,b)" in bexI, auto) |
|
1869 then obtain t' n' where tnU': "(t',n') \<in> U'" and th: "?g ((t,n),(s,m)) = ?f (t',n')" by blast |
|
1870 from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto |
|
1871 from usubst_I[OF lp mnp stnb, where bs="bs" and x="x"] Pst |
|
1872 have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp |
|
1873 from conjunct1[OF usubst_I[OF lp np' tnb', where bs="bs" and x="x"], symmetric] th[simplified split_def fst_conv snd_conv,symmetric] Pst2[simplified st[symmetric]] |
|
1874 have "Ifm (x # bs) (usubst p (t', n')) " by (simp only: st) |
|
1875 then show ?rhs using tnU' by auto |
|
1876 next |
|
1877 assume ?rhs |
|
1878 then obtain t' n' where tnU': "(t',n') \<in> U'" and Pt': "Ifm (x # bs) (usubst p (t', n'))" |
|
1879 by blast |
|
1880 from tnU' UU' have "?f (t',n') \<in> ?g ` (U\<times>U)" by blast |
|
1881 hence "\<exists> ((t,n),(s,m)) \<in> (U\<times>U). ?f (t',n') = ?g ((t,n),(s,m))" |
|
1882 by auto (rule_tac x="(a,b)" in bexI, auto) |
|
1883 then obtain t n s m where tnU: "(t,n) \<in> U" and smU:"(s,m) \<in> U" and |
|
1884 th: "?f (t',n') = ?g((t,n),(s,m)) "by blast |
|
1885 let ?N = "\<lambda> t. Inum (x#bs) t" |
|
1886 from tnU smU U have tnb: "numbound0 t" and np: "n > 0" |
|
1887 and snb: "numbound0 s" and mp:"m > 0" by auto |
|
1888 let ?st= "Add (Mul m t) (Mul n s)" |
|
1889 from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" |
|
1890 by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) |
|
1891 from tnb snb have stnb: "numbound0 ?st" by simp |
|
1892 have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" |
|
1893 using mp np by (simp add: algebra_simps add_divide_distrib) |
|
1894 from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto |
|
1895 from usubst_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt' |
|
1896 have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp |
|
1897 with usubst_I[OF lp mnp stnb, where x="x" and bs="bs"] tnU smU show ?lhs by blast |
|
1898 qed |
|
1899 |
|
1900 lemma ferrack: |
|
1901 assumes qf: "qfree p" |
|
1902 shows "qfree (ferrack p) \<and> ((Ifm bs (ferrack p)) = (\<exists> x. Ifm (x#bs) p))" |
|
1903 (is "_ \<and> (?rhs = ?lhs)") |
|
1904 proof- |
|
1905 let ?I = "\<lambda> x p. Ifm (x#bs) p" |
|
1906 fix x |
|
1907 let ?N = "\<lambda> t. Inum (x#bs) t" |
|
1908 let ?q = "rlfm (simpfm p)" |
|
1909 let ?U = "uset ?q" |
|
1910 let ?Up = "alluopairs ?U" |
|
1911 let ?g = "\<lambda> ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)" |
|
1912 let ?S = "map ?g ?Up" |
|
1913 let ?SS = "map simp_num_pair ?S" |
|
1914 let ?Y = "remdps ?SS" |
|
1915 let ?f= "(\<lambda> (t,n). ?N t / real n)" |
|
1916 let ?h = "\<lambda> ((t,n),(s,m)). (?N t/real n + ?N s/ real m) /2" |
|
1917 let ?F = "\<lambda> p. \<exists> a \<in> set (uset p). \<exists> b \<in> set (uset p). ?I x (usubst p (?g(a,b)))" |
|
1918 let ?ep = "evaldjf (simpfm o (usubst ?q)) ?Y" |
|
1919 from rlfm_I[OF simpfm_qf[OF qf]] have lq: "isrlfm ?q" by blast |
|
1920 from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp |
|
1921 from uset_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" . |
|
1922 from U_l UpU |
|
1923 have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto |
|
1924 hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 " |
|
1925 by (auto simp add: mult_pos_pos) |
|
1926 have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" |
|
1927 proof- |
|
1928 { fix t n assume tnY: "(t,n) \<in> set ?Y" |
|
1929 hence "(t,n) \<in> set ?SS" by simp |
|
1930 hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)" |
|
1931 by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all) |
|
1932 then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast |
|
1933 from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto |
|
1934 from simp_num_pair_l[OF tnb np tns] |
|
1935 have "numbound0 t \<and> n > 0" . } |
|
1936 thus ?thesis by blast |
|
1937 qed |
|
1938 |
|
1939 have YU: "(?f ` set ?Y) = (?h ` (set ?U \<times> set ?U))" |
|
1940 proof- |
|
1941 from simp_num_pair_ci[where bs="x#bs"] have |
|
1942 "\<forall>x. (?f o simp_num_pair) x = ?f x" by auto |
|
1943 hence th: "?f o simp_num_pair = ?f" using ext by blast |
|
1944 have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_compose) |
|
1945 also have "\<dots> = (?f ` set ?S)" by (simp add: th) |
|
1946 also have "\<dots> = ((?f o ?g) ` set ?Up)" |
|
1947 by (simp only: set_map o_def image_compose[symmetric]) |
|
1948 also have "\<dots> = (?h ` (set ?U \<times> set ?U))" |
|
1949 using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_compose[symmetric]] by blast |
|
1950 finally show ?thesis . |
|
1951 qed |
|
1952 have "\<forall> (t,n) \<in> set ?Y. bound0 (simpfm (usubst ?q (t,n)))" |
|
1953 proof- |
|
1954 { fix t n assume tnY: "(t,n) \<in> set ?Y" |
|
1955 with Y_l have tnb: "numbound0 t" and np: "real n > 0" by auto |
|
1956 from usubst_I[OF lq np tnb] |
|
1957 have "bound0 (usubst ?q (t,n))" by simp hence "bound0 (simpfm (usubst ?q (t,n)))" |
|
1958 using simpfm_bound0 by simp} |
|
1959 thus ?thesis by blast |
|
1960 qed |
|
1961 hence ep_nb: "bound0 ?ep" using evaldjf_bound0[where xs="?Y" and f="simpfm o (usubst ?q)"] by auto |
|
1962 let ?mp = "minusinf ?q" |
|
1963 let ?pp = "plusinf ?q" |
|
1964 let ?M = "?I x ?mp" |
|
1965 let ?P = "?I x ?pp" |
|
1966 let ?res = "disj ?mp (disj ?pp ?ep)" |
|
1967 from rminusinf_bound0[OF lq] rplusinf_bound0[OF lq] ep_nb |
|
1968 have nbth: "bound0 ?res" by auto |
|
1969 |
|
1970 from conjunct1[OF rlfm_I[OF simpfm_qf[OF qf]]] simpfm |
|
1971 |
|
1972 have th: "?lhs = (\<exists> x. ?I x ?q)" by auto |
|
1973 from th fr_equsubst[OF lq, where bs="bs" and x="x"] have lhfr: "?lhs = (?M \<or> ?P \<or> ?F ?q)" |
|
1974 by (simp only: split_def fst_conv snd_conv) |
|
1975 also have "\<dots> = (?M \<or> ?P \<or> (\<exists> (t,n) \<in> set ?Y. ?I x (simpfm (usubst ?q (t,n)))))" |
|
1976 using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm) |
|
1977 also have "\<dots> = (Ifm (x#bs) ?res)" |
|
1978 using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="simpfm o (usubst ?q)",symmetric] |
|
1979 by (simp add: split_def pair_collapse) |
|
1980 finally have lheq: "?lhs = (Ifm bs (decr ?res))" using decr[OF nbth] by blast |
|
1981 hence lr: "?lhs = ?rhs" apply (unfold ferrack_def Let_def) |
|
1982 by (cases "?mp = T \<or> ?pp = T", auto) (simp add: disj_def)+ |
|
1983 from decr_qf[OF nbth] have "qfree (ferrack p)" by (auto simp add: Let_def ferrack_def) |
|
1984 with lr show ?thesis by blast |
|
1985 qed |
|
1986 |
|
1987 definition linrqe:: "fm \<Rightarrow> fm" where |
|
1988 "linrqe p = qelim (prep p) ferrack" |
|
1989 |
|
1990 theorem linrqe: "Ifm bs (linrqe p) = Ifm bs p \<and> qfree (linrqe p)" |
|
1991 using ferrack qelim_ci prep |
|
1992 unfolding linrqe_def by auto |
|
1993 |
|
1994 definition ferrack_test :: "unit \<Rightarrow> fm" where |
|
1995 "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) |
|
1996 (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" |
|
1997 |
|
1998 ML {* @{code ferrack_test} () *} |
|
1999 |
|
2000 oracle linr_oracle = {* |
|
2001 let |
|
2002 |
|
2003 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |
|
2004 of NONE => error "Variable not found in the list!" |
|
2005 | SOME n => @{code Bound} n) |
|
2006 | num_of_term vs @{term "real (0::int)"} = @{code C} 0 |
|
2007 | num_of_term vs @{term "real (1::int)"} = @{code C} 1 |
|
2008 | num_of_term vs @{term "0::real"} = @{code C} 0 |
|
2009 | num_of_term vs @{term "1::real"} = @{code C} 1 |
|
2010 | num_of_term vs (Bound i) = @{code Bound} i |
|
2011 | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t') |
|
2012 | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2) |
|
2013 | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Sub} (num_of_term vs t1, num_of_term vs t2) |
|
2014 | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case (num_of_term vs t1) |
|
2015 of @{code C} i => @{code Mul} (i, num_of_term vs t2) |
|
2016 | _ => error "num_of_term: unsupported Multiplication") |
|
2017 | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t') |
|
2018 | num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') = @{code C} (HOLogic.dest_numeral t') |
|
2019 | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t); |
|
2020 |
|
2021 fun fm_of_term vs @{term True} = @{code T} |
|
2022 | fm_of_term vs @{term False} = @{code F} |
|
2023 | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
|
2024 | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
|
2025 | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
|
2026 | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2) |
|
2027 | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2) |
|
2028 | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2) |
|
2029 | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) |
|
2030 | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t') |
|
2031 | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) = |
|
2032 @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
|
2033 | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) = |
|
2034 @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
|
2035 | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); |
|
2036 |
|
2037 fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i |
|
2038 | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs)) |
|
2039 | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \<Rightarrow> real"} $ term_of_num vs t' |
|
2040 | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ |
|
2041 term_of_num vs t1 $ term_of_num vs t2 |
|
2042 | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ |
|
2043 term_of_num vs t1 $ term_of_num vs t2 |
|
2044 | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ |
|
2045 term_of_num vs (@{code C} i) $ term_of_num vs t2 |
|
2046 | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t)); |
|
2047 |
|
2048 fun term_of_fm vs @{code T} = HOLogic.true_const |
|
2049 | term_of_fm vs @{code F} = HOLogic.false_const |
|
2050 | term_of_fm vs (@{code Lt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ |
|
2051 term_of_num vs t $ @{term "0::real"} |
|
2052 | term_of_fm vs (@{code Le} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ |
|
2053 term_of_num vs t $ @{term "0::real"} |
|
2054 | term_of_fm vs (@{code Gt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ |
|
2055 @{term "0::real"} $ term_of_num vs t |
|
2056 | term_of_fm vs (@{code Ge} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ |
|
2057 @{term "0::real"} $ term_of_num vs t |
|
2058 | term_of_fm vs (@{code Eq} t) = @{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ |
|
2059 term_of_num vs t $ @{term "0::real"} |
|
2060 | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t)) |
|
2061 | term_of_fm vs (@{code NOT} t') = HOLogic.Not $ term_of_fm vs t' |
|
2062 | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2 |
|
2063 | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2 |
|
2064 | term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2 |
|
2065 | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ |
|
2066 term_of_fm vs t1 $ term_of_fm vs t2 |
|
2067 | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent."; |
|
2068 |
|
2069 in fn ct => |
|
2070 let |
|
2071 val thy = Thm.theory_of_cterm ct; |
|
2072 val t = Thm.term_of ct; |
|
2073 val fs = OldTerm.term_frees t; |
|
2074 val vs = fs ~~ (0 upto (length fs - 1)); |
|
2075 val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))); |
|
2076 in Thm.cterm_of thy res end |
|
2077 end; |
|
2078 *} |
|
2079 |
|
2080 use "ferrack_tac.ML" |
|
2081 setup Ferrack_Tac.setup |
|
2082 |
|
2083 lemma |
|
2084 fixes x :: real |
|
2085 shows "2 * x \<le> 2 * x \<and> 2 * x \<le> 2 * x + 1" |
|
2086 apply rferrack |
|
2087 done |
|
2088 |
|
2089 lemma |
|
2090 fixes x :: real |
|
2091 shows "\<exists>y \<le> x. x = y + 1" |
|
2092 apply rferrack |
|
2093 done |
|
2094 |
|
2095 lemma |
|
2096 fixes x :: real |
|
2097 shows "\<not> (\<exists>z. x + z = x + z + 1)" |
|
2098 apply rferrack |
|
2099 done |
|
2100 |
|
2101 end |