# HG changeset patch
# User lcp
# Date 775754686 -7200
# Node ID 77e36960fd9e5cf2bf416c9cf04d05ec6ec39a59
# Parent  9c724f7085f9ea4d3a5f1d31737988bb0ad6166a
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
many other tidies

diff -r 9c724f7085f9 -r 77e36960fd9e src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Jul 29 16:07:22 1994 +0200
+++ b/src/ZF/Perm.ML	Mon Aug 01 17:24:46 1994 +0200
@@ -26,6 +26,23 @@
 by (best_tac (ZF_cs addIs [equalityI,apply_Pair] addEs [range_type]) 1);
 val surj_range = result();
 
+(** A function with a right inverse is a surjection **)
+
+val prems = goalw Perm.thy [surj_def]
+    "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y \
+\    |] ==> f: surj(A,B)";
+by (fast_tac (ZF_cs addIs prems) 1);
+val f_imp_surjective = result();
+
+val prems = goal Perm.thy
+    "[| !!x. x:A ==> c(x): B;		\
+\       !!y. y:B ==> d(y): A; 		\
+\       !!y. y:B ==> c(d(y)) = y      	\
+\    |] ==> (lam x:A.c(x)) : surj(A,B)";
+by (res_inst_tac [("d", "d")] f_imp_surjective 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([lam_type]@prems)) ));
+val lam_surjective = result();
+
 
 (** Injective function space **)
 
@@ -70,6 +87,15 @@
 (* f: bij(A,B) ==> f: A->B *)
 val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
 
+val prems = goalw Perm.thy [bij_def]
+    "[| !!x. x:A ==> c(x): B;		\
+\       !!y. y:B ==> d(y): A;  		\
+\       !!x. x:A ==> d(c(x)) = x;      	\
+\       !!y. y:B ==> c(d(y)) = y	\
+\    |] ==> (lam x:A.c(x)) : bij(A,B)";
+by (REPEAT (ares_tac (prems @ [IntI, lam_injective, lam_surjective]) 1));
+val lam_bijective = result();
+
 
 (** Identity function **)
 
@@ -110,7 +136,7 @@
 val id_bij = result();
 
 
-(** Converse of a relation **)
+(*** Converse of a function ***)
 
 val [prem] = goal Perm.thy "f: inj(A,B) ==> converse(f) : range(f)->A";
 by (rtac (prem RS inj_is_fun RS PiE) 1);
@@ -120,11 +146,7 @@
 by flexflex_tac;
 val inj_converse_fun = result();
 
-val prems = goalw Perm.thy [surj_def]
-    "f: inj(A,B) ==> converse(f): surj(range(f), A)";
-by (fast_tac (ZF_cs addIs (prems@[inj_converse_fun,apply_Pair,apply_equality,
-			 converseI,inj_is_fun])) 1);
-val inj_converse_surj = result();
+(** Equations for converse(f) **)
 
 (*The premises are equivalent to saying that f is injective...*) 
 val prems = goal Perm.thy
@@ -145,8 +167,9 @@
 by (REPEAT (resolve_tac prems 1));
 val right_inverse_lemma = result();
 
-goal Perm.thy
-    "!!f. [| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b";
+(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
+  No: they would not imply that converse(f) was a function! *)
+goal Perm.thy "!!f. [| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b";
 by (rtac right_inverse_lemma 1);
 by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
 val right_inverse = result();
@@ -158,18 +181,21 @@
 	    assume_tac]);
 val right_inverse_bij = result();
 
-val prems = goal Perm.thy
-    "f: inj(A,B) ==> converse(f): inj(range(f), A)";
-by (rewtac inj_def);  (*rewrite subgoal but not prems!!*)
-by (cut_facts_tac prems 1);
-by (safe_tac ZF_cs);
-(*apply f to both sides and simplify using right_inverse
-  -- could also use  etac[subst_context RS box_equals]  in this proof *)
-by (rtac simp_equals 2);
-by (REPEAT (eresolve_tac [inj_converse_fun, right_inverse RS sym, ssubst] 1
-     ORELSE ares_tac [refl,rangeI] 1));
+(** Converses of injections, surjections, bijections **)
+
+goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): inj(range(f), A)";
+by (resolve_tac [f_imp_injective] 1);
+by (eresolve_tac [inj_converse_fun] 1);
+by (resolve_tac [right_inverse] 1);
+by (REPEAT (assume_tac 1));
 val inj_converse_inj = result();
 
+goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): surj(range(f), A)";
+by (REPEAT (ares_tac [f_imp_surjective, inj_converse_fun] 1));
+by (REPEAT (ares_tac [left_inverse] 2));
+by (REPEAT (ares_tac [inj_is_fun, range_of_fun RS apply_type] 1));
+val inj_converse_surj = result();
+
 goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";
 by (etac IntE 1);
 by (eresolve_tac [(surj_range RS subst)] 1);
@@ -272,10 +298,12 @@
 		      apply_Pair,apply_type] 1));
 val comp_fun_apply = result();
 
-goalw Perm.thy [inj_def]
-    "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
-by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1
-     ORELSE step_tac (ZF_cs addSIs [comp_fun,apply_type,comp_fun_apply]) 1));
+goal Perm.thy "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
+by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
+    f_imp_injective 1);
+by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
+by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply, left_inverse] 
+                        setsolver type_auto_tac [inj_is_fun, apply_type]) 1);
 val comp_inj = result();
 
 goalw Perm.thy [surj_def]
@@ -356,20 +384,6 @@
 
 (** Proving that a function is a bijection **)
 
-val prems = 
-goalw Perm.thy [bij_def, inj_def, surj_def]
-    "[| !!x. x:A ==> c(x): B;		\
-\       !!y. y:B ==> d(y): A;  		\
-\       !!x. x:A ==> d(c(x)) = x;      	\
-\       !!y. y:B ==> c(d(y)) = y	\
-\    |] ==> (lam x:A.c(x)) : bij(A,B)";
-by (simp_tac (ZF_ss addsimps ([lam_type]@prems)) 1);
-by (safe_tac ZF_cs);
-by (eresolve_tac [subst_context RS box_equals] 1);
-by (REPEAT (ares_tac prems 1));
-by (fast_tac (ZF_cs addIs prems) 1);
-val lam_bijective = result();
-
 goalw Perm.thy [id_def]
     "!!f A B. [| f: A->B;  g: B->A |] ==> \
 \             f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
@@ -381,29 +395,21 @@
 by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
 val comp_eq_id_iff = result();
 
-goalw Perm.thy [bij_def, inj_def, surj_def]
+goalw Perm.thy [bij_def]
     "!!f A B. [| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) \
 \             |] ==> f : bij(A,B)";
 by (asm_full_simp_tac (ZF_ss addsimps [comp_eq_id_iff]) 1);
-by (safe_tac ZF_cs);
-(*Apply g to both sides then simplify*)
-by (dres_inst_tac [("t", "op `(g)"), ("a", "f`x")] subst_context 1);
-by (asm_full_simp_tac ZF_ss 1);
-by (fast_tac (ZF_cs addIs [apply_type]) 1);
+by (REPEAT (ares_tac [conjI, f_imp_injective, f_imp_surjective] 1
+       ORELSE eresolve_tac [bspec, apply_type] 1));
 val fg_imp_bijective = result();
 
 goal Perm.thy "!!f A. [| f: A->A;  f O f = id(A) |] ==> f : bij(A,A)";
 by (REPEAT (ares_tac [fg_imp_bijective] 1));
 val nilpotent_imp_bijective = result();
 
-(*Injective case applies converse(f) to both sides then simplifies
-    using left_inverse_lemma*)
-goalw Perm.thy [bij_def,inj_def,surj_def]
-    "!!f A B. [| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)";
-val cf_cong = read_instantiate_sg (sign_of Perm.thy)
-                [("t","%x.?f`x")]   subst_context;
-by (fast_tac (ZF_cs addIs [left_inverse_lemma, right_inverse_lemma, apply_type]
-		    addEs [cf_cong RS box_equals]) 1);
+goal Perm.thy "!!f A B. [| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)";
+by (asm_simp_tac (ZF_ss addsimps [fg_imp_bijective, comp_eq_id_iff, 
+				  left_inverse_lemma, right_inverse_lemma]) 1);
 val invertible_imp_bijective = result();
 
 (** Unions of functions -- cf similar theorems on func.ML **)
@@ -425,7 +431,7 @@
 val surj_disjoint_Un = result();
 
 (*A simple, high-level proof; the version for injections follows from it,
-  using  f:inj(A,B)<->f:bij(A,range(f))  *)
+  using  f:inj(A,B) <-> f:bij(A,range(f))  *)
 goal Perm.thy
     "!!f g. [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
 \           (f Un g) : bij(A Un C, B Un D)";