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