src/HOL/Decision_Procs/MIR.thy
changeset 41849 1a65b780bd56
parent 41839 421a795cee05
child 41882 ae8d62656392
equal deleted 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 by (metis add_0_left add_le_cancel_right diff_add_cancel)
    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)
   146 
       
   147 lemma rdvd_trans: assumes mn:"m rdvd n" and  nk:"n rdvd k" 
       
   148   shows "m rdvd k"
       
   149 proof-
       
   150   from rdvd_def mn obtain c where nmc:"n = m * real (c::int)" by auto
       
   151   from rdvd_def nk obtain c' where nkc:"k = n * real (c'::int)" by auto
       
   152   hence "k = m * real (c * c')" using nmc by simp
       
   153   thus ?thesis using rdvd_def by blast
       
   154 qed
       
   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 
   516 lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"
       
   517 by(induct p rule: disjuncts.induct, auto)
       
   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)
   520 
       
   521 lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"
       
   522 proof-
       
   523   assume nb: "bound0 p"
       
   524   hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)
       
   525   thus ?thesis by (simp only: list_all_iff)
       
   526 qed
       
   527 lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). bound0 q"
       
   528 proof-
       
   529   assume nb: "bound0 p"
       
   530   hence "list_all bound0 (conjuncts p)" by (induct p rule:conjuncts.induct,auto)
       
   531   thus ?thesis by (simp only: list_all_iff)
       
   532 qed
       
   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 
   653 declare dvd_trans [trans add]
   581 declare dvd_trans [trans add]
   654 
       
   655 lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
       
   656 by arith
       
   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)
  1141 lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
       
  1142   using imp_def by (cases "p=F \<or> q=T \<or> p=q",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)
  1153 lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
       
  1154 using iff_def 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)
  1660 lemma not_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm (not p) bs"
       
  1661   by (induct p rule:iszlfm.induct ,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"]) 
  1744     (simp add: algebra_simps diff_minus[symmetric],arith)
  1663     (simp add: algebra_simps diff_minus[symmetric],arith)
  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
  2429     by (simp add: algebra_simps
  2348     by (simp add: algebra_simps
  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 *)
  2902 
       
  2903 recdef a\<rho> "measure size"
       
  2904   "a\<rho> (And p q) = (\<lambda> k. And (a\<rho> p k) (a\<rho> q k))" 
       
  2905   "a\<rho> (Or p q) = (\<lambda> k. Or (a\<rho> p k) (a\<rho> q k))" 
       
  2906   "a\<rho> (Eq (CN 0 c e)) = (\<lambda> k. if k dvd c then (Eq (CN 0 (c div k) e)) 
       
  2907                                            else (Eq (CN 0 c (Mul k e))))"
       
  2908   "a\<rho> (NEq (CN 0 c e)) = (\<lambda> k. if k dvd c then (NEq (CN 0 (c div k) e)) 
       
  2909                                            else (NEq (CN 0 c (Mul k e))))"
       
  2910   "a\<rho> (Lt (CN 0 c e)) = (\<lambda> k. if k dvd c then (Lt (CN 0 (c div k) e)) 
       
  2911                                            else (Lt (CN 0 c (Mul k e))))"
       
  2912   "a\<rho> (Le (CN 0 c e)) = (\<lambda> k. if k dvd c then (Le (CN 0 (c div k) e)) 
       
  2913                                            else (Le (CN 0 c (Mul k e))))"
       
  2914   "a\<rho> (Gt (CN 0 c e)) = (\<lambda> k. if k dvd c then (Gt (CN 0 (c div k) e)) 
       
  2915                                            else (Gt (CN 0 c (Mul k e))))"
       
  2916   "a\<rho> (Ge (CN 0 c e)) = (\<lambda> k. if k dvd c then (Ge (CN 0 (c div k) e)) 
       
  2917                                             else (Ge (CN 0 c (Mul k e))))"
       
  2918   "a\<rho> (Dvd i (CN 0 c e)) = (\<lambda> k. if k dvd c then (Dvd i (CN 0 (c div k) e)) 
       
  2919                                             else (Dvd (i*k) (CN 0 c (Mul k e))))"
       
  2920   "a\<rho> (NDvd i (CN 0 c e)) = (\<lambda> k. if k dvd c then (NDvd i (CN 0 (c div k) e)) 
       
  2921                                             else (NDvd (i*k) (CN 0 c (Mul k e))))"
       
  2922   "a\<rho> p = (\<lambda> k. p)"
       
  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"]
  3108         by (simp add: ti)
  3006         by (simp add: ti)
  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"] 
       
  3176       by (simp add: algebra_simps)
       
  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"] 
       
  3190       by (simp add: algebra_simps)
       
  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 
       
  3194 qed (simp_all add: nth_pos2)
       
  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]
       
  3203     by (simp add: algebra_simps)
       
  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)
  3231 
       
  3232 lemma zminusinf_\<rho>:
       
  3233   assumes lp: "iszlfm p (real (i::int)#bs)"
       
  3234   and nmi: "\<not> (Ifm (real i#bs) (minusinf p))" (is "\<not> (Ifm (real i#bs) (?M p))")
       
  3235   and ex: "Ifm (real i#bs) p" (is "?I i p")
       
  3236   shows "\<exists> (e,c) \<in> set (\<rho> p). real (c*i) > Inum (real i#bs) e" (is "\<exists> (e,c) \<in> ?R p. real (c*i) > ?N i e")
       
  3237   using lp nmi ex
       
  3238 by (induct p rule: minusinf.induct, auto)
       
  3239 
       
  3240 
       
  3241 lemma \<sigma>_And: "Ifm bs (\<sigma> (And p q) k t)  = Ifm bs (And (\<sigma> p k t) (\<sigma> q k t))"
       
  3242 using \<sigma>_def by auto
       
  3243 lemma \<sigma>_Or: "Ifm bs (\<sigma> (Or p q) k t)  = Ifm bs (Or (\<sigma> p k t) (\<sigma> q k t))"
       
  3244 using \<sigma>_def by 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 
  3376       by (simp add: algebra_simps)
  3158       by (simp add: algebra_simps)
  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 
  3514 lemma not_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm (not p)"
       
  3515   by (induct p rule: isrlfm.induct, auto)
       
  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)"
  3765       using pns by (simp add: fp_def np algebra_simps numsub numadd)
  3545       using pns by (simp add: fp_def np algebra_simps numsub numadd)
  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)"
  3793       using pns by (simp add: fp_def nn diff_minus add_ac mult_ac numfloor numadd numneg
  3573       using pns by (simp add: fp_def nn diff_minus add_ac mult_ac numfloor numadd numneg
  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)
  4144 lemma zgcd_le1: assumes ip: "(0::int) < i" shows "gcd i j \<le> i"
       
  4145 proof-
       
  4146   from gcd_dvd1_int have th: "gcd i j dvd i" by blast
       
  4147   from zdvd_imp_le[OF th ip] show ?thesis .
       
  4148 qed
       
  4149 
       
  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)
  3942         by (simp add: numgcd_def)
  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)
  3967         by (simp add: numgcd_def)
  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)
  3992         by (simp add: numgcd_def)
  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)
  4017         by (simp add: numgcd_def)
  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)
  4042         by (simp add: numgcd_def)
  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)
  4067         by (simp add: numgcd_def)
  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"] 
  4819       by (simp add: algebra_simps)
  4593       by (simp add: algebra_simps)
  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