Tidied proofs
authorpaulson
Fri Apr 03 11:22:51 1998 +0200 (1998-04-03)
changeset 477566b1a7c42d94
parent 4774 b4760a833480
child 4776 1f9362e769c1
Tidied proofs
src/HOL/Finite.ML
     1.1 --- a/src/HOL/Finite.ML	Fri Apr 03 11:20:41 1998 +0200
     1.2 +++ b/src/HOL/Finite.ML	Fri Apr 03 11:22:51 1998 +0200
     1.3 @@ -320,11 +320,9 @@
     1.4  by (Clarify_tac 1);
     1.5  by (case_tac "x:B" 1);
     1.6   by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
     1.7 - by (SELECT_GOAL Safe_tac 1);
     1.8 - by (rotate_tac ~1 1);
     1.9 - by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
    1.10 -by (rotate_tac ~1 1);
    1.11 -by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
    1.12 +by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
    1.13 +by (fast_tac (claset() addss
    1.14 +	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
    1.15  qed_spec_mp "card_mono";
    1.16  
    1.17  goal Finite.thy "!!A B. [| finite A; finite B |]\
    1.18 @@ -399,23 +397,20 @@
    1.19  
    1.20  (*Proper subsets*)
    1.21  goalw Finite.thy [psubset_def]
    1.22 -"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
    1.23 +    "!!B. finite B ==> !A. A < B --> card(A) < card(B)";
    1.24  by (etac finite_induct 1);
    1.25  by (Simp_tac 1);
    1.26  by (Clarify_tac 1);
    1.27  by (case_tac "x:A" 1);
    1.28  (*1*)
    1.29  by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
    1.30 -by (etac exE 1);
    1.31 -by (etac conjE 1);
    1.32 -by (hyp_subst_tac 1);
    1.33 -by (rotate_tac ~1 1);
    1.34 -by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
    1.35 +by (Clarify_tac 1);
    1.36 +by (rotate_tac ~3 1);
    1.37 +by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1);
    1.38  by (Blast_tac 1);
    1.39  (*2*)
    1.40 -by (rotate_tac ~1 1);
    1.41  by (eres_inst_tac [("P","?a<?b")] notE 1);
    1.42 -by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
    1.43 +by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1);
    1.44  by (case_tac "A=F" 1);
    1.45  by (ALLGOALS Asm_simp_tac);
    1.46  qed_spec_mp "psubset_card" ;