# 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
+