Some cleaning up
authornipkow
Fri Feb 25 20:07:48 2011 +0100 (2011-02-25)
changeset 418491a65b780bd56
parent 41843 15d76ed6ea67
child 41850 edfc06b8a507
Some cleaning up
src/HOL/Decision_Procs/DP_Library.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Decision_Procs/DP_Library.thy	Fri Feb 25 20:07:48 2011 +0100
     1.3 @@ -0,0 +1,36 @@
     1.4 +theory DP_Library
     1.5 +imports Main
     1.6 +begin
     1.7 +
     1.8 +primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
     1.9 +  "alluopairs [] = []"
    1.10 +| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
    1.11 +
    1.12 +lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
    1.13 +by (induct xs, auto)
    1.14 +
    1.15 +lemma alluopairs_set:
    1.16 +  "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
    1.17 +by (induct xs, auto)
    1.18 +
    1.19 +lemma alluopairs_bex:
    1.20 +  assumes Pc: "\<forall> x \<in> set xs. \<forall>y\<in> set xs. P x y = P y x"
    1.21 +  shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
    1.22 +proof
    1.23 +  assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
    1.24 +  then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"  by blast
    1.25 +  from alluopairs_set[OF x y] P Pc x y show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" 
    1.26 +    by auto
    1.27 +next
    1.28 +  assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
    1.29 +  then obtain "x" and "y"  where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
    1.30 +  from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
    1.31 +  with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
    1.32 +qed
    1.33 +
    1.34 +lemma alluopairs_ex:
    1.35 +  "\<forall> x y. P x y = P y x \<Longrightarrow>
    1.36 +  (\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
    1.37 +by(blast intro!: alluopairs_bex)
    1.38 +
    1.39 +end
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Feb 25 14:25:52 2011 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Feb 25 20:07:48 2011 +0100
     2.3 @@ -277,10 +277,7 @@
     2.4  end
     2.5  
     2.6  (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
     2.7 -lemma dnf[no_atp]:
     2.8 -  "(P & (Q | R)) = ((P&Q) | (P&R))" 
     2.9 -  "((Q | R) & P) = ((Q&P) | (R&P))"
    2.10 -  by blast+
    2.11 +lemmas dnf[no_atp] = conj_disj_distribL conj_disj_distribR
    2.12  
    2.13  lemmas weak_dnf_simps[no_atp] = simp_thms dnf
    2.14  
    2.15 @@ -875,7 +872,7 @@
    2.16    {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
    2.17  end
    2.18  *}
    2.19 -
    2.20 +(*
    2.21  lemma upper_bound_finite_set:
    2.22    assumes fS: "finite S"
    2.23    shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> a"
    2.24 @@ -927,7 +924,6 @@
    2.25    hence ?thesis by blast}
    2.26  ultimately show ?thesis by blast
    2.27  qed
    2.28 -
    2.29 -
    2.30 +*)
    2.31  
    2.32  end 
     3.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Feb 25 14:25:52 2011 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Feb 25 20:07:48 2011 +0100
     3.3 @@ -3,44 +3,14 @@
     3.4  *)
     3.5  
     3.6  theory Ferrack
     3.7 -imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
     3.8 +imports Complex_Main Dense_Linear_Order DP_Library
     3.9 +  "~~/src/HOL/Library/Efficient_Nat"
    3.10  uses ("ferrack_tac.ML")
    3.11  begin
    3.12  
    3.13  section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *}
    3.14  
    3.15    (*********************************************************************************)
    3.16 -  (*          SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB                      *)
    3.17 -  (*********************************************************************************)
    3.18 -
    3.19 -primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
    3.20 -  "alluopairs [] = []"
    3.21 -| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
    3.22 -
    3.23 -lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
    3.24 -by (induct xs, auto)
    3.25 -
    3.26 -lemma alluopairs_set:
    3.27 -  "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
    3.28 -by (induct xs, auto)
    3.29 -
    3.30 -lemma alluopairs_ex:
    3.31 -  assumes Pc: "\<forall> x y. P x y = P y x"
    3.32 -  shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
    3.33 -proof
    3.34 -  assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
    3.35 -  then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"  by blast
    3.36 -  from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" 
    3.37 -    by auto
    3.38 -next
    3.39 -  assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
    3.40 -  then obtain "x" and "y"  where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
    3.41 -  from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
    3.42 -  with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
    3.43 -qed
    3.44 -
    3.45 -
    3.46 -  (*********************************************************************************)
    3.47    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    3.48    (*********************************************************************************)
    3.49  
    3.50 @@ -1596,20 +1566,6 @@
    3.51    from ainS binS noy ax xb px show ?thesis by blast
    3.52  qed
    3.53  
    3.54 -lemma finite_set_intervals2:
    3.55 -  assumes px: "P (x::real)" 
    3.56 -  and lx: "l \<le> x" and xu: "x \<le> u"
    3.57 -  and linS: "l\<in> S" and uinS: "u \<in> S"
    3.58 -  and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
    3.59 -  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)"
    3.60 -proof-
    3.61 -  from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
    3.62 -  obtain a and b where 
    3.63 -    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
    3.64 -  from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto
    3.65 -  thus ?thesis using px as bs noS by blast 
    3.66 -qed
    3.67 -
    3.68  lemma rinf_uset:
    3.69    assumes lp: "isrlfm p"
    3.70    and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))")
     4.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Feb 25 14:25:52 2011 +0100
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Feb 25 20:07:48 2011 +0100
     4.3 @@ -3,7 +3,8 @@
     4.4  *)
     4.5  
     4.6  theory MIR
     4.7 -imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
     4.8 +imports Complex_Main Dense_Linear_Order DP_Library
     4.9 +  "~~/src/HOL/Library/Efficient_Nat"
    4.10  uses ("mir_tac.ML")
    4.11  begin
    4.12  
    4.13 @@ -11,57 +12,13 @@
    4.14  
    4.15  declare real_of_int_floor_cancel [simp del]
    4.16  
    4.17 -primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where 
    4.18 -  "alluopairs [] = []"
    4.19 -| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
    4.20 -
    4.21 -lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
    4.22 -by (induct xs, auto)
    4.23 -
    4.24 -lemma alluopairs_set:
    4.25 -  "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
    4.26 -by (induct xs, auto)
    4.27 -
    4.28 -lemma alluopairs_ex:
    4.29 -  assumes Pc: "\<forall> x y. P x y = P y x"
    4.30 -  shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
    4.31 -proof
    4.32 -  assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
    4.33 -  then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"  by blast
    4.34 -  from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" 
    4.35 -    by auto
    4.36 -next
    4.37 -  assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
    4.38 -  then obtain "x" and "y"  where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
    4.39 -  from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
    4.40 -  with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
    4.41 -qed
    4.42 -
    4.43 -lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
    4.44 -using Nat.gr0_conv_Suc
    4.45 -by clarsimp
    4.46 -
    4.47 -
    4.48 -lemma myl: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a \<le> b) = (0 \<le> b - a)" 
    4.49 -proof(clarify)
    4.50 -  fix x y ::"'a"
    4.51 -  have "(x \<le> y) = (x - y \<le> 0)" by (simp only: le_iff_diff_le_0[where a="x" and b="y"])
    4.52 -  also have "\<dots> = (- (y - x) \<le> 0)" by simp
    4.53 -  also have "\<dots> = (0 \<le> y - x)" by (simp only: neg_le_0_iff_le[where a="y-x"])
    4.54 -  finally show "(x \<le> y) = (0 \<le> y - x)" .
    4.55 -qed
    4.56 -
    4.57 -lemma myless: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a < b) = (0 < b - a)" 
    4.58 -proof(clarify)
    4.59 -  fix x y ::"'a"
    4.60 -  have "(x < y) = (x - y < 0)" by (simp only: less_iff_diff_less_0[where a="x" and b="y"])
    4.61 -  also have "\<dots> = (- (y - x) < 0)" by simp
    4.62 -  also have "\<dots> = (0 < y - x)" by (simp only: neg_less_0_iff_less[where a="y-x"])
    4.63 -  finally show "(x < y) = (0 < y - x)" .
    4.64 -qed
    4.65 -
    4.66 -lemma myeq: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a = b) = (0 = b - a)"
    4.67 -  by auto
    4.68 +lemma myle: fixes a b :: "'a::{ordered_ab_group_add}"
    4.69 +  shows "(a \<le> b) = (0 \<le> b - a)"
    4.70 +by (metis add_0_left add_le_cancel_right diff_add_cancel)
    4.71 +
    4.72 +lemma myless: fixes a b :: "'a::{ordered_ab_group_add}"
    4.73 +  shows "(a < b) = (0 < b - a)"
    4.74 +by (metis le_iff_diff_le_0 less_le_not_le myle)
    4.75  
    4.76    (* Maybe should be added to the library \<dots> *)
    4.77  lemma floor_int_eq: "(real n\<le> x \<and> x < real (n+1)) = (floor x = n)"
    4.78 @@ -144,15 +101,6 @@
    4.79    shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)"
    4.80  using knz by (simp add:rdvd_def)
    4.81  
    4.82 -lemma rdvd_trans: assumes mn:"m rdvd n" and  nk:"n rdvd k" 
    4.83 -  shows "m rdvd k"
    4.84 -proof-
    4.85 -  from rdvd_def mn obtain c where nmc:"n = m * real (c::int)" by auto
    4.86 -  from rdvd_def nk obtain c' where nkc:"k = n * real (c'::int)" by auto
    4.87 -  hence "k = m * real (c * c')" using nmc by simp
    4.88 -  thus ?thesis using rdvd_def by blast
    4.89 -qed
    4.90 -
    4.91    (*********************************************************************************)
    4.92    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    4.93    (*********************************************************************************)
    4.94 @@ -335,7 +283,7 @@
    4.95  lemma numbound0_I:
    4.96    assumes nb: "numbound0 a"
    4.97    shows "Inum (b#bs) a = Inum (b'#bs) a"
    4.98 -  using nb by (induct a) (auto simp add: nth_pos2)
    4.99 +  using nb by (induct a) auto
   4.100  
   4.101  lemma numbound0_gen: 
   4.102    assumes nb: "numbound0 t" and ti: "isint t (x#bs)"
   4.103 @@ -371,7 +319,7 @@
   4.104    assumes bp: "bound0 p"
   4.105    shows "Ifm (b#bs) p = Ifm (b'#bs) p"
   4.106   using bp numbound0_I [where b="b" and bs="bs" and b'="b'"]
   4.107 -  by (induct p) (auto simp add: nth_pos2)
   4.108 +  by (induct p) auto
   4.109  
   4.110  primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where
   4.111    "numsubst0 t (C c) = (C c)"
   4.112 @@ -386,12 +334,7 @@
   4.113  
   4.114  lemma numsubst0_I:
   4.115    shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   4.116 -  by (induct t) (simp_all add: nth_pos2)
   4.117 -
   4.118 -lemma numsubst0_I':
   4.119 -  assumes nb: "numbound0 a"
   4.120 -  shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   4.121 -  by (induct t) (simp_all add: nth_pos2 numbound0_I[OF nb, where b="b" and b'="b'"])
   4.122 +  by (induct t) simp_all
   4.123  
   4.124  primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   4.125    "subst0 t T = T"
   4.126 @@ -413,7 +356,7 @@
   4.127  lemma subst0_I: assumes qfp: "qfree p"
   4.128    shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"
   4.129    using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
   4.130 -  by (induct p) (simp_all add: nth_pos2 )
   4.131 +  by (induct p) simp_all
   4.132  
   4.133  fun decrnum:: "num \<Rightarrow> num" where
   4.134    "decrnum (Bound n) = Bound (n - 1)"
   4.135 @@ -444,12 +387,12 @@
   4.136  
   4.137  lemma decrnum: assumes nb: "numbound0 t"
   4.138    shows "Inum (x#bs) t = Inum bs (decrnum t)"
   4.139 -  using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)
   4.140 +  using nb by (induct t rule: decrnum.induct, simp_all)
   4.141  
   4.142  lemma decr: assumes nb: "bound0 p"
   4.143    shows "Ifm (x#bs) p = Ifm bs (decr p)"
   4.144    using nb 
   4.145 -  by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)
   4.146 +  by (induct p rule: decr.induct, simp_all add: decrnum)
   4.147  
   4.148  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
   4.149  by (induct p, simp_all)
   4.150 @@ -513,24 +456,9 @@
   4.151  | "conjuncts T = []"
   4.152  | "conjuncts p = [p]"
   4.153  
   4.154 -lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"
   4.155 -by(induct p rule: disjuncts.induct, auto)
   4.156  lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm bs q) = Ifm bs p"
   4.157  by(induct p rule: conjuncts.induct, auto)
   4.158  
   4.159 -lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"
   4.160 -proof-
   4.161 -  assume nb: "bound0 p"
   4.162 -  hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)
   4.163 -  thus ?thesis by (simp only: list_all_iff)
   4.164 -qed
   4.165 -lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). bound0 q"
   4.166 -proof-
   4.167 -  assume nb: "bound0 p"
   4.168 -  hence "list_all bound0 (conjuncts p)" by (induct p rule:conjuncts.induct,auto)
   4.169 -  thus ?thesis by (simp only: list_all_iff)
   4.170 -qed
   4.171 -
   4.172  lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
   4.173  proof-
   4.174    assume qf: "qfree p"
   4.175 @@ -652,9 +580,6 @@
   4.176  
   4.177  declare dvd_trans [trans add]
   4.178  
   4.179 -lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
   4.180 -by arith
   4.181 -
   4.182  lemma numgcd0:
   4.183    assumes g0: "numgcd t = 0"
   4.184    shows "Inum bs t = 0"
   4.185 @@ -1138,8 +1063,6 @@
   4.186    by (cases "p=F \<or> q=T",simp_all add: imp_def)
   4.187  lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
   4.188    using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
   4.189 -lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
   4.190 -  using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 
   4.191  
   4.192  definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   4.193    "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
   4.194 @@ -1150,8 +1073,6 @@
   4.195  (cases "not p= q", auto simp add:not)
   4.196  lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
   4.197    by (unfold iff_def,cases "p=q", auto)
   4.198 -lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
   4.199 -using iff_def by (unfold iff_def,cases "p=q", auto)
   4.200  
   4.201  fun check_int:: "num \<Rightarrow> bool" where
   4.202    "check_int (C i) = True"
   4.203 @@ -1657,8 +1578,6 @@
   4.204    using conj_def by (cases p,auto)
   4.205  lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"
   4.206    using disj_def by (cases p,auto)
   4.207 -lemma not_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm (not p) bs"
   4.208 -  by (induct p rule:iszlfm.induct ,auto)
   4.209  
   4.210  recdef zlfm "measure fmsize"
   4.211    "zlfm (And p q) = conj (zlfm p) (zlfm q)"
   4.212 @@ -1739,7 +1658,7 @@
   4.213    "(real (a::int) + b > 0) = (real a + real (floor b) > 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"
   4.214  proof- 
   4.215    have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
   4.216 -  show ?thesis using myless[rule_format, where b="real (floor b)"] 
   4.217 +  show ?thesis using myless[of _ "real (floor b)"] 
   4.218      by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) 
   4.219      (simp add: algebra_simps diff_minus[symmetric],arith)
   4.220  qed
   4.221 @@ -2291,7 +2210,7 @@
   4.222          by blast
   4.223        thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
   4.224      qed
   4.225 -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)
   4.226 +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)
   4.227  
   4.228  lemma minusinf_ex:
   4.229    assumes lin: "iszlfm p (real (a::int) #bs)"
   4.230 @@ -2428,7 +2347,7 @@
   4.231    from prems th show  ?case
   4.232      by (simp add: algebra_simps
   4.233        numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
   4.234 -qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"] nth_pos2)
   4.235 +qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"])
   4.236  
   4.237  lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
   4.238  by (induct p rule: mirror.induct, auto simp add: isint_neg)
   4.239 @@ -2636,7 +2555,7 @@
   4.240      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
   4.241    also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
   4.242    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
   4.243 -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)
   4.244 +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)
   4.245  
   4.246  lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0"
   4.247    shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
   4.248 @@ -2780,7 +2699,7 @@
   4.249      also have "\<dots> = (\<not> real j rdvd real x - real d + ?e)" 
   4.250        using ie by simp
   4.251      finally show ?case using numbound0_I[OF bn,where b="real (x-d)" and b'="real x" and bs="bs"] c1 p by simp
   4.252 -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)
   4.253 +qed (auto simp add: numbound0_I[where bs="bs" and b="real (x - d)" and b'="real x"] simp del: real_of_int_diff)
   4.254  
   4.255  lemma \<beta>':   
   4.256    assumes lp: "iszlfm p (a #bs)"
   4.257 @@ -2900,27 +2819,6 @@
   4.258  
   4.259      (* Simulates normal substituion by modifying the formula see correctness theorem *)
   4.260  
   4.261 -recdef a\<rho> "measure size"
   4.262 -  "a\<rho> (And p q) = (\<lambda> k. And (a\<rho> p k) (a\<rho> q k))" 
   4.263 -  "a\<rho> (Or p q) = (\<lambda> k. Or (a\<rho> p k) (a\<rho> q k))" 
   4.264 -  "a\<rho> (Eq (CN 0 c e)) = (\<lambda> k. if k dvd c then (Eq (CN 0 (c div k) e)) 
   4.265 -                                           else (Eq (CN 0 c (Mul k e))))"
   4.266 -  "a\<rho> (NEq (CN 0 c e)) = (\<lambda> k. if k dvd c then (NEq (CN 0 (c div k) e)) 
   4.267 -                                           else (NEq (CN 0 c (Mul k e))))"
   4.268 -  "a\<rho> (Lt (CN 0 c e)) = (\<lambda> k. if k dvd c then (Lt (CN 0 (c div k) e)) 
   4.269 -                                           else (Lt (CN 0 c (Mul k e))))"
   4.270 -  "a\<rho> (Le (CN 0 c e)) = (\<lambda> k. if k dvd c then (Le (CN 0 (c div k) e)) 
   4.271 -                                           else (Le (CN 0 c (Mul k e))))"
   4.272 -  "a\<rho> (Gt (CN 0 c e)) = (\<lambda> k. if k dvd c then (Gt (CN 0 (c div k) e)) 
   4.273 -                                           else (Gt (CN 0 c (Mul k e))))"
   4.274 -  "a\<rho> (Ge (CN 0 c e)) = (\<lambda> k. if k dvd c then (Ge (CN 0 (c div k) e)) 
   4.275 -                                            else (Ge (CN 0 c (Mul k e))))"
   4.276 -  "a\<rho> (Dvd i (CN 0 c e)) = (\<lambda> k. if k dvd c then (Dvd i (CN 0 (c div k) e)) 
   4.277 -                                            else (Dvd (i*k) (CN 0 c (Mul k e))))"
   4.278 -  "a\<rho> (NDvd i (CN 0 c e)) = (\<lambda> k. if k dvd c then (NDvd i (CN 0 (c div k) e)) 
   4.279 -                                            else (NDvd (i*k) (CN 0 c (Mul k e))))"
   4.280 -  "a\<rho> p = (\<lambda> k. p)"
   4.281 -
   4.282  definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
   4.283    "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))"
   4.284  
   4.285 @@ -3108,110 +3006,8 @@
   4.286          by (simp add: ti)
   4.287        finally have ?case . }
   4.288      ultimately show ?case by blast 
   4.289 -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"])
   4.290 -
   4.291 -
   4.292 -lemma a\<rho>: 
   4.293 -  assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "real k > 0" 
   4.294 -  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")
   4.295 -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"]
   4.296 -proof(induct p rule: a\<rho>.induct)
   4.297 -  case (3 c e)  
   4.298 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.299 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.300 -    {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.301 -    moreover 
   4.302 -    {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)}
   4.303 -    ultimately show ?case by blast 
   4.304 -next
   4.305 -  case (4 c e)   
   4.306 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.307 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.308 -    {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.309 -    moreover 
   4.310 -    {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)}
   4.311 -    ultimately show ?case by blast 
   4.312 -next
   4.313 -  case (5 c e)   
   4.314 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.315 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.316 -    {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.317 -    moreover 
   4.318 -    {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)}
   4.319 -    ultimately show ?case by blast 
   4.320 -next
   4.321 -  case (6 c e)    
   4.322 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.323 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.324 -    {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.325 -    moreover 
   4.326 -    {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)}
   4.327 -    ultimately show ?case by blast 
   4.328 -next
   4.329 -  case (7 c e)    
   4.330 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.331 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.332 -    {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.333 -    moreover 
   4.334 -    {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)}
   4.335 -    ultimately show ?case by blast 
   4.336 -next
   4.337 -  case (8 c e)    
   4.338 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.339 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.340 -    {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.341 -    moreover 
   4.342 -    {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)}
   4.343 -    ultimately show ?case by blast 
   4.344 -next
   4.345 -  case (9 i c e)
   4.346 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.347 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.348 -  {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.349 -  moreover 
   4.350 -  {assume "\<not> k dvd c"
   4.351 -    hence "Ifm (real (x*k)#bs) (a\<rho> (Dvd i (CN 0 c e)) k) = 
   4.352 -      (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k)" 
   4.353 -      using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] 
   4.354 -      by (simp add: algebra_simps)
   4.355 -    also have "\<dots> = (Ifm (real x#bs) (Dvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
   4.356 -    finally have ?case . }
   4.357 -  ultimately show ?case by blast 
   4.358 -next
   4.359 -  case (10 i c e) 
   4.360 -  from prems have cp: "c > 0" and nb: "numbound0 e" by auto
   4.361 -  from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.362 -  {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.363 -  moreover 
   4.364 -  {assume "\<not> k dvd c"
   4.365 -    hence "Ifm (real (x*k)#bs) (a\<rho> (NDvd i (CN 0 c e)) k) = 
   4.366 -      (\<not> (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k))" 
   4.367 -      using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] 
   4.368 -      by (simp add: algebra_simps)
   4.369 -    also have "\<dots> = (Ifm (real x#bs) (NDvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
   4.370 -    finally have ?case . }
   4.371 -  ultimately show ?case by blast 
   4.372 -qed (simp_all add: nth_pos2)
   4.373 -
   4.374 -lemma a\<rho>_ex: 
   4.375 -  assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "k > 0"
   4.376 -  shows "(\<exists> (x::int). real k rdvd real x \<and> Ifm (real x#bs) (a\<rho> p k)) = 
   4.377 -  (\<exists> (x::int). Ifm (real x#bs) p)" (is "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. ?P x)")
   4.378 -proof-
   4.379 -  have "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. k dvd x \<and> ?P' x)" using int_rdvd_iff by simp
   4.380 -  also have "\<dots> = (\<exists>x. ?P' (x*k))" using unity_coeff_ex[where P="?P'" and l="k", simplified]
   4.381 -    by (simp add: algebra_simps)
   4.382 -  also have "\<dots> = (\<exists> x. ?P x)" using a\<rho> iszlfm_gen[OF lp] kp by auto
   4.383 -  finally show ?thesis .
   4.384 -qed
   4.385 -
   4.386 -lemma \<sigma>\<rho>': assumes lp: "iszlfm p (real (x::int)#bs)" and kp: "k > 0" and nb: "numbound0 t"
   4.387 -  shows "Ifm (real x#bs) (\<sigma>\<rho> p (t,k)) = Ifm ((Inum (real x#bs) t)#bs) (a\<rho> p k)"
   4.388 -using lp 
   4.389 -by(induct p rule: \<sigma>\<rho>.induct, simp_all add: 
   4.390 -  numbound0_I[OF nb, where bs="bs" and b="Inum (real x#bs) t" and b'="real x"] 
   4.391 -  numbound0_I[where bs="bs" and b="Inum (real x#bs) t" and b'="real x"] 
   4.392 -  bound0_I[where bs="bs" and b="Inum (real x#bs) t" and b'="real x"] nth_pos2 cong: imp_cong)
   4.393 +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"])
   4.394 +
   4.395  
   4.396  lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
   4.397    shows "bound0 (\<sigma>\<rho> p (t,k))"
   4.398 @@ -3229,20 +3025,6 @@
   4.399  using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"]
   4.400   by (induct p rule: \<alpha>\<rho>.induct, auto)
   4.401  
   4.402 -lemma zminusinf_\<rho>:
   4.403 -  assumes lp: "iszlfm p (real (i::int)#bs)"
   4.404 -  and nmi: "\<not> (Ifm (real i#bs) (minusinf p))" (is "\<not> (Ifm (real i#bs) (?M p))")
   4.405 -  and ex: "Ifm (real i#bs) p" (is "?I i p")
   4.406 -  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")
   4.407 -  using lp nmi ex
   4.408 -by (induct p rule: minusinf.induct, auto)
   4.409 -
   4.410 -
   4.411 -lemma \<sigma>_And: "Ifm bs (\<sigma> (And p q) k t)  = Ifm bs (And (\<sigma> p k t) (\<sigma> q k t))"
   4.412 -using \<sigma>_def by auto
   4.413 -lemma \<sigma>_Or: "Ifm bs (\<sigma> (Or p q) k t)  = Ifm bs (Or (\<sigma> p k t) (\<sigma> q k t))"
   4.414 -using \<sigma>_def by auto
   4.415 -
   4.416  lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)"
   4.417    and pi: "Ifm (real i#bs) p"
   4.418    and d: "d\<delta> p d"
   4.419 @@ -3374,7 +3156,7 @@
   4.420      finally show ?case 
   4.421        using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p 
   4.422        by (simp add: algebra_simps)
   4.423 -qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] nth_pos2)
   4.424 +qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"])
   4.425  
   4.426  lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
   4.427    shows "bound0 (\<sigma> p k t)"
   4.428 @@ -3511,8 +3293,6 @@
   4.429  by pat_completeness auto
   4.430  termination by (relation "measure num_size") auto
   4.431  
   4.432 -lemma not_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm (not p)"
   4.433 -  by (induct p rule: isrlfm.induct, auto)
   4.434  lemma conj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
   4.435    using conj_def by (cases p, auto)
   4.436  lemma disj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
   4.437 @@ -3760,7 +3540,7 @@
   4.438      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
   4.439      
   4.440      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"
   4.441 -      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)"]) 
   4.442 +      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)"]) 
   4.443      hence "\<exists> j\<in> {0.. n}. ?I (?p (p,n,s) j)"
   4.444        using pns by (simp add: fp_def np algebra_simps numsub numadd)
   4.445      then obtain "j" where j_def: "j\<in> {0 .. n} \<and> ?I (?p (p,n,s) j)" by blast
   4.446 @@ -3787,7 +3567,7 @@
   4.447      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
   4.448      
   4.449      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"
   4.450 -      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)"]) 
   4.451 +      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)"]) 
   4.452      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])
   4.453      hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
   4.454        using pns by (simp add: fp_def nn diff_minus add_ac mult_ac numfloor numadd numneg
   4.455 @@ -3885,7 +3665,7 @@
   4.456    fix a n s
   4.457    assume H: "?N a = ?N (CN 0 n s)"
   4.458    show "?I (lt n s) = ?I (Lt a)" using H by (cases "n=0", (simp add: lt_def))
   4.459 -  (cases "n > 0", simp_all add: lt_def algebra_simps myless[rule_format, where b="0"])
   4.460 +  (cases "n > 0", simp_all add: lt_def algebra_simps myless[of _ "0"])
   4.461  qed
   4.462  
   4.463  lemma lt_l: "isrlfm (rsplit lt a)"
   4.464 @@ -3897,7 +3677,7 @@
   4.465    fix a n s
   4.466    assume H: "?N a = ?N (CN 0 n s)"
   4.467    show "?I (le n s) = ?I (Le a)" using H by (cases "n=0", (simp add: le_def))
   4.468 -  (cases "n > 0", simp_all add: le_def algebra_simps myl[rule_format, where b="0"])
   4.469 +  (cases "n > 0", simp_all add: le_def algebra_simps myle[of _ "0"])
   4.470  qed
   4.471  
   4.472  lemma le_l: "isrlfm (rsplit le a)"
   4.473 @@ -3909,7 +3689,7 @@
   4.474    fix a n s
   4.475    assume H: "?N a = ?N (CN 0 n s)"
   4.476    show "?I (gt n s) = ?I (Gt a)" using H by (cases "n=0", (simp add: gt_def))
   4.477 -  (cases "n > 0", simp_all add: gt_def algebra_simps myless[rule_format, where b="0"])
   4.478 +  (cases "n > 0", simp_all add: gt_def algebra_simps myless[of _ "0"])
   4.479  qed
   4.480  lemma gt_l: "isrlfm (rsplit gt a)"
   4.481    by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def) 
   4.482 @@ -3920,7 +3700,7 @@
   4.483    fix a n s 
   4.484    assume H: "?N a = ?N (CN 0 n s)"
   4.485    show "?I (ge n s) = ?I (Ge a)" using H by (cases "n=0", (simp add: ge_def))
   4.486 -  (cases "n > 0", simp_all add: ge_def algebra_simps myl[rule_format, where b="0"])
   4.487 +  (cases "n > 0", simp_all add: ge_def algebra_simps myle[of _ "0"])
   4.488  qed
   4.489  lemma ge_l: "isrlfm (rsplit ge a)"
   4.490    by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def) 
   4.491 @@ -3962,9 +3742,9 @@
   4.492    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")
   4.493  proof-
   4.494    let ?ss = "s - real (floor s)"
   4.495 -  from real_of_int_floor_add_one_gt[where r="s", simplified myless[rule_format,where a="s"]] 
   4.496 +  from real_of_int_floor_add_one_gt[where r="s", simplified myless[of "s"]] 
   4.497      real_of_int_floor_le[where r="s"]  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1" 
   4.498 -    by (auto simp add: myl[rule_format, where b="s", symmetric] myless[rule_format, where a="?ss"])
   4.499 +    by (auto simp add: myle[of _ "s", symmetric] myless[of "?ss"])
   4.500    from np have n0: "real n \<ge> 0" by simp
   4.501    from mult_left_mono[OF up n0] mult_strict_left_mono[OF u1 np] 
   4.502    have nu0:"real n * u - s \<ge> -s" and nun:"real n * u -s < real n - s" by auto  
   4.503 @@ -4141,12 +3921,6 @@
   4.504  
   4.505  lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
   4.506    by (induct p rule: isrlfm.induct, auto)
   4.507 -lemma zgcd_le1: assumes ip: "(0::int) < i" shows "gcd i j \<le> i"
   4.508 -proof-
   4.509 -  from gcd_dvd1_int have th: "gcd i j dvd i" by blast
   4.510 -  from zdvd_imp_le[OF th ip] show ?thesis .
   4.511 -qed
   4.512 -
   4.513  
   4.514  lemma simpfm_rl: "isrlfm p \<Longrightarrow> isrlfm (simpfm p)"
   4.515  proof (induct p)
   4.516 @@ -4165,7 +3939,7 @@
   4.517        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   4.518        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   4.519        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   4.520 -        by (simp add: numgcd_def zgcd_le1)
   4.521 +        by (simp add: numgcd_def)
   4.522        from prems have th': "c\<noteq>0" by auto
   4.523        from prems have cp: "c \<ge> 0" by simp
   4.524        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.525 @@ -4190,7 +3964,7 @@
   4.526        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   4.527        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   4.528        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   4.529 -        by (simp add: numgcd_def zgcd_le1)
   4.530 +        by (simp add: numgcd_def)
   4.531        from prems have th': "c\<noteq>0" by auto
   4.532        from prems have cp: "c \<ge> 0" by simp
   4.533        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.534 @@ -4215,7 +3989,7 @@
   4.535        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   4.536        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   4.537        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   4.538 -        by (simp add: numgcd_def zgcd_le1)
   4.539 +        by (simp add: numgcd_def)
   4.540        from prems have th': "c\<noteq>0" by auto
   4.541        from prems have cp: "c \<ge> 0" by simp
   4.542        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.543 @@ -4240,7 +4014,7 @@
   4.544        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   4.545        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   4.546        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   4.547 -        by (simp add: numgcd_def zgcd_le1)
   4.548 +        by (simp add: numgcd_def)
   4.549        from prems have th': "c\<noteq>0" by auto
   4.550        from prems have cp: "c \<ge> 0" by simp
   4.551        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.552 @@ -4265,7 +4039,7 @@
   4.553        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   4.554        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   4.555        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   4.556 -        by (simp add: numgcd_def zgcd_le1)
   4.557 +        by (simp add: numgcd_def)
   4.558        from prems have th': "c\<noteq>0" by auto
   4.559        from prems have cp: "c \<ge> 0" by simp
   4.560        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.561 @@ -4290,7 +4064,7 @@
   4.562        with numgcd_pos[where t="CN 0 c (simpnum e)"]
   4.563        have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
   4.564        from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c" 
   4.565 -        by (simp add: numgcd_def zgcd_le1)
   4.566 +        by (simp add: numgcd_def)
   4.567        from prems have th': "c\<noteq>0" by auto
   4.568        from prems have cp: "c \<ge> 0" by simp
   4.569        from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.570 @@ -4674,7 +4448,7 @@
   4.571    also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
   4.572      using np by simp 
   4.573    finally show ?case using nbt nb by (simp add: algebra_simps)
   4.574 -qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
   4.575 +qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"])
   4.576  
   4.577  lemma \<Upsilon>_l:
   4.578    assumes lp: "isrlfm p"
   4.579 @@ -4690,7 +4464,7 @@
   4.580  proof-
   4.581    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")
   4.582      using lp nmi ex
   4.583 -    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
   4.584 +    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
   4.585    then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<ge> ?N a s" by blast
   4.586    from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
   4.587    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" 
   4.588 @@ -4706,7 +4480,7 @@
   4.589  proof-
   4.590    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")
   4.591      using lp nmi ex
   4.592 -    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
   4.593 +    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
   4.594    then obtain s m where smU: "(s,m) \<in> set (\<Upsilon> p)" and mx: "real m * x \<le> ?N a s" by blast
   4.595    from \<Upsilon>_l[OF lp] smU have mp: "real m > 0" by auto
   4.596    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" 
   4.597 @@ -4817,56 +4591,7 @@
   4.598      hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
   4.599      thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
   4.600        by (simp add: algebra_simps)
   4.601 -qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
   4.602 -
   4.603 -lemma finite_set_intervals:
   4.604 -  assumes px: "P (x::real)" 
   4.605 -  and lx: "l \<le> x" and xu: "x \<le> u"
   4.606 -  and linS: "l\<in> S" and uinS: "u \<in> S"
   4.607 -  and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   4.608 -  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"
   4.609 -proof-
   4.610 -  let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
   4.611 -  let ?xM = "{y. y\<in> S \<and> x \<le> y}"
   4.612 -  let ?a = "Max ?Mx"
   4.613 -  let ?b = "Min ?xM"
   4.614 -  have MxS: "?Mx \<subseteq> S" by blast
   4.615 -  hence fMx: "finite ?Mx" using fS finite_subset by auto
   4.616 -  from lx linS have linMx: "l \<in> ?Mx" by blast
   4.617 -  hence Mxne: "?Mx \<noteq> {}" by blast
   4.618 -  have xMS: "?xM \<subseteq> S" by blast
   4.619 -  hence fxM: "finite ?xM" using fS finite_subset by auto
   4.620 -  from xu uinS have linxM: "u \<in> ?xM" by blast
   4.621 -  hence xMne: "?xM \<noteq> {}" by blast
   4.622 -  have ax:"?a \<le> x" using Mxne fMx by auto
   4.623 -  have xb:"x \<le> ?b" using xMne fxM by auto
   4.624 -  have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
   4.625 -  have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
   4.626 -  have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
   4.627 -  proof(clarsimp)
   4.628 -    fix y
   4.629 -    assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
   4.630 -    from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by auto
   4.631 -    moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp}
   4.632 -    moreover {assume "y \<in> ?xM" hence "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp}
   4.633 -    ultimately show "False" by blast
   4.634 -  qed
   4.635 -  from ainS binS noy ax xb px show ?thesis by blast
   4.636 -qed
   4.637 -
   4.638 -lemma finite_set_intervals2:
   4.639 -  assumes px: "P (x::real)" 
   4.640 -  and lx: "l \<le> x" and xu: "x \<le> u"
   4.641 -  and linS: "l\<in> S" and uinS: "u \<in> S"
   4.642 -  and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   4.643 -  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)"
   4.644 -proof-
   4.645 -  from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
   4.646 -  obtain a and b where 
   4.647 -    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
   4.648 -  from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto
   4.649 -  thus ?thesis using px as bs noS by blast 
   4.650 -qed
   4.651 +qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"])
   4.652  
   4.653  lemma rinf_\<Upsilon>:
   4.654    assumes lp: "isrlfm p"
   4.655 @@ -5059,7 +4784,7 @@
   4.656    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")
   4.657  proof-
   4.658    have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
   4.659 -    by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_minus)
   4.660 +    by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac diff_minus)
   4.661    also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
   4.662      by (simp only: exsplit[OF qf] add_ac)
   4.663    also have "\<dots> = (\<exists> x. Ifm (x#bs) p)" 
   4.664 @@ -5896,4 +5621,6 @@
   4.665  apply mir
   4.666  done
   4.667  
   4.668 +unused_thms
   4.669 +
   4.670  end
     5.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 25 14:25:52 2011 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 25 20:07:48 2011 +0100
     5.3 @@ -5,9 +5,7 @@
     5.4  header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
     5.5  
     5.6  theory Parametric_Ferrante_Rackoff
     5.7 -imports
     5.8 -  Reflected_Multivariate_Polynomial
     5.9 -  Dense_Linear_Order
    5.10 +imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
    5.11    "~~/src/HOL/Library/Efficient_Nat"
    5.12  begin
    5.13  
    5.14 @@ -2440,34 +2438,6 @@
    5.15  from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis .
    5.16  qed 
    5.17  
    5.18 -text {* Rest of the implementation *}
    5.19 -
    5.20 -primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
    5.21 -  "alluopairs [] = []"
    5.22 -| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
    5.23 -
    5.24 -lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
    5.25 -by (induct xs, auto)
    5.26 -
    5.27 -lemma alluopairs_set:
    5.28 -  "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
    5.29 -by (induct xs, auto)
    5.30 -
    5.31 -lemma alluopairs_ex:
    5.32 -  assumes Pc: "\<forall> x \<in> set xs. \<forall>y\<in> set xs. P x y = P y x"
    5.33 -  shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
    5.34 -proof
    5.35 -  assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
    5.36 -  then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"  by blast
    5.37 -  from alluopairs_set[OF x y] P Pc x y show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" 
    5.38 -    by auto
    5.39 -next
    5.40 -  assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
    5.41 -  then obtain "x" and "y"  where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
    5.42 -  from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
    5.43 -  with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
    5.44 -qed
    5.45 -
    5.46  lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    5.47    shows "qfree p \<Longrightarrow> islin (simpfm p)"
    5.48    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
    5.49 @@ -2516,7 +2486,7 @@
    5.50    from decr0_qf[OF th1] have thqf: "qfree (ferrack p)" by (simp add: ferrack_def Let_def)
    5.51    have "?lhs \<longleftrightarrow> (\<exists>x. Ifm vs (x#bs) ?q)" by simp
    5.52    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists>(c, t)\<in>set ?U. \<exists>(d, s)\<in>set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))" using fr_eq_msubst[OF lq, of vs bs x] by simp
    5.53 -  also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists> (x,y) \<in> set ?Up. ?I ((simpfm o (msubst ?q)) (x,y)))" using alluopairs_ex[OF th0] by simp
    5.54 +  also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists> (x,y) \<in> set ?Up. ?I ((simpfm o (msubst ?q)) (x,y)))" using alluopairs_bex[OF th0] by simp
    5.55    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (evaldjf (simpfm o (msubst ?q)) ?Up)" 
    5.56      by (simp add: evaldjf_ex)
    5.57    also have "\<dots> \<longleftrightarrow> ?I (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up)))" by simp
    5.58 @@ -2857,7 +2827,7 @@
    5.59    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or> (\<exists>(n,t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or> (\<exists> x\<in>set ?U. \<exists> y \<in>set ?U. ?I (?s (x,y)))"
    5.60      by (simp add: split_def)
    5.61    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or> (\<exists>(n,t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or> (\<exists> (x,y) \<in> set ?Up. ?I (?s (x,y)))"
    5.62 -    using alluopairs_ex[OF th0] by simp 
    5.63 +    using alluopairs_bex[OF th0] by simp 
    5.64    also have "\<dots> \<longleftrightarrow> ?I ?R" 
    5.65      by (simp add: list_disj_def evaldjf_ex split_def)
    5.66    also have "\<dots> \<longleftrightarrow> ?rhs"