src/HOL/Presburger.thy
changeset 35050 9f841f20dca6
parent 33318 ddd97d9dfbfb
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Presburger.thy	Mon Feb 08 17:12:32 2010 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Mon Feb 08 17:12:38 2010 +0100
     1.3 @@ -30,8 +30,8 @@
     1.4    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
     1.5    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
     1.6    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
     1.7 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (d dvd x + s) = (d dvd x + s)"
     1.8 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
     1.9 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
    1.10 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    1.11    "\<exists>z.\<forall>x<z. F = F"
    1.12    by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
    1.13  
    1.14 @@ -46,8 +46,8 @@
    1.15    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
    1.16    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
    1.17    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
    1.18 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (d dvd x + s) = (d dvd x + s)"
    1.19 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Ring_and_Field.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    1.20 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
    1.21 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    1.22    "\<exists>z.\<forall>x>z. F = F"
    1.23    by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
    1.24  
    1.25 @@ -56,8 +56,8 @@
    1.26      \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
    1.27    "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    1.28      \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
    1.29 -  "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
    1.30 -  "(d::'a::{comm_ring,Ring_and_Field.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    1.31 +  "(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
    1.32 +  "(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    1.33    "\<forall>x k. F = F"
    1.34  apply (auto elim!: dvdE simp add: algebra_simps)
    1.35  unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
    1.36 @@ -243,7 +243,7 @@
    1.37    {fix x
    1.38      have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
    1.39      also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"]
    1.40 -      by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
    1.41 +      by (simp add: algebra_simps)
    1.42      ultimately have "P x \<longrightarrow> P(x - (i + 1) * d)" by blast}
    1.43    thus ?case ..
    1.44  qed
    1.45 @@ -360,7 +360,7 @@
    1.46  apply(fastsimp)
    1.47  done
    1.48  
    1.49 -theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Ring_and_Field.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
    1.50 +theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Rings.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
    1.51    apply (rule eq_reflection [symmetric])
    1.52    apply (rule iffI)
    1.53    defer