src/HOL/Library/Code_Index.thy
author haftmann
Tue Dec 18 14:37:00 2007 +0100 (2007-12-18)
changeset 25691 8f8d83af100a
parent 25502 9200b36280c0
child 25767 852bce03412a
permissions -rw-r--r--
switched from PreList to ATP_Linkup
haftmann@24999
     1
(*  ID:         $Id$
haftmann@24999
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@24999
     3
*)
haftmann@24999
     4
haftmann@24999
     5
header {* Type of indices *}
haftmann@24999
     6
haftmann@24999
     7
theory Code_Index
haftmann@25691
     8
imports ATP_Linkup
haftmann@24999
     9
begin
haftmann@24999
    10
haftmann@24999
    11
text {*
haftmann@24999
    12
  Indices are isomorphic to HOL @{typ int} but
haftmann@24999
    13
  mapped to target-language builtin integers
haftmann@24999
    14
*}
haftmann@24999
    15
haftmann@24999
    16
subsection {* Datatype of indices *}
haftmann@24999
    17
haftmann@24999
    18
datatype index = index_of_int int
haftmann@24999
    19
haftmann@24999
    20
lemmas [code func del] = index.recs index.cases
haftmann@24999
    21
haftmann@24999
    22
fun
haftmann@24999
    23
  int_of_index :: "index \<Rightarrow> int"
haftmann@24999
    24
where
haftmann@24999
    25
  "int_of_index (index_of_int k) = k"
haftmann@24999
    26
lemmas [code func del] = int_of_index.simps
haftmann@24999
    27
haftmann@24999
    28
lemma index_id [simp]:
haftmann@24999
    29
  "index_of_int (int_of_index k) = k"
haftmann@24999
    30
  by (cases k) simp_all
haftmann@24999
    31
haftmann@24999
    32
lemma index:
haftmann@24999
    33
  "(\<And>k\<Colon>index. PROP P k) \<equiv> (\<And>k\<Colon>int. PROP P (index_of_int k))"
haftmann@24999
    34
proof
haftmann@24999
    35
  fix k :: int
haftmann@24999
    36
  assume "\<And>k\<Colon>index. PROP P k"
haftmann@24999
    37
  then show "PROP P (index_of_int k)" .
haftmann@24999
    38
next
haftmann@24999
    39
  fix k :: index
haftmann@24999
    40
  assume "\<And>k\<Colon>int. PROP P (index_of_int k)"
haftmann@24999
    41
  then have "PROP P (index_of_int (int_of_index k))" .
haftmann@24999
    42
  then show "PROP P k" by simp
haftmann@24999
    43
qed
haftmann@24999
    44
haftmann@24999
    45
lemma [code func]: "size (k\<Colon>index) = 0"
haftmann@24999
    46
  by (cases k) simp_all
haftmann@24999
    47
haftmann@24999
    48
haftmann@24999
    49
subsection {* Built-in integers as datatype on numerals *}
haftmann@24999
    50
haftmann@24999
    51
instance index :: number
haftmann@24999
    52
  "number_of \<equiv> index_of_int" ..
haftmann@24999
    53
haftmann@24999
    54
code_datatype "number_of \<Colon> int \<Rightarrow> index"
haftmann@24999
    55
haftmann@24999
    56
lemma number_of_index_id [simp]:
haftmann@24999
    57
  "number_of (int_of_index k) = k"
haftmann@24999
    58
  unfolding number_of_index_def by simp
haftmann@24999
    59
haftmann@24999
    60
lemma number_of_index_shift:
haftmann@24999
    61
  "number_of k = index_of_int (number_of k)"
haftmann@24999
    62
  by (simp add: number_of_is_id number_of_index_def)
haftmann@24999
    63
haftmann@25335
    64
lemma int_of_index_number_of [simp]:
haftmann@25335
    65
  "int_of_index (number_of k) = number_of k"
haftmann@25335
    66
  unfolding number_of_index_def number_of_is_id by simp
haftmann@25335
    67
haftmann@24999
    68
haftmann@24999
    69
subsection {* Basic arithmetic *}
haftmann@24999
    70
haftmann@24999
    71
