src/HOL/Library/Numeral_Type.thy
author huffman
Thu Feb 19 17:13:35 2009 -0800 (2009-02-19)
changeset 29999 da85a244e328
parent 29998 19e1ef628b25
child 30001 dd27e16677b2
permissions -rw-r--r--
fix case_names
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@27487
     8
imports Plain "~~/src/HOL/Presburger"
kleing@24332
     9
begin
kleing@24332
    10
kleing@24332
    11
subsection {* Preliminary lemmas *}
kleing@24332
    12
(* These should be moved elsewhere *)
kleing@24332
    13
kleing@24332
    14
lemma (in type_definition) univ:
kleing@24332
    15
  "UNIV = Abs ` A"
kleing@24332
    16
proof
kleing@24332
    17
  show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
kleing@24332
    18
  show "UNIV \<subseteq> Abs ` A"
kleing@24332
    19
  proof
kleing@24332
    20
    fix x :: 'b
kleing@24332
    21
    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
kleing@24332
    22
    moreover have "Rep x \<in> A" by (rule Rep)
kleing@24332
    23
    ultimately show "x \<in> Abs ` A" by (rule image_eqI)
kleing@24332
    24
  qed
kleing@24332
    25
qed
kleing@24332
    26
kleing@24332
    27
lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
kleing@24332
    28
  by (simp add: univ card_image inj_on_def Abs_inject)
kleing@24332
    29
kleing@24332
    30
kleing@24332
    31
subsection {* Cardinalities of types *}
kleing@24332
    32
kleing@24332
    33
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
kleing@24332
    34
huffman@28920
    35
translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
kleing@24332
    36
huffman@24407
    37
typed_print_translation {*
huffman@24407
    38
let
huffman@28920
    39
  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
huffman@24407
    40
    Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
huffman@28920
    41
in [(@{const_syntax card}, card_univ_tr')]
huffman@24407
    42
end
huffman@24407
    43
*}
huffman@24407
    44
kleing@24332
    45
lemma card_unit: "CARD(unit) = 1"
haftmann@26153
    46
  unfolding UNIV_unit by simp
kleing@24332
    47
kleing@24332
    48
lemma card_bool: "CARD(bool) = 2"
haftmann@26153
    49
  unfolding UNIV_bool by simp
kleing@24332
    50
kleing@24332
    51
lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
haftmann@26153
    52
  unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
kleing@24332
    53
kleing@24332
    54
lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
haftmann@26153
    55
  unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
kleing@24332
    56
kleing@24332
    57
lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
haftmann@26153
    58
  unfolding insert_None_conv_UNIV [symmetric]
kleing@24332
    59
  apply (subgoal_tac "(None::'a option) \<notin> range Some")
huffman@29997
    60
  apply (simp add: card_image)
kleing@24332
    61
  apply fast
kleing@24332
    62
  done
kleing@24332
    63
kleing@24332
    64
lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
haftmann@26153
    65
  unfolding Pow_UNIV [symmetric]
kleing@24332
    66
  by (simp only: card_Pow finite numeral_2_eq_2)
kleing@24332
    67
huffman@29997
    68
lemma card_finite_pos [simp]: "0 < CARD('a::finite)"
huffman@29997
    69
  unfolding neq0_conv [symmetric] by simp
huffman@29997
    70
wenzelm@25378
    71
kleing@24332
    72
subsection {* Numeral Types *}
kleing@24332
    73
huffman@24406
    74
typedef (open) num0 = "UNIV :: nat set" ..
kleing@24332
    75
typedef (open) num1 = "UNIV :: unit set" ..
huffman@29997
    76
huffman@29997
    77
typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
huffman@29997
    78
proof
huffman@29997
    79
  show "0 \<in> {0 ..< 2 * int CARD('a)}"
huffman@29997
    80
    by simp
huffman@29997
    81
qed
huffman@29997
    82
huffman@29997
    83
typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
huffman@29997
    84
proof
huffman@29997
    85
  show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}"
huffman@29997
    86
    by simp
huffman@29997
    87
qed
kleing@24332
    88
kleing@24332
    89
instance num1 :: finite
kleing@24332
    90
proof
kleing@24332
    91
  show "finite (UNIV::num1 set)"
kleing@24332
    92
    unfolding type_definition.univ [OF type_definition_num1]
kleing@24332
    93
    using finite by (rule finite_imageI)
kleing@24332
    94
qed
kleing@24332
    95
kleing@24332
    96
instance bit0 :: (finite) finite
kleing@24332
    97
proof
kleing@24332
    98
  show "finite (UNIV::'a bit0 set)"
kleing@24332
    99
    unfolding type_definition.univ [OF type_definition_bit0]
huffman@29997
   100
    by simp
kleing@24332
   101
qed
kleing@24332
   102
kleing@24332
   103
instance bit1 :: (finite) finite
kleing@24332
   104
proof
kleing@24332
   105
  show "finite (UNIV::'a bit1 set)"
kleing@24332
   106
    unfolding type_definition.univ [OF type_definition_bit1]
huffman@29997
   107
    by simp
kleing@24332
   108
qed
kleing@24332
   109
kleing@24332
   110
lemma card_num1: "CARD(num1) = 1"
kleing@24332
   111
  unfolding type_definition.card [OF type_definition_num1]
kleing@24332
   112
  by (simp only: card_unit)
kleing@24332
   113
kleing@24332
   114
lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)"
kleing@24332
   115
  unfolding type_definition.card [OF type_definition_bit0]
