src/HOL/Library/Numeral_Type.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 37653 847e95ca9b0a
child 46236 ae79f2978a67
permissions -rw-r--r--
Quotient_Info stores only relation maps
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
huffman@24406
    13
typedef (open) num0 = "UNIV :: nat set" ..
kleing@24332
    14
typedef (open) num1 = "UNIV :: unit set" ..
huffman@29997
    15
huffman@29997
    16
typedef (open) '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
huffman@29997
    22
typedef (open) '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@30001
    34
  by (simp only: card_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
wenzelm@25378
    69
haftmann@37653
    70
subsection {* Locales for for modular arithmetic subtypes *}
huffman@29997
    71
huffman@29997
    72
locale mod_type =
huffman@29997
    73
  fixes n :: int
haftmann@30960
    74
  and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
haftmann@30960
    75
  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
huffman@29997
    76
  assumes type: "type_definition Rep Abs {0..<n}"
huffman@29997
    77
  and size1: "1 < n"
huffman@29997
    78
  and zero_def: "0 = Abs 0"
huffman@29997
    79
  and one_def:  "1 = Abs 1"
huffman@29997
    80
  and add_def:  "x + y = Abs ((Rep x + Rep y) mod n)"
huffman@29997
    81
  and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
huffman@29997
    82
  and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
huffman@29997
    83
  and minus_def: "- x = Abs ((- Rep x) mod n)"
huffman@29997
    84
begin
huffman@29997
    85
huffman@29997
    86
lemma size0: "0 < n"
wenzelm@35362
    87
using size1 by simp
huffman@29997
    88
huffman@29997
    89
lemmas definitions =
haftmann@30960
    90
  zero_def one_def add_def mult_def minus_def diff_def
huffman@29997
    91
huffman@29997
    92
lemma Rep_less_n: "Rep x < n"
huffman@29997
    93
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
huffman@29997
    94
huffman@29997
    95
lemma Rep_le_n: "Rep x \<le> n"
huffman@29997
    96
by (rule Rep_less_n [THEN order_less_imp_le])
huffman@29997
    97
huffman@29997
    98
lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
huffman@29997
    99
by (rule type_definition.Rep_inject [OF type, symmetric])
huffman@29997
   100
huffman@29997
   101
lemma Rep_inverse: "Abs (Rep x) = x"
huffman@29997
   102
by (rule type_definition.Rep_inverse [OF type])
huffman@29997
   103
huffman@29997
   104
lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
huffman@29997
   105
by (rule type_definition.Abs_inverse [OF type])
huffman@29997
   106
huffman@29997
   107
lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
haftmann@33361
   108
by (simp add: Abs_inverse pos_mod_conj [OF size0])
huffman@29997
   109
huffman@29997
   110
lemma Rep_Abs_0: "Rep (Abs 0) = 0"
huffman@29997
   111
by (simp add: Abs_inverse size0)
huffman@29997
   112
huffman@29997
   113
lemma Rep_0: "Rep 0 = 0"
huffman@29997
   114
by (simp add: zero_def Rep_Abs_0)
huffman@29997
   115
huffman@29997
   116
lemma Rep_Abs_1: "Rep (Abs 1) = 1"
huffman@29997
   117
by (simp add: Abs_inverse size1)
huffman@29997
   118
huffman@29997
   119
lemma Rep_1: "Rep 1 = 1"
huffman@29997
   120
by (simp add: one_def Rep_Abs_1)
huffman@29997
   121
huffman@29997
   122
lemma Rep_mod: "Rep x mod n = Rep x"
huffman@29997
   123
apply (rule_tac x=x in type_definition.Abs_cases [OF type])
huffman@29997
   124
apply (simp add: type_definition.Abs_inverse [OF type])
huffman@29997
   125
apply (simp add: mod_pos_pos_trivial)
huffman@29997
   126
done
huffman@29997
   127
huffman@29997
   128
lemmas Rep_simps =
huffman@29997
   129
  Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
huffman@29997
   130
huffman@29997
   131
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
huffman@29997
   132
apply (intro_classes, unfold definitions)
haftmann@36350
   133
apply (simp_all add: Rep_simps zmod_simps field_simps)
huffman@29997
   134
done
huffman@29997
   135
huffman@29997
   136
end
huffman@29997
   137
huffman@29997
   138
locale mod_ring = mod_type +
huffman@29997
   139
  constrains n :: int
haftmann@30960
   140
  and Rep :: "'a::{number_ring} \<Rightarrow> int"
haftmann@30960
   141
  and Abs :: "int \<Rightarrow> 'a::{number_ring}"
huffman@29997
   142
begin
huffman@29997
   143
huffman@29997
   144
lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
huffman@29997
   145
apply (induct k)
huffman@29997
   146
apply (simp add: zero_def)
huffman@29997
   147
apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
huffman@29997
   148
done
huffman@29997
   149
huffman@29997
   150
lemma of_int_eq: "of_int z = Abs (z mod n)"
huffman@29997
   151
apply (cases z rule: int_diff_cases)
huffman@29997
   152
apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
huffman@29997
   153
done
huffman@29997
   154
huffman@29997
   155
lemma Rep_number_of:
huffman@29997
   156
  "Rep (number_of w) = number_of w mod n"
huffman@29997
   157
by (simp add: number_of_eq of_int_eq Rep_Abs_mod)
huffman@29997
   158
huffman@29997
   159
lemma iszero_number_of:
huffman@29997
   160
  "iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0"
huffman@29997
   161
by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_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@29997
   178
subsection {* Number ring instances *}
huffman@29997
   179
huffman@30032
   180
text {*
huffman@30032
   181
  Unfortunately a number ring instance is not possible for
huffman@30032
   182
  @{typ num1}, since 0 and 1 are not distinct.
huffman@30032
   183
*}
huffman@30032
   184
haftmann@30960
   185
instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
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
haftmann@31021
   255
  by (rule bit0.comm_ring_1)+
huffman@29997
   256
haftmann@31021
   257
instance bit1 :: (finite) comm_ring_1
haftmann@31021
   258
  by (rule bit1.comm_ring_1)+
huffman@29997
   259
huffman@29997
   260
instantiation bit0 and bit1 :: (finite) number_ring
huffman@29997
   261
begin
huffman@29997
   262
huffman@29997
   263
definition "(number_of w :: _ bit0) = of_int w"
huffman@29997
   264
huffman@29997
   265
definition "(number_of w :: _ bit1) = of_int w"
huffman@29997
   266
huffman@29997
   267
instance proof
huffman@29997
   268
qed (rule number_of_bit0_def number_of_bit1_def)+
huffman@29997
   269
huffman@29997
   270
end
huffman@29997
   271
wenzelm@30729
   272
interpretation bit0:
huffman@29998
   273
  mod_ring "int CARD('a::finite bit0)"
huffman@29997
   274
           "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
huffman@29997
   275
           "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
huffman@29997
   276
  ..
huffman@29997
   277
wenzelm@30729
   278
interpretation bit1:
huffman@29998
   279
  mod_ring "int CARD('a::finite bit1)"
huffman@29997
   280
           "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
huffman@29997
   281
           "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
huffman@29997
   282
  ..
huffman@29997
   283
huffman@29997
   284
text {* Set up cases, induction, and arithmetic *}
huffman@29997
   285
huffman@29999
   286
lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
huffman@29999
   287
lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
huffman@29997
   288
huffman@29999
   289
lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
huffman@29999
   290
lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
huffman@29997
   291
huffman@29997
   292
lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
huffman@29997
   293
lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
huffman@29997
   294
huffman@29997
   295
kleing@24332
   296
subsection {* Syntax *}
kleing@24332
   297
kleing@24332
   298
syntax
kleing@24332
   299
  "_NumeralType" :: "num_const => type"  ("_")
kleing@24332
   300
  "_NumeralType0" :: type ("0")
kleing@24332
   301
  "_NumeralType1" :: type ("1")
kleing@24332
   302
kleing@24332
   303
translations
wenzelm@35362
   304
  (type) "1" == (type) "num1"
wenzelm@35362
   305
  (type) "0" == (type) "num0"
kleing@24332
   306
kleing@24332
   307
parse_translation {*
kleing@24332
   308
let
kleing@24332
   309
fun mk_bintype n =
kleing@24332
   310
  let
wenzelm@35362
   311
    fun mk_bit 0 = Syntax.const @{type_syntax bit0}
wenzelm@35362
   312
      | mk_bit 1 = Syntax.const @{type_syntax bit1};
kleing@24332
   313
    fun bin_of n =
wenzelm@35362
   314
      if n = 1 then Syntax.const @{type_syntax num1}
wenzelm@35362
   315
      else if n = 0 then Syntax.const @{type_syntax num0}
kleing@24332
   316
      else if n = ~1 then raise TERM ("negative type numeral", [])
kleing@24332
   317
      else
wenzelm@24630
   318
        let val (q, r) = Integer.div_mod n 2;
kleing@24332
   319
        in mk_bit r $ bin_of q end;
kleing@24332
   320
  in bin_of n end;
kleing@24332
   321
kleing@24332
   322
fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
wenzelm@33035
   323
      mk_bintype (the (Int.fromString str))
kleing@24332
   324
  | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
kleing@24332
   325
wenzelm@35115
   326
in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
kleing@24332
   327
*}
kleing@24332
   328
kleing@24332
   329
print_translation {*
kleing@24332
   330
let
kleing@24332
   331
fun int_of [] = 0
wenzelm@24630
   332
  | int_of (b :: bs) = b + 2 * int_of bs;
kleing@24332
   333
wenzelm@35362
   334
fun bin_of (Const (@{type_syntax num0}, _)) = []
wenzelm@35362
   335
  | bin_of (Const (@{type_syntax num1}, _)) = [1]
wenzelm@35362
   336
  | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
wenzelm@35362
   337
  | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
wenzelm@35362
   338
  | bin_of t = raise TERM ("bin_of", [t]);
kleing@24332
   339
kleing@24332
   340
fun bit_tr' b [t] =
wenzelm@35362
   341
      let
wenzelm@35362
   342
        val rev_digs = b :: bin_of t handle TERM _ => raise Match
wenzelm@35362
   343
        val i = int_of rev_digs;
wenzelm@35362
   344
        val num = string_of_int (abs i);
wenzelm@35362
   345
      in
wenzelm@35362
   346
        Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
wenzelm@35362
   347
      end
kleing@24332
   348
  | bit_tr' b _ = raise Match;
wenzelm@35362
   349
in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
kleing@24332
   350
*}
kleing@24332
   351
kleing@24332
   352
subsection {* Examples *}
kleing@24332
   353
kleing@24332
   354
lemma "CARD(0) = 0" by simp
kleing@24332
   355
lemma "CARD(17) = 17" by simp
huffman@29997
   356
lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
huffman@28920
   357
kleing@24332
   358
end