other UNIV lemmas
authorhaftmann
Tue Feb 26 20:38:18 2008 +0100 (2008-02-26)
changeset 26153b037fd9016fa
parent 26152 cf2cccf17d6d
child 26154 894f3860ebfd
other UNIV lemmas
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Feb 26 20:38:17 2008 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Tue Feb 26 20:38:18 2008 +0100
     1.3 @@ -63,26 +63,26 @@
     1.4  *}
     1.5  
     1.6  lemma card_unit: "CARD(unit) = 1"
     1.7 -  unfolding univ_unit by simp
     1.8 +  unfolding UNIV_unit by simp
     1.9  
    1.10  lemma card_bool: "CARD(bool) = 2"
    1.11 -  unfolding univ_bool by simp
    1.12 +  unfolding UNIV_bool by simp
    1.13  
    1.14  lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
    1.15 -  unfolding univ_prod by (simp only: card_cartesian_product)
    1.16 +  unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    1.17  
    1.18  lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
    1.19 -  unfolding univ_sum by (simp only: finite card_Plus)
    1.20 +  unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
    1.21  
    1.22  lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
    1.23 -  unfolding univ_option
    1.24 +  unfolding insert_None_conv_UNIV [symmetric]
    1.25    apply (subgoal_tac "(None::'a option) \<notin> range Some")
    1.26    apply (simp add: finite card_image)
    1.27    apply fast
    1.28    done
    1.29  
    1.30  lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
    1.31 -  unfolding univ_set
    1.32 +  unfolding Pow_UNIV [symmetric]
    1.33    by (simp only: card_Pow finite numeral_2_eq_2)
    1.34  
    1.35