instance index :: zero
haftmann@24999
    72
  [simp]: "0 \<equiv> index_of_int 0" ..
haftmann@24999
    73
lemmas [code func del] = zero_index_def
haftmann@24999
    74
haftmann@24999
    75
instance index :: one
haftmann@24999
    76
  [simp]: "1 \<equiv> index_of_int 1" ..
haftmann@24999
    77
lemmas [code func del] = one_index_def
haftmann@24999
    78
haftmann@24999
    79
instance index :: plus
haftmann@24999
    80
  [simp]: "k + l \<equiv> index_of_int (int_of_index k + int_of_index l)" ..
haftmann@24999
    81
lemmas [code func del] = plus_index_def
haftmann@24999
    82
lemma plus_index_code [code func]:
haftmann@24999
    83
  "index_of_int k + index_of_int l = index_of_int (k + l)"
haftmann@24999
    84
  unfolding plus_index_def by simp
haftmann@24999
    85
haftmann@24999
    86
instance index :: minus
haftmann@24999
    87
  [simp]: "- k \<equiv> index_of_int (- int_of_index k)"
haftmann@24999
    88
  [simp]: "k - l \<equiv> index_of_int (int_of_index k - int_of_index l)" ..
haftmann@24999
    89
lemmas [code func del] = uminus_index_def minus_index_def
haftmann@24999
    90
lemma uminus_index_code [code func]:
haftmann@24999
    91
  "- index_of_int k \<equiv> index_of_int (- k)"
haftmann@24999
    92
  unfolding uminus_index_def by simp
haftmann@24999
    93
lemma minus_index_code [code func]:
haftmann@24999
    94
  "index_of_int k - index_of_int l = index_of_int (k - l)"
haftmann@24999
    95
  unfolding minus_index_def by simp
haftmann@24999
    96
haftmann@24999
    97
instance index :: times
haftmann@24999
    98
  [simp]: "k * l \<equiv> index_of_int (int_of_index k * int_of_index l)" ..
haftmann@24999
    99
lemmas [code func del] = times_index_def
haftmann@24999
   100
lemma times_index_code [code func]:
haftmann@24999
   101
  "index_of_int k * index_of_int l = index_of_int (k * l)"
haftmann@24999
   102
  unfolding times_index_def by simp
haftmann@24999
   103
haftmann@24999
   104
instance index :: ord
haftmann@24999
   105
  [simp]: "k \<le> l \<equiv> int_of_index k \<le> int_of_index l"
haftmann@24999
   106
  [simp]: "k < l \<equiv> int_of_index k < int_of_index l" ..
haftmann@24999
   107
lemmas [code func del] = less_eq_index_def less_index_def
haftmann@24999
   108
lemma less_eq_index_code [code func]:
haftmann@24999
   109
  "index_of_int k \<le> index_of_int l \<longleftrightarrow> k \<le> l"
haftmann@24999
   110
  unfolding less_eq_index_def by simp
haftmann@24999
   111
lemma less_index_code [code func]:
haftmann@24999
   112
  "index_of_int k < index_of_int l \<longleftrightarrow> k < l"
haftmann@24999
   113
  unfolding less_index_def by simp
haftmann@24999
   114
haftmann@25335
   115
instance index :: "Divides.div"
haftmann@25335
   116
  [simp]: "k div l \<equiv> index_of_int (int_of_index k div int_of_index l)"
haftmann@25335
   117
  [simp]: "k mod l \<equiv> index_of_int (int_of_index k mod int_of_index l)" ..
haftmann@25335
   118
haftmann@24999
   119
instance index :: ring_1
haftmann@24999
   120
  by default (auto simp add: left_distrib right_distrib)
haftmann@24999
   121
haftmann@24999
   122
lemma of_nat_index: "of_nat n = index_of_int (of_nat n)"
haftmann@24999
   123
proof (induct n)
haftmann@24999
   124
  case 0 show ?case by simp
haftmann@24999
   125
next
haftmann@24999
   126
  case (Suc n)
haftmann@24999
   127
  then have "int_of_index (index_of_int (int n))
