src/HOL/Nat.thy
changeset 60562 24af00b010cf
parent 60427 b4b672f09270
child 60636 ee18efe9b246
     1.1 --- a/src/HOL/Nat.thy	Mon Jun 22 23:19:48 2015 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Jun 23 16:55:28 2015 +0100
     1.3 @@ -282,10 +282,25 @@
     1.4    show "n * m = m * n" by (induct n) simp_all
     1.5    show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
     1.6    show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
     1.7 +next
     1.8 +  fix k m n :: nat
     1.9 +  show "k * ((m::nat) - n) = (k * m) - (k * n)"
    1.10 +    by (induct m n rule: diff_induct) simp_all
    1.11  qed
    1.12  
    1.13  end
    1.14  
    1.15 +text {* Difference distributes over multiplication *}
    1.16 +
    1.17 +lemma diff_mult_distrib:
    1.18 +  "((m::nat) - n) * k = (m * k) - (n * k)"
    1.19 +  by (fact left_diff_distrib')
    1.20 +
    1.21 +lemma diff_mult_distrib2:
    1.22 +  "k * ((m::nat) - n) = (k * m) - (k * n)"
    1.23 +  by (fact right_diff_distrib')
    1.24 +
    1.25 +
    1.26  subsubsection {* Addition *}
    1.27  
    1.28  lemma nat_add_left_cancel:
    1.29 @@ -364,24 +379,6 @@
    1.30  lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
    1.31    unfolding One_nat_def by simp
    1.32  
    1.33 -text {* Difference distributes over multiplication *}
    1.34 -
    1.35 -instance nat :: comm_semiring_1_diff_distrib
    1.36 -proof
    1.37 -  fix k m n :: nat
    1.38 -  show "k * ((m::nat) - n) = (k * m) - (k * n)"
    1.39 -    by (induct m n rule: diff_induct) simp_all
    1.40 -qed
    1.41 -
    1.42 -lemma diff_mult_distrib:
    1.43 -  "((m::nat) - n) * k = (m * k) - (n * k)"
    1.44 -  by (fact left_diff_distrib')
    1.45 -  
    1.46 -lemma diff_mult_distrib2:
    1.47 -  "k * ((m::nat) - n) = (k * m) - (k * n)"
    1.48 -  by (fact right_diff_distrib')
    1.49 -
    1.50 -
    1.51  subsubsection {* Multiplication *}
    1.52  
    1.53  lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
    1.54 @@ -488,7 +485,7 @@
    1.55  instance
    1.56  proof
    1.57    fix n m :: nat
    1.58 -  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 
    1.59 +  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
    1.60    proof (induct n arbitrary: m)
    1.61      case 0 then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
    1.62    next
    1.63 @@ -550,7 +547,7 @@
    1.64    by (rule order_less_irrefl)
    1.65  
    1.66  lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
    1.67 -  by (rule not_sym) (rule less_imp_neq) 
    1.68 +  by (rule not_sym) (rule less_imp_neq)
    1.69  
    1.70  lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
    1.71    by (rule less_imp_neq)
    1.72 @@ -594,7 +591,7 @@
    1.73  subsubsection {* Inductive (?) properties *}
    1.74  
    1.75  lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
    1.76 -  unfolding less_eq_Suc_le [of m] le_less by simp 
    1.77 +  unfolding less_eq_Suc_le [of m] le_less by simp
    1.78  
    1.79  lemma lessE:
    1.80    assumes major: "i < k"
    1.81 @@ -783,6 +780,12 @@
    1.82  apply (simp_all add: add_less_mono)
    1.83  done
    1.84  
    1.85 +text {* Addition is the inverse of subtraction:
    1.86 +  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
    1.87 +lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
    1.88 +by (induct m n rule: diff_induct) simp_all
    1.89 +
    1.90 +
    1.91  text{*The naturals form an ordered @{text semidom}*}
    1.92  instance nat :: linordered_semidom
    1.93  proof
    1.94 @@ -790,7 +793,9 @@
    1.95    show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
    1.96    show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
    1.97    show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
    1.98 -qed
    1.99 +  show "\<And>m n :: nat. n \<le> m ==> (m - n) + n = (m::nat)"
   1.100 +    by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
   1.101 +qed 
   1.102  
   1.103  
   1.104  subsubsection {* @{term min} and @{term max} *}
   1.105 @@ -989,7 +994,7 @@
   1.106    "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
   1.107  by (induct n rule: less_induct) auto
   1.108  
   1.109 -lemma infinite_descent0[case_names 0 smaller]: 
   1.110 +lemma infinite_descent0[case_names 0 smaller]:
   1.111    "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
   1.112  by (rule infinite_descent) (case_tac "n>0", auto)
   1.113  
   1.114 @@ -1112,17 +1117,6 @@
   1.115  
   1.116  subsubsection {* More results about difference *}
   1.117  
   1.118 -text {* Addition is the inverse of subtraction:
   1.119 -  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
   1.120 -lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
   1.121 -by (induct m n rule: diff_induct) simp_all
   1.122 -
   1.123 -lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
   1.124 -by (simp add: add_diff_inverse linorder_not_less)
   1.125 -
   1.126 -lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   1.127 -by (simp add: add.commute)
   1.128 -
   1.129  lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
   1.130  by (induct m n rule: diff_induct) simp_all
   1.131  
   1.132 @@ -1490,8 +1484,8 @@
   1.133  
   1.134  lemma of_nat_0_neq [simp]:
   1.135    "0 \<noteq> of_nat (Suc n)"
   1.136 -  unfolding of_nat_0_eq_iff by simp  
   1.137 -  
   1.138 +  unfolding of_nat_0_eq_iff by simp
   1.139 +
   1.140  end
   1.141  
   1.142  context linordered_semidom
   1.143 @@ -1770,7 +1764,7 @@
   1.144  lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
   1.145  by auto
   1.146  
   1.147 -lemma inj_on_diff_nat: 
   1.148 +lemma inj_on_diff_nat:
   1.149    assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
   1.150    shows "inj_on (\<lambda>n. n - k) N"
   1.151  proof (rule inj_onI)
   1.152 @@ -1980,7 +1974,7 @@
   1.153  
   1.154  lemma nat_mult_1: "(1::nat) * n = n"
   1.155    by (fact mult_1_left)
   1.156 - 
   1.157 +
   1.158  lemma nat_mult_1_right: "n * (1::nat) = n"
   1.159    by (fact mult_1_right)
   1.160