--- a/src/ZF/Perm.thy Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Perm.thy Tue Mar 06 16:06:52 2012 +0000
@@ -15,7 +15,7 @@
definition
(*composition of relations and functions; NOT Suppes's relative product*)
comp :: "[i,i]=>i" (infixr "O" 60) where
- "r O s == {xz \<in> domain(s)*range(r) .
+ "r O s == {xz \<in> domain(s)*range(r) .
\<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
definition
@@ -58,17 +58,17 @@
text{* A function with a right inverse is a surjection *}
-lemma f_imp_surjective:
+lemma f_imp_surjective:
"[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y |]
==> f: surj(A,B)"
by (simp add: surj_def, blast)
-lemma lam_surjective:
- "[| !!x. x:A ==> c(x): B;
- !!y. y:B ==> d(y): A;
- !!y. y:B ==> c(d(y)) = y
+lemma lam_surjective:
+ "[| !!x. x:A ==> c(x): B;
+ !!y. y:B ==> d(y): A;
+ !!y. y:B ==> c(d(y)) = y
|] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)"
-apply (rule_tac d = d in f_imp_surjective)
+apply (rule_tac d = d in f_imp_surjective)
apply (simp_all add: lam_type)
done
@@ -76,7 +76,7 @@
lemma cantor_surj: "f \<notin> surj(A,Pow(A))"
apply (unfold surj_def, safe)
apply (cut_tac cantor)
-apply (best del: subsetI)
+apply (best del: subsetI)
done
@@ -88,7 +88,7 @@
done
text{*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*}
-lemma inj_equality:
+lemma inj_equality:
"[| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c"
apply (unfold inj_def)
apply (blast dest: Pair_mem_PiD)
@@ -104,8 +104,8 @@
apply (blast intro: subst_context [THEN box_equals])
done
-lemma lam_injective:
- "[| !!x. x:A ==> c(x): B;
+lemma lam_injective:
+ "[| !!x. x:A ==> c(x): B;
!!x. x:A ==> d(c(x)) = x |]
==> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)"
apply (rule_tac d = d in f_imp_injective)
@@ -127,17 +127,17 @@
text{* f: bij(A,B) ==> f: A->B *}
lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun]
-lemma lam_bijective:
- "[| !!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
+lemma lam_bijective:
+ "[| !!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
|] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
apply (unfold bij_def)
apply (blast intro!: lam_injective lam_surjective)
done
-lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
+lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
==> (\<lambda>z\<in>{f(y). y:x}. THE y. f(y) = z) \<in> bij({f(y). y:x}, x)"
apply (rule_tac d = f in lam_bijective)
apply (auto simp add: the_equality2)
@@ -171,7 +171,7 @@
lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
apply (simp add: inj_def id_def)
-apply (blast intro: lam_type)
+apply (blast intro: lam_type)
done
lemmas id_inj = subset_refl [THEN id_subset_inj]
@@ -186,13 +186,13 @@
apply (blast intro: id_inj id_surj)
done
-lemma subset_iff_id: "A \<subseteq> B <-> id(A) \<in> A->B"
+lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B"
apply (unfold id_def)
apply (force intro!: lam_type dest: apply_type)
done
text{*@{term id} as the identity relation*}
-lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
+lemma id_iff [simp]: "<x,y> \<in> id(A) \<longleftrightarrow> x=y & y \<in> A"
by auto
@@ -224,7 +224,7 @@
lemma right_inverse_lemma:
"[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"
-by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
+by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
(*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! *)
@@ -239,14 +239,14 @@
lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
apply (rule f_imp_injective)
-apply (erule inj_converse_fun, clarify)
+apply (erule inj_converse_fun, clarify)
apply (rule right_inverse)
apply assumption
-apply blast
+apply blast
done
lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
-by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
+by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
range_of_fun [THEN apply_type])
text{*Adding this as an intro! rule seems to cause looping*}
@@ -264,17 +264,17 @@
lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> \<in> r O s"
by (unfold comp_def, blast)
-lemma compE [elim!]:
- "[| xz \<in> r O s;
+lemma compE [elim!]:
+ "[| xz \<in> r O s;
!!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P |]
==> P"
by (unfold comp_def, blast)
-lemma compEpair:
- "[| <a,c> \<in> r O s;
+lemma compEpair:
+ "[| <a,c> \<in> r O s;
!!y. [| <a,y>:s; <y,c>:r |] ==> P |]
==> P"
-by (erule compE, simp)
+by (erule compE, simp)
lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
by blast
@@ -302,7 +302,7 @@
by (auto simp add: inj_def Pi_iff function_def)
lemma inj_bij_range: "f: inj(A,B) ==> f \<in> bij(A,range(f))"
- by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
+ by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
subsection{*Other Results*}
@@ -319,7 +319,7 @@
by blast
(*left identity of composition; provable inclusions are
- id(A) O r \<subseteq> r
+ id(A) O r \<subseteq> r
and [| r<=A*B; B<=C |] ==> r \<subseteq> id(C) O r *)
lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
by blast
@@ -339,44 +339,44 @@
text{*Don't think the premises can be weakened much*}
lemma comp_fun: "[| g: A->B; f: B->C |] ==> (f O g) \<in> A->C"
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
-apply (subst range_rel_subset [THEN domain_comp_eq], auto)
+apply (subst range_rel_subset [THEN domain_comp_eq], auto)
done
(*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
lemma comp_fun_apply [simp]:
"[| g: A->B; a:A |] ==> (f O g)`a = f`(g`a)"
-apply (frule apply_Pair, assumption)
+apply (frule apply_Pair, assumption)
apply (simp add: apply_def image_comp)
-apply (blast dest: apply_equality)
+apply (blast dest: apply_equality)
done
text{*Simplifies compositions of lambda-abstractions*}
-lemma comp_lam:
+lemma comp_lam:
"[| !!x. x:A ==> b(x): B |]
==> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))"
-apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B")
+apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B")
apply (rule fun_extension)
apply (blast intro: comp_fun lam_funtype)
apply (rule lam_funtype)
- apply simp
-apply (simp add: lam_type)
+ apply simp
+apply (simp add: lam_type)
done
lemma comp_inj:
"[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) \<in> inj(A,C)"
-apply (frule inj_is_fun [of g])
-apply (frule inj_is_fun [of f])
+apply (frule inj_is_fun [of g])
+apply (frule inj_is_fun [of f])
apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
- apply (blast intro: comp_fun, simp)
+ apply (blast intro: comp_fun, simp)
done
-lemma comp_surj:
+lemma comp_surj:
"[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) \<in> surj(A,C)"
apply (unfold surj_def)
apply (blast intro!: comp_fun comp_fun_apply)
done
-lemma comp_bij:
+lemma comp_bij:
"[| g: bij(A,B); f: bij(B,C) |] ==> (f O g) \<in> bij(A,C)"
apply (unfold bij_def)
apply (blast intro: comp_inj comp_surj)
@@ -386,14 +386,14 @@
subsection{*Dual Properties of @{term inj} and @{term surj}*}
text{*Useful for proofs from
- D Pastre. Automatic theorem proving in set theory.
+ D Pastre. Automatic theorem proving in set theory.
Artificial Intelligence, 10:1--27, 1978.*}
-lemma comp_mem_injD1:
+lemma comp_mem_injD1:
"[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"
-by (unfold inj_def, force)
+by (unfold inj_def, force)
-lemma comp_mem_injD2:
+lemma comp_mem_injD2:
"[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"
apply (unfold inj_def surj_def, safe)
apply (rule_tac x1 = x in bspec [THEN bexE])
@@ -403,17 +403,17 @@
apply (simp (no_asm_simp))
done
-lemma comp_mem_surjD1:
+lemma comp_mem_surjD1:
"[| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"
apply (unfold surj_def)
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
done
-lemma comp_mem_surjD2:
+lemma comp_mem_surjD2:
"[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"
apply (unfold inj_def surj_def, safe)
-apply (drule_tac x = "f`y" in bspec, auto)
+apply (drule_tac x = "f`y" in bspec, auto)
apply (blast intro: apply_funtype)
done
@@ -422,16 +422,16 @@
text{*left inverse of composition; one inclusion is
@{term "f: A->B ==> id(A) \<subseteq> converse(f) O f"} *}
lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
-apply (unfold inj_def, clarify)
-apply (rule equalityI)
- apply (auto simp add: apply_iff, blast)
+apply (unfold inj_def, clarify)
+apply (rule equalityI)
+ apply (auto simp add: apply_iff, blast)
done
text{*right inverse of composition; one inclusion is
@{term "f: A->B ==> f O converse(f) \<subseteq> id(B)"} *}
-lemma right_comp_inverse:
+lemma right_comp_inverse:
"f: surj(A,B) ==> f O converse(f) = id(B)"
-apply (simp add: surj_def, clarify)
+apply (simp add: surj_def, clarify)
apply (rule equalityI)
apply (best elim: domain_type range_type dest: apply_equality2)
apply (blast intro: apply_Pair)
@@ -440,8 +440,8 @@
subsubsection{*Proving that a Function is a Bijection*}
-lemma comp_eq_id_iff:
- "[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (\<forall>y\<in>B. f`(g`y)=y)"
+lemma comp_eq_id_iff:
+ "[| f: A->B; g: B->A |] ==> f O g = id(B) \<longleftrightarrow> (\<forall>y\<in>B. f`(g`y)=y)"
apply (unfold id_def, safe)
apply (drule_tac t = "%h. h`y " in subst_context)
apply simp
@@ -450,7 +450,7 @@
apply auto
done
-lemma fg_imp_bijective:
+lemma fg_imp_bijective:
"[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) |] ==> f \<in> bij(A,B)"
apply (unfold bij_def)
apply (simp add: comp_eq_id_iff)
@@ -462,7 +462,7 @@
lemma invertible_imp_bijective:
"[| converse(f): B->A; f: A->B |] ==> f \<in> bij(A,B)"
-by (simp add: fg_imp_bijective comp_eq_id_iff
+by (simp add: fg_imp_bijective comp_eq_id_iff
left_inverse_lemma right_inverse_lemma)
subsubsection{*Unions of Functions*}
@@ -471,25 +471,25 @@
text{*Theorem by KG, proof by LCP*}
lemma inj_disjoint_Un:
- "[| f: inj(A,B); g: inj(C,D); B \<inter> D = 0 |]
+ "[| f: inj(A,B); g: inj(C,D); B \<inter> D = 0 |]
==> (\<lambda>a\<in>A \<union> C. if a:A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)"
-apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z"
+apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z"
in lam_injective)
apply (auto simp add: inj_is_fun [THEN apply_type])
done
-lemma surj_disjoint_Un:
- "[| f: surj(A,B); g: surj(C,D); A \<inter> C = 0 |]
+lemma surj_disjoint_Un:
+ "[| f: surj(A,B); g: surj(C,D); A \<inter> C = 0 |]
==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)"
-apply (simp add: surj_def fun_disjoint_Un)
-apply (blast dest!: domain_of_fun
+apply (simp add: surj_def fun_disjoint_Un)
+apply (blast dest!: domain_of_fun
intro!: fun_disjoint_apply1 fun_disjoint_apply2)
done
text{*A simple, high-level proof; the version for injections follows from it,
- using @term{f:inj(A,B) <-> f:bij(A,range(f))} *}
+ using @{term "f:inj(A,B) \<longleftrightarrow> f:bij(A,range(f))"} *}
lemma bij_disjoint_Un:
- "[| f: bij(A,B); g: bij(C,D); A \<inter> C = 0; B \<inter> D = 0 |]
+ "[| f: bij(A,B); g: bij(C,D); A \<inter> C = 0; B \<inter> D = 0 |]
==> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)"
apply (rule invertible_imp_bijective)
apply (subst converse_Un)
@@ -501,25 +501,25 @@
lemma surj_image:
"f: Pi(A,B) ==> f: surj(A, f``A)"
-apply (simp add: surj_def)
-apply (blast intro: apply_equality apply_Pair Pi_type)
+apply (simp add: surj_def)
+apply (blast intro: apply_equality apply_Pair Pi_type)
done
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
by (auto simp add: restrict_def)
-lemma restrict_inj:
+lemma restrict_inj:
"[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)"
apply (unfold inj_def)
-apply (safe elim!: restrict_type2, auto)
+apply (safe elim!: restrict_type2, auto)
done
lemma restrict_surj: "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)"
apply (insert restrict_type2 [THEN surj_image])
-apply (simp add: restrict_image)
+apply (simp add: restrict_image)
done
-lemma restrict_bij:
+lemma restrict_bij:
"[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"
apply (simp add: inj_def bij_def)
apply (blast intro: restrict_surj surj_is_fun)
@@ -541,8 +541,8 @@
done
-lemma inj_extend:
- "[| f: inj(A,B); a\<notin>A; b\<notin>B |]
+lemma inj_extend:
+ "[| f: inj(A,B); a\<notin>A; b\<notin>B |]
==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))"
apply (unfold inj_def)
apply (force intro: apply_type simp add: fun_extend)