src/HOL/Decision_Procs/MIR.thy
 changeset 41849 1a65b780bd56 parent 41839 421a795cee05 child 41882 ae8d62656392
equal inserted replaced
41843:15d76ed6ea67 41849:1a65b780bd56
1 (*  Title:      HOL/Decision_Procs/MIR.thy
1 (*  Title:      HOL/Decision_Procs/MIR.thy
2     Author:     Amine Chaieb
2     Author:     Amine Chaieb
3 *)
3 *)
4
4
5 theory MIR
5 theory MIR
6 imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
6 imports Complex_Main Dense_Linear_Order DP_Library

7   "~~/src/HOL/Library/Efficient_Nat"
7 uses ("mir_tac.ML")
8 uses ("mir_tac.ML")
8 begin
9 begin
9
10
10 section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}
11 section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}
11
12
12 declare real_of_int_floor_cancel [simp del]
13 declare real_of_int_floor_cancel [simp del]
13
14
14 primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
15 lemma myle: fixes a b :: "'a::{ordered_ab_group_add}"
15   "alluopairs [] = []"
16   shows "(a \<le> b) = (0 \<le> b - a)"
16 | "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
17
18
18 lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
19 lemma myless: fixes a b :: "'a::{ordered_ab_group_add}"
19 by (induct xs, auto)
20   shows "(a < b) = (0 < b - a)"
20
21 by (metis le_iff_diff_le_0 less_le_not_le myle)
21 lemma alluopairs_set:

22   "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "

23 by (induct xs, auto)

24

25 lemma alluopairs_ex:

26   assumes Pc: "\<forall> x y. P x y = P y x"

27   shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"

28 proof

29   assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"

30   then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"  by blast

31   from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y"

32     by auto

33 next

34   assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"

35   then obtain "x" and "y"  where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+

36   from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast

37   with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast

38 qed

39

40 lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"

41 using Nat.gr0_conv_Suc

42 by clarsimp

43

44

45 lemma myl: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a \<le> b) = (0 \<le> b - a)"

46 proof(clarify)

47   fix x y ::"'a"

48   have "(x \<le> y) = (x - y \<le> 0)" by (simp only: le_iff_diff_le_0[where a="x" and b="y"])

49   also have "\<dots> = (- (y - x) \<le> 0)" by simp

50   also have "\<dots> = (0 \<le> y - x)" by (simp only: neg_le_0_iff_le[where a="y-x"])

51   finally show "(x \<le> y) = (0 \<le> y - x)" .

52 qed

53

54 lemma myless: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a < b) = (0 < b - a)"

55 proof(clarify)

56   fix x y ::"'a"

57   have "(x < y) = (x - y < 0)" by (simp only: less_iff_diff_less_0[where a="x" and b="y"])

58   also have "\<dots> = (- (y - x) < 0)" by simp

59   also have "\<dots> = (0 < y - x)" by (simp only: neg_less_0_iff_less[where a="y-x"])

60   finally show "(x < y) = (0 < y - x)" .

61 qed

62

63 lemma myeq: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a = b) = (0 = b - a)"

64   by auto

