- Converted to new theory format
authorberghofe
Mon Aug 05 14:27:42 2002 +0200 (2002-08-05)
changeset 1344943c9ec498291
parent 13448 3196f93030bb
child 13450 17fec4798b91
- Converted to new theory format
- Moved NatDef stuff to theory Nat
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Mon Aug 05 14:26:54 2002 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Aug 05 14:27:42 2002 +0200
     1.3 @@ -6,43 +6,1076 @@
     1.4  and * (for div, mod and dvd, see theory Divides).
     1.5  *)
     1.6  
     1.7 -Nat = NatDef + 
     1.8 +header {* Natural numbers *}
     1.9 +
    1.10 +theory Nat = Wellfounded_Recursion:
    1.11 +
    1.12 +subsection {* Type @{text ind} *}
    1.13 +
    1.14 +typedecl ind
    1.15 +
    1.16 +consts
    1.17 +  Zero_Rep      :: ind
    1.18 +  Suc_Rep       :: "ind => ind"
    1.19 +
    1.20 +axioms
    1.21 +  -- {* the axiom of infinity in 2 parts *}
    1.22 +  inj_Suc_Rep:          "inj Suc_Rep"
    1.23 +  Suc_Rep_not_Zero_Rep: "Suc_Rep x ~= Zero_Rep"
    1.24 +
    1.25 +
    1.26 +subsection {* Type nat *}
    1.27 +
    1.28 +text {* Type definition *}
    1.29 +
    1.30 +consts
    1.31 +  Nat :: "ind set"
    1.32 +
    1.33 +inductive Nat
    1.34 +intros
    1.35 +  Zero_RepI: "Zero_Rep : Nat"
    1.36 +  Suc_RepI: "i : Nat ==> Suc_Rep i : Nat"
    1.37 +
    1.38 +global
    1.39 +
    1.40 +typedef (open Nat)
    1.41 +  nat = "Nat" by (rule exI, rule Nat.Zero_RepI)
    1.42 +
    1.43 +instance nat :: ord ..
    1.44 +instance nat :: zero ..
    1.45 +instance nat :: one ..
    1.46 +
    1.47 +
    1.48 +text {* Abstract constants and syntax *}
    1.49 +
    1.50 +consts
    1.51 +  Suc :: "nat => nat"
    1.52 +  pred_nat :: "(nat * nat) set"
    1.53 +
    1.54 +local
    1.55 +
    1.56 +defs
    1.57 +  Zero_nat_def: "0 == Abs_Nat Zero_Rep"
    1.58 +  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    1.59 +  One_nat_def [simp]: "1 == Suc 0"
    1.60 +
    1.61 +  -- {* nat operations *}
    1.62 +  pred_nat_def: "pred_nat == {(m, n). n = Suc m}"
    1.63 +
    1.64 +  less_def: "m < n == (m, n) : trancl pred_nat"
    1.65 +
    1.66 +  le_def: "m <= (n::nat) == ~ (n < m)"
    1.67 +
    1.68 +
    1.69 +text {* Induction *}
    1.70  
    1.71 -(* type "nat" is a wellfounded linear order, and a datatype *)
    1.72 +theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
    1.73 +  apply (unfold Zero_nat_def Suc_def)
    1.74 +  apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    1.75 +  apply (erule Rep_Nat [THEN Nat.induct])
    1.76 +  apply (rules elim: Abs_Nat_inverse [THEN subst])
    1.77 +  done
    1.78 +
    1.79 +
    1.80 +text {* Isomorphisms: @{text Abs_Nat} and @{text Rep_Nat} *}
    1.81 +
    1.82 +lemma inj_Rep_Nat: "inj Rep_Nat"
    1.83 +  apply (rule inj_inverseI)
    1.84 +  apply (rule Rep_Nat_inverse)
    1.85 +  done
    1.86 +
    1.87 +lemma inj_on_Abs_Nat: "inj_on Abs_Nat Nat"
    1.88 +  apply (rule inj_on_inverseI)
    1.89 +  apply (erule Abs_Nat_inverse)
    1.90 +  done
    1.91 +
    1.92 +text {* Distinctness of constructors *}
    1.93 +
    1.94 +lemma Suc_not_Zero [iff]: "Suc m ~= 0"
    1.95 +  apply (unfold Zero_nat_def Suc_def)
    1.96 +  apply (rule inj_on_Abs_Nat [THEN inj_on_contraD])
    1.97 +  apply (rule Suc_Rep_not_Zero_Rep)
    1.98 +  apply (rule Rep_Nat Nat.Suc_RepI Nat.Zero_RepI)+
    1.99 +  done
   1.100 +
   1.101 +lemma Zero_not_Suc [iff]: "0 ~= Suc m"
   1.102 +  by (rule not_sym, rule Suc_not_Zero not_sym)
   1.103 +
   1.104 +lemma Suc_neq_Zero: "Suc m = 0 ==> R"
   1.105 +  by (rule notE, rule Suc_not_Zero)
   1.106 +
   1.107 +lemma Zero_neq_Suc: "0 = Suc m ==> R"
   1.108 +  by (rule Suc_neq_Zero, erule sym)
   1.109 +
   1.110 +text {* Injectiveness of @{term Suc} *}
   1.111 +
   1.112 +lemma inj_Suc: "inj Suc"
   1.113 +  apply (unfold Suc_def)
   1.114 +  apply (rule injI)
   1.115 +  apply (drule inj_on_Abs_Nat [THEN inj_onD])
   1.116 +  apply (rule Rep_Nat Nat.Suc_RepI)+
   1.117 +  apply (drule inj_Suc_Rep [THEN injD])
   1.118 +  apply (erule inj_Rep_Nat [THEN injD])
   1.119 +  done
   1.120 +
   1.121 +lemma Suc_inject: "Suc x = Suc y ==> x = y"
   1.122 +  by (rule inj_Suc [THEN injD])
   1.123 +
   1.124 +lemma Suc_Suc_eq [iff]: "(Suc m = Suc n) = (m = n)"
   1.125 +  apply (rule iffI)
   1.126 +  apply (erule Suc_inject)
   1.127 +  apply (erule arg_cong)
   1.128 +  done
   1.129 +
   1.130 +lemma nat_not_singleton: "(ALL x. x = (0::nat)) = False"
   1.131 +  by auto
   1.132 +
   1.133 +text {* @{typ nat} is a datatype *}
   1.134  
   1.135  rep_datatype nat
   1.136 -  distinct Suc_not_Zero, Zero_not_Suc
   1.137 -  inject   Suc_Suc_eq
   1.138 -  induct   nat_induct
   1.139 +  distinct  Suc_not_Zero Zero_not_Suc
   1.140 +  inject    Suc_Suc_eq
   1.141 +  induction nat_induct
   1.142 +
   1.143 +lemma n_not_Suc_n: "n ~= Suc n"
   1.144 +  by (induct n) simp_all
   1.145 +
   1.146 +lemma Suc_n_not_n: "Suc t ~= t"
   1.147 +  by (rule not_sym, rule n_not_Suc_n)
   1.148 +
   1.149 +text {* A special form of induction for reasoning
   1.150 +  about @{term "m < n"} and @{term "m - n"} *}
   1.151 +
   1.152 +theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
   1.153 +    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
   1.154 +  apply (rule_tac x = "m" in spec)
   1.155 +  apply (induct_tac n)
   1.156 +  prefer 2
   1.157 +  apply (rule allI)
   1.158 +  apply (induct_tac x)
   1.159 +  apply rules+
   1.160 +  done
   1.161 +
   1.162 +subsection {* Basic properties of "less than" *}
   1.163 +
   1.164 +lemma wf_pred_nat: "wf pred_nat"
   1.165 +  apply (unfold wf_def pred_nat_def)
   1.166 +  apply clarify
   1.167 +  apply (induct_tac x)
   1.168 +  apply blast+
   1.169 +  done
   1.170 +
   1.171 +lemma wf_less: "wf {(x, y::nat). x < y}"
   1.172 +  apply (unfold less_def)
   1.173 +  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset])
   1.174 +  apply blast
   1.175 +  done
   1.176 +
   1.177 +lemma less_eq: "((m, n) : pred_nat^+) = (m < n)"
   1.178 +  apply (unfold less_def)
   1.179 +  apply (rule refl)
   1.180 +  done
   1.181 +
   1.182 +subsubsection {* Introduction properties *}
   1.183 +
   1.184 +lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
   1.185 +  apply (unfold less_def)
   1.186 +  apply (rule trans_trancl [THEN transD])
   1.187 +  apply assumption+
   1.188 +  done
   1.189 +
   1.190 +lemma lessI [iff]: "n < Suc n"
   1.191 +  apply (unfold less_def pred_nat_def)
   1.192 +  apply (simp add: r_into_trancl)
   1.193 +  done
   1.194 +
   1.195 +lemma less_SucI: "i < j ==> i < Suc j"
   1.196 +  apply (rule less_trans)
   1.197 +  apply assumption
   1.198 +  apply (rule lessI)
   1.199 +  done
   1.200 +
   1.201 +lemma zero_less_Suc [iff]: "0 < Suc n"
   1.202 +  apply (induct n)
   1.203 +  apply (rule lessI)
   1.204 +  apply (erule less_trans)
   1.205 +  apply (rule lessI)
   1.206 +  done
   1.207 +
   1.208 +subsubsection {* Elimination properties *}
   1.209 +
   1.210 +lemma less_not_sym: "n < m ==> ~ m < (n::nat)"
   1.211 +  apply (unfold less_def)
   1.212 +  apply (blast intro: wf_pred_nat wf_trancl [THEN wf_asym])
   1.213 +  done
   1.214 +
   1.215 +lemma less_asym:
   1.216 +  assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P
   1.217 +  apply (rule contrapos_np)
   1.218 +  apply (rule less_not_sym)
   1.219 +  apply (rule h1)
   1.220 +  apply (erule h2)
   1.221 +  done
   1.222 +
   1.223 +lemma less_not_refl: "~ n < (n::nat)"
   1.224 +  apply (unfold less_def)
   1.225 +  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_not_refl])
   1.226 +  done
   1.227 +
   1.228 +lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
   1.229 +  by (rule notE, rule less_not_refl)
   1.230 +
   1.231 +lemma less_not_refl2: "n < m ==> m ~= (n::nat)" by blast
   1.232 +
   1.233 +lemma less_not_refl3: "(s::nat) < t ==> s ~= t"
   1.234 +  by (rule not_sym, rule less_not_refl2)
   1.235 +
   1.236 +lemma lessE:
   1.237 +  assumes major: "i < k"
   1.238 +  and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
   1.239 +  shows P
   1.240 +  apply (rule major [unfolded less_def pred_nat_def, THEN tranclE])
   1.241 +  apply simp_all
   1.242 +  apply (erule p1)
   1.243 +  apply (rule p2)
   1.244 +  apply (simp add: less_def pred_nat_def)
   1.245 +  apply assumption
   1.246 +  done
   1.247 +
   1.248 +lemma not_less0 [iff]: "~ n < (0::nat)"
   1.249 +  by (blast elim: lessE)
   1.250 +
   1.251 +lemma less_zeroE: "(n::nat) < 0 ==> R"
   1.252 +  by (rule notE, rule not_less0)
   1.253 +
   1.254 +lemma less_SucE: assumes major: "m < Suc n"
   1.255 +  and less: "m < n ==> P" and eq: "m = n ==> P" shows P
   1.256 +  apply (rule major [THEN lessE])
   1.257 +  apply (rule eq)
   1.258 +  apply blast
   1.259 +  apply (rule less)
   1.260 +  apply blast
   1.261 +  done
   1.262 +
   1.263 +lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
   1.264 +  by (blast elim!: less_SucE intro: less_trans)
   1.265 +
   1.266 +lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
   1.267 +  by (simp add: less_Suc_eq)
   1.268 +
   1.269 +lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   1.270 +  by (simp add: less_Suc_eq)
   1.271 +
   1.272 +lemma Suc_mono: "m < n ==> Suc m < Suc n"
   1.273 +  by (induct n) (fast elim: less_trans lessE)+
   1.274 +
   1.275 +text {* "Less than" is a linear ordering *}
   1.276 +lemma less_linear: "m < n | m = n | n < (m::nat)"
   1.277 +  apply (induct_tac m)
   1.278 +  apply (induct_tac n)
   1.279 +  apply (rule refl [THEN disjI1, THEN disjI2])
   1.280 +  apply (rule zero_less_Suc [THEN disjI1])
   1.281 +  apply (blast intro: Suc_mono less_SucI elim: lessE)
   1.282 +  done
   1.283 +
   1.284 +lemma nat_neq_iff: "((m::nat) ~= n) = (m < n | n < m)"
   1.285 +  using less_linear by blast
   1.286 +
   1.287 +lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
   1.288 +  and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m"
   1.289 +  shows "P n m"
   1.290 +  apply (rule less_linear [THEN disjE])
   1.291 +  apply (erule_tac [2] disjE)
   1.292 +  apply (erule lessCase)
   1.293 +  apply (erule sym [THEN eqCase])
   1.294 +  apply (erule major)
   1.295 +  done
   1.296 +
   1.297 +
   1.298 +subsubsection {* Inductive (?) properties *}
   1.299 +
   1.300 +lemma Suc_lessI: "m < n ==> Suc m ~= n ==> Suc m < n"
   1.301 +  apply (simp add: nat_neq_iff)
   1.302 +  apply (blast elim!: less_irrefl less_SucE elim: less_asym)
   1.303 +  done
   1.304 +
   1.305 +lemma Suc_lessD: "Suc m < n ==> m < n"
   1.306 +  apply (induct n)
   1.307 +  apply (fast intro!: lessI [THEN less_SucI] elim: less_trans lessE)+
   1.308 +  done
   1.309 +
   1.310 +lemma Suc_lessE: assumes major: "Suc i < k"
   1.311 +  and minor: "!!j. i < j ==> k = Suc j ==> P" shows P
   1.312 +  apply (rule major [THEN lessE])
   1.313 +  apply (erule lessI [THEN minor])
   1.314 +  apply (erule Suc_lessD [THEN minor])
   1.315 +  apply assumption
   1.316 +  done
   1.317 +
   1.318 +lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   1.319 +  by (blast elim: lessE dest: Suc_lessD)
   1.320  
   1.321 -instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
   1.322 -instance nat :: linorder (nat_le_linear)
   1.323 -instance nat :: wellorder (wf_less)
   1.324 +lemma Suc_less_eq [iff]: "(Suc m < Suc n) = (m < n)"
   1.325 +  apply (rule iffI)
   1.326 +  apply (erule Suc_less_SucD)
   1.327 +  apply (erule Suc_mono)
   1.328 +  done
   1.329 +
   1.330 +lemma less_trans_Suc:
   1.331 +  assumes le: "i < j" shows "j < k ==> Suc i < k"
   1.332 +  apply (induct k)
   1.333 +  apply simp_all
   1.334 +  apply (insert le)
   1.335 +  apply (simp add: less_Suc_eq)
   1.336 +  apply (blast dest: Suc_lessD)
   1.337 +  done
   1.338 +
   1.339 +text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
   1.340 +lemma not_less_eq: "(~ m < n) = (n < Suc m)"
   1.341 +  apply (rule_tac m = "m" and n = "n" in diff_induct)
   1.342 +  apply simp_all
   1.343 +  done
   1.344 +
   1.345 +text {* Complete induction, aka course-of-values induction *}
   1.346 +lemma nat_less_induct:
   1.347 +  assumes prem: "!!n. ALL m::nat. m < n --> P m ==> P n" shows "P n"
   1.348 +  apply (rule_tac a=n in wf_induct)
   1.349 +  apply (rule wf_pred_nat [THEN wf_trancl])
   1.350 +  apply (rule prem)
   1.351 +  apply (unfold less_def)
   1.352 +  apply assumption
   1.353 +  done
   1.354 +
   1.355 +subsection {* Properties of "less or equal than" *}
   1.356 +
   1.357 +text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
   1.358 +lemma less_Suc_eq_le: "(m < Suc n) = (m <= n)"
   1.359 +  by (unfold le_def, rule not_less_eq [symmetric])
   1.360 +
   1.361 +lemma le_imp_less_Suc: "m <= n ==> m < Suc n"
   1.362 +  by (rule less_Suc_eq_le [THEN iffD2])
   1.363 +
   1.364 +lemma le0 [iff]: "(0::nat) <= n"
   1.365 +  by (unfold le_def, rule not_less0)
   1.366 +
   1.367 +lemma Suc_n_not_le_n: "~ Suc n <= n"
   1.368 +  by (simp add: le_def)
   1.369 +
   1.370 +lemma le_0_eq [iff]: "((i::nat) <= 0) = (i = 0)"
   1.371 +  by (induct i) (simp_all add: le_def)
   1.372 +
   1.373 +lemma le_Suc_eq: "(m <= Suc n) = (m <= n | m = Suc n)"
   1.374 +  by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
   1.375 +
   1.376 +lemma le_SucE: "m <= Suc n ==> (m <= n ==> R) ==> (m = Suc n ==> R) ==> R"
   1.377 +  by (drule le_Suc_eq [THEN iffD1], rules+)
   1.378 +
   1.379 +lemma leI: "~ n < m ==> m <= (n::nat)" by (simp add: le_def)
   1.380 +
   1.381 +lemma leD: "m <= n ==> ~ n < (m::nat)"
   1.382 +  by (simp add: le_def)
   1.383 +
   1.384 +lemmas leE = leD [elim_format]
   1.385 +
   1.386 +lemma not_less_iff_le: "(~ n < m) = (m <= (n::nat))"
   1.387 +  by (blast intro: leI elim: leE)
   1.388 +
   1.389 +lemma not_leE: "~ m <= n ==> n<(m::nat)"
   1.390 +  by (simp add: le_def)
   1.391 +
   1.392 +lemma not_le_iff_less: "(~ n <= m) = (m < (n::nat))"
   1.393 +  by (simp add: le_def)
   1.394 +
   1.395 +lemma Suc_leI: "m < n ==> Suc(m) <= n"
   1.396 +  apply (simp add: le_def less_Suc_eq)
   1.397 +  apply (blast elim!: less_irrefl less_asym)
   1.398 +  done -- {* formerly called lessD *}
   1.399 +
   1.400 +lemma Suc_leD: "Suc(m) <= n ==> m <= n"
   1.401 +  by (simp add: le_def less_Suc_eq)
   1.402 +
   1.403 +text {* Stronger version of @{text Suc_leD} *}
   1.404 +lemma Suc_le_lessD: "Suc m <= n ==> m < n"
   1.405 +  apply (simp add: le_def less_Suc_eq)
   1.406 +  using less_linear
   1.407 +  apply blast
   1.408 +  done
   1.409 +
   1.410 +lemma Suc_le_eq: "(Suc m <= n) = (m < n)"
   1.411 +  by (blast intro: Suc_leI Suc_le_lessD)
   1.412 +
   1.413 +lemma le_SucI: "m <= n ==> m <= Suc n"
   1.414 +  by (unfold le_def) (blast dest: Suc_lessD)
   1.415 +
   1.416 +lemma less_imp_le: "m < n ==> m <= (n::nat)"
   1.417 +  by (unfold le_def) (blast elim: less_asym)
   1.418 +
   1.419 +text {* For instance, @{text "(Suc m < Suc n) = (Suc m <= n) = (m < n)"} *}
   1.420 +lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
   1.421 +
   1.422 +
   1.423 +text {* Equivalence of @{term "m <= n"} and @{term "m < n | m = n"} *}
   1.424 +
   1.425 +lemma le_imp_less_or_eq: "m <= n ==> m < n | m = (n::nat)"
   1.426 +  apply (unfold le_def)
   1.427 +  using less_linear
   1.428 +  apply (blast elim: less_irrefl less_asym)
   1.429 +  done
   1.430 +
   1.431 +lemma less_or_eq_imp_le: "m < n | m = n ==> m <= (n::nat)"
   1.432 +  apply (unfold le_def)
   1.433 +  using less_linear
   1.434 +  apply (blast elim!: less_irrefl elim: less_asym)
   1.435 +  done
   1.436 +
   1.437 +lemma le_eq_less_or_eq: "(m <= (n::nat)) = (m < n | m=n)"
   1.438 +  by (rules intro: less_or_eq_imp_le le_imp_less_or_eq)
   1.439 +
   1.440 +text {* Useful with @{text Blast}. *}
   1.441 +lemma eq_imp_le: "(m::nat) = n ==> m <= n"
   1.442 +  by (rule less_or_eq_imp_le, rule disjI2)
   1.443 +
   1.444 +lemma le_refl: "n <= (n::nat)"
   1.445 +  by (simp add: le_eq_less_or_eq)
   1.446 +
   1.447 +lemma le_less_trans: "[| i <= j; j < k |] ==> i < (k::nat)"
   1.448 +  by (blast dest!: le_imp_less_or_eq intro: less_trans)
   1.449 +
   1.450 +lemma less_le_trans: "[| i < j; j <= k |] ==> i < (k::nat)"
   1.451 +  by (blast dest!: le_imp_less_or_eq intro: less_trans)
   1.452 +
   1.453 +lemma le_trans: "[| i <= j; j <= k |] ==> i <= (k::nat)"
   1.454 +  by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
   1.455 +
   1.456 +lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)"
   1.457 +  -- {* @{text order_less_irrefl} could make this proof fail *}
   1.458 +  by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
   1.459 +
   1.460 +lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)"
   1.461 +  by (simp add: le_simps)
   1.462 +
   1.463 +text {* Axiom @{text order_less_le} of class @{text order}: *}
   1.464 +lemma nat_less_le: "((m::nat) < n) = (m <= n & m ~= n)"
   1.465 +  by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
   1.466 +
   1.467 +lemma le_neq_implies_less: "(m::nat) <= n ==> m ~= n ==> m < n"
   1.468 +  by (rule iffD2, rule nat_less_le, rule conjI)
   1.469 +
   1.470 +text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
   1.471 +lemma nat_le_linear: "(m::nat) <= n | n <= m"
   1.472 +  apply (simp add: le_eq_less_or_eq)
   1.473 +  using less_linear
   1.474 +  apply blast
   1.475 +  done
   1.476 +
   1.477 +lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   1.478 +  by (blast elim!: less_SucE)
   1.479 +
   1.480 +
   1.481 +text {*
   1.482 +  Rewrite @{term "n < Suc m"} to @{term "n = m"}
   1.483 +  if @{term "~ n < m"} or @{term "m <= n"} hold.
   1.484 +  Not suitable as default simprules because they often lead to looping
   1.485 +*}
   1.486 +lemma le_less_Suc_eq: "m <= n ==> (n < Suc m) = (n = m)"
   1.487 +  by (rule not_less_less_Suc_eq, rule leD)
   1.488 +
   1.489 +lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
   1.490 +
   1.491 +
   1.492 +text {*
   1.493 +  Re-orientation of the equations @{text "0 = x"} and @{text "1 = x"}. 
   1.494 +  No longer added as simprules (they loop) 
   1.495 +  but via @{text reorient_simproc} in Bin
   1.496 +*}
   1.497 +
   1.498 +text {* Polymorphic, not just for @{typ nat} *}
   1.499 +lemma zero_reorient: "(0 = x) = (x = 0)"
   1.500 +  by auto
   1.501 +
   1.502 +lemma one_reorient: "(1 = x) = (x = 1)"
   1.503 +  by auto
   1.504 +
   1.505 +text {* Type {@typ nat} is a wellfounded linear order *}
   1.506 +
   1.507 +instance nat :: order by (intro_classes,
   1.508 +  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
   1.509 +instance nat :: linorder by (intro_classes, rule nat_le_linear)
   1.510 +instance nat :: wellorder by (intro_classes, rule wf_less)
   1.511 +
   1.512 +subsection {* Arithmetic operators *}
   1.513  
   1.514  axclass power < type
   1.515  
   1.516  consts
   1.517 -  power :: ['a::power, nat] => 'a            (infixr "^" 80)
   1.518 +  power :: "('a::power) => nat => 'a"            (infixr "^" 80)
   1.519  
   1.520  
   1.521 -(* arithmetic operators + - and * *)
   1.522 +text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
   1.523 +
   1.524 +instance nat :: plus ..
   1.525 +instance nat :: minus ..
   1.526 +instance nat :: times ..
   1.527 +instance nat :: power ..
   1.528  
   1.529 -instance
   1.530 -  nat :: {plus, minus, times, power}
   1.531 +text {* size of a datatype value; overloaded *}
   1.532 +consts size :: "'a => nat"
   1.533  
   1.534 -(* size of a datatype value; overloaded *)
   1.535 -consts size :: 'a => nat
   1.536 +primrec
   1.537 +  add_0:    "0 + n = n"
   1.538 +  add_Suc:  "Suc m + n = Suc (m + n)"
   1.539 +
   1.540 +primrec
   1.541 +  diff_0:   "m - 0 = m"
   1.542 +  diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
   1.543  
   1.544  primrec
   1.545 -  add_0    "0 + n = n"
   1.546 -  add_Suc  "Suc m + n = Suc(m + n)"
   1.547 +  mult_0:   "0 * n = 0"
   1.548 +  mult_Suc: "Suc m * n = n + (m * n)"
   1.549 +
   1.550 +text {* These 2 rules ease the use of primitive recursion. NOTE USE OF @{text "=="} *}
   1.551 +lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
   1.552 +  by simp
   1.553 +
   1.554 +lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
   1.555 +  by simp
   1.556 +
   1.557 +lemma not0_implies_Suc: "n ~= 0 ==> EX m. n = Suc m"
   1.558 +  by (case_tac n) simp_all
   1.559 +
   1.560 +lemma gr_implies_not0: "!!n::nat. m<n ==> n ~= 0"
   1.561 +  by (case_tac n) simp_all
   1.562 +
   1.563 +lemma neq0_conv [iff]: "!!n::nat. (n ~= 0) = (0 < n)"
   1.564 +  by (case_tac n) simp_all
   1.565 +
   1.566 +text {* This theorem is useful with @{text blast} *}
   1.567 +lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   1.568 +  by (rule iffD1, rule neq0_conv, rules)
   1.569 +
   1.570 +lemma gr0_conv_Suc: "(0 < n) = (EX m. n = Suc m)"
   1.571 +  by (fast intro: not0_implies_Suc)
   1.572 +
   1.573 +lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   1.574 +  apply (rule iffI)
   1.575 +  apply (rule ccontr)
   1.576 +  apply simp_all
   1.577 +  done
   1.578 +
   1.579 +lemma Suc_le_D: "(Suc n <= m') ==> (? m. m' = Suc m)"
   1.580 +  by (induct m') simp_all
   1.581 +
   1.582 +text {* Useful in certain inductive arguments *}
   1.583 +lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (EX j. m = Suc j & j < n))"
   1.584 +  by (case_tac m) simp_all
   1.585 +
   1.586 +lemma nat_induct2: "P 0 ==> P (Suc 0) ==> (!!k. P k ==> P (Suc (Suc k))) ==> P n"
   1.587 +  apply (rule nat_less_induct)
   1.588 +  apply (case_tac n)
   1.589 +  apply (case_tac [2] nat)
   1.590 +  apply (blast intro: less_trans)+
   1.591 +  done
   1.592 +
   1.593 +subsection {* @{text LEAST} theorems for type @{typ nat} by specialization *}
   1.594 +
   1.595 +lemmas LeastI = wellorder_LeastI
   1.596 +lemmas Least_le = wellorder_Least_le
   1.597 +lemmas not_less_Least = wellorder_not_less_Least
   1.598 +
   1.599 +lemma Least_Suc: "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   1.600 +  apply (case_tac "n")
   1.601 +  apply auto
   1.602 +  apply (frule LeastI)
   1.603 +  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   1.604 +  apply (subgoal_tac " (LEAST x. P x) <= Suc (LEAST x. P (Suc x))")
   1.605 +  apply (erule_tac [2] Least_le)
   1.606 +  apply (case_tac "LEAST x. P x")
   1.607 +  apply auto
   1.608 +  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   1.609 +  apply (blast intro: order_antisym)
   1.610 +  done
   1.611 +
   1.612 +lemma Least_Suc2: "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   1.613 +  apply (erule (1) Least_Suc [THEN ssubst])
   1.614 +  apply simp
   1.615 +  done
   1.616 +
   1.617 +
   1.618 +subsection {* @{term min} and @{term max} *}
   1.619 +
   1.620 +lemma min_0L [simp]: "min 0 n = (0::nat)"
   1.621 +  by (rule min_leastL) simp
   1.622 +
   1.623 +lemma min_0R [simp]: "min n 0 = (0::nat)"
   1.624 +  by (rule min_leastR) simp
   1.625 +
   1.626 +lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   1.627 +  by (simp add: min_of_mono)
   1.628 +
   1.629 +lemma max_0L [simp]: "max 0 n = (n::nat)"
   1.630 +  by (rule max_leastL) simp
   1.631 +
   1.632 +lemma max_0R [simp]: "max n 0 = (n::nat)"
   1.633 +  by (rule max_leastR) simp
   1.634 +
   1.635 +lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
   1.636 +  by (simp add: max_of_mono)
   1.637 +
   1.638 +
   1.639 +subsection {* Basic rewrite rules for the arithmetic operators *}
   1.640 +
   1.641 +text {* Difference *}
   1.642 +
   1.643 +lemma diff_0_eq_0 [simp]: "0 - n = (0::nat)"
   1.644 +  by (induct_tac n) simp_all
   1.645 +
   1.646 +lemma diff_Suc_Suc [simp]: "Suc(m) - Suc(n) = m - n"
   1.647 +  by (induct_tac n) simp_all
   1.648 +
   1.649 +
   1.650 +text {*
   1.651 +  Could be (and is, below) generalized in various ways
   1.652 +  However, none of the generalizations are currently in the simpset,
   1.653 +  and I dread to think what happens if I put them in
   1.654 +*}
   1.655 +lemma Suc_pred [simp]: "0 < n ==> Suc (n - Suc 0) = n"
   1.656 +  by (simp split add: nat.split)
   1.657 +
   1.658 +declare diff_Suc [simp del]
   1.659 +
   1.660 +
   1.661 +subsection {* Addition *}
   1.662 +
   1.663 +lemma add_0_right [simp]: "m + 0 = (m::nat)"
   1.664 +  by (induct m) simp_all
   1.665 +
   1.666 +lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   1.667 +  by (induct m) simp_all
   1.668 +
   1.669 +
   1.670 +text {* Associative law for addition *}
   1.671 +lemma add_assoc: "(m + n) + k = m + ((n + k)::nat)"
   1.672 +  by (induct m) simp_all
   1.673 +
   1.674 +text {* Commutative law for addition *}
   1.675 +lemma add_commute: "m + n = n + (m::nat)"
   1.676 +  by (induct m) simp_all
   1.677 +
   1.678 +lemma add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   1.679 +  apply (rule mk_left_commute [of "op +"])
   1.680 +  apply (rule add_assoc)
   1.681 +  apply (rule add_commute)
   1.682 +  done
   1.683 +
   1.684 +text {* Addition is an AC-operator *}
   1.685 +lemmas add_ac = add_assoc add_commute add_left_commute
   1.686 +
   1.687 +lemma add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
   1.688 +  by (induct k) simp_all
   1.689 +
   1.690 +lemma add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
   1.691 +  by (induct k) simp_all
   1.692 +
   1.693 +lemma add_left_cancel_le [simp]: "(k + m <= k + n) = (m<=(n::nat))"
   1.694 +  by (induct k) simp_all
   1.695 +
   1.696 +lemma add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
   1.697 +  by (induct k) simp_all
   1.698 +
   1.699 +text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
   1.700 +
   1.701 +lemma add_is_0 [iff]: "!!m::nat. (m + n = 0) = (m = 0 & n = 0)"
   1.702 +  by (case_tac m) simp_all
   1.703 +
   1.704 +lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
   1.705 +  by (case_tac m) simp_all
   1.706 +
   1.707 +lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   1.708 +  by (rule trans, rule eq_commute, rule add_is_1)
   1.709 +
   1.710 +lemma add_gr_0 [iff]: "!!m::nat. (0 < m + n) = (0 < m | 0 < n)"
   1.711 +  by (simp del: neq0_conv add: neq0_conv [symmetric])
   1.712 +
   1.713 +lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   1.714 +  apply (drule add_0_right [THEN ssubst])
   1.715 +  apply (simp add: add_assoc del: add_0_right)
   1.716 +  done
   1.717 +
   1.718 +subsection {* Additional theorems about "less than" *}
   1.719 +
   1.720 +text {* Deleted @{text less_natE}; instead use @{text "less_imp_Suc_add RS exE"} *}
   1.721 +lemma less_imp_Suc_add: "m < n ==> (EX k. n = Suc (m + k))"
   1.722 +  apply (induct n)
   1.723 +  apply (simp_all add: order_le_less)
   1.724 +  apply (blast elim!: less_SucE intro!: add_0_right [symmetric] add_Suc_right [symmetric])
   1.725 +  done
   1.726 +
   1.727 +lemma le_add2: "n <= ((m + n)::nat)"
   1.728 +  apply (induct m)
   1.729 +  apply simp_all
   1.730 +  apply (erule le_SucI)
   1.731 +  done
   1.732 +
   1.733 +lemma le_add1: "n <= ((n + m)::nat)"
   1.734 +  apply (simp add: add_ac)
   1.735 +  apply (rule le_add2)
   1.736 +  done
   1.737 +
   1.738 +lemma less_add_Suc1: "i < Suc (i + m)"
   1.739 +  by (rule le_less_trans, rule le_add1, rule lessI)
   1.740 +
   1.741 +lemma less_add_Suc2: "i < Suc (m + i)"
   1.742 +  by (rule le_less_trans, rule le_add2, rule lessI)
   1.743 +
   1.744 +lemma less_iff_Suc_add: "(m < n) = (EX k. n = Suc (m + k))"
   1.745 +  by (rules intro!: less_add_Suc1 less_imp_Suc_add)
   1.746 +
   1.747 +
   1.748 +lemma trans_le_add1: "(i::nat) <= j ==> i <= j + m"
   1.749 +  by (rule le_trans, assumption, rule le_add1)
   1.750 +
   1.751 +lemma trans_le_add2: "(i::nat) <= j ==> i <= m + j"
   1.752 +  by (rule le_trans, assumption, rule le_add2)
   1.753 +
   1.754 +lemma trans_less_add1: "(i::nat) < j ==> i < j + m"
   1.755 +  by (rule less_le_trans, assumption, rule le_add1)
   1.756 +
   1.757 +lemma trans_less_add2: "(i::nat) < j ==> i < m + j"
   1.758 +  by (rule less_le_trans, assumption, rule le_add2)
   1.759 +
   1.760 +lemma add_lessD1: "i + j < (k::nat) ==> i < k"
   1.761 +  apply (induct j)
   1.762 +  apply simp_all
   1.763 +  apply (blast dest: Suc_lessD)
   1.764 +  done
   1.765 +
   1.766 +lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
   1.767 +  apply (rule notI)
   1.768 +  apply (erule add_lessD1 [THEN less_irrefl])
   1.769 +  done
   1.770 +
   1.771 +lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
   1.772 +  by (simp add: add_commute not_add_less1)
   1.773 +
   1.774 +lemma add_leD1: "m + k <= n ==> m <= (n::nat)"
   1.775 +  by (induct k) (simp_all add: le_simps)
   1.776 +
   1.777 +lemma add_leD2: "m + k <= n ==> k <= (n::nat)"
   1.778 +  apply (simp add: add_commute)
   1.779 +  apply (erule add_leD1)
   1.780 +  done
   1.781 +
   1.782 +lemma add_leE: "(m::nat) + k <= n ==> (m <= n ==> k <= n ==> R) ==> R"
   1.783 +  by (blast dest: add_leD1 add_leD2)
   1.784 +
   1.785 +text {* needs @{text "!!k"} for @{text add_ac} to work *}
   1.786 +lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
   1.787 +  by (force simp del: add_Suc_right
   1.788 +    simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
   1.789 +
   1.790 +
   1.791 +subsection {* Monotonicity of Addition *}
   1.792 +
   1.793 +text {* strict, in 1st argument *}
   1.794 +lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   1.795 +  by (induct k) simp_all
   1.796 +
   1.797 +text {* strict, in both arguments *}
   1.798 +lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   1.799 +  apply (rule add_less_mono1 [THEN less_trans])
   1.800 +  apply assumption+
   1.801 +  apply (induct_tac j)
   1.802 +  apply simp_all
   1.803 +  done
   1.804 +
   1.805 +text {* A [clumsy] way of lifting @{text "<"}
   1.806 +  monotonicity to @{text "<="} monotonicity *}
   1.807 +lemma less_mono_imp_le_mono:
   1.808 +  assumes lt_mono: "!!i j::nat. i < j ==> f i < f j"
   1.809 +  and le: "i <= j" shows "f i <= ((f j)::nat)" using le
   1.810 +  apply (simp add: order_le_less)
   1.811 +  apply (blast intro!: lt_mono)
   1.812 +  done
   1.813 +
   1.814 +text {* non-strict, in 1st argument *}
   1.815 +lemma add_le_mono1: "i <= j ==> i + k <= j + (k::nat)"
   1.816 +  apply (rule_tac f = "%j. j + k" in less_mono_imp_le_mono)
   1.817 +  apply (erule add_less_mono1)
   1.818 +  apply assumption
   1.819 +  done
   1.820  
   1.821 -primrec
   1.822 -  diff_0   "m - 0 = m"
   1.823 -  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
   1.824 +text {* non-strict, in both arguments *}
   1.825 +lemma add_le_mono: "[| i <= j;  k <= l |] ==> i + k <= j + (l::nat)"
   1.826 +  apply (erule add_le_mono1 [THEN le_trans])
   1.827 +  apply (simp add: add_commute)
   1.828 +  done
   1.829 +
   1.830 +
   1.831 +subsection {* Multiplication *}
   1.832 +
   1.833 +text {* right annihilation in product *}
   1.834 +lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
   1.835 +  by (induct m) simp_all
   1.836 +
   1.837 +text {* right successor law for multiplication *}
   1.838 +lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   1.839 +  by (induct m) (simp_all add: add_ac)
   1.840 +
   1.841 +lemma mult_1: "(1::nat) * n = n" by simp
   1.842 +
   1.843 +lemma mult_1_right: "n * (1::nat) = n" by simp
   1.844 +
   1.845 +text {* Commutative law for multiplication *}
   1.846 +lemma mult_commute: "m * n = n * (m::nat)"
   1.847 +  by (induct m) simp_all
   1.848 +
   1.849 +text {* addition distributes over multiplication *}
   1.850 +lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
   1.851 +  by (induct m) (simp_all add: add_ac)
   1.852 +
   1.853 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   1.854 +  by (induct m) (simp_all add: add_ac)
   1.855 +
   1.856 +text {* Associative law for multiplication *}
   1.857 +lemma mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
   1.858 +  by (induct m) (simp_all add: add_mult_distrib)
   1.859 +
   1.860 +lemma mult_left_commute: "x * (y * z) = y * ((x * z)::nat)"
   1.861 +  apply (rule mk_left_commute [of "op *"])
   1.862 +  apply (rule mult_assoc)
   1.863 +  apply (rule mult_commute)
   1.864 +  done
   1.865 +
   1.866 +lemmas mult_ac = mult_assoc mult_commute mult_left_commute
   1.867 +
   1.868 +lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   1.869 +  apply (induct_tac m)
   1.870 +  apply (induct_tac [2] n)
   1.871 +  apply simp_all
   1.872 +  done
   1.873 +
   1.874 +
   1.875 +subsection {* Difference *}
   1.876 +
   1.877 +lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
   1.878 +  by (induct m) simp_all
   1.879 +
   1.880 +text {* Addition is the inverse of subtraction:
   1.881 +  if @{term "n <= m"} then @{term "n + (m - n) = m"}. *}
   1.882 +lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
   1.883 +  by (induct m n rule: diff_induct) simp_all
   1.884 +
   1.885 +lemma le_add_diff_inverse [simp]: "n <= m ==> n + (m - n) = (m::nat)"
   1.886 +  by (simp add: add_diff_inverse not_less_iff_le)
   1.887 +
   1.888 +lemma le_add_diff_inverse2 [simp]: "n <= m ==> (m - n) + n = (m::nat)"
   1.889 +  by (simp add: le_add_diff_inverse add_commute)
   1.890 +
   1.891 +
   1.892 +subsection {* More results about difference *}
   1.893 +
   1.894 +lemma Suc_diff_le: "n <= m ==> Suc m - n = Suc (m - n)"
   1.895 +  by (induct m n rule: diff_induct) simp_all
   1.896 +
   1.897 +lemma diff_less_Suc: "m - n < Suc m"
   1.898 +  apply (induct m n rule: diff_induct)
   1.899 +  apply (erule_tac [3] less_SucE)
   1.900 +  apply (simp_all add: less_Suc_eq)
   1.901 +  done
   1.902 +
   1.903 +lemma diff_le_self [simp]: "m - n <= (m::nat)"
   1.904 +  by (induct m n rule: diff_induct) (simp_all add: le_SucI)
   1.905 +
   1.906 +lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
   1.907 +  by (rule le_less_trans, rule diff_le_self)
   1.908 +
   1.909 +lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)"
   1.910 +  by (induct i j rule: diff_induct) simp_all
   1.911 +
   1.912 +lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
   1.913 +  by (simp add: diff_diff_left)
   1.914 +
   1.915 +lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n"
   1.916 +  apply (case_tac "n")
   1.917 +  apply safe
   1.918 +  apply (simp add: le_simps)
   1.919 +  done
   1.920 +
   1.921 +text {* This and the next few suggested by Florian Kammueller *}
   1.922 +lemma diff_commute: "(i::nat) - j - k = i - k - j"
   1.923 +  by (simp add: diff_diff_left add_commute)
   1.924 +
   1.925 +lemma diff_add_assoc: "k <= (j::nat) ==> (i + j) - k = i + (j - k)"
   1.926 +  by (induct j k rule: diff_induct) simp_all
   1.927 +
   1.928 +lemma diff_add_assoc2: "k <= (j::nat) ==> (j + i) - k = (j - k) + i"
   1.929 +  by (simp add: add_commute diff_add_assoc)
   1.930 +
   1.931 +lemma diff_add_inverse: "(n + m) - n = (m::nat)"
   1.932 +  by (induct n) simp_all
   1.933 +
   1.934 +lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
   1.935 +  by (simp add: diff_add_assoc)
   1.936 +
   1.937 +lemma le_imp_diff_is_add: "i <= (j::nat) ==> (j - i = k) = (j = k + i)"
   1.938 +  apply safe
   1.939 +  apply (simp_all add: diff_add_inverse2)
   1.940 +  done
   1.941 +
   1.942 +lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m <= n)"
   1.943 +  by (induct m n rule: diff_induct) simp_all
   1.944 +
   1.945 +lemma diff_is_0_eq' [simp]: "m <= n ==> (m::nat) - n = 0"
   1.946 +  by (rule iffD2, rule diff_is_0_eq)
   1.947 +
   1.948 +lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)"
   1.949 +  by (induct m n rule: diff_induct) simp_all
   1.950 +
   1.951 +lemma less_imp_add_positive: "i < j  ==> EX k::nat. 0 < k & i + k = j"
   1.952 +  apply (rule_tac x = "j - i" in exI)
   1.953 +  apply (simp (no_asm_simp) add: add_diff_inverse less_not_sym)
   1.954 +  done
   1.955  
   1.956 -primrec
   1.957 -  mult_0   "0 * n = 0"
   1.958 -  mult_Suc "Suc m * n = n + (m * n)"
   1.959 +lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
   1.960 +  apply (induct k i rule: diff_induct)
   1.961 +  apply (simp_all (no_asm))
   1.962 +  apply rules
   1.963 +  done
   1.964 +
   1.965 +lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   1.966 +  apply (rule diff_self_eq_0 [THEN subst])
   1.967 +  apply (rule zero_induct_lemma)
   1.968 +  apply rules+
   1.969 +  done
   1.970 +
   1.971 +lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
   1.972 +  by (induct k) simp_all
   1.973 +
   1.974 +lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
   1.975 +  by (simp add: diff_cancel add_commute)
   1.976 +
   1.977 +lemma diff_add_0: "n - (n + m) = (0::nat)"
   1.978 +  by (induct n) simp_all
   1.979 +
   1.980 +
   1.981 +text {* Difference distributes over multiplication *}
   1.982 +
   1.983 +lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
   1.984 +  by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
   1.985 +
   1.986 +lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
   1.987 +  by (simp add: diff_mult_distrib mult_commute [of k])
   1.988 +  -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
   1.989 +
   1.990 +lemmas nat_distrib =
   1.991 +  add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
   1.992 +
   1.993 +
   1.994 +subsection {* Monotonicity of Multiplication *}
   1.995 +
   1.996 +lemma mult_le_mono1: "i <= (j::nat) ==> i * k <= j * k"
   1.997 +  by (induct k) (simp_all add: add_le_mono)
   1.998 +
   1.999 +lemma mult_le_mono2: "i <= (j::nat) ==> k * i <= k * j"
  1.1000 +  apply (drule mult_le_mono1)
  1.1001 +  apply (simp add: mult_commute)
  1.1002 +  done
  1.1003 +
  1.1004 +text {* @{text "<="} monotonicity, BOTH arguments *}
  1.1005 +lemma mult_le_mono: "i <= (j::nat) ==> k <= l ==> i * k <= j * l"
  1.1006 +  apply (erule mult_le_mono1 [THEN le_trans])
  1.1007 +  apply (erule mult_le_mono2)
  1.1008 +  done
  1.1009 +
  1.1010 +text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
  1.1011 +lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
  1.1012 +  apply (erule_tac m1 = "0" in less_imp_Suc_add [THEN exE])
  1.1013 +  apply simp
  1.1014 +  apply (induct_tac x)
  1.1015 +  apply (simp_all add: add_less_mono)
  1.1016 +  done
  1.1017 +
  1.1018 +lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
  1.1019 +  by (drule mult_less_mono2) (simp_all add: mult_commute)
  1.1020 +
  1.1021 +lemma zero_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
  1.1022 +  apply (induct m)
  1.1023 +  apply (case_tac [2] n)
  1.1024 +  apply simp_all
  1.1025 +  done
  1.1026 +
  1.1027 +lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)"
  1.1028 +  apply (induct m)
  1.1029 +  apply (case_tac [2] n)
  1.1030 +  apply simp_all
  1.1031 +  done
  1.1032 +
  1.1033 +lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
  1.1034 +  apply (induct_tac m)
  1.1035 +  apply simp
  1.1036 +  apply (induct_tac n)
  1.1037 +  apply simp
  1.1038 +  apply fastsimp
  1.1039 +  done
  1.1040 +
  1.1041 +lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
  1.1042 +  apply (rule trans)
  1.1043 +  apply (rule_tac [2] mult_eq_1_iff)
  1.1044 +  apply fastsimp
  1.1045 +  done
  1.1046 +
  1.1047 +lemma mult_less_cancel2: "((m::nat) * k < n * k) = (0 < k & m < n)"
  1.1048 +  apply (safe intro!: mult_less_mono1)
  1.1049 +  apply (case_tac k)
  1.1050 +  apply auto
  1.1051 +  apply (simp del: le_0_eq add: linorder_not_le [symmetric])
  1.1052 +  apply (blast intro: mult_le_mono1)
  1.1053 +  done
  1.1054 +
  1.1055 +lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
  1.1056 +  by (simp add: mult_less_cancel2 mult_commute [of k])
  1.1057 +
  1.1058 +declare mult_less_cancel2 [simp]
  1.1059 +
  1.1060 +lemma mult_le_cancel1 [simp]: "(k * (m::nat) <= k * n) = (0 < k --> m <= n)"
  1.1061 +  apply (simp add: linorder_not_less [symmetric])
  1.1062 +  apply auto
  1.1063 +  done
  1.1064 +
  1.1065 +lemma mult_le_cancel2 [simp]: "((m::nat) * k <= n * k) = (0 < k --> m <= n)"
  1.1066 +  apply (simp add: linorder_not_less [symmetric])
  1.1067 +  apply auto
  1.1068 +  done
  1.1069 +
  1.1070 +lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))"
  1.1071 +  apply (cut_tac less_linear)
  1.1072 +  apply safe
  1.1073 +  apply auto
  1.1074 +  apply (drule mult_less_mono1, assumption, simp)+
  1.1075 +  done
  1.1076 +
  1.1077 +lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
  1.1078 +  by (simp add: mult_cancel2 mult_commute [of k])
  1.1079 +
  1.1080 +declare mult_cancel2 [simp]
  1.1081 +
  1.1082 +lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
  1.1083 +  by (subst mult_less_cancel1) simp
  1.1084 +
  1.1085 +lemma Suc_mult_le_cancel1: "(Suc k * m <= Suc k * n) = (m <= n)"
  1.1086 +  by (subst mult_le_cancel1) simp
  1.1087 +
  1.1088 +lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
  1.1089 +  by (subst mult_cancel1) simp
  1.1090 +
  1.1091 +
  1.1092 +text {* Lemma for @{text gcd} *}
  1.1093 +lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
  1.1094 +  apply (drule sym)
  1.1095 +  apply (rule disjCI)
  1.1096 +  apply (rule nat_less_cases, erule_tac [2] _)
  1.1097 +  apply (fastsimp elim!: less_SucE)
  1.1098 +  apply (fastsimp dest: mult_less_mono2)
  1.1099 +  done
  1.1100  
  1.1101  end