src/HOL/Integ/Presburger.thy
changeset 14271 8ed6989228bb
parent 14139 ca3dd7ed5ac5
child 14353 79f9fbef9106
     1.1 --- a/src/HOL/Integ/Presburger.thy	Tue Dec 02 11:48:15 2003 +0100
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Wed Dec 03 10:49:34 2003 +0100
     1.3 @@ -395,7 +395,7 @@
     1.4    apply(clarsimp)
     1.5    apply(rename_tac n m)
     1.6    apply(rule_tac x = "m - n*k" in exI)
     1.7 -  apply(simp add:int_distrib zmult_ac)
     1.8 +  apply(simp add:int_distrib mult_ac)
     1.9    done
    1.10  
    1.11  lemma  not_dvd_modd_pinf: "((d::int) dvd d1) ==>
    1.12 @@ -405,11 +405,11 @@
    1.13    apply(clarsimp)
    1.14    apply(rename_tac n m)
    1.15    apply(erule_tac x = "m - n*k" in allE)
    1.16 -  apply(simp add:int_distrib zmult_ac)
    1.17 +  apply(simp add:int_distrib mult_ac)
    1.18    apply(clarsimp)
    1.19    apply(rename_tac n m)
    1.20    apply(erule_tac x = "m + n*k" in allE)
    1.21 -  apply(simp add:int_distrib zmult_ac)
    1.22 +  apply(simp add:int_distrib mult_ac)
    1.23    done
    1.24  
    1.25  (*=============================================================================*)
    1.26 @@ -462,7 +462,7 @@
    1.27  apply(clarsimp)
    1.28  apply(rename_tac n m)
    1.29  apply(rule_tac x = "m + n*k" in exI)
    1.30 -apply(simp add:int_distrib zmult_ac)
    1.31 +apply(simp add:int_distrib mult_ac)
    1.32  done
    1.33  
    1.34  
    1.35 @@ -473,11 +473,11 @@
    1.36  apply(clarsimp)
    1.37  apply(rename_tac n m)
    1.38  apply(erule_tac x = "m + n*k" in allE)
    1.39 -apply(simp add:int_distrib zmult_ac)
    1.40 +apply(simp add:int_distrib mult_ac)
    1.41  apply(clarsimp)
    1.42  apply(rename_tac n m)
    1.43  apply(erule_tac x = "m - n*k" in allE)
    1.44 -apply(simp add:int_distrib zmult_ac)
    1.45 +apply(simp add:int_distrib mult_ac)
    1.46  done
    1.47  
    1.48  
    1.49 @@ -626,7 +626,7 @@
    1.50    assume ?LHS
    1.51    then obtain x where P: "P x" ..
    1.52    have "x mod d = x - (x div d)*d"
    1.53 -    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
    1.54 +    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
    1.55    hence Pmod: "P x = P(x mod d)" using modd by simp
    1.56    show ?RHS
    1.57    proof (cases)
    1.58 @@ -661,7 +661,7 @@
    1.59    assume ?LHS
    1.60    then obtain x where P: "P x" ..
    1.61    have "x mod d = x + (-(x div d))*d"
    1.62 -    by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
    1.63 +    by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
    1.64    hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
    1.65    show ?RHS
    1.66    proof (cases)
    1.67 @@ -702,7 +702,7 @@
    1.68      have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
    1.69      also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
    1.70        using minus[THEN spec, of "x - i * d"]
    1.71 -      by (simp add:int_distrib zdiff_zdiff_eq[symmetric])
    1.72 +      by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric])
    1.73      ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
    1.74    qed
    1.75  qed
    1.76 @@ -864,12 +864,12 @@
    1.77      apply(drule_tac f = "op * k" in arg_cong)
    1.78      apply(simp only:int_distrib)
    1.79      apply(rule_tac x = "d" in exI)
    1.80 -    apply(simp only:zmult_ac)
    1.81 +    apply(simp only:mult_ac)
    1.82      done
    1.83  next
    1.84    assume ?Q
    1.85    then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
    1.86 -  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib zmult_ac)
    1.87 +  hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
    1.88    hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
    1.89    hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
    1.90    thus ?P by(simp add:dvd_def)
    1.91 @@ -879,10 +879,10 @@
    1.92  shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
    1.93  proof
    1.94    assume P: ?P
    1.95 -  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib zmult_ac)
    1.96 +  show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
    1.97  next
    1.98    assume ?Q
    1.99 -  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib zmult_ac)
   1.100 +  hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
   1.101    with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
   1.102    thus ?P by(simp)
   1.103  qed
   1.104 @@ -896,7 +896,7 @@
   1.105      done
   1.106  next
   1.107    assume ?Q
   1.108 -  hence "m * k = (c*n + t) * k" by(simp add:int_distrib zmult_ac)
   1.109 +  hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
   1.110    hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
   1.111    thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
   1.112  qed
   1.113 @@ -904,9 +904,9 @@
   1.114  lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
   1.115  proof -
   1.116    have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
   1.117 -  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib zmult_ac)
   1.118 +  also have  "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
   1.119    also have "0<(-1*c)*n + (-t+1) = (0 < (k*(-1*c)*n) + (k*(-t+1)))" by(rule ac_lt_eq[of _ 0,OF gr0,simplified])
   1.120 -  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib zmult_ac)
   1.121 +  also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
   1.122    finally show ?thesis .
   1.123  qed
   1.124  
   1.125 @@ -963,7 +963,7 @@
   1.126    apply (simp add: linorder_not_le)
   1.127    apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
   1.128    apply assumption
   1.129 -  apply (simp add: zmult_ac)
   1.130 +  apply (simp add: mult_ac)
   1.131    done
   1.132  
   1.133  theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"