Renamed lessD to Suc_leI
authorpaulson
Mon May 26 12:39:57 1997 +0200 (1997-05-26)
changeset 334345986997f1fe
parent 3342 ec3b55fcb165
child 3344 b3e39a2987c1
Renamed lessD to Suc_leI
src/HOL/Hoare/Arith2.ML
src/HOL/NatDef.ML
     1.1 --- a/src/HOL/Hoare/Arith2.ML	Mon May 26 12:38:29 1997 +0200
     1.2 +++ b/src/HOL/Hoare/Arith2.ML	Mon May 26 12:39:57 1997 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  by (rtac (Suc_diff_n RS sym) 1);
     1.5  by (rtac le_less_trans 1);
     1.6  by (etac (not_less_eq RS subst) 2);
     1.7 -by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1);
     1.8 +by (rtac (hd ([diff_less_Suc RS Suc_leI] RL [Suc_le_mono RS subst])) 1);
     1.9  qed "diff_add_not_assoc";
    1.10  
    1.11  val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
     2.1 --- a/src/HOL/NatDef.ML	Mon May 26 12:38:29 1997 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Mon May 26 12:39:57 1997 +0200
     2.3 @@ -402,6 +402,9 @@
     2.4  by (rtac not_less_eq 1);
     2.5  qed "le_eq_less_Suc";
     2.6  
     2.7 +(*  m<=n ==> m < Suc n  *)
     2.8 +bind_thm ("le_imp_less_Suc", le_eq_less_Suc RS iffD1);
     2.9 +
    2.10  goalw thy [le_def] "0 <= n";
    2.11  by (rtac not_less0 1);
    2.12  qed "le0";
    2.13 @@ -464,7 +467,7 @@
    2.14  goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    2.15  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    2.16  by (blast_tac (!claset addSEs [less_irrefl,less_asym]) 1);
    2.17 -qed "lessD";
    2.18 +qed "Suc_leI";  (*formerly called lessD*)
    2.19  
    2.20  goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    2.21  by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    2.22 @@ -479,7 +482,7 @@
    2.23  qed "Suc_le_lessD";
    2.24  
    2.25  goal thy "(Suc m <= n) = (m < n)";
    2.26 -by (blast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
    2.27 +by (blast_tac (!claset addIs [Suc_leI, Suc_le_lessD]) 1);
    2.28  qed "Suc_le_eq";
    2.29  
    2.30  goalw thy [le_def] "!!m. m <= n ==> m <= Suc n";
    2.31 @@ -493,6 +496,8 @@
    2.32  by (blast_tac (!claset addEs [less_asym]) 1);
    2.33  qed "less_imp_le";
    2.34  
    2.35 +(** Equivalence of m<=n and  m<n | m=n **)
    2.36 +
    2.37  goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
    2.38  by (cut_facts_tac [less_linear] 1);
    2.39  by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
    2.40 @@ -503,7 +508,7 @@
    2.41  by (blast_tac (!claset addSEs [less_irrefl] addEs [less_asym]) 1);
    2.42  qed "less_or_eq_imp_le";
    2.43  
    2.44 -goal thy "(x <= (y::nat)) = (x < y | x=y)";
    2.45 +goal thy "(m <= (n::nat)) = (m < n | m=n)";
    2.46  by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
    2.47  qed "le_eq_less_or_eq";
    2.48  
    2.49 @@ -642,7 +647,7 @@
    2.50  val less_incr_rhs = Suc_mono RS Suc_lessD;
    2.51  val less_decr_lhs = Suc_lessD;
    2.52  val less_trans_Suc = less_trans_Suc;
    2.53 -val leI = lessD RS (Suc_le_mono RS iffD1);
    2.54 +val leI = Suc_leI RS (Suc_le_mono RS iffD1);
    2.55  val not_lessI = leI RS leD
    2.56  val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n"
    2.57    (fn _ => [etac swap2 1, etac leD 1]);