huffman@29997
   116
  by simp
kleing@24332
   117
kleing@24332
   118
lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))"
kleing@24332
   119
  unfolding type_definition.card [OF type_definition_bit1]
huffman@29997
   120
  by simp
kleing@24332
   121
huffman@24406
   122
lemma card_num0: "CARD (num0) = 0"
chaieb@26506
   123
  by (simp add: infinite_UNIV_nat card_eq_0_iff type_definition.card [OF type_definition_num0])
kleing@24332
   124
kleing@24332
   125
lemmas card_univ_simps [simp] =
kleing@24332
   126
  card_unit
kleing@24332
   127
  card_bool
kleing@24332
   128
  card_prod
kleing@24332
   129
  card_sum
kleing@24332
   130
  card_option
kleing@24332
   131
  card_set
kleing@24332
   132
  card_num1
kleing@24332
   133
  card_bit0
kleing@24332
   134
  card_bit1
huffman@24406
   135
  card_num0
kleing@24332
   136
wenzelm@25378
   137
huffman@29997
   138
subsection {* Locale for modular arithmetic subtypes *}
huffman@29997
   139
huffman@29997
   140
locale mod_type =
huffman@29997
   141
  fixes n :: int
huffman@29997
   142
  and Rep :: "'a::{zero,one,plus,times,uminus,minus,power} \<Rightarrow> int"
huffman@29997
   143
  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus,power}"
huffman@29997
   144
  assumes type: "type_definition Rep Abs {0..<n}"
huffman@29997
   145
  and size1: "1 < n"
huffman@29997
   146
  and zero_def: "0 = Abs 0"
huffman@29997
   147
  and one_def:  "1 = Abs 1"
huffman@29997
   148
  and add_def:  "x + y = Abs ((Rep x + Rep y) mod n)"
huffman@29997
   149
  and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
huffman@29997
   150
  and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
huffman@29997
   151
  and minus_def: "- x = Abs ((- Rep x) mod n)"
huffman@29997
   152
  and power_def: "x ^ k = Abs (Rep x ^ k mod n)"
huffman@29997
   153
begin
huffman@29997
   154
huffman@29997
   155
lemma size0: "0 < n"
huffman@29997
   156
by (cut_tac size1, simp)
huffman@29997
   157
huffman@29997
   158
lemmas definitions =
huffman@29997
   159
  zero_def one_def add_def mult_def minus_def diff_def power_def
