src/HOL/Integ/Presburger.thy
changeset 17589 58eeffd73be1
parent 17378 105519771c67
child 18202 46af82efd311
     1.1 --- a/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -244,10 +244,10 @@
     1.4  text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
     1.5  
     1.6  lemma P_eqtrue: "(P=True) = P"
     1.7 -  by rules
     1.8 +  by iprover
     1.9  
    1.10  lemma P_eqfalse: "(P=False) = (~P)"
    1.11 -  by rules
    1.12 +  by iprover
    1.13  
    1.14  text {*
    1.15    \medskip Theorems for the generation of the bachwards direction of
    1.16 @@ -831,10 +831,10 @@
    1.17    by simp
    1.18  
    1.19  lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
    1.20 -  by rules
    1.21 +  by iprover
    1.22  
    1.23  lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
    1.24 -  by rules
    1.25 +  by iprover
    1.26  
    1.27  lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
    1.28  ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
    1.29 @@ -952,13 +952,13 @@
    1.30    apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
    1.31      nat_0_le cong add: conj_cong)
    1.32    apply (rule iffI)
    1.33 -  apply rules
    1.34 +  apply iprover
    1.35    apply (erule exE)
    1.36    apply (case_tac "x=0")
    1.37    apply (rule_tac x=0 in exI)
    1.38    apply simp
    1.39    apply (case_tac "0 \<le> k")
    1.40 -  apply rules
    1.41 +  apply iprover
    1.42    apply (simp add: linorder_not_le)
    1.43    apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
    1.44    apply assumption