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