src/HOL/Library/Code_Index.thy
author haftmann
Tue Jan 15 16:19:21 2008 +0100 (2008-01-15)
changeset 25918 82dd239e0f65
parent 25767 852bce03412a
child 25928 042e877d9841
permissions -rw-r--r--
tuned
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Type of indices *}
     6 
     7 theory Code_Index
     8 imports ATP_Linkup
     9 begin
    10 
    11 text {*
    12   Indices are isomorphic to HOL @{typ nat} but
    13   mapped to target-language builtin integers
    14 *}
    15 
    16 subsection {* Datatype of indices *}
    17 
    18 datatype index = index_of_nat nat
    19 
    20 lemmas [code func del] = index.recs index.cases
    21 
    22 primrec
    23   nat_of_index :: "index \<Rightarrow> nat"
    24 where
    25   "nat_of_index (index_of_nat k) = k"
    26 lemmas [code func del] = nat_of_index.simps
    27 
    28 lemma index_id [simp]:
    29   "index_of_nat (nat_of_index n) = n"
    30   by (cases n) simp_all
    31 
    32 lemma nat_of_index_inject [simp]:
    33   "nat_of_index n = nat_of_index m \<longleftrightarrow> n = m"
    34   by (cases n) auto
    35 
    36 lemma index:
    37   "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
    38 proof
    39   fix n :: nat
    40   assume "\<And>n\<Colon>index. PROP P n"
    41   then show "PROP P (index_of_nat n)" .
    42 next
    43   fix n :: index
    44   assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)"
    45   then have "PROP P (index_of_nat (nat_of_index n))" .
    46   then show "PROP P n" by simp
    47 qed
    48 
    49 lemma [code func]: "size (n\<Colon>index) = 0"
    50   by (cases n) simp_all
    51 
    52 
    53 subsection {* Indices as datatype of ints *}
    54 
    55 instantiation index :: number
    56 begin
    57 
    58 definition
    59   "number_of = index_of_nat o nat"
    60 
    61 instance ..
    62 
    63 end
    64 
    65 code_datatype "number_of \<Colon> int \<Rightarrow> index"
    66 
    67 
    68 subsection {* Basic arithmetic *}
    69 
    70 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
    71 begin
    72 
    73 definition [simp, code func del]:
    74   "(0\<Colon>index) = index_of_nat 0"
    75 
    76 lemma zero_index_code [code inline, code func]:
    77   "(0\<Colon>index) = Numeral0"
    78   by (simp add: number_of_index_def Pls_def)
    79 
    80 definition [simp, code func del]:
    81   "(1\<Colon>index) = index_of_nat 1"
    82 
    83 lemma one_index_code [code inline, code func]:
    84   "(1\<Colon>index) = Numeral1"
    85   by (simp add: number_of_index_def Pls_def Bit_def)
    86 
    87 definition [simp, code func del]:
    88   "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
    89 
    90 lemma plus_index_code [code func]:
    91   "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
    92   by simp
    93 
    94 definition [simp, code func del]:
    95   "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
    96 
    97 definition [simp, code func del]:
    98   "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
    99 
   100 lemma times_index_code [code func]:
   101   "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
   102   by simp
   103 
   104 definition [simp, code func del]:
   105   "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
   106 
   107 definition [simp, code func del]:
   108   "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
   109 
   110 lemma div_index_code [code func]:
   111   "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
   112   by simp
   113 
   114 lemma mod_index_code [code func]:
   115   "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
   116   by simp
   117 
   118 definition [simp, code func del]:
   119   "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
   120 
   121 definition [simp, code func del]:
   122   "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
   123 
   124 lemma less_eq_index_code [code func]:
   125   "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
   126   by simp
   127 
   128 lemma less_index_code [code func]:
   129   "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
   130   by simp
   131 
   132 instance by default (auto simp add: left_distrib index)
   133 
   134 end
   135 
   136 lemma index_of_nat_code [code func]:
   137   "index_of_nat = of_nat"
   138 proof
   139   fix n :: nat
   140   have "of_nat n = index_of_nat n"
   141     by (induct n) simp_all
   142   then show "index_of_nat n = of_nat n"
   143     by (rule sym)
   144 qed
   145 
   146 lemma nat_of_index_code [code func]:
   147   "nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n - 1)))"
   148   by (induct n) simp
   149 
   150 
   151 subsection {* ML interface *}
   152 
   153 ML {*
   154 structure Index =
   155 struct
   156 
   157 fun mk k = @{term index_of_nat} $ HOLogic.mk_number @{typ index} k;
   158 
   159 end;
   160 *}
   161 
   162 
   163 subsection {* Code serialization *}
   164 
   165 text {* Implementation of indices by bounded integers *}
   166 
   167 code_type index
   168   (SML "int")
   169   (OCaml "int")
   170   (Haskell "Integer")
   171 
   172 code_instance index :: eq
   173   (Haskell -)
   174 
   175 setup {*
   176   fold (fn target => CodeTarget.add_pretty_numeral target false
   177     @{const_name number_index_inst.number_of_index}
   178     @{const_name Int.B0} @{const_name Int.B1}
   179     @{const_name Int.Pls} @{const_name Int.Min}
   180     @{const_name Int.Bit}
   181   ) ["SML", "OCaml", "Haskell"]
   182 *}
   183 
   184 code_reserved SML Int int
   185 code_reserved OCaml Pervasives int
   186 
   187 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   188   (SML "Int.+ ((_), (_))")
   189   (OCaml "Pervasives.+")
   190   (Haskell infixl 6 "+")
   191 
   192 code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   193   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   194   (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   195   (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
   196 
   197 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   198   (SML "Int.* ((_), (_))")
   199   (OCaml "Pervasives.*")
   200   (Haskell infixl 7 "*")
   201 
   202 code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   203   (SML "!((_ : Int.int) = _)")
   204   (OCaml "!((_ : Pervasives.int) = _)")
   205   (Haskell infixl 4 "==")
   206 
   207 code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   208   (SML "Int.<= ((_), (_))")
   209   (OCaml "!((_ : Pervasives.int) <= _)")
   210   (Haskell infix 4 "<=")
   211 
   212 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   213   (SML "Int.< ((_), (_))")
   214   (OCaml "!((_ : Pervasives.int) < _)")
   215   (Haskell infix 4 "<")
   216 
   217 code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   218   (SML "IntInf.div ((_), (_))")
   219   (OCaml "Big'_int.div'_big'_int")
   220   (Haskell "div")
   221 
   222 code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   223   (SML "IntInf.mod ((_), (_))")
   224   (OCaml "Big'_int.mod'_big'_int")
   225   (Haskell "mod")
   226 
   227 end