change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
authorAndreas Lochbihler
Thu Jun 28 09:16:00 2012 +0200 (2012-06-28)
changeset 48164e97369f20c30
parent 48163 f0ecc1550998
child 48165 d07a0b9601aa
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
src/HOL/Library/Cardinality.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Thu Jun 28 09:14:57 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Thu Jun 28 09:16:00 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Cardinality of types *}
     1.5  
     1.6  theory Cardinality
     1.7 -imports "~~/src/HOL/Main"
     1.8 +imports Phantom_Type
     1.9  begin
    1.10  
    1.11  subsection {* Preliminary lemmas *}
    1.12 @@ -176,11 +176,14 @@
    1.13  by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
    1.14     dest: subst[where P="finite", OF _ finite_set] card_eq_UNIV_imp_eq_UNIV)
    1.15  
    1.16 +type_synonym 'a card_UNIV = "('a, nat) phantom"
    1.17 +
    1.18  class card_UNIV = 
    1.19 -  fixes card_UNIV :: "'a itself \<Rightarrow> nat"
    1.20 -  assumes card_UNIV: "card_UNIV x = CARD('a)"
    1.21 +  fixes card_UNIV :: "'a card_UNIV"
    1.22 +  assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
    1.23  
    1.24 -lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)"
    1.25 +lemma card_UNIV_code [code_unfold]: 
    1.26 +  "CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)"
    1.27  by(simp add: card_UNIV)
    1.28  
    1.29  lemma is_list_UNIV_code [code]:
    1.30 @@ -189,74 +192,78 @@
    1.31  by(rule is_list_UNIV_def)
    1.32  
    1.33  lemma finite_UNIV_conv_card_UNIV [code_unfold]:
    1.34 -  "finite (UNIV :: 'a :: card_UNIV set) \<longleftrightarrow> card_UNIV TYPE('a) > 0"
    1.35 +  "finite (UNIV :: 'a :: card_UNIV set) \<longleftrightarrow> 
    1.36 +  of_phantom (card_UNIV :: 'a card_UNIV) > 0"
    1.37  by(simp add: card_UNIV card_gt_0_iff)
    1.38  
    1.39  subsection {* Instantiations for @{text "card_UNIV"} *}
    1.40  
    1.41  instantiation nat :: card_UNIV begin
    1.42 -definition "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
    1.43 +definition "card_UNIV = Phantom(nat) 0"
    1.44  instance by intro_classes (simp add: card_UNIV_nat_def)
    1.45  end
    1.46  
    1.47  instantiation int :: card_UNIV begin
    1.48 -definition "card_UNIV = (\<lambda>a :: int itself. 0)"
    1.49 +definition "card_UNIV = Phantom(int) 0"
    1.50  instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
    1.51  end
    1.52  
    1.53  instantiation list :: (type) card_UNIV begin
    1.54 -definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
    1.55 +definition "card_UNIV = Phantom('a list) 0"
    1.56  instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
    1.57  end
    1.58  
    1.59  instantiation unit :: card_UNIV begin
    1.60 -definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
    1.61 +definition "card_UNIV = Phantom(unit) 1"
    1.62  instance by intro_classes (simp add: card_UNIV_unit_def card_UNIV_unit)
    1.63  end
    1.64  
    1.65  instantiation bool :: card_UNIV begin
    1.66 -definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
    1.67 +definition "card_UNIV = Phantom(bool) 2"
    1.68  instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
    1.69  end
    1.70  
    1.71  instantiation char :: card_UNIV begin
    1.72 -definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
    1.73 +definition "card_UNIV = Phantom(char) 256"
    1.74  instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)
    1.75  end
    1.76  
    1.77  instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
    1.78 -definition "card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
    1.79 +definition "card_UNIV = 
    1.80 +  Phantom('a \<times> 'b) (of_phantom (card_UNIV :: 'a card_UNIV) * of_phantom (card_UNIV :: 'b card_UNIV))"
    1.81  instance by intro_classes (simp add: card_UNIV_prod_def card_UNIV)
    1.82  end
    1.83  
    1.84  instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
    1.85 -definition "card_UNIV = (\<lambda>a :: ('a + 'b) itself. 
    1.86 -  let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
    1.87 -  in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
    1.88 +definition "card_UNIV = Phantom('a + 'b)
    1.89 +  (let ca = of_phantom (card_UNIV :: 'a card_UNIV); 
    1.90 +       cb = of_phantom (card_UNIV :: 'b card_UNIV)
    1.91 +   in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
    1.92  instance by intro_classes (auto simp add: card_UNIV_sum_def card_UNIV card_UNIV_sum)
    1.93  end
    1.94  
    1.95  instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
    1.96 -definition "card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. 
    1.97 -  let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
    1.98 -  in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
    1.99 +definition "card_UNIV = Phantom('a \<Rightarrow> 'b)
   1.100 +  (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
   1.101 +       cb = of_phantom (card_UNIV :: 'b card_UNIV)
   1.102 +   in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
   1.103  instance by intro_classes (simp add: card_UNIV_fun_def card_UNIV Let_def card_fun)
   1.104  end
   1.105  
   1.106  instantiation option :: (card_UNIV) card_UNIV begin
   1.107 -definition "card_UNIV = (\<lambda>a :: 'a option itself. 
   1.108 -  let c = card_UNIV (TYPE('a)) in if c \<noteq> 0 then Suc c else 0)"
   1.109 +definition "card_UNIV = Phantom('a option)
   1.110 +  (let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c \<noteq> 0 then Suc c else 0)"
   1.111  instance by intro_classes (simp add: card_UNIV_option_def card_UNIV card_UNIV_option)
   1.112  end
   1.113  
   1.114  instantiation String.literal :: card_UNIV begin
   1.115 -definition "card_UNIV = (\<lambda>a :: String.literal itself. 0)"
   1.116 +definition "card_UNIV = Phantom(String.literal) 0"
   1.117  instance by intro_classes (simp add: card_UNIV_literal_def card_literal)
   1.118  end
   1.119  
   1.120  instantiation set :: (card_UNIV) card_UNIV begin
   1.121 -definition "card_UNIV = (\<lambda>a :: 'a set itself.
   1.122 -  let c = card_UNIV (TYPE('a)) in if c = 0 then 0 else 2 ^ c)"
   1.123 +definition "card_UNIV = Phantom('a set)
   1.124 +  (let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c = 0 then 0 else 2 ^ c)"
   1.125  instance by intro_classes (simp add: card_UNIV_set_def card_UNIV_set card_UNIV)
   1.126  end
   1.127  
   1.128 @@ -278,27 +285,27 @@
   1.129  by(auto intro: finite_5.exhaust)
   1.130  
   1.131  instantiation Enum.finite_1 :: card_UNIV begin
   1.132 -definition "card_UNIV = (\<lambda>a :: Enum.finite_1 itself. 1)"
   1.133 +definition "card_UNIV = Phantom(Enum.finite_1) 1"
   1.134  instance by intro_classes (simp add: UNIV_finite_1 card_UNIV_finite_1_def)
   1.135  end
   1.136  
   1.137  instantiation Enum.finite_2 :: card_UNIV begin
   1.138 -definition "card_UNIV = (\<lambda>a :: Enum.finite_2 itself. 2)"
   1.139 +definition "card_UNIV = Phantom(Enum.finite_2) 2"
   1.140  instance by intro_classes (simp add: UNIV_finite_2 card_UNIV_finite_2_def)
   1.141  end
   1.142  
   1.143  instantiation Enum.finite_3 :: card_UNIV begin
   1.144 -definition "card_UNIV = (\<lambda>a :: Enum.finite_3 itself. 3)"
   1.145 +definition "card_UNIV = Phantom(Enum.finite_3) 3"
   1.146  instance by intro_classes (simp add: UNIV_finite_3 card_UNIV_finite_3_def)
   1.147  end
   1.148  
   1.149  instantiation Enum.finite_4 :: card_UNIV begin
   1.150 -definition "card_UNIV = (\<lambda>a :: Enum.finite_4 itself. 4)"
   1.151 +definition "card_UNIV = Phantom(Enum.finite_4) 4"
   1.152  instance by intro_classes (simp add: UNIV_finite_4 card_UNIV_finite_4_def)
   1.153  end
   1.154  
   1.155  instantiation Enum.finite_5 :: card_UNIV begin
   1.156 -definition "card_UNIV = (\<lambda>a :: Enum.finite_5 itself. 5)"
   1.157 +definition "card_UNIV = Phantom(Enum.finite_5) 5"
   1.158  instance by intro_classes (simp add: UNIV_finite_5 card_UNIV_finite_5_def)
   1.159  end
   1.160  
   1.161 @@ -316,10 +323,11 @@
   1.162  
   1.163  lemma card'_code [code]:
   1.164    "card' (set xs) = length (remdups xs)"
   1.165 -  "card' (List.coset xs) =  card_UNIV TYPE('a) - length (remdups xs)"
   1.166 +  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
   1.167  by(simp_all add: List.card_set card_Compl card_UNIV)
   1.168  
   1.169 -lemma card'_UNIV [code_unfold]: "card' (UNIV :: 'a :: card_UNIV set) = card_UNIV TYPE('a)"
   1.170 +lemma card'_UNIV [code_unfold]: 
   1.171 +  "card' (UNIV :: 'a :: card_UNIV set) = of_phantom (card_UNIV :: 'a card_UNIV)"
   1.172  by(simp add: card_UNIV)
   1.173  
   1.174  definition finite' :: "'a set \<Rightarrow> bool"