haftmann@24999: (* ID: $Id$ haftmann@24999: Author: Florian Haftmann, TU Muenchen haftmann@24999: *) haftmann@24999: haftmann@24999: header {* Type of indices *} haftmann@24999: haftmann@24999: theory Code_Index haftmann@25691: imports ATP_Linkup haftmann@24999: begin haftmann@24999: haftmann@24999: text {* haftmann@25767: Indices are isomorphic to HOL @{typ nat} but haftmann@24999: mapped to target-language builtin integers haftmann@24999: *} haftmann@24999: haftmann@24999: subsection {* Datatype of indices *} haftmann@24999: haftmann@25767: datatype index = index_of_nat nat haftmann@24999: haftmann@25967: lemma [code func]: haftmann@25967: "index_size k = 0" haftmann@25967: by (cases k) simp haftmann@25967: haftmann@24999: lemmas [code func del] = index.recs index.cases haftmann@24999: haftmann@25767: primrec haftmann@25767: nat_of_index :: "index \ nat" haftmann@24999: where haftmann@25767: "nat_of_index (index_of_nat k) = k" haftmann@25767: lemmas [code func del] = nat_of_index.simps haftmann@24999: haftmann@24999: lemma index_id [simp]: haftmann@25767: "index_of_nat (nat_of_index n) = n" haftmann@25767: by (cases n) simp_all haftmann@25767: haftmann@25767: lemma nat_of_index_inject [simp]: haftmann@25767: "nat_of_index n = nat_of_index m \ n = m" haftmann@25767: by (cases n) auto haftmann@24999: haftmann@24999: lemma index: haftmann@25767: "(\n\index. PROP P n) \ (\n\nat. PROP P (index_of_nat n))" haftmann@24999: proof haftmann@25767: fix n :: nat haftmann@25767: assume "\n\index. PROP P n" haftmann@25767: then show "PROP P (index_of_nat n)" . haftmann@24999: next haftmann@25767: fix n :: index haftmann@25767: assume "\n\nat. PROP P (index_of_nat n)" haftmann@25767: then have "PROP P (index_of_nat (nat_of_index n))" . haftmann@25767: then show "PROP P n" by simp haftmann@24999: qed haftmann@24999: haftmann@25767: lemma [code func]: "size (n\index) = 0" haftmann@25767: by (cases n) simp_all haftmann@24999: 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@25767: "number_of = index_of_nat o nat" haftmann@25767: haftmann@25767: instance .. haftmann@25767: haftmann@25767: end haftmann@24999: haftmann@24999: code_datatype "number_of \ int \ index" haftmann@24999: haftmann@24999: haftmann@24999: subsection {* Basic arithmetic *} haftmann@24999: haftmann@25767: instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" haftmann@25767: begin haftmann@24999: haftmann@25767: definition [simp, code func del]: haftmann@25767: "(0\index) = index_of_nat 0" haftmann@24999: haftmann@24999: lemma zero_index_code [code inline, code func]: haftmann@24999: "(0\index) = Numeral0" haftmann@25767: by (simp add: number_of_index_def Pls_def) haftmann@25967: lemma [code post]: "Numeral0 = (0\index)" haftmann@25967: using zero_index_code .. haftmann@25767: haftmann@25767: definition [simp, code func del]: haftmann@25767: "(1\index) = index_of_nat 1" haftmann@24999: haftmann@24999: lemma one_index_code [code inline, code func]: haftmann@24999: "(1\index) = Numeral1" huffman@26086: by (simp add: number_of_index_def Pls_def Bit1_def) haftmann@25967: lemma [code post]: "Numeral1 = (1\index)" haftmann@25967: using one_index_code .. haftmann@25767: haftmann@25767: definition [simp, code func del]: haftmann@25767: "n + m = index_of_nat (nat_of_index n + nat_of_index m)" haftmann@25767: haftmann@25767: lemma plus_index_code [code func]: haftmann@25767: "index_of_nat n + index_of_nat m = index_of_nat (n + m)" haftmann@25767: by simp haftmann@25767: haftmann@25767: definition [simp, code func del]: haftmann@25767: "n - m = index_of_nat (nat_of_index n - nat_of_index m)" haftmann@25767: haftmann@25767: definition [simp, code func del]: haftmann@25767: "n * m = index_of_nat (nat_of_index n * nat_of_index m)" haftmann@25767: haftmann@25767: lemma times_index_code [code func]: haftmann@25767: "index_of_nat n * index_of_nat m = index_of_nat (n * m)" haftmann@24999: by simp haftmann@24999: haftmann@25767: definition [simp, code func del]: haftmann@25767: "n div m = index_of_nat (nat_of_index n div nat_of_index m)" haftmann@24999: haftmann@25767: definition [simp, code func del]: haftmann@25767: "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)" haftmann@24999: haftmann@25767: lemma div_index_code [code func]: haftmann@25767: "index_of_nat n div index_of_nat m = index_of_nat (n div m)" haftmann@25767: by simp haftmann@25335: haftmann@25767: lemma mod_index_code [code func]: haftmann@25767: "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)" haftmann@25767: by simp haftmann@24999: haftmann@25767: definition [simp, code func del]: haftmann@25767: "n \ m \ nat_of_index n \ nat_of_index m" haftmann@24999: haftmann@25767: definition [simp, code func del]: haftmann@25767: "n < m \ nat_of_index n < nat_of_index m" haftmann@24999: haftmann@25767: lemma less_eq_index_code [code func]: haftmann@25767: "index_of_nat n \ index_of_nat m \ n \ m" haftmann@25767: by simp haftmann@24999: haftmann@25767: lemma less_index_code [code func]: haftmann@25767: "index_of_nat n < index_of_nat m \ n < m" haftmann@25767: by simp haftmann@24999: haftmann@25767: instance by default (auto simp add: left_distrib index) haftmann@25767: haftmann@25767: end haftmann@24999: haftmann@25928: lemma index_of_nat_code [code]: haftmann@25918: "index_of_nat = of_nat" haftmann@25918: proof haftmann@25918: fix n :: nat haftmann@25918: have "of_nat n = index_of_nat n" haftmann@25918: by (induct n) simp_all haftmann@25918: then show "index_of_nat n = of_nat n" haftmann@25918: by (rule sym) haftmann@25918: qed haftmann@25918: haftmann@25928: lemma index_not_eq_zero: "i \ index_of_nat 0 \ i \ 1" haftmann@25928: by (cases i) auto haftmann@25928: haftmann@25928: definition haftmann@25928: nat_of_index_aux :: "index \ nat \ nat" haftmann@25928: where haftmann@25928: "nat_of_index_aux i n = nat_of_index i + n" haftmann@25928: haftmann@25928: lemma nat_of_index_aux_code [code]: haftmann@25928: "nat_of_index_aux i n = (if i = 0 then n else nat_of_index_aux (i - 1) (Suc n))" haftmann@25928: by (auto simp add: nat_of_index_aux_def index_not_eq_zero) haftmann@25928: haftmann@25928: lemma nat_of_index_code [code]: haftmann@25928: "nat_of_index i = nat_of_index_aux i 0" haftmann@25928: by (simp add: nat_of_index_aux_def) haftmann@25918: haftmann@24999: haftmann@24999: subsection {* ML interface *} haftmann@24999: haftmann@24999: ML {* haftmann@24999: structure Index = haftmann@24999: struct haftmann@24999: haftmann@25928: fun mk k = HOLogic.mk_number @{typ index} k; haftmann@24999: haftmann@24999: end; haftmann@24999: *} haftmann@24999: haftmann@24999: haftmann@26009: subsection {* Specialized @{term "op - \ index \ index \ index"}, haftmann@26009: @{term "op div \ index \ index \ index"} and @{term "op mod \ index \ index \ index"} haftmann@26009: operations *} haftmann@26009: haftmann@26009: definition haftmann@26009: minus_index_aux :: "index \ index \ index" haftmann@26009: where haftmann@26009: [code func del]: "minus_index_aux = op -" haftmann@26009: haftmann@26009: lemma [code func]: "op - = minus_index_aux" haftmann@26009: using minus_index_aux_def .. haftmann@26009: haftmann@26009: definition haftmann@26009: div_mod_index :: "index \ index \ index \ index" haftmann@26009: where haftmann@26009: [code func del]: "div_mod_index n m = (n div m, n mod m)" haftmann@26009: haftmann@26009: lemma [code func]: 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@26009: lemma [code func]: haftmann@26009: "n div m = fst (div_mod_index n m)" haftmann@26009: unfolding div_mod_index_def by simp haftmann@26009: haftmann@26009: lemma [code func]: haftmann@26009: "n mod m = snd (div_mod_index n m)" haftmann@26009: unfolding div_mod_index_def by simp haftmann@26009: haftmann@26009: haftmann@24999: subsection {* Code serialization *} 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@26009: code_const "minus_index_aux \ 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@26009: (SML "(fn n => fn m =>/ (n div m, n mod m))") haftmann@26009: (OCaml "(fun n -> fun m ->/ (n '/ m, n mod m))") haftmann@26009: (Haskell "divMod") haftmann@25928: haftmann@24999: code_const "op = \ 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.