src/HOL/Nat.thy
changeset 14341 a09441bd4f1e
parent 14331 8dbbb7cf3637
child 14348 744c868ee0b7
     1.1 --- a/src/HOL/Nat.thy	Tue Jan 06 10:38:14 2004 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Jan 06 10:40:15 2004 +0100
     1.3 @@ -460,6 +460,14 @@
     1.4    apply blast
     1.5    done
     1.6  
     1.7 +text {* Type {@typ nat} is a wellfounded linear order *}
     1.8 +
     1.9 +instance nat :: order by (intro_classes,
    1.10 +  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
    1.11 +instance nat :: linorder by (intro_classes, rule nat_le_linear)
    1.12 +instance nat :: wellorder by (intro_classes, rule wf_less)
    1.13 +
    1.14 +
    1.15  lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
    1.16    by (blast elim!: less_SucE)
    1.17  
    1.18 @@ -488,13 +496,6 @@
    1.19  lemma one_reorient: "(1 = x) = (x = 1)"
    1.20    by auto
    1.21  
    1.22 -text {* Type {@typ nat} is a wellfounded linear order *}
    1.23 -
    1.24 -instance nat :: order by (intro_classes,
    1.25 -  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
    1.26 -instance nat :: linorder by (intro_classes, rule nat_le_linear)
    1.27 -instance nat :: wellorder by (intro_classes, rule wf_less)
    1.28 -
    1.29  subsection {* Arithmetic operators *}
    1.30  
    1.31  axclass power < type
    1.32 @@ -525,7 +526,8 @@
    1.33    mult_0:   "0 * n = 0"
    1.34    mult_Suc: "Suc m * n = n + (m * n)"
    1.35  
    1.36 -text {* These 2 rules ease the use of primitive recursion. NOTE USE OF @{text "=="} *}
    1.37 +text {* These two rules ease the use of primitive recursion. 
    1.38 +NOTE USE OF @{text "=="} *}
    1.39  lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
    1.40    by simp
    1.41  
    1.42 @@ -560,7 +562,7 @@
    1.43  lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
    1.44    by (case_tac m) simp_all
    1.45  
    1.46 -lemma nat_induct2: "P 0 ==> P (Suc 0) ==> (!!k. P k ==> P (Suc (Suc k))) ==> P n"
    1.47 +lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
    1.48    apply (rule nat_less_induct)
    1.49    apply (case_tac n)
    1.50    apply (case_tac [2] nat)
    1.51 @@ -690,25 +692,6 @@
    1.52    apply (simp add: nat_add_assoc del: add_0_right)
    1.53    done
    1.54  
    1.55 -subsection {* Monotonicity of Addition *}
    1.56 -
    1.57 -text {* strict, in 1st argument *}
    1.58 -lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
    1.59 -  by (induct k) simp_all
    1.60 -
    1.61 -text {* strict, in both arguments *}
    1.62 -lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
    1.63 -  apply (rule add_less_mono1 [THEN less_trans], assumption+)
    1.64 -  apply (induct_tac j, simp_all)
    1.65 -  done
    1.66 -
    1.67 -text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
    1.68 -lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
    1.69 -  apply (induct n)
    1.70 -  apply (simp_all add: order_le_less)
    1.71 -  apply (blast elim!: less_SucE intro!: add_0_right [symmetric] add_Suc_right [symmetric])
    1.72 -  done
    1.73 -
    1.74  
    1.75  subsection {* Multiplication *}
    1.76  
    1.77 @@ -735,20 +718,9 @@
    1.78  lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
    1.79    by (induct m) (simp_all add: add_mult_distrib)
    1.80  
    1.81 -lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
    1.82 -  apply (induct_tac m)
    1.83 -  apply (induct_tac [2] n, simp_all)
    1.84 -  done
    1.85  
    1.86 -text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
    1.87 -lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
    1.88 -  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
    1.89 -  apply (induct_tac x) 
    1.90 -  apply (simp_all add: add_less_mono)
    1.91 -  done
    1.92 -
    1.93 -text{*The Naturals Form an Ordered Semiring*}
    1.94 -instance nat :: ordered_semiring
    1.95 +text{*The Naturals Form A Semiring*}
    1.96 +instance nat :: semiring
    1.97  proof
    1.98    fix i j k :: nat
    1.99    show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
   1.100 @@ -759,6 +731,46 @@
   1.101    show "1 * i = i" by simp
   1.102    show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
   1.103    show "0 \<noteq> (1::nat)" by simp
   1.104 +  assume "k+i = k+j" thus "i=j" by simp
   1.105 +qed
   1.106 +
   1.107 +lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   1.108 +  apply (induct_tac m)
   1.109 +  apply (induct_tac [2] n, simp_all)
   1.110 +  done
   1.111 +
   1.112 +subsection {* Monotonicity of Addition *}
   1.113 +
   1.114 +text {* strict, in 1st argument *}
   1.115 +lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   1.116 +  by (induct k) simp_all
   1.117 +
   1.118 +text {* strict, in both arguments *}
   1.119 +lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   1.120 +  apply (rule add_less_mono1 [THEN less_trans], assumption+)
   1.121 +  apply (induct_tac j, simp_all)
   1.122 +  done
   1.123 +
   1.124 +text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
   1.125 +lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   1.126 +  apply (induct n)
   1.127 +  apply (simp_all add: order_le_less)
   1.128 +  apply (blast elim!: less_SucE 
   1.129 +               intro!: add_0_right [symmetric] add_Suc_right [symmetric])
   1.130 +  done
   1.131 +
   1.132 +text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   1.133 +lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
   1.134 +  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
   1.135 +  apply (induct_tac x) 
   1.136 +  apply (simp_all add: add_less_mono)
   1.137 +  done
   1.138 +
   1.139 +
   1.140 +text{*The Naturals Form an Ordered Semiring*}
   1.141 +instance nat :: ordered_semiring
   1.142 +proof
   1.143 +  fix i j k :: nat
   1.144    show "i \<le> j ==> k + i \<le> k + j" by simp
   1.145    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
   1.146  qed
   1.147 @@ -790,14 +802,10 @@
   1.148    by (rule add_mono)
   1.149  
   1.150  lemma le_add2: "n \<le> ((m + n)::nat)"
   1.151 -  apply (induct m, simp_all)
   1.152 -  apply (erule le_SucI)
   1.153 -  done
   1.154 +  by (insert add_right_mono [of 0 m n], simp) 
   1.155  
   1.156  lemma le_add1: "n \<le> ((n + m)::nat)"
   1.157 -  apply (simp add: add_ac)
   1.158 -  apply (rule le_add2)
   1.159 -  done
   1.160 +  by (simp add: add_commute, rule le_add2)
   1.161  
   1.162  lemma less_add_Suc1: "i < Suc (i + m)"
   1.163    by (rule le_less_trans, rule le_add1, rule lessI)
   1.164 @@ -808,7 +816,6 @@
   1.165  lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
   1.166    by (rules intro!: less_add_Suc1 less_imp_Suc_add)
   1.167  
   1.168 -
   1.169  lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
   1.170    by (rule le_trans, assumption, rule le_add1)
   1.171  
   1.172 @@ -822,8 +829,8 @@
   1.173    by (rule less_le_trans, assumption, rule le_add2)
   1.174  
   1.175  lemma add_lessD1: "i + j < (k::nat) ==> i < k"
   1.176 -  apply (induct j, simp_all)
   1.177 -  apply (blast dest: Suc_lessD)
   1.178 +  apply (rule le_less_trans [of _ "i+j"]) 
   1.179 +  apply (simp_all add: le_add1)
   1.180    done
   1.181  
   1.182  lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
   1.183 @@ -835,7 +842,9 @@
   1.184    by (simp add: add_commute not_add_less1)
   1.185  
   1.186  lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
   1.187 -  by (induct k) (simp_all add: le_simps)
   1.188 +  apply (rule order_trans [of _ "m+k"]) 
   1.189 +  apply (simp_all add: le_add1)
   1.190 +  done
   1.191  
   1.192  lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
   1.193    apply (simp add: add_commute)
   1.194 @@ -969,21 +978,17 @@
   1.195  subsection {* Monotonicity of Multiplication *}
   1.196  
   1.197  lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
   1.198 -  by (induct k) (simp_all add: add_le_mono)
   1.199 +  by (simp add: mult_right_mono) 
   1.200  
   1.201  lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
   1.202 -  apply (drule mult_le_mono1)
   1.203 -  apply (simp add: mult_commute)
   1.204 -  done
   1.205 +  by (simp add: mult_left_mono) 
   1.206  
   1.207  text {* @{text "\<le>"} monotonicity, BOTH arguments *}
   1.208  lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
   1.209 -  apply (erule mult_le_mono1 [THEN le_trans])
   1.210 -  apply (erule mult_le_mono2)
   1.211 -  done
   1.212 +  by (simp add: mult_mono) 
   1.213  
   1.214  lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
   1.215 -  by (drule mult_less_mono2) (simp_all add: mult_commute)
   1.216 +  by (simp add: mult_strict_right_mono) 
   1.217  
   1.218  text{*Differs from the standard @{text zero_less_mult_iff} in that
   1.219        there are no negative numbers.*}
   1.220 @@ -1007,7 +1012,7 @@
   1.221    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   1.222    done
   1.223  
   1.224 -lemma mult_less_cancel2: "((m::nat) * k < n * k) = (0 < k & m < n)"
   1.225 +lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
   1.226    apply (safe intro!: mult_less_mono1)
   1.227    apply (case_tac k, auto)
   1.228    apply (simp del: le_0_eq add: linorder_not_le [symmetric])
   1.229 @@ -1015,9 +1020,7 @@
   1.230    done
   1.231  
   1.232  lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
   1.233 -  by (simp add: mult_less_cancel2 mult_commute [of k])
   1.234 -
   1.235 -declare mult_less_cancel2 [simp]
   1.236 +  by (simp add: mult_commute [of k])
   1.237  
   1.238  lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
   1.239  by (simp add: linorder_not_less [symmetric], auto)
   1.240 @@ -1025,15 +1028,13 @@
   1.241  lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
   1.242  by (simp add: linorder_not_less [symmetric], auto)
   1.243  
   1.244 -lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   1.245 +lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   1.246    apply (cut_tac less_linear, safe, auto)
   1.247    apply (drule mult_less_mono1, assumption, simp)+
   1.248    done
   1.249  
   1.250  lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
   1.251 -  by (simp add: mult_cancel2 mult_commute [of k])
   1.252 -
   1.253 -declare mult_cancel2 [simp]
   1.254 +  by (simp add: mult_commute [of k])
   1.255  
   1.256  lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
   1.257    by (subst mult_less_cancel1) simp
   1.258 @@ -1044,7 +1045,6 @@
   1.259  lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
   1.260    by (subst mult_cancel1) simp
   1.261  
   1.262 -
   1.263  text {* Lemma for @{text gcd} *}
   1.264  lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
   1.265    apply (drule sym)
   1.266 @@ -1054,5 +1054,4 @@
   1.267    apply (fastsimp dest: mult_less_mono2)
   1.268    done
   1.269  
   1.270 -
   1.271  end