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