<= and < on nat no longer depend on wellfounded relations
authorhaftmann
Fri Feb 15 16:09:12 2008 +0100 (2008-02-15)
changeset 26072f65a7fa2da6c
parent 26071 046fe7ddfc4b
child 26073 0e70d3bd2eb4
<= and < on nat no longer depend on wellfounded relations
NEWS
src/HOL/Complex/ex/NSPrimes.thy
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Int.thy
src/HOL/Library/Permutation.thy
src/HOL/Nat.thy
src/HOL/Relation_Power.thy
src/HOL/SetInterval.thy
src/HOL/Wellfounded_Recursion.thy
src/HOL/Wellfounded_Relations.thy
src/HOL/Word/Num_Lemmas.thy
src/HOL/Word/WordShift.thy
src/HOL/ex/Primrec.thy
     1.1 --- a/NEWS	Fri Feb 15 16:09:10 2008 +0100
     1.2 +++ b/NEWS	Fri Feb 15 16:09:12 2008 +0100
     1.3 @@ -35,10 +35,15 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Nat: definition of <= and < on natural numbers no longer depend
     1.8 +on well-founded relations.  INCOMPATIBILITY.  Definitions le_def and less_def
     1.9 +have disappeared.  Consider lemmas not_less [symmetric, where ?'a = nat]
    1.10 +and less_eq [symmetric] instead.
    1.11 +
    1.12  * Theory Finite_Set: locales ACf, ACIf, ACIfSL and ACIfSLlin (whose purpose 
    1.13  mainly if for various fold_set functionals) have been abandoned in favour of
    1.14  the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult,
    1.15 -lower_semilattice (resp. uper_semilattice) and linorder.  INCOMPATIBILITY.
    1.16 +lower_semilattice (resp. upper_semilattice) and linorder.  INCOMPATIBILITY.
    1.17  
    1.18  * Theorem Inductive.lfp_ordinal_induct generalized to complete lattices.  The
    1.19  form set-specific version is available as Inductive.lfp_ordinal_induct_set.
     2.1 --- a/src/HOL/Complex/ex/NSPrimes.thy	Fri Feb 15 16:09:10 2008 +0100
     2.2 +++ b/src/HOL/Complex/ex/NSPrimes.thy	Fri Feb 15 16:09:12 2008 +0100
     2.3 @@ -113,7 +113,7 @@
     2.4  by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite)
     2.5  
     2.6  lemma not_finite_nat_set_iff: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n <= (i::nat))"
     2.7 -by (auto simp add: finite_nat_set_bounded_iff le_def)
     2.8 +by (auto simp add: finite_nat_set_bounded_iff not_less)
     2.9  
    2.10  lemma bounded_nat_set_is_finite2: "(\<forall>i \<in> N. i<=(n::nat)) ==> finite N"
    2.11  apply (rule finite_subset)
    2.12 @@ -129,7 +129,7 @@
    2.13  by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2)
    2.14  
    2.15  lemma not_finite_nat_set_iff2: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n < (i::nat))"
    2.16 -by (auto simp add: finite_nat_set_bounded_iff2 le_def)
    2.17 +by (auto simp add: finite_nat_set_bounded_iff2 not_le)
    2.18  
    2.19  
    2.20  subsection{*An injective function cannot define an embedded natural number*}
     3.1 --- a/src/HOL/Datatype.thy	Fri Feb 15 16:09:10 2008 +0100
     3.2 +++ b/src/HOL/Datatype.thy	Fri Feb 15 16:09:12 2008 +0100
     3.3 @@ -12,6 +12,11 @@
     3.4  imports Finite_Set
     3.5  begin
     3.6  
     3.7 +lemma size_bool [code func]:
     3.8 +  "size (b\<Colon>bool) = 0" by (cases b) auto
     3.9 +
    3.10 +declare "prod.size" [noatp]
    3.11 +
    3.12  typedef (Node)
    3.13    ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    3.14      --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
     4.1 --- a/src/HOL/Divides.thy	Fri Feb 15 16:09:10 2008 +0100
     4.2 +++ b/src/HOL/Divides.thy	Fri Feb 15 16:09:12 2008 +0100
     4.3 @@ -7,7 +7,7 @@
     4.4  header {* The division operators div, mod and the divides relation "dvd" *}
     4.5  
     4.6  theory Divides
     4.7 -imports Power
     4.8 +imports Power Wellfounded_Recursion
     4.9  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Feb 15 16:09:10 2008 +0100
     5.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Feb 15 16:09:12 2008 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     5.5  
     5.6  theory Hilbert_Choice
     5.7 -imports Nat
     5.8 +imports Nat Wellfounded_Recursion
     5.9  uses ("Tools/meson.ML") ("Tools/specification_package.ML")
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Feb 15 16:09:10 2008 +0100
     6.2 +++ b/src/HOL/Hyperreal/Integration.thy	Fri Feb 15 16:09:12 2008 +0100
     6.3 @@ -560,7 +560,7 @@
     6.4  apply (drule_tac n = m in partition_lt_gen, auto)
     6.5  apply (frule partition_eq_bound)
     6.6  apply (drule_tac [2] partition_gt, auto)
     6.7 -apply (metis dense_linear_order_class.dlo_simps(8) le_def partition_rhs partition_rhs2)
     6.8 +apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2)
     6.9  apply (metis Nat.le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
    6.10  done
    6.11  
     7.1 --- a/src/HOL/Int.thy	Fri Feb 15 16:09:10 2008 +0100
     7.2 +++ b/src/HOL/Int.thy	Fri Feb 15 16:09:12 2008 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4  header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     7.5  
     7.6  theory Int
     7.7 -imports Equiv_Relations Wellfounded_Relations Datatype Nat
     7.8 +imports Equiv_Relations Datatype Nat Wellfounded_Relations
     7.9  uses
    7.10    ("Tools/numeral.ML")
    7.11    ("Tools/numeral_syntax.ML")
     8.1 --- a/src/HOL/Library/Permutation.thy	Fri Feb 15 16:09:10 2008 +0100
     8.2 +++ b/src/HOL/Library/Permutation.thy	Fri Feb 15 16:09:12 2008 +0100
     8.3 @@ -188,7 +188,7 @@
     8.4     apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
     8.5      apply (fastsimp simp add: insert_ident)
     8.6     apply (metis distinct_remdups set_remdups)
     8.7 -  apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
     8.8 +  apply (metis Nat.le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
     8.9    done
    8.10  
    8.11  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
     9.1 --- a/src/HOL/Nat.thy	Fri Feb 15 16:09:10 2008 +0100
     9.2 +++ b/src/HOL/Nat.thy	Fri Feb 15 16:09:12 2008 +0100
     9.3 @@ -9,14 +9,13 @@
     9.4  header {* Natural numbers *}
     9.5  
     9.6  theory Nat
     9.7 -imports Wellfounded_Recursion Ring_and_Field
     9.8 +imports Inductive Ring_and_Field
     9.9  uses
    9.10    "~~/src/Tools/rat.ML"
    9.11    "~~/src/Provers/Arith/cancel_sums.ML"
    9.12    ("arith_data.ML")
    9.13    "~~/src/Provers/Arith/fast_lin_arith.ML"
    9.14    ("Tools/lin_arith.ML")
    9.15 -  ("Tools/function_package/size.ML")
    9.16  begin
    9.17  
    9.18  subsection {* Type @{text ind} *}
    9.19 @@ -36,21 +35,20 @@
    9.20  
    9.21  text {* Type definition *}
    9.22  
    9.23 -inductive_set Nat :: "ind set"
    9.24 +inductive Nat :: "ind \<Rightarrow> bool"
    9.25  where
    9.26 -    Zero_RepI: "Zero_Rep : Nat"
    9.27 -  | Suc_RepI: "i : Nat ==> Suc_Rep i : Nat"
    9.28 +    Zero_RepI: "Nat Zero_Rep"
    9.29 +  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    9.30  
    9.31  global
    9.32  
    9.33  typedef (open Nat)
    9.34 -  nat = Nat
    9.35 -proof
    9.36 -  show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
    9.37 -qed
    9.38 +  nat = "Collect Nat"
    9.39 +  by (rule exI, rule CollectI, rule Nat.Zero_RepI)
    9.40  
    9.41 -consts
    9.42 +constdefs
    9.43    Suc :: "nat => nat"
    9.44 +  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    9.45  
    9.46  local
    9.47  
    9.48 @@ -64,28 +62,26 @@
    9.49  
    9.50  end
    9.51  
    9.52 -defs
    9.53 -  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    9.54 -
    9.55 -theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
    9.56 +lemma nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
    9.57    apply (unfold Zero_nat_def Suc_def)
    9.58    apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    9.59 -  apply (erule Rep_Nat [THEN Nat.induct])
    9.60 -  apply (iprover elim: Abs_Nat_inverse [THEN subst])
    9.61 +  apply (erule Rep_Nat [THEN CollectD, THEN Nat.induct])
    9.62 +  apply (iprover elim: Abs_Nat_inverse [OF CollectI, THEN subst])
    9.63    done
    9.64  
    9.65  lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
    9.66 -  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI
    9.67 -                Suc_Rep_not_Zero_Rep)
    9.68 +  by (simp add: Zero_nat_def Suc_def
    9.69 +    Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI Zero_RepI
    9.70 +      Suc_Rep_not_Zero_Rep)
    9.71  
    9.72  lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
    9.73    by (rule not_sym, rule Suc_not_Zero not_sym)
    9.74  
    9.75  lemma inj_Suc[simp]: "inj_on Suc N"
    9.76 -  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI
    9.77 +  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI
    9.78                  inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    9.79  
    9.80 -lemma Suc_Suc_eq [iff]: "(Suc m = Suc n) = (m = n)"
    9.81 +lemma Suc_Suc_eq [iff]: "Suc m = Suc n \<longleftrightarrow> m = n"
    9.82    by (rule inj_Suc [THEN inj_eq])
    9.83  
    9.84  rep_datatype nat
    9.85 @@ -105,29 +101,25 @@
    9.86  
    9.87  text {* Injectiveness and distinctness lemmas *}
    9.88  
    9.89 -lemma Suc_neq_Zero: "Suc m = 0 ==> R"
    9.90 +lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
    9.91  by (rule notE, rule Suc_not_Zero)
    9.92  
    9.93 -lemma Zero_neq_Suc: "0 = Suc m ==> R"
    9.94 +lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R"
    9.95  by (rule Suc_neq_Zero, erule sym)
    9.96  
    9.97 -lemma Suc_inject: "Suc x = Suc y ==> x = y"
    9.98 +lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y"
    9.99  by (rule inj_Suc [THEN injD])
   9.100  
   9.101 -lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
   9.102 -by auto
   9.103 -
   9.104  lemma n_not_Suc_n: "n \<noteq> Suc n"
   9.105  by (induct n) simp_all
   9.106  
   9.107 -lemma Suc_n_not_n: "Suc t \<noteq> t"
   9.108 +lemma Suc_n_not_n: "Suc n \<noteq> n"
   9.109  by (rule not_sym, rule n_not_Suc_n)
   9.110  
   9.111 -
   9.112  text {* A special form of induction for reasoning
   9.113    about @{term "m < n"} and @{term "m - n"} *}
   9.114  
   9.115 -theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
   9.116 +lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
   9.117      (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
   9.118    apply (rule_tac x = m in spec)
   9.119    apply (induct n)
   9.120 @@ -139,96 +131,317 @@
   9.121  
   9.122  subsection {* Arithmetic operators *}
   9.123  
   9.124 -instantiation nat :: "{one, plus, minus, times}"
   9.125 +instantiation nat :: "{minus, comm_monoid_add}"
   9.126  begin
   9.127  
   9.128 -definition
   9.129 -  One_nat_def [simp]: "1 = Suc 0"
   9.130 -
   9.131  primrec plus_nat
   9.132  where
   9.133    add_0:      "0 + n = (n\<Colon>nat)"
   9.134    | add_Suc:  "Suc m + n = Suc (m + n)"
   9.135  
   9.136 +lemma add_0_right [simp]: "m + 0 = (m::nat)"
   9.137 +  by (induct m) simp_all
   9.138 +
   9.139 +lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   9.140 +  by (induct m) simp_all
   9.141 +
   9.142 +lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   9.143 +  by simp
   9.144 +
   9.145  primrec minus_nat
   9.146  where
   9.147    diff_0:     "m - 0 = (m\<Colon>nat)"
   9.148    | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
   9.149  
   9.150 +declare diff_Suc [simp del, code del]
   9.151 +
   9.152 +lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
   9.153 +  by (induct n) (simp_all add: diff_Suc)
   9.154 +
   9.155 +lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n"
   9.156 +  by (induct n) (simp_all add: diff_Suc)
   9.157 +
   9.158 +instance proof
   9.159 +  fix n m q :: nat
   9.160 +  show "(n + m) + q = n + (m + q)" by (induct n) simp_all
   9.161 +  show "n + m = m + n" by (induct n) simp_all
   9.162 +  show "0 + n = n" by simp
   9.163 +qed
   9.164 +
   9.165 +end
   9.166 +
   9.167 +instantiation nat :: comm_semiring_1_cancel
   9.168 +begin
   9.169 +
   9.170 +definition
   9.171 +  One_nat_def [simp]: "1 = Suc 0"
   9.172 +
   9.173  primrec times_nat
   9.174  where
   9.175    mult_0:     "0 * n = (0\<Colon>nat)"
   9.176    | mult_Suc: "Suc m * n = n + (m * n)"
   9.177  
   9.178 -instance ..
   9.179 +lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
   9.180 +  by (induct m) simp_all
   9.181 +
   9.182 +lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   9.183 +  by (induct m) (simp_all add: add_left_commute)
   9.184 +
   9.185 +lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
   9.186 +  by (induct m) (simp_all add: add_assoc)
   9.187 +
   9.188 +instance proof
   9.189 +  fix n m q :: nat
   9.190 +  show "0 \<noteq> (1::nat)" by simp
   9.191 +  show "1 * n = n" by simp
   9.192 +  show "n * m = m * n" by (induct n) simp_all
   9.193 +  show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
   9.194 +  show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
   9.195 +  assume "n + m = n + q" thus "m = q" by (induct n) simp_all
   9.196 +qed
   9.197  
   9.198  end
   9.199  
   9.200 +subsubsection {* Addition *}
   9.201 +
   9.202 +lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
   9.203 +  by (rule add_assoc)
   9.204 +
   9.205 +lemma nat_add_commute: "m + n = n + (m::nat)"
   9.206 +  by (rule add_commute)
   9.207 +
   9.208 +lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   9.209 +  by (rule add_left_commute)
   9.210 +
   9.211 +lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
   9.212 +  by (rule add_left_cancel)
   9.213 +
   9.214 +lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
   9.215 +  by (rule add_right_cancel)
   9.216 +
   9.217 +text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
   9.218 +
   9.219 +lemma add_is_0 [iff]:
   9.220 +  fixes m n :: nat
   9.221 +  shows "(m + n = 0) = (m = 0 & n = 0)"
   9.222 +  by (cases m) simp_all
   9.223 +
   9.224 +lemma add_is_1:
   9.225 +  "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
   9.226 +  by (cases m) simp_all
   9.227 +
   9.228 +lemma one_is_add:
   9.229 +  "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   9.230 +  by (rule trans, rule eq_commute, rule add_is_1)
   9.231 +
   9.232 +lemma add_eq_self_zero:
   9.233 +  fixes m n :: nat
   9.234 +  shows "m + n = m \<Longrightarrow> n = 0"
   9.235 +  by (induct m) simp_all
   9.236 +
   9.237 +lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N"
   9.238 +  apply (induct k)
   9.239 +   apply simp
   9.240 +  apply(drule comp_inj_on[OF _ inj_Suc])
   9.241 +  apply (simp add:o_def)
   9.242 +  done
   9.243 +
   9.244 +
   9.245 +subsubsection {* Difference *}
   9.246 +
   9.247 +lemma diff_self_eq_0 [simp]: "(m\<Colon>nat) - m = 0"
   9.248 +  by (induct m) simp_all
   9.249 +
   9.250 +lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)"
   9.251 +  by (induct i j rule: diff_induct) simp_all
   9.252 +
   9.253 +lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
   9.254 +  by (simp add: diff_diff_left)
   9.255 +
   9.256 +lemma diff_commute: "(i::nat) - j - k = i - k - j"
   9.257 +  by (simp add: diff_diff_left add_commute)
   9.258 +
   9.259 +lemma diff_add_inverse: "(n + m) - n = (m::nat)"
   9.260 +  by (induct n) simp_all
   9.261 +
   9.262 +lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
   9.263 +  by (simp add: diff_add_inverse add_commute [of m n])
   9.264 +
   9.265 +lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
   9.266 +  by (induct k) simp_all
   9.267 +
   9.268 +lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
   9.269 +  by (simp add: diff_cancel add_commute)
   9.270 +
   9.271 +lemma diff_add_0: "n - (n + m) = (0::nat)"
   9.272 +  by (induct n) simp_all
   9.273 +
   9.274 +text {* Difference distributes over multiplication *}
   9.275 +
   9.276 +lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
   9.277 +by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
   9.278 +
   9.279 +lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
   9.280 +by (simp add: diff_mult_distrib mult_commute [of k])
   9.281 +  -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
   9.282 +
   9.283 +
   9.284 +subsubsection {* Multiplication *}
   9.285 +
   9.286 +lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
   9.287 +  by (rule mult_assoc)
   9.288 +
   9.289 +lemma nat_mult_commute: "m * n = n * (m::nat)"
   9.290 +  by (rule mult_commute)
   9.291 +
   9.292 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   9.293 +  by (rule right_distrib)
   9.294 +
   9.295 +lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   9.296 +  by (induct m) auto
   9.297 +
   9.298 +lemmas nat_distrib =
   9.299 +  add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
   9.300 +
   9.301 +lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
   9.302 +  apply (induct m)
   9.303 +   apply simp
   9.304 +  apply (induct n)
   9.305 +   apply auto
   9.306 +  done
   9.307 +
   9.308 +lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
   9.309 +  apply (rule trans)
   9.310 +  apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   9.311 +  done
   9.312 +
   9.313 +lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
   9.314 +proof -
   9.315 +  have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
   9.316 +  proof (induct n arbitrary: m)
   9.317 +    case 0 then show "m = 0" by simp
   9.318 +  next
   9.319 +    case (Suc n) then show "m = Suc n"
   9.320 +      by (cases m) (simp_all add: eq_commute [of "0"])
   9.321 +  qed
   9.322 +  then show ?thesis by auto
   9.323 +qed
   9.324 +
   9.325 +lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   9.326 +  by (simp add: mult_commute)
   9.327 +
   9.328 +lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
   9.329 +  by (subst mult_cancel1) simp
   9.330 +
   9.331  
   9.332  subsection {* Orders on @{typ nat} *}
   9.333  
   9.334 -definition
   9.335 -  pred_nat :: "(nat * nat) set" where
   9.336 -  "pred_nat = {(m, n). n = Suc m}"
   9.337 +subsubsection {* Operation definition *}
   9.338  
   9.339 -instantiation nat :: ord
   9.340 +instantiation nat :: linorder
   9.341  begin
   9.342  
   9.343 -definition
   9.344 -  less_def [code func del]: "m < n \<longleftrightarrow> (m, n) : pred_nat^+"
   9.345 +primrec less_eq_nat where
   9.346 +  "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
   9.347 +  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
   9.348 +
   9.349 +declare less_eq_nat.simps [simp del, code del]
   9.350 +lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
   9.351 +lemma le0 [iff]: "0 \<le> (n\<Colon>nat)" by (simp add: less_eq_nat.simps)
   9.352 +
   9.353 +definition less_nat where
   9.354 +  less_eq_Suc_le [code func del]: "n < m \<longleftrightarrow> Suc n \<le> m"
   9.355 +
   9.356 +lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m"
   9.357 +  by (simp add: less_eq_nat.simps(2))
   9.358 +
   9.359 +lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n"
   9.360 +  unfolding less_eq_Suc_le ..
   9.361 +
   9.362 +lemma le_0_eq [iff]: "(n\<Colon>nat) \<le> 0 \<longleftrightarrow> n = 0"
   9.363 +  by (induct n) (simp_all add: less_eq_nat.simps(2))
   9.364 +
   9.365 +lemma not_less0 [iff]: "\<not> n < (0\<Colon>nat)"
   9.366 +  by (simp add: less_eq_Suc_le)
   9.367 +
   9.368 +lemma less_nat_zero_code [code]: "n < (0\<Colon>nat) \<longleftrightarrow> False"
   9.369 +  by simp
   9.370 +
   9.371 +lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n"
   9.372 +  by (simp add: less_eq_Suc_le)
   9.373 +
   9.374 +lemma less_Suc_eq_le [code]: "m < Suc n \<longleftrightarrow> m \<le> n"
   9.375 +  by (simp add: less_eq_Suc_le)
   9.376 +
   9.377 +lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n"
   9.378 +  by (induct m arbitrary: n)
   9.379 +    (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   9.380 +
   9.381 +lemma Suc_leD: "Suc m \<le> n \<Longrightarrow> m \<le> n"
   9.382 +  by (cases n) (auto intro: le_SucI)
   9.383 +
   9.384 +lemma less_SucI: "m < n \<Longrightarrow> m < Suc n"
   9.385 +  by (simp add: less_eq_Suc_le) (erule Suc_leD)
   9.386  
   9.387 -definition
   9.388 -  le_def [code func del]:   "m \<le> (n\<Colon>nat) \<longleftrightarrow> \<not> n < m"
   9.389 +lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n"
   9.390 +  by (simp add: less_eq_Suc_le) (erule Suc_leD)
   9.391  
   9.392 -instance ..
   9.393 +instance proof
   9.394 +  fix n m :: nat
   9.395 +  have less_imp_le: "n < m \<Longrightarrow> n \<le> m"
   9.396 +    unfolding less_eq_Suc_le by (erule Suc_leD)
   9.397 +  have irrefl: "\<not> m < m" by (induct m) auto
   9.398 +  have strict: "n \<le> m \<Longrightarrow> n \<noteq> m \<Longrightarrow> n < m"
   9.399 +  proof (induct n arbitrary: m)
   9.400 +    case 0 then show ?case
   9.401 +      by (cases m) (simp_all add: less_eq_Suc_le)
   9.402 +  next
   9.403 +    case (Suc n) then show ?case
   9.404 +      by (cases m) (simp_all add: less_eq_Suc_le)
   9.405 +  qed
   9.406 +  show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
   9.407 +    by (auto simp add: irrefl intro: less_imp_le strict)
   9.408 +next
   9.409 +  fix n :: nat show "n \<le> n" by (induct n) simp_all
   9.410 +next
   9.411 +  fix n m :: nat assume "n \<le> m" and "m \<le> n"
   9.412 +  then show "n = m"
   9.413 +    by (induct n arbitrary: m)
   9.414 +      (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   9.415 +next
   9.416 +  fix n m q :: nat assume "n \<le> m" and "m \<le> q"
   9.417 +  then show "n \<le> q"
   9.418 +  proof (induct n arbitrary: m q)
   9.419 +    case 0 show ?case by simp
   9.420 +  next
   9.421 +    case (Suc n) then show ?case
   9.422 +      by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
   9.423 +        simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
   9.424 +        simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits)
   9.425 +  qed
   9.426 +next
   9.427 +  fix n m :: nat show "n \<le> m \<or> m \<le> n"
   9.428 +    by (induct n arbitrary: m)
   9.429 +      (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   9.430 +qed
   9.431  
   9.432  end
   9.433  
   9.434 -lemma wf_pred_nat: "wf pred_nat"
   9.435 -  apply (unfold wf_def pred_nat_def, clarify)
   9.436 -  apply (induct_tac x, blast+)
   9.437 -  done
   9.438 +subsubsection {* Introduction properties *}
   9.439  
   9.440 -lemma wf_less: "wf {(x, y::nat). x < y}"
   9.441 -  apply (unfold less_def)
   9.442 -  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast)
   9.443 -  done
   9.444 +lemma lessI [iff]: "n < Suc n"
   9.445 +  by (simp add: less_Suc_eq_le)
   9.446  
   9.447 -lemma less_eq: "((m, n) : pred_nat^+) = (m < n)"
   9.448 -  apply (unfold less_def)
   9.449 -  apply (rule refl)
   9.450 -  done
   9.451 -
   9.452 -subsubsection {* Introduction properties *}
   9.453 +lemma zero_less_Suc [iff]: "0 < Suc n"
   9.454 +  by (simp add: less_Suc_eq_le)
   9.455  
   9.456  lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
   9.457 -  apply (unfold less_def)
   9.458 -  apply (rule trans_trancl [THEN transD], assumption+)
   9.459 -  done
   9.460 -
   9.461 -lemma lessI [iff]: "n < Suc n"
   9.462 -  apply (unfold less_def pred_nat_def)
   9.463 -  apply (simp add: r_into_trancl)
   9.464 -  done
   9.465 -
   9.466 -lemma less_SucI: "i < j ==> i < Suc j"
   9.467 -  apply (rule less_trans, assumption)
   9.468 -  apply (rule lessI)
   9.469 -  done
   9.470 -
   9.471 -lemma zero_less_Suc [iff]: "0 < Suc n"
   9.472 -  apply (induct n)
   9.473 -  apply (rule lessI)
   9.474 -  apply (erule less_trans)
   9.475 -  apply (rule lessI)
   9.476 -  done
   9.477 +  by (rule order_less_trans)
   9.478  
   9.479  subsubsection {* Elimination properties *}
   9.480  
   9.481  lemma less_not_sym: "n < m ==> ~ m < (n::nat)"
   9.482 -  apply (unfold less_def)
   9.483 -  apply (blast intro: wf_pred_nat wf_trancl [THEN wf_asym])
   9.484 -  done
   9.485 +  by (rule order_less_not_sym)
   9.486  
   9.487  lemma less_asym:
   9.488    assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P
   9.489 @@ -239,70 +452,41 @@
   9.490    done
   9.491  
   9.492  lemma less_not_refl: "~ n < (n::nat)"
   9.493 -  apply (unfold less_def)
   9.494 -  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_not_refl])
   9.495 -  done
   9.496 +  by (rule order_less_irrefl)
   9.497  
   9.498  lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
   9.499 -by (rule notE, rule less_not_refl)
   9.500 -
   9.501 -lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
   9.502 +  by (rule notE, rule less_not_refl)
   9.503  
   9.504  lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   9.505 -by (rule not_sym, rule less_not_refl2)
   9.506 +  by (rule less_imp_neq)
   9.507  
   9.508 -lemma lessE:
   9.509 -  assumes major: "i < k"
   9.510 -  and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
   9.511 -  shows P
   9.512 -  apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all)
   9.513 -  apply (erule p1)
   9.514 -  apply (rule p2)
   9.515 -  apply (simp add: less_def pred_nat_def, assumption)
   9.516 -  done
   9.517 -
   9.518 -lemma not_less0 [iff]: "~ n < (0::nat)"
   9.519 -by (blast elim: lessE)
   9.520 +lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
   9.521 +  by (rule not_sym) (rule less_imp_neq) 
   9.522  
   9.523  lemma less_zeroE: "(n::nat) < 0 ==> R"
   9.524 -by (rule notE, rule not_less0)
   9.525 -
   9.526 -lemma less_SucE: assumes major: "m < Suc n"
   9.527 -  and less: "m < n ==> P" and eq: "m = n ==> P" shows P
   9.528 -  apply (rule major [THEN lessE])
   9.529 -  apply (rule eq, blast)
   9.530 -  apply (rule less, blast)
   9.531 -  done
   9.532 +  by (rule notE) (rule not_less0)
   9.533  
   9.534  lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
   9.535 -by (blast elim!: less_SucE intro: less_trans)
   9.536 +  unfolding less_Suc_eq_le le_less ..
   9.537  
   9.538 -lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)"
   9.539 -by (simp add: less_Suc_eq)
   9.540 +lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
   9.541 +  by (simp add: less_Suc_eq)
   9.542  
   9.543  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   9.544 -by (simp add: less_Suc_eq)
   9.545 +  by (simp add: less_Suc_eq)
   9.546  
   9.547  lemma Suc_mono: "m < n ==> Suc m < Suc n"
   9.548 -by (induct n) (fast elim: less_trans lessE)+
   9.549 +  by simp
   9.550  
   9.551 -text {* "Less than" is a linear ordering *}
   9.552  lemma less_linear: "m < n | m = n | n < (m::nat)"
   9.553 -  apply (induct m)
   9.554 -  apply (induct n)
   9.555 -  apply (rule refl [THEN disjI1, THEN disjI2])
   9.556 -  apply (rule zero_less_Suc [THEN disjI1])
   9.557 -  apply (blast intro: Suc_mono less_SucI elim: lessE)
   9.558 -  done
   9.559 +  by (rule less_linear)
   9.560  
   9.561  text {* "Less than" is antisymmetric, sort of *}
   9.562  lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
   9.563 -  apply(simp only:less_Suc_eq)
   9.564 -  apply blast
   9.565 -  done
   9.566 +  unfolding not_less less_Suc_eq_le by (rule antisym)
   9.567  
   9.568  lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
   9.569 -  using less_linear by blast
   9.570 +  by (rule linorder_neq_iff)
   9.571  
   9.572  lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
   9.573    and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m"
   9.574 @@ -318,13 +502,25 @@
   9.575  subsubsection {* Inductive (?) properties *}
   9.576  
   9.577  lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
   9.578 -  apply (simp add: nat_neq_iff)
   9.579 -  apply (blast elim!: less_irrefl less_SucE elim: less_asym)
   9.580 -  done
   9.581 +  unfolding less_eq_Suc_le [of m] le_less by simp 
   9.582  
   9.583 -lemma Suc_lessD: "Suc m < n ==> m < n"
   9.584 -  apply (induct n)
   9.585 -  apply (fast intro!: lessI [THEN less_SucI] elim: less_trans lessE)+
   9.586 +lemma lessE:
   9.587 +  assumes major: "i < k"
   9.588 +  and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
   9.589 +  shows P
   9.590 +proof -
   9.591 +  from major have "\<exists>j. i \<le> j \<and> k = Suc j"
   9.592 +    unfolding less_eq_Suc_le by (induct k) simp_all
   9.593 +  then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i"
   9.594 +    by (clarsimp simp add: less_le)
   9.595 +  with p1 p2 show P by auto
   9.596 +qed
   9.597 +
   9.598 +lemma less_SucE: assumes major: "m < Suc n"
   9.599 +  and less: "m < n ==> P" and eq: "m = n ==> P" shows P
   9.600 +  apply (rule major [THEN lessE])
   9.601 +  apply (rule eq, blast)
   9.602 +  apply (rule less, blast)
   9.603    done
   9.604  
   9.605  lemma Suc_lessE: assumes major: "Suc i < k"
   9.606 @@ -335,13 +531,7 @@
   9.607    done
   9.608  
   9.609  lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   9.610 -by (blast elim: lessE dest: Suc_lessD)
   9.611 -
   9.612 -lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
   9.613 -  apply (rule iffI)
   9.614 -  apply (erule Suc_less_SucD)
   9.615 -  apply (erule Suc_mono)
   9.616 -  done
   9.617 +  by simp
   9.618  
   9.619  lemma less_trans_Suc:
   9.620    assumes le: "i < j" shows "j < k ==> Suc i < k"
   9.621 @@ -352,67 +542,35 @@
   9.622    done
   9.623  
   9.624  text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
   9.625 -lemma not_less_eq: "(~ m < n) = (n < Suc m)"
   9.626 -by (induct m n rule: diff_induct) simp_all
   9.627 +lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
   9.628 +  unfolding not_less less_Suc_eq_le ..
   9.629  
   9.630 -text {* Complete induction, aka course-of-values induction *}
   9.631 -lemma nat_less_induct:
   9.632 -  assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   9.633 -  apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]])
   9.634 -  apply (rule prem)
   9.635 -  apply (unfold less_def, assumption)
   9.636 -  done
   9.637 -
   9.638 -lemmas less_induct = nat_less_induct [rule_format, case_names less]
   9.639 -
   9.640 +lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m"
   9.641 +  unfolding not_le Suc_le_eq ..
   9.642  
   9.643  text {* Properties of "less than or equal" *}
   9.644  
   9.645 -text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
   9.646 -lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)"
   9.647 -  unfolding le_def by (rule not_less_eq [symmetric])
   9.648 -
   9.649  lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
   9.650 -by (rule less_Suc_eq_le [THEN iffD2])
   9.651 -
   9.652 -lemma le0 [iff]: "(0::nat) \<le> n"
   9.653 -  unfolding le_def by (rule not_less0)
   9.654 +  unfolding less_Suc_eq_le .
   9.655  
   9.656  lemma Suc_n_not_le_n: "~ Suc n \<le> n"
   9.657 -by (simp add: le_def)
   9.658 -
   9.659 -lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
   9.660 -by (induct i) (simp_all add: le_def)
   9.661 +  unfolding not_le less_Suc_eq_le ..
   9.662  
   9.663  lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
   9.664 -by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
   9.665 +  by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq)
   9.666  
   9.667  lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   9.668 -by (drule le_Suc_eq [THEN iffD1], iprover+)
   9.669 +  by (drule le_Suc_eq [THEN iffD1], iprover+)
   9.670  
   9.671  lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   9.672 -  apply (simp add: le_def less_Suc_eq)
   9.673 -  apply (blast elim!: less_irrefl less_asym)
   9.674 -  done -- {* formerly called lessD *}
   9.675 -
   9.676 -lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
   9.677 -by (simp add: le_def less_Suc_eq)
   9.678 +  unfolding Suc_le_eq .
   9.679  
   9.680  text {* Stronger version of @{text Suc_leD} *}
   9.681  lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   9.682 -  apply (simp add: le_def less_Suc_eq)
   9.683 -  using less_linear
   9.684 -  apply blast
   9.685 -  done
   9.686 -
   9.687 -lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
   9.688 -by (blast intro: Suc_leI Suc_le_lessD)
   9.689 -
   9.690 -lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
   9.691 -by (unfold le_def) (blast dest: Suc_lessD)
   9.692 +  unfolding Suc_le_eq .
   9.693  
   9.694  lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
   9.695 -by (unfold le_def) (blast elim: less_asym)
   9.696 +  unfolding less_eq_Suc_le by (rule Suc_leD)
   9.697  
   9.698  text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
   9.699  lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
   9.700 @@ -421,88 +579,52 @@
   9.701  text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
   9.702  
   9.703  lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
   9.704 -  unfolding le_def
   9.705 -  using less_linear
   9.706 -  by (blast elim: less_irrefl less_asym)
   9.707 +  unfolding le_less .
   9.708  
   9.709  lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   9.710 -  unfolding le_def
   9.711 -  using less_linear
   9.712 -  by (blast elim!: less_irrefl elim: less_asym)
   9.713 +  unfolding le_less .
   9.714  
   9.715  lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   9.716 -by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
   9.717 +  by (rule le_less)
   9.718  
   9.719  text {* Useful with @{text blast}. *}
   9.720  lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   9.721 -by (rule less_or_eq_imp_le) (rule disjI2)
   9.722 +  by auto
   9.723  
   9.724  lemma le_refl: "n \<le> (n::nat)"
   9.725 -by (simp add: le_eq_less_or_eq)
   9.726 +  by simp
   9.727  
   9.728  lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
   9.729 -by (blast dest!: le_imp_less_or_eq intro: less_trans)
   9.730 +  by (rule order_le_less_trans)
   9.731  
   9.732  lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
   9.733 -by (blast dest!: le_imp_less_or_eq intro: less_trans)
   9.734 +  by (rule order_less_le_trans)
   9.735  
   9.736  lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   9.737 -by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
   9.738 +  by (rule order_trans)
   9.739  
   9.740  lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
   9.741 -by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
   9.742 +  by (rule antisym)
   9.743  
   9.744 -lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
   9.745 -by (simp add: le_simps)
   9.746 -
   9.747 -text {* Axiom @{text order_less_le} of class @{text order}: *}
   9.748  lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
   9.749 -by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
   9.750 +  by (rule less_le)
   9.751  
   9.752  lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
   9.753 -by (rule iffD2, rule nat_less_le, rule conjI)
   9.754 -
   9.755 -text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
   9.756 -lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
   9.757 -  apply (simp add: le_eq_less_or_eq)
   9.758 -  using less_linear by blast
   9.759 +  unfolding less_le ..
   9.760  
   9.761 -text {* Type @{typ nat} is a wellfounded linear order *}
   9.762 -
   9.763 -instance nat :: wellorder
   9.764 -  by intro_classes
   9.765 -    (assumption |
   9.766 -      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
   9.767 +lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
   9.768 +  by (rule linear)
   9.769  
   9.770  lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
   9.771  
   9.772 -lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   9.773 -by (blast elim!: less_SucE)
   9.774 +lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
   9.775 +  unfolding less_Suc_eq_le by auto
   9.776  
   9.777 -text {*
   9.778 -  Rewrite @{term "n < Suc m"} to @{term "n = m"}
   9.779 -  if @{term "~ n < m"} or @{term "m \<le> n"} hold.
   9.780 -  Not suitable as default simprules because they often lead to looping
   9.781 -*}
   9.782 -lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
   9.783 -by (rule not_less_less_Suc_eq, rule leD)
   9.784 +lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   9.785 +  unfolding not_less by (rule le_less_Suc_eq)
   9.786  
   9.787  lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
   9.788  
   9.789 -
   9.790 -text {*
   9.791 -  Re-orientation of the equations @{text "0 = x"} and @{text "1 = x"}.
   9.792 -  No longer added as simprules (they loop)
   9.793 -  but via @{text reorient_simproc} in Bin
   9.794 -*}
   9.795 -
   9.796 -text {* Polymorphic, not just for @{typ nat} *}
   9.797 -lemma zero_reorient: "(0 = x) = (x = 0)"
   9.798 -by auto
   9.799 -
   9.800 -lemma one_reorient: "(1 = x) = (x = 1)"
   9.801 -by auto
   9.802 -
   9.803  text {* These two rules ease the use of primitive recursion.
   9.804  NOTE USE OF @{text "=="} *}
   9.805  lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
   9.806 @@ -540,34 +662,8 @@
   9.807  lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
   9.808  by (cases m) simp_all
   9.809  
   9.810 -lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
   9.811 -  apply (rule nat_less_induct)
   9.812 -  apply (case_tac n)
   9.813 -  apply (case_tac [2] nat)
   9.814 -  apply (blast intro: less_trans)+
   9.815 -  done
   9.816  
   9.817 -
   9.818 -subsection {* @{text LEAST} theorems for type @{typ nat}*}
   9.819 -
   9.820 -lemma Least_Suc:
   9.821 -     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   9.822 -  apply (case_tac "n", auto)
   9.823 -  apply (frule LeastI)
   9.824 -  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   9.825 -  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   9.826 -  apply (erule_tac [2] Least_le)
   9.827 -  apply (case_tac "LEAST x. P x", auto)
   9.828 -  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   9.829 -  apply (blast intro: order_antisym)
   9.830 -  done
   9.831 -
   9.832 -lemma Least_Suc2:
   9.833 -   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   9.834 -by (erule (1) Least_Suc [THEN ssubst], simp)
   9.835 -
   9.836 -
   9.837 -subsection {* @{term min} and @{term max} *}
   9.838 +subsubsection {* @{term min} and @{term max} *}
   9.839  
   9.840  lemma mono_Suc: "mono Suc"
   9.841  by (rule monoI) simp
   9.842 @@ -607,66 +703,10 @@
   9.843  by (simp split: nat.split)
   9.844  
   9.845  
   9.846 -subsection {* Basic rewrite rules for the arithmetic operators *}
   9.847 -
   9.848 -text {* Difference *}
   9.849 -
   9.850 -lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
   9.851 -by (induct n) simp_all
   9.852 -
   9.853 -lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
   9.854 -by (induct n) simp_all
   9.855 -
   9.856 -
   9.857 -text {*
   9.858 -  Could be (and is, below) generalized in various ways
   9.859 -  However, none of the generalizations are currently in the simpset,
   9.860 -  and I dread to think what happens if I put them in
   9.861 -*}
   9.862 -lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
   9.863 -by (simp split add: nat.split)
   9.864 -
   9.865 -declare diff_Suc [simp del, code del]
   9.866 -
   9.867 -lemma [code]:
   9.868 -  "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
   9.869 -  "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
   9.870 -  "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
   9.871 -  "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
   9.872 -  using Suc_le_eq less_Suc_eq_le by simp_all
   9.873 -
   9.874 +subsubsection {* Monotonicity of Addition *}
   9.875  
   9.876 -subsection {* Addition *}
   9.877 -
   9.878 -lemma add_0_right [simp]: "m + 0 = (m::nat)"
   9.879 -by (induct m) simp_all
   9.880 -
   9.881 -lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   9.882 -by (induct m) simp_all
   9.883 -
   9.884 -lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   9.885 -by simp
   9.886 -
   9.887 -
   9.888 -text {* Associative law for addition *}
   9.889 -lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
   9.890 -by (induct m) simp_all
   9.891 -
   9.892 -text {* Commutative law for addition *}
   9.893 -lemma nat_add_commute: "m + n = n + (m::nat)"
   9.894 -by (induct m) simp_all
   9.895 -
   9.896 -lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   9.897 -  apply (rule mk_left_commute [of "op +"])
   9.898 -  apply (rule nat_add_assoc)
   9.899 -  apply (rule nat_add_commute)
   9.900 -  done
   9.901 -
   9.902 -lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
   9.903 -by (induct k) simp_all
   9.904 -
   9.905 -lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
   9.906 -by (induct k) simp_all
   9.907 +lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
   9.908 +by (simp add: diff_Suc split: nat.split)
   9.909  
   9.910  lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
   9.911  by (induct k) simp_all
   9.912 @@ -674,83 +714,9 @@
   9.913  lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
   9.914  by (induct k) simp_all
   9.915  
   9.916 -text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
   9.917 -
   9.918 -lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)"
   9.919 -by (cases m) simp_all
   9.920 -
   9.921 -lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
   9.922 -by (cases m) simp_all
   9.923 -
   9.924 -lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   9.925 -by (rule trans, rule eq_commute, rule add_is_1)
   9.926 -
   9.927  lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
   9.928  by(auto dest:gr0_implies_Suc)
   9.929  
   9.930 -lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   9.931 -  apply (drule add_0_right [THEN ssubst])
   9.932 -  apply (simp add: nat_add_assoc del: add_0_right)
   9.933 -  done
   9.934 -
   9.935 -lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N"
   9.936 -  apply (induct k)
   9.937 -   apply simp
   9.938 -  apply(drule comp_inj_on[OF _ inj_Suc])
   9.939 -  apply (simp add:o_def)
   9.940 -  done
   9.941 -
   9.942 -
   9.943 -subsection {* Multiplication *}
   9.944 -
   9.945 -text {* right annihilation in product *}
   9.946 -lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
   9.947 -by (induct m) simp_all
   9.948 -
   9.949 -text {* right successor law for multiplication *}
   9.950 -lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   9.951 -by (induct m) (simp_all add: nat_add_left_commute)
   9.952 -
   9.953 -text {* Commutative law for multiplication *}
   9.954 -lemma nat_mult_commute: "m * n = n * (m::nat)"
   9.955 -by (induct m) simp_all
   9.956 -
   9.957 -text {* addition distributes over multiplication *}
   9.958 -lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
   9.959 -by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
   9.960 -
   9.961 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   9.962 -by (induct m) (simp_all add: nat_add_assoc)
   9.963 -
   9.964 -text {* Associative law for multiplication *}
   9.965 -lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
   9.966 -by (induct m) (simp_all add: add_mult_distrib)
   9.967 -
   9.968 -
   9.969 -text{*The naturals form a @{text comm_semiring_1_cancel}*}
   9.970 -instance nat :: comm_semiring_1_cancel
   9.971 -proof
   9.972 -  fix i j k :: nat
   9.973 -  show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
   9.974 -  show "i + j = j + i" by (rule nat_add_commute)
   9.975 -  show "0 + i = i" by simp
   9.976 -  show "(i * j) * k = i * (j * k)" by (rule nat_mult_assoc)
   9.977 -  show "i * j = j * i" by (rule nat_mult_commute)
   9.978 -  show "1 * i = i" by simp
   9.979 -  show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
   9.980 -  show "0 \<noteq> (1::nat)" by simp
   9.981 -  assume "k+i = k+j" thus "i=j" by simp
   9.982 -qed
   9.983 -
   9.984 -lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   9.985 -  apply (induct m)
   9.986 -   apply (induct_tac [2] n)
   9.987 -    apply simp_all
   9.988 -  done
   9.989 -
   9.990 -
   9.991 -subsection {* Monotonicity of Addition *}
   9.992 -
   9.993  text {* strict, in 1st argument *}
   9.994  lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   9.995  by (induct k) simp_all
   9.996 @@ -776,7 +742,6 @@
   9.997  apply (simp_all add: add_less_mono)
   9.998  done
   9.999  
  9.1000 -
  9.1001  text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
  9.1002  instance nat :: ordered_semidom
  9.1003  proof
  9.1004 @@ -793,7 +758,7 @@
  9.1005  by simp
  9.1006  
  9.1007  
  9.1008 -subsection {* Additional theorems about "less than" *}
  9.1009 +subsubsection {* Additional theorems about "less than" *}
  9.1010  
  9.1011  text{*An induction rule for estabilishing binary relations*}
  9.1012  lemma less_Suc_induct:
  9.1013 @@ -814,67 +779,6 @@
  9.1014    thus "P i j" by (simp add: j)
  9.1015  qed
  9.1016  
  9.1017 -text {* The method of infinite descent, frequently used in number theory.
  9.1018 -Provided by Roelof Oosterhuis.
  9.1019 -$P(n)$ is true for all $n\in\mathbb{N}$ if
  9.1020 -\begin{itemize}
  9.1021 -  \item case ``0'': given $n=0$ prove $P(n)$,
  9.1022 -  \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
  9.1023 -        a smaller integer $m$ such that $\neg P(m)$.
  9.1024 -\end{itemize} *}
  9.1025 -
  9.1026 -lemma infinite_descent0[case_names 0 smaller]: 
  9.1027 -  "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
  9.1028 -by (induct n rule: less_induct, case_tac "n>0", auto)
  9.1029 -
  9.1030 -text{* A compact version without explicit base case: *}
  9.1031 -lemma infinite_descent:
  9.1032 -  "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
  9.1033 -by (induct n rule: less_induct, auto)
  9.1034 -
  9.1035 -
  9.1036 -text {* Infinite descent using a mapping to $\mathbb{N}$:
  9.1037 -$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
  9.1038 -\begin{itemize}
  9.1039 -\item case ``0'': given $V(x)=0$ prove $P(x)$,
  9.1040 -\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
  9.1041 -\end{itemize}
  9.1042 -NB: the proof also shows how to use the previous lemma. *}
  9.1043 -corollary infinite_descent0_measure [case_names 0 smaller]:
  9.1044 -  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
  9.1045 -    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
  9.1046 -  shows "P x"
  9.1047 -proof -
  9.1048 -  obtain n where "n = V x" by auto
  9.1049 -  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
  9.1050 -  proof (induct n rule: infinite_descent0)
  9.1051 -    case 0 -- "i.e. $V(x) = 0$"
  9.1052 -    with A0 show "P x" by auto
  9.1053 -  next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
  9.1054 -    case (smaller n)
  9.1055 -    then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  9.1056 -    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
  9.1057 -    with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
  9.1058 -    thus ?case by auto
  9.1059 -  qed
  9.1060 -  ultimately show "P x" by auto
  9.1061 -qed
  9.1062 -
  9.1063 -text{* Again, without explicit base case: *}
  9.1064 -lemma infinite_descent_measure:
  9.1065 -assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
  9.1066 -proof -
  9.1067 -  from assms obtain n where "n = V x" by auto
  9.1068 -  moreover have "!!x. V x = n \<Longrightarrow> P x"
  9.1069 -  proof (induct n rule: infinite_descent, auto)
  9.1070 -    fix x assume "\<not> P x"
  9.1071 -    with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
  9.1072 -  qed
  9.1073 -  ultimately show "P x" by auto
  9.1074 -qed
  9.1075 -
  9.1076 -
  9.1077 -
  9.1078  text {* A [clumsy] way of lifting @{text "<"}
  9.1079    monotonicity to @{text "\<le>"} monotonicity *}
  9.1080  lemma less_mono_imp_le_mono:
  9.1081 @@ -949,7 +853,7 @@
  9.1082      simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
  9.1083  
  9.1084  
  9.1085 -subsection {* Difference *}
  9.1086 +subsubsection {* More results about difference *}
  9.1087  
  9.1088  lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
  9.1089  by (induct m) simp_all
  9.1090 @@ -965,9 +869,6 @@
  9.1091  lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
  9.1092  by (simp add: le_add_diff_inverse add_commute)
  9.1093  
  9.1094 -
  9.1095 -subsection {* More results about difference *}
  9.1096 -
  9.1097  lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
  9.1098  by (induct m n rule: diff_induct) simp_all
  9.1099  
  9.1100 @@ -980,34 +881,21 @@
  9.1101  lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
  9.1102  by (induct m n rule: diff_induct) (simp_all add: le_SucI)
  9.1103  
  9.1104 +lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
  9.1105 +  by (auto simp: le_add1 dest!: le_add_diff_inverse sym [of _ n])
  9.1106 +
  9.1107  lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
  9.1108  by (rule le_less_trans, rule diff_le_self)
  9.1109  
  9.1110 -lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)"
  9.1111 -by (induct i j rule: diff_induct) simp_all
  9.1112 -
  9.1113 -lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
  9.1114 -by (simp add: diff_diff_left)
  9.1115 -
  9.1116  lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n"
  9.1117  by (cases n) (auto simp add: le_simps)
  9.1118  
  9.1119 -text {* This and the next few suggested by Florian Kammueller *}
  9.1120 -lemma diff_commute: "(i::nat) - j - k = i - k - j"
  9.1121 -by (simp add: diff_diff_left add_commute)
  9.1122 -
  9.1123  lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
  9.1124  by (induct j k rule: diff_induct) simp_all
  9.1125  
  9.1126  lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
  9.1127  by (simp add: add_commute diff_add_assoc)
  9.1128  
  9.1129 -lemma diff_add_inverse: "(n + m) - n = (m::nat)"
  9.1130 -by (induct n) simp_all
  9.1131 -
  9.1132 -lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
  9.1133 -by (simp add: diff_add_assoc)
  9.1134 -
  9.1135  lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
  9.1136  by (auto simp add: diff_add_inverse2)
  9.1137  
  9.1138 @@ -1028,30 +916,26 @@
  9.1139      by (simp add: order_less_imp_le)
  9.1140  qed
  9.1141  
  9.1142 -lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
  9.1143 -by (induct k) simp_all
  9.1144 +text {* a nice rewrite for bounded subtraction *}
  9.1145 +lemma nat_minus_add_max:
  9.1146 +  fixes n m :: nat
  9.1147 +  shows "n - m + m = max n m"
  9.1148 +    by (simp add: max_def not_le order_less_imp_le)
  9.1149  
  9.1150 -lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
  9.1151 -by (simp add: diff_cancel add_commute)
  9.1152 +lemma nat_diff_split:
  9.1153 +  "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
  9.1154 +    -- {* elimination of @{text -} on @{text nat} *}
  9.1155 +by (cases "a < b")
  9.1156 +  (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
  9.1157 +    not_less le_less dest!: sym [of a] sym [of b] add_eq_self_zero)
  9.1158  
  9.1159 -lemma diff_add_0: "n - (n + m) = (0::nat)"
  9.1160 -by (induct n) simp_all
  9.1161 +lemma nat_diff_split_asm:
  9.1162 +  "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
  9.1163 +    -- {* elimination of @{text -} on @{text nat} in assumptions *}
  9.1164 +by (auto split: nat_diff_split)
  9.1165  
  9.1166  
  9.1167 -text {* Difference distributes over multiplication *}
  9.1168 -
  9.1169 -lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
  9.1170 -by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
  9.1171 -
  9.1172 -lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
  9.1173 -by (simp add: diff_mult_distrib mult_commute [of k])
  9.1174 -  -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
  9.1175 -
  9.1176 -lemmas nat_distrib =
  9.1177 -  add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
  9.1178 -
  9.1179 -
  9.1180 -subsection {* Monotonicity of Multiplication *}
  9.1181 +subsubsection {* Monotonicity of Multiplication *}
  9.1182  
  9.1183  lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
  9.1184  by (simp add: mult_right_mono)
  9.1185 @@ -1082,18 +966,6 @@
  9.1186     apply simp_all
  9.1187    done
  9.1188  
  9.1189 -lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
  9.1190 -  apply (induct m)
  9.1191 -   apply simp
  9.1192 -  apply (induct n)
  9.1193 -   apply auto
  9.1194 -  done
  9.1195 -
  9.1196 -lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
  9.1197 -  apply (rule trans)
  9.1198 -  apply (rule_tac [2] mult_eq_1_iff, fastsimp)
  9.1199 -  done
  9.1200 -
  9.1201  lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
  9.1202    apply (safe intro!: mult_less_mono1)
  9.1203    apply (case_tac k, auto)
  9.1204 @@ -1110,22 +982,17 @@
  9.1205  lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
  9.1206  by (simp add: linorder_not_less [symmetric], auto)
  9.1207  
  9.1208 -lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
  9.1209 -apply (cut_tac less_linear, safe, auto)
  9.1210 -apply (drule mult_less_mono1, assumption, simp)+
  9.1211 -done
  9.1212 -
  9.1213 -lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
  9.1214 -by (simp add: mult_commute [of k])
  9.1215 -
  9.1216  lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
  9.1217  by (subst mult_less_cancel1) simp
  9.1218  
  9.1219  lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)"
  9.1220  by (subst mult_le_cancel1) simp
  9.1221  
  9.1222 -lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
  9.1223 -by (subst mult_cancel1) simp
  9.1224 +lemma le_square: "m \<le> m * (m::nat)"
  9.1225 +  by (cases m) (auto intro: le_add1)
  9.1226 +
  9.1227 +lemma le_cube: "(m::nat) \<le> m * (m * m)"
  9.1228 +  by (cases m) (auto intro: le_add1)
  9.1229  
  9.1230  text {* Lemma for @{text gcd} *}
  9.1231  lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
  9.1232 @@ -1136,23 +1003,22 @@
  9.1233      apply (auto)
  9.1234    done
  9.1235  
  9.1236 -
  9.1237 -subsection {* size of a datatype value *}
  9.1238 +text {* the lattice order on @{typ nat} *}
  9.1239  
  9.1240 -class size = type +
  9.1241 -  fixes size :: "'a \<Rightarrow> nat"
  9.1242 +instantiation nat :: distrib_lattice
  9.1243 +begin
  9.1244  
  9.1245 -use "Tools/function_package/size.ML"
  9.1246 +definition
  9.1247 +  "(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
  9.1248  
  9.1249 -setup Size.setup
  9.1250 -
  9.1251 -lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
  9.1252 -by (induct n) simp_all
  9.1253 +definition
  9.1254 +  "(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
  9.1255  
  9.1256 -lemma size_bool [code func]:
  9.1257 -  "size (b\<Colon>bool) = 0" by (cases b) auto
  9.1258 +instance by intro_classes
  9.1259 +  (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
  9.1260 +    intro: order_less_imp_le antisym elim!: order_trans order_less_trans)
  9.1261  
  9.1262 -declare "prod.size" [noatp]
  9.1263 +end
  9.1264  
  9.1265  
  9.1266  subsection {* Embedding of the Naturals into any
  9.1267 @@ -1192,6 +1058,26 @@
  9.1268  
  9.1269  end
  9.1270  
  9.1271 +text{*Class for unital semirings with characteristic zero.
  9.1272 + Includes non-ordered rings like the complex numbers.*}
  9.1273 +
  9.1274 +class semiring_char_0 = semiring_1 +
  9.1275 +  assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
  9.1276 +begin
  9.1277 +
  9.1278 +text{*Special cases where either operand is zero*}
  9.1279 +
  9.1280 +lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
  9.1281 +  by (rule of_nat_eq_iff [of 0, simplified])
  9.1282 +
  9.1283 +lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
  9.1284 +  by (rule of_nat_eq_iff [of _ 0, simplified])
  9.1285 +
  9.1286 +lemma inj_of_nat: "inj of_nat"
  9.1287 +  by (simp add: inj_on_def)
  9.1288 +
  9.1289 +end
  9.1290 +
  9.1291  context ordered_semidom
  9.1292  begin
  9.1293  
  9.1294 @@ -1216,17 +1102,13 @@
  9.1295  lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
  9.1296    by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
  9.1297  
  9.1298 -text{*Special cases where either operand is zero*}
  9.1299 -
  9.1300 -lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
  9.1301 -  by (rule of_nat_less_iff [of 0, simplified])
  9.1302 +lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
  9.1303 +  by (simp add: not_less [symmetric] linorder_not_less [symmetric])
  9.1304  
  9.1305 -lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
  9.1306 -  by (rule of_nat_less_iff [of _ 0, simplified])
  9.1307 +text{*Every @{text ordered_semidom} has characteristic zero.*}
  9.1308  
  9.1309 -lemma of_nat_le_iff [simp]:
  9.1310 -  "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
  9.1311 -  by (simp add: not_less [symmetric] linorder_not_less [symmetric])
  9.1312 +subclass semiring_char_0
  9.1313 +  by unfold_locales (simp add: eq_iff order_eq_iff)
  9.1314  
  9.1315  text{*Special cases where either operand is zero*}
  9.1316  
  9.1317 @@ -1236,6 +1118,28 @@
  9.1318  lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
  9.1319    by (rule of_nat_le_iff [of _ 0, simplified])
  9.1320  
  9.1321 +lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
  9.1322 +  by (rule of_nat_less_iff [of 0, simplified])
  9.1323 +
  9.1324 +lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
  9.1325 +  by (rule of_nat_less_iff [of _ 0, simplified])
  9.1326 +
  9.1327 +end
  9.1328 +
  9.1329 +context ring_1
  9.1330 +begin
  9.1331 +
  9.1332 +lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
  9.1333 +  by (simp add: compare_rls of_nat_add [symmetric])
  9.1334 +
  9.1335 +end
  9.1336 +
  9.1337 +context ordered_idom
  9.1338 +begin
  9.1339 +
  9.1340 +lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
  9.1341 +  unfolding abs_if by auto
  9.1342 +
  9.1343  end
  9.1344  
  9.1345  lemma of_nat_id [simp]: "of_nat n = n"
  9.1346 @@ -1244,30 +1148,45 @@
  9.1347  lemma of_nat_eq_id [simp]: "of_nat = id"
  9.1348    by (auto simp add: expand_fun_eq)
  9.1349  
  9.1350 -text{*Class for unital semirings with characteristic zero.
  9.1351 - Includes non-ordered rings like the complex numbers.*}
  9.1352 -
  9.1353 -class semiring_char_0 = semiring_1 +
  9.1354 -  assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
  9.1355  
  9.1356 -text{*Every @{text ordered_semidom} has characteristic zero.*}
  9.1357 +subsection {*The Set of Natural Numbers*}
  9.1358  
  9.1359 -subclass (in ordered_semidom) semiring_char_0
  9.1360 -  by unfold_locales (simp add: eq_iff order_eq_iff)
  9.1361 -
  9.1362 -context semiring_char_0
  9.1363 +context semiring_1
  9.1364  begin
  9.1365  
  9.1366 -text{*Special cases where either operand is zero*}
  9.1367 +definition
  9.1368 +  Nats  :: "'a set" where
  9.1369 +  "Nats = range of_nat"
  9.1370 +
  9.1371 +notation (xsymbols)
  9.1372 +  Nats  ("\<nat>")
  9.1373  
  9.1374 -lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
  9.1375 -  by (rule of_nat_eq_iff [of 0, simplified])
  9.1376 +lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
  9.1377 +  by (simp add: Nats_def)
  9.1378 +
  9.1379 +lemma Nats_0 [simp]: "0 \<in> \<nat>"
  9.1380 +apply (simp add: Nats_def)
  9.1381 +apply (rule range_eqI)
  9.1382 +apply (rule of_nat_0 [symmetric])
  9.1383 +done
  9.1384  
  9.1385 -lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
  9.1386 -  by (rule of_nat_eq_iff [of _ 0, simplified])
  9.1387 +lemma Nats_1 [simp]: "1 \<in> \<nat>"
  9.1388 +apply (simp add: Nats_def)
  9.1389 +apply (rule range_eqI)
  9.1390 +apply (rule of_nat_1 [symmetric])
  9.1391 +done
  9.1392  
  9.1393 -lemma inj_of_nat: "inj of_nat"
  9.1394 -  by (simp add: inj_on_def)
  9.1395 +lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
  9.1396 +apply (auto simp add: Nats_def)
  9.1397 +apply (rule range_eqI)
  9.1398 +apply (rule of_nat_add [symmetric])
  9.1399 +done
  9.1400 +
  9.1401 +lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
  9.1402 +apply (auto simp add: Nats_def)
  9.1403 +apply (rule range_eqI)
  9.1404 +apply (rule of_nat_mult [symmetric])
  9.1405 +done
  9.1406  
  9.1407  end
  9.1408  
  9.1409 @@ -1285,47 +1204,8 @@
  9.1410  use "Tools/lin_arith.ML"
  9.1411  declaration {* K LinArith.setup *}
  9.1412  
  9.1413 -
  9.1414 -text{*The following proofs may rely on the arithmetic proof procedures.*}
  9.1415 -
  9.1416 -lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
  9.1417 -by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
  9.1418 -
  9.1419 -lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
  9.1420 -by (simp add: less_eq reflcl_trancl [symmetric] del: reflcl_trancl, arith)
  9.1421 -
  9.1422 -lemma nat_diff_split:
  9.1423 -  "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
  9.1424 -    -- {* elimination of @{text -} on @{text nat} *}
  9.1425 -by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
  9.1426 -
  9.1427 -context ring_1
  9.1428 -begin
  9.1429 -
  9.1430 -lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
  9.1431 -  by (simp del: of_nat_add
  9.1432 -    add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
  9.1433 -
  9.1434 -end
  9.1435 -
  9.1436 -lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
  9.1437 -  unfolding abs_if by auto
  9.1438 -
  9.1439 -lemma nat_diff_split_asm:
  9.1440 -  "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
  9.1441 -    -- {* elimination of @{text -} on @{text nat} in assumptions *}
  9.1442 -by (simp split: nat_diff_split)
  9.1443 -
  9.1444  lemmas [arith_split] = nat_diff_split split_min split_max
  9.1445  
  9.1446 -
  9.1447 -lemma le_square: "m \<le> m * (m::nat)"
  9.1448 -by (induct m) auto
  9.1449 -
  9.1450 -lemma le_cube: "(m::nat) \<le> m * (m * m)"
  9.1451 -by (induct m) auto
  9.1452 -
  9.1453 -
  9.1454  text{*Subtraction laws, mostly by Clemens Ballarin*}
  9.1455  
  9.1456  lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
  9.1457 @@ -1351,8 +1231,7 @@
  9.1458  lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
  9.1459  by arith
  9.1460  
  9.1461 -
  9.1462 -(** Simplification of relational expressions involving subtraction **)
  9.1463 +text {* Simplification of relational expressions involving subtraction *}
  9.1464  
  9.1465  lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
  9.1466  by (simp split add: nat_diff_split)
  9.1467 @@ -1366,7 +1245,6 @@
  9.1468  lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
  9.1469  by (auto split add: nat_diff_split)
  9.1470  
  9.1471 -
  9.1472  text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
  9.1473  
  9.1474  (* Monotonicity of subtraction in first argument *)
  9.1475 @@ -1382,6 +1260,17 @@
  9.1476  lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
  9.1477  by (simp split add: nat_diff_split)
  9.1478  
  9.1479 +text{*Rewriting to pull differences out*}
  9.1480 +
  9.1481 +lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
  9.1482 +by arith
  9.1483 +
  9.1484 +lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
  9.1485 +by arith
  9.1486 +
  9.1487 +lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
  9.1488 +by arith
  9.1489 +
  9.1490  text{*Lemmas for ex/Factorization*}
  9.1491  
  9.1492  lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
  9.1493 @@ -1435,16 +1324,8 @@
  9.1494  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
  9.1495    using inc_induct[of 0 k P] by blast
  9.1496  
  9.1497 -text{*Rewriting to pull differences out*}
  9.1498 -
  9.1499 -lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
  9.1500 -by arith
  9.1501 -
  9.1502 -lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
  9.1503 -by arith
  9.1504 -
  9.1505 -lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
  9.1506 -by arith
  9.1507 +lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
  9.1508 +  by auto
  9.1509  
  9.1510  (*The others are
  9.1511        i - j - k = i - (j + k),
  9.1512 @@ -1452,108 +1333,14 @@
  9.1513        k \<le> j ==> i + (j - k) = i + j - k *)
  9.1514  lemmas add_diff_assoc = diff_add_assoc [symmetric]
  9.1515  lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
  9.1516 -declare diff_diff_left [simp]  add_diff_assoc [simp]  add_diff_assoc2[simp]
  9.1517 +declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
  9.1518  
  9.1519  text{*At present we prove no analogue of @{text not_less_Least} or @{text
  9.1520  Least_Suc}, since there appears to be no need.*}
  9.1521  
  9.1522 -text {* a nice rewrite for bounded subtraction *}
  9.1523 -
  9.1524 -lemma nat_minus_add_max:
  9.1525 -  fixes n m :: nat
  9.1526 -  shows "n - m + m = max n m"
  9.1527 -  by (simp add: max_def)
  9.1528 -
  9.1529 -
  9.1530 -subsection {*The Set of Natural Numbers*}
  9.1531 -
  9.1532 -context semiring_1
  9.1533 -begin
  9.1534 -
  9.1535 -definition
  9.1536 -  Nats  :: "'a set" where
  9.1537 -  "Nats = range of_nat"
  9.1538 -
  9.1539 -notation (xsymbols)
  9.1540 -  Nats  ("\<nat>")
  9.1541 -
  9.1542 -lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
  9.1543 -  by (simp add: Nats_def)
  9.1544 +subsection {* size of a datatype value *}
  9.1545  
  9.1546 -lemma Nats_0 [simp]: "0 \<in> \<nat>"
  9.1547 -apply (simp add: Nats_def)
  9.1548 -apply (rule range_eqI)
  9.1549 -apply (rule of_nat_0 [symmetric])
  9.1550 -done
  9.1551 -
  9.1552 -lemma Nats_1 [simp]: "1 \<in> \<nat>"
  9.1553 -apply (simp add: Nats_def)
  9.1554 -apply (rule range_eqI)
  9.1555 -apply (rule of_nat_1 [symmetric])
  9.1556 -done
  9.1557 -
  9.1558 -lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
  9.1559 -apply (auto simp add: Nats_def)
  9.1560 -apply (rule range_eqI)
  9.1561 -apply (rule of_nat_add [symmetric])
  9.1562 -done
  9.1563 -
  9.1564 -lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
  9.1565 -apply (auto simp add: Nats_def)
  9.1566 -apply (rule range_eqI)
  9.1567 -apply (rule of_nat_mult [symmetric])
  9.1568 -done
  9.1569 +class size = type +
  9.1570 +  fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded_Recursion} *}
  9.1571  
  9.1572  end
  9.1573 -
  9.1574 -
  9.1575 -text {* the lattice order on @{typ nat} *}
  9.1576 -
  9.1577 -instantiation nat :: distrib_lattice
  9.1578 -begin
  9.1579 -
  9.1580 -definition
  9.1581 -  "(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
  9.1582 -
  9.1583 -definition
  9.1584 -  "(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
  9.1585 -
  9.1586 -instance by intro_classes
  9.1587 -  (simp_all add: inf_nat_def sup_nat_def)
  9.1588 -
  9.1589 -end
  9.1590 -
  9.1591 -
  9.1592 -subsection {* legacy bindings *}
  9.1593 -
  9.1594 -ML
  9.1595 -{*
  9.1596 -val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
  9.1597 -val nat_diff_split = thm "nat_diff_split";
  9.1598 -val nat_diff_split_asm = thm "nat_diff_split_asm";
  9.1599 -val le_square = thm "le_square";
  9.1600 -val le_cube = thm "le_cube";
  9.1601 -val diff_less_mono = thm "diff_less_mono";
  9.1602 -val less_diff_conv = thm "less_diff_conv";
  9.1603 -val le_diff_conv = thm "le_diff_conv";
  9.1604 -val le_diff_conv2 = thm "le_diff_conv2";
  9.1605 -val diff_diff_cancel = thm "diff_diff_cancel";
  9.1606 -val le_add_diff = thm "le_add_diff";
  9.1607 -val diff_less = thm "diff_less";
  9.1608 -val diff_diff_eq = thm "diff_diff_eq";
  9.1609 -val eq_diff_iff = thm "eq_diff_iff";
  9.1610 -val less_diff_iff = thm "less_diff_iff";
  9.1611 -val le_diff_iff = thm "le_diff_iff";
  9.1612 -val diff_le_mono = thm "diff_le_mono";
  9.1613 -val diff_le_mono2 = thm "diff_le_mono2";
  9.1614 -val diff_less_mono2 = thm "diff_less_mono2";
  9.1615 -val diffs0_imp_equal = thm "diffs0_imp_equal";
  9.1616 -val one_less_mult = thm "one_less_mult";
  9.1617 -val n_less_m_mult_n = thm "n_less_m_mult_n";
  9.1618 -val n_less_n_mult_m = thm "n_less_n_mult_m";
  9.1619 -val diff_diff_right = thm "diff_diff_right";
  9.1620 -val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
  9.1621 -val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
  9.1622 -*}
  9.1623 -
  9.1624 -end
    10.1 --- a/src/HOL/Relation_Power.thy	Fri Feb 15 16:09:10 2008 +0100
    10.2 +++ b/src/HOL/Relation_Power.thy	Fri Feb 15 16:09:12 2008 +0100
    10.3 @@ -7,7 +7,7 @@
    10.4  header{*Powers of Relations and Functions*}
    10.5  
    10.6  theory Relation_Power
    10.7 -imports Power
    10.8 +imports Power Transitive_Closure
    10.9  begin
   10.10  
   10.11  instance
    11.1 --- a/src/HOL/SetInterval.thy	Fri Feb 15 16:09:10 2008 +0100
    11.2 +++ b/src/HOL/SetInterval.thy	Fri Feb 15 16:09:12 2008 +0100
    11.3 @@ -122,8 +122,7 @@
    11.4  
    11.5  lemma Compl_greaterThan [simp]:
    11.6      "!!k:: 'a::linorder. -greaterThan k = atMost k"
    11.7 -apply (simp add: greaterThan_def atMost_def le_def, auto)
    11.8 -done
    11.9 +  by (auto simp add: greaterThan_def atMost_def)
   11.10  
   11.11  lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
   11.12  apply (subst Compl_greaterThan [symmetric])
   11.13 @@ -135,8 +134,7 @@
   11.14  
   11.15  lemma Compl_atLeast [simp]:
   11.16      "!!k:: 'a::linorder. -atLeast k = lessThan k"
   11.17 -apply (simp add: lessThan_def atLeast_def le_def, auto)
   11.18 -done
   11.19 +  by (auto simp add: lessThan_def atLeast_def)
   11.20  
   11.21  lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)"
   11.22  by (simp add: atMost_def)
    12.1 --- a/src/HOL/Wellfounded_Recursion.thy	Fri Feb 15 16:09:10 2008 +0100
    12.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Fri Feb 15 16:09:12 2008 +0100
    12.3 @@ -6,7 +6,8 @@
    12.4  header {*Well-founded Recursion*}
    12.5  
    12.6  theory Wellfounded_Recursion
    12.7 -imports Transitive_Closure
    12.8 +imports Transitive_Closure Nat
    12.9 +uses ("Tools/function_package/size.ML")
   12.10  begin
   12.11  
   12.12  inductive
   12.13 @@ -479,6 +480,169 @@
   12.14  apply (erule Least_le)
   12.15  done
   12.16  
   12.17 +subsection {* @{typ nat} is well-founded *}
   12.18 +
   12.19 +lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
   12.20 +proof (rule ext, rule ext, rule iffI)
   12.21 +  fix n m :: nat
   12.22 +  assume "m < n"
   12.23 +  then show "(\<lambda>m n. n = Suc m)^++ m n"
   12.24 +  proof (induct n)
   12.25 +    case 0 then show ?case by auto
   12.26 +  next
   12.27 +    case (Suc n) then show ?case
   12.28 +    by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
   12.29 +  qed
   12.30 +next
   12.31 +  fix n m :: nat
   12.32 +  assume "(\<lambda>m n. n = Suc m)^++ m n"
   12.33 +  then show "m < n"
   12.34 +    by (induct n)
   12.35 +      (simp_all add: less_Suc_eq_le reflexive le_less)
   12.36 +qed
   12.37 +
   12.38 +definition
   12.39 +  pred_nat :: "(nat * nat) set" where
   12.40 +  "pred_nat = {(m, n). n = Suc m}"
   12.41 +
   12.42 +definition
   12.43 +  less_than :: "(nat * nat)set" where
   12.44 +  "less_than = pred_nat^+"
   12.45 +
   12.46 +lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
   12.47 +  unfolding less_nat_rel pred_nat_def trancl_def by simp
   12.48 +
   12.49 +lemma pred_nat_trancl_eq_le:
   12.50 +  "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"
   12.51 +  unfolding less_eq rtrancl_eq_or_trancl by auto
   12.52 +
   12.53 +lemma wf_pred_nat: "wf pred_nat"
   12.54 +  apply (unfold wf_def pred_nat_def, clarify)
   12.55 +  apply (induct_tac x, blast+)
   12.56 +  done
   12.57 +
   12.58 +lemma wf_less_than [iff]: "wf less_than"
   12.59 +  by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
   12.60 +
   12.61 +lemma trans_less_than [iff]: "trans less_than"
   12.62 +  by (simp add: less_than_def trans_trancl)
   12.63 +
   12.64 +lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
   12.65 +  by (simp add: less_than_def less_eq)
   12.66 +
   12.67 +lemma wf_less: "wf {(x, y::nat). x < y}"
   12.68 +  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
   12.69 +
   12.70 +text {* Complete induction, aka course-of-values induction *}
   12.71 +lemma nat_less_induct:
   12.72 +  assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   12.73 +  apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]])
   12.74 +  apply (rule prem)
   12.75 +  apply (unfold less_eq [symmetric], assumption)
   12.76 +  done
   12.77 +
   12.78 +lemmas less_induct = nat_less_induct [rule_format, case_names less]
   12.79 +
   12.80 +text {* Type @{typ nat} is a wellfounded order *}
   12.81 +
   12.82 +instance nat :: wellorder
   12.83 +  by intro_classes
   12.84 +    (assumption |
   12.85 +      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
   12.86 +
   12.87 +lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
   12.88 +  apply (rule nat_less_induct)
   12.89 +  apply (case_tac n)
   12.90 +  apply (case_tac [2] nat)
   12.91 +  apply (blast intro: less_trans)+
   12.92 +  done
   12.93 +
   12.94 +text {* The method of infinite descent, frequently used in number theory.
   12.95 +Provided by Roelof Oosterhuis.
   12.96 +$P(n)$ is true for all $n\in\mathbb{N}$ if
   12.97 +\begin{itemize}
   12.98 +  \item case ``0'': given $n=0$ prove $P(n)$,
   12.99 +  \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
  12.100 +        a smaller integer $m$ such that $\neg P(m)$.
  12.101 +\end{itemize} *}
  12.102 +
  12.103 +lemma infinite_descent0[case_names 0 smaller]: 
  12.104 +  "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
  12.105 +by (induct n rule: less_induct, case_tac "n>0", auto)
  12.106 +
  12.107 +text{* A compact version without explicit base case: *}
  12.108 +lemma infinite_descent:
  12.109 +  "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
  12.110 +by (induct n rule: less_induct, auto)
  12.111 +
  12.112 +text {* Infinite descent using a mapping to $\mathbb{N}$:
  12.113 +$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
  12.114 +\begin{itemize}
  12.115 +\item case ``0'': given $V(x)=0$ prove $P(x)$,
  12.116 +\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
  12.117 +\end{itemize}
  12.118 +NB: the proof also shows how to use the previous lemma. *}
  12.119 +corollary infinite_descent0_measure [case_names 0 smaller]:
  12.120 +  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
  12.121 +    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
  12.122 +  shows "P x"
  12.123 +proof -
  12.124 +  obtain n where "n = V x" by auto
  12.125 +  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
  12.126 +  proof (induct n rule: infinite_descent0)
  12.127 +    case 0 -- "i.e. $V(x) = 0$"
  12.128 +    with A0 show "P x" by auto
  12.129 +  next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
  12.130 +    case (smaller n)
  12.131 +    then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  12.132 +    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
  12.133 +    with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
  12.134 +    thus ?case by auto
  12.135 +  qed
  12.136 +  ultimately show "P x" by auto
  12.137 +qed
  12.138 +
  12.139 +text{* Again, without explicit base case: *}
  12.140 +lemma infinite_descent_measure:
  12.141 +assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
  12.142 +proof -
  12.143 +  from assms obtain n where "n = V x" by auto
  12.144 +  moreover have "!!x. V x = n \<Longrightarrow> P x"
  12.145 +  proof (induct n rule: infinite_descent, auto)
  12.146 +    fix x assume "\<not> P x"
  12.147 +    with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
  12.148 +  qed
  12.149 +  ultimately show "P x" by auto
  12.150 +qed
  12.151 +
  12.152 +text {* @{text LEAST} theorems for type @{typ nat}*}
  12.153 +
  12.154 +lemma Least_Suc:
  12.155 +     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
  12.156 +  apply (case_tac "n", auto)
  12.157 +  apply (frule LeastI)
  12.158 +  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
  12.159 +  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
  12.160 +  apply (erule_tac [2] Least_le)
  12.161 +  apply (case_tac "LEAST x. P x", auto)
  12.162 +  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
  12.163 +  apply (blast intro: order_antisym)
  12.164 +  done
  12.165 +
  12.166 +lemma Least_Suc2:
  12.167 +   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
  12.168 +by (erule (1) Least_Suc [THEN ssubst], simp)
  12.169 +
  12.170 +
  12.171 +subsection {* size of a datatype value *}
  12.172 +
  12.173 +use "Tools/function_package/size.ML"
  12.174 +
  12.175 +setup Size.setup
  12.176 +
  12.177 +lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
  12.178 +  by (induct n) simp_all
  12.179 +
  12.180  ML
  12.181  {*
  12.182  val wf_def = thm "wf_def";
    13.1 --- a/src/HOL/Wellfounded_Relations.thy	Fri Feb 15 16:09:10 2008 +0100
    13.2 +++ b/src/HOL/Wellfounded_Relations.thy	Fri Feb 15 16:09:12 2008 +0100
    13.3 @@ -18,9 +18,6 @@
    13.4  lexicographic product, and therefore does not need to be defined separately.*}
    13.5  
    13.6  constdefs
    13.7 - less_than :: "(nat*nat)set"
    13.8 -    "less_than == pred_nat^+"
    13.9 -
   13.10   measure   :: "('a => nat) => ('a * 'a)set"
   13.11      "measure == inv_image less_than"
   13.12  
   13.13 @@ -39,21 +36,10 @@
   13.14         See @{text "Library/While_Combinator.thy"} for an application.*}
   13.15  
   13.16  
   13.17 -
   13.18 -
   13.19  subsection{*Measure Functions make Wellfounded Relations*}
   13.20  
   13.21  subsubsection{*`Less than' on the natural numbers*}
   13.22  
   13.23 -lemma wf_less_than [iff]: "wf less_than"
   13.24 -by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
   13.25 -
   13.26 -lemma trans_less_than [iff]: "trans less_than"
   13.27 -by (simp add: less_than_def trans_trancl)
   13.28 -
   13.29 -lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
   13.30 -by (simp add: less_than_def less_def)
   13.31 -
   13.32  lemma full_nat_induct:
   13.33    assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
   13.34    shows "P n"
   13.35 @@ -187,7 +173,7 @@
   13.36  lemma wf_finite_psubset: "wf(finite_psubset)"
   13.37  apply (unfold finite_psubset_def)
   13.38  apply (rule wf_measure [THEN wf_subset])
   13.39 -apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric])
   13.40 +apply (simp add: measure_def inv_image_def less_than_def less_eq)
   13.41  apply (fast elim!: psubset_card_mono)
   13.42  done
   13.43  
    14.1 --- a/src/HOL/Word/Num_Lemmas.thy	Fri Feb 15 16:09:10 2008 +0100
    14.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Fri Feb 15 16:09:12 2008 +0100
    14.3 @@ -535,7 +535,7 @@
    14.4    apply (erule th2)
    14.5    done
    14.6    
    14.7 -lemmas td_gal_lt = td_gal [simplified le_def, simplified]
    14.8 +lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
    14.9  
   14.10  lemma div_mult_le: "(a :: nat) div b * b <= a"
   14.11    apply (cases b)
    15.1 --- a/src/HOL/Word/WordShift.thy	Fri Feb 15 16:09:10 2008 +0100
    15.2 +++ b/src/HOL/Word/WordShift.thy	Fri Feb 15 16:09:12 2008 +0100
    15.3 @@ -1202,7 +1202,7 @@
    15.4    apply (clarsimp simp add : test_bit_rcat word_size)
    15.5    apply (subst refl [THEN test_bit_rsplit])
    15.6      apply (simp_all add: word_size 
    15.7 -      refl [THEN length_word_rsplit_size [simplified le_def, simplified]])
    15.8 +      refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
    15.9     apply safe
   15.10     apply (erule xtr7, rule len_gt_0 [THEN dtle])+
   15.11    done
    16.1 --- a/src/HOL/ex/Primrec.thy	Fri Feb 15 16:09:10 2008 +0100
    16.2 +++ b/src/HOL/ex/Primrec.thy	Fri Feb 15 16:09:12 2008 +0100
    16.3 @@ -138,10 +138,13 @@
    16.4  text {* PROPERTY A 6 *}
    16.5  
    16.6  lemma ack2_le_ack1 [iff]: "ack (i, Suc j) \<le> ack (Suc i, j)"
    16.7 -  apply (induct j)
    16.8 -   apply simp_all
    16.9 -  apply (metis Suc_leI Suc_lessI ack_le_mono2 le_def less_ack2)
   16.10 -  done
   16.11 +proof (induct j)
   16.12 +  case 0 show ?case by simp
   16.13 +next
   16.14 +  case (Suc j) show ?case 
   16.15 +    by (auto intro!: ack_le_mono2)
   16.16 +      (metis Suc Suc_leI Suc_lessI less_ack2 linorder_not_less)
   16.17 +qed
   16.18  
   16.19  
   16.20  text {* PROPERTY A 7-, the single-step lemma *}