theorem le_diff_conv2; tidying and expandshort
authorpaulson
Fri Sep 18 14:36:03 1998 +0200 (1998-09-18)
changeset 5497497215d66441
parent 5496 42d13691be86
child 5498 7b81cae2774f
theorem le_diff_conv2; tidying and expandshort
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Sep 18 14:34:06 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Sep 18 14:36:03 1998 +0200
     1.3 @@ -130,9 +130,9 @@
     1.4  (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
     1.5  Goal "m<n --> (? k. n=Suc(m+k))";
     1.6  by (induct_tac "n" 1);
     1.7 -by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
     1.8 +by (ALLGOALS (simp_tac (simpset() addsimps [le_eq_less_or_eq])));
     1.9  by (blast_tac (claset() addSEs [less_SucE] 
    1.10 -                       addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.11 +                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.12  qed_spec_mp "less_eq_Suc_add";
    1.13  
    1.14  Goal "n <= ((m + n)::nat)";
    1.15 @@ -186,8 +186,7 @@
    1.16  
    1.17  Goal "m+k<=n --> m<=(n::nat)";
    1.18  by (induct_tac "k" 1);
    1.19 -by (ALLGOALS Asm_simp_tac);
    1.20 -by (blast_tac (claset() addDs [Suc_leD]) 1);
    1.21 +by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
    1.22  qed_spec_mp "add_leD1";
    1.23  
    1.24  Goal "m+k<=n ==> k<=(n::nat)";
    1.25 @@ -201,12 +200,10 @@
    1.26  
    1.27  (*needs !!k for add_ac to work*)
    1.28  Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
    1.29 -by (safe_tac (claset() addSDs [less_eq_Suc_add]));
    1.30 -by (asm_full_simp_tac
    1.31 -    (simpset() delsimps [add_Suc_right]
    1.32 -               addsimps ([add_Suc_right RS sym, add_left_cancel] @ add_ac)) 1);
    1.33 -by (etac subst 1);
    1.34 -by (simp_tac (simpset() addsimps [less_add_Suc1]) 1);
    1.35 +by (auto_tac (claset(),
    1.36 +	      simpset() delsimps [add_Suc_right]
    1.37 +	                addsimps ([less_iff_Suc_add,
    1.38 +				   add_Suc_right RS sym] @ add_ac)));
    1.39  qed "less_add_eq_less";
    1.40  
    1.41  
    1.42 @@ -374,14 +371,14 @@
    1.43  Goal "0<n ==> n - Suc i < n";
    1.44  by (exhaust_tac "n" 1);
    1.45  by Safe_tac;
    1.46 -by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
    1.47 +by (asm_simp_tac (simpset() addsimps le_simps) 1);
    1.48  qed "diff_Suc_less";
    1.49  Addsimps [diff_Suc_less];
    1.50  
    1.51  Goal "i<n ==> n - Suc i < n - i";
    1.52  by (exhaust_tac "n" 1);
    1.53 -by Safe_tac;
    1.54 -by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc, Suc_diff_le]) 1);
    1.55 +by (auto_tac (claset(),
    1.56 +	      simpset() addsimps ([Suc_diff_le]@le_simps)));
    1.57  qed "diff_Suc_less_diff";
    1.58  
    1.59  Goal "m - n <= Suc m - n";
    1.60 @@ -427,7 +424,7 @@
    1.61  
    1.62  Goal "(m-n = 0) = (m <= n)";
    1.63  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.64 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_eq_less_Suc])));
    1.65 +by (ALLGOALS Asm_simp_tac);
    1.66  qed "diff_is_0_eq";
    1.67  Addsimps [diff_is_0_eq RS iffD2];
    1.68  
    1.69 @@ -623,23 +620,29 @@
    1.70  qed "add_less_imp_less_diff";
    1.71  
    1.72  Goal "(i < j-k) = (i+k < (j::nat))";
    1.73 -br iffI 1;
    1.74 - by(case_tac "k <= j" 1);
    1.75 -  bd le_add_diff_inverse2 1;
    1.76 -  by(dres_inst_tac [("k","k")] add_less_mono1 1);
    1.77 -  by(Asm_full_simp_tac 1);
    1.78 - by(rotate_tac 1 1);
    1.79 - by(asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
    1.80 -be add_less_imp_less_diff 1;
    1.81 +by (rtac iffI 1);
    1.82 + by (case_tac "k <= j" 1);
    1.83 +  by (dtac le_add_diff_inverse2 1);
    1.84 +  by (dres_inst_tac [("k","k")] add_less_mono1 1);
    1.85 +  by (Asm_full_simp_tac 1);
    1.86 + by (rotate_tac 1 1);
    1.87 + by (asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
    1.88 +by (etac add_less_imp_less_diff 1);
    1.89  qed "less_diff_conv";
    1.90  
    1.91 -Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
    1.92 -by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc, less_diff_conv,
    1.93 -					   Suc_diff_le RS sym]) 1);
    1.94 +Goal "(j-k <= (i::nat)) = (j <= i+k)";
    1.95 +by (simp_tac (simpset() addsimps [less_diff_conv, le_def]) 1);
    1.96  qed "le_diff_conv";
    1.97  
    1.98 +Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
    1.99 +by (asm_full_simp_tac
   1.100 +    (simpset() delsimps [less_Suc_eq_le]
   1.101 +               addsimps [less_Suc_eq_le RS sym, less_diff_conv,
   1.102 +			 Suc_diff_le RS sym]) 1);
   1.103 +qed "le_diff_conv2";
   1.104 +
   1.105  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
   1.106 -by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
   1.107 +by (asm_full_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
   1.108  qed "Suc_diff_Suc";
   1.109  
   1.110  Goal "i <= (n::nat) ==> n - (n - i) = i";
   1.111 @@ -653,7 +656,7 @@
   1.112  by (etac rev_mp 1);
   1.113  by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
   1.114  by (Simp_tac 1);
   1.115 -by (simp_tac (simpset() addsimps [less_add_Suc2, less_imp_le]) 1);
   1.116 +by (simp_tac (simpset() addsimps [le_add2, less_imp_le]) 1);
   1.117  by (Simp_tac 1);
   1.118  qed "le_add_diff";
   1.119  
   1.120 @@ -682,15 +685,14 @@
   1.121  
   1.122  Goal "n - Suc i <= n - i";
   1.123  by (case_tac "i<n" 1);
   1.124 -bd diff_Suc_less_diff 1;
   1.125 -by (auto_tac (claset(), simpset() addsimps [leI RS le_imp_less_Suc]));
   1.126 +by (dtac diff_Suc_less_diff 1);
   1.127 +by (auto_tac (claset(), simpset() addsimps [leI]));
   1.128  qed "diff_Suc_le_diff";
   1.129  AddIffs [diff_Suc_le_diff];
   1.130  
   1.131  Goal "0 < n ==> (m <= n-1) = (m<n)";
   1.132  by (exhaust_tac "n" 1);
   1.133 -by Auto_tac;
   1.134 -by (ALLGOALS trans_tac);
   1.135 +by (auto_tac (claset(), simpset() addsimps le_simps));
   1.136  qed "le_pred_eq";
   1.137  
   1.138  Goal "0 < n ==> (m-1 < n) = (m<=n)";