src/HOL/Library/Numeral_Type.thy
author haftmann
Sat Dec 17 15:22:14 2016 +0100 (2016-12-17)
changeset 64593 50c715579715
parent 62348 9a5f43dac883
child 66886 960509bfd47e
permissions -rw-r--r--
reoriented congruence rules in non-explosive direction
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
apply (simp add: mod_pos_pos_trivial)
huffman@29997
   129
done
huffman@29997
   130
huffman@29997
   131
lemmas Rep_simps =
huffman@29997
   132
  Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
huffman@29997
   133
huffman@29997
   134
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
huffman@29997
   135
apply (intro_classes, unfold definitions)
haftmann@64593
   136
apply (simp_all add: Rep_simps mod_simps field_simps)
huffman@29997
   137
done
huffman@29997
   138
huffman@29997
   139
end
huffman@29997
   140
wenzelm@46868
   141
locale mod_ring = mod_type n Rep Abs
wenzelm@46868
   142
  for n :: int
huffman@47108
   143
  and Rep :: "'a::{comm_ring_1} \<Rightarrow> int"
huffman@47108
   144
  and Abs :: "int \<Rightarrow> 'a::{comm_ring_1}"
huffman@29997
   145
begin
huffman@29997
   146
huffman@29997
   147
lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
huffman@29997
   148
apply (induct k)
huffman@29997
   149
apply (simp add: zero_def)
haftmann@64593
   150
apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
huffman@29997
   151
done
huffman@29997
   152
huffman@29997
   153
lemma of_int_eq: "of_int z = Abs (z mod n)"
huffman@29997
   154
apply (cases z rule: int_diff_cases)
haftmann@64593
   155
apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
huffman@29997
   156
done
huffman@29997
   157
huffman@47108
   158
lemma Rep_numeral:
huffman@47108
   159
  "Rep (numeral w) = numeral w mod n"
huffman@47108
   160
using of_int_eq [of "numeral w"]
huffman@47108
   161
by (simp add: Rep_inject_sym Rep_Abs_mod)
huffman@29997
   162
huffman@47108
   163
lemma iszero_numeral:
huffman@47108
   164
  "iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0"
huffman@47108
   165
by (simp add: Rep_inject_sym Rep_numeral Rep_0 iszero_def)
huffman@29997
   166
huffman@29997
   167
lemma cases:
huffman@29997
   168
  assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
huffman@29997
   169
  shows "P"
huffman@29997
   170
apply (cases x rule: type_definition.Abs_cases [OF type])
huffman@29997
   171
apply (rule_tac z="y" in 1)
huffman@29997
   172
apply (simp_all add: of_int_eq mod_pos_pos_trivial)
huffman@29997
   173
done
huffman@29997
   174
huffman@29997
   175
lemma induct:
huffman@29997
   176
  "(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
huffman@29997
   177
by (cases x rule: cases) simp
huffman@29997
   178
huffman@29997
   179
end
huffman@29997
   180
huffman@29997
   181
wenzelm@60500
   182
subsection \<open>Ring class instances\<close>
huffman@29997
   183
wenzelm@60500
   184
text \<open>
wenzelm@61585
   185
  Unfortunately \<open>ring_1\<close> instance is not possible for
huffman@30032
   186
  @{typ num1}, since 0 and 1 are not distinct.
wenzelm@60500
   187
\<close>
huffman@30032
   188
huffman@47108
   189
instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}"
huffman@30032
   190
begin
huffman@30032
   191
huffman@30032
   192
lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
huffman@30032
   193
  by (induct x, induct y) simp
huffman@30032
   194
wenzelm@60679
   195
instance
wenzelm@60679
   196
  by standard (simp_all add: num1_eq_iff)
huffman@30032
   197
huffman@30032
   198
end
huffman@30032
   199
huffman@29997
   200
instantiation
haftmann@30960
   201
  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
huffman@29997
   202
begin
huffman@29997
   203
huffman@29997
   204
definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
huffman@29998
   205
  "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))"
huffman@29997
   206
huffman@29997
   207
definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where
huffman@29998
   208
  "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))"
huffman@29997
   209
huffman@29997
   210
definition "0 = Abs_bit0 0"
huffman@29997
   211
definition "1 = Abs_bit0 1"
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 - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
huffman@29997
   215
definition "- x = Abs_bit0' (- Rep_bit0 x)"
huffman@29997
   216
huffman@29997
   217
definition "0 = Abs_bit1 0"
huffman@29997
   218
definition "1 = Abs_bit1 1"
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 - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
huffman@29997
   222
