src/HOL/Divides.thy
changeset 46552 5d33a3269029
parent 46551 866bce5442a3
child 46560 8e252a608765
     1.1 --- a/src/HOL/Divides.thy	Mon Feb 20 14:23:46 2012 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Feb 20 15:17:03 2012 +0100
     1.3 @@ -767,27 +767,23 @@
     1.4  subsubsection {* Quotient and Remainder *}
     1.5  
     1.6  lemma divmod_nat_rel_mult1_eq:
     1.7 -  "divmod_nat_rel b c (q, r) \<Longrightarrow> c > 0
     1.8 +  "divmod_nat_rel b c (q, r)
     1.9     \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
    1.10  by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
    1.11  
    1.12  lemma div_mult1_eq:
    1.13    "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
    1.14 -apply (cases "c = 0", simp)
    1.15 -apply (blast intro: divmod_nat_rel [THEN divmod_nat_rel_mult1_eq, THEN div_eq])
    1.16 -done
    1.17 +by (blast intro: divmod_nat_rel [THEN divmod_nat_rel_mult1_eq, THEN div_eq])
    1.18  
    1.19  lemma divmod_nat_rel_add1_eq:
    1.20 -  "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br) \<Longrightarrow>  c > 0
    1.21 +  "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
    1.22     \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
    1.23  by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
    1.24  
    1.25  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    1.26  lemma div_add1_eq:
    1.27    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    1.28 -apply (cases "c = 0", simp)
    1.29 -apply (blast intro: divmod_nat_rel_add1_eq [THEN div_eq] divmod_nat_rel)
    1.30 -done
    1.31 +by (blast intro: divmod_nat_rel_add1_eq [THEN div_eq] divmod_nat_rel)
    1.32  
    1.33  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
    1.34    apply (cut_tac m = q and n = c in mod_less_divisor)
    1.35 @@ -797,21 +793,15 @@
    1.36    done
    1.37  
    1.38  lemma divmod_nat_rel_mult2_eq:
    1.39 -  "divmod_nat_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
    1.40 +  "divmod_nat_rel a b (q, r)
    1.41     \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
    1.42  by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
    1.43  
    1.44  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
    1.45 -  apply (cases "b = 0", simp)
    1.46 -  apply (cases "c = 0", simp)
    1.47 -  apply (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_eq])
    1.48 -  done
    1.49 +by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_eq])
    1.50  
    1.51  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
    1.52 -  apply (cases "b = 0", simp)
    1.53 -  apply (cases "c = 0", simp)
    1.54 -  apply (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_eq])
    1.55 -  done
    1.56 +by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_eq])
    1.57  
    1.58  
    1.59  subsubsection {* Further Facts about Quotient and Remainder *}
    1.60 @@ -1307,7 +1297,7 @@
    1.61      auto)
    1.62  
    1.63  lemma unique_quotient:
    1.64 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r');  b \<noteq> 0 |]  
    1.65 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
    1.66        ==> q = q'"
    1.67  apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
    1.68  apply (blast intro: order_antisym
    1.69 @@ -1317,7 +1307,7 @@
    1.70  
    1.71  
    1.72  lemma unique_remainder:
    1.73 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r');  b \<noteq> 0 |]  
    1.74 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
    1.75        ==> r = r'"
    1.76  apply (subgoal_tac "q = q'")
    1.77   apply (simp add: divmod_int_rel_def)
    1.78 @@ -1477,10 +1467,14 @@
    1.79  apply (force simp add: divmod_int_rel_def linorder_neq_iff)
    1.80  done
    1.81  
    1.82 -lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r);  b \<noteq> 0 |] ==> a div b = q"
    1.83 +lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
    1.84 +apply (cases "b = 0")
    1.85 +apply (simp add: divmod_int_rel_def)
    1.86  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
    1.87  
    1.88 -lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r);  b \<noteq> 0 |] ==> a mod b = r"
    1.89 +lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
    1.90 +apply (cases "b = 0")
    1.91 +apply (simp add: divmod_int_rel_def)
    1.92  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
    1.93  
    1.94  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
    1.95 @@ -1595,7 +1589,7 @@
    1.96  apply (simp add: right_diff_distrib)
    1.97  done
    1.98  
    1.99 -lemma self_quotient: "[| divmod_int_rel a a (q, r);  a \<noteq> (0::int) |] ==> q = 1"
   1.100 +lemma self_quotient: "[| divmod_int_rel a a (q, r) |] ==> q = 1"
   1.101  apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)
   1.102  apply (rule order_antisym, safe, simp_all)
   1.103  apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
   1.104 @@ -1603,8 +1597,8 @@
   1.105  apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
   1.106  done
   1.107  
   1.108 -lemma self_remainder: "[| divmod_int_rel a a (q, r);  a \<noteq> (0::int) |] ==> r = 0"
   1.109 -apply (frule self_quotient, assumption)
   1.110 +lemma self_remainder: "[| divmod_int_rel a a (q, r) |] ==> r = 0"
   1.111 +apply (frule self_quotient)
   1.112  apply (simp add: divmod_int_rel_def)
   1.113  done
   1.114  
   1.115 @@ -1671,20 +1665,19 @@
   1.116  text {*Simplify expresions in which div and mod combine numerical constants*}
   1.117  
   1.118  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
   1.119 -  by (rule divmod_int_rel_div [of a b q r],
   1.120 -    simp add: divmod_int_rel_def, simp)
   1.121 +  by (rule divmod_int_rel_div [of a b q r]) (simp add: divmod_int_rel_def)
   1.122  
   1.123  lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   1.124    by (rule divmod_int_rel_div [of a b q r],
   1.125 -    simp add: divmod_int_rel_def, simp)
   1.126 +    simp add: divmod_int_rel_def)
   1.127  
   1.128  lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   1.129    by (rule divmod_int_rel_mod [of a b q r],
   1.130 -    simp add: divmod_int_rel_def, simp)
   1.131 +    simp add: divmod_int_rel_def)
   1.132  
   1.133  lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   1.134    by (rule divmod_int_rel_mod [of a b q r],
   1.135 -    simp add: divmod_int_rel_def, simp)
   1.136 +    simp add: divmod_int_rel_def)
   1.137  
   1.138  lemmas arithmetic_simps =
   1.139    arith_simps
   1.140 @@ -1847,7 +1840,7 @@
   1.141  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
   1.142  
   1.143  lemma zmult1_lemma:
   1.144 -     "[| divmod_int_rel b c (q, r);  c \<noteq> 0 |]  
   1.145 +     "[| divmod_int_rel b c (q, r) |]  
   1.146        ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
   1.147  by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib mult_ac)
   1.148  
   1.149 @@ -1869,7 +1862,7 @@
   1.150  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
   1.151  
   1.152  lemma zadd1_lemma:
   1.153 -     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br);  c \<noteq> 0 |]  
   1.154 +     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
   1.155        ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   1.156  by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib)
   1.157  
   1.158 @@ -1903,8 +1896,7 @@
   1.159        done
   1.160      moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
   1.161      ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
   1.162 -    moreover from  `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp
   1.163 -    ultimately show ?thesis by (rule divmod_int_rel_div)
   1.164 +    from this show ?thesis by (rule divmod_int_rel_div)
   1.165    qed
   1.166  qed auto
   1.167  
   1.168 @@ -1918,7 +1910,7 @@
   1.169    case False with assms posDivAlg_correct
   1.170      have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
   1.171      by simp
   1.172 -  from divmod_int_rel_div [OF this `l \<noteq> 0`] divmod_int_rel_mod [OF this `l \<noteq> 0`]
   1.173 +  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
   1.174    show ?thesis by simp
   1.175  qed
   1.176  
   1.177 @@ -1931,7 +1923,7 @@
   1.178    from assms negDivAlg_correct
   1.179      have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
   1.180      by simp
   1.181 -  from divmod_int_rel_div [OF this `l \<noteq> 0`] divmod_int_rel_mod [OF this `l \<noteq> 0`]
   1.182 +  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
   1.183    show ?thesis by simp
   1.184  qed
   1.185  
   1.186 @@ -1985,7 +1977,7 @@
   1.187  apply simp
   1.188  done
   1.189  
   1.190 -lemma zmult2_lemma: "[| divmod_int_rel a b (q, r);  b \<noteq> 0;  0 < c |]  
   1.191 +lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
   1.192        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   1.193  by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
   1.194                     zero_less_mult_iff right_distrib [symmetric]