# HG changeset patch
# User paulson
# Date 994428272 -7200
# Node ID 1605aeb98fd5262797e7aaa7703c49ba222e0c5d
# Parent  d7711be8c3a913c201a8a49d0f741a6028f9bb63
two Isar tactic scripts

diff -r d7711be8c3a9 -r 1605aeb98fd5 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Tue Jul 03 22:11:09 2001 +0200
+++ b/src/ZF/IsaMakefile	Fri Jul 06 16:04:32 2001 +0200
@@ -109,7 +109,7 @@
 ZF-ex: ZF $(LOG)/ZF-ex.gz
 
 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \
-  ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
+  ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
   ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Commutation.ML ex/Commutation.thy \
   ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \
   ex/LList.ML ex/LList.thy \
@@ -118,7 +118,7 @@
   ex/NatSum.ML ex/NatSum.thy  ex/Primrec_defs.ML ex/Primrec_defs.thy \
   ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
   ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
-  ex/Term.ML ex/Term.thy ex/misc.ML
+  ex/Term.ML ex/Term.thy ex/misc.thy
 	@$(ISATOOL) usedir $(OUT)/ZF ex
 
 
diff -r d7711be8c3a9 -r 1605aeb98fd5 src/ZF/ex/BinEx.ML
--- a/src/ZF/ex/BinEx.ML	Tue Jul 03 22:11:09 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,122 +0,0 @@
-(*  Title:      ZF/ex/BinEx.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Examples of performing binary arithmetic by simplification
-*)
-
-context Main.thy;
-
-(*All runtimes below are on a 300MHz Pentium*)
-
-Goal "#13  $+  #19 = #32";
-by (Simp_tac 1);    (*0 secs*)
-result();
-
-Goal "#1234  $+  #5678 = #6912";
-by (Simp_tac 1);    (*190 msec*)
-result();
-
-Goal "#1359  $+  #-2468 = #-1109";
-by (Simp_tac 1);    (*160 msec*)
-result();
-
-Goal "#93746  $+  #-46375 = #47371";
-by (Simp_tac 1);    (*300 msec*)
-result();
-
-Goal "$- #65745 = #-65745";
-by (Simp_tac 1);    (*80 msec*)
-result();
-
-(* negation of ~54321 *)
-Goal "$- #-54321 = #54321";
-by (Simp_tac 1);    (*90 msec*)
-result();
-
-Goal "#13  $*  #19 = #247";
-by (Simp_tac 1);    (*110 msec*)
-result();
-
-Goal "#-84  $*  #51 = #-4284";
-by (Simp_tac 1);    (*210 msec*)
-result();
-
-(*The worst case for 8-bit operands *)
-Goal "#255  $*  #255 = #65025";
-by (Simp_tac 1);    (*730 msec*)
-result();
-
-Goal "#1359  $*  #-2468 = #-3354012";
-by (Simp_tac 1);    (*1.04 secs*)
-result();
-
-
-(** Comparisons **)
-
-Goal "(#89) $* #10 \\<noteq> #889";  
-by (Simp_tac 1); 
-result();
-
-Goal "(#13) $< #18 $- #4";  
-by (Simp_tac 1); 
-result();
-
-Goal "(#-345) $< #-242 $+ #-100";  
-by (Simp_tac 1); 
-result();
-
-Goal "(#13557456) $< #18678654";  
-by (Simp_tac 1); 
-result();
-
-Goal "(#999999) $<= (#1000001 $+ #1) $- #2";  
-by (Simp_tac 1); 
-result();
-
-Goal "(#1234567) $<= #1234567";  
-by (Simp_tac 1); 
-result();
-
-
-(*** Quotient and remainder!! [they could be faster] ***)
-
-Goal "#23 zdiv #3 = #7";
-by (Simp_tac 1); 
-result();
-
-Goal "#23 zmod #3 = #2";
-by (Simp_tac 1); 
-result();
-
-(** negative dividend **)
-
-Goal "#-23 zdiv #3 = #-8";
-by (Simp_tac 1); 
-result();
-
-Goal "#-23 zmod #3 = #1";
-by (Simp_tac 1); 
-result();
-
-(** negative divisor **)
-
-Goal "#23 zdiv #-3 = #-8";
-by (Simp_tac 1); 
-result();
-
-Goal "#23 zmod #-3 = #-1";
-by (Simp_tac 1); 
-result();
-
-(** Negative dividend and divisor **)
-
-Goal "#-23 zdiv #-3 = #7";
-by (Simp_tac 1); 
-result();
-
-Goal "#-23 zmod #-3 = #-2";
-by (Simp_tac 1); 
-result();
-
diff -r d7711be8c3a9 -r 1605aeb98fd5 src/ZF/ex/BinEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/BinEx.thy	Fri Jul 06 16:04:32 2001 +0200
@@ -0,0 +1,99 @@
+(*  Title:      ZF/ex/BinEx.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Examples of performing binary arithmetic by simplification
+*)
+
+theory BinEx = Main:
+(*All runtimes below are on a 300MHz Pentium*)
+
+lemma "#13  $+  #19 = #32"
+by simp (*0 secs*)
+
+lemma "#1234  $+  #5678 = #6912"
+by simp (*190 msec*)
+
+lemma "#1359  $+  #-2468 = #-1109"
+by simp (*160 msec*)
+
+lemma "#93746  $+  #-46375 = #47371"
+by simp (*300 msec*)
+
+lemma "$- #65745 = #-65745"
+by simp (*80 msec*)
+
+(* negation of ~54321 *)
+lemma "$- #-54321 = #54321"
+by simp (*90 msec*)
+
+lemma "#13  $*  #19 = #247"
+by simp (*110 msec*)
+
+lemma "#-84  $*  #51 = #-4284"
+by simp (*210 msec*)
+
+(*The worst case for 8-bit operands *)
+lemma "#255  $*  #255 = #65025"
+by simp (*730 msec*)
+
+lemma "#1359  $*  #-2468 = #-3354012"
+by simp (*1.04 secs*)
+
+
+(** Comparisons **)
+
+lemma "(#89) $* #10 \<noteq> #889"
+by simp
+
+lemma "(#13) $< #18 $- #4"
+by simp
+
+lemma "(#-345) $< #-242 $+ #-100"
+by simp
+
+lemma "(#13557456) $< #18678654"
+by simp
+
+lemma "(#999999) $<= (#1000001 $+ #1) $- #2"
+by simp
+
+lemma "(#1234567) $<= #1234567"
+by simp
+
+
+(*** Quotient and remainder!! [they could be faster] ***)
+
+lemma "#23 zdiv #3 = #7"
+by simp
+
+lemma "#23 zmod #3 = #2"
+by simp
+
+(** negative dividend **)
+
+lemma "#-23 zdiv #3 = #-8"
+by simp
+
+lemma "#-23 zmod #3 = #1"
+by simp
+
+(** negative divisor **)
+
+lemma "#23 zdiv #-3 = #-8"
+by simp
+
+lemma "#23 zmod #-3 = #-1"
+by simp
+
+(** Negative dividend and divisor **)
+
+lemma "#-23 zdiv #-3 = #7"
+by simp
+
+lemma "#-23 zmod #-3 = #-2"
+by simp
+
+end
+
diff -r d7711be8c3a9 -r 1605aeb98fd5 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Tue Jul 03 22:11:09 2001 +0200
+++ b/src/ZF/ex/ROOT.ML	Fri Jul 06 16:04:32 2001 +0200
@@ -6,12 +6,12 @@
 Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
 *)
 
