src/HOL/Library/Code_Index.thy
author haftmann
Fri Oct 12 10:26:18 2007 +0200 (2007-10-12)
changeset 24999 1dbe785ed529
child 25335 182a001a7ea4
permissions -rw-r--r--
added
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@24999
     8
imports PreList
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@24999
    64
haftmann@24999
    65
subsection {* Basic arithmetic *}
haftmann@24999
    66
haftmann@24999
    67
instance index :: zero
haftmann@24999
    68
  [simp]: "0 \<equiv> index_of_int 0" ..
haftmann@24999
    69
lemmas [code func del] = zero_index_def
haftmann@24999
    70
haftmann@24999
    71
instance index :: one
haftmann@24999
    72
  [simp]: "1 \<equiv> index_of_int 1" ..
haftmann@24999
    73
lemmas [code func del] = one_index_def
haftmann@24999
    74
haftmann@24999
    75
instance index :: plus
haftmann@24999
    76
  [simp]: "k + l \<equiv> index_of_int (int_of_index k + int_of_index l)" ..
haftmann@24999
    77
lemmas [code func del] = plus_index_def
haftmann@24999
    78
lemma plus_index_code [code func]:
haftmann@24999
    79
  "index_of_int k + index_of_int l = index_of_int (k + l)"
haftmann@24999
    80
  unfolding plus_index_def by simp
haftmann@24999
    81
haftmann@24999
    82
instance index :: minus
haftmann@24999
    83
  [simp]: "- k \<equiv> index_of_int (- int_of_index k)"
haftmann@24999
    84
  [simp]: "k - l \<equiv> index_of_int (int_of_index k - int_of_index l)" ..
haftmann@24999
    85
lemmas [code func del] = uminus_index_def minus_index_def
haftmann@24999
    86
lemma uminus_index_code [code func]:
haftmann@24999
    87
  "- index_of_int k \<equiv> index_of_int (- k)"
haftmann@24999
    88
  unfolding uminus_index_def by simp
haftmann@24999
    89
lemma minus_index_code [code func]:
haftmann@24999
    90
  "index_of_int k - index_of_int l = index_of_int (k - l)"
haftmann@24999
    91
  unfolding minus_index_def by simp
haftmann@24999
    92
haftmann@24999
    93
instance index :: times
haftmann@24999
    94
  [simp]: "k * l \<equiv> index_of_int (int_of_index k * int_of_index l)" ..
haftmann@24999
    95
lemmas [code func del] = times_index_def
haftmann@24999
    96
lemma times_index_code [code func]:
haftmann@24999
    97
  "index_of_int k * index_of_int l = index_of_int (k * l)"
haftmann@24999
    98
  unfolding times_index_def by simp
haftmann@24999
    99
haftmann@24999
   100
instance index :: ord
haftmann@24999
   101
  [simp]: "k \<le> l \<equiv> int_of_index k \<le> int_of_index l"
haftmann@24999
   102
  [simp]: "k < l \<equiv> int_of_index k < int_of_index l" ..
haftmann@24999
   103
lemmas [code func del] = less_eq_index_def less_index_def
haftmann@24999
   104
lemma less_eq_index_code [code func]:
haftmann@24999
   105
  "index_of_int k \<le> index_of_int l \<longleftrightarrow> k \<le> l"
haftmann@24999
   106
  unfolding less_eq_index_def by simp
haftmann@24999
   107
lemma less_index_code [code func]:
haftmann@24999
   108
  "index_of_int k < index_of_int l \<longleftrightarrow> k < l"
haftmann@24999
   109
  unfolding less_index_def by simp
haftmann@24999
   110
haftmann@24999
   111
instance index :: ring_1
haftmann@24999
   112
  by default (auto simp add: left_distrib right_distrib)
haftmann@24999
   113
haftmann@24999
   114
lemma of_nat_index: "of_nat n = index_of_int (of_nat n)"
haftmann@24999
   115
