# HG changeset patch
# User paulson
# Date 1033137890 -7200
# Node ID 7e6cdcd113a246aa752cff1427905bf96a6f60c9
# Parent  c2ee8f5a5652734cdf018d00aeee0b434fef92ae
Proof tidying

diff -r c2ee8f5a5652 -r 7e6cdcd113a2 src/HOL/Finite_Set.thy
--- 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 {*
diff -r c2ee8f5a5652 -r 7e6cdcd113a2 src/HOL/GroupTheory/Coset.thy
--- 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:
diff -r c2ee8f5a5652 -r 7e6cdcd113a2 src/HOL/GroupTheory/Sylow.thy
--- 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"
diff -r c2ee8f5a5652 -r 7e6cdcd113a2 src/HOL/Library/FuncSet.thy
--- 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)