# HG changeset patch
# User haftmann
# Date 1243952623 -7200
# Node ID f25536c0bb803c39e65804a3e5accfc805f4178b
# Parent  21329965657526e0705a0f53d44886d3a91de339
added/moved lemmas by Andreas Lochbihler

diff -r 213299656575 -r f25536c0bb80 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jun 02 15:53:34 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jun 02 16:23:43 2009 +0200
@@ -1926,34 +1926,40 @@
 But now that we have @{text setsum} things are easy:
 *}
 
-definition card :: "'a set \<Rightarrow> nat"
-where "card A = setsum (\<lambda>x. 1) A"
+definition card :: "'a set \<Rightarrow> nat" where
+  "card A = setsum (\<lambda>x. 1) A"
+
+lemmas card_eq_setsum = card_def
 
 lemma card_empty [simp]: "card {} = 0"
-by (simp add: card_def)
-
-lemma card_infinite [simp]: "~ finite A ==> card A = 0"
-by (simp add: card_def)
-
-lemma card_eq_setsum: "card A = setsum (%x. 1) A"
-by (simp add: card_def)
+  by (simp add: card_def)
 
 lemma card_insert_disjoint [simp]:
   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
-by(simp add: card_def)
+  by (simp add: card_def)
 
 lemma card_insert_if:
   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
-by (simp add: insert_absorb)
+  by (simp add: insert_absorb)
+
+lemma card_infinite [simp]: "~ finite A ==> card A = 0"
+  by (simp add: card_def)
+
+lemma card_ge_0_finite:
+  "card A > 0 \<Longrightarrow> finite A"
+  by (rule ccontr) simp
 
 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
-apply auto
-apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
-done
+  apply auto
+  apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
+  done
+
+lemma finite_UNIV_card_ge_0:
+  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
+  by (rule ccontr) simp
 
 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
-by auto
-
+  by auto
 
 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
@@ -2049,6 +2055,24 @@
        finite_subset [of _ "\<Union> (insert x F)"])
 done
 
+lemma card_eq_UNIV_imp_eq_UNIV:
+  assumes fin: "finite (UNIV :: 'a set)"
+  and card: "card A = card (UNIV :: 'a set)"
+  shows "A = (UNIV :: 'a set)"
+proof
+  show "A \<subseteq> UNIV" by simp
+  show "UNIV \<subseteq> A"
+  proof
+    fix x
+    show "x \<in> A"
+    proof (rule ccontr)
+      assume "x \<notin> A"
+      then have "A \<subset> UNIV" by auto
+      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
+      with card show False by simp
+    qed
+  qed
+qed
 
 text{*The form of a finite set of given cardinality*}
 
@@ -2078,6 +2102,17 @@
  apply(auto intro:ccontr)
 done
 
+lemma finite_fun_UNIVD2:
+  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
+  shows "finite (UNIV :: 'b set)"
+proof -
+  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
+    by(rule finite_imageI)
+  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
+    by(rule UNIV_eq_I) auto
+  ultimately show "finite (UNIV :: 'b set)" by simp
+qed
+
 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
 apply (cases "finite A")
 apply (erule finite_induct)
diff -r 213299656575 -r f25536c0bb80 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Tue Jun 02 15:53:34 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Tue Jun 02 16:23:43 2009 +0200
@@ -219,6 +219,25 @@
 apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
 done
 
+lemma finite_fun_UNIVD1:
+  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
+  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
+  shows "finite (UNIV :: 'a set)"
+proof -
+  from fin have finb: "finite (UNIV :: 'b set)" by (rule finite_fun_UNIVD2)
+  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
+    by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
+  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)" by auto
+  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by (auto simp add: card_Suc_eq)
+  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by (rule finite_imageI)
+  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
+  proof (rule UNIV_eq_I)
+    fix x :: 'a
+    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
+    thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
+  qed
+  ultimately show "finite (UNIV :: 'a set)" by simp
+qed
 
 subsection {*Inverse of a PI-function (restricted domain)*}
 
diff -r 213299656575 -r f25536c0bb80 src/HOL/Library/Fin_Fun.thy
--- a/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 15:53:34 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 16:23:43 2009 +0200
@@ -17,68 +17,12 @@
   For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
 *}
 
-subsection {* Auxiliary definitions and lemmas *}
-
-(*FIXME move these to Finite_Set.thy*)
-lemma card_ge_0_finite:
-  "card A > 0 \<Longrightarrow> finite A"
-by(rule ccontr, drule card_infinite, simp)
-
-lemma finite_UNIV_card_ge_0:
-  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
-by(rule ccontr) simp
-
-lemma card_eq_UNIV_imp_eq_UNIV:
-  assumes fin: "finite (UNIV :: 'a set)"
-  and card: "card A = card (UNIV :: 'a set)"
-  shows "A = (UNIV :: 'a set)"
-apply -
-  proof
-  show "A \<subseteq> UNIV" by simp
-  show "UNIV \<subseteq> A"
-  proof
-    fix x
-    show "x \<in> A"
-    proof(rule ccontr)
-      assume "x \<notin> A"
-      hence "A \<subset> UNIV" by auto
-      from psubset_card_mono[OF fin this] card show False by simp
-    qed
-  qed
-qed
-
-lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
-  shows "finite (UNIV :: 'b set)"
-proof -
-  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
-    by(rule finite_imageI)
-  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
-    by(rule UNIV_eq_I) auto
-  ultimately show "finite (UNIV :: 'b set)" by simp
-qed
-
-lemma finite_fun_UNIVD1: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
-  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
-  shows "finite (UNIV :: 'a set)"
-proof -
-  from fin have finb: "finite (UNIV :: 'b set)" by(rule finite_fun_UNIVD2)
-  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
-    by(cases "card (UNIV :: 'b set)")(auto simp add: card_eq_0_iff)
-  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - 2" by(auto)
-  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by(auto simp add: card_Suc_eq)
-  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by(rule finite_imageI)
-  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
-  proof(rule UNIV_eq_I)
-    fix x :: 'a
-    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by(simp add: inv_def)
-    thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
-  qed
-  ultimately show "finite (UNIV :: 'a set)" by simp
-qed
-
 (*FIXME move to Map.thy*)
 lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-by(auto simp add: restrict_map_def intro: ext)
+  by (auto simp add: restrict_map_def intro: ext)
+
+
+subsection {* The @{text "map_default"} operation *}
 
 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
diff -r 213299656575 -r f25536c0bb80 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Jun 02 15:53:34 2009 +0200
+++ b/src/HOL/Map.thy	Tue Jun 02 16:23:43 2009 +0200
@@ -332,6 +332,9 @@
 lemma restrict_map_to_empty [simp]: "m|`{} = empty"
 by (simp add: restrict_map_def)
 
+lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
+by (auto simp add: restrict_map_def intro: ext)
+
 lemma restrict_map_empty [simp]: "empty|`D = empty"
 by (simp add: restrict_map_def)