# HG changeset patch
# User huffman
# Date 1228865498 28800
# Node ID 8c8859c0d7349f8137f4054e863bdc6015574bc8
# Parent  6cfa380af73b0b5d611b2eacd7e94a05361395ee
move lemmas from Numeral_Type.thy to other theories

diff -r 6cfa380af73b -r 8c8859c0d734 src/HOL/Datatype.thy
--- 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 *}
 
diff -r 6cfa380af73b -r 8c8859c0d734 src/HOL/Finite_Set.thy
--- 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 *}
 
diff -r 6cfa380af73b -r 8c8859c0d734 src/HOL/Library/Numeral_Type.thy
--- 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
diff -r 6cfa380af73b -r 8c8859c0d734 src/HOL/Sum_Type.thy
--- 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])