src/HOL/Library/Numeral_Type.thy
author huffman
Wed Aug 22 18:53:54 2007 +0200 (2007-08-22)
changeset 24406 d96eb21fc1bc
parent 24332 e3a2b75b1cf9
child 24407 61b10ffb2549
permissions -rw-r--r--
rename type pls to num0
     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)" => "card (UNIV::t set)"
    56 
    57 lemma card_unit: "CARD(unit) = 1"
    58   unfolding univ_unit by simp
    59 
    60 lemma card_bool: "CARD(bool) = 2"
    61   unfolding univ_bool by simp
    62 
    63 lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
    64   unfolding univ_prod by (simp only: card_cartesian_product)
    65 
    66 lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
    67   unfolding univ_sum by (simp only: finite card_Plus)
    68 
    69 lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
    70   unfolding univ_option
    71   apply (subgoal_tac "(None::'a option) \<notin> range Some")
    72   apply (simp add: finite card_image)
    73   apply fast
    74   done
    75 
    76 lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
    77   unfolding univ_set
    78   by (simp only: card_Pow finite numeral_2_eq_2)
    79 
    80 subsection {* Numeral Types *}
    81 
    82 typedef (open) num0 = "UNIV :: nat set" ..
    83 typedef (open) num1 = "UNIV :: unit set" ..
    84 typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
    85 typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
    86 
    87 instance num1 :: finite
    88 proof
    89   show "finite (UNIV::num1 set)"
    90     unfolding type_definition.univ [OF type_definition_num1]
    91     using finite by (rule finite_imageI)
    92 qed
    93 
    94 instance bit0 :: (finite) finite
    95 proof
    96   show "finite (UNIV::'a bit0 set)"
    97     unfolding type_definition.univ [OF type_definition_bit0]
    98     using finite by (rule finite_imageI)
    99 qed
   100 
   101 instance bit1 :: (finite) finite
   102 proof
   103   show "finite (UNIV::'a bit1 set)"
   104     unfolding type_definition.univ [OF type_definition_bit1]
   105     using finite by (rule finite_imageI)
   106 qed
   107 
   108 lemma card_num1: "CARD(num1) = 1"
   109   unfolding type_definition.card [OF type_definition_num1]
   110   by (simp only: card_unit)
   111 
   112 lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)"
   113   unfolding type_definition.card [OF type_definition_bit0]
   114   by (simp only: card_prod card_bool)
   115 
   116 lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))"
   117   unfolding type_definition.card [OF type_definition_bit1]
   118   by (simp only: card_prod card_option card_bool)
   119 
   120 lemma card_num0: "CARD (num0) = 0"
   121   by (simp add: type_definition.card [OF type_definition_num0])
   122 
   123 lemmas card_univ_simps [simp] =
   124   card_unit
   125   card_bool
   126   card_prod
   127   card_sum
   128   card_option
   129   card_set
   130   card_num1
   131   card_bit0
   132   card_bit1
   133   card_num0
   134 
   135 subsection {* Syntax *}
   136 
   137 
   138 syntax
   139   "_NumeralType" :: "num_const => type"  ("_")
   140   "_NumeralType0" :: type ("0")
   141   "_NumeralType1" :: type ("1")
   142 
   143 translations
   144   "_NumeralType1" == (type) "num1"
   145   "_NumeralType0" == (type) "num0"
   146 
   147 parse_translation {*
   148 let
   149 
   150 val num1_const = Syntax.const "Numeral_Type.num1";
   151 val num0_const = Syntax.const "Numeral_Type.num0";
   152 val B0_const = Syntax.const "Numeral_Type.bit0";
   153 val B1_const = Syntax.const "Numeral_Type.bit1";
   154 
   155 fun mk_bintype n =
   156   let
   157     fun mk_bit n = if n = 0 then B0_const else B1_const;
   158     fun bin_of n =
   159       if n = 1 then num1_const
   160       else if n = 0 then num0_const
   161       else if n = ~1 then raise TERM ("negative type numeral", [])
   162       else
   163         let val (q, r) = IntInf.divMod (n, 2);
   164         in mk_bit r $ bin_of q end;
   165   in bin_of n end;
   166 
   167 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
   168       mk_bintype (valOf (IntInf.fromString str))
   169   | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
   170 
   171 in [("_NumeralType", numeral_tr)] end;
   172 *}
   173 
   174 print_translation {*
   175 let
   176 fun int_of [] = 0
   177   | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
   178 
   179 fun bin_of (Const ("num0", _)) = []
   180   | bin_of (Const ("num1", _)) = [1]
   181   | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
   182   | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
   183   | bin_of t = raise TERM("bin_of", [t]);
   184 
   185 fun bit_tr' b [t] =
   186   let
   187     val rev_digs = b :: bin_of t handle TERM _ => raise Match
   188     val i = int_of rev_digs;
   189     val num = IntInf.toString (IntInf.abs i);
   190   in
   191     Syntax.const "_NumeralType" $ Syntax.free num
   192   end
   193   | bit_tr' b _ = raise Match;
   194 
   195 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
   196 *}
   197 
   198 
   199 subsection {* Classes with at values least 1 and 2  *}
   200 
   201 text {* Class finite already captures "at least 1" *}
   202 
   203 lemma zero_less_card_finite:
   204   "0 < CARD('a::finite)"
   205 proof (cases "CARD('a::finite) = 0")
   206   case False thus ?thesis by (simp del: card_0_eq)
   207 next
   208   case True
   209   thus ?thesis by (simp add: finite)
   210 qed
   211 
   212 lemma one_le_card_finite:
   213   "Suc 0 <= CARD('a::finite)"
   214   by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
   215 
   216 
   217 text {* Class for cardinality "at least 2" *}
   218 
   219 class card2 = finite + 
   220   assumes two_le_card: "2 <= CARD('a)"
   221 
   222 lemma one_less_card: "Suc 0 < CARD('a::card2)"
   223   using two_le_card [where 'a='a] by simp
   224 
   225 instance bit0 :: (finite) card2
   226   by intro_classes (simp add: one_le_card_finite)
   227 
   228 instance bit1 :: (finite) card2
   229   by intro_classes (simp add: one_le_card_finite)
   230 
   231 subsection {* Examples *}
   232 
   233 term "TYPE(10)"
   234 
   235 lemma "CARD(0) = 0" by simp
   236 lemma "CARD(17) = 17" by simp
   237   
   238 end