1.1 --- a/src/HOL/ex/Reflected_Presburger.thy Fri Jan 30 13:41:45 2009 +0000
1.2 +++ b/src/HOL/ex/Reflected_Presburger.thy Sat Jan 31 09:04:16 2009 +0100
1.3 @@ -995,7 +995,7 @@
1.4 hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
1.5 moreover
1.6 {assume "?c=0" and "j\<noteq>0" hence ?case
1.7 - using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
1.8 + using zsplit0_I[OF spl, where x="i" and bs="bs"]
1.9 apply (auto simp add: Let_def split_def algebra_simps)
1.10 apply (cases "?r",auto)
1.11 apply (case_tac nat, auto)
1.12 @@ -1003,14 +1003,12 @@
1.13 moreover
1.14 {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
1.15 by (simp add: nb Let_def split_def)
1.16 - hence ?case using Ia cp jnz by (simp add: Let_def split_def
1.17 - zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
1.18 + hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
1.19 moreover
1.20 {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
1.21 by (simp add: nb Let_def split_def)
1.22 hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
1.23 - by (simp add: Let_def split_def
1.24 - zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
1.25 + by (simp add: Let_def split_def) }
1.26 ultimately show ?case by blast
1.27 next
1.28 case (12 j a)
1.29 @@ -1026,7 +1024,7 @@
1.30 hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
1.31 moreover
1.32 {assume "?c=0" and "j\<noteq>0" hence ?case
1.33 - using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
1.34 + using zsplit0_I[OF spl, where x="i" and bs="bs"]
1.35 apply (auto simp add: Let_def split_def algebra_simps)
1.36 apply (cases "?r",auto)
1.37 apply (case_tac nat, auto)
1.38 @@ -1034,14 +1032,12 @@
1.39 moreover
1.40 {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
1.41 by (simp add: nb Let_def split_def)
1.42 - hence ?case using Ia cp jnz by (simp add: Let_def split_def
1.43 - zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
1.44 + hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
1.45 moreover
1.46 {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
1.47 by (simp add: nb Let_def split_def)
1.48 hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
1.49 - by (simp add: Let_def split_def
1.50 - zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
1.51 + by (simp add: Let_def split_def)}
1.52 ultimately show ?case by blast
1.53 qed auto
1.54
1.55 @@ -1210,7 +1206,7 @@
1.56 "mirror p = p"
1.57 (* Lemmas for the correctness of \<sigma>\<rho> *)
1.58 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
1.59 -by auto
1.60 +by simp
1.61
1.62 lemma minusinf_inf:
1.63 assumes linp: "iszlfm p"
1.64 @@ -1220,12 +1216,12 @@
1.65 using linp u
1.66 proof (induct p rule: minusinf.induct)
1.67 case (1 p q) thus ?case
1.68 - by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
1.69 + by auto (rule_tac x="min z za" in exI,simp)
1.70 next
1.71 case (2 p q) thus ?case
1.72 - by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
1.73 + by auto (rule_tac x="min z za" in exI,simp)
1.74 next
1.75 - case (3 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
1.76 + case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
1.77 fix a
1.78 from 3 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
1.79 proof(clarsimp)
1.80 @@ -1235,7 +1231,7 @@
1.81 qed
1.82 thus ?case by auto
1.83 next
1.84 - case (4 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
1.85 + case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
1.86 fix a
1.87 from 4 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
1.88 proof(clarsimp)
1.89 @@ -1245,7 +1241,7 @@
1.90 qed
1.91 thus ?case by auto
1.92 next
1.93 - case (5 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
1.94 + case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
1.95 fix a
1.96 from 5 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
1.97 proof(clarsimp)
1.98 @@ -1255,7 +1251,7 @@
1.99 qed
1.100 thus ?case by auto
1.101 next
1.102 - case (6 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
1.103 + case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
1.104 fix a
1.105 from 6 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
1.106 proof(clarsimp)
1.107 @@ -1265,7 +1261,7 @@
1.108 qed
1.109 thus ?case by auto
1.110 next
1.111 - case (7 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
1.112 + case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
1.113 fix a
1.114 from 7 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
1.115 proof(clarsimp)
1.116 @@ -1275,7 +1271,7 @@
1.117 qed
1.118 thus ?case by auto
1.119 next
1.120 - case (8 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
1.121 + case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
1.122 fix a
1.123 from 8 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
1.124 proof(clarsimp)
1.125 @@ -1595,15 +1591,15 @@
1.126 shows "?P (x - d)"
1.127 using lp u d dp nob p
1.128 proof(induct p rule: iszlfm.induct)
1.129 - case (5 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
1.130 + case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+
1.131 with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
1.132 show ?case by simp
1.133 next
1.134 - case (6 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
1.135 + case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+
1.136 with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
1.137 show ?case by simp
1.138 next
1.139 - case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
1.140 + case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp+
1.141 let ?e = "Inum (x # bs) e"
1.142 {assume "(x-d) +?e > 0" hence ?case using c1
1.143 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
1.144 @@ -1622,7 +1618,7 @@
1.145 ultimately show ?case by blast
1.146 next
1.147 case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
1.148 - using dvd1_eq1[where x="c"] by simp+
1.149 + by simp+
1.150 let ?e = "Inum (x # bs) e"
1.151 {assume "(x-d) +?e \<ge> 0" hence ?case using c1
1.152 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
1.153 @@ -1640,7 +1636,7 @@
1.154 with nob have ?case by simp }
1.155 ultimately show ?case by blast
1.156 next
1.157 - case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
1.158 + case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
1.159 let ?e = "Inum (x # bs) e"
1.160 let ?v="(Sub (C -1) e)"
1.161 have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
1.162 @@ -1648,7 +1644,7 @@
1.163 by simp (erule ballE[where x="1"],
1.164 simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
1.165 next
1.166 - case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
1.167 + case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
1.168 let ?e = "Inum (x # bs) e"
1.169 let ?v="Neg e"
1.170 have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
1.171 @@ -1662,7 +1658,7 @@
1.172 with prems(11) have ?case using dp by simp}
1.173 ultimately show ?case by blast
1.174 next
1.175 - case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
1.176 + case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
1.177 let ?e = "Inum (x # bs) e"
1.178 from prems have id: "j dvd d" by simp
1.179 from c1 have "?p x = (j dvd (x+ ?e))" by simp
1.180 @@ -1671,7 +1667,7 @@
1.181 finally show ?case
1.182 using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
1.183 next
1.184 - case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
1.185 + case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
1.186 let ?e = "Inum (x # bs) e"
1.187 from prems have id: "j dvd d" by simp
1.188 from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp