--- a/src/HOL/Datatype.thy Tue Dec 09 12:53:25 2008 -0800
+++ b/src/HOL/Datatype.thy Tue Dec 09 15:31:38 2008 -0800
@@ -605,6 +605,9 @@
lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
by (rule set_ext, case_tac x) auto
+lemma inj_Some [simp]: "inj_on Some A"
+ by (rule inj_onI) simp
+
subsubsection {* Operations *}
--- a/src/HOL/Finite_Set.thy Tue Dec 09 12:53:25 2008 -0800
+++ b/src/HOL/Finite_Set.thy Tue Dec 09 15:31:38 2008 -0800
@@ -1828,6 +1828,18 @@
by (simp add: card_cartesian_product)
+subsubsection {* Cardinality of sums *}
+
+lemma card_Plus:
+ assumes "finite A" and "finite B"
+ shows "card (A <+> B) = card A + card B"
+proof -
+ have "Inl`A \<inter> Inr`B = {}" by fast
+ with assms show ?thesis
+ unfolding Plus_def
+ by (simp add: card_Un_disjoint card_image)
+qed
+
subsubsection {* Cardinality of the Powerset *}
--- a/src/HOL/Library/Numeral_Type.thy Tue Dec 09 12:53:25 2008 -0800
+++ b/src/HOL/Library/Numeral_Type.thy Tue Dec 09 15:31:38 2008 -0800
@@ -14,23 +14,6 @@
subsection {* Preliminary lemmas *}
(* These should be moved elsewhere *)
-lemma inj_Inl [simp]: "inj_on Inl A"
- by (rule inj_onI, simp)
-
-lemma inj_Inr [simp]: "inj_on Inr A"
- by (rule inj_onI, simp)
-
-lemma inj_Some [simp]: "inj_on Some A"
- by (rule inj_onI, simp)
-
-lemma card_Plus:
- "[| finite A; finite B |] ==> card (A <+> B) = card A + card B"
- unfolding Plus_def
- apply (subgoal_tac "Inl ` A \<inter> Inr ` B = {}")
- apply (simp add: card_Un_disjoint card_image)
- apply fast
- done
-
lemma (in type_definition) univ:
"UNIV = Abs ` A"
proof
--- a/src/HOL/Sum_Type.thy Tue Dec 09 12:53:25 2008 -0800
+++ b/src/HOL/Sum_Type.thy Tue Dec 09 15:31:38 2008 -0800
@@ -93,16 +93,17 @@
lemma Inr_Rep_inject: "Inr_Rep(b) = Inr_Rep(d) ==> b=d"
by (auto simp add: Inr_Rep_def expand_fun_eq)
-lemma inj_Inl: "inj(Inl)"
+lemma inj_Inl [simp]: "inj_on Inl A"
apply (simp add: Inl_def)
apply (rule inj_onI)
apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inl_Rep_inject])
apply (rule Inl_RepI)
apply (rule Inl_RepI)
done
+
lemmas Inl_inject = inj_Inl [THEN injD, standard]
-lemma inj_Inr: "inj(Inr)"
+lemma inj_Inr [simp]: "inj_on Inr A"
apply (simp add: Inr_def)
apply (rule inj_onI)
apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inr_Rep_inject])