65
22
66   (* Maybe should be added to the library \<dots> *)
23   (* Maybe should be added to the library \<dots> *)
67 lemma floor_int_eq: "(real n\<le> x \<and> x < real (n+1)) = (floor x = n)"
24 lemma floor_int_eq: "(real n\<le> x \<and> x < real (n+1)) = (floor x = n)"
68 proof( auto)
25 proof( auto)
69   assume lb: "real n \<le> x"
26   assume lb: "real n \<le> x"
141
98
142 lemma rdvd_mult:
99 lemma rdvd_mult:
143   assumes knz: "k\<noteq>0"
100   assumes knz: "k\<noteq>0"
144   shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)"
101   shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)"
145 using knz by (simp add:rdvd_def)
102 using knz by (simp add:rdvd_def)
155
103
156   (*********************************************************************************)
104   (*********************************************************************************)
157   (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
105   (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
158   (*********************************************************************************)
106   (*********************************************************************************)
159
107
333   | "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)"
281   | "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)"
334
282
335 lemma numbound0_I:
283 lemma numbound0_I:
336   assumes nb: "numbound0 a"
284   assumes nb: "numbound0 a"
337   shows "Inum (b#bs) a = Inum (b'#bs) a"
285   shows "Inum (b#bs) a = Inum (b'#bs) a"
338   using nb by (induct a) (auto simp add: nth_pos2)
286   using nb by (induct a) auto
339
287
340 lemma numbound0_gen:
288 lemma numbound0_gen:
341   assumes nb: "numbound0 t" and ti: "isint t (x#bs)"
289   assumes nb: "numbound0 t" and ti: "isint t (x#bs)"
342   shows "\<forall> y. isint t (y#bs)"
290   shows "\<forall> y. isint t (y#bs)"
343 using nb ti
291 using nb ti
369
317
370 lemma bound0_I:
318 lemma bound0_I:
371   assumes bp: "bound0 p"
319   assumes bp: "bound0 p"
372   shows "Ifm (b#bs) p = Ifm (b'#bs) p"
320   shows "Ifm (b#bs) p = Ifm (b'#bs) p"
373  using bp numbound0_I [where b="b" and bs="bs" and b'="b'"]
321  using bp numbound0_I [where b="b" and bs="bs" and b'="b'"]
374   by (induct p) (auto simp add: nth_pos2)
322   by (induct p) auto
375
323
376 primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where
324 primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where
377   "numsubst0 t (C c) = (C c)"
325   "numsubst0 t (C c) = (C c)"
378   | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
326   | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
379   | "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))"
327   | "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))"
384   | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
332   | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
385   | "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
333   | "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
386
334
387 lemma numsubst0_I:
335 lemma numsubst0_I:
388   shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
336   shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
389   by (induct t) (simp_all add: nth_pos2)
337   by (induct t) simp_all
390

391 lemma numsubst0_I':

392   assumes nb: "numbound0 a"

393   shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"

394   by (induct t) (simp_all add: nth_pos2 numbound0_I[OF nb, where b="b" and b'="b'"])

395
338
396 primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
339 primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
397   "subst0 t T = T"
340   "subst0 t T = T"
398   | "subst0 t F = F"
341   | "subst0 t F = F"
399   | "subst0 t (Lt a) = Lt (numsubst0 t a)"
342   | "subst0 t (Lt a) = Lt (numsubst0 t a)"
411   | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
354   | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
412
355
413 lemma subst0_I: assumes qfp: "qfree p"
356 lemma subst0_I: assumes qfp: "qfree p"
414   shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"
357   shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"
415   using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
358   using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
416   by (induct p) (simp_all add: nth_pos2 )
359   by (induct p) simp_all
417
360
418 fun decrnum:: "num \<Rightarrow> num" where
361 fun decrnum:: "num \<Rightarrow> num" where
419   "decrnum (Bound n) = Bound (n - 1)"
362   "decrnum (Bound n) = Bound (n - 1)"
420 | "decrnum (Neg a) = Neg (decrnum a)"
363 | "decrnum (Neg a) = Neg (decrnum a)"
421 | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
364 | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
442 | "decr (Iff p q) = Iff (decr p) (decr q)"
385 | "decr (Iff p q) = Iff (decr p) (decr q)"
443 | "decr p = p"
386 | "decr p = p"
444
387
445 lemma decrnum: assumes nb: "numbound0 t"
388 lemma decrnum: assumes nb: "numbound0 t"
446   shows "Inum (x#bs) t = Inum bs (decrnum t)"
389   shows "Inum (x#bs) t = Inum bs (decrnum t)"
447   using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)
390   using nb by (induct t rule: decrnum.induct, simp_all)
448
391
449 lemma decr: assumes nb: "bound0 p"
392 lemma decr: assumes nb: "bound0 p"
450   shows "Ifm (x#bs) p = Ifm bs (decr p)"
393   shows "Ifm (x#bs) p = Ifm bs (decr p)"
451   using nb
394   using nb
452   by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)
395   by (induct p rule: decr.induct, simp_all add: decrnum)
453
396
454 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
397 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
455 by (induct p, simp_all)
398 by (induct p, simp_all)
456
399
457 fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
400 fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
511 fun conjuncts :: "fm \<Rightarrow> fm list" where
454 fun conjuncts :: "fm \<Rightarrow> fm list" where
512   "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
455   "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
513 | "conjuncts T = []"
456 | "conjuncts T = []"
514 | "conjuncts p = [p]"
457 | "conjuncts p = [p]"
515
458
518 lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm bs q) = Ifm bs p"
459 lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm bs q) = Ifm bs p"
519 by(induct p rule: conjuncts.induct, auto)
460 by(induct p rule: conjuncts.induct, auto)
533
461
534 lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
462 lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
535 proof-
463 proof-
536   assume qf: "qfree p"
464   assume qf: "qfree p"
537   hence "list_all qfree (disjuncts p)"
465   hence "list_all qfree (disjuncts p)"
649   shows "dvdnumcoeff t g"
577   shows "dvdnumcoeff t g"
650   using dgt' gdg
578   using dgt' gdg
651   by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
579   by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
652
580
657
582
658 lemma numgcd0:
583 lemma numgcd0:
659   assumes g0: "numgcd t = 0"
584   assumes g0: "numgcd t = 0"
660   shows "Inum bs t = 0"
585   shows "Inum bs t = 0"
661 proof-
586 proof-
1136     else Imp p q)"
1061     else Imp p q)"
1137 lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
1062 lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
1138   by (cases "p=F \<or> q=T",simp_all add: imp_def)
1063   by (cases "p=F \<or> q=T",simp_all add: imp_def)
1139 lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
1064 lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
1140   using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
1065   using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
1143
1066
1144 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
1067 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
1145   "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else
1068   "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else
1146        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
1069        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
1147   Iff p q)"
1070   Iff p q)"
1148 lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
1071 lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
1149   by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not)
1072   by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not)
1150 (cases "not p= q", auto simp add:not)
1073 (cases "not p= q", auto simp add:not)
1151 lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
1074 lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
1152   by (unfold iff_def,cases "p=q", auto)
1075   by (unfold iff_def,cases "p=q", auto)
1155
1076
1156 fun check_int:: "num \<Rightarrow> bool" where
1077 fun check_int:: "num \<Rightarrow> bool" where
1157   "check_int (C i) = True"
1078   "check_int (C i) = True"
1158 | "check_int (Floor t) = True"
1079 | "check_int (Floor t) = True"
1159 | "check_int (Mul i t) = check_int t"
1080 | "check_int (Mul i t) = check_int t"
1655
1576
1656 lemma conj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (conj p q) bs"
1577 lemma conj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (conj p q) bs"
1657   using conj_def by (cases p,auto)
1578   using conj_def by (cases p,auto)
1658 lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"
1579 lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"
1659   using disj_def by (cases p,auto)
1580   using disj_def by (cases p,auto)
1662
1581
1663 recdef zlfm "measure fmsize"
1582 recdef zlfm "measure fmsize"
1664   "zlfm (And p q) = conj (zlfm p) (zlfm q)"
1583   "zlfm (And p q) = conj (zlfm p) (zlfm q)"
1665   "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
1584   "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
1666   "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
1585   "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
1737
1656
1738 lemma split_int_gt_real':
1657 lemma split_int_gt_real':
1739   "(real (a::int) + b > 0) = (real a + real (floor b) > 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"
1658   "(real (a::int) + b > 0) = (real a + real (floor b) > 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"
1740 proof-
1659 proof-
1741   have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
1660   have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
1742   show ?thesis using myless[rule_format, where b="real (floor b)"]
1661   show ?thesis using myless[of _ "real (floor b)"]
1743     by (simp only:th split_int_less_real'[where a="-a" and b="-b"])
1662     by (simp only:th split_int_less_real'[where a="-a" and b="-b"])
1745 qed
1664 qed
1746
1665
1747 lemma split_int_le_real:
1666 lemma split_int_le_real:
2289       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps)
2208       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps)
2290       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"
2209       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"
2291         by blast
2210         by blast
2292       thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
2211       thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
2293     qed
2212     qed
2294 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="real(x - k*d)" and b'="real x"] simp del: real_of_int_mult real_of_int_diff)
2213 qed (auto simp add: numbound0_I[where bs="bs" and b="real(x - k*d)" and b'="real x"] simp del: real_of_int_mult real_of_int_diff)
2295
2214
2296 lemma minusinf_ex:
2215 lemma minusinf_ex:
2297   assumes lin: "iszlfm p (real (a::int) #bs)"
2216   assumes lin: "iszlfm p (real (a::int) #bs)"
2298   and exmi: "\<exists> (x::int). Ifm (real x#bs) (minusinf p)" (is "\<exists> x. ?P1 x")
2217   and exmi: "\<exists> (x::int). Ifm (real x#bs) (minusinf p)" (is "\<exists> x. ?P1 x")
2299   shows "\<exists> (x::int). Ifm (real x#bs) p" (is "\<exists> x. ?P x")
2218   shows "\<exists> (x::int). Ifm (real x#bs) p" (is "\<exists> x. ?P x")
2426        (real j rdvd - (real c * real x - Inum (real x # bs) e))"
2345        (real j rdvd - (real c * real x - Inum (real x # bs) e))"
2427     by (simp only: rdvd_minus[symmetric])
2346     by (simp only: rdvd_minus[symmetric])
2428   from prems th show  ?case
2347   from prems th show  ?case
2430       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
2349       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
2431 qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"] nth_pos2)
2350 qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"])
2432
2351
2433 lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
2352 lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
2434 by (induct p rule: mirror.induct, auto simp add: isint_neg)
2353 by (induct p rule: mirror.induct, auto simp add: isint_neg)
2435
2354
2436 lemma mirror_d\<beta>: "iszlfm p (a#bs) \<and> d\<beta> p 1
2355 lemma mirror_d\<beta>: "iszlfm p (a#bs) \<and> d\<beta> p 1
2634     also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps)
2553     also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps)
2635     also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
2554     also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
2636     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
2555     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
2637   also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
2556   also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
2638   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def  be  isint_Mul[OF ei]  mult_strict_mono[OF ldcp jp ldcp ] by simp
2557   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def  be  isint_Mul[OF ei]  mult_strict_mono[OF ldcp jp ldcp ] by simp
2639 qed (simp_all add: nth_pos2 numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)
2558 qed (simp_all add: numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)
2640
2559
2641 lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0"
2560 lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0"
2642   shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
2561   shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
2643   (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
2562   (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
2644 proof-
2563 proof-
2778       using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified]
2697       using int_rdvd_real[where i="j" and x="real (x-d + floor ?e)",symmetric, simplified]
2779       ie by simp
2698       ie by simp
2780     also have "\<dots> = (\<not> real j rdvd real x - real d + ?e)"
2699     also have "\<dots> = (\<not> real j rdvd real x - real d + ?e)"
2781       using ie by simp
2700       using ie by simp
2782     finally show ?case using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp
2701     finally show ?case using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp
2783 qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] nth_pos2 simp del: real_of_int_diff)
2702 qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] simp del: real_of_int_diff)
2784
2703
2785 lemma \<beta>':
2704 lemma \<beta>':
2786   assumes lp: "iszlfm p (a #bs)"
2705   assumes lp: "iszlfm p (a #bs)"
2787   and u: "d\<beta> p 1"
2706   and u: "d\<beta> p 1"
2788   and d: "d\<delta> p d"
2707   and d: "d\<delta> p d"
2897   "\<alpha>\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
2816   "\<alpha>\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
2898   "\<alpha>\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
2817   "\<alpha>\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
2899   "\<alpha>\<rho> p = []"
2818   "\<alpha>\<rho> p = []"
2900
2819
2901     (* Simulates normal substituion by modifying the formula see correctness theorem *)
2820     (* Simulates normal substituion by modifying the formula see correctness theorem *)
2923
2821
2924 definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
2822 definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
2925   "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))"
2823   "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))"
2926
2824
2927 lemma \<sigma>\<rho>:
2825 lemma \<sigma>\<rho>:
3106       also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
3004       also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
3107           numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
3005           numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
3109       finally have ?case . }
3007       finally have ?case . }
3110     ultimately show ?case by blast
3008     ultimately show ?case by blast
3111 qed (simp_all add: nth_pos2 bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"])
3009 qed (simp_all add: bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"])
3112
3010
3113

3114 lemma a\<rho>:

3115   assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "real k > 0"

3116   shows "Ifm (real (x*k)#bs) (a\<rho> p k) = Ifm (real x#bs) p" (is "?I (x*k) (?f p k) = ?I x p")

3117 using lp bound0_I[where bs="bs" and b="real (x*k)" and b'="real x"] numbound0_I[where bs="bs" and b="real (x*k)" and b'="real x"]

3118 proof(induct p rule: a\<rho>.induct)

3119   case (3 c e)

3120   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3121   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3122     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3123     moreover

3124     {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}

3125     ultimately show ?case by blast

3126 next

3127   case (4 c e)

3128   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3129   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3130     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3131     moreover

3132     {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}

3133     ultimately show ?case by blast

3134 next

3135   case (5 c e)

3136   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3137   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3138     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3139     moreover

3140     {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}

3141     ultimately show ?case by blast

3142 next

3143   case (6 c e)

3144   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3145   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3146     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3147     moreover

3148     {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}

3149     ultimately show ?case by blast

3150 next

3151   case (7 c e)

3152   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3153   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3154     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3155     moreover

3156     {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}

3157     ultimately show ?case by blast

3158 next

3159   case (8 c e)

3160   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3161   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3162     {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3163     moreover

3164     {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: algebra_simps)}

3165     ultimately show ?case by blast

3166 next

3167   case (9 i c e)

3168   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3169   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3170   {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3171   moreover

3172   {assume "\<not> k dvd c"

3173     hence "Ifm (real (x*k)#bs) (a\<rho> (Dvd i (CN 0 c e)) k) =

3174       (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k)"

3175       using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"]

3177     also have "\<dots> = (Ifm (real x#bs) (Dvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])

3178     finally have ?case . }

3179   ultimately show ?case by blast

3180 next

3181   case (10 i c e)

3182   from prems have cp: "c > 0" and nb: "numbound0 e" by auto

3183   from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp

3184   {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp }

3185   moreover

3186   {assume "\<not> k dvd c"

3187     hence "Ifm (real (x*k)#bs) (a\<rho> (NDvd i (CN 0 c e)) k) =

3188       (\<not> (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k))"

3189       using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"]

3191     also have "\<dots> = (Ifm (real x#bs) (NDvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])

3192     finally have ?case . }

3193   ultimately show ?case by blast

3195

3196 lemma a\<rho>_ex:

3197   assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "k > 0"

3198   shows "(\<exists> (x::int). real k rdvd real x \<and> Ifm (real x#bs) (a\<rho> p k)) =

3199   (\<exists> (x::int). Ifm (real x#bs) p)" (is "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. ?P x)")

3200 proof-

3201   have "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. k dvd x \<and> ?P' x)" using int_rdvd_iff by simp

3202   also have "\<dots> = (\<exists>x. ?P' (x*k))" using unity_coeff_ex[where P="?P'" and l="k", simplified]

3204   also have "\<dots> = (\<exists> x. ?P x)" using a\<rho> iszlfm_gen[OF lp] kp by auto

3205   finally show ?thesis .

3206 qed

3207

3208 lemma \<sigma>\<rho>': assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "k > 0" and nb: "numbound0 t"

3209   shows "Ifm (real x#bs) (\<sigma>\<rho> p (t,k)) = Ifm ((Inum (real x#bs) t)#bs) (a\<rho> p k)"

3210 using lp

3211 by(induct p rule: \<sigma>\<rho>.induct, simp_all add:

3212   numbound0_I[OF nb, where bs="bs" and b="Inum (real x#bs) t" and b'="real x"]

3213   numbound0_I[where bs="bs" and b="Inum (real x#bs) t" and b'="real x"]

3214   bound0_I[where bs="bs" and b="Inum (real x#bs) t" and b'="real x"] nth_pos2 cong: imp_cong)

3215
3011
3216 lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
3012 lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
3217   shows "bound0 (\<sigma>\<rho> p (t,k))"
3013   shows "bound0 (\<sigma>\<rho> p (t,k))"
3218   using lp
3014   using lp
3219   by (induct p rule: iszlfm.induct, auto simp add: nb)
3015   by (induct p rule: iszlfm.induct, auto simp add: nb)
3226 lemma \<alpha>\<rho>_l:
3022 lemma \<alpha>\<rho>_l:
3227   assumes lp: "iszlfm p (real (i::int)#bs)"
3023   assumes lp: "iszlfm p (real (i::int)#bs)"
3228   shows "\<forall> (b,k) \<in> set (\<alpha>\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
3024   shows "\<forall> (b,k) \<in> set (\<alpha>\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
3229 using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"]
3025 using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"]
3230  by (induct p rule: \<alpha>\<rho>.induct, auto)
3026  by (induct p rule: \<alpha>\<rho>.induct, auto)
3245
3027
3246 lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)"
3028 lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)"
3247   and pi: "Ifm (real i#bs) p"
3029   and pi: "Ifm (real i#bs) p"
3248   and d: "d\<delta> p d"
3030   and d: "d\<delta> p d"
3249   and dp: "d > 0"
3031   and dp: "d > 0"
3372     also have "\<dots> = Not (real j rdvd real (c*(i - d)) + ?e)"
3154     also have "\<dots> = Not (real j rdvd real (c*(i - d)) + ?e)"
3373       using ie by (simp add:algebra_simps)
3155       using ie by (simp add:algebra_simps)
3374     finally show ?case
3156     finally show ?case
3375       using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p
3157       using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p
3377 qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] nth_pos2)
3159 qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"])
3378
3160
3379 lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
3161 lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
3380   shows "bound0 (\<sigma> p k t)"
3162   shows "bound0 (\<sigma> p k t)"
3381   using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
3163   using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
3382
3164
3509 | "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)"
3291 | "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)"
3510 | "rsplit0 t = [(T,0,t)]"
3292 | "rsplit0 t = [(T,0,t)]"
3511 by pat_completeness auto
3293 by pat_completeness auto
3512 termination by (relation "measure num_size") auto
3294 termination by (relation "measure num_size") auto
3513
3295
3516 lemma conj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
3296 lemma conj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
3517   using conj_def by (cases p, auto)
3297   using conj_def by (cases p, auto)
3518 lemma disj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
3298 lemma disj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
3519   using disj_def by (cases p, auto)
3299   using disj_def by (cases p, auto)
3520
3300
3758     ultimately have "?N (Floor s) \<le> real n *x + ?N s\<and> real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp
3538     ultimately have "?N (Floor s) \<le> real n *x + ?N s\<and> real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp
3759     hence th: "0 \<le> real n *x + ?N s - ?N (Floor s) \<and> real n *x + ?N s - ?N (Floor s) < real (n+1)" by simp
3539     hence th: "0 \<le> real n *x + ?N s - ?N (Floor s) \<and> real n *x + ?N s - ?N (Floor s) < real (n+1)" by simp
3760     from real_in_int_intervals th have  "\<exists> j\<in> {0 .. n}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp
3540     from real_in_int_intervals th have  "\<exists> j\<in> {0 .. n}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp
3761
3541
3762     hence "\<exists> j\<in> {0 .. n}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
3542     hence "\<exists> j\<in> {0 .. n}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
3763       by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
3543       by(simp only: myle[of _ "real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
3764     hence "\<exists> j\<in> {0.. n}. ?I (?p (p,n,s) j)"
3544     hence "\<exists> j\<in> {0.. n}. ?I (?p (p,n,s) j)"
3766     then obtain "j" where j_def: "j\<in> {0 .. n} \<and> ?I (?p (p,n,s) j)" by blast
3546     then obtain "j" where j_def: "j\<in> {0 .. n} \<and> ?I (?p (p,n,s) j)" by blast
3767     hence "\<exists>x \<in> {?p (p,n,s) j |j. 0\<le> j \<and> j \<le> n }. ?I x" by auto
3547     hence "\<exists>x \<in> {?p (p,n,s) j |j. 0\<le> j \<and> j \<le> n }. ?I x" by auto
3768     hence ?case using pns
3548     hence ?case using pns
3785     have th1: "\<forall> (a::real). (- a > 0) = (a < 0)" by auto
3565     have th1: "\<forall> (a::real). (- a > 0) = (a < 0)" by auto
3786     have th2: "\<forall> (a::real). (0 \<ge> - a) = (a \<ge> 0)" by auto
3566     have th2: "\<forall> (a::real). (0 \<ge> - a) = (a \<ge> 0)" by auto
3787     from real_in_int_intervals th  have  "\<exists> j\<in> {n .. 0}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp
3567     from real_in_int_intervals th  have  "\<exists> j\<in> {n .. 0}. real j \<le> real n *x + ?N s - ?N (Floor s)\<and> real n *x + ?N s - ?N (Floor s) < real (j+1)" by simp
3788
3568
3789     hence "\<exists> j\<in> {n .. 0}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
3569     hence "\<exists> j\<in> {n .. 0}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
3790       by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
3570       by(simp only: myle[of _ "real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
3791     hence "\<exists> j\<in> {n .. 0}. 0 \<ge> - (real n *x + ?N s - ?N (Floor s) - real j) \<and> - (real n *x + ?N s - ?N (Floor s) - real (j+1)) > 0" by (simp only: th1[rule_format] th2[rule_format])
3571     hence "\<exists> j\<in> {n .. 0}. 0 \<ge> - (real n *x + ?N s - ?N (Floor s) - real j) \<and> - (real n *x + ?N s - ?N (Floor s) - real (j+1)) > 0" by (simp only: th1[rule_format] th2[rule_format])
3792     hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
3572     hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
3794         del: diff_less_0_iff_less diff_le_0_iff_le)
3574         del: diff_less_0_iff_less diff_le_0_iff_le)
3795     then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
3575     then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
3883   (is "\<forall> a n s . ?N a = ?N (CN 0 n s) \<and> _\<longrightarrow> ?I (lt n s) = ?I (Lt a)")
3663   (is "\<forall> a n s . ?N a = ?N (CN 0 n s) \<and> _\<longrightarrow> ?I (lt n s) = ?I (Lt a)")
3884 proof(clarify)
3664 proof(clarify)
3885   fix a n s
3665   fix a n s
3886   assume H: "?N a = ?N (CN 0 n s)"
3666   assume H: "?N a = ?N (CN 0 n s)"
3887   show "?I (lt n s) = ?I (Lt a)" using H by (cases "n=0", (simp add: lt_def))
3667   show "?I (lt n s) = ?I (Lt a)" using H by (cases "n=0", (simp add: lt_def))
3888   (cases "n > 0", simp_all add: lt_def algebra_simps myless[rule_format, where b="0"])
3668   (cases "n > 0", simp_all add: lt_def algebra_simps myless[of _ "0"])
3889 qed
3669 qed
3890
3670
3891 lemma lt_l: "isrlfm (rsplit lt a)"
3671 lemma lt_l: "isrlfm (rsplit lt a)"
3892   by (rule rsplit_l[where f="lt" and a="a"], auto simp add: lt_def,
3672   by (rule rsplit_l[where f="lt" and a="a"], auto simp add: lt_def,
3893     case_tac s, simp_all, case_tac "nat", simp_all)
3673     case_tac s, simp_all, case_tac "nat", simp_all)
3895 lemma le_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (le n s) = Ifm (x#bs) (Le a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (le n s) = ?I (Le a)")
3675 lemma le_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (le n s) = Ifm (x#bs) (Le a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (le n s) = ?I (Le a)")
3896 proof(clarify)
3676 proof(clarify)
3897   fix a n s
3677   fix a n s
3898   assume H: "?N a = ?N (CN 0 n s)"
3678   assume H: "?N a = ?N (CN 0 n s)"
3899   show "?I (le n s) = ?I (Le a)" using H by (cases "n=0", (simp add: le_def))
3679   show "?I (le n s) = ?I (Le a)" using H by (cases "n=0", (simp add: le_def))
3900   (cases "n > 0", simp_all add: le_def algebra_simps myl[rule_format, where b="0"])
3680   (cases "n > 0", simp_all add: le_def algebra_simps myle[of _ "0"])
3901 qed
3681 qed
3902
3682
3903 lemma le_l: "isrlfm (rsplit le a)"
3683 lemma le_l: "isrlfm (rsplit le a)"
3904   by (rule rsplit_l[where f="le" and a="a"], auto simp add: le_def)
3684   by (rule rsplit_l[where f="le" and a="a"], auto simp add: le_def)
3905 (case_tac s, simp_all, case_tac "nat",simp_all)
3685 (case_tac s, simp_all, case_tac "nat",simp_all)
3907 lemma gt_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (gt n s) = Ifm (x#bs) (Gt a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (gt n s) = ?I (Gt a)")
3687 lemma gt_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (gt n s) = Ifm (x#bs) (Gt a)" (is "\<forall> a n s. ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (gt n s) = ?I (Gt a)")
3908 proof(clarify)
3688 proof(clarify)
3909   fix a n s
3689   fix a n s
3910   assume H: "?N a = ?N (CN 0 n s)"
3690   assume H: "?N a = ?N (CN 0 n s)"
3911   show "?I (gt n s) = ?I (Gt a)" using H by (cases "n=0", (simp add: gt_def))
3691   show "?I (gt n s) = ?I (Gt a)" using H by (cases "n=0", (simp add: gt_def))
3912   (cases "n > 0", simp_all add: gt_def algebra_simps myless[rule_format, where b="0"])
3692   (cases "n > 0", simp_all add: gt_def algebra_simps myless[of _ "0"])
3913 qed
3693 qed
3914 lemma gt_l: "isrlfm (rsplit gt a)"
3694 lemma gt_l: "isrlfm (rsplit gt a)"
3915   by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def)
3695   by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def)
3916 (case_tac s, simp_all, case_tac "nat", simp_all)
3696 (case_tac s, simp_all, case_tac "nat", simp_all)
3917
3697
3918 lemma ge_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (ge n s) = Ifm (x#bs) (Ge a)" (is "\<forall> a n s . ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (ge n s) = ?I (Ge a)")
3698 lemma ge_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (ge n s) = Ifm (x#bs) (Ge a)" (is "\<forall> a n s . ?N a = ?N (CN 0 n s) \<and> _ \<longrightarrow> ?I (ge n s) = ?I (Ge a)")
3919 proof(clarify)
3699 proof(clarify)
3920   fix a n s
3700   fix a n s
3921   assume H: "?N a = ?N (CN 0 n s)"
3701   assume H: "?N a = ?N (CN 0 n s)"
3922   show "?I (ge n s) = ?I (Ge a)" using H by (cases "n=0", (simp add: ge_def))
3702   show "?I (ge n s) = ?I (Ge a)" using H by (cases "n=0", (simp add: ge_def))
3923   (cases "n > 0", simp_all add: ge_def algebra_simps myl[rule_format, where b="0"])
3703   (cases "n > 0", simp_all add: ge_def algebra_simps myle[of _ "0"])
3924 qed
3704 qed
3925 lemma ge_l: "isrlfm (rsplit ge a)"
3705 lemma ge_l: "isrlfm (rsplit ge a)"
3926   by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def)
3706   by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def)
3927 (case_tac s, simp_all, case_tac "nat", simp_all)
3707 (case_tac s, simp_all, case_tac "nat", simp_all)
3928
3708
3960 lemma rdvd01_cs:
3740 lemma rdvd01_cs:
3961   assumes up: "u \<ge> 0" and u1: "u<1" and np: "real n > 0"
3741   assumes up: "u \<ge> 0" and u1: "u<1" and np: "real n > 0"
3962   shows "(real (i::int) rdvd real (n::int) * u - s) = (\<exists> j\<in> {0 .. n - 1}. real n * u = s - real (floor s) + real j \<and> real i rdvd real (j - floor s))" (is "?lhs = ?rhs")
3742   shows "(real (i::int) rdvd real (n::int) * u - s) = (\<exists> j\<in> {0 .. n - 1}. real n * u = s - real (floor s) + real j \<and> real i rdvd real (j - floor s))" (is "?lhs = ?rhs")
3963 proof-
3743 proof-
3964   let ?ss = "s - real (floor s)"
3744   let ?ss = "s - real (floor s)"
3965   from real_of_int_floor_add_one_gt[where r="s", simplified myless[rule_format,where a="s"]]
3745   from real_of_int_floor_add_one_gt[where r="s", simplified myless[of "s"]]
3966     real_of_int_floor_le[where r="s"]  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1"
3746     real_of_int_floor_le[where r="s"]  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1"
3967     by (auto simp add: myl[rule_format, where b="s", symmetric] myless[rule_format, where a="?ss"])
3747     by (auto simp add: myle[of _ "s", symmetric] myless[of "?ss"])
3968   from np have n0: "real n \<ge> 0" by simp
3748   from np have n0: "real n \<ge> 0" by simp
3969   from mult_left_mono[OF up n0] mult_strict_left_mono[OF u1 np]
3749   from mult_left_mono[OF up n0] mult_strict_left_mono[OF u1 np]
3970   have nu0:"real n * u - s \<ge> -s" and nun:"real n * u -s < real n - s" by auto
3750   have nu0:"real n * u - s \<ge> -s" and nun:"real n * u -s < real n - s" by auto
3971   from int_rdvd_real[where i="i" and x="real (n::int) * u - s"]
3751   from int_rdvd_real[where i="i" and x="real (n::int) * u - s"]
3972   have "real i rdvd real n * u - s =
3752   have "real i rdvd real n * u - s =
4139   "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
3919   "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
4140   "rlfm p = p" (hints simp add: fmsize_pos)
3920   "rlfm p = p" (hints simp add: fmsize_pos)
4141
3921
4142 lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
3922 lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
4143   by (induct p rule: isrlfm.induct, auto)
3923   by (induct p rule: isrlfm.induct, auto)
4150
3924
4151 lemma simpfm_rl: "isrlfm p \<Longrightarrow> isrlfm (simpfm p)"
3925 lemma simpfm_rl: "isrlfm p \<Longrightarrow> isrlfm (simpfm p)"
4152 proof (induct p)
3926 proof (induct p)
4153   case (Lt a)
3927   case (Lt a)
4154   hence "bound0 (Lt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
3928   hence "bound0 (Lt a) \<or> (\<exists> c e. a = CN 0 c e \<and> c > 0 \<and> numbound0 e)"
4163     {
3937     {
4164       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
3938       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4165       with numgcd_pos[where t="CN 0 c (simpnum e)"]
3939       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4166       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
3940       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4167       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
3941       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4168         by (simp add: numgcd_def zgcd_le1)
4169       from prems have th': "c\<noteq>0" by auto
3943       from prems have th': "c\<noteq>0" by auto
4170       from prems have cp: "c \<ge> 0" by simp
3944       from prems have cp: "c \<ge> 0" by simp
4171       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
3945       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4172         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
3946         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4173     }
3947     }
4188     {
3962     {
4189       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
3963       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4190       with numgcd_pos[where t="CN 0 c (simpnum e)"]
3964       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4191       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
3965       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4192       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
3966       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4193         by (simp add: numgcd_def zgcd_le1)
4194       from prems have th': "c\<noteq>0" by auto
3968       from prems have th': "c\<noteq>0" by auto
4195       from prems have cp: "c \<ge> 0" by simp
3969       from prems have cp: "c \<ge> 0" by simp
4196       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
3970       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4197         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
3971         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4198     }
3972     }
4213     {
3987     {
4214       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
3988       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4215       with numgcd_pos[where t="CN 0 c (simpnum e)"]
3989       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4216       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
3990       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4217       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
3991       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4218         by (simp add: numgcd_def zgcd_le1)
4219       from prems have th': "c\<noteq>0" by auto
3993       from prems have th': "c\<noteq>0" by auto
4220       from prems have cp: "c \<ge> 0" by simp
3994       from prems have cp: "c \<ge> 0" by simp
4221       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
3995       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4222         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
3996         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4223     }
3997     }
4238     {
4012     {
4239       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4013       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4240       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4014       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4241       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4015       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4242       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4016       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4243         by (simp add: numgcd_def zgcd_le1)
4244       from prems have th': "c\<noteq>0" by auto
4018       from prems have th': "c\<noteq>0" by auto
4245       from prems have cp: "c \<ge> 0" by simp
4019       from prems have cp: "c \<ge> 0" by simp
4246       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4020       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4247         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4021         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4248     }
4022     }
4263     {
4037     {
4264       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4038       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4265       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4039       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4266       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4040       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4267       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4041       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4268         by (simp add: numgcd_def zgcd_le1)
4269       from prems have th': "c\<noteq>0" by auto
4043       from prems have th': "c\<noteq>0" by auto
4270       from prems have cp: "c \<ge> 0" by simp
4044       from prems have cp: "c \<ge> 0" by simp
4271       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4045       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4272         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4046         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4273     }
4047     }
4288     {
4062     {
4289       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4063       assume cn1:"numgcd (CN 0 c (simpnum e)) \<noteq> 1" and cnz:"numgcd (CN 0 c (simpnum e)) \<noteq> 0"
4290       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4064       with numgcd_pos[where t="CN 0 c (simpnum e)"]
4291       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4065       have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
4292       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4066       from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
4293         by (simp add: numgcd_def zgcd_le1)
4294       from prems have th': "c\<noteq>0" by auto
4068       from prems have th': "c\<noteq>0" by auto
4295       from prems have cp: "c \<ge> 0" by simp
4069       from prems have cp: "c \<ge> 0" by simp
4296       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4070       from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
4297         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4071         have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
4298     }
4072     }
4672     by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)"
4446     by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)"
4673       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
4447       and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
4674   also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
4448   also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
4675     using np by simp
4449     using np by simp
4676   finally show ?case using nbt nb by (simp add: algebra_simps)
4450   finally show ?case using nbt nb by (simp add: algebra_simps)
4677 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
4451 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"])
4678
4452
4679 lemma \<Upsilon>_l:
4453 lemma \<Upsilon>_l:
4680   assumes lp: "isrlfm p"
4454   assumes lp: "isrlfm p"
4681   shows "\<forall> (t,k) \<in> set (\<Upsilon> p). numbound0 t \<and> k >0"
4455   shows "\<forall> (t,k) \<in> set (\<Upsilon> p). numbound0 t \<and> k >0"
4682 using lp
4456 using lp
4688   and ex: "Ifm (x#bs) p" (is "?I x p")
4462   and ex: "Ifm (x#bs) p" (is "?I x p")
4689   shows "\<exists> (s,m) \<in> set (\<Upsilon> p). x \<ge> Inum (a#bs) s / real m" (is "\<exists> (s,m) \<in> ?U p. x \<ge> ?N a s / real m")
4463   shows "\<exists> (s,m) \<in> set (\<Upsilon> p). x \<ge> Inum (a#bs) s / real m" (is "\<exists> (s,m) \<in> ?U p. x \<ge> ?N a s / real m")
4690 proof-
4464 proof-
4691   have "\<exists> (s,m) \<in> set (\<Upsilon> p). real m * x \<ge> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<ge> ?N a s")
4465   have "\<exists> (s,m) \<in> set (\<Upsilon> p). real m * x \<ge> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<ge> ?N a s")
4692     using lp nmi ex
4466     using lp nmi ex
4693     by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
4467     by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
4694   then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<ge> ?N a s" by blast
4468   then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<ge> ?N a s" by blast
4695   from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
4469   from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
4696   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"
4470   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"
4697     by (auto simp add: mult_commute)
4471     by (auto simp add: mult_commute)
4698   thus ?thesis using smU by auto
4472   thus ?thesis using smU by auto
4704   and ex: "Ifm (x#bs) p" (is "?I x p")
4478   and ex: "Ifm (x#bs) p" (is "?I x p")
4705   shows "\<exists> (s,m) \<in> set (\<Upsilon> p). x \<le> Inum (a#bs) s / real m" (is "\<exists> (s,m) \<in> ?U p. x \<le> ?N a s / real m")
4479   shows "\<exists> (s,m) \<in> set (\<Upsilon> p). x \<le> Inum (a#bs) s / real m" (is "\<exists> (s,m) \<in> ?U p. x \<le> ?N a s / real m")
4706 proof-
4480 proof-
4707   have "\<exists> (s,m) \<in> set (\<Upsilon> p). real m * x \<le> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<le> ?N a s")
4481   have "\<exists> (s,m) \<in> set (\<Upsilon> p). real m * x \<le> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<le> ?N a s")
4708     using lp nmi ex
4482     using lp nmi ex
4709     by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
4483     by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
4710   then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<le> ?N a s" by blast
4484   then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<le> ?N a s" by blast
4711   from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
4485   from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
4712   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"
4486   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"
4713     by (auto simp add: mult_commute)
4487     by (auto simp add: mult_commute)
4714   thus ?thesis using smU by auto
4488   thus ?thesis using smU by auto
4815     hence "y* real c \<noteq> -?N x e"
4589     hence "y* real c \<noteq> -?N x e"
4816       by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
4590       by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
4817     hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
4591     hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
4818     thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
4592     thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
4820 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
4594 qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"])
4821

4822 lemma finite_set_intervals:

4823   assumes px: "P (x::real)"

4824   and lx: "l \<le> x" and xu: "x \<le> u"

4825   and linS: "l\<in> S" and uinS: "u \<in> S"

4826   and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"

4827   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"

4828 proof-

4829   let ?Mx = "{y. y\<in> S \<and> y \<le> x}"

4830   let ?xM = "{y. y\<in> S \<and> x \<le> y}"

4831   let ?a = "Max ?Mx"

4832   let ?b = "Min ?xM"

4833   have MxS: "?Mx \<subseteq> S" by blast

4834   hence fMx: "finite ?Mx" using fS finite_subset by auto

4835   from lx linS have linMx: "l \<in> ?Mx" by blast

4836   hence Mxne: "?Mx \<noteq> {}" by blast

4837   have xMS: "?xM \<subseteq> S" by blast

4838   hence fxM: "finite ?xM" using fS finite_subset by auto

4839   from xu uinS have linxM: "u \<in> ?xM" by blast

4840   hence xMne: "?xM \<noteq> {}" by blast

4841   have ax:"?a \<le> x" using Mxne fMx by auto

4842   have xb:"x \<le> ?b" using xMne fxM by auto

4843   have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast

4844   have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast

4845   have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"

4846   proof(clarsimp)

4847     fix y

4848     assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"

4849     from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by auto

4850     moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp}

4851     moreover {assume "y \<in> ?xM" hence "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp}

4852     ultimately show "False" by blast

4853   qed

4854   from ainS binS noy ax xb px show ?thesis by blast

4855 qed

4856

4857 lemma finite_set_intervals2:

4858   assumes px: "P (x::real)"

4859   and lx: "l \<le> x" and xu: "x \<le> u"

4860   and linS: "l\<in> S" and uinS: "u \<in> S"

4861   and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"

4862   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)"

4863 proof-

4864   from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]

4865   obtain a and b where

4866     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

4867   from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto

4868   thus ?thesis using px as bs noS by blast

4869 qed

4870
4595
4871 lemma rinf_\<Upsilon>:
4596 lemma rinf_\<Upsilon>:
4872   assumes lp: "isrlfm p"
4597   assumes lp: "isrlfm p"
4873   and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))")
4598   and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))")
4874   and npi: "\<not> (Ifm (x#bs) (plusinf p))" (is "\<not> (Ifm (x#bs) (?P p))")
4599   and npi: "\<not> (Ifm (x#bs) (plusinf p))" (is "\<not> (Ifm (x#bs) (?P p))")
5057 lemma splitex:
4782 lemma splitex:
5058   assumes qf: "qfree p"
4783   assumes qf: "qfree p"
5059   shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
4784   shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
5060 proof-
4785 proof-
5061   have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
4786   have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
5062     by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_minus)
4787     by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac diff_minus)
5063   also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
4788   also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
5064     by (simp only: exsplit[OF qf] add_ac)
4789     by (simp only: exsplit[OF qf] add_ac)
5065   also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
4790   also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
5066     by (simp only: real_ex_int_real01[where P="\<lambda> x. Ifm (x#bs) p"])
4791     by (simp only: real_ex_int_real01[where P="\<lambda> x. Ifm (x#bs) p"])
5067   finally show ?thesis by simp
4792   finally show ?thesis by simp
5894
5619
5895 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
5620 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
5896 apply mir
5621 apply mir
5897 done
5622 done
5898
5623

5624 unused_thms

5625
5899 end
5626 end