src/HOL/Library/Numeral_Type.thy
changeset 24332 e3a2b75b1cf9
child 24406 d96eb21fc1bc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Aug 20 00:22:18 2007 +0200
     1.3 @@ -0,0 +1,238 @@
     1.4 +(*
     1.5 +  ID:     $Id$
     1.6 +  Author: Brian Huffman
     1.7 +
     1.8 +  Numeral Syntax for Types
     1.9 +*)
    1.10 +
    1.11 +header "Numeral Syntax for Types"
    1.12 +
    1.13 +theory Numeral_Type
    1.14 +  imports Infinite_Set
    1.15 +begin
    1.16 +
    1.17 +subsection {* Preliminary lemmas *}
    1.18 +(* These should be moved elsewhere *)
    1.19 +
    1.20 +lemma inj_Inl [simp]: "inj_on Inl A"
    1.21 +  by (rule inj_onI, simp)
    1.22 +
    1.23 +lemma inj_Inr [simp]: "inj_on Inr A"
    1.24 +  by (rule inj_onI, simp)
    1.25 +
    1.26 +lemma inj_Some [simp]: "inj_on Some A"
    1.27 +  by (rule inj_onI, simp)
    1.28 +
    1.29 +lemma card_Plus:
    1.30 +  "[| finite A; finite B |] ==> card (A <+> B) = card A + card B"
    1.31 +  unfolding Plus_def
    1.32 +  apply (subgoal_tac "Inl ` A \<inter> Inr ` B = {}")
    1.33 +  apply (simp add: card_Un_disjoint card_image)
    1.34 +  apply fast
    1.35 +  done
    1.36 +
    1.37 +lemma (in type_definition) univ:
    1.38 +  "UNIV = Abs ` A"
    1.39 +proof
    1.40 +  show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
    1.41 +  show "UNIV \<subseteq> Abs ` A"
    1.42 +  proof
    1.43 +    fix x :: 'b
    1.44 +    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
    1.45 +    moreover have "Rep x \<in> A" by (rule Rep)
    1.46 +    ultimately show "x \<in> Abs ` A" by (rule image_eqI)
    1.47 +  qed
    1.48 +qed
    1.49 +
    1.50 +lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
    1.51 +  by (simp add: univ card_image inj_on_def Abs_inject)
    1.52 +
    1.53 +
    1.54 +subsection {* Cardinalities of types *}
    1.55 +
    1.56 +syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    1.57 +
    1.58 +translations "CARD(t)" => "card (UNIV::t set)"
    1.59 +
    1.60 +lemma card_unit: "CARD(unit) = 1"
    1.61 +  unfolding univ_unit by simp
    1.62 +
    1.63 +lemma card_bool: "CARD(bool) = 2"
    1.64 +  unfolding univ_bool by simp
    1.65 +
    1.66 +lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
    1.67 +  unfolding univ_prod by (simp only: card_cartesian_product)
    1.68 +
    1.69 +lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
    1.70 +  unfolding univ_sum by (simp only: finite card_Plus)
    1.71 +
    1.72 +lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
    1.73 +  unfolding univ_option
    1.74 +  apply (subgoal_tac "(None::'a option) \<notin> range Some")
    1.75 +  apply (simp add: finite card_image)
    1.76 +  apply fast
    1.77 +  done
    1.78 +
    1.79 +lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
    1.80 +  unfolding univ_set
    1.81 +  by (simp only: card_Pow finite numeral_2_eq_2)
    1.82 +
    1.83 +subsection {* Numeral Types *}
    1.84 +
    1.85 +typedef (open) pls = "UNIV :: nat set" ..
    1.86 +typedef (open) num1 = "UNIV :: unit set" ..
    1.87 +typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
    1.88 +typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
    1.89 +
    1.90 +instance num1 :: finite
    1.91 +proof
    1.92 +  show "finite (UNIV::num1 set)"
    1.93 +    unfolding type_definition.univ [OF type_definition_num1]
    1.94 +    using finite by (rule finite_imageI)
    1.95 +qed
    1.96 +
    1.97 +instance bit0 :: (finite) finite
    1.98 +proof
    1.99 +  show "finite (UNIV::'a bit0 set)"
   1.100 +    unfolding type_definition.univ [OF type_definition_bit0]
   1.101 +    using finite by (rule finite_imageI)
   1.102 +qed
   1.103 +
   1.104 +instance bit1 :: (finite) finite
   1.105 +proof
   1.106 +  show "finite (UNIV::'a bit1 set)"
   1.107 +    unfolding type_definition.univ [OF type_definition_bit1]
   1.108 +    using finite by (rule finite_imageI)
   1.109 +qed
   1.110 +
   1.111 +lemma card_num1: "CARD(num1) = 1"
   1.112 +  unfolding type_definition.card [OF type_definition_num1]
   1.113 +  by (simp only: card_unit)
   1.114 +
   1.115 +lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)"
   1.116 +  unfolding type_definition.card [OF type_definition_bit0]
   1.117 +  by (simp only: card_prod card_bool)
   1.118 +
   1.119 +lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))"
   1.120 +  unfolding type_definition.card [OF type_definition_bit1]
   1.121 +  by (simp only: card_prod card_option card_bool)
   1.122 +
   1.123 +lemma card_pls: "CARD (pls) = 0"
   1.124 +  by (simp add: type_definition.card [OF type_definition_pls])
   1.125 +
   1.126 +lemmas card_univ_simps [simp] =
   1.127 +  card_unit
   1.128 +  card_bool
   1.129 +  card_prod
   1.130 +  card_sum
   1.131 +  card_option
   1.132 +  card_set
   1.133 +  card_num1
   1.134 +  card_bit0
   1.135 +  card_bit1
   1.136 +  card_pls
   1.137 +
   1.138 +subsection {* Syntax *}
   1.139 +
   1.140 +
   1.141 +syntax
   1.142 +  "_NumeralType" :: "num_const => type"  ("_")
   1.143 +  "_NumeralType0" :: type ("0")
   1.144 +  "_NumeralType1" :: type ("1")
   1.145 +
   1.146 +translations
   1.147 +  "_NumeralType1" == (type) "num1"
   1.148 +  "_NumeralType0" == (type) "pls"
   1.149 +
   1.150 +parse_translation {*
   1.151 +let
   1.152 +
   1.153 +val num1_const = Syntax.const "Numeral_Type.num1";
   1.154 +val pls_const = Syntax.const "Numeral_Type.pls";
   1.155 +val B0_const = Syntax.const "Numeral_Type.bit0";
   1.156 +val B1_const = Syntax.const "Numeral_Type.bit1";
   1.157 +
   1.158 +fun mk_bintype n =
   1.159 +  let
   1.160 +    fun mk_bit n = if n = 0 then B0_const else B1_const;
   1.161 +    fun bin_of n =
   1.162 +      if n = 1 then num1_const
   1.163 +      else if n = 0 then pls_const
   1.164 +      else if n = ~1 then raise TERM ("negative type numeral", [])
   1.165 +      else
   1.166 +        let val (q, r) = IntInf.divMod (n, 2);
   1.167 +        in mk_bit r $ bin_of q end;
   1.168 +  in bin_of n end;
   1.169 +
   1.170 +fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
   1.171 +      mk_bintype (valOf (IntInf.fromString str))
   1.172 +  | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
   1.173 +
   1.174 +in [("_NumeralType", numeral_tr)] end;
   1.175 +*}
   1.176 +
   1.177 +print_translation {*
   1.178 +let
   1.179 +fun int_of [] = 0
   1.180 +  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
   1.181 +
   1.182 +fun bin_of (Const ("pls", _)) = []
   1.183 +  | bin_of (Const ("num1", _)) = [1]
   1.184 +  | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
   1.185 +  | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
   1.186 +  | bin_of t = raise TERM("bin_of", [t]);
   1.187 +
   1.188 +fun bit_tr' b [t] =
   1.189 +  let
   1.190 +    val rev_digs = b :: bin_of t handle TERM _ => raise Match
   1.191 +    val i = int_of rev_digs;
   1.192 +    val num = IntInf.toString (IntInf.abs i);
   1.193 +  in
   1.194 +    Syntax.const "_NumeralType" $ Syntax.free num
   1.195 +  end
   1.196 +  | bit_tr' b _ = raise Match;
   1.197 +
   1.198 +in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
   1.199 +*}
   1.200 +
   1.201 +
   1.202 +subsection {* Classes with at values least 1 and 2  *}
   1.203 +
   1.204 +text {* Class finite already captures "at least 1" *}
   1.205 +
   1.206 +lemma zero_less_card_finite:
   1.207 +  "0 < CARD('a::finite)"
   1.208 +proof (cases "CARD('a::finite) = 0")
   1.209 +  case False thus ?thesis by (simp del: card_0_eq)
   1.210 +next
   1.211 +  case True
   1.212 +  thus ?thesis by (simp add: finite)
   1.213 +qed
   1.214 +
   1.215 +lemma one_le_card_finite:
   1.216 +  "Suc 0 <= CARD('a::finite)"
   1.217 +  by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
   1.218 +
   1.219 +
   1.220 +text {* Class for cardinality "at least 2" *}
   1.221 +
   1.222 +class card2 = finite + 
   1.223 +  assumes two_le_card: "2 <= CARD('a)"
   1.224 +
   1.225 +lemma one_less_card: "Suc 0 < CARD('a::card2)"
   1.226 +  using two_le_card [where 'a='a] by simp
   1.227 +
   1.228 +instance bit0 :: (finite) card2
   1.229 +  by intro_classes (simp add: one_le_card_finite)
   1.230 +
   1.231 +instance bit1 :: (finite) card2
   1.232 +  by intro_classes (simp add: one_le_card_finite)
   1.233 +
   1.234 +subsection {* Examples *}
   1.235 +
   1.236 +term "TYPE(10)"
   1.237 +
   1.238 +lemma "CARD(0) = 0" by simp
   1.239 +lemma "CARD(17) = 17" by simp
   1.240 +  
   1.241 +end