proof (induct n)
haftmann@24999
   116
  case 0 show ?case by simp
haftmann@24999
   117
next
haftmann@24999
   118
  case (Suc n)
haftmann@24999
   119
  then have "int_of_index (index_of_int (int n))
haftmann@24999
   120
    = int_of_index (of_nat n)" by simp
haftmann@24999
   121
  then have "int n = int_of_index (of_nat n)" by simp
haftmann@24999
   122
  then show ?case by simp
haftmann@24999
   123
qed
haftmann@24999
   124
haftmann@24999
   125
instance index :: number_ring
haftmann@24999
   126
  by default
haftmann@24999
   127
    (simp_all add: left_distrib number_of_index_def of_int_of_nat of_nat_index)
haftmann@24999
   128
haftmann@24999
   129
lemma zero_index_code [code inline, code func]:
haftmann@24999
   130
  "(0\<Colon>index) = Numeral0"
haftmann@24999
   131
  by simp
haftmann@24999
   132
haftmann@24999
   133
lemma one_index_code [code inline, code func]:
haftmann@24999
   134
  "(1\<Colon>index) = Numeral1"
haftmann@24999
   135
  by simp
haftmann@24999
   136
haftmann@24999
   137
instance index :: abs
haftmann@24999
   138
  "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
haftmann@24999
   139
haftmann@24999
   140
lemma index_of_int [code func]:
haftmann@24999
   141
  "index_of_int k = (if k = 0 then 0
haftmann@24999
   142
    else if k = -1 then -1
haftmann@24999
   143
    else let (l, m) = divAlg (k, 2) in 2 * index_of_int l +
haftmann@24999
   144
      (if m = 0 then 0 else 1))"
haftmann@24999
   145
  by (simp add: number_of_index_shift Let_def split_def divAlg_mod_div) arith
haftmann@24999
   146
haftmann@24999
   147
haftmann@24999
   148
subsection {* Conversion to and from @{typ nat} *}
haftmann@24999
   149
haftmann@24999
   150
definition
haftmann@24999
   151
  nat_of_index :: "index \<Rightarrow> nat"
haftmann@24999
   152
where
haftmann@24999
   153
  [code func del]: "nat_of_index = nat o int_of_index"
haftmann@24999
   154
haftmann@24999
   155
definition
haftmann@24999
   156
  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
haftmann@24999
   157
  [code func del]: "nat_of_index_aux i n = nat_of_index i + n"
haftmann@24999
   158
haftmann@24999
   159
lemma nat_of_index_aux_code [code]:
haftmann@24999
   160
  "nat_of_index_aux i n = (if i \<le> 0 then n else nat_of_index_aux (i - 1) (Suc n))"
haftmann@24999
   161
  by (auto simp add: nat_of_index_aux_def nat_of_index_def)
haftmann@24999
   162
haftmann@24999
   163
lemma nat_of_index_code [code]:
haftmann@24999
   164
  "nat_of_index i = nat_of_index_aux i 0"
haftmann@24999
   165
  by (simp add: nat_of_index_aux_def)
haftmann@24999
   166
haftmann@24999
   167
definition
haftmann@24999
   168
  index_of_nat :: "nat \<Rightarrow> index"
haftmann@24999
   169
where
haftmann@24999
   170
  [code func del]: "index_of_nat = index_of_int o of_nat"
haftmann@24999
   171
haftmann@24999
   172
lemma index_of_nat [code func]:
haftmann@24999
   173
  "index_of_nat 0 = 0"
haftmann@24999
   174
  "index_of_nat (Suc n) = index_of_nat n + 1"
haftmann@24999
   175
  unfolding index_of_nat_def by simp_all
haftmann@24999
   176
haftmann@24999
   177
lemma index_nat_id [simp]:
haftmann@24999
   178
  "nat_of_index (index_of_nat n) = n"
