added lemmas and tuned proofs
authorhaftmann
Fri Oct 20 07:46:10 2017 +0200 (20 months ago)
changeset 66886960509bfd47e
parent 66885 d3d508b23d1d
child 66887 72b78ee82f7b
added lemmas and tuned proofs
src/HOL/Code_Numeral.thy
src/HOL/Computational_Algebra/Normalized_Fraction.thy
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/Int.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Oct 19 17:16:13 2017 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Oct 20 07:46:10 2017 +0200
     1.3 @@ -578,16 +578,15 @@
     1.4         l'' = l' + l'
     1.5       in if j = 0 then l'' else l'' + 1)"
     1.6  proof -
     1.7 -  obtain j where "k = integer_of_int j"
     1.8 +  obtain j where k: "k = integer_of_int j"
     1.9    proof
    1.10      show "k = integer_of_int (int_of_integer k)" by simp
    1.11    qed
    1.12 -  moreover have "2 * (j div 2) = j - j mod 2"
    1.13 -    by (simp add: minus_mod_eq_mult_div [symmetric] mult.commute)
    1.14 -  ultimately show ?thesis
    1.15 -    by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
    1.16 -      nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
    1.17 -      (auto simp add: mult_2 [symmetric])
    1.18 +  have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)" if "j \<ge> 0"
    1.19 +    using that by transfer (simp add: nat_mod_distrib)
    1.20 +  from k show ?thesis
    1.21 +    by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric]
    1.22 +      minus_mod_eq_mult_div [symmetric] *)
    1.23  qed
    1.24  
    1.25  lemma int_of_integer_code [code]:
     2.1 --- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Thu Oct 19 17:16:13 2017 +0100
     2.2 +++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Oct 20 07:46:10 2017 +0200
     2.3 @@ -239,7 +239,6 @@
     2.4    
     2.5  lemma normalize_quot_eq_0_iff [simp]: "fst (normalize_quot x) = 0 \<longleftrightarrow> fst x = 0 \<or> snd x = 0"
     2.6    by (auto simp: normalize_quot_def case_prod_unfold Let_def div_mult_unit2 dvd_div_eq_0_iff)
     2.7 -  find_theorems "_ div _ = 0"
     2.8    
     2.9  lemma fst_quot_of_fract_0_imp: "fst (quot_of_fract x) = 0 \<Longrightarrow> snd (quot_of_fract x) = 1"
    2.10    by transfer auto
     3.1 --- a/src/HOL/Divides.thy	Thu Oct 19 17:16:13 2017 +0100
     3.2 +++ b/src/HOL/Divides.thy	Fri Oct 20 07:46:10 2017 +0200
     3.3 @@ -501,15 +501,13 @@
     3.4  
     3.5  subsubsection \<open>General Properties of div and mod\<close>
     3.6  
     3.7 -lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
     3.8 -apply (rule div_int_unique)
     3.9 -apply (auto simp add: eucl_rel_int_iff)
    3.10 -done
    3.11 +lemma div_pos_pos_trivial [simp]:
    3.12 +  "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
    3.13 +  using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
    3.14  
    3.15 -lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
    3.16 -apply (rule div_int_unique)
    3.17 -apply (auto simp add: eucl_rel_int_iff)
    3.18 -done
    3.19 +lemma div_neg_neg_trivial [simp]:
    3.20 +  "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
    3.21 +  using that by (auto intro!: div_int_unique [of _ _ _ k] simp add: eucl_rel_int_iff)
    3.22  
    3.23  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
    3.24  apply (rule div_int_unique)
    3.25 @@ -522,15 +520,13 @@
    3.26  
    3.27  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
    3.28  
    3.29 -lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
    3.30 -apply (rule_tac q = 0 in mod_int_unique)
    3.31 -apply (auto simp add: eucl_rel_int_iff)
    3.32 -done
    3.33 +lemma mod_pos_pos_trivial [simp]:
    3.34 +  "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
    3.35 +  using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
    3.36  
    3.37 -lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
    3.38 -apply (rule_tac q = 0 in mod_int_unique)
    3.39 -apply (auto simp add: eucl_rel_int_iff)
    3.40 -done
    3.41 +lemma mod_neg_neg_trivial [simp]:
    3.42 +  "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
    3.43 +  using that by (auto intro!: mod_int_unique [of _ _ 0] simp add: eucl_rel_int_iff)
    3.44  
    3.45  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
    3.46  apply (rule_tac q = "-1" in mod_int_unique)
    3.47 @@ -775,38 +771,22 @@
    3.48  lemma split_pos_lemma:
    3.49   "0<k ==>
    3.50      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
    3.51 -apply (rule iffI, clarify)
    3.52 - apply (erule_tac P="P x y" for x y in rev_mp)
    3.53 - apply (subst mod_add_eq [symmetric])
    3.54 - apply (subst zdiv_zadd1_eq)
    3.55 - apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
    3.56 -txt\<open>converse direction\<close>
    3.57 -apply (drule_tac x = "n div k" in spec)
    3.58 -apply (drule_tac x = "n mod k" in spec, simp)
    3.59 -done
    3.60 +  by auto
    3.61  
    3.62  lemma split_neg_lemma:
    3.63   "k<0 ==>
    3.64      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
    3.65 -apply (rule iffI, clarify)
    3.66 - apply (erule_tac P="P x y" for x y in rev_mp)
    3.67 - apply (subst mod_add_eq [symmetric])
    3.68 - apply (subst zdiv_zadd1_eq)
    3.69 - apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
    3.70 -txt\<open>converse direction\<close>
    3.71 -apply (drule_tac x = "n div k" in spec)
    3.72 -apply (drule_tac x = "n mod k" in spec, simp)
    3.73 -done
    3.74 +  by auto
    3.75  
    3.76  lemma split_zdiv:
    3.77   "P(n div k :: int) =
    3.78    ((k = 0 --> P 0) &
    3.79     (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
    3.80     (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
    3.81 -apply (case_tac "k=0", simp)
    3.82 +  apply (cases "k = 0")
    3.83 +  apply simp
    3.84  apply (simp only: linorder_neq_iff)
    3.85 -apply (erule disjE)
    3.86 - apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
    3.87 + apply (auto simp add: split_pos_lemma [of concl: "%x y. P x"]
    3.88                        split_neg_lemma [of concl: "%x y. P x"])
    3.89  done
    3.90  
    3.91 @@ -897,14 +877,17 @@
    3.92    by (rule pos_zmod_mult_2, simp)
    3.93  
    3.94  lemma zdiv_eq_0_iff:
    3.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")
    3.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")
    3.97 +  for i k :: int
    3.98  proof
    3.99    assume ?L
   3.100 -  have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
   3.101 -  with \<open>?L\<close> show ?R by blast
   3.102 +  moreover have "?L \<longrightarrow> ?R"
   3.103 +    by (rule split_zdiv [THEN iffD2]) simp
   3.104 +  ultimately show ?R
   3.105 +    by blast
   3.106  next
   3.107 -  assume ?R thus ?L
   3.108 -    by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
   3.109 +  assume ?R then show ?L
   3.110 +    by auto
   3.111  qed
   3.112  
   3.113  lemma zmod_trival_iff:
   3.114 @@ -1004,7 +987,7 @@
   3.115  
   3.116  instance
   3.117    by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
   3.118 -    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
   3.119 +    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
   3.120  
   3.121  end
   3.122  
     4.1 --- a/src/HOL/Euclidean_Division.thy	Thu Oct 19 17:16:13 2017 +0100
     4.2 +++ b/src/HOL/Euclidean_Division.thy	Fri Oct 20 07:46:10 2017 +0200
     4.3 @@ -128,6 +128,18 @@
     4.4  end
     4.5  
     4.6  class euclidean_ring = idom_modulo + euclidean_semiring
     4.7 +begin
     4.8 +
     4.9 +lemma dvd_diff_commute:
    4.10 +  "a dvd c - b \<longleftrightarrow> a dvd b - c"
    4.11 +proof -
    4.12 +  have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"
    4.13 +    by (subst dvd_mult_unit_iff) simp_all
    4.14 +  then show ?thesis
    4.15 +    by simp
    4.16 +qed
    4.17 + 
    4.18 +end
    4.19  
    4.20  
    4.21  subsection \<open>Euclidean (semi)rings with cancel rules\<close>
    4.22 @@ -711,6 +723,21 @@
    4.23      by simp
    4.24  qed
    4.25  
    4.26 +lemma div_eq_0_iff:
    4.27 +  "a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0" (is "_ \<longleftrightarrow> ?P")
    4.28 +  if "division_segment a = division_segment b"
    4.29 +proof
    4.30 +  assume ?P
    4.31 +  with that show "a div b = 0"
    4.32 +    by (cases "b = 0") (auto intro: div_eqI)
    4.33 +next
    4.34 +  assume "a div b = 0"
    4.35 +  then have "a mod b = a"
    4.36 +    using div_mult_mod_eq [of a b] by simp
    4.37 +  with mod_size_less [of b a] show ?P
    4.38 +    by auto
    4.39 +qed
    4.40 +
    4.41  end
    4.42  
    4.43  class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
    4.44 @@ -954,7 +981,7 @@
    4.45  
    4.46  lemma div_eq_0_iff:
    4.47    "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
    4.48 -  by (simp add: div_if)
    4.49 +  by (simp add: div_eq_0_iff)
    4.50  
    4.51  lemma div_greater_zero_iff:
    4.52    "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
     5.1 --- a/src/HOL/Int.thy	Thu Oct 19 17:16:13 2017 +0100
     5.2 +++ b/src/HOL/Int.thy	Fri Oct 20 07:46:10 2017 +0200
     5.3 @@ -552,6 +552,10 @@
     5.4  lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
     5.5    by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
     5.6  
     5.7 +lemma nat_abs_triangle_ineq:
     5.8 +  "nat \<bar>k + l\<bar> \<le> nat \<bar>k\<bar> + nat \<bar>l\<bar>"
     5.9 +  by (simp add: nat_add_distrib [symmetric] nat_le_eq_zle abs_triangle_ineq)
    5.10 +
    5.11  lemma nat_of_bool [simp]:
    5.12    "nat (of_bool P) = of_bool P"
    5.13    by auto
     6.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Oct 19 17:16:13 2017 +0100
     6.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Oct 20 07:46:10 2017 +0200
     6.3 @@ -125,7 +125,6 @@
     6.4  lemma Rep_mod: "Rep x mod n = Rep x"
     6.5  apply (rule_tac x=x in type_definition.Abs_cases [OF type])
     6.6  apply (simp add: type_definition.Abs_inverse [OF type])
     6.7 -apply (simp add: mod_pos_pos_trivial)
     6.8  done
     6.9  
    6.10  lemmas Rep_simps =
     7.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Thu Oct 19 17:16:13 2017 +0100
     7.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Oct 20 07:46:10 2017 +0200
     7.3 @@ -276,16 +276,7 @@
     7.4  
     7.5  lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
     7.6    for a :: int
     7.7 -  apply clarsimp
     7.8 -  apply safe
     7.9 -   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
    7.10 -   apply (drule le_iff_add [THEN iffD1])
    7.11 -   apply (force simp: power_add)
    7.12 -  apply (rule mod_pos_pos_trivial)
    7.13 -   apply (simp)
    7.14 -  apply (rule power_strict_increasing)
    7.15 -   apply auto
    7.16 -  done
    7.17 +  by (simp add: mod_eq_0_iff le_imp_power_dvd)
    7.18  
    7.19  lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
    7.20    for a b c d :: nat