huffman@29997
   160
huffman@29997
   161
lemma Rep_less_n: "Rep x < n"
huffman@29997
   162
by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
huffman@29997
   163
huffman@29997
   164
lemma Rep_le_n: "Rep x \<le> n"
huffman@29997
   165
by (rule Rep_less_n [THEN order_less_imp_le])
huffman@29997
   166
huffman@29997
   167
lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
huffman@29997
   168
by (rule type_definition.Rep_inject [OF type, symmetric])
huffman@29997
   169
huffman@29997
   170
lemma Rep_inverse: "Abs (Rep x) = x"
huffman@29997
   171
by (rule type_definition.Rep_inverse [OF type])
huffman@29997
   172
huffman@29997
   173
lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
huffman@29997
   174
by (rule type_definition.Abs_inverse [OF type])
huffman@29997
   175
huffman@29997
   176
lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
huffman@29997
   177
by (simp add: Abs_inverse IntDiv.pos_mod_conj [OF size0])
huffman@29997
   178
huffman@29997
   179
lemma Rep_Abs_0: "Rep (Abs 0) = 0"
huffman@29997
   180
by (simp add: Abs_inverse size0)
huffman@29997
   181
huffman@29997
   182
lemma Rep_0: "Rep 0 = 0"
huffman@29997
   183
by (simp add: zero_def Rep_Abs_0)
huffman@29997
   184
huffman@29997
   185
lemma Rep_Abs_1: "Rep (Abs 1) = 1"
huffman@29997
   186
by (simp add: Abs_inverse size1)
huffman@29997
   187
huffman@29997
   188
lemma Rep_1: "Rep 1 = 1"
huffman@29997
   189
by (simp add: one_def Rep_Abs_1)
huffman@29997
   190
huffman@29997
   191
lemma Rep_mod: "Rep x mod n = Rep x"
huffman@29997
   192
apply (rule_tac x=x in type_definition.Abs_cases [OF type])
huffman@29997
   193
apply (simp add: type_definition.Abs_inverse [OF type])
huffman@29997
   194
apply (simp add: mod_pos_pos_trivial)
huffman@29997
   195
done
huffman@29997
   196
huffman@29997
   197
lemmas Rep_simps =
huffman@29997
   198
  Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
huffman@29997
   199
huffman@29997
   200
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
huffman@29997
   201
apply (intro_classes, unfold definitions)
huffman@29997
   202
apply (simp_all add: Rep_simps zmod_simps ring_simps)
huffman@29997
   203
done
huffman@29997
   204
huffman@29997
   205
lemma recpower: "OFCLASS('a, recpower_class)"
huffman@29997
   206
apply (intro_classes, unfold definitions)
huffman@29997
   207
apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
huffman@29997
   208
                     mod_pos_pos_trivial size1)
huffman@29997
   209
done
huffman@29997
   210
huffman@29997
   211
end
huffman@29997
   212
huffman@29997
   213
locale mod_ring = mod_type +
huffman@29997
   214
  constrains n :: int
huffman@29997
   215
  and Rep :: "'a::{number_ring,power} \<Rightarrow> int"
huffman@29997
   216
  and Abs :: "int \<Rightarrow> 'a::{number_ring,power}"
huffman@29997
   217
begin
huffman@29997
   218
huffman@29997
   219
lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
huffman@29997
   220
apply (induct k)
huffman@29997
   221
apply (simp add: zero_def)
huffman@29997
   222
apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
huffman@29997
   223
done
huffman@29997
   224
huffman@29997
   225
lemma of_int_eq: "of_int z = Abs (z mod n)"
huffman@29997
   226
apply (cases z rule: int_diff_cases)
huffman@29997
   227
apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
huffman@29997
   228
done
huffman@29997
   229
huffman@29997
   230
lemma Rep_number_of:
huffman@29997
   231
  "Rep (number_of w) = number_of w mod n"
huffman@29997
   232
