author paulson Fri, 27 Sep 2002 16:44:50 +0200 changeset 13595 7e6cdcd113a2 parent 13594 c2ee8f5a5652 child 13596 ee5f79b210c1
Proof tidying
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/GroupTheory/Coset.thy file | annotate | diff | comparison | revisions src/HOL/GroupTheory/Sylow.thy file | annotate | diff | comparison | revisions src/HOL/Library/FuncSet.thy file | annotate | diff | comparison | revisions
```--- 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)
+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"
-(*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 (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 (rule bexI [of _ \<zero>])
+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)
-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)
-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"