haftmann@24999
   179
  "index_of_nat (nat_of_index i) = (if i \<le> 0 then 0 else i)"
haftmann@24999
   180
  unfolding index_of_nat_def nat_of_index_def by simp_all
haftmann@24999
   181
haftmann@24999
   182
haftmann@24999
   183
subsection {* ML interface *}
haftmann@24999
   184
haftmann@24999
   185
ML {*
haftmann@24999
   186
structure Index =
haftmann@24999
   187
struct
haftmann@24999
   188
haftmann@24999
   189
fun mk k = @{term index_of_int} $ HOLogic.mk_number @{typ index} k;
haftmann@24999
   190
haftmann@24999
   191
end;
haftmann@24999
   192
*}
haftmann@24999
   193
haftmann@24999
   194
haftmann@24999
   195
subsection {* Code serialization *}
haftmann@24999
   196
haftmann@24999
   197
code_type index
haftmann@24999
   198
  (SML "int")
haftmann@24999
   199
  (OCaml "int")
haftmann@24999
   200
  (Haskell "Integer")
haftmann@24999
   201
haftmann@24999
   202
code_instance index :: eq
haftmann@24999
   203
  (Haskell -)
haftmann@24999
   204
haftmann@24999
   205
setup {*
haftmann@24999
   206
  fold (fn target => CodeTarget.add_pretty_numeral target true
haftmann@24999
   207
    @{const_name number_index_inst.number_of_index}
haftmann@24999
   208
    @{const_name Numeral.B0} @{const_name Numeral.B1}
haftmann@24999
   209
    @{const_name Numeral.Pls} @{const_name Numeral.Min}
haftmann@24999
   210
    @{const_name Numeral.Bit}
haftmann@24999
   211
  ) ["SML", "OCaml", "Haskell"]
haftmann@24999
   212
*}
haftmann@24999
   213
haftmann@24999
   214
code_reserved SML int
haftmann@24999
   215
code_reserved OCaml int
haftmann@24999
   216
haftmann@24999
   217
code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
haftmann@24999
   218
  (SML "Int.+ ((_), (_))")
haftmann@24999
   219
  (OCaml "Pervasives.+")
haftmann@24999
   220
  (Haskell infixl 6 "+")
haftmann@24999
   221
haftmann@24999
   222
code_const "uminus \<Colon> index \<Rightarrow> index"
haftmann@24999
   223
  (SML "Int.~")
haftmann@24999
   224
  (OCaml "Pervasives.~-")
haftmann@24999
   225
  (Haskell "negate")
haftmann@24999
   226
haftmann@24999
   227
code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
haftmann@24999
   228
  (SML "Int.- ((_), (_))")
haftmann@24999
   229
  (OCaml "Pervasives.-")
haftmann@24999
   230
  (Haskell infixl 6 "-")
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 7 "*")
haftmann@24999
   236
haftmann@24999
   237
code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
haftmann@24999
   238
  (SML "!((_ : Int.int) = _)")
haftmann@24999
   239
  (OCaml "!((_ : Pervasives.int) = _)")
haftmann@24999
   240
  (Haskell infixl 4 "==")
haftmann@24999
   241
haftmann@24999
   242
code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
haftmann@24999
   243
  (SML "Int.<= ((_), (_))")
haftmann@24999
   244
  (OCaml "!((_ : Pervasives.int) <= _)")
haftmann@24999
   245
  (Haskell infix 4 "<=")
haftmann@24999
   246
haftmann@24999
   247
code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
haftmann@24999
   248
  (SML "Int.< ((_), (_))")
haftmann@24999
   249
  (OCaml "!((_ : Pervasives.int) < _)")
haftmann@24999
   250
  (Haskell infix 4 "<")
haftmann@24999
   251
haftmann@24999
   252
code_reserved SML Int
haftmann@24999
   253
code_reserved OCaml Pervasives
haftmann@24999
   254
haftmann@24999
   255
end