src/HOL/Presburger.thy
changeset 45425 7fee7d7abf2f
parent 44890 22f665a2e91c
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Presburger.thy	Wed Nov 09 15:18:39 2011 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Wed Nov 09 17:08:40 2011 +0100
     1.3 @@ -25,8 +25,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,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
     1.8 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
     1.9 +  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
    1.10 +  "\<exists>z.\<forall>(x::'b::{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,fastforce)+) simp_all
    1.13  
    1.14 @@ -41,8 +41,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,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
    1.19 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    1.20 +  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
    1.21 +  "\<exists>z.\<forall>(x::'b::{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,fastforce)+) simp_all
    1.24