-time_use     "misc.ML";
+time_use_thy "misc";
 time_use_thy "Primes";          (*GCD theory*)
 time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
 time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
 time_use_thy "Limit";           (*Inverse limit construction of domains*)
-time_use     "BinEx";		(*Binary integer arithmetic*)
+time_use_thy "BinEx";		(*Binary integer arithmetic*)
 
 (** Datatypes **)
 time_use_thy "BT";              (*binary trees*)
diff -r d7711be8c3a9 -r 1605aeb98fd5 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Tue Jul 03 22:11:09 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(*  Title:      ZF/ex/misc.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Miscellaneous examples for Zermelo-Fraenkel Set Theory 
-Composition of homomorphisms, Pastre's examples, ...
-*)
-
-(*These two are cited in Benzmueller and Kohlhase's system description of LEO,
-  CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
-
-Goal "(X = Y Un Z) <-> (Y \\<subseteq> X & Z \\<subseteq> X & (\\<forall>V. Y \\<subseteq> V & Z \\<subseteq> V --> X \\<subseteq> V))";
-by (blast_tac (claset() addSIs [equalityI]) 1);
-qed "";
-
-(*the dual of the previous one*)
-Goal "(X = Y Int Z) <-> (X \\<subseteq> Y & X \\<subseteq> Z & (\\<forall>V. V \\<subseteq> Y & V \\<subseteq> Z --> V \\<subseteq> X))";
-by (blast_tac (claset() addSIs [equalityI]) 1);
-qed "";
-
-(*trivial example of term synthesis: apparently hard for some provers!*)
-Goal "a \\<noteq> b ==> a:?X & b \\<notin> ?X";
-by (Blast_tac 1);
-qed "";
-
-(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
-Goal "\\<forall>x \\<in> S. \\<forall>y \\<in> S. x \\<subseteq> y ==> \\<exists>z. S \\<subseteq> {z}";
-by (Blast_tac 1);
-qed "";
-
-(*variant of the benchmark above*)
-Goal "\\<forall>x \\<in> S. Union(S) \\<subseteq> x ==> \\<exists>z. S \\<subseteq> {z}";
-by (Blast_tac 1);
-qed "";
-
-context Perm.thy;
-
-(*Example 12 (credited to Peter Andrews) from
- W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
- In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
- Ellis Horwood, 53-100 (1979). *)
-Goal "(\\<forall>F. {x}: F --> {y}:F) --> (\\<forall>A. x \\<in> A --> y \\<in> A)";
-by (Best_tac 1);
-qed "";
-
-
-(*** Composition of homomorphisms is a homomorphism ***)
-
-(*Given as a challenge problem in
-  R. Boyer et al.,
-  Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
-  JAR 2 (1986), 287-327 
-*)
-
-(*collecting the relevant lemmas*)
-Addsimps [comp_fun, SigmaI, apply_funtype];
-
-(*This version uses a super application of simp_tac.  Needs setloop to help
-  proving conditions of rewrites such as comp_fun_apply;
-  rewriting does not instantiate Vars*)
-goal Perm.thy
-    "(\\<forall>A f B g. hom(A,f,B,g) = \
-\          {H \\<in> A->B. f \\<in> A*A->A & g \\<in> B*B->B & \
-\                    (\\<forall>x \\<in> A. \\<forall>y \\<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
-\    J \\<in> hom(A,f,B,g) & K \\<in> hom(B,g,C,h) -->  \
-\    (K O J) \\<in> hom(A,f,C,h)";
-by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
-qed "";
-
-(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
-val [hom_def] = goal Perm.thy
-    "(!! A f B g. hom(A,f,B,g) == \
-\          {H \\<in> A->B. f \\<in> A*A->A & g \\<in> B*B->B & \
-\                    (\\<forall>x \\<in> A. \\<forall>y \\<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
-\    J \\<in> hom(A,f,B,g) & K \\<in> hom(B,g,C,h) -->  \
-\    (K O J) \\<in> hom(A,f,C,h)";
-by (rewtac hom_def);
-by Safe_tac;
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
-qed "comp_homs";
-
-
-(** A characterization of functions, suggested by Tobias Nipkow **)
-
-Goalw [Pi_def, function_def]
-    "r \\<in> domain(r)->B  <->  r \\<subseteq> domain(r)*B & (\\<forall>X. r `` (r -`` X) \\<subseteq> X)";
-by (Best_tac 1);
-qed "";
-
-
-(**** From D Pastre.  Automatic theorem proving in set theory. 
-         Artificial Intelligence, 10:1--27, 1978.
-             These examples require forward reasoning! ****)
-
-(*reduce the clauses to units by type checking -- beware of nontermination*)
-fun forw_typechk tyrls [] = []
-  | forw_typechk tyrls clauses =
-    let val (units, others) = partition (has_fewer_prems 1) clauses
-    in  gen_union eq_thm (units, forw_typechk tyrls (tyrls RL others))
-    end;
-
-(*A crude form of forward reasoning*)
-fun forw_iterate tyrls rls facts 0 = facts
-  | forw_iterate tyrls rls facts n =
-      let val facts' = 
-          gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts)
-      in  forw_iterate tyrls rls facts' (n-1)  end;
-
-val pastre_rls =
-    [comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2];
-
-fun pastre_facts (fact1::fact2::fact3::prems) = 
-    forw_iterate (prems @ [comp_surj, comp_inj, comp_fun])
-               pastre_rls [fact1,fact2,fact3] 4;
-
-val prems = goalw Perm.thy [bij_def]
-    "[| (h O g O f): inj(A,A);          \
-\       (f O h O g): surj(B,B);         \
-\       (g O f O h): surj(C,C);         \
-\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
-by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-qed "pastre1";
-
-val prems = goalw Perm.thy [bij_def]
-    "[| (h O g O f): surj(A,A);         \
-\       (f O h O g): inj(B,B);          \
-\       (g O f O h): surj(C,C);         \
-\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
-by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-qed "pastre2";
-
-val prems = goalw Perm.thy [bij_def]
-    "[| (h O g O f): surj(A,A);         \
-\       (f O h O g): surj(B,B);         \
-\       (g O f O h): inj(C,C);          \
-\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
-by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-qed "pastre3";
-
-val prems = goalw Perm.thy [bij_def]
-    "[| (h O g O f): surj(A,A);         \
-\       (f O h O g): inj(B,B);          \
-\       (g O f O h): inj(C,C);          \
-\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
-by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-qed "pastre4";
-
-val prems = goalw Perm.thy [bij_def]
-    "[| (h O g O f): inj(A,A);          \
-\       (f O h O g): surj(B,B);         \
-\       (g O f O h): inj(C,C);          \
-\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
-by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-qed "pastre5";
-
-val prems = goalw Perm.thy [bij_def]
-    "[| (h O g O f): inj(A,A);          \
-\       (f O h O g): inj(B,B);          \
-\       (g O f O h): surj(C,C);         \
-\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
-by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
-qed "pastre6";
-
-(** Yet another example... **)
-
-goal Perm.thy
-    "(\\<lambda>Z \\<in> Pow(A+B). <{x \\<in> A. Inl(x):Z}, {y \\<in> B. Inr(y):Z}>) \
-\    \\<in> bij(Pow(A+B), Pow(A)*Pow(B))";
-by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x \\<in> X} Un {Inr(y).y \\<in> Y}")] 
-    lam_bijective 1);
-(*Auto_tac no longer proves it*)
-by Auto_tac;
-by (ALLGOALS Blast_tac);  
-qed "Pow_sum_bij";
-
-(*As a special case, we have  bij(Pow(A*B), A -> Pow B)  *)
-goal Perm.thy
-    "(\\<lambda>r \\<in> Pow(Sigma(A,B)). \\<lambda>x \\<in> A. r``{x}) \
-\    \\<in> bij(Pow(Sigma(A,B)), \\<Pi>x \\<in> A. Pow(B(x)))";
-by (res_inst_tac [("d", "%f. \\<Union>x \\<in> A. \\<Union>y \\<in> f`x. {<x,y>}")] lam_bijective 1);
-by (blast_tac (claset() addDs [apply_type]) 2);
-by (blast_tac (claset() addIs [lam_type]) 1);
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-by (rtac fun_extension 1);
-by (assume_tac 2);
-by (rtac (singletonI RS lam_type) 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "Pow_Sigma_bij";
diff -r d7711be8c3a9 -r 1605aeb98fd5 src/ZF/ex/misc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/misc.thy	Fri Jul 06 16:04:32 2001 +0200
@@ -0,0 +1,149 @@
+(*  Title:      ZF/ex/misc.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Miscellaneous examples for Zermelo-Fraenkel Set Theory 
+Composition of homomorphisms, Pastre's examples, ...
+*)
+
+theory misc = Main:
+
+
+
+(*These two are cited in Benzmueller and Kohlhase's system description of LEO,
+  CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
+lemma "(X = Y Un Z) <-> (Y \<subseteq> X & Z \<subseteq> X & (\<forall>V. Y \<subseteq> V & Z \<subseteq> V --> X \<subseteq> V))"
+by (blast intro!: equalityI)
+
+(*the dual of the previous one*)
+lemma "(X = Y Int Z) <-> (X \<subseteq> Y & X \<subseteq> Z & (\<forall>V. V \<subseteq> Y & V \<subseteq> Z --> V \<subseteq> X))"
+by (blast intro!: equalityI)
+
+(*trivial example of term synthesis: apparently hard for some provers!*)
+lemma "a \<noteq> b ==> a:?X & b \<notin> ?X"
+by blast
+
+(*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
+lemma "\<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y ==> \<exists>z. S \<subseteq> {z}"
+by blast
+
+(*variant of the benchmark above*)
+lemma "\<forall>x \<in> S. Union(S) \<subseteq> x ==> \<exists>z. S \<subseteq> {z}"
+by blast
+
+(*Example 12 (credited to Peter Andrews) from
+ W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
+ In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
+ Ellis Horwood, 53-100 (1979). *)
+lemma "(\<forall>F. {x} \<in> F --> {y} \<in> F) --> (\<forall>A. x \<in> A --> y \<in> A)"
+by best
+
+
+(*** Composition of homomorphisms is a homomorphism ***)
+
+(*Given as a challenge problem in
+  R. Boyer et al.,
+  Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
+  JAR 2 (1986), 287-327 
+*)
+
+(*collecting the relevant lemmas*)
+declare comp_fun [simp] SigmaI [simp] apply_funtype [simp]
+
+(*Force helps prove conditions of rewrites such as comp_fun_apply, since
+  rewriting does not instantiate Vars.*)
+lemma "(\<forall>A f B g. hom(A,f,B,g) =  
+           {H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &  
+                     (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) -->  
+       J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) -->   
+       (K O J) \<in> hom(A,f,C,h)"
+by force
+
+(*Another version , with meta-level rewriting*)
+lemma "(!! A f B g. hom(A,f,B,g) ==  
+           {H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &  
+                     (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) 
+       ==> J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) --> (K O J) \<in> hom(A,f,C,h)"
+by force
+
+
+
+(** A characterization of functions suggested by Tobias Nipkow **)
+
+lemma "r \<in> domain(r)->B  <->  r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> X)"
+apply (unfold Pi_def function_def)
+apply best
+done
+
+(**** From D Pastre.  Automatic theorem proving in set theory. 
+         Artificial Intelligence, 10:1--27, 1978.
+
+      Previously, these were done using ML code, but blast manages fine.
+****)
+
+lemmas compIs [intro] = comp_surj comp_inj comp_fun [intro]
+lemmas compDs [dest] =  comp_mem_injD1 comp_mem_surjD1 
+                        comp_mem_injD2 comp_mem_surjD2
+
+lemma pastre1: 
+    "[| (h O g O f) \<in> inj(A,A);           
+        (f O h O g) \<in> surj(B,B);          
+        (g O f O h) \<in> surj(C,C);          
+        f \<in> A->B;  g \<in> B->C;  h \<in> C->A |] ==> h \<in> bij(C,A)";
+by (unfold bij_def, blast)
+
+lemma pastre3: 
+    "[| (h O g O f) \<in> surj(A,A);          
+        (f O h O g) \<in> surj(B,B);          
+        (g O f O h) \<in> inj(C,C);           
+        f \<in> A->B;  g \<in> B->C;  h \<in> C->A |] ==> h \<in> bij(C,A)"
+by (unfold bij_def, blast)
+
+lemma pastre4: 
+    "[| (h O g O f) \<in> surj(A,A);          
+        (f O h O g) \<in> inj(B,B);           
+        (g O f O h) \<in> inj(C,C);           
+        f \<in> A->B;  g \<in> B->C;  h \<in> C->A |] ==> h \<in> bij(C,A)"
+by (unfold bij_def, blast)
+
+lemma pastre5: 
+    "[| (h O g O f) \<in> inj(A,A);           
+        (f O h O g) \<in> surj(B,B);          
+        (g O f O h) \<in> inj(C,C);           
+        f \<in> A->B;  g \<in> B->C;  h \<in> C->A |] ==> h \<in> bij(C,A)"
+by (unfold bij_def, blast)
+
+lemma pastre6: 
+    "[| (h O g O f) \<in> inj(A,A);           
+        (f O h O g) \<in> inj(B,B);           
+        (g O f O h) \<in> surj(C,C);          
+        f \<in> A->B;  g \<in> B->C;  h \<in> C->A |] ==> h \<in> bij(C,A)"
+by (unfold bij_def, blast)
+
+
+(** Yet another example... **)
+
+lemma Pow_sum_bij:
+    "(\<lambda>Z \<in> Pow(A+B). <{x \<in> A. Inl(x) \<in> Z}, {y \<in> B. Inr(y) \<in> Z}>)  
+     \<in> bij(Pow(A+B), Pow(A)*Pow(B))"
+apply (rule_tac d = "%<X,Y>. {Inl (x). x \<in> X} Un {Inr (y). y \<in> Y}" 
+       in lam_bijective)
+apply force+
+done
+
+(*As a special case, we have  bij(Pow(A*B), A -> Pow B)  *)
+lemma Pow_Sigma_bij:
+    "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})  
+     \<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
+apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
+apply (blast intro: lam_type)
+apply (blast dest: apply_type)
+apply simp_all
+apply fast (*strange, but blast can't do it*)
+apply (rule fun_extension)
+apply auto
+by blast
+
+end
+