Better simplification allows deletion of parts of proofs
authorpaulson
Tue Mar 03 15:15:04 1998 +0100 (1998-03-03)
changeset 4676335dfafb1816
parent 4675 6efc56450d09
child 4677 c4b07b8579fd
Better simplification allows deletion of parts of proofs
src/HOL/Integ/Integ.ML
     1.1 --- a/src/HOL/Integ/Integ.ML	Tue Mar 03 15:13:24 1998 +0100
     1.2 +++ b/src/HOL/Integ/Integ.ML	Tue Mar 03 15:15:04 1998 +0100
     1.3 @@ -158,32 +158,15 @@
     1.4  
     1.5  (**** znegative: the test for negative integers ****)
     1.6  
     1.7 -goal Arith.thy "!!m x n::nat. n+m=x ==> m<=x";
     1.8 -by (dtac (disjI2 RS less_or_eq_imp_le) 1);
     1.9 -by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
    1.10 -by (dtac add_leD1 1);
    1.11 -by (assume_tac 1);
    1.12 -qed "not_znegative_znat_lemma";
    1.13 -
    1.14  
    1.15  goalw Integ.thy [znegative_def, znat_def]
    1.16      "~ znegative($# n)";
    1.17  by (Simp_tac 1);
    1.18  by Safe_tac;
    1.19 -by (rtac ccontr 1);
    1.20 -by (etac notE 1);
    1.21 -by (Asm_full_simp_tac 1);
    1.22 -by (dtac not_znegative_znat_lemma 1);
    1.23 -by (fast_tac (claset() addDs [leD]) 1);
    1.24  qed "not_znegative_znat";
    1.25  
    1.26  goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
    1.27  by (simp_tac (simpset() addsimps [zminus]) 1);
    1.28 -by (REPEAT (ares_tac [exI, conjI] 1));
    1.29 -by (rtac (intrelI RS ImageI) 2);
    1.30 -by (rtac singletonI 3);
    1.31 -by (Simp_tac 2);
    1.32 -by (rtac less_add_Suc1 1);
    1.33  qed "znegative_zminus_znat";
    1.34  
    1.35  
    1.36 @@ -572,24 +555,15 @@
    1.37  by Safe_tac;
    1.38  by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
    1.39  by (safe_tac (claset() addSDs [less_eq_Suc_add]));
    1.40 -by (rename_tac "k" 1);
    1.41  by (res_inst_tac [("x","k")] exI 1);
    1.42 -(*To cancel x2, rename it to be first!*)
    1.43 -by (rename_tac "a b c" 1);
    1.44 -by (Asm_full_simp_tac 1);
    1.45 -by (asm_full_simp_tac (simpset() delsimps [add_Suc_right]
    1.46 -                                addsimps ([add_Suc_right RS sym] @ add_ac)) 1);
    1.47 +by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
    1.48  qed "zless_eq_zadd_Suc";
    1.49  
    1.50  goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
    1.51      "z < z + $#(Suc(n))";
    1.52  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
    1.53 -by Safe_tac;
    1.54 +by (Clarify_tac 1);
    1.55  by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
    1.56 -by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
    1.57 -by (rtac le_less_trans 1);
    1.58 -by (rtac lessI 2);
    1.59 -by (asm_simp_tac (simpset() addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1);
    1.60  qed "zless_zadd_Suc";
    1.61  
    1.62  goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";