definition "- x = Abs_bit1' (- Rep_bit1 x)"
huffman@29997
   223
huffman@29997
   224
instance ..
huffman@29997
   225
huffman@29997
   226
end
huffman@29997
   227
wenzelm@30729
   228
interpretation bit0:
huffman@29998
   229
  mod_type "int CARD('a::finite bit0)"
huffman@29997
   230
           "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
huffman@29997
   231
           "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
huffman@29997
   232
apply (rule mod_type.intro)
haftmann@62348
   233
apply (simp add: of_nat_mult type_definition_bit0)
huffman@30001
   234
apply (rule one_less_int_card)
huffman@29997
   235
apply (rule zero_bit0_def)
huffman@29997
   236
apply (rule one_bit0_def)
huffman@29997
   237
apply (rule plus_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   238
apply (rule times_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   239
apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   240
apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   241
done
huffman@29997
   242
wenzelm@30729
   243
interpretation bit1:
huffman@29998
   244
  mod_type "int CARD('a::finite bit1)"
huffman@29997
   245
           "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
huffman@29997
   246
           "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
huffman@29997
   247
apply (rule mod_type.intro)
haftmann@62348
   248
apply (simp add: of_nat_mult type_definition_bit1)
huffman@30001
   249
apply (rule one_less_int_card)
huffman@29997
   250
apply (rule zero_bit1_def)
huffman@29997
   251
apply (rule one_bit1_def)
huffman@29997
   252
apply (rule plus_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   253
apply (rule times_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   254
apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   255
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   256
done
huffman@29997
   257
haftmann@31021
   258
instance bit0 :: (finite) comm_ring_1
huffman@47108
   259
  by (rule bit0.comm_ring_1)
huffman@29997
   260
haftmann@31021
   261
instance bit1 :: (finite) comm_ring_1
huffman@47108
   262
  by (rule bit1.comm_ring_1)
huffman@29997
   263
wenzelm@30729
   264
interpretation bit0:
huffman@29998
   265
  mod_ring "int CARD('a::finite bit0)"
huffman@29997
   266
           "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
huffman@29997
   267
           "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
huffman@29997
   268
  ..
huffman@29997
   269
wenzelm@30729
   270
interpretation bit1:
huffman@29998
   271
  mod_ring "int CARD('a::finite bit1)"
huffman@29997
   272
           "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
huffman@29997
   273
           "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
huffman@29997
   274
  ..
huffman@29997
   275
wenzelm@60500
   276
text \<open>Set up cases, induction, and arithmetic\<close>
huffman@29997
   277
huffman@29999
   278
lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
huffman@29999
   279
lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
huffman@29997
   280
huffman@29999
   281
lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
huffman@29999
   282
lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
huffman@29997
   283
huffman@47108
   284
lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
huffman@47108
   285
lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
huffman@29997
   286
wenzelm@55142
   287
lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
wenzelm@55142
   288
lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
huffman@29997
   289
wenzelm@60500
   290
subsection \<open>Order instances\<close>
Andreas@51153
   291
Andreas@51153
   292
instantiation bit0 and bit1 :: (finite) linorder begin
Andreas@51153
   293
definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b"
Andreas@51153
   294
definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b"
Andreas@51153
   295
definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b"
Andreas@51153
   296
definition "a \<le> b \<longleftrightarrow> Rep_bit1 a \<le> Rep_bit1 b"
Andreas@51153
   297
Andreas@51153
   298
instance
Andreas@51153
   299
  by(intro_classes)
Andreas@51153
   300
    (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
   301
end
Andreas@51153
   302
Andreas@51288
   303
lemma (in preorder) tranclp_less: "op <\<^sup>+\<^sup>+ = op <"
Andreas@51288
   304
by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
Andreas@51288
   305
Andreas@51288
   306
instance bit0 and bit1 :: (finite) wellorder
Andreas@51288
   307
proof -
Andreas@51288
   308
  have "wf {(x :: 'a bit0, y). x < y}"
Andreas@51288
   309
    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
Andreas@51288
   310
  thus "OFCLASS('a bit0, wellorder_class)"
Andreas@51288
   311
    by(rule wf_wellorderI) intro_classes
Andreas@51288
   312
next
Andreas@51288
   313
  have "wf {(x :: 'a bit1, y). x < y}"
Andreas@51288
   314
    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
Andreas@51288
   315
  thus "OFCLASS('a bit1, wellorder_class)"
Andreas@51288
   316
    by(rule wf_wellorderI) intro_classes
Andreas@51288
   317
qed
Andreas@51153
   318
wenzelm@60500
   319
subsection \<open>Code setup and type classes for code generation\<close>
Andreas@51153
   320
wenzelm@60500
   321
text \<open>Code setup for @{typ num0} and @{typ num1}\<close>
Andreas@51153
   322
Andreas@51153
   323
definition Num0 :: num0 where "Num0 = Abs_num0 0"
Andreas@51153
   324
code_datatype Num0
Andreas@51153
   325
Andreas@51153
   326
instantiation num0 :: equal begin
wenzelm@52143
   327
definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
Andreas@51153
   328
  where "equal_num0 = op ="
Andreas@51153
   329
instance by intro_classes (simp add: equal_num0_def)
Andreas@51153
   330
end
Andreas@51153
   331
Andreas@51153
   332
lemma equal_num0_code [code]:
Andreas@51153
   333
  "equal_class.equal Num0 Num0 = True"
Andreas@51153
   334
by(rule equal_refl)
Andreas@51153
   335
Andreas@51153
   336
code_datatype "1 :: num1"
Andreas@51153
   337
Andreas@51153
   338
instantiation num1 :: equal begin
Andreas@51153
   339
definition equal_num1 :: "num1 \<Rightarrow> num1 \<Rightarrow> bool"
Andreas@51153
   340
  where "equal_num1 = op ="
Andreas@51153
   341
instance by intro_classes (simp add: equal_num1_def)
Andreas@51153
   342
end
Andreas@51153
   343
Andreas@51153
   344
lemma equal_num1_code [code]:
Andreas@51153
   345
  "equal_class.equal (1 :: num1) 1 = True"
Andreas@51153
   346
by(rule equal_refl)
Andreas@51153
   347
Andreas@51153
   348
instantiation num1 :: enum begin
Andreas@51153
   349
definition "enum_class.enum = [1 :: num1]"
Andreas@51153
   350
definition "enum_class.enum_all P = P (1 :: num1)"
Andreas@51153
   351
definition "enum_class.enum_ex P = P (1 :: num1)"
Andreas@51153
   352
instance
Andreas@51153
   353
  by intro_classes
wenzelm@52143
   354
     (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
Andreas@51153
   355
      (metis (full_types) num1_eq_iff)+)
Andreas@51153
   356
end
Andreas@51153
   357
Andreas@51153
   358
instantiation num0 and num1 :: card_UNIV begin
Andreas@51153
   359
definition "finite_UNIV = Phantom(num0) False"
Andreas@51153
   360
definition "card_UNIV = Phantom(num0) 0"
Andreas@51153
   361
definition "finite_UNIV = Phantom(num1) True"
Andreas@51153
   362
definition "card_UNIV = Phantom(num1) 1"
Andreas@51153
   363
instance
Andreas@51153
   364
  by intro_classes
Andreas@51153
   365
     (simp_all add: finite_UNIV_num0_def card_UNIV_num0_def infinite_num0 finite_UNIV_num1_def card_UNIV_num1_def)
Andreas@51153
   366
end
Andreas@51153
   367
Andreas@51153
   368
wenzelm@60500
   369
text \<open>Code setup for @{typ "'a bit0"} and @{typ "'a bit1"}\<close>
Andreas@51153
   370
Andreas@51153
   371
declare
Andreas@51153
   372
  bit0.Rep_inverse[code abstype]
Andreas@51153
   373
  bit0.Rep_0[code abstract]
Andreas@51153
   374
  bit0.Rep_1[code abstract]
Andreas@51153
   375
Andreas@51153
   376
lemma Abs_bit0'_code [code abstract]:
Andreas@51153
   377
  "Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))"
Andreas@51153
   378
by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse)
Andreas@51153
   379
Andreas@51153
   380
lemma inj_on_Abs_bit0:
Andreas@51153
   381
  "inj_on (Abs_bit0 :: int \<Rightarrow> 'a bit0) {0..<2 * int CARD('a :: finite)}"
Andreas@51153
   382
by(auto intro: inj_onI simp add: Abs_bit0_inject)
Andreas@51153
   383
Andreas@51153
   384
declare
Andreas@51153
   385
  bit1.Rep_inverse[code abstype]
Andreas@51153
   386
  bit1.Rep_0[code abstract]
Andreas@51153
   387
  bit1.Rep_1[code abstract]
Andreas@51153
   388
Andreas@51153
   389
lemma Abs_bit1'_code [code abstract]:
Andreas@51153
   390
  "Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))"
lp15@61649
   391
  by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
Andreas@51153
   392
Andreas@51153
   393
lemma inj_on_Abs_bit1:
Andreas@51153
   394
  "inj_on (Abs_bit1 :: int \<Rightarrow> 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}"
Andreas@51153
   395
by(auto intro: inj_onI simp add: Abs_bit1_inject)
Andreas@51153
   396
Andreas@51153
   397
instantiation bit0 and bit1 :: (finite) equal begin
Andreas@51153
   398
Andreas@51153
   399
definition "equal_class.equal x y \<longleftrightarrow> Rep_bit0 x = Rep_bit0 y"
Andreas@51153
   400
definition "equal_class.equal x y \<longleftrightarrow> Rep_bit1 x = Rep_bit1 y"
Andreas@51153
   401
Andreas@51153
   402
instance
Andreas@51153
   403
  by intro_classes (simp_all add: equal_bit0_def equal_bit1_def Rep_bit0_inject Rep_bit1_inject)
Andreas@51153
   404
Andreas@51153
   405
end
Andreas@51153
   406
Andreas@51153
   407
instantiation bit0 :: (finite) enum begin
Andreas@51153
   408
definition "(enum_class.enum :: 'a bit0 list) = map (Abs_bit0' \<circ> int) (upt 0 (CARD('a bit0)))"
Andreas@51153
   409
definition "enum_class.enum_all P = (\<forall>b :: 'a bit0 \<in> set enum_class.enum. P b)"
Andreas@51153
   410
definition "enum_class.enum_ex P = (\<exists>b :: 'a bit0 \<in> set enum_class.enum. P b)"
Andreas@51153
   411
Andreas@51153
   412
instance
Andreas@51153
   413
proof(intro_classes)
Andreas@51153
   414
  show "distinct (enum_class.enum :: 'a bit0 list)"
lp15@61649
   415
    by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial)
Andreas@51153
   416
Andreas@51153
   417
  show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
Andreas@51153
   418
    unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
haftmann@56154
   419
    by(simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
Andreas@51153
   420
      (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def mod_pos_pos_trivial)
Andreas@51153
   421
Andreas@51153
   422
  fix P :: "'a bit0 \<Rightarrow> bool"
Andreas@51153
   423
  show "enum_class.enum_all P = Ball UNIV P"
Andreas@51153
   424
    and "enum_class.enum_ex P = Bex UNIV P"
Andreas@51153
   425
    by(simp_all add: enum_all_bit0_def enum_ex_bit0_def univ_eq)
Andreas@51153
   426
qed
Andreas@51153
   427
Andreas@51153
   428
end
Andreas@51153
   429
Andreas@51153
   430
instantiation bit1 :: (finite) enum begin
Andreas@51153
   431
definition "(enum_class.enum :: 'a bit1 list) = map (Abs_bit1' \<circ> int) (upt 0 (CARD('a bit1)))"
Andreas@51153
   432
definition "enum_class.enum_all P = (\<forall>b :: 'a bit1 \<in> set enum_class.enum. P b)"
Andreas@51153
   433
definition "enum_class.enum_ex P = (\<exists>b :: 'a bit1 \<in> set enum_class.enum. P b)"
Andreas@51153
   434
Andreas@51153
   435
instance
Andreas@51153
   436
proof(intro_classes)
Andreas@51153
   437
  show "distinct (enum_class.enum :: 'a bit1 list)"
Andreas@51153
   438
    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
   439
      (clarsimp simp add: Abs_bit1_inject)
Andreas@51153
   440
Andreas@51153
   441
  show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
Andreas@51153
   442
    unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
haftmann@56154
   443
    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
Andreas@51153
   444
      (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def mod_pos_pos_trivial)
Andreas@51153
   445
Andreas@51153
   446
  fix P :: "'a bit1 \<Rightarrow> bool"
Andreas@51153
   447
  show "enum_class.enum_all P = Ball UNIV P"
Andreas@51153
   448
    and "enum_class.enum_ex P = Bex UNIV P"
Andreas@51153
   449
    by(simp_all add: enum_all_bit1_def enum_ex_bit1_def univ_eq)
Andreas@51153
   450
qed
Andreas@51153
   451
Andreas@51153
   452
end
Andreas@51153
   453
Andreas@51153
   454
instantiation bit0 and bit1 :: (finite) finite_UNIV begin
Andreas@51153
   455
definition "finite_UNIV = Phantom('a bit0) True"
Andreas@51153
   456
definition "finite_UNIV = Phantom('a bit1) True"
Andreas@51153
   457
instance by intro_classes (simp_all add: finite_UNIV_bit0_def finite_UNIV_bit1_def)
Andreas@51153
   458
end
Andreas@51153
   459
Andreas@51153
   460
instantiation bit0 and bit1 :: ("{finite,card_UNIV}") card_UNIV begin
Andreas@51153
   461
definition "card_UNIV = Phantom('a bit0) (2 * of_phantom (card_UNIV :: 'a card_UNIV))"
Andreas@51175
   462
definition "card_UNIV = Phantom('a bit1) (1 + 2 * of_phantom (card_UNIV :: 'a card_UNIV))"
Andreas@51153
   463
instance by intro_classes (simp_all add: card_UNIV_bit0_def card_UNIV_bit1_def card_UNIV)
Andreas@51153
   464
end
Andreas@51153
   465
wenzelm@60500
   466
subsection \<open>Syntax\<close>
kleing@24332
   467
kleing@24332
   468
syntax
wenzelm@46236
   469
  "_NumeralType" :: "num_token => type"  ("_")
kleing@24332
   470
  "_NumeralType0" :: type ("0")
kleing@24332
   471
  "_NumeralType1" :: type ("1")
kleing@24332
   472
kleing@24332
   473
translations
wenzelm@35362
   474
  (type) "1" == (type) "num1"
wenzelm@35362
   475
  (type) "0" == (type) "num0"
kleing@24332
   476
wenzelm@60500
   477
parse_translation \<open>
wenzelm@52143
   478
  let
wenzelm@52143
   479
    fun mk_bintype n =
wenzelm@52143
   480
      let
wenzelm@52143
   481
        fun mk_bit 0 = Syntax.const @{type_syntax bit0}
wenzelm@52143
   482
          | mk_bit 1 = Syntax.const @{type_syntax bit1};
wenzelm@52143
   483
        fun bin_of n =
wenzelm@52143
   484
          if n = 1 then Syntax.const @{type_syntax num1}
wenzelm@52143
   485
          else if n = 0 then Syntax.const @{type_syntax num0}
wenzelm@52143
   486
          else if n = ~1 then raise TERM ("negative type numeral", [])
wenzelm@52143
   487
          else
wenzelm@52143
   488
            let val (q, r) = Integer.div_mod n 2;
wenzelm@52143
   489
            in mk_bit r $ bin_of q end;
wenzelm@52143
   490
      in bin_of n end;
kleing@24332
   491
wenzelm@52143
   492
    fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
wenzelm@52143
   493
      | numeral_tr ts = raise TERM ("numeral_tr", ts);
kleing@24332
   494
wenzelm@52143
   495
  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
wenzelm@60500
   496
\<close>
kleing@24332
   497
wenzelm@60500
   498
print_translation \<open>
wenzelm@52143
   499
  let
wenzelm@52143
   500
    fun int_of [] = 0
wenzelm@52143
   501
      | int_of (b :: bs) = b + 2 * int_of bs;
kleing@24332
   502
wenzelm@52143
   503
    fun bin_of (Const (@{type_syntax num0}, _)) = []
wenzelm@52143
   504
      | bin_of (Const (@{type_syntax num1}, _)) = [1]
wenzelm@52143
   505
      | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
wenzelm@52143
   506
      | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
wenzelm@52143
   507
      | bin_of t = raise TERM ("bin_of", [t]);
kleing@24332
   508
wenzelm@52143
   509
    fun bit_tr' b [t] =
wenzelm@52143
   510
          let
wenzelm@52143
   511
            val rev_digs = b :: bin_of t handle TERM _ => raise Match
wenzelm@52143
   512
            val i = int_of rev_digs;
wenzelm@52143
   513
            val num = string_of_int (abs i);
wenzelm@52143
   514
          in
wenzelm@52143
   515
            Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
wenzelm@52143
   516
          end
wenzelm@52143
   517
      | bit_tr' b _ = raise Match;
wenzelm@52143
   518
  in
wenzelm@52143
   519
   [(@{type_syntax bit0}, K (bit_tr' 0)),
wenzelm@52147
   520
    (@{type_syntax bit1}, K (bit_tr' 1))]
wenzelm@52147
   521
  end;
wenzelm@60500
   522
\<close>
kleing@24332
   523
wenzelm@60500
   524
subsection \<open>Examples\<close>
kleing@24332
   525
kleing@24332
   526
lemma "CARD(0) = 0" by simp
kleing@24332
   527
lemma "CARD(17) = 17" by simp
huffman@29997
   528
lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
huffman@28920
   529
kleing@24332
   530
end