tidied
authorpaulson
Thu Oct 01 18:23:00 1998 +0200 (1998-10-01)
changeset 5591fbb4e1ac234d
parent 5590 477fc12adceb
child 5592 64697e426048
tidied
src/HOL/Hoare/Examples.ML
src/HOL/NatDef.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Hoare/Examples.ML	Thu Oct 01 18:22:24 1998 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.ML	Thu Oct 01 18:23:00 1998 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  by (etac gcd_nnn 4);
     1.5  by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
     1.6  by (force_tac (claset(),
     1.7 -	       simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
     1.8 +	       simpset() addsimps [not_less_iff_le, order_le_less]) 2);
     1.9  by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
    1.10  qed "Euclid_GCD";
    1.11  
     2.1 --- a/src/HOL/NatDef.ML	Thu Oct 01 18:22:24 1998 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Thu Oct 01 18:23:00 1998 +0200
     2.3 @@ -383,10 +383,6 @@
     2.4  by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1);
     2.5  qed "Suc_le_eq";
     2.6  
     2.7 -(*For instance, (Suc m < Suc n)  =   (Suc m <= n)  =  (m<n) *)
     2.8 -val le_simps = [less_Suc_eq_le, Suc_le_eq];
     2.9 -
    2.10 -
    2.11  Goalw [le_def] "m <= n ==> m <= Suc n";
    2.12  by (blast_tac (claset() addDs [Suc_lessD]) 1);
    2.13  qed "le_SucI";
    2.14 @@ -398,6 +394,9 @@
    2.15  by (blast_tac (claset() addEs [less_asym]) 1);
    2.16  qed "less_imp_le";
    2.17  
    2.18 +(*For instance, (Suc m < Suc n)  =   (Suc m <= n)  =  (m<n) *)
    2.19 +val le_simps = [less_imp_le, less_Suc_eq_le, Suc_le_eq];
    2.20 +
    2.21  
    2.22  (** Equivalence of m<=n and  m<n | m=n **)
    2.23  
    2.24 @@ -421,11 +420,8 @@
    2.25  Goal "n <= (n::nat)";
    2.26  by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    2.27  qed "le_refl";
    2.28 -AddSIs [le_refl];
    2.29  
    2.30 -(*Obvious ways of proving m<=n; 
    2.31 -  adding these rules to claset might be risky*)
    2.32 -Addsimps [le_refl, less_imp_le];
    2.33 +AddIffs [le_refl];
    2.34  
    2.35  
    2.36  Goal "[| i <= j; j < k |] ==> i < (k::nat)";
     3.1 --- a/src/HOL/arith_data.ML	Thu Oct 01 18:22:24 1998 +0200
     3.2 +++ b/src/HOL/arith_data.ML	Thu Oct 01 18:23:00 1998 +0200
     3.3 @@ -230,5 +230,5 @@
     3.4  by (Clarify_tac 2);
     3.5  by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
     3.6  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
     3.7 -				      Suc_diff_le]) 1);
     3.8 +				      Suc_diff_le, less_imp_le]) 1);
     3.9  qed_spec_mp "diff_less_mono2";