haftmann@24999
   128
    = int_of_index (of_nat n)" by simp
haftmann@24999
   129
  then have "int n = int_of_index (of_nat n)" by simp
haftmann@24999
   130
  then show ?case by simp
haftmann@24999
   131
qed
haftmann@24999
   132
haftmann@24999
   133
instance index :: number_ring
haftmann@24999
   134
  by default
haftmann@24999
   135
    (simp_all add: left_distrib number_of_index_def of_int_of_nat of_nat_index)
haftmann@24999
   136
haftmann@24999
   137
lemma zero_index_code [code inline, code func]:
haftmann@24999
   138
  "(0\<Colon>index) = Numeral0"
haftmann@24999
   139
  by simp
haftmann@24999
   140
haftmann@24999
   141
lemma one_index_code [code inline, code func]:
haftmann@24999
   142
  "(1\<Colon>index) = Numeral1"
haftmann@24999
   143
  by simp
haftmann@24999
   144
haftmann@24999
   145
instance index :: abs
haftmann@25502
   146
  "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" ..
haftmann@24999
   147
haftmann@24999
   148
lemma index_of_int [code func]:
haftmann@24999
   149
  "index_of_int k = (if k = 0 then 0
haftmann@24999
   150
    else if k = -1 then -1
haftmann@24999
   151
    else let (l, m) = divAlg (k, 2) in 2 * index_of_int l +
haftmann@24999
   152
      (if m = 0 then 0 else 1))"
haftmann@24999
   153
  by (simp add: number_of_index_shift Let_def split_def divAlg_mod_div) arith
haftmann@24999
   154
haftmann@25335
   155
lemma int_of_index [code func]:
haftmann@25335
   156
  "int_of_index k = (if k = 0 then 0
haftmann@25335
   157
    else if k = -1 then -1
haftmann@25335
   158
    else let l = k div 2; m = k mod 2 in 2 * int_of_index l +
haftmann@25335
   159
      (if m = 0 then 0 else 1))"
haftmann@25335
   160
  by (auto simp add: number_of_index_shift Let_def split_def) arith
haftmann@25335
   161
haftmann@24999
   162
haftmann@24999
   163
subsection {* Conversion to and from @{typ nat} *}
haftmann@24999
   164
haftmann@24999
   165
definition
haftmann@24999
   166
  nat_of_index :: "index \<Rightarrow> nat"
haftmann@24999
   167
where
haftmann@24999
   168
  [code func del]: "nat_of_index = nat o int_of_index"
haftmann@24999
   169
haftmann@24999
   170
definition
haftmann@24999
   171
  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
haftmann@24999
   172
  [code func del]: "nat_of_index_aux i n = nat_of_index i + n"
haftmann@24999
   173
haftmann@24999
   174
lemma nat_of_index_aux_code [code]:
haftmann@24999
   175
  "nat_of_index_aux i n = (if i \<le> 0 then n else nat_of_index_aux (i - 1) (Suc n))"
haftmann@24999
   176
  by (auto simp add: nat_of_index_aux_def nat_of_index_def)
haftmann@24999
   177
haftmann@24999
   178
lemma nat_of_index_code [code]:
haftmann@24999
   179
  "nat_of_index i = nat_of_index_aux i 0"
haftmann@24999
   180
  by (simp add: nat_of_index_aux_def)
haftmann@24999
   181
haftmann@24999
   182
definition
haftmann@24999
   183
  index_of_nat :: "nat \<Rightarrow> index"
haftmann@24999
   184
where
haftmann@24999
   185
  [code func del]: "index_of_nat = index_of_int o of_nat"
haftmann@24999
   186
haftmann@24999
   187
lemma index_of_nat [code func]:
haftmann@24999
   188
  "index_of_nat 0 = 0"
haftmann@24999
   189
  "index_of_nat (Suc n) = index_of_nat n + 1"
haftmann@24999
   190
  unfolding index_of_nat_def by simp_all
haftmann@24999
   191
haftmann@24999
   192
lemma index_nat_id [simp]:
haftmann@24999
   193
  "nat_of_index (index_of_nat n) = n"
