src/HOL/Divides.thy
changeset 66886 960509bfd47e
parent 66837 6ba663ff2b1c
child 67083 6b2c0681ef28
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 19 17:16:13 2017 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Oct 20 07:46:10 2017 +0200
     1.3 @@ -501,15 +501,13 @@
     1.4  
     1.5  subsubsection \<open>General Properties of div and mod\<close>
     1.6  
     1.7 -lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
     1.8 -apply (rule div_int_unique)
     1.9 -apply (auto simp add: eucl_rel_int_iff)
    1.10 -done
    1.11 +lemma div_pos_pos_trivial [simp]:
    1.12 +  "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
    1.13 +  using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
    1.14  
    1.15 -lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
    1.16 -apply (rule div_int_unique)
    1.17 -apply (auto simp add: eucl_rel_int_iff)
    1.18 -done
    1.19 +lemma div_neg_neg_trivial [simp]:
    1.20 +  "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
    1.21 +  using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
    1.22  
    1.23  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
    1.24  apply (rule div_int_unique)
    1.25 @@ -522,15 +520,13 @@
    1.26  
    1.27  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
    1.28  
    1.29 -lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
    1.30 -apply (rule_tac q = 0 in mod_int_unique)
    1.31 -apply (auto simp add: eucl_rel_int_iff)
    1.32 -done
    1.33 +lemma mod_pos_pos_trivial [simp]:
    1.34 +  "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
    1.35 +  using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
    1.36  
    1.37 -lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
    1.38 -apply (rule_tac q = 0 in mod_int_unique)
    1.39 -apply (auto simp add: eucl_rel_int_iff)
    1.40 -done
    1.41 +lemma mod_neg_neg_trivial [simp]:
    1.42 +  "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
    1.43 +  using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
    1.44  
    1.45  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
    1.46  apply (rule_tac q = "-1" in mod_int_unique)
    1.47 @@ -775,38 +771,22 @@
    1.48  lemma split_pos_lemma:
    1.49   "0<k ==>
    1.50      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
    1.51 -apply (rule iffI, clarify)
    1.52 - apply (erule_tac P="P x y" for x y in rev_mp)
    1.53 - apply (subst mod_add_eq [symmetric])
    1.54 - apply (subst zdiv_zadd1_eq)
    1.55 - apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
    1.56 -txt\<open>converse direction\<close>
    1.57 -apply (drule_tac x = "n div k" in spec)
    1.58 -apply (drule_tac x = "n mod k" in spec, simp)
    1.59 -done
    1.60 +  by auto
    1.61  
    1.62  lemma split_neg_lemma:
    1.63   "k<0 ==>
    1.64      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
    1.65 -apply (rule iffI, clarify)
    1.66 - apply (erule_tac P="P x y" for x y in rev_mp)
    1.67 - apply (subst mod_add_eq [symmetric])
    1.68 - apply (subst zdiv_zadd1_eq)
    1.69 - apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
    1.70 -txt\<open>converse direction\<close>
    1.71 -apply (drule_tac x = "n div k" in spec)
    1.72 -apply (drule_tac x = "n mod k" in spec, simp)
    1.73 -done
    1.74 +  by auto
    1.75  
    1.76  lemma split_zdiv:
    1.77   "P(n div k :: int) =
    1.78    ((k = 0 --> P 0) &
    1.79     (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
    1.80     (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
    1.81 -apply (case_tac "k=0", simp)
    1.82 +  apply (cases "k = 0")
    1.83 +  apply simp
    1.84  apply (simp only: linorder_neq_iff)
    1.85 -apply (erule disjE)
    1.86 - apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
    1.87 + apply (auto simp add: split_pos_lemma [of concl: "%x y. P x"]
    1.88                        split_neg_lemma [of concl: "%x y. P x"])
    1.89  done
    1.90  
    1.91 @@ -897,14 +877,17 @@
    1.92    by (rule pos_zmod_mult_2, simp)
    1.93  
    1.94  lemma zdiv_eq_0_iff:
    1.95 - "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")
    1.96 +  "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
    1.97 +  for i k :: int
    1.98  proof
    1.99    assume ?L
   1.100 -  have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
   1.101 -  with \<open>?L\<close> show ?R by blast
   1.102 +  moreover have "?L \<longrightarrow> ?R"
   1.103 +    by (rule split_zdiv [THEN iffD2]) simp
   1.104 +  ultimately show ?R
   1.105 +    by blast
   1.106  next
   1.107 -  assume ?R thus ?L
   1.108 -    by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
   1.109 +  assume ?R then show ?L
   1.110 +    by auto
   1.111  qed
   1.112  
   1.113  lemma zmod_trival_iff:
   1.114 @@ -1004,7 +987,7 @@
   1.115  
   1.116  instance
   1.117    by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
   1.118 -    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
   1.119 +    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
   1.120  
   1.121  end
   1.122