src/HOL/Library/Numeral_Type.thy
author wenzelm
Tue Sep 18 16:08:00 2007 +0200 (2007-09-18)
changeset 24630 351a308ab58d
parent 24407 61b10ffb2549
child 25378 dca691610489
permissions -rw-r--r--
simplified type int (eliminated IntInf.int, integer);
     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 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 subsection {* Numeral Types *}
    89 
    90 typedef (open) num0 = "UNIV :: nat set" ..
    91 typedef (open) num1 = "UNIV :: unit set" ..
    92 typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
    93 typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
    94 
    95 instance num1 :: finite
    96 proof
    97   show "finite (UNIV::num1 set)"
    98     unfolding type_definition.univ [OF type_definition_num1]
    99     using finite by (rule finite_imageI)
   100 qed
   101 
   102 instance bit0 :: (finite) finite
   103 proof
   104   show "finite (UNIV::'a bit0 set)"
   105     unfolding type_definition.univ [OF type_definition_bit0]
   106     using finite by (rule finite_imageI)
   107 qed
   108 
   109 instance bit1 :: (finite) finite
   110 proof
   111   show "finite (UNIV::'a bit1 set)"
   112     unfolding type_definition.univ [OF type_definition_bit1]
   113     using finite by (rule finite_imageI)
   114 qed
   115 
   116 lemma card_num1: "CARD(num1) = 1"
   117   unfolding type_definition.card [OF type_definition_num1]
   118   by (simp only: card_unit)
   119 
   120 lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)"
   121   unfolding type_definition.card [OF type_definition_bit0]
   122   by (simp only: card_prod card_bool)
   123 
   124 lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))"
   125   unfolding type_definition.card [OF type_definition_bit1]
   126   by (simp only: card_prod card_option card_bool)
   127 
   128 lemma card_num0: "CARD (num0) = 0"
   129   by (simp add: type_definition.card [OF type_definition_num0])
   130 
   131 lemmas card_univ_simps [simp] =
   132   card_unit
   133   card_bool
   134   card_prod
   135   card_sum
   136   card_option
   137   card_set
   138   card_num1
   139   card_bit0
   140   card_bit1
   141   card_num0
   142 
   143 subsection {* Syntax *}
   144 
   145 
   146 syntax
   147   "_NumeralType" :: "num_const => type"  ("_")
   148   "_NumeralType0" :: type ("0")
   149   "_NumeralType1" :: type ("1")
   150 
   151 translations
   152   "_NumeralType1" == (type) "num1"
   153   "_NumeralType0" == (type) "num0"
   154 
   155 parse_translation {*
   156 let
   157 
   158 val num1_const = Syntax.const "Numeral_Type.num1";
   159 val num0_const = Syntax.const "Numeral_Type.num0";
   160 val B0_const = Syntax.const "Numeral_Type.bit0";
   161 val B1_const = Syntax.const "Numeral_Type.bit1";
   162 
   163 fun mk_bintype n =
   164   let
   165     fun mk_bit n = if n = 0 then B0_const else B1_const;
   166     fun bin_of n =
   167       if n = 1 then num1_const
   168       else if n = 0 then num0_const
   169       else if n = ~1 then raise TERM ("negative type numeral", [])
   170       else
   171         let val (q, r) = Integer.div_mod n 2;
   172         in mk_bit r $ bin_of q end;
   173   in bin_of n end;
   174 
   175 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
   176       mk_bintype (valOf (Int.fromString str))
   177   | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
   178 
   179 in [("_NumeralType", numeral_tr)] end;
   180 *}
   181 
   182 print_translation {*
   183 let
   184 fun int_of [] = 0
   185   | int_of (b :: bs) = b + 2 * int_of bs;
   186 
   187 fun bin_of (Const ("num0", _)) = []
   188   | bin_of (Const ("num1", _)) = [1]
   189   | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
   190   | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
   191   | bin_of t = raise TERM("bin_of", [t]);
   192 
   193 fun bit_tr' b [t] =
   194   let
   195     val rev_digs = b :: bin_of t handle TERM _ => raise Match
   196     val i = int_of rev_digs;
   197     val num = string_of_int (abs i);
   198   in
   199     Syntax.const "_NumeralType" $ Syntax.free num
   200   end
   201   | bit_tr' b _ = raise Match;
   202 
   203 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
   204 *}
   205 
   206 
   207 subsection {* Classes with at values least 1 and 2  *}
   208 
   209 text {* Class finite already captures "at least 1" *}
   210 
   211 lemma zero_less_card_finite [simp]:
   212   "0 < CARD('a::finite)"
   213 proof (cases "CARD('a::finite) = 0")
   214   case False thus ?thesis by (simp del: card_0_eq)
   215 next
   216   case True
   217   thus ?thesis by (simp add: finite)
   218 qed
   219 
   220 lemma one_le_card_finite [simp]:
   221   "Suc 0 <= CARD('a::finite)"
   222   by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
   223 
   224 
   225 text {* Class for cardinality "at least 2" *}
   226 
   227 class card2 = finite + 
   228   assumes two_le_card: "2 <= CARD('a)"
   229 
   230 lemma one_less_card: "Suc 0 < CARD('a::card2)"
   231   using two_le_card [where 'a='a] by simp
   232 
   233 instance bit0 :: (finite) card2
   234   by intro_classes (simp add: one_le_card_finite)
   235 
   236 instance bit1 :: (finite) card2
   237   by intro_classes (simp add: one_le_card_finite)
   238 
   239 subsection {* Examples *}
   240 
   241 term "TYPE(10)"
   242 
   243 lemma "CARD(0) = 0" by simp
   244 lemma "CARD(17) = 17" by simp
   245   
   246 end