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