haftmann@24999
   194
  "index_of_nat (nat_of_index i) = (if i \<le> 0 then 0 else i)"
haftmann@24999
   195
  unfolding index_of_nat_def nat_of_index_def by simp_all
haftmann@24999
   196
haftmann@24999
   197
haftmann@24999
   198
subsection {* ML interface *}
haftmann@24999
   199
haftmann@24999
   200
ML {*
haftmann@24999
   201
structure Index =
haftmann@24999
   202
struct
haftmann@24999
   203
haftmann@24999
   204
fun mk k = @{term index_of_int} $ HOLogic.mk_number @{typ index} k;
haftmann@24999
   205
haftmann@24999
   206
end;
haftmann@24999
   207
*}
haftmann@24999
   208
haftmann@24999
   209
haftmann@24999
   210
subsection {* Code serialization *}
haftmann@24999
   211
haftmann@24999
   212
code_type index
haftmann@24999
   213
  (SML "int")
haftmann@24999
   214
  (OCaml "int")
haftmann@24999
   215
  (Haskell "Integer")
haftmann@24999
   216
haftmann@24999
   217
code_instance index :: eq
haftmann@24999
   218
  (Haskell -)
haftmann@24999
   219
haftmann@24999
   220
setup {*
haftmann@24999
   221
  fold (fn target => CodeTarget.add_pretty_numeral target true
haftmann@24999
   222
    @{const_name number_index_inst.number_of_index}
haftmann@24999
   223
    @{const_name Numeral.B0} @{const_name Numeral.B1}
haftmann@24999
   224
    @{const_name Numeral.Pls} @{const_name Numeral.Min}
haftmann@24999
   225
    @{const_name Numeral.Bit}
haftmann@24999
   226
  ) ["SML", "OCaml", "Haskell"]
haftmann@24999
   227
*}
haftmann@24999
   228
haftmann@24999
   229
code_reserved SML int
haftmann@24999
   230
code_reserved OCaml int
haftmann@24999
   231
haftmann@24999
   232
code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
haftmann@24999
   233
  (SML "Int.+ ((_), (_))")
haftmann@24999
   234
  (OCaml "Pervasives.+")
haftmann@24999
   235
  (Haskell infixl 6 "+")
haftmann@24999
   236
haftmann@24999
   237
code_const "uminus \<Colon> index \<Rightarrow> index"
haftmann@24999
   238
  (SML "Int.~")
haftmann@24999
   239
  (OCaml "Pervasives.~-")
haftmann@24999
   240
  (Haskell "negate")
haftmann@24999
   241
haftmann@24999
   242
code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
haftmann@24999
   243
  (SML "Int.- ((_), (_))")
haftmann@24999
   244
  (OCaml "Pervasives.-")
haftmann@24999
   245
  (Haskell infixl 6 "-")
haftmann@24999
   246
haftmann@24999
   247
code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
haftmann@24999
   248
  (SML "Int.* ((_), (_))")
haftmann@24999
   249
  (OCaml "Pervasives.*")
haftmann@24999
   250
  (Haskell infixl 7 "*")
haftmann@24999
   251
haftmann@24999
   252
code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
haftmann@24999
   253
  (SML "!((_ : Int.int) = _)")
haftmann@24999
   254
  (OCaml "!((_ : Pervasives.int) = _)")
haftmann@24999
   255
  (Haskell infixl 4 "==")
haftmann@24999
   256
haftmann@24999
   257
code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
haftmann@24999
   258
  (SML "Int.<= ((_), (_))")
haftmann@24999
   259
  (OCaml "!((_ : Pervasives.int) <= _)")
haftmann@24999
   260
  (Haskell infix 4 "<=")
haftmann@24999
   261
haftmann@24999
   262
code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
haftmann@24999
   263
  (SML "Int.< ((_), (_))")
haftmann@24999
   264
  (OCaml "!((_ : Pervasives.int) < _)")
haftmann@24999
   265
  (Haskell infix 4 "<")
haftmann@24999
   266
haftmann@24999
   267
code_reserved SML Int
haftmann@24999
   268
code_reserved OCaml Pervasives
haftmann@24999
   269
haftmann@24999
   270
end