author lcp Thu, 24 Nov 1994 00:32:43 +0100 changeset 735 f99621230c2e parent 734 a3e0fd3c0f2f child 736 a8d1758bb113
moved version of Cantors theorem to ZF/Perm.ML
 src/ZF/Perm.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/Perm.ML	Thu Nov 24 00:32:12 1994 +0100
+++ b/src/ZF/Perm.ML	Thu Nov 24 00:32:43 1994 +0100
@@ -1,9 +1,9 @@
-(*  Title: 	ZF/perm.ML
+(*  Title: 	ZF/Perm.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

-For perm.thy.  The theory underlying permutation groups
+The theory underlying permutation groups
-- Composition of relations, the identity relation
-- Injections, surjections, bijections
-- Lemmas for the Schroeder-Bernstein Theorem
@@ -43,6 +43,13 @@
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([lam_type]@prems)) ));
val lam_surjective = result();

+(*Cantor's theorem revisited*)
+goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))";
+by (safe_tac ZF_cs);
+by (cut_facts_tac [cantor] 1);
+by (fast_tac subset_cs 1);
+val cantor_surj = result();
+

(** Injective function space **)

@@ -235,7 +242,7 @@
THEN prune_params_tac)

(** Domain and Range -- see Suppes, section 3.1 **)

@@ -298,7 +305,7 @@

goalw Perm.thy [function_def]
"!!f g. [| function(g);  function(f) |] ==> function(f O g)";
val comp_function = result();

goalw Perm.thy [Pi_def]
@@ -389,7 +396,8 @@
val left_comp_inverse = result();

(*right inverse of composition; one inclusion is
-        f: A->B ==> f O converse(f) <= id(B) *)
+	        f: A->B ==> f O converse(f) <= id(B)
+*)
val [prem] = goalw Perm.thy [surj_def]
"f: surj(A,B) ==> f O converse(f) = id(B)";
val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
@@ -466,8 +474,7 @@
by (fast_tac (ZF_cs addIs rls) 1);
val surj_image = result();

-goal Perm.thy
-    "!!f. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A)``A = f``A";
+goal Perm.thy "!!f. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A)``A = f``A";
by (rtac equalityI 1);
by (SELECT_GOAL (rewtac restrict_def) 2);
by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2```