src/HOL/Library/Numeral_Type.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69678 0f4d4a13dc16
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*  Title:      HOL/Library/Numeral_Type.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Numeral Syntax for Types\<close>
     6 
     7 theory Numeral_Type
     8 imports Cardinality
     9 begin
    10 
    11 subsection \<open>Numeral Types\<close>
    12 
    13 typedef num0 = "UNIV :: nat set" ..
    14 typedef num1 = "UNIV :: unit set" ..
    15 
    16 typedef '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 '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 infinite_num0: "\<not> finite (UNIV :: num0 set)"
    33   using card_num0[unfolded card_eq_0_iff]
    34   by simp
    35 
    36 lemma card_num1 [simp]: "CARD(num1) = 1"
    37   unfolding type_definition.card [OF type_definition_num1]
    38   by (simp only: card_UNIV_unit)
    39 
    40 lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
    41   unfolding type_definition.card [OF type_definition_bit0]
    42   by simp
    43 
    44 lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))"
    45   unfolding type_definition.card [OF type_definition_bit1]
    46   by simp
    47 
    48 subsection \<open>@{typ num1}\<close>
    49 
    50 instance num1 :: finite
    51 proof
    52   show "finite (UNIV::num1 set)"
    53     unfolding type_definition.univ [OF type_definition_num1]
    54     using finite by (rule finite_imageI)
    55 qed
    56 
    57 instantiation num1 :: CARD_1
    58 begin
    59 
    60 instance
    61 proof
    62   show "CARD(num1) = 1" by auto
    63 qed
    64 
    65 end
    66 
    67 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
    68   by (induct x, induct y) simp
    69 
    70 instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}"
    71 begin
    72 
    73 instance
    74   by standard (simp_all add: num1_eq_iff)
    75 
    76 end
    77 
    78 lemma num1_eqI:
    79   fixes a::num1 shows "a = b"
    80 by(simp add: num1_eq_iff)
    81 
    82 lemma num1_eq1 [simp]:
    83   fixes a::num1 shows "a = 1"
    84   by (rule num1_eqI)
    85 
    86 lemma forall_1[simp]: "(\<forall>i::num1. P i) \<longleftrightarrow> P 1"
    87   by (metis (full_types) num1_eq_iff)
    88 
    89 lemma ex_1[simp]: "(\<exists>x::num1. P x) \<longleftrightarrow> P 1"
    90   by auto (metis (full_types) num1_eq_iff)
    91 
    92 instantiation num1 :: linorder begin
    93 definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b"
    94 definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b"
    95 instance
    96   by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI)
    97 end
    98 
    99 instance num1 :: wellorder
   100   by intro_classes (auto simp: less_eq_num1_def less_num1_def)
   101 
   102 
   103 instance bit0 :: (finite) card2
   104 proof
   105   show "finite (UNIV::'a bit0 set)"
   106     unfolding type_definition.univ [OF type_definition_bit0]
   107     by simp
   108   show "2 \<le> CARD('a bit0)"
   109     by simp
   110 qed
   111 
   112 instance bit1 :: (finite) card2
   113 proof
   114   show "finite (UNIV::'a bit1 set)"
   115     unfolding type_definition.univ [OF type_definition_bit1]
   116     by simp
   117   show "2 \<le> CARD('a bit1)"
   118     by simp
   119 qed
   120 
   121 subsection \<open>Locales for for modular arithmetic subtypes\<close>
   122 
   123 locale mod_type =
   124   fixes n :: int
   125   and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
   126   and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
   127   assumes type: "type_definition Rep Abs {0..<n}"
   128   and size1: "1 < n"
   129   and zero_def: "0 = Abs 0"
   130   and one_def:  "1 = Abs 1"
   131   and add_def:  "x + y = Abs ((Rep x + Rep y) mod n)"
   132   and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
   133   and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
   134   and minus_def: "- x = Abs ((- Rep x) mod n)"
   135 begin
   136 
   137 lemma size0: "0 < n"
   138 using size1 by simp
   139 
   140 lemmas definitions =
   141   zero_def one_def add_def mult_def minus_def diff_def
   142 
   143 lemma Rep_less_n: "Rep x < n"
   144 by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
   145 
   146 lemma Rep_le_n: "Rep x \<le> n"
   147 by (rule Rep_less_n [THEN order_less_imp_le])
   148 
   149 lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
   150 by (rule type_definition.Rep_inject [OF type, symmetric])
   151 
   152 lemma Rep_inverse: "Abs (Rep x) = x"
   153 by (rule type_definition.Rep_inverse [OF type])
   154 
   155 lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
   156 by (rule type_definition.Abs_inverse [OF type])
   157 
   158 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
   159 by (simp add: Abs_inverse pos_mod_conj [OF size0])
   160 
   161 lemma Rep_Abs_0: "Rep (Abs 0) = 0"
   162 by (simp add: Abs_inverse size0)
   163 
   164 lemma Rep_0: "Rep 0 = 0"
   165 by (simp add: zero_def Rep_Abs_0)
   166 
   167 lemma Rep_Abs_1: "Rep (Abs 1) = 1"
   168 by (simp add: Abs_inverse size1)
   169 
   170 lemma Rep_1: "Rep 1 = 1"
   171 by (simp add: one_def Rep_Abs_1)
   172 
   173 lemma Rep_mod: "Rep x mod n = Rep x"
   174 apply (rule_tac x=x in type_definition.Abs_cases [OF type])
   175 apply (simp add: type_definition.Abs_inverse [OF type])
   176 done
   177 
   178 lemmas Rep_simps =
   179   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
   180 
   181 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
   182 apply (intro_classes, unfold definitions)
   183 apply (simp_all add: Rep_simps mod_simps field_simps)
   184 done
   185 
   186 end
   187 
   188 locale mod_ring = mod_type n Rep Abs
   189   for n :: int
   190   and Rep :: "'a::{comm_ring_1} \<Rightarrow> int"
   191   and Abs :: "int \<Rightarrow> 'a::{comm_ring_1}"
   192 begin
   193 
   194 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
   195 apply (induct k)
   196 apply (simp add: zero_def)
   197 apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
   198 done
   199 
   200 lemma of_int_eq: "of_int z = Abs (z mod n)"
   201 apply (cases z rule: int_diff_cases)
   202 apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
   203 done
   204 
   205 lemma Rep_numeral:
   206   "Rep (numeral w) = numeral w mod n"
   207 using of_int_eq [of "numeral w"]
   208 by (simp add: Rep_inject_sym Rep_Abs_mod)
   209 
   210 lemma iszero_numeral:
   211   "iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0"
   212 by (simp add: Rep_inject_sym Rep_numeral Rep_0 iszero_def)
   213 
   214 lemma cases:
   215   assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
   216   shows "P"
   217 apply (cases x rule: type_definition.Abs_cases [OF type])
   218 apply (rule_tac z="y" in 1)
   219 apply (simp_all add: of_int_eq)
   220 done
   221 
   222 lemma induct:
   223   "(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
   224 by (cases x rule: cases) simp
   225 
   226 end
   227 
   228 
   229 subsection \<open>Ring class instances\<close>
   230 
   231 text \<open>
   232   Unfortunately \<open>ring_1\<close> instance is not possible for
   233   \<^typ>\<open>num1\<close>, since 0 and 1 are not distinct.
   234 \<close>
   235 
   236 instantiation
   237   bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
   238 begin
   239 
   240 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
   241   "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))"
   242 
   243 definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where
   244   "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))"
   245 
   246 definition "0 = Abs_bit0 0"
   247 definition "1 = Abs_bit0 1"
   248 definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)"
   249 definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
   250 definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
   251 definition "- x = Abs_bit0' (- Rep_bit0 x)"
   252 
   253 definition "0 = Abs_bit1 0"
   254 definition "1 = Abs_bit1 1"
   255 definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)"
   256 definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
   257 definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
   258 definition "- x = Abs_bit1' (- Rep_bit1 x)"
   259 
   260 instance ..
   261 
   262 end
   263 
   264 interpretation bit0:
   265   mod_type "int CARD('a::finite bit0)"
   266            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   267            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   268 apply (rule mod_type.intro)
   269 apply (simp add: type_definition_bit0)
   270 apply (rule one_less_int_card)
   271 apply (rule zero_bit0_def)
   272 apply (rule one_bit0_def)
   273 apply (rule plus_bit0_def [unfolded Abs_bit0'_def])
   274 apply (rule times_bit0_def [unfolded Abs_bit0'_def])
   275 apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
   276 apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
   277 done
   278 
   279 interpretation bit1:
   280   mod_type "int CARD('a::finite bit1)"
   281            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   282            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   283 apply (rule mod_type.intro)
   284 apply (simp add: type_definition_bit1)
   285 apply (rule one_less_int_card)
   286 apply (rule zero_bit1_def)
   287 apply (rule one_bit1_def)
   288 apply (rule plus_bit1_def [unfolded Abs_bit1'_def])
   289 apply (rule times_bit1_def [unfolded Abs_bit1'_def])
   290 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
   291 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
   292 done
   293 
   294 instance bit0 :: (finite) comm_ring_1
   295   by (rule bit0.comm_ring_1)
   296 
   297 instance bit1 :: (finite) comm_ring_1
   298   by (rule bit1.comm_ring_1)
   299 
   300 interpretation bit0:
   301   mod_ring "int CARD('a::finite bit0)"
   302            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
   303            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   304   ..
   305 
   306 interpretation bit1:
   307   mod_ring "int CARD('a::finite bit1)"
   308            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
   309            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   310   ..
   311 
   312 text \<open>Set up cases, induction, and arithmetic\<close>
   313 
   314 lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
   315 lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
   316 
   317 lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
   318 lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
   319 
   320 lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
   321 lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
   322 
   323 lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
   324 lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
   325 
   326 subsection \<open>Order instances\<close>
   327 
   328 instantiation bit0 and bit1 :: (finite) linorder begin
   329 definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b"
   330 definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b"
   331 definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b"
   332 definition "a \<le> b \<longleftrightarrow> Rep_bit1 a \<le> Rep_bit1 b"
   333 
   334 instance
   335   by(intro_classes)
   336     (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
   337 end
   338 
   339 lemma (in preorder) tranclp_less: "(<) \<^sup>+\<^sup>+ = (<)"
   340 by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
   341 
   342 instance bit0 and bit1 :: (finite) wellorder
   343 proof -
   344   have "wf {(x :: 'a bit0, y). x < y}"
   345     by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
   346   thus "OFCLASS('a bit0, wellorder_class)"
   347     by(rule wf_wellorderI) intro_classes
   348 next
   349   have "wf {(x :: 'a bit1, y). x < y}"
   350     by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
   351   thus "OFCLASS('a bit1, wellorder_class)"
   352     by(rule wf_wellorderI) intro_classes
   353 qed
   354 
   355 subsection \<open>Code setup and type classes for code generation\<close>
   356 
   357 text \<open>Code setup for \<^typ>\<open>num0\<close> and \<^typ>\<open>num1\<close>\<close>
   358 
   359 definition Num0 :: num0 where "Num0 = Abs_num0 0"
   360 code_datatype Num0
   361 
   362 instantiation num0 :: equal begin
   363 definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
   364   where "equal_num0 = (=)"
   365 instance by intro_classes (simp add: equal_num0_def)
   366 end
   367 
   368 lemma equal_num0_code [code]:
   369   "equal_class.equal Num0 Num0 = True"
   370 by(rule equal_refl)
   371 
   372 code_datatype "1 :: num1"
   373 
   374 instantiation num1 :: equal begin
   375 definition equal_num1 :: "num1 \<Rightarrow> num1 \<Rightarrow> bool"
   376   where "equal_num1 = (=)"
   377 instance by intro_classes (simp add: equal_num1_def)
   378 end
   379 
   380 lemma equal_num1_code [code]:
   381   "equal_class.equal (1 :: num1) 1 = True"
   382 by(rule equal_refl)
   383 
   384 instantiation num1 :: enum begin
   385 definition "enum_class.enum = [1 :: num1]"
   386 definition "enum_class.enum_all P = P (1 :: num1)"
   387 definition "enum_class.enum_ex P = P (1 :: num1)"
   388 instance
   389   by intro_classes
   390      (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def)
   391 end
   392 
   393 instantiation num0 and num1 :: card_UNIV begin
   394 definition "finite_UNIV = Phantom(num0) False"
   395 definition "card_UNIV = Phantom(num0) 0"
   396 definition "finite_UNIV = Phantom(num1) True"
   397 definition "card_UNIV = Phantom(num1) 1"
   398 instance
   399   by intro_classes
   400      (simp_all add: finite_UNIV_num0_def card_UNIV_num0_def infinite_num0 finite_UNIV_num1_def card_UNIV_num1_def)
   401 end
   402 
   403 
   404 text \<open>Code setup for \<^typ>\<open>'a bit0\<close> and \<^typ>\<open>'a bit1\<close>\<close>
   405 
   406 declare
   407   bit0.Rep_inverse[code abstype]
   408   bit0.Rep_0[code abstract]
   409   bit0.Rep_1[code abstract]
   410 
   411 lemma Abs_bit0'_code [code abstract]:
   412   "Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))"
   413 by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse)
   414 
   415 lemma inj_on_Abs_bit0:
   416   "inj_on (Abs_bit0 :: int \<Rightarrow> 'a bit0) {0..<2 * int CARD('a :: finite)}"
   417 by(auto intro: inj_onI simp add: Abs_bit0_inject)
   418 
   419 declare
   420   bit1.Rep_inverse[code abstype]
   421   bit1.Rep_0[code abstract]
   422   bit1.Rep_1[code abstract]
   423 
   424 lemma Abs_bit1'_code [code abstract]:
   425   "Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))"
   426   by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
   427 
   428 lemma inj_on_Abs_bit1:
   429   "inj_on (Abs_bit1 :: int \<Rightarrow> 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}"
   430 by(auto intro: inj_onI simp add: Abs_bit1_inject)
   431 
   432 instantiation bit0 and bit1 :: (finite) equal begin
   433 
   434 definition "equal_class.equal x y \<longleftrightarrow> Rep_bit0 x = Rep_bit0 y"
   435 definition "equal_class.equal x y \<longleftrightarrow> Rep_bit1 x = Rep_bit1 y"
   436 
   437 instance
   438   by intro_classes (simp_all add: equal_bit0_def equal_bit1_def Rep_bit0_inject Rep_bit1_inject)
   439 
   440 end
   441 
   442 instantiation bit0 :: (finite) enum begin
   443 definition "(enum_class.enum :: 'a bit0 list) = map (Abs_bit0' \<circ> int) (upt 0 (CARD('a bit0)))"
   444 definition "enum_class.enum_all P = (\<forall>b :: 'a bit0 \<in> set enum_class.enum. P b)"
   445 definition "enum_class.enum_ex P = (\<exists>b :: 'a bit0 \<in> set enum_class.enum. P b)"
   446 
   447 instance proof
   448   show "distinct (enum_class.enum :: 'a bit0 list)"
   449     by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject)
   450 
   451   let ?Abs = "Abs_bit0 :: _ \<Rightarrow> 'a bit0"
   452   interpret type_definition Rep_bit0 ?Abs "{0..<2 * int CARD('a)}"
   453     by (fact type_definition_bit0)
   454   have "UNIV = ?Abs ` {0..<2 * int CARD('a)}"
   455     by (simp add: Abs_image)
   456   also have "\<dots> = ?Abs ` (int ` {0..<2 * CARD('a)})"
   457     by (simp add: image_int_atLeastLessThan)
   458   also have "\<dots> = (?Abs \<circ> int) ` {0..<2 * CARD('a)}"
   459     by (simp add: image_image cong: image_cong)
   460   also have "\<dots> = set enum_class.enum"
   461     by (simp add: enum_bit0_def Abs_bit0'_def cong: image_cong_simp)
   462   finally show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum" .
   463 
   464   fix P :: "'a bit0 \<Rightarrow> bool"
   465   show "enum_class.enum_all P = Ball UNIV P"
   466     and "enum_class.enum_ex P = Bex UNIV P"
   467     by(simp_all add: enum_all_bit0_def enum_ex_bit0_def univ_eq)
   468 qed
   469 
   470 end
   471 
   472 instantiation bit1 :: (finite) enum begin
   473 definition "(enum_class.enum :: 'a bit1 list) = map (Abs_bit1' \<circ> int) (upt 0 (CARD('a bit1)))"
   474 definition "enum_class.enum_all P = (\<forall>b :: 'a bit1 \<in> set enum_class.enum. P b)"
   475 definition "enum_class.enum_ex P = (\<exists>b :: 'a bit1 \<in> set enum_class.enum. P b)"
   476 
   477 instance
   478 proof(intro_classes)
   479   show "distinct (enum_class.enum :: 'a bit1 list)"
   480     by(simp only: Abs_bit1'_def zmod_int[symmetric] enum_bit1_def distinct_map Suc_eq_plus1 card_bit1 o_apply inj_on_def)
   481       (clarsimp simp add: Abs_bit1_inject)
   482 
   483   let ?Abs = "Abs_bit1 :: _ \<Rightarrow> 'a bit1"
   484   interpret type_definition Rep_bit1 ?Abs "{0..<1 + 2 * int CARD('a)}"
   485     by (fact type_definition_bit1)
   486   have "UNIV = ?Abs ` {0..<1 + 2 * int CARD('a)}"
   487     by (simp add: Abs_image)
   488   also have "\<dots> = ?Abs ` (int ` {0..<1 + 2 * CARD('a)})"
   489     by (simp add: image_int_atLeastLessThan)
   490   also have "\<dots> = (?Abs \<circ> int) ` {0..<1 + 2 * CARD('a)}"
   491     by (simp add: image_image cong: image_cong)
   492   finally show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
   493     by (simp only: enum_bit1_def set_map set_upt) (simp add: Abs_bit1'_def cong: image_cong_simp)
   494 
   495   fix P :: "'a bit1 \<Rightarrow> bool"
   496   show "enum_class.enum_all P = Ball UNIV P"
   497     and "enum_class.enum_ex P = Bex UNIV P"
   498     by(simp_all add: enum_all_bit1_def enum_ex_bit1_def univ_eq)
   499 qed
   500 
   501 end
   502 
   503 instantiation bit0 and bit1 :: (finite) finite_UNIV begin
   504 definition "finite_UNIV = Phantom('a bit0) True"
   505 definition "finite_UNIV = Phantom('a bit1) True"
   506 instance by intro_classes (simp_all add: finite_UNIV_bit0_def finite_UNIV_bit1_def)
   507 end
   508 
   509 instantiation bit0 and bit1 :: ("{finite,card_UNIV}") card_UNIV begin
   510 definition "card_UNIV = Phantom('a bit0) (2 * of_phantom (card_UNIV :: 'a card_UNIV))"
   511 definition "card_UNIV = Phantom('a bit1) (1 + 2 * of_phantom (card_UNIV :: 'a card_UNIV))"
   512 instance by intro_classes (simp_all add: card_UNIV_bit0_def card_UNIV_bit1_def card_UNIV)
   513 end
   514 
   515 subsection \<open>Syntax\<close>
   516 
   517 syntax
   518   "_NumeralType" :: "num_token => type"  ("_")
   519   "_NumeralType0" :: type ("0")
   520   "_NumeralType1" :: type ("1")
   521 
   522 translations
   523   (type) "1" == (type) "num1"
   524   (type) "0" == (type) "num0"
   525 
   526 parse_translation \<open>
   527   let
   528     fun mk_bintype n =
   529       let
   530         fun mk_bit 0 = Syntax.const \<^type_syntax>\<open>bit0\<close>
   531           | mk_bit 1 = Syntax.const \<^type_syntax>\<open>bit1\<close>;
   532         fun bin_of n =
   533           if n = 1 then Syntax.const \<^type_syntax>\<open>num1\<close>
   534           else if n = 0 then Syntax.const \<^type_syntax>\<open>num0\<close>
   535           else if n = ~1 then raise TERM ("negative type numeral", [])
   536           else
   537             let val (q, r) = Integer.div_mod n 2;
   538             in mk_bit r $ bin_of q end;
   539       in bin_of n end;
   540 
   541     fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
   542       | numeral_tr ts = raise TERM ("numeral_tr", ts);
   543 
   544   in [(\<^syntax_const>\<open>_NumeralType\<close>, K numeral_tr)] end
   545 \<close>
   546 
   547 print_translation \<open>
   548   let
   549     fun int_of [] = 0
   550       | int_of (b :: bs) = b + 2 * int_of bs;
   551 
   552     fun bin_of (Const (\<^type_syntax>\<open>num0\<close>, _)) = []
   553       | bin_of (Const (\<^type_syntax>\<open>num1\<close>, _)) = [1]
   554       | bin_of (Const (\<^type_syntax>\<open>bit0\<close>, _) $ bs) = 0 :: bin_of bs
   555       | bin_of (Const (\<^type_syntax>\<open>bit1\<close>, _) $ bs) = 1 :: bin_of bs
   556       | bin_of t = raise TERM ("bin_of", [t]);
   557 
   558     fun bit_tr' b [t] =
   559           let
   560             val rev_digs = b :: bin_of t handle TERM _ => raise Match
   561             val i = int_of rev_digs;
   562             val num = string_of_int (abs i);
   563           in
   564             Syntax.const \<^syntax_const>\<open>_NumeralType\<close> $ Syntax.free num
   565           end
   566       | bit_tr' b _ = raise Match;
   567   in
   568    [(\<^type_syntax>\<open>bit0\<close>, K (bit_tr' 0)),
   569     (\<^type_syntax>\<open>bit1\<close>, K (bit_tr' 1))]
   570   end
   571 \<close>
   572 
   573 subsection \<open>Examples\<close>
   574 
   575 lemma "CARD(0) = 0" by simp
   576 lemma "CARD(17) = 17" by simp
   577 lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
   578 
   579 end