--- a/src/HOL/Finite_Set.thy Fri Sep 27 13:24:29 2002 +0200
+++ b/src/HOL/Finite_Set.thy Fri Sep 27 16:44:50 2002 +0200
@@ -989,24 +989,28 @@
done
lemma card_inj_on_le:
- "finite A ==> finite B ==> f ` A \<subseteq> B ==> inj_on f A ==> card A <= card B"
+ "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
by (auto intro: card_mono simp add: card_image [symmetric])
-lemma card_bij_eq: "finite A ==> finite B ==>
- f ` A \<subseteq> B ==> inj_on f A ==> g ` B \<subseteq> A ==> inj_on g B ==> card A = card B"
+lemma card_bij_eq:
+ "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
+ finite A; finite B |] ==> card A = card B"
by (auto intro: le_anti_sym card_inj_on_le)
-lemma constr_bij: "finite A ==> x \<notin> A ==>
- card {B. EX C. C <= A & card(C) = k & B = insert x C} =
+text{*There are as many subsets of @{term A} having cardinality @{term k}
+ as there are sets obtained from the former by inserting a fixed element
+ @{term x} into each.*}
+lemma constr_bij:
+ "[|finite A; x \<notin> A|] ==>
+ card {B. EX C. C <= A & card(C) = k & B = insert x C} =
card {B. B <= A & card(B) = k}"
apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
- apply (rule_tac B = "Pow (insert x A) " in finite_subset)
- apply (rule_tac [3] B = "Pow (A) " in finite_subset)
- apply fast+
- txt {* arity *}
- apply (auto elim!: equalityE simp add: inj_on_def)
- apply (subst Diff_insert0)
- apply auto
+ apply (auto elim!: equalityE simp add: inj_on_def)
+ apply (subst Diff_insert0, auto)
+ txt {* finiteness of the two sets *}
+ apply (rule_tac [2] B = "Pow (A)" in finite_subset)
+ apply (rule_tac B = "Pow (insert x A)" in finite_subset)
+ apply fast+
done
text {*
--- a/src/HOL/GroupTheory/Coset.thy Fri Sep 27 13:24:29 2002 +0200
+++ b/src/HOL/GroupTheory/Coset.thy Fri Sep 27 16:44:50 2002 +0200
@@ -193,7 +193,7 @@
lemma (in coset) l_repr_independence:
"[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> x <# H = y <# H"
-apply (auto simp add: l_coset_eq sum_assoc left_cancellation_iff
+apply (auto simp add: l_coset_eq sum_assoc
subgroup_imp_subset [THEN subsetD] subgroup_sum_closed)
apply (rule_tac x = "sum G (gminus G h) ha" in bexI)
--{*FIXME: locales don't currently work with @{text rule_tac},
@@ -229,7 +229,7 @@
assume "h \<in> H"
hence "((\<ominus>x) \<oplus> (\<ominus>h) \<oplus> x) \<oplus> \<ominus>x = \<ominus>(h \<oplus> x)"
by (simp add: xinG sum_assoc minus_sum H_subset [THEN subsetD])
- thus "\<exists>ha\<in>H. ha \<oplus> \<ominus>x = \<ominus>(h \<oplus> x)"
+ thus "\<exists>j\<in>H. j \<oplus> \<ominus>x = \<ominus>(h \<oplus> x)"
using prems
by (blast intro: normal_minus_op_closed1 normal_imp_subgroup
subgroup_minus_closed)
@@ -337,31 +337,36 @@
apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
done
+text{*The next two lemmas support the proof of @{text card_cosets_equal},
+since we can't use @{text rule_tac} with explicit terms for @{term f} and
+@{term g}.*}
+lemma (in coset) inj_on_f:
+ "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> \<ominus>a) (H #> a)"
+apply (rule inj_onI)
+apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
+ prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
+apply (rotate_tac -1)
+apply (simp add: subsetD)
+done
+
+lemma (in coset) inj_on_g:
+ "[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<oplus> a) H"
+by (force simp add: inj_on_def subsetD)
+
lemma (in coset) card_cosets_equal:
"[| c \<in> rcosets G H; H <= carrier G; finite(carrier G) |]
==> card c = card H"
apply (auto simp add: setrcos_eq)
-(*FIXME: I can't say
-apply (rule_tac f = "%y. y \<oplus> (\<ominus>a)" and g = "%y. y \<oplus> a" in card_bij_eq)
-*)
-apply (rule_tac f = "%y. sum G y (gminus G a)"
- and g = "%y. sum G y a" in card_bij_eq)
- apply (simp add: r_coset_subset_G [THEN finite_subset])
- apply (blast intro: finite_subset)
- txt{*inclusion in @{term H}*}
- apply (force simp add: sum_assoc subsetD r_coset_eq)
- defer 1
- txt{*inclusion in @{term "H #> a"}*}
- apply (blast intro: rcosI)
- apply (force simp add: inj_on_def right_cancellation_iff subsetD)
-apply (rule inj_onI)
-apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
- prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
-apply (rotate_tac -1)
-apply (simp add: right_cancellation_iff subsetD)
+apply (rule card_bij_eq)
+ apply (rule inj_on_f, assumption+)
+ apply (force simp add: sum_assoc subsetD r_coset_eq)
+ apply (rule inj_on_g, assumption+)
+ apply (force simp add: sum_assoc subsetD r_coset_eq)
+ txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
+ apply (simp add: r_coset_subset_G [THEN finite_subset])
+apply (blast intro: finite_subset)
done
-
subsection{*Two distinct right cosets are disjoint*}
lemma (in coset) rcos_equation:
--- a/src/HOL/GroupTheory/Sylow.thy Fri Sep 27 13:24:29 2002 +0200
+++ b/src/HOL/GroupTheory/Sylow.thy Fri Sep 27 16:44:50 2002 +0200
@@ -24,24 +24,22 @@
(\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
lemma (in sylow) RelM_refl: "refl calM RelM"
-apply (unfold refl_def RelM_def, auto)
-apply (simp add: calM_def)
-apply (rule bexI [of _ \<zero>])
-apply (auto simp add: zero_closed)
+apply (auto simp add: refl_def RelM_def calM_def)
+apply (blast intro!: coset_sum_zero [symmetric])
done
lemma (in sylow) RelM_sym: "sym RelM"
-apply (unfold sym_def RelM_def, auto)
-apply (rule_tac x = "gminus G g" in bexI)
-apply (erule_tac [2] minus_closed)
-apply (simp add: coset_sum_assoc calM_def)
-done
+proof (unfold sym_def RelM_def, clarify)
+ fix y g
+ assume "y \<in> calM"
+ and g: "g \<in> carrier G"
+ hence "y = y #> g #> (\<ominus>g)" by (simp add: coset_sum_assoc calM_def)
+ thus "\<exists>g'\<in>carrier G. y = y #> g #> g'"
+ by (blast intro: g minus_closed)
+qed
lemma (in sylow) RelM_trans: "trans RelM"
-apply (unfold trans_def RelM_def, auto)
-apply (rule_tac x = "sum G ga g" in bexI)
-apply (simp_all add: coset_sum_assoc calM_def)
-done
+by (auto simp add: trans_def RelM_def calM_def coset_sum_assoc)
lemma (in sylow) RelM_equiv: "equiv calM RelM"
apply (unfold equiv_def)
@@ -113,8 +111,7 @@
lemma (in sylow) zero_less_o_G: "0 < order(G)"
apply (unfold order_def)
-apply (cut_tac zero_closed)
-apply (blast intro: zero_less_card_empty)
+apply (blast intro: zero_closed zero_less_card_empty)
done
lemma (in sylow) zero_less_m: "0 < m"
--- a/src/HOL/Library/FuncSet.thy Fri Sep 27 13:24:29 2002 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Sep 27 16:44:50 2002 +0200
@@ -39,6 +39,7 @@
compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
"compose A g f == \<lambda>x\<in>A. g (f x)"
+print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
subsection{*Basic Properties of @{term Pi}*}
@@ -105,7 +106,6 @@
lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
by (simp add: Pi_def restrict_def)
-
lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
by (simp add: Pi_def restrict_def)