--- a/src/HOL/ex/Reflected_Presburger.thy Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/ex/Reflected_Presburger.thy Wed Jan 28 16:29:16 2009 +0100
@@ -437,7 +437,7 @@
apply (induct t s rule: numadd.induct, simp_all add: Let_def)
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2")
- apply(simp_all add: ring_simps)
+ apply(simp_all add: algebra_simps)
apply(simp add: left_distrib[symmetric])
done
@@ -452,7 +452,7 @@
| "nummul i t = Mul i t"
lemma nummul: "\<And> i. Inum bs (nummul i t) = Inum bs (Mul i t)"
-by (induct t rule: nummul.induct, auto simp add: ring_simps numadd)
+by (induct t rule: nummul.induct, auto simp add: algebra_simps numadd)
lemma nummul_nb: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
by (induct t rule: nummul.induct, auto simp add: numadd_nb)
@@ -912,7 +912,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done
@@ -925,7 +925,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done
@@ -938,7 +938,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done
@@ -951,7 +951,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done
@@ -964,7 +964,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done
@@ -977,7 +977,7 @@
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb show ?case
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done
@@ -996,7 +996,7 @@
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done}
@@ -1027,7 +1027,7 @@
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
- apply (auto simp add: Let_def split_def ring_simps)
+ apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
done}
@@ -1301,9 +1301,9 @@
(is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
- by (simp add: ring_simps di_def)
+ by (simp add: algebra_simps di_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
next
@@ -1312,7 +1312,7 @@
hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
- hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
+ hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
by blast
thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
@@ -1328,9 +1328,9 @@
(is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
- by (simp add: ring_simps di_def)
+ by (simp add: algebra_simps di_def)
hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
next
@@ -1339,7 +1339,7 @@
hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
- hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
+ hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
by blast
thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
@@ -1363,7 +1363,7 @@
by (simp only: zdvd_zminus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
by simp
@@ -1375,7 +1375,7 @@
by (simp only: zdvd_zminus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
by simp
@@ -1443,7 +1443,7 @@
hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
by simp
- also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: ring_simps)
+ also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: algebra_simps)
also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
@@ -1461,7 +1461,7 @@
hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: ring_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: algebra_simps)
also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
@@ -1479,7 +1479,7 @@
hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: ring_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: algebra_simps)
also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
@@ -1498,7 +1498,7 @@
((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
by simp
also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" using ldcp
zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp
finally show ?case using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]
@@ -1517,7 +1517,7 @@
hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: ring_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: algebra_simps)
also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
@@ -1535,7 +1535,7 @@
hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)"
by simp
- also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: ring_simps)
+ also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: algebra_simps)
also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)"
using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
@@ -1551,7 +1551,7 @@
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
- also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
+ also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps)
also fix k have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
@@ -1568,7 +1568,7 @@
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
- also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
+ also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps)
also fix k have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
@@ -1617,7 +1617,7 @@
hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)"
- by (simp add: ring_simps)
+ by (simp add: algebra_simps)
with nob have ?case by auto}
ultimately show ?case by blast
next
@@ -1636,7 +1636,7 @@
from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
- hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: ring_simps)
+ hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps)
with nob have ?case by simp }
ultimately show ?case by blast
next
@@ -1646,7 +1646,7 @@
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
by simp (erule ballE[where x="1"],
- simp_all add:ring_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
+ simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
next
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+
let ?e = "Inum (x # bs) e"