src/HOL/Library/Numeral_Type.thy
author wenzelm
Mon Jan 16 21:50:15 2012 +0100 (2012-01-16)
changeset 46236 ae79f2978a67
parent 37653 847e95ca9b0a
child 46868 6c250adbe101
permissions -rw-r--r--
position constraints for numerals enable PIDE markup;
     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 Cardinality
     9 begin
    10 
    11 subsection {* Numeral Types *}
    12 
    13 typedef (open) num0 = "UNIV :: nat set" ..
    14 typedef (open) num1 = "UNIV :: unit set" ..
    15 
    16 typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
    17 proof
    18   show "0 \<in> {0 ..< 2 * int CARD('a)}"
    19     by simp
    20 qed
    21 
    22 typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
    23 proof
    24   show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}"
    25     by simp
    26 qed
    27 
    28 lemma card_num0 [simp]: "CARD (num0) = 0"
    29   unfolding type_definition.card [OF type_definition_num0]
    30   by simp
    31 
    32 lemma card_num1 [simp]: "CARD(num1) = 1"
    33   unfolding type_definition.card [OF type_definition_num1]
    34   by (simp only: card_unit)
    35 
    36 lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
    37   unfolding type_definition.card [OF type_definition_bit0]
    38   by simp
    39 
    40 lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))"
    41   unfolding type_definition.card [OF type_definition_bit1]
    42   by simp
    43 
    44 instance num1 :: finite
    45 proof
    46   show "finite (UNIV::num1 set)"
    47     unfolding type_definition.univ [OF type_definition_num1]
    48     using finite by (rule finite_imageI)
    49 qed
    50 
    51 instance bit0 :: (finite) card2
    52 proof
    53   show "finite (UNIV::'a bit0 set)"
    54     unfolding type_definition.univ [OF type_definition_bit0]
    55     by simp
    56   show "2 \<le> CARD('a bit0)"
    57     by simp
    58 qed
    59 
    60 instance bit1 :: (finite) card2
    61 proof
    62   show "finite (UNIV::'a bit1 set)"
    63     unfolding type_definition.univ [OF type_definition_bit1]
    64     by simp
    65   show "2 \<le> CARD('a bit1)"
    66     by simp
    67 qed
    68 
    69 
    70 subsection {* Locales for for modular arithmetic subtypes *}
    71 
    72 locale mod_type =
    73   fixes n :: int
    74   and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
    75   and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
    76   assumes type: "type_definition Rep Abs {0..<n}"
    77   and size1: "1 < n"
    78   and zero_def: "0 = Abs 0"
    79   and one_def:  "1 = Abs 1"
    80   and add_def:  "x + y = Abs ((Rep x + Rep y) mod n)"
    81   and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
    82   and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
    83   and minus_def: "- x = Abs ((- Rep x) mod n)"
    84 begin
    85 
    86 lemma size0: "0 < n"
    87 using size1 by simp
    88 
    89 lemmas definitions =
    90   zero_def one_def add_def mult_def minus_def diff_def
    91 
    92 lemma Rep_less_n: "Rep x < n"
    93 by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
    94 
    95 lemma Rep_le_n: "Rep x \<le> n"
    96 by (rule Rep_less_n [THEN order_less_imp_le])
    97 
    98 lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
    99 by (rule type_definition.Rep_inject [OF type, symmetric])
   100 
   101 lemma Rep_inverse: "Abs (Rep x) = x"
   102 by (rule type_definition.Rep_inverse [OF type])
   103 
   104 lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
   105 by (rule type_definition.Abs_inverse [OF type])
   106 
   107 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
   108 by (simp add: Abs_inverse pos_mod_conj [OF size0])
   109 
   110 lemma Rep_Abs_0: "Rep (Abs 0) = 0"
   111 by (simp add: Abs_inverse size0)
   112 
   113 lemma Rep_0: "Rep 0 = 0"
   114 by (simp add: zero_def Rep_Abs_0)
   115 
   116 lemma Rep_Abs_1: "Rep (Abs 1) = 1"
   117 by (simp add: Abs_inverse size1)
   118 
   119 lemma Rep_1: "Rep 1 = 1"
   120 by (simp add: one_def Rep_Abs_1)
   121 
   122 lemma Rep_mod: "Rep x mod n = Rep x"
   123 apply (rule_tac x=x in type_definition.Abs_cases [OF type])
   124 apply (simp add: type_definition.Abs_inverse [OF type])
   125 apply (simp add: mod_pos_pos_trivial)
   126 done
   127 
   128 lemmas Rep_simps =
   129   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
   130 
   131 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
   132 apply (intro_classes, unfold definitions)
   133 apply (simp_all add: Rep_simps zmod_simps field_simps)
   134 done
   135 
   136 end
   137 
   138 locale mod_ring = mod_type +
   139   constrains n :: int
   140   and Rep :: "'a::{number_ring} \<Rightarrow> int"
   141   and Abs :: "int \<Rightarrow> 'a::{number_ring}"
   142 begin
   143 
   144 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
   145 apply (induct k)
   146 apply (simp add: zero_def)
   147 apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
   148 done
   149 
   150 lemma of_int_eq: "of_int z = Abs (z mod n)"
   151 apply (cases z rule: int_diff_cases)
   152 apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
   153 done
   154 
   155 lemma Rep_number_of:
   156   "Rep (number_of w) = number_of w mod n"
   157 by (simp add: number_of_eq of_int_eq Rep_Abs_mod)
   158 
   159 lemma iszero_number_of:
   160   "iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0"
   161 by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def)
   162 
   163 lemma cases:
   164   assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
   165   shows "P"
   166 apply (cases x rule: type_definition.Abs_cases [OF type])
   167 apply (rule_tac z="y" in 1)
   168 apply (simp_all add: of_int_eq mod_pos_pos_trivial)
   169 done
   170 
   171 lemma induct:
   172   "(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
   173 by (cases x rule: cases) simp
   174 
   175 end
   176 
   177 
   178 subsection {* Number ring instances *}
   179 
   180 text {*
   181   Unfortunately a number ring instance is not possible for
   182   @{typ num1}, since 0 and 1 are not distinct.
   183 *}
   184 
   185 instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
   186 begin
   187 
   188 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
   189   by (induct x, induct y) simp
   190 
   191 instance proof
   192 qed (simp_all add: num1_eq_iff)
   193 
   194 end
   195 
   196 instantiation
   197   bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
   198 begin
   199 
   200 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
   201   "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))"
   202 
   203 definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where
   204   "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))"
   205 
   206 definition "0 = Abs_bit0 0"
   207 definition "1 = Abs_bit0 1"
   208 definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)"
   209 definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
   210 definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
   211 definition "- x = Abs_bit0' (- Rep_bit0 x)"
   212 
   213 definition "0 = Abs_bit1 0"
   214 definition "1 = Abs_bit1 1"
   215 definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)"
   216 definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
   217 definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
   218 definition "- x = Abs_bit1' (- Rep_bit1 x)"
   219 
   220 instance ..
   221 
   222 end
   223 
   224 interpretation bit0:
   225   mod_type "int CARD('a::finite bit0)"
   226            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   227            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   228 apply (rule mod_type.intro)
   229 apply (simp add: int_mult type_definition_bit0)
   230 apply (rule one_less_int_card)
   231 apply (rule zero_bit0_def)
   232 apply (rule one_bit0_def)
   233 apply (rule plus_bit0_def [unfolded Abs_bit0'_def])
   234 apply (rule times_bit0_def [unfolded Abs_bit0'_def])
   235 apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
   236 apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
   237 done
   238 
   239 interpretation bit1:
   240   mod_type "int CARD('a::finite bit1)"
   241            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   242            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   243 apply (rule mod_type.intro)
   244 apply (simp add: int_mult type_definition_bit1)
   245 apply (rule one_less_int_card)
   246 apply (rule zero_bit1_def)
   247 apply (rule one_bit1_def)
   248 apply (rule plus_bit1_def [unfolded Abs_bit1'_def])
   249 apply (rule times_bit1_def [unfolded Abs_bit1'_def])
   250 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
   251 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
   252 done
   253 
   254 instance bit0 :: (finite) comm_ring_1
   255   by (rule bit0.comm_ring_1)+
   256 
   257 instance bit1 :: (finite) comm_ring_1
   258   by (rule bit1.comm_ring_1)+
   259 
   260 instantiation bit0 and bit1 :: (finite) number_ring
   261 begin
   262 
   263 definition "(number_of w :: _ bit0) = of_int w"
   264 
   265 definition "(number_of w :: _ bit1) = of_int w"
   266 
   267 instance proof
   268 qed (rule number_of_bit0_def number_of_bit1_def)+
   269 
   270 end
   271 
   272 interpretation bit0:
   273   mod_ring "int CARD('a::finite bit0)"
   274            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   275            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   276   ..
   277 
   278 interpretation bit1:
   279   mod_ring "int CARD('a::finite bit1)"
   280            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   281            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   282   ..
   283 
   284 text {* Set up cases, induction, and arithmetic *}
   285 
   286 lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
   287 lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
   288 
   289 lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
   290 lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
   291 
   292 lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
   293 lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
   294 
   295 
   296 subsection {* Syntax *}
   297 
   298 syntax
   299   "_NumeralType" :: "num_token => type"  ("_")
   300   "_NumeralType0" :: type ("0")
   301   "_NumeralType1" :: type ("1")
   302 
   303 translations
   304   (type) "1" == (type) "num1"
   305   (type) "0" == (type) "num0"
   306 
   307 parse_translation {*
   308 let
   309   fun mk_bintype n =
   310     let
   311       fun mk_bit 0 = Syntax.const @{type_syntax bit0}
   312         | mk_bit 1 = Syntax.const @{type_syntax bit1};
   313       fun bin_of n =
   314         if n = 1 then Syntax.const @{type_syntax num1}
   315         else if n = 0 then Syntax.const @{type_syntax num0}
   316         else if n = ~1 then raise TERM ("negative type numeral", [])
   317         else
   318           let val (q, r) = Integer.div_mod n 2;
   319           in mk_bit r $ bin_of q end;
   320     in bin_of n end;
   321 
   322   fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
   323     | numeral_tr ts = raise TERM ("numeral_tr", ts);
   324 
   325 in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
   326 *}
   327 
   328 print_translation {*
   329 let
   330   fun int_of [] = 0
   331     | int_of (b :: bs) = b + 2 * int_of bs;
   332 
   333   fun bin_of (Const (@{type_syntax num0}, _)) = []
   334     | bin_of (Const (@{type_syntax num1}, _)) = [1]
   335     | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
   336     | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
   337     | bin_of t = raise TERM ("bin_of", [t]);
   338 
   339   fun bit_tr' b [t] =
   340         let
   341           val rev_digs = b :: bin_of t handle TERM _ => raise Match
   342           val i = int_of rev_digs;
   343           val num = string_of_int (abs i);
   344         in
   345           Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
   346         end
   347     | bit_tr' b _ = raise Match;
   348 in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
   349 *}
   350 
   351 subsection {* Examples *}
   352 
   353 lemma "CARD(0) = 0" by simp
   354 lemma "CARD(17) = 17" by simp
   355 lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
   356 
   357 end