src/HOL/Finite.ML
changeset 4830 bd73675adbed
parent 4775 66b1a7c42d94
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Finite.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Finite.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -111,23 +111,23 @@
     1.4  AddIffs [finite_Diff_singleton];
     1.5  
     1.6  (*Lemma for proving finite_imageD*)
     1.7 -goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
     1.8 +goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A";
     1.9  by (etac finite_induct 1);
    1.10   by (ALLGOALS Asm_simp_tac);
    1.11  by (Clarify_tac 1);
    1.12  by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
    1.13   by (Clarify_tac 1);
    1.14 - by (full_simp_tac (simpset() addsimps [inj_onto_def]) 1);
    1.15 + by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
    1.16   by (Blast_tac 1);
    1.17  by (thin_tac "ALL A. ?PP(A)" 1);
    1.18  by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
    1.19  by (Clarify_tac 1);
    1.20  by (res_inst_tac [("x","xa")] bexI 1);
    1.21  by (ALLGOALS 
    1.22 -    (asm_full_simp_tac (simpset() addsimps [inj_onto_image_set_diff])));
    1.23 +    (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
    1.24  val lemma = result();
    1.25  
    1.26 -goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
    1.27 +goal Finite.thy "!!A. [| finite(f``A);  inj_on f A |] ==> finite A";
    1.28  by (dtac lemma 1);
    1.29  by (Blast_tac 1);
    1.30  qed "finite_imageD";
    1.31 @@ -156,7 +156,7 @@
    1.32  by (rtac finite_subset 2);
    1.33  by (assume_tac 3);
    1.34  by (ALLGOALS
    1.35 -    (fast_tac (claset() addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
    1.36 +    (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD])));
    1.37  val lemma = result();
    1.38  
    1.39  goal Finite.thy "finite(Pow A) = finite A";
    1.40 @@ -174,8 +174,8 @@
    1.41  by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
    1.42   by (Asm_simp_tac 1);
    1.43   by (rtac iffI 1);
    1.44 -  by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
    1.45 -  by (simp_tac (simpset() addsplits [expand_split]) 1);
    1.46 +  by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
    1.47 +  by (simp_tac (simpset() addsplits [split_split]) 1);
    1.48   by (etac finite_imageI 1);
    1.49  by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
    1.50  by Auto_tac;
    1.51 @@ -370,11 +370,11 @@
    1.52  qed "card_insert";
    1.53  Addsimps [card_insert];
    1.54  
    1.55 -goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A";
    1.56 +goal Finite.thy "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A";
    1.57  by (etac finite_induct 1);
    1.58  by (ALLGOALS Asm_simp_tac);
    1.59  by Safe_tac;
    1.60 -by (rewtac inj_onto_def);
    1.61 +by (rewtac inj_on_def);
    1.62  by (Blast_tac 1);
    1.63  by (stac card_insert_disjoint 1);
    1.64  by (etac finite_imageI 1);
    1.65 @@ -387,9 +387,9 @@
    1.66  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
    1.67  by (stac card_Un_disjoint 1);
    1.68  by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
    1.69 -by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
    1.70 +by (subgoal_tac "inj_on (insert x) (Pow F)" 1);
    1.71  by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
    1.72 -by (rewtac inj_onto_def);
    1.73 +by (rewtac inj_on_def);
    1.74  by (blast_tac (claset() addSEs [equalityE]) 1);
    1.75  qed "card_Pow";
    1.76  Addsimps [card_Pow];