Tidied some proofs
authorpaulson
Tue Jun 04 12:49:04 1996 +0200 (1996-06-04)
changeset 17879246e236a57f
parent 1786 8a31d85d27b8
child 1788 ca62fab4ce92
Tidied some proofs
src/ZF/Perm.ML
     1.1 --- a/src/ZF/Perm.ML	Mon Jun 03 17:10:56 1996 +0200
     1.2 +++ b/src/ZF/Perm.ML	Tue Jun 04 12:49:04 1996 +0200
     1.3 @@ -57,6 +57,7 @@
     1.4  by (etac CollectD1 1);
     1.5  qed "inj_is_fun";
     1.6  
     1.7 +(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
     1.8  goalw Perm.thy [inj_def]
     1.9      "!!f A B. [| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
    1.10  by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
    1.11 @@ -69,13 +70,10 @@
    1.12  
    1.13  (** A function with a left inverse is an injection **)
    1.14  
    1.15 -val prems = goal Perm.thy
    1.16 -    "[| f: A->B;  !!x. x:A ==> d(f`x)=x |] ==> f: inj(A,B)";
    1.17 -by (asm_simp_tac (ZF_ss addsimps ([inj_def] @ prems)) 1);
    1.18 -by (safe_tac ZF_cs);
    1.19 -by (eresolve_tac [subst_context RS box_equals] 1);
    1.20 -by (REPEAT (ares_tac prems 1));
    1.21 -qed "f_imp_injective";
    1.22 +goal Perm.thy "!!f. [| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
    1.23 +by (asm_simp_tac (ZF_ss addsimps [inj_def]) 1);
    1.24 +by (deepen_tac (ZF_cs addEs [subst_context RS box_equals]) 0 1);
    1.25 +bind_thm ("f_imp_injective", ballI RSN (2,result()));
    1.26  
    1.27  val prems = goal Perm.thy
    1.28      "[| !!x. x:A ==> c(x): B;           \
    1.29 @@ -151,23 +149,19 @@
    1.30  qed "id_bij";
    1.31  
    1.32  goalw Perm.thy [id_def] "A <= B <-> id(A) : A->B";
    1.33 -by (safe_tac ZF_cs);
    1.34 -by (fast_tac (ZF_cs addSIs [lam_type]) 1);
    1.35 -by (dtac apply_type 1);
    1.36 -by (assume_tac 1);
    1.37 -by (asm_full_simp_tac ZF_ss 1);
    1.38 +by (fast_tac (ZF_cs addSIs [lam_type] addDs [apply_type] addss ZF_ss) 1);
    1.39  qed "subset_iff_id";
    1.40  
    1.41  
    1.42  (*** Converse of a function ***)
    1.43  
    1.44 -val [prem] = goal Perm.thy "f: inj(A,B) ==> converse(f) : range(f)->A";
    1.45 -by (cut_facts_tac [prem] 1);
    1.46 -by (asm_full_simp_tac (ZF_ss addsimps [inj_def, Pi_iff, domain_converse]) 1);
    1.47 -by (rtac conjI 1);
    1.48 -by (deepen_tac ZF_cs 0 2);
    1.49 -by (simp_tac (ZF_ss addsimps [function_def, converse_iff]) 1);
    1.50 -by (fast_tac (ZF_cs addEs [prem RSN (3,inj_equality)]) 1);
    1.51 +goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) : range(f)->A";
    1.52 +by (asm_simp_tac 
    1.53 +    (ZF_ss addsimps [Pi_iff, function_def, 
    1.54 +		     domain_converse, converse_iff]) 1);
    1.55 +by (eresolve_tac [CollectE] 1);
    1.56 +by (asm_simp_tac (ZF_ss addsimps [apply_iff]) 1);
    1.57 +by (fast_tac (ZF_cs addDs [fun_is_rel]) 1);
    1.58  qed "inj_converse_fun";
    1.59  
    1.60  (** Equations for converse(f) **)
    1.61 @@ -198,11 +192,9 @@
    1.62  by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
    1.63  qed "right_inverse";
    1.64  
    1.65 -goalw Perm.thy [bij_def]
    1.66 -    "!!f. [| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b";
    1.67 -by (EVERY1 [etac IntE, etac right_inverse, 
    1.68 -            etac (surj_range RS ssubst),
    1.69 -            assume_tac]);
    1.70 +goal Perm.thy "!!f. [| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b";
    1.71 +by (fast_tac (ZF_cs addss
    1.72 +	      (ZF_ss addsimps [bij_def, right_inverse, surj_range])) 1);
    1.73  qed "right_inverse_bij";
    1.74  
    1.75  (** Converses of injections, surjections, bijections **)
    1.76 @@ -215,17 +207,14 @@
    1.77  qed "inj_converse_inj";
    1.78  
    1.79  goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): surj(range(f), A)";
    1.80 -by (REPEAT (ares_tac [f_imp_surjective, inj_converse_fun] 1));
    1.81 -by (REPEAT (ares_tac [left_inverse] 2));
    1.82 -by (REPEAT (ares_tac [inj_is_fun, range_of_fun RS apply_type] 1));
    1.83 +by (ITER_DEEPEN (has_fewer_prems 1)
    1.84 +    (ares_tac [f_imp_surjective, inj_converse_fun, left_inverse,
    1.85 +	       inj_is_fun, range_of_fun RS apply_type]));
    1.86  qed "inj_converse_surj";
    1.87  
    1.88  goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";
    1.89 -by (etac IntE 1);
    1.90 -by (eresolve_tac [(surj_range RS subst)] 1);
    1.91 -by (rtac IntI 1);
    1.92 -by (etac inj_converse_inj 1);
    1.93 -by (etac inj_converse_surj 1);
    1.94 +by (fast_tac (ZF_cs addEs [surj_range RS subst, inj_converse_inj,
    1.95 +			   inj_converse_surj]) 1);
    1.96  qed "bij_converse_bij";
    1.97  
    1.98  
    1.99 @@ -316,13 +305,12 @@
   1.100  by (fast_tac (ZF_cs addIs [compI] addSEs [compE, Pair_inject]) 1);
   1.101  qed "comp_function";
   1.102  
   1.103 -goalw Perm.thy [Pi_def]
   1.104 -    "!!f g. [| g: A->B;  f: B->C |] ==> (f O g) : A->C";
   1.105 -by (safe_tac subset_cs);
   1.106 -by (asm_simp_tac (ZF_ss addsimps [comp_function]) 3);
   1.107 -by (rtac (range_rel_subset RS domain_comp_eq RS ssubst) 2 THEN assume_tac 3);
   1.108 -by (fast_tac ZF_cs 2);
   1.109 -by (asm_simp_tac (ZF_ss addsimps [comp_rel]) 1);
   1.110 +goal Perm.thy "!!f g. [| g: A->B;  f: B->C |] ==> (f O g) : A->C";
   1.111 +by (asm_full_simp_tac
   1.112 +    (ZF_ss addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
   1.113 +           setloop etac conjE) 1);
   1.114 +by (rtac (range_rel_subset RS domain_comp_eq RS ssubst) 1 THEN assume_tac 2);
   1.115 +by (fast_tac ZF_cs 1);
   1.116  qed "comp_fun";
   1.117  
   1.118  goal Perm.thy "!!f g. [| g: A->B;  f: B->C;  a:A |] ==> (f O g)`a = f`(g`a)";
   1.119 @@ -407,12 +395,10 @@
   1.120  
   1.121  (*left inverse of composition; one inclusion is
   1.122          f: A->B ==> id(A) <= converse(f) O f *)
   1.123 -val [prem] = goal Perm.thy
   1.124 -    "f: inj(A,B) ==> converse(f) O f = id(A)";
   1.125 -val injfD = prem RSN (3,inj_equality);
   1.126 -by (cut_facts_tac [prem RS inj_is_fun] 1);
   1.127 -by (fast_tac (comp_cs addIs [equalityI,apply_Pair] 
   1.128 -                      addEs [domain_type, make_elim injfD]) 1);
   1.129 +goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) O f = id(A)";
   1.130 +by (fast_tac (comp_cs addIs [equalityI, apply_Pair] 
   1.131 +                      addEs [domain_type]
   1.132 +               addss (ZF_ss addsimps [apply_iff])) 1);
   1.133  qed "left_comp_inverse";
   1.134  
   1.135  (*right inverse of composition; one inclusion is
   1.136 @@ -548,15 +534,8 @@
   1.137  goalw Perm.thy [inj_def]
   1.138      "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
   1.139  \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
   1.140 -(*cannot use safe_tac: must preserve the implication*)
   1.141 -by (etac CollectE 1);
   1.142 -by (rtac CollectI 1);
   1.143 -by (etac fun_extend 1);
   1.144 -by (REPEAT (ares_tac [ballI] 1));
   1.145 -by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
   1.146 -(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
   1.147 -  using ZF_ss!  But FOL_ss ignores the assumption...*)
   1.148 -by (ALLGOALS (asm_simp_tac 
   1.149 -              (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
   1.150 -by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
   1.151 +by (fast_tac (ZF_cs  addIs [apply_type]
   1.152 +	             addss (ZF_ss addsimps [fun_extend, fun_extend_apply2,
   1.153 +					    fun_extend_apply1]) ) 1);
   1.154  qed "inj_extend";
   1.155 +