new theorems; adds [le_refl, less_imp_le] as simprules
authorpaulson
Thu Aug 20 16:47:52 1998 +0200 (1998-08-20)
changeset 5354da63d9b35caf
parent 5353 0526ade4a23b
child 5355 a9f71e87f53e
new theorems; adds [le_refl, less_imp_le] as simprules
src/HOL/NatDef.ML
     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