src/HOL/Integ/IntDiv.thy
changeset 13524 604d0f3622d6
parent 13517 42efec18f5b2
child 13601 fd3e3d6b37b2
     1.1 --- a/src/HOL/Integ/IntDiv.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/Integ/IntDiv.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -352,12 +352,12 @@
     1.4  
     1.5  (*** division of a number by itself ***)
     1.6  
     1.7 -lemma lemma1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
     1.8 +lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
     1.9  apply (subgoal_tac "0 < a*q")
    1.10   apply (simp add: int_0_less_mult_iff, arith)
    1.11  done
    1.12  
    1.13 -lemma lemma2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
    1.14 +lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
    1.15  apply (subgoal_tac "0 <= a* (1-q) ")
    1.16   apply (simp add: int_0_le_mult_iff)
    1.17  apply (simp add: zdiff_zmult_distrib2)
    1.18 @@ -366,9 +366,9 @@
    1.19  lemma self_quotient: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> q = 1"
    1.20  apply (simp add: split_ifs quorem_def linorder_neq_iff)
    1.21  apply (rule order_antisym, auto)
    1.22 -apply (rule_tac [3] a = "-a" and r = "-r" in lemma1)
    1.23 -apply (rule_tac a = "-a" and r = "-r" in lemma2)
    1.24 -apply (force intro: lemma1 lemma2 simp add: zadd_commute zmult_zminus)+
    1.25 +apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
    1.26 +apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
    1.27 +apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: zadd_commute zmult_zminus)+
    1.28  done
    1.29  
    1.30  lemma self_remainder: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> r = 0"
    1.31 @@ -699,7 +699,7 @@
    1.32  
    1.33  (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
    1.34  
    1.35 -lemma lemma1: "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r"
    1.36 +lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r"
    1.37  apply (subgoal_tac "b * (c - q mod c) < r * 1")
    1.38  apply (simp add: zdiff_zmult_distrib2)
    1.39  apply (rule order_le_less_trans)
    1.40 @@ -709,19 +709,19 @@
    1.41                        add1_zle_eq pos_mod_bound)
    1.42  done
    1.43  
    1.44 -lemma lemma2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
    1.45 +lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
    1.46  apply (subgoal_tac "b * (q mod c) <= 0")
    1.47   apply arith
    1.48  apply (simp add: zmult_le_0_iff pos_mod_sign)
    1.49  done
    1.50  
    1.51 -lemma lemma3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
    1.52 +lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
    1.53  apply (subgoal_tac "0 <= b * (q mod c) ")
    1.54  apply arith
    1.55  apply (simp add: int_0_le_mult_iff pos_mod_sign)
    1.56  done
    1.57  
    1.58 -lemma lemma4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
    1.59 +lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
    1.60  apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
    1.61  apply (simp add: zdiff_zmult_distrib2)
    1.62  apply (rule order_less_le_trans)
    1.63 @@ -735,7 +735,7 @@
    1.64        ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
    1.65  by (auto simp add: zmult_ac quorem_def linorder_neq_iff
    1.66                     int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
    1.67 -                   lemma1 lemma2 lemma3 lemma4)
    1.68 +                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
    1.69  
    1.70  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
    1.71  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
    1.72 @@ -751,17 +751,17 @@
    1.73  
    1.74  (*** Cancellation of common factors in div ***)
    1.75  
    1.76 -lemma lemma1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
    1.77 +lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
    1.78  by (subst zdiv_zmult2_eq, auto)
    1.79  
    1.80 -lemma lemma2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
    1.81 +lemma zdiv_zmult_zmult1_aux2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
    1.82  apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
    1.83 -apply (rule_tac [2] lemma1, auto)
    1.84 +apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
    1.85  done
    1.86  
    1.87  lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b"
    1.88  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
    1.89 -apply (auto simp add: linorder_neq_iff lemma1 lemma2)
    1.90 +apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
    1.91  done
    1.92  
    1.93  lemma zdiv_zmult_zmult2: "c ~= (0::int) ==> (a*c) div (b*c) = a div b"
    1.94 @@ -773,18 +773,18 @@
    1.95  
    1.96  (*** Distribution of factors over mod ***)
    1.97  
    1.98 -lemma lemma1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
    1.99 +lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
   1.100  by (subst zmod_zmult2_eq, auto)
   1.101  
   1.102 -lemma lemma2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
   1.103 +lemma zmod_zmult_zmult1_aux2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
   1.104  apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
   1.105 -apply (rule_tac [2] lemma1, auto)
   1.106 +apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
   1.107  done
   1.108  
   1.109  lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
   1.110  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
   1.111  apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
   1.112 -apply (auto simp add: linorder_neq_iff lemma1 lemma2)
   1.113 +apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
   1.114  done
   1.115  
   1.116  lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"