# HG changeset patch
# User paulson
# Date 888934504 -3600
# Node ID 335dfafb18165f7b20d9b5c5a49dda935d39ddd2
# Parent  6efc56450d09532fd996c72f5774ccdcb49f2194
Better simplification allows deletion of parts of proofs

diff -r 6efc56450d09 -r 335dfafb1816 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Tue Mar 03 15:13:24 1998 +0100
+++ b/src/HOL/Integ/Integ.ML	Tue Mar 03 15:15:04 1998 +0100
@@ -158,32 +158,15 @@
 
 (**** znegative: the test for negative integers ****)
 
-goal Arith.thy "!!m x n::nat. n+m=x ==> m<=x";
-by (dtac (disjI2 RS less_or_eq_imp_le) 1);
-by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
-by (dtac add_leD1 1);
-by (assume_tac 1);
-qed "not_znegative_znat_lemma";
-
 
 goalw Integ.thy [znegative_def, znat_def]
     "~ znegative($# n)";
 by (Simp_tac 1);
 by Safe_tac;
-by (rtac ccontr 1);
-by (etac notE 1);
-by (Asm_full_simp_tac 1);
-by (dtac not_znegative_znat_lemma 1);
-by (fast_tac (claset() addDs [leD]) 1);
 qed "not_znegative_znat";
 
 goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
 by (simp_tac (simpset() addsimps [zminus]) 1);
-by (REPEAT (ares_tac [exI, conjI] 1));
-by (rtac (intrelI RS ImageI) 2);
-by (rtac singletonI 3);
-by (Simp_tac 2);
-by (rtac less_add_Suc1 1);
 qed "znegative_zminus_znat";
 
 
@@ -572,24 +555,15 @@
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
 by (safe_tac (claset() addSDs [less_eq_Suc_add]));
-by (rename_tac "k" 1);
 by (res_inst_tac [("x","k")] exI 1);
-(*To cancel x2, rename it to be first!*)
-by (rename_tac "a b c" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() delsimps [add_Suc_right]
-                                addsimps ([add_Suc_right RS sym] @ add_ac)) 1);
+by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
 qed "zless_eq_zadd_Suc";
 
 goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
     "z < z + $#(Suc(n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by Safe_tac;
+by (Clarify_tac 1);
 by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
-by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
-by (rtac le_less_trans 1);
-by (rtac lessI 2);
-by (asm_simp_tac (simpset() addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1);
 qed "zless_zadd_Suc";
 
 goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";