haftmann@29815: (* Author: Florian Haftmann, TU Muenchen *) haftmann@24999: haftmann@24999: header {* Type of indices *} haftmann@24999: haftmann@24999: theory Code_Index haftmann@30663: imports Main haftmann@24999: begin haftmann@24999: haftmann@24999: text {* haftmann@25767: Indices are isomorphic to HOL @{typ nat} but haftmann@27104: mapped to target-language builtin integers. haftmann@24999: *} haftmann@24999: haftmann@24999: subsection {* Datatype of indices *} haftmann@24999: haftmann@29815: typedef (open) index = "UNIV \ nat set" haftmann@29815: morphisms nat_of of_nat by rule haftmann@24999: haftmann@29815: lemma of_nat_nat_of [simp]: haftmann@29815: "of_nat (nat_of k) = k" haftmann@29815: by (rule nat_of_inverse) haftmann@24999: haftmann@29815: lemma nat_of_of_nat [simp]: haftmann@29815: "nat_of (of_nat n) = n" haftmann@29815: by (rule of_nat_inverse) (rule UNIV_I) haftmann@24999: haftmann@28708: lemma [measure_function]: haftmann@29815: "is_measure nat_of" by (rule is_measure_trivial) haftmann@28708: haftmann@24999: lemma index: haftmann@29815: "(\n\index. PROP P n) \ (\n\nat. PROP P (of_nat n))" haftmann@24999: proof haftmann@25767: fix n :: nat haftmann@25767: assume "\n\index. PROP P n" haftmann@29815: then show "PROP P (of_nat n)" . haftmann@24999: next haftmann@25767: fix n :: index haftmann@29815: assume "\n\nat. PROP P (of_nat n)" haftmann@29815: then have "PROP P (of_nat (nat_of n))" . haftmann@25767: then show "PROP P n" by simp haftmann@24999: qed haftmann@24999: haftmann@26140: lemma index_case: haftmann@29815: assumes "\n. k = of_nat n \ P" haftmann@26140: shows P haftmann@29815: by (rule assms [of "nat_of k"]) simp haftmann@26140: wenzelm@26304: lemma index_induct_raw: haftmann@29815: assumes "\n. P (of_nat n)" haftmann@26140: shows "P k" haftmann@26140: proof - haftmann@29815: from assms have "P (of_nat (nat_of k))" . haftmann@26140: then show ?thesis by simp haftmann@26140: qed haftmann@26140: haftmann@29815: lemma nat_of_inject [simp]: haftmann@29815: "nat_of k = nat_of l \ k = l" haftmann@29815: by (rule nat_of_inject) haftmann@26140: haftmann@29815: lemma of_nat_inject [simp]: haftmann@29815: "of_nat n = of_nat m \ n = m" haftmann@29815: by (rule of_nat_inject) (rule UNIV_I)+ haftmann@26140: haftmann@26140: instantiation index :: zero haftmann@26140: begin haftmann@26140: haftmann@28562: definition [simp, code del]: haftmann@29815: "0 = of_nat 0" haftmann@26140: haftmann@26140: instance .. haftmann@26140: haftmann@26140: end haftmann@26140: haftmann@26140: definition [simp]: haftmann@29815: "Suc_index k = of_nat (Suc (nat_of k))" haftmann@26140: haftmann@27104: rep_datatype "0 \ index" Suc_index haftmann@26140: proof - haftmann@27104: fix P :: "index \ bool" haftmann@27104: fix k :: index haftmann@29815: assume "P 0" then have init: "P (of_nat 0)" by simp haftmann@26140: assume "\k. P k \ P (Suc_index k)" haftmann@29815: then have "\n. P (of_nat n) \ P (Suc_index (of_nat n))" . haftmann@29815: then have step: "\n. P (of_nat n) \ P (of_nat (Suc n))" by simp haftmann@29815: from init step have "P (of_nat (nat_of k))" haftmann@29815: by (induct "nat_of k") simp_all haftmann@26140: then show "P k" by simp haftmann@27104: qed simp_all haftmann@26140: haftmann@26140: declare index_case [case_names nat, cases type: index] haftmann@27104: declare index.induct [case_names nat, induct type: index] haftmann@26140: haftmann@30245: lemma index_decr [termination_simp]: haftmann@30245: "k \ Code_Index.of_nat 0 \ Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k" haftmann@30245: by (cases k) simp haftmann@30245: haftmann@30245: lemma [simp, code]: haftmann@29815: "index_size = nat_of" haftmann@26140: proof (rule ext) haftmann@26140: fix k haftmann@29815: have "index_size k = nat_size (nat_of k)" haftmann@26140: by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) haftmann@29815: also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all haftmann@29815: finally show "index_size k = nat_of k" . haftmann@26140: qed haftmann@26140: haftmann@30245: lemma [simp, code]: haftmann@29815: "size = nat_of" haftmann@26140: proof (rule ext) haftmann@26140: fix k haftmann@29815: show "size k = nat_of k" haftmann@26140: by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) haftmann@26140: qed haftmann@26140: haftmann@30245: lemmas [code del] = index.recs index.cases haftmann@30245: haftmann@28562: lemma [code]: haftmann@29815: "eq_class.eq k l \ eq_class.eq (nat_of k) (nat_of l)" haftmann@28346: by (cases k, cases l) (simp add: eq) haftmann@24999: haftmann@28351: lemma [code nbe]: haftmann@28351: "eq_class.eq (k::index) k \ True" haftmann@28351: by (rule HOL.eq_refl) haftmann@28351: haftmann@24999: haftmann@25767: subsection {* Indices as datatype of ints *} haftmann@25767: haftmann@25767: instantiation index :: number haftmann@25767: begin haftmann@24999: haftmann@25767: definition haftmann@29815: "number_of = of_nat o nat" haftmann@25767: haftmann@25767: instance .. haftmann@25767: haftmann@25767: end haftmann@24999: haftmann@29815: lemma nat_of_number [simp]: haftmann@29815: "nat_of (number_of k) = number_of k" haftmann@26264: by (simp add: number_of_index_def nat_number_of_def number_of_is_id) haftmann@26264: haftmann@24999: code_datatype "number_of \ int \ index" haftmann@24999: haftmann@24999: haftmann@24999: subsection {* Basic arithmetic *} haftmann@24999: haftmann@30926: instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}" haftmann@25767: begin haftmann@24999: haftmann@28562: definition [simp, code del]: haftmann@29815: "(1\index) = of_nat 1" haftmann@24999: haftmann@28562: definition [simp, code del]: haftmann@29815: "n + m = of_nat (nat_of n + nat_of m)" haftmann@25767: haftmann@28562: definition [simp, code del]: haftmann@29815: "n - m = of_nat (nat_of n - nat_of m)" haftmann@25767: haftmann@28562: definition [simp, code del]: haftmann@29815: "n * m = of_nat (nat_of n * nat_of m)" haftmann@25767: haftmann@28562: definition [simp, code del]: haftmann@29815: "n div m = of_nat (nat_of n div nat_of m)" haftmann@24999: haftmann@28562: definition [simp, code del]: haftmann@29815: "n mod m = of_nat (nat_of n mod nat_of m)" haftmann@24999: haftmann@28562: definition [simp, code del]: haftmann@29815: "n \ m \ nat_of n \ nat_of m" haftmann@24999: haftmann@28562: definition [simp, code del]: haftmann@29815: "n < m \ nat_of n < nat_of m" haftmann@24999: haftmann@29815: instance proof haftmann@30926: qed (auto simp add: index left_distrib div_mult_self1) haftmann@28708: haftmann@28708: end haftmann@28708: haftmann@28708: lemma zero_index_code [code inline, code]: haftmann@28708: "(0\index) = Numeral0" haftmann@28708: by (simp add: number_of_index_def Pls_def) haftmann@28708: lemma [code post]: "Numeral0 = (0\index)" haftmann@28708: using zero_index_code .. haftmann@28708: haftmann@28708: lemma one_index_code [code inline, code]: haftmann@28708: "(1\index) = Numeral1" haftmann@28708: by (simp add: number_of_index_def Pls_def Bit1_def) haftmann@28708: lemma [code post]: "Numeral1 = (1\index)" haftmann@28708: using one_index_code .. haftmann@28708: haftmann@28708: lemma plus_index_code [code nbe]: haftmann@29815: "of_nat n + of_nat m = of_nat (n + m)" haftmann@28708: by simp haftmann@28708: haftmann@28708: definition subtract_index :: "index \ index \ index" where haftmann@28708: [simp, code del]: "subtract_index = op -" haftmann@28708: haftmann@28708: lemma subtract_index_code [code nbe]: haftmann@29815: "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)" haftmann@28708: by simp haftmann@28708: haftmann@28708: lemma minus_index_code [code]: haftmann@28708: "n - m = subtract_index n m" haftmann@28708: by simp haftmann@28708: haftmann@28708: lemma times_index_code [code nbe]: haftmann@29815: "of_nat n * of_nat m = of_nat (n * m)" haftmann@28708: by simp haftmann@28708: haftmann@28708: lemma less_eq_index_code [code nbe]: haftmann@29815: "of_nat n \ of_nat m \ n \ m" haftmann@25767: by simp haftmann@24999: haftmann@28708: lemma less_index_code [code nbe]: haftmann@29815: "of_nat n < of_nat m \ n < m" haftmann@25767: by simp haftmann@24999: haftmann@26140: lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp haftmann@26140: haftmann@29815: lemma of_nat_code [code]: haftmann@29815: "of_nat = Nat.of_nat" haftmann@25918: proof haftmann@25918: fix n :: nat haftmann@29815: have "Nat.of_nat n = of_nat n" haftmann@25918: by (induct n) simp_all haftmann@29815: then show "of_nat n = Nat.of_nat n" haftmann@25918: by (rule sym) haftmann@25918: qed haftmann@25918: haftmann@29815: lemma index_not_eq_zero: "i \ of_nat 0 \ i \ 1" haftmann@25928: by (cases i) auto haftmann@25928: haftmann@29815: definition nat_of_aux :: "index \ nat \ nat" where haftmann@29815: "nat_of_aux i n = nat_of i + n" haftmann@25928: haftmann@29815: lemma nat_of_aux_code [code]: haftmann@29815: "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))" haftmann@29815: by (auto simp add: nat_of_aux_def index_not_eq_zero) haftmann@25928: haftmann@29815: lemma nat_of_code [code]: haftmann@29815: "nat_of i = nat_of_aux i 0" haftmann@29815: by (simp add: nat_of_aux_def) haftmann@25918: haftmann@28708: definition div_mod_index :: "index \ index \ index \ index" where haftmann@28562: [code del]: "div_mod_index n m = (n div m, n mod m)" haftmann@26009: haftmann@28562: lemma [code]: haftmann@26009: "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))" haftmann@26009: unfolding div_mod_index_def by auto haftmann@26009: haftmann@28562: lemma [code]: haftmann@26009: "n div m = fst (div_mod_index n m)" haftmann@26009: unfolding div_mod_index_def by simp haftmann@26009: haftmann@28562: lemma [code]: haftmann@26009: "n mod m = snd (div_mod_index n m)" haftmann@26009: unfolding div_mod_index_def by simp haftmann@26009: haftmann@31192: definition int_of :: "index \ int" where haftmann@31192: "int_of = Nat.of_nat o nat_of" haftmann@28708: haftmann@31192: lemma int_of_code [code]: haftmann@31192: "int_of k = (if k = 0 then 0 haftmann@31192: else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" haftmann@31192: by (auto simp add: int_of_def mod_div_equality') haftmann@28708: haftmann@31192: lemma (in term_syntax) term_of_index_code [code]: haftmann@31192: "Code_Eval.term_of k = haftmann@31192: Code_Eval.termify (number_of :: int \ int) <\> Code_Eval.term_of_num (2::index) k" haftmann@31192: by (simp only: term_of_anything) haftmann@28708: haftmann@31192: hide (open) const of_nat nat_of int_of haftmann@28708: haftmann@28708: haftmann@28228: subsection {* Code generator setup *} haftmann@24999: haftmann@25767: text {* Implementation of indices by bounded integers *} haftmann@25767: haftmann@24999: code_type index haftmann@24999: (SML "int") haftmann@24999: (OCaml "int") haftmann@25967: (Haskell "Int") haftmann@24999: haftmann@24999: code_instance index :: eq haftmann@24999: (Haskell -) haftmann@24999: haftmann@24999: setup {* haftmann@25928: fold (Numeral.add_code @{const_name number_index_inst.number_of_index} haftmann@25928: false false) ["SML", "OCaml", "Haskell"] haftmann@24999: *} haftmann@24999: haftmann@25918: code_reserved SML Int int haftmann@25918: code_reserved OCaml Pervasives int haftmann@24999: haftmann@24999: code_const "op + \ index \ index \ index" haftmann@25928: (SML "Int.+/ ((_),/ (_))") haftmann@25967: (OCaml "Pervasives.( + )") haftmann@24999: (Haskell infixl 6 "+") haftmann@24999: haftmann@28708: code_const "subtract_index \ index \ index \ index" haftmann@25918: (SML "Int.max/ (_/ -/ _,/ 0 : int)") haftmann@25918: (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") haftmann@25918: (Haskell "max/ (_/ -/ _)/ (0 :: Int)") haftmann@24999: haftmann@24999: code_const "op * \ index \ index \ index" haftmann@25928: (SML "Int.*/ ((_),/ (_))") haftmann@25967: (OCaml "Pervasives.( * )") haftmann@24999: (Haskell infixl 7 "*") haftmann@24999: haftmann@26009: code_const div_mod_index haftmann@29823: (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))") haftmann@29823: (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))") haftmann@26009: (Haskell "divMod") haftmann@25928: haftmann@28346: code_const "eq_class.eq \ index \ index \ bool" haftmann@24999: (SML "!((_ : Int.int) = _)") haftmann@25967: (OCaml "!((_ : int) = _)") haftmann@24999: (Haskell infixl 4 "==") haftmann@24999: haftmann@24999: code_const "op \ \ index \ index \ bool" haftmann@25928: (SML "Int.<=/ ((_),/ (_))") haftmann@25967: (OCaml "!((_ : int) <= _)") haftmann@24999: (Haskell infix 4 "<=") haftmann@24999: haftmann@24999: code_const "op < \ index \ index \ bool" haftmann@25928: (SML "Int.