# HG changeset patch
# User wenzelm
# Date 1082746108 -7200
# Node ID 9ead82084de823448a0a22099b6d18da0709196a
# Parent  934e03881ad6d70aa0d5cb01d879c25b2dbfefab
tuned notation;

diff -r 934e03881ad6 -r 9ead82084de8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Apr 23 20:47:48 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Apr 23 20:48:28 2004 +0200
@@ -26,9 +26,12 @@
   finite: "finite UNIV"
 
 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
- "[| ~finite(UNIV::'a set); finite A  |] ==> \<exists>a::'a. a \<notin> A"
-by(subgoal_tac "A \<noteq> UNIV", blast, blast)
-
+  assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
+  shows "\<exists>a::'a. a \<notin> A"
+proof -
+  from prems have "A \<noteq> UNIV" by blast
+  thus ?thesis by blast
+qed
 
 lemma finite_induct [case_names empty insert, induct set: Finites]:
   "finite F ==>
@@ -730,7 +733,7 @@
       by (simp add: AC)
     also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
       by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
-	auto simp add: left_commute)
+        auto simp add: left_commute)
     finally show ?case .
   qed
 qed
@@ -743,11 +746,11 @@
   "setsum f A == if finite A then fold (op + o f) 0 A else 0"
 
 syntax
-  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
+  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("(3\<Sum>_:_. _)" [0, 51, 10] 10)
 syntax (xsymbols)
-  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
+  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
 syntax (HTML output)
-  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
+  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
 translations
   "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
 
@@ -775,7 +778,7 @@
     setsum f B = setsum id (f ` B)"
 by (auto simp add: setsum_reindex id_o)
 
-lemma setsum_reindex_cong: "finite A ==> inj_on f A ==> 
+lemma setsum_reindex_cong: "finite A ==> inj_on f A ==>
     B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
   by (frule setsum_reindex, assumption, simp)
 
@@ -845,15 +848,15 @@
   apply (unfold Union_def id_def, assumption+)
   done
 
-lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
-    (\<Sum> x:A. (\<Sum> y:B x. f x y)) = 
-    (\<Sum> z:(SIGMA x:A. B x). f (fst z) (snd z))"
+lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
+    (\<Sum>x:A. (\<Sum>y:B x. f x y)) =
+    (\<Sum>z:(SIGMA x:A. B x). f (fst z) (snd z))"
   apply (subst Sigma_def)
   apply (subst setsum_UN_disjoint)
   apply assumption
   apply (rule ballI)
   apply (drule_tac x = i in bspec, assumption)
-  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
+  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
   apply (rule finite_surj)
   apply auto
   apply (rule setsum_cong, rule refl)
@@ -863,8 +866,8 @@
   done
 
 lemma setsum_cartesian_product: "finite A ==> finite B ==>
-    (\<Sum> x:A. (\<Sum> y:B. f x y)) = 
-    (\<Sum> z:A <*> B. f (fst z) (snd z))"
+    (\<Sum>x:A. (\<Sum>y:B. f x y)) =
+    (\<Sum>z:A <*> B. f (fst z) (snd z))"
   by (erule setsum_Sigma, auto);
 
 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
@@ -984,19 +987,15 @@
   "setprod f A == if finite A then fold (op * o f) 1 A else 1"
 
 syntax
-  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
-                ("\<Prod>_:_. _" [0, 51, 10] 10)
+  "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
 
 syntax (xsymbols)
-  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
-                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+  "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
 syntax (HTML output)
-  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
-                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+  "_setprod" :: "idt => 'a set => 'b => 'b::times_ac1"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
 translations
   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
 
-
 lemma setprod_empty [simp]: "setprod f {} = 1"
   by (auto simp add: setprod_def)
 
@@ -1020,7 +1019,7 @@
     setprod f B = setprod id (f ` B)"
 by (auto simp add: setprod_reindex id_o)
 
-lemma setprod_reindex_cong: "finite A ==> inj_on f A ==> 
+lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
   by (frule setprod_reindex, assumption, simp)
 
@@ -1086,15 +1085,15 @@
   apply (unfold Union_def id_def, assumption+)
   done
 
-lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
-    (\<Prod> x:A. (\<Prod> y: B x. f x y)) = 
-    (\<Prod> z:(SIGMA x:A. B x). f (fst z) (snd z))"
+lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
+    (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
+    (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
   apply (subst Sigma_def)
   apply (subst setprod_UN_disjoint)
   apply assumption
   apply (rule ballI)
   apply (drule_tac x = i in bspec, assumption)
-  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)") 
+  apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
   apply (rule finite_surj)
   apply auto
   apply (rule setprod_cong, rule refl)
@@ -1103,9 +1102,9 @@
   apply auto
   done
 
-lemma setprod_cartesian_product: "finite A ==> finite B ==> 
-    (\<Prod> x:A. (\<Prod> y: B. f x y)) = 
-    (\<Prod> z:(A <*> B). f (fst z) (snd z))"
+lemma setprod_cartesian_product: "finite A ==> finite B ==>
+    (\<Prod>x:A. (\<Prod>y: B. f x y)) =
+    (\<Prod>z:(A <*> B). f (fst z) (snd z))"
   by (erule setprod_Sigma, auto)
 
 lemma setprod_timesf: "setprod (%x. f x * g x) A =
@@ -1238,7 +1237,7 @@
       assume "x \<le> m" thus ?thesis using m by blast
     next
       assume "~ x \<le> m" thus ?thesis using m
-	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
+        by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
     qed
   qed
 qed
@@ -1261,47 +1260,50 @@
       assume "m \<le> x" thus ?thesis using m by blast
     next
       assume "~ m \<le> x" thus ?thesis using m
-	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
+        by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
     qed
   qed
 qed
 
 constdefs
- Min :: "('a::linorder)set => 'a"
-"Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
+  Min :: "('a::linorder)set => 'a"
+  "Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
 
- Max :: "('a::linorder)set => 'a"
-"Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
+  Max :: "('a::linorder)set => 'a"
+  "Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
 
-lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
-                 shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
+lemma Min [simp]:
+  assumes a: "finite S"  "S \<noteq> {}"
+  shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
 proof (unfold Min_def, rule theI')
   show "\<exists>!m. ?P m"
   proof (rule ex_ex1I)
     show "\<exists>m. ?P m" using ex_Min[OF a] by blast
   next
-    fix m1 m2 assume "?P m1" "?P m2"
-    thus "m1 = m2" by (blast dest:order_antisym)
+    fix m1 m2 assume "?P m1" and "?P m2"
+    thus "m1 = m2" by (blast dest: order_antisym)
   qed
 qed
 
-lemma Max[simp]: assumes a: "finite S" "S \<noteq> {}"
-                 shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
+lemma Max [simp]:
+  assumes a: "finite S"  "S \<noteq> {}"
+  shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
 proof (unfold Max_def, rule theI')
   show "\<exists>!m. ?P m"
   proof (rule ex_ex1I)
     show "\<exists>m. ?P m" using ex_Max[OF a] by blast
   next
     fix m1 m2 assume "?P m1" "?P m2"
-    thus "m1 = m2" by (blast dest:order_antisym)
+    thus "m1 = m2" by (blast dest: order_antisym)
   qed
 qed
 
+
 subsection {* Theorems about @{text "choose"} *}
 
 text {*
   \medskip Basic theorem about @{text "choose"}.  By Florian
-  Kammüller, tidied by LCP.
+  Kamm\"uller, tidied by LCP.
 *}
 
 lemma card_s_0_eq_empty:
@@ -1370,5 +1372,4 @@
     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   by (simp add: n_sub_lemma)
 
-
 end