src/HOL/Library/Numeral_Type.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 48063 f02b4302d5dd
child 49834 b27bbb021df1
permissions -rw-r--r--
tuned headers;
     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_UNIV_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 subsection {* Locales for for modular arithmetic subtypes *}
    70 
    71 locale mod_type =
    72   fixes n :: int
    73   and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
    74   and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
    75   assumes type: "type_definition Rep Abs {0..<n}"
    76   and size1: "1 < n"
    77   and zero_def: "0 = Abs 0"
    78   and one_def:  "1 = Abs 1"
    79   and add_def:  "x + y = Abs ((Rep x + Rep y) mod n)"
    80   and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
    81   and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
    82   and minus_def: "- x = Abs ((- Rep x) mod n)"
    83 begin
    84 
    85 lemma size0: "0 < n"
    86 using size1 by simp
    87 
    88 lemmas definitions =
    89   zero_def one_def add_def mult_def minus_def diff_def
    90 
    91 lemma Rep_less_n: "Rep x < n"
    92 by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
    93 
    94 lemma Rep_le_n: "Rep x \<le> n"
    95 by (rule Rep_less_n [THEN order_less_imp_le])
    96 
    97 lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
    98 by (rule type_definition.Rep_inject [OF type, symmetric])
    99 
   100 lemma Rep_inverse: "Abs (Rep x) = x"
   101 by (rule type_definition.Rep_inverse [OF type])
   102 
   103 lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
   104 by (rule type_definition.Abs_inverse [OF type])
   105 
   106 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
   107 by (simp add: Abs_inverse pos_mod_conj [OF size0])
   108 
   109 lemma Rep_Abs_0: "Rep (Abs 0) = 0"
   110 by (simp add: Abs_inverse size0)
   111 
   112 lemma Rep_0: "Rep 0 = 0"
   113 by (simp add: zero_def Rep_Abs_0)
   114 
   115 lemma Rep_Abs_1: "Rep (Abs 1) = 1"
   116 by (simp add: Abs_inverse size1)
   117 
   118 lemma Rep_1: "Rep 1 = 1"
   119 by (simp add: one_def Rep_Abs_1)
   120 
   121 lemma Rep_mod: "Rep x mod n = Rep x"
   122 apply (rule_tac x=x in type_definition.Abs_cases [OF type])
   123 apply (simp add: type_definition.Abs_inverse [OF type])
   124 apply (simp add: mod_pos_pos_trivial)
   125 done
   126 
   127 lemmas Rep_simps =
   128   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
   129 
   130 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
   131 apply (intro_classes, unfold definitions)
   132 apply (simp_all add: Rep_simps zmod_simps field_simps)
   133 done
   134 
   135 end
   136 
   137 locale mod_ring = mod_type n Rep Abs
   138   for n :: int
   139   and Rep :: "'a::{comm_ring_1} \<Rightarrow> int"
   140   and Abs :: "int \<Rightarrow> 'a::{comm_ring_1}"
   141 begin
   142 
   143 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
   144 apply (induct k)
   145 apply (simp add: zero_def)
   146 apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
   147 done
   148 
   149 lemma of_int_eq: "of_int z = Abs (z mod n)"
   150 apply (cases z rule: int_diff_cases)
   151 apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
   152 done
   153 
   154 lemma Rep_numeral:
   155   "Rep (numeral w) = numeral w mod n"
   156 using of_int_eq [of "numeral w"]
   157 by (simp add: Rep_inject_sym Rep_Abs_mod)
   158 
   159 lemma iszero_numeral:
   160   "iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0"
   161 by (simp add: Rep_inject_sym Rep_numeral Rep_0 iszero_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 {* Ring class instances *}
   179 
   180 text {*
   181   Unfortunately @{text ring_1} 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,numeral}"
   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 interpretation bit0:
   261   mod_ring "int CARD('a::finite bit0)"
   262            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   263            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   264   ..
   265 
   266 interpretation bit1:
   267   mod_ring "int CARD('a::finite bit1)"
   268            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   269            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   270   ..
   271 
   272 text {* Set up cases, induction, and arithmetic *}
   273 
   274 lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
   275 lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
   276 
   277 lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
   278 lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
   279 
   280 lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
   281 lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
   282 
   283 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
   284 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
   285 
   286 subsection {* Syntax *}
   287 
   288 syntax
   289   "_NumeralType" :: "num_token => type"  ("_")
   290   "_NumeralType0" :: type ("0")
   291   "_NumeralType1" :: type ("1")
   292 
   293 translations
   294   (type) "1" == (type) "num1"
   295   (type) "0" == (type) "num0"
   296 
   297 parse_translation {*
   298 let
   299   fun mk_bintype n =
   300     let
   301       fun mk_bit 0 = Syntax.const @{type_syntax bit0}
   302         | mk_bit 1 = Syntax.const @{type_syntax bit1};
   303       fun bin_of n =
   304         if n = 1 then Syntax.const @{type_syntax num1}
   305         else if n = 0 then Syntax.const @{type_syntax num0}
   306         else if n = ~1 then raise TERM ("negative type numeral", [])
   307         else
   308           let val (q, r) = Integer.div_mod n 2;
   309           in mk_bit r $ bin_of q end;
   310     in bin_of n end;
   311 
   312   fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
   313     | numeral_tr ts = raise TERM ("numeral_tr", ts);
   314 
   315 in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
   316 *}
   317 
   318 print_translation {*
   319 let
   320   fun int_of [] = 0
   321     | int_of (b :: bs) = b + 2 * int_of bs;
   322 
   323   fun bin_of (Const (@{type_syntax num0}, _)) = []
   324     | bin_of (Const (@{type_syntax num1}, _)) = [1]
   325     | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
   326     | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
   327     | bin_of t = raise TERM ("bin_of", [t]);
   328 
   329   fun bit_tr' b [t] =
   330         let
   331           val rev_digs = b :: bin_of t handle TERM _ => raise Match
   332           val i = int_of rev_digs;
   333           val num = string_of_int (abs i);
   334         in
   335           Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
   336         end
   337     | bit_tr' b _ = raise Match;
   338 in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
   339 *}
   340 
   341 subsection {* Examples *}
   342 
   343 lemma "CARD(0) = 0" by simp
   344 lemma "CARD(17) = 17" by simp
   345 lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
   346 
   347 end