more sort constraints for FinFun code generation
authorAndreas Lochbihler
Mon Jun 04 09:50:57 2012 +0200 (2012-06-04)
changeset 4807002d64fd40852
parent 48068 04aeda922be2
child 48071 d7864276bca8
more sort constraints for FinFun code generation
src/HOL/Library/Cardinality.thy
src/HOL/Library/FinFun.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Sun Jun 03 15:49:55 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Mon Jun 04 09:50:57 2012 +0200
     1.3 @@ -170,9 +170,7 @@
     1.4  subsection {* A type class for computing the cardinality of types *}
     1.5  
     1.6  definition is_list_UNIV :: "'a list \<Rightarrow> bool"
     1.7 -where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
     1.8 -
     1.9 -lemmas [code_unfold] = is_list_UNIV_def[abs_def]
    1.10 +where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
    1.11  
    1.12  lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    1.13  by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
    1.14 @@ -185,6 +183,11 @@
    1.15  lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)"
    1.16  by(simp add: card_UNIV)
    1.17  
    1.18 +lemma is_list_UNIV_code [code]:
    1.19 +  "is_list_UNIV (xs :: 'a list) = 
    1.20 +  (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
    1.21 +by(rule is_list_UNIV_def)
    1.22 +
    1.23  lemma finite_UNIV_conv_card_UNIV [code_unfold]:
    1.24    "finite (UNIV :: 'a :: card_UNIV set) \<longleftrightarrow> card_UNIV TYPE('a) > 0"
    1.25  by(simp add: card_UNIV card_gt_0_iff)
     2.1 --- a/src/HOL/Library/FinFun.thy	Sun Jun 03 15:49:55 2012 +0200
     2.2 +++ b/src/HOL/Library/FinFun.thy	Mon Jun 04 09:50:57 2012 +0200
     2.3 @@ -435,7 +435,7 @@
     2.4  by transfer (simp add: finfun_default_aux_update_const)
     2.5  
     2.6  lemma finfun_default_const_code [code]:
     2.7 -  "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
     2.8 +  "finfun_default ((K$ c) :: 'a :: card_UNIV \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
     2.9  by(simp add: finfun_default_const)
    2.10  
    2.11  lemma finfun_default_update_code [code]: