src/HOL/Library/Numeral_Type.thy
author chaieb
Mon Feb 09 17:21:46 2009 +0000 (2009-02-09)
changeset 29847 af32126ee729
parent 29629 5111ce425e7a
child 29997 f6756c097c2d
child 30240 5b25fee0362c
permissions -rw-r--r--
added Determinants to Library
     1 (*  Title:      HOL/Library/Numeral_Type.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Numeral Syntax for Types *}
     6 
     7 theory Numeral_Type
     8 imports Plain "~~/src/HOL/Presburger"
     9 begin
    10 
    11 subsection {* Preliminary lemmas *}
    12 (* These should be moved elsewhere *)
    13 
    14 lemma (in type_definition) univ:
    15   "UNIV = Abs ` A"
    16 proof
    17   show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
    18   show "UNIV \<subseteq> Abs ` A"
    19   proof
    20     fix x :: 'b
    21     have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
    22     moreover have "Rep x \<in> A" by (rule Rep)
    23     ultimately show "x \<in> Abs ` A" by (rule image_eqI)
    24   qed
    25 qed
    26 
    27 lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
    28   by (simp add: univ card_image inj_on_def Abs_inject)
    29 
    30 
    31 subsection {* Cardinalities of types *}
    32 
    33 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    34 
    35 translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
    36 
    37 typed_print_translation {*
    38 let
    39   fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
    40     Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
    41 in [(@{const_syntax card}, card_univ_tr')]
    42 end
    43 *}
    44 
    45 lemma card_unit: "CARD(unit) = 1"
    46   unfolding UNIV_unit by simp
    47 
    48 lemma card_bool: "CARD(bool) = 2"
    49   unfolding UNIV_bool by simp
    50 
    51 lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
    52   unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    53 
    54 lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
    55   unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
    56 
    57 lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
    58   unfolding insert_None_conv_UNIV [symmetric]
    59   apply (subgoal_tac "(None::'a option) \<notin> range Some")
    60   apply (simp add: finite card_image)
    61   apply fast
    62   done
    63 
    64 lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
    65   unfolding Pow_UNIV [symmetric]
    66   by (simp only: card_Pow finite numeral_2_eq_2)
    67 
    68 
    69 subsection {* Numeral Types *}
    70 
    71 typedef (open) num0 = "UNIV :: nat set" ..
    72 typedef (open) num1 = "UNIV :: unit set" ..
    73 typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
    74 typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
    75 
    76 instance num1 :: finite
    77 proof
    78   show "finite (UNIV::num1 set)"
    79     unfolding type_definition.univ [OF type_definition_num1]
    80     using finite by (rule finite_imageI)
    81 qed
    82 
    83 instance bit0 :: (finite) finite
    84 proof
    85   show "finite (UNIV::'a bit0 set)"
    86     unfolding type_definition.univ [OF type_definition_bit0]
    87     using finite by (rule finite_imageI)
    88 qed
    89 
    90 instance bit1 :: (finite) finite
    91 proof
    92   show "finite (UNIV::'a bit1 set)"
    93     unfolding type_definition.univ [OF type_definition_bit1]
    94     using finite by (rule finite_imageI)
    95 qed
    96 
    97 lemma card_num1: "CARD(num1) = 1"
    98   unfolding type_definition.card [OF type_definition_num1]
    99   by (simp only: card_unit)
   100 
   101 lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)"
   102   unfolding type_definition.card [OF type_definition_bit0]
   103   by (simp only: card_prod card_bool)
   104 
   105 lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))"
   106   unfolding type_definition.card [OF type_definition_bit1]
   107   by (simp only: card_prod card_option card_bool)
   108 
   109 lemma card_num0: "CARD (num0) = 0"
   110   by (simp add: infinite_UNIV_nat card_eq_0_iff type_definition.card [OF type_definition_num0])
   111 
   112 lemmas card_univ_simps [simp] =
   113   card_unit
   114   card_bool
   115   card_prod
   116   card_sum
   117   card_option
   118   card_set
   119   card_num1
   120   card_bit0
   121   card_bit1
   122   card_num0
   123 
   124 
   125 subsection {* Syntax *}
   126 
   127 syntax
   128   "_NumeralType" :: "num_const => type"  ("_")
   129   "_NumeralType0" :: type ("0")
   130   "_NumeralType1" :: type ("1")
   131 
   132 translations
   133   "_NumeralType1" == (type) "num1"
   134   "_NumeralType0" == (type) "num0"
   135 
   136 parse_translation {*
   137 let
   138 
   139 val num1_const = Syntax.const "Numeral_Type.num1";
   140 val num0_const = Syntax.const "Numeral_Type.num0";
   141 val B0_const = Syntax.const "Numeral_Type.bit0";
   142 val B1_const = Syntax.const "Numeral_Type.bit1";
   143 
   144 fun mk_bintype n =
   145   let
   146     fun mk_bit n = if n = 0 then B0_const else B1_const;
   147     fun bin_of n =
   148       if n = 1 then num1_const
   149       else if n = 0 then num0_const
   150       else if n = ~1 then raise TERM ("negative type numeral", [])
   151       else
   152         let val (q, r) = Integer.div_mod n 2;
   153         in mk_bit r $ bin_of q end;
   154   in bin_of n end;
   155 
   156 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
   157       mk_bintype (valOf (Int.fromString str))
   158   | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
   159 
   160 in [("_NumeralType", numeral_tr)] end;
   161 *}
   162 
   163 print_translation {*
   164 let
   165 fun int_of [] = 0
   166   | int_of (b :: bs) = b + 2 * int_of bs;
   167 
   168 fun bin_of (Const ("num0", _)) = []
   169   | bin_of (Const ("num1", _)) = [1]
   170   | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
   171   | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
   172   | bin_of t = raise TERM("bin_of", [t]);
   173 
   174 fun bit_tr' b [t] =
   175   let
   176     val rev_digs = b :: bin_of t handle TERM _ => raise Match
   177     val i = int_of rev_digs;
   178     val num = string_of_int (abs i);
   179   in
   180     Syntax.const "_NumeralType" $ Syntax.free num
   181   end
   182   | bit_tr' b _ = raise Match;
   183 
   184 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
   185 *}
   186 
   187 
   188 subsection {* Classes with at least 1 and 2  *}
   189 
   190 text {* Class finite already captures "at least 1" *}
   191 
   192 lemma zero_less_card_finite [simp]:
   193   "0 < CARD('a::finite)"
   194 proof (cases "CARD('a::finite) = 0")
   195   case False thus ?thesis by (simp del: card_0_eq)
   196 next
   197   case True
   198   thus ?thesis by (simp add: finite)
   199 qed
   200 
   201 lemma one_le_card_finite [simp]:
   202   "Suc 0 <= CARD('a::finite)"
   203   by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
   204 
   205 
   206 text {* Class for cardinality "at least 2" *}
   207 
   208 class card2 = finite + 
   209   assumes two_le_card: "2 <= CARD('a)"
   210 
   211 lemma one_less_card: "Suc 0 < CARD('a::card2)"
   212   using two_le_card [where 'a='a] by simp
   213 
   214 instance bit0 :: (finite) card2
   215   by intro_classes (simp add: one_le_card_finite)
   216 
   217 instance bit1 :: (finite) card2
   218   by intro_classes (simp add: one_le_card_finite)
   219 
   220 subsection {* Examples *}
   221 
   222 lemma "CARD(0) = 0" by simp
   223 lemma "CARD(17) = 17" by simp
   224 
   225 end