1.1 --- a/src/HOL/NatDef.ML Thu Aug 20 16:44:05 1998 +0200
1.2 +++ b/src/HOL/NatDef.ML Thu Aug 20 16:47:52 1998 +0200
1.3 @@ -175,6 +175,9 @@
1.4 by (blast_tac (claset() addSEs [less_irrefl]) 1);
1.5 qed "less_not_refl2";
1.6
1.7 +(* s < t ==> s ~= t *)
1.8 +bind_thm ("less_not_refl3", less_not_refl2 RS not_sym);
1.9 +
1.10
1.11 val major::prems = Goalw [less_def, pred_nat_def]
1.12 "[| i<k; k=Suc(i) ==> P; !!j. [| i<j; k=Suc(j) |] ==> P \
1.13 @@ -403,6 +406,7 @@
1.14 by (blast_tac (claset() addEs [less_asym]) 1);
1.15 qed "less_imp_le";
1.16
1.17 +
1.18 (** Equivalence of m<=n and m<n | m=n **)
1.19
1.20 Goalw [le_def] "m <= n ==> m < n | m=(n::nat)";
1.21 @@ -426,6 +430,11 @@
1.22 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
1.23 qed "le_refl";
1.24
1.25 +(*Obvious ways of proving m<=n;
1.26 + adding these rules to claset might be risky*)
1.27 +Addsimps [le_refl, less_imp_le];
1.28 +
1.29 +
1.30 Goal "[| i <= j; j < k |] ==> i < (k::nat)";
1.31 by (blast_tac (claset() addSDs [le_imp_less_or_eq]
1.32 addIs [less_trans]) 1);
1.33 @@ -459,6 +468,9 @@
1.34 by (blast_tac (claset() addSEs [less_asym]) 1);
1.35 qed "nat_less_le";
1.36
1.37 +(* [| m <= n; m ~= n |] ==> m < n *)
1.38 +bind_thm ("le_neq_implies_less", [nat_less_le, conjI] MRS iffD2);
1.39 +
1.40 (* Axiom 'linorder_linear' of class 'linorder': *)
1.41 Goal "(m::nat) <= n | n <= m";
1.42 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
1.43 @@ -466,6 +478,14 @@
1.44 by (Blast_tac 1);
1.45 qed "nat_le_linear";
1.46
1.47 +Goal "~ n < m ==> (n < Suc m) = (n = m)";
1.48 +by (blast_tac (claset() addSEs [less_SucE]) 1);
1.49 +qed "not_less_less_Suc_eq";
1.50 +
1.51 +
1.52 +(*Rewrite (n < Suc m) to (n=m) if ~ n<m or m<=n hold.
1.53 + Not suitable as default simprules because they often lead to looping*)
1.54 +val not_less_simps = [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq];
1.55
1.56 (** max
1.57