src/HOL/Finite_Set.thy
 changeset 14661 9ead82084de8 parent 14565 c6dc17aab88a child 14738 83f1a514dcb4
```--- 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 @@
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,
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"

@@ -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)"