src/HOL/Presburger.thy
 changeset 27540 dc38e79f5a1c parent 26508 4cd7c4f936bb child 27651 16a26996c30e
```     1.1 --- a/src/HOL/Presburger.thy	Fri Jul 11 00:35:19 2008 +0200
1.2 +++ b/src/HOL/Presburger.thy	Fri Jul 11 09:02:22 2008 +0200
1.3 @@ -31,8 +31,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,Divides.div})<z. (d dvd x + s) = (d dvd x + s)"
1.8 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
1.9 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (d dvd x + s) = (d dvd x + s)"
1.10 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.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 @@ -47,8 +47,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,Divides.div})>z. (d dvd x + s) = (d dvd x + s)"
1.19 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
1.20 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (d dvd x + s) = (d dvd x + s)"
1.21 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.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 @@ -57,8 +57,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,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
1.30 -  "(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
1.31 +  "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
1.32 +  "(d::'a::{comm_ring,Divides.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  by simp_all
1.35    (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
1.36 @@ -360,7 +360,7 @@
1.37  apply(fastsimp)
1.38  done
1.39
1.40 -theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.div}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
1.41 +theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
1.42    apply (rule eq_reflection[symmetric])
1.43    apply (rule iffI)
1.44    defer
```