move lemmas from Numeral_Type.thy to other theories
authorhuffman
Tue Dec 09 15:31:38 2008 -0800 (2008-12-09)
changeset 290258c8859c0d734
parent 29024 6cfa380af73b
child 29027 501780b0bcae
child 29037 208fee4049a0
move lemmas from Numeral_Type.thy to other theories
src/HOL/Datatype.thy
src/HOL/Finite_Set.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Datatype.thy	Tue Dec 09 12:53:25 2008 -0800
     1.2 +++ b/src/HOL/Datatype.thy	Tue Dec 09 15:31:38 2008 -0800
     1.3 @@ -605,6 +605,9 @@
     1.4  lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
     1.5    by (rule set_ext, case_tac x) auto
     1.6  
     1.7 +lemma inj_Some [simp]: "inj_on Some A"
     1.8 +  by (rule inj_onI) simp
     1.9 +
    1.10  
    1.11  subsubsection {* Operations *}
    1.12  
     2.1 --- a/src/HOL/Finite_Set.thy	Tue Dec 09 12:53:25 2008 -0800
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Dec 09 15:31:38 2008 -0800
     2.3 @@ -1828,6 +1828,18 @@
     2.4  by (simp add: card_cartesian_product)
     2.5  
     2.6  
     2.7 +subsubsection {* Cardinality of sums *}
     2.8 +
     2.9 +lemma card_Plus:
    2.10 +  assumes "finite A" and "finite B"
    2.11 +  shows "card (A <+> B) = card A + card B"
    2.12 +proof -
    2.13 +  have "Inl`A \<inter> Inr`B = {}" by fast
    2.14 +  with assms show ?thesis
    2.15 +    unfolding Plus_def
    2.16 +    by (simp add: card_Un_disjoint card_image)
    2.17 +qed
    2.18 +
    2.19  
    2.20  subsubsection {* Cardinality of the Powerset *}
    2.21  
     3.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Dec 09 12:53:25 2008 -0800
     3.2 +++ b/src/HOL/Library/Numeral_Type.thy	Tue Dec 09 15:31:38 2008 -0800
     3.3 @@ -14,23 +14,6 @@
     3.4  subsection {* Preliminary lemmas *}
     3.5  (* These should be moved elsewhere *)
     3.6  
     3.7 -lemma inj_Inl [simp]: "inj_on Inl A"
     3.8 -  by (rule inj_onI, simp)
     3.9 -
    3.10 -lemma inj_Inr [simp]: "inj_on Inr A"
    3.11 -  by (rule inj_onI, simp)
    3.12 -
    3.13 -lemma inj_Some [simp]: "inj_on Some A"
    3.14 -  by (rule inj_onI, simp)
    3.15 -
    3.16 -lemma card_Plus:
    3.17 -  "[| finite A; finite B |] ==> card (A <+> B) = card A + card B"
    3.18 -  unfolding Plus_def
    3.19 -  apply (subgoal_tac "Inl ` A \<inter> Inr ` B = {}")
    3.20 -  apply (simp add: card_Un_disjoint card_image)
    3.21 -  apply fast
    3.22 -  done
    3.23 -
    3.24  lemma (in type_definition) univ:
    3.25    "UNIV = Abs ` A"
    3.26  proof
     4.1 --- a/src/HOL/Sum_Type.thy	Tue Dec 09 12:53:25 2008 -0800
     4.2 +++ b/src/HOL/Sum_Type.thy	Tue Dec 09 15:31:38 2008 -0800
     4.3 @@ -93,16 +93,17 @@
     4.4  lemma Inr_Rep_inject: "Inr_Rep(b) = Inr_Rep(d) ==> b=d"
     4.5  by (auto simp add: Inr_Rep_def expand_fun_eq)
     4.6  
     4.7 -lemma inj_Inl: "inj(Inl)"
     4.8 +lemma inj_Inl [simp]: "inj_on Inl A"
     4.9  apply (simp add: Inl_def)
    4.10  apply (rule inj_onI)
    4.11  apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inl_Rep_inject])
    4.12  apply (rule Inl_RepI)
    4.13  apply (rule Inl_RepI)
    4.14  done
    4.15 +
    4.16  lemmas Inl_inject = inj_Inl [THEN injD, standard]
    4.17  
    4.18 -lemma inj_Inr: "inj(Inr)"
    4.19 +lemma inj_Inr [simp]: "inj_on Inr A"
    4.20  apply (simp add: Inr_def)
    4.21  apply (rule inj_onI)
    4.22  apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inr_Rep_inject])