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