--- a/src/HOL/Finite_Set.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Finite_Set.thy Sat May 09 07:25:22 2009 +0200
@@ -365,6 +365,29 @@
lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
by (simp add: Plus_def)
+lemma finite_PlusD:
+ fixes A :: "'a set" and B :: "'b set"
+ assumes fin: "finite (A <+> B)"
+ shows "finite A" "finite B"
+proof -
+ have "Inl ` A \<subseteq> A <+> B" by auto
+ hence "finite (Inl ` A :: ('a + 'b) set)" using fin by(rule finite_subset)
+ thus "finite A" by(rule finite_imageD)(auto intro: inj_onI)
+next
+ have "Inr ` B \<subseteq> A <+> B" by auto
+ hence "finite (Inr ` B :: ('a + 'b) set)" using fin by(rule finite_subset)
+ thus "finite B" by(rule finite_imageD)(auto intro: inj_onI)
+qed
+
+lemma finite_Plus_iff[simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
+by(auto intro: finite_PlusD finite_Plus)
+
+lemma finite_Plus_UNIV_iff[simp]:
+ "finite (UNIV :: ('a + 'b) set) =
+ (finite (UNIV :: 'a set) & finite (UNIV :: 'b set))"
+by(subst UNIV_Plus_UNIV[symmetric])(rule finite_Plus_iff)
+
+
text {* Sigma of finite sets *}
lemma finite_SigmaI [simp]:
@@ -1563,6 +1586,20 @@
qed
+lemma setsum_Plus:
+ fixes A :: "'a set" and B :: "'b set"
+ assumes fin: "finite A" "finite B"
+ shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
+proof -
+ have "A <+> B = Inl ` A \<union> Inr ` B" by auto
+ moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
+ by(auto intro: finite_imageI)
+ moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
+ moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
+ ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
+qed
+
+
text {* Commuting outer and inner summation *}
lemma swap_inj_on:
@@ -2091,6 +2128,10 @@
qed
+lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
+ unfolding UNIV_unit by simp
+
+
subsubsection {* Cardinality of unions *}
lemma card_UN_disjoint:
@@ -2201,6 +2242,10 @@
by (simp add: card_Un_disjoint card_image)
qed
+lemma card_Plus_conv_if:
+ "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)"
+by(auto simp: card_def setsum_Plus simp del: setsum_constant)
+
subsubsection {* Cardinality of the Powerset *}
--- a/src/HOL/Fun.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Fun.thy Sat May 09 07:25:22 2009 +0200
@@ -412,6 +412,9 @@
"f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
by auto
+lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
+by(auto intro: ext)
+
subsection {* @{text override_on} *}
--- a/src/HOL/Library/Numeral_Type.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Sat May 09 07:25:22 2009 +0200
@@ -55,7 +55,7 @@
unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
- unfolding insert_None_conv_UNIV [symmetric]
+ unfolding UNIV_option_conv
apply (subgoal_tac "(None::'a option) \<notin> range Some")
apply (simp add: card_image)
apply fast
--- a/src/HOL/List.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/List.thy Sat May 09 07:25:22 2009 +0200
@@ -1347,8 +1347,7 @@
by (induct xs, auto)
lemma update_zip:
- "length xs = length ys ==>
- (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
+ "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
@@ -1829,6 +1828,10 @@
apply simp_all
done
+text{* Courtesy of Andreas Lochbihler: *}
+lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
+by(induct xs) auto
+
lemma nth_zip [simp]:
"[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
apply (induct ys arbitrary: i xs, simp)
@@ -1838,11 +1841,11 @@
lemma set_zip:
"set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
-by (simp add: set_conv_nth cong: rev_conj_cong)
+by(simp add: set_conv_nth cong: rev_conj_cong)
lemma zip_update:
-"length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
-by (rule sym, simp add: update_zip)
+ "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
+by(rule sym, simp add: update_zip)
lemma zip_replicate [simp]:
"zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
@@ -2577,6 +2580,11 @@
apply (simp add: add_commute)
done
+text{* Courtesy of Andreas Lochbihler: *}
+lemma filter_replicate:
+ "filter P (replicate n x) = (if P x then replicate n x else [])"
+by(induct n) auto
+
lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
by (induct n) auto
--- a/src/HOL/Map.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Map.thy Sat May 09 07:25:22 2009 +0200
@@ -452,6 +452,9 @@
subsection {* @{term [source] dom} *}
+lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
+by(auto intro!:ext simp: dom_def)
+
lemma domI: "m a = Some b ==> a : dom m"
by(simp add:dom_def)
(* declare domI [intro]? *)
@@ -593,4 +596,19 @@
lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)
+
+lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
+proof(rule iffI)
+ assume "\<exists>v. f = [x \<mapsto> v]"
+ thus "dom f = {x}" by(auto split: split_if_asm)
+next
+ assume "dom f = {x}"
+ then obtain v where "f x = Some v" by auto
+ hence "[x \<mapsto> v] \<subseteq>\<^sub>m f" by(auto simp add: map_le_def)
+ moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using `dom f = {x}` `f x = Some v`
+ by(auto simp add: map_le_def)
+ ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym)
+ thus "\<exists>v. f = [x \<mapsto> v]" by blast
+qed
+
end
--- a/src/HOL/Nat_Numeral.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Sat May 09 07:25:22 2009 +0200
@@ -982,6 +982,9 @@
subsubsection{*Various Other Lemmas*}
+lemma card_UNIV_bool[simp]: "card (UNIV :: bool set) = 2"
+by(simp add: UNIV_bool)
+
text {*Evens and Odds, for Mutilated Chess Board*}
text{*Lemmas for specialist use, NOT as default simprules*}
--- a/src/HOL/Option.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Option.thy Sat May 09 07:25:22 2009 +0200
@@ -20,6 +20,9 @@
only when applied to assumptions, in practice it seems better to give
them the uniform iff attribute. *}
+lemma inj_Some [simp]: "inj_on Some A"
+by (rule inj_onI) simp
+
lemma option_caseE:
assumes c: "(case x of None => P | Some y => Q y)"
obtains
@@ -27,14 +30,15 @@
| (Some) y where "x = Some y" and "Q y"
using c by (cases x) simp_all
-lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
- by (rule set_ext, case_tac x) auto
+lemma UNIV_option_conv: "UNIV = insert None (range Some)"
+by(auto intro: classical)
+
+lemma finite_option_UNIV[simp]:
+ "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
+by(auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
instance option :: (finite) finite proof
-qed (simp add: insert_None_conv_UNIV [symmetric])
-
-lemma inj_Some [simp]: "inj_on Some A"
- by (rule inj_onI) simp
+qed (simp add: UNIV_option_conv)
subsubsection {* Operations *}
--- a/src/HOL/Sum_Type.thy Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Sum_Type.thy Sat May 09 07:25:22 2009 +0200
@@ -157,6 +157,8 @@
apply auto
done
+lemma Plus_eq_empty_conv[simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
+by(auto)
subsection{*The @{term Part} Primitive*}