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 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)`
`   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 `
`   653 declare dvd_trans [trans add]`
`   581 declare dvd_trans [trans add]`
`   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"]) `
`  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 *)`
`  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)`
`  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 `
`  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)`
`  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`