src/HOL/Library/FinFun.thy
changeset 48059 f6ce99d3719b
parent 48051 53a0df441e20
child 48070 02d64fd40852
     1.1 --- a/src/HOL/Library/FinFun.thy	Fri Jun 01 13:52:51 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Fri Jun 01 14:34:46 2012 +0200
     1.3 @@ -435,8 +435,8 @@
     1.4  by transfer (simp add: finfun_default_aux_update_const)
     1.5  
     1.6  lemma finfun_default_const_code [code]:
     1.7 -  "finfun_default ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
     1.8 -by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
     1.9 +  "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
    1.10 +by(simp add: finfun_default_const)
    1.11  
    1.12  lemma finfun_default_update_code [code]:
    1.13    "finfun_default (finfun_update_code f a b) = finfun_default f"
    1.14 @@ -1285,9 +1285,8 @@
    1.15  
    1.16  lemma finfun_dom_const_code [code]:
    1.17    "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
    1.18 -   (if card_UNIV (TYPE('a)) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
    1.19 -unfolding card_UNIV_eq_0_infinite_UNIV
    1.20 -by(simp add: finfun_dom_const)
    1.21 +   (if CARD('a) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
    1.22 +by(simp add: finfun_dom_const card_UNIV card_eq_0_iff)
    1.23  
    1.24  lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
    1.25  using finite_finfun_default[of f]
    1.26 @@ -1349,9 +1348,8 @@
    1.27  
    1.28  lemma finfun_to_list_const_code [code]:
    1.29    "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
    1.30 -   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
    1.31 -unfolding card_UNIV_eq_0_infinite_UNIV
    1.32 -by(auto simp add: finfun_to_list_const)
    1.33 +   (if CARD('a) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
    1.34 +by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff)
    1.35  
    1.36  lemma remove1_insort_insert_same:
    1.37    "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"