src/HOL/Library/Numeral_Type.thy
changeset 29025 8c8859c0d734
parent 28920 4ed4b8b1988d
child 29629 5111ce425e7a
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Dec 09 12:53:25 2008 -0800
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Tue Dec 09 15:31:38 2008 -0800
     1.3 @@ -14,23 +14,6 @@
     1.4  subsection {* Preliminary lemmas *}
     1.5  (* These should be moved elsewhere *)
     1.6  
     1.7 -lemma inj_Inl [simp]: "inj_on Inl A"
     1.8 -  by (rule inj_onI, simp)
     1.9 -
    1.10 -lemma inj_Inr [simp]: "inj_on Inr A"
    1.11 -  by (rule inj_onI, simp)
    1.12 -
    1.13 -lemma inj_Some [simp]: "inj_on Some A"
    1.14 -  by (rule inj_onI, simp)
    1.15 -
    1.16 -lemma card_Plus:
    1.17 -  "[| finite A; finite B |] ==> card (A <+> B) = card A + card B"
    1.18 -  unfolding Plus_def
    1.19 -  apply (subgoal_tac "Inl ` A \<inter> Inr ` B = {}")
    1.20 -  apply (simp add: card_Un_disjoint card_image)
    1.21 -  apply fast
    1.22 -  done
    1.23 -
    1.24  lemma (in type_definition) univ:
    1.25    "UNIV = Abs ` A"
    1.26  proof