by (simp add: number_of_eq of_int_eq Rep_Abs_mod)
huffman@29997
   233
huffman@29997
   234
lemma iszero_number_of:
huffman@29997
   235
  "iszero (number_of w::'a) \<longleftrightarrow> number_of w mod n = 0"
huffman@29997
   236
by (simp add: Rep_simps number_of_eq of_int_eq iszero_def zero_def)
huffman@29997
   237
huffman@29997
   238
lemma cases:
huffman@29997
   239
  assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
huffman@29997
   240
  shows "P"
huffman@29997
   241
apply (cases x rule: type_definition.Abs_cases [OF type])
huffman@29997
   242
apply (rule_tac z="y" in 1)
huffman@29997
   243
apply (simp_all add: of_int_eq mod_pos_pos_trivial)
huffman@29997
   244
done
huffman@29997
   245
huffman@29997
   246
lemma induct:
huffman@29997
   247
  "(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
huffman@29997
   248
by (cases x rule: cases) simp
huffman@29997
   249
huffman@29997
   250
end
huffman@29997
   251
huffman@29997
   252
huffman@29997
   253
subsection {* Number ring instances *}
huffman@29997
   254
huffman@29997
   255
instantiation
huffman@29997
   256
  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
huffman@29997
   257
begin
huffman@29997
   258
huffman@29997
   259
definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
huffman@29998
   260
  "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))"
huffman@29997
   261
huffman@29997
   262
definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where
huffman@29998
   263
  "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))"
huffman@29997
   264
huffman@29997
   265
definition "0 = Abs_bit0 0"
huffman@29997
   266
definition "1 = Abs_bit0 1"
huffman@29997
   267
definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)"
huffman@29997
   268
definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
huffman@29997
   269
definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
huffman@29997
   270
definition "- x = Abs_bit0' (- Rep_bit0 x)"
huffman@29997
   271
definition "x ^ k = Abs_bit0' (Rep_bit0 x ^ k)"
huffman@29997
   272
huffman@29997
   273
definition "0 = Abs_bit1 0"
huffman@29997
   274
definition "1 = Abs_bit1 1"
huffman@29997
   275
definition "x + y = Abs_bit1' (Rep_bit1 x + Rep_bit1 y)"
huffman@29997
   276
definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
huffman@29997
   277
definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
huffman@29997
   278
definition "- x = Abs_bit1' (- Rep_bit1 x)"
huffman@29997
   279
definition "x ^ k = Abs_bit1' (Rep_bit1 x ^ k)"
huffman@29997
   280
huffman@29997
   281
instance ..
huffman@29997
   282
huffman@29997
   283
end
huffman@29997
   284
huffman@29997
   285
interpretation bit0!:
huffman@29998
   286
  mod_type "int CARD('a::finite bit0)"
huffman@29997
   287
           "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
huffman@29997
   288
           "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
huffman@29997
   289
apply (rule mod_type.intro)
huffman@29998
   290
apply (simp add: int_mult type_definition_bit0)
huffman@29998
   291
apply simp
huffman@29997
   292
using card_finite_pos [where ?'a='a] apply arith
huffman@29997
   293
apply (rule zero_bit0_def)
huffman@29997
   294
apply (rule one_bit0_def)
huffman@29997
   295
