# HG changeset patch # User Andreas Lochbihler # Date 1338796257 -7200 # Node ID 02d64fd408529fc0936be0961b8d97840ad0c6ec # Parent 04aeda922be240dc3dc1e5a79c498c48fb3b074d more sort constraints for FinFun code generation diff -r 04aeda922be2 -r 02d64fd40852 src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Sun Jun 03 15:49:55 2012 +0200 +++ b/src/HOL/Library/Cardinality.thy Mon Jun 04 09:50:57 2012 +0200 @@ -170,9 +170,7 @@ subsection {* A type class for computing the cardinality of types *} definition is_list_UNIV :: "'a list \ bool" -where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)" - -lemmas [code_unfold] = is_list_UNIV_def[abs_def] +where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)" lemma is_list_UNIV_iff: "is_list_UNIV xs \ set xs = UNIV" by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] @@ -185,6 +183,11 @@ lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)" by(simp add: card_UNIV) +lemma is_list_UNIV_code [code]: + "is_list_UNIV (xs :: 'a list) = + (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)" +by(rule is_list_UNIV_def) + lemma finite_UNIV_conv_card_UNIV [code_unfold]: "finite (UNIV :: 'a :: card_UNIV set) \ card_UNIV TYPE('a) > 0" by(simp add: card_UNIV card_gt_0_iff) diff -r 04aeda922be2 -r 02d64fd40852 src/HOL/Library/FinFun.thy --- a/src/HOL/Library/FinFun.thy Sun Jun 03 15:49:55 2012 +0200 +++ b/src/HOL/Library/FinFun.thy Mon Jun 04 09:50:57 2012 +0200 @@ -435,7 +435,7 @@ by transfer (simp add: finfun_default_aux_update_const) lemma finfun_default_const_code [code]: - "finfun_default ((K$ c) :: 'a \f 'b) = (if CARD('a) = 0 then c else undefined)" + "finfun_default ((K$ c) :: 'a :: card_UNIV \f 'b) = (if CARD('a) = 0 then c else undefined)" by(simp add: finfun_default_const) lemma finfun_default_update_code [code]: