src/HOL/Presburger.thy
changeset 44890 22f665a2e91c
parent 44766 d4d33a4d7548
child 45425 7fee7d7abf2f
     1.1 --- a/src/HOL/Presburger.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
     1.5    "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
     1.6    "\<exists>z.\<forall>x<z. F = F"
     1.7 -  by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
     1.8 +  by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastforce)+) simp_all
     1.9  
    1.10  lemma pinf:
    1.11    "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 
    1.12 @@ -44,7 +44,7 @@
    1.13    "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
    1.14    "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    1.15    "\<exists>z.\<forall>x>z. F = F"
    1.16 -  by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
    1.17 +  by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastforce)+) simp_all
    1.18  
    1.19  lemma inf_period:
    1.20    "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    1.21 @@ -342,7 +342,7 @@
    1.22  
    1.23  lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
    1.24  apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
    1.25 -apply(fastsimp)
    1.26 +apply(fastforce)
    1.27  done
    1.28  
    1.29  theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Rings.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"