apply (rule plus_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   296
apply (rule times_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   297
apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   298
apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   299
apply (rule power_bit0_def [unfolded Abs_bit0'_def])
huffman@29997
   300
done
huffman@29997
   301
huffman@29997
   302
interpretation bit1!:
huffman@29998
   303
  mod_type "int CARD('a::finite bit1)"
huffman@29997
   304
           "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
huffman@29997
   305
           "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
huffman@29997
   306
apply (rule mod_type.intro)
huffman@29998
   307
apply (simp add: int_mult type_definition_bit1)
huffman@29997
   308
apply simp
huffman@29997
   309
apply (rule zero_bit1_def)
huffman@29997
   310
apply (rule one_bit1_def)
huffman@29997
   311
apply (rule plus_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   312
apply (rule times_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   313
apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   314
apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   315
apply (rule power_bit1_def [unfolded Abs_bit1'_def])
huffman@29997
   316
done
huffman@29997
   317
huffman@29997
   318
instance bit0 :: (finite) "{comm_ring_1,recpower}"
huffman@29997
   319
  by (rule bit0.comm_ring_1 bit0.recpower)+
huffman@29997
   320
huffman@29997
   321
instance bit1 :: (finite) "{comm_ring_1,recpower}"
huffman@29997
   322
  by (rule bit1.comm_ring_1 bit1.recpower)+
huffman@29997
   323
huffman@29997
   324
instantiation bit0 and bit1 :: (finite) number_ring
huffman@29997
   325
begin
huffman@29997
   326
huffman@29997
   327
definition "(number_of w :: _ bit0) = of_int w"
huffman@29997
   328
huffman@29997
   329
definition "(number_of w :: _ bit1) = of_int w"
huffman@29997
   330
huffman@29997
   331
instance proof
huffman@29997
   332
qed (rule number_of_bit0_def number_of_bit1_def)+
huffman@29997
   333
huffman@29997
   334
end
huffman@29997
   335
huffman@29997
   336
interpretation bit0!:
huffman@29998
   337
  mod_ring "int CARD('a::finite bit0)"
huffman@29997
   338
           "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
huffman@29997
   339
           "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
huffman@29997
   340
  ..
huffman@29997
   341
huffman@29997
   342
interpretation bit1!:
huffman@29998
   343
  mod_ring "int CARD('a::finite bit1)"
huffman@29997
   344
           "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
huffman@29997
   345
           "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
huffman@29997
   346
  ..
huffman@29997
   347
huffman@29997
   348
text {* Set up cases, induction, and arithmetic *}
huffman@29997
   349
huffman@29999
   350
lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
huffman@29999
   351
lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
huffman@29997
   352
huffman@29999
   353
lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct
huffman@29999
   354
lemmas bit1_induct [case_names of_int, induct type: bit1] = bit1.induct
huffman@29997
   355
huffman@29997
   356
lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
huffman@29997
   357
lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
huffman@29997
   358
huffman@29997
   359
declare power_Suc [where ?'a="'a::finite bit0", standard, simp]
huffman@29997
   360
declare power_Suc [where ?'a="'a::finite bit1", standard, simp]
huffman@29997
   361
huffman@29997
   362
kleing@24332
   363
subsection {* Syntax *}
kleing@24332
   364
kleing@24332
   365
syntax
kleing@24332
   366
  "_NumeralType" :: "num_const => type"  ("_")
kleing@24332
   367
  "_NumeralType0" :: type ("0")
kleing@24332
   368
  "_NumeralType1" :: type ("1")
kleing@24332
   369
kleing@24332
   370
translations
kleing@24332
   371
  "_NumeralType1" == (type) "num1"
huffman@24406
   372
  "_NumeralType0" == (type) "num0"
kleing@24332
   373
kleing@24332
   374
parse_translation {*
kleing@24332
   375
let
kleing@24332
   376
kleing@24332
   377
val num1_const = Syntax.const "Numeral_Type.num1";
huffman@24406
   378
val num0_const = Syntax.const "Numeral_Type.num0";
kleing@24332
   379
val B0_const = Syntax.const "Numeral_Type.bit0";
kleing@24332
   380
val B1_const = Syntax.const "Numeral_Type.bit1";
kleing@24332
   381
kleing@24332
   382
fun mk_bintype n =
kleing@24332
   383
  let
kleing@24332
   384
    fun mk_bit n = if n = 0 then B0_const else B1_const;
kleing@24332
   385
    fun bin_of n =
kleing@24332
   386
      if n = 1 then num1_const
huffman@24406
   387
      else if n = 0 then num0_const
kleing@24332
   388
      else if n = ~1 then raise TERM ("negative type numeral", [])
kleing@24332
   389
      else
wenzelm@24630
   390
        let val (q, r) = Integer.div_mod n 2;
kleing@24332
   391
        in mk_bit r $ bin_of q end;
kleing@24332
   392
  in bin_of n end;
kleing@24332
   393
kleing@24332
   394
fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
wenzelm@24630
   395
      mk_bintype (valOf (Int.fromString str))
kleing@24332
   396
  | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
kleing@24332
   397
kleing@24332
   398
in [("_NumeralType", numeral_tr)] end;
kleing@24332
   399
*}
kleing@24332
   400
kleing@24332
   401
print_translation {*
kleing@24332
   402
let
kleing@24332
   403
fun int_of [] = 0
wenzelm@24630
   404
  | int_of (b :: bs) = b + 2 * int_of bs;
kleing@24332
   405
huffman@24406
   406
fun bin_of (Const ("num0", _)) = []
kleing@24332
   407
  | bin_of (Const ("num1", _)) = [1]
kleing@24332
   408
  | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
kleing@24332
   409
  | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
kleing@24332
   410
  | bin_of t = raise TERM("bin_of", [t]);
kleing@24332
   411
kleing@24332
   412
fun bit_tr' b [t] =
kleing@24332
   413
  let
kleing@24332
   414
    val rev_digs = b :: bin_of t handle TERM _ => raise Match
kleing@24332
   415
    val i = int_of rev_digs;
wenzelm@24630
   416
    val num = string_of_int (abs i);
kleing@24332
   417
  in
kleing@24332
   418
    Syntax.const "_NumeralType" $ Syntax.free num
kleing@24332
   419
  end
kleing@24332
   420
  | bit_tr' b _ = raise Match;
kleing@24332
   421
kleing@24332
   422
in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
kleing@24332
   423
*}
kleing@24332
   424
kleing@24332
   425
wenzelm@25378
   426
subsection {* Classes with at least 1 and 2  *}
kleing@24332
   427
kleing@24332
   428
text {* Class finite already captures "at least 1" *}
kleing@24332
   429
huffman@24407
   430
lemma zero_less_card_finite [simp]:
kleing@24332
   431
  "0 < CARD('a::finite)"
kleing@24332
   432
proof (cases "CARD('a::finite) = 0")
kleing@24332
   433
  case False thus ?thesis by (simp del: card_0_eq)
kleing@24332
   434
next
kleing@24332
   435
  case True
kleing@24332
   436
  thus ?thesis by (simp add: finite)
kleing@24332
   437
qed
kleing@24332
   438
huffman@24407
   439
lemma one_le_card_finite [simp]:
kleing@24332
   440
  "Suc 0 <= CARD('a::finite)"
kleing@24332
   441
  by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
kleing@24332
   442
kleing@24332
   443
kleing@24332
   444
text {* Class for cardinality "at least 2" *}
kleing@24332
   445
kleing@24332
   446
class card2 = finite + 
kleing@24332
   447
  assumes two_le_card: "2 <= CARD('a)"
kleing@24332
   448
kleing@24332
   449
lemma one_less_card: "Suc 0 < CARD('a::card2)"
kleing@24332
   450
  using two_le_card [where 'a='a] by simp
kleing@24332
   451
kleing@24332
   452
instance bit0 :: (finite) card2
kleing@24332
   453
  by intro_classes (simp add: one_le_card_finite)
kleing@24332
   454
kleing@24332
   455
instance bit1 :: (finite) card2
kleing@24332
   456
  by intro_classes (simp add: one_le_card_finite)
kleing@24332
   457
kleing@24332
   458
subsection {* Examples *}
kleing@24332
   459
kleing@24332
   460
lemma "CARD(0) = 0" by simp
kleing@24332
   461
lemma "CARD(17) = 17" by simp
huffman@29997
   462
lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
huffman@28920
   463
kleing@24332
   464
end