src/HOL/Library/Code_Index.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 28042 1471f2974eb1
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Type of indices *}
     6 
     7 theory Code_Index
     8 imports Plain "~~/src/HOL/Presburger"
     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 typedef index = "UNIV \<Colon> nat set"
    19   morphisms nat_of_index index_of_nat by rule
    20 
    21 lemma index_of_nat_nat_of_index [simp]:
    22   "index_of_nat (nat_of_index k) = k"
    23   by (rule nat_of_index_inverse)
    24 
    25 lemma nat_of_index_index_of_nat [simp]:
    26   "nat_of_index (index_of_nat n) = n"
    27   by (rule index_of_nat_inverse) 
    28     (unfold index_def, rule UNIV_I)
    29 
    30 lemma index:
    31   "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
    32 proof
    33   fix n :: nat
    34   assume "\<And>n\<Colon>index. PROP P n"
    35   then show "PROP P (index_of_nat n)" .
    36 next
    37   fix n :: index
    38   assume "\<And>n\<Colon>nat. PROP P (index_of_nat n)"
    39   then have "PROP P (index_of_nat (nat_of_index n))" .
    40   then show "PROP P n" by simp
    41 qed
    42 
    43 lemma index_case:
    44   assumes "\<And>n. k = index_of_nat n \<Longrightarrow> P"
    45   shows P
    46   by (rule assms [of "nat_of_index k"]) simp
    47 
    48 lemma index_induct_raw:
    49   assumes "\<And>n. P (index_of_nat n)"
    50   shows "P k"
    51 proof -
    52   from assms have "P (index_of_nat (nat_of_index k))" .
    53   then show ?thesis by simp
    54 qed
    55 
    56 lemma nat_of_index_inject [simp]:
    57   "nat_of_index k = nat_of_index l \<longleftrightarrow> k = l"
    58   by (rule nat_of_index_inject)
    59 
    60 lemma index_of_nat_inject [simp]:
    61   "index_of_nat n = index_of_nat m \<longleftrightarrow> n = m"
    62   by (auto intro!: index_of_nat_inject simp add: index_def)
    63 
    64 instantiation index :: zero
    65 begin
    66 
    67 definition [simp, code func del]:
    68   "0 = index_of_nat 0"
    69 
    70 instance ..
    71 
    72 end
    73 
    74 definition [simp]:
    75   "Suc_index k = index_of_nat (Suc (nat_of_index k))"
    76 
    77 rep_datatype "0 \<Colon> index" Suc_index
    78 proof -
    79   fix P :: "index \<Rightarrow> bool"
    80   fix k :: index
    81   assume "P 0" then have init: "P (index_of_nat 0)" by simp
    82   assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
    83     then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" .
    84     then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp
    85   from init step have "P (index_of_nat (nat_of_index k))"
    86     by (induct "nat_of_index k") simp_all
    87   then show "P k" by simp
    88 qed simp_all
    89 
    90 lemmas [code func del] = index.recs index.cases
    91 
    92 declare index_case [case_names nat, cases type: index]
    93 declare index.induct [case_names nat, induct type: index]
    94 
    95 lemma [code func]:
    96   "index_size = nat_of_index"
    97 proof (rule ext)
    98   fix k
    99   have "index_size k = nat_size (nat_of_index k)"
   100     by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
   101   also have "nat_size (nat_of_index k) = nat_of_index k" by (induct "nat_of_index k") simp_all
   102   finally show "index_size k = nat_of_index k" .
   103 qed
   104 
   105 lemma [code func]:
   106   "size = nat_of_index"
   107 proof (rule ext)
   108   fix k
   109   show "size k = nat_of_index k"
   110   by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
   111 qed
   112 
   113 lemma [code func]:
   114   "k = l \<longleftrightarrow> nat_of_index k = nat_of_index l"
   115   by (cases k, cases l) simp
   116 
   117 
   118 subsection {* Indices as datatype of ints *}
   119 
   120 instantiation index :: number
   121 begin
   122 
   123 definition
   124   "number_of = index_of_nat o nat"
   125 
   126 instance ..
   127 
   128 end
   129 
   130 lemma nat_of_index_number [simp]:
   131   "nat_of_index (number_of k) = number_of k"
   132   by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
   133 
   134 code_datatype "number_of \<Colon> int \<Rightarrow> index"
   135 
   136 
   137 subsection {* Basic arithmetic *}
   138 
   139 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
   140 begin
   141 
   142 lemma zero_index_code [code inline, code func]:
   143   "(0\<Colon>index) = Numeral0"
   144   by (simp add: number_of_index_def Pls_def)
   145 lemma [code post]: "Numeral0 = (0\<Colon>index)"
   146   using zero_index_code ..
   147 
   148 definition [simp, code func del]:
   149   "(1\<Colon>index) = index_of_nat 1"
   150 
   151 lemma one_index_code [code inline, code func]:
   152   "(1\<Colon>index) = Numeral1"
   153   by (simp add: number_of_index_def Pls_def Bit1_def)
   154 lemma [code post]: "Numeral1 = (1\<Colon>index)"
   155   using one_index_code ..
   156 
   157 definition [simp, code func del]:
   158   "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
   159 
   160 lemma plus_index_code [code func]:
   161   "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
   162   by simp
   163 
   164 definition [simp, code func del]:
   165   "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
   166 
   167 definition [simp, code func del]:
   168   "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
   169 
   170 lemma times_index_code [code func]:
   171   "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
   172   by simp
   173 
   174 definition [simp, code func del]:
   175   "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
   176 
   177 definition [simp, code func del]:
   178   "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
   179 
   180 lemma div_index_code [code func]:
   181   "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
   182   by simp
   183 
   184 lemma mod_index_code [code func]:
   185   "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
   186   by simp
   187 
   188 definition [simp, code func del]:
   189   "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
   190 
   191 definition [simp, code func del]:
   192   "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
   193 
   194 lemma less_eq_index_code [code func]:
   195   "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
   196   by simp
   197 
   198 lemma less_index_code [code func]:
   199   "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
   200   by simp
   201 
   202 instance by default (auto simp add: left_distrib index)
   203 
   204 end
   205 
   206 lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
   207 
   208 lemma index_of_nat_code [code]:
   209   "index_of_nat = of_nat"
   210 proof
   211   fix n :: nat
   212   have "of_nat n = index_of_nat n"
   213     by (induct n) simp_all
   214   then show "index_of_nat n = of_nat n"
   215     by (rule sym)
   216 qed
   217 
   218 lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
   219   by (cases i) auto
   220 
   221 definition
   222   nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat"
   223 where
   224   "nat_of_index_aux i n = nat_of_index i + n"
   225 
   226 lemma nat_of_index_aux_code [code]:
   227   "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))"
   228   by (auto simp add: nat_of_index_aux_def index_not_eq_zero)
   229 
   230 lemma nat_of_index_code [code]:
   231   "nat_of_index i = nat_of_index_aux i 0"
   232   by (simp add: nat_of_index_aux_def)
   233 
   234 
   235 subsection {* ML interface *}
   236 
   237 ML {*
   238 structure Index =
   239 struct
   240 
   241 fun mk k = HOLogic.mk_number @{typ index} k;
   242 
   243 end;
   244 *}
   245 
   246 
   247 subsection {* Specialized @{term "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"},
   248   @{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"}
   249   operations *}
   250 
   251 definition
   252   minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
   253 where
   254   [code func del]: "minus_index_aux = op -"
   255 
   256 lemma [code func]: "op - = minus_index_aux"
   257   using minus_index_aux_def ..
   258 
   259 definition
   260   div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index"
   261 where
   262   [code func del]: "div_mod_index n m = (n div m, n mod m)"
   263 
   264 lemma [code func]:
   265   "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   266   unfolding div_mod_index_def by auto
   267 
   268 lemma [code func]:
   269   "n div m = fst (div_mod_index n m)"
   270   unfolding div_mod_index_def by simp
   271 
   272 lemma [code func]:
   273   "n mod m = snd (div_mod_index n m)"
   274   unfolding div_mod_index_def by simp
   275 
   276 
   277 subsection {* Code serialization *}
   278 
   279 text {* Implementation of indices by bounded integers *}
   280 
   281 code_type index
   282   (SML "int")
   283   (OCaml "int")
   284   (Haskell "Int")
   285 
   286 code_instance index :: eq
   287   (Haskell -)
   288 
   289 setup {*
   290   fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
   291     false false) ["SML", "OCaml", "Haskell"]
   292 *}
   293 
   294 code_reserved SML Int int
   295 code_reserved OCaml Pervasives int
   296 
   297 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   298   (SML "Int.+/ ((_),/ (_))")
   299   (OCaml "Pervasives.( + )")
   300   (Haskell infixl 6 "+")
   301 
   302 code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   303   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   304   (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   305   (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
   306 
   307 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   308   (SML "Int.*/ ((_),/ (_))")
   309   (OCaml "Pervasives.( * )")
   310   (Haskell infixl 7 "*")
   311 
   312 code_const div_mod_index
   313   (SML "(fn n => fn m =>/ (n div m, n mod m))")
   314   (OCaml "(fun n -> fun m ->/ (n '/ m, n mod m))")
   315   (Haskell "divMod")
   316 
   317 code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   318   (SML "!((_ : Int.int) = _)")
   319   (OCaml "!((_ : int) = _)")
   320   (Haskell infixl 4 "==")
   321 
   322 code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   323   (SML "Int.<=/ ((_),/ (_))")
   324   (OCaml "!((_ : int) <= _)")
   325   (Haskell infix 4 "<=")
   326 
   327 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   328   (SML "Int.</ ((_),/ (_))")
   329   (OCaml "!((_ : int) < _)")
   330   (Haskell infix 4 "<")
   331 
   332 end