added finite_converse
authornipkow
Thu Jun 05 19:44:13 1997 +0200 (1997-06-05)
changeset 34166d9e0cca6083
parent 3415 c068bd2f0bbd
child 3417 58ccb80eb50a
added finite_converse
src/HOL/Finite.ML
     1.1 --- a/src/HOL/Finite.ML	Thu Jun 05 17:19:05 1997 +0200
     1.2 +++ b/src/HOL/Finite.ML	Thu Jun 05 19:44:13 1997 +0200
     1.3 @@ -174,6 +174,22 @@
     1.4  qed "finite_Pow_iff";
     1.5  AddIffs [finite_Pow_iff];
     1.6  
     1.7 +goal Finite.thy "finite(converse r) = finite r";
     1.8 +by(subgoal_tac "converse r = (%(x,y).(y,x))``r" 1);
     1.9 + by(Asm_simp_tac 1);
    1.10 + br iffI 1;
    1.11 +  be (rewrite_rule [inj_onto_def] finite_imageD) 1;
    1.12 +  by(simp_tac (!simpset setloop (split_tac[expand_split])) 1);
    1.13 + be finite_imageI 1;
    1.14 +by(simp_tac (!simpset addsimps [converse_def,image_def]) 1);
    1.15 +by(Auto_tac());
    1.16 + br bexI 1;
    1.17 + ba 2;
    1.18 + by(Simp_tac 1);
    1.19 +by(split_all_tac 1);
    1.20 +by(Asm_full_simp_tac 1);
    1.21 +qed "finite_converse";
    1.22 +AddIffs [finite_converse];
    1.23  
    1.24  section "Finite cardinality -- 'card'";
    1.25