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@27487: imports Plain "~~/src/HOL/Presburger" 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@26140: typedef index = "UNIV \ nat set" haftmann@26140: morphisms nat_of_index index_of_nat by rule haftmann@24999: haftmann@26140: lemma index_of_nat_nat_of_index [simp]: haftmann@26140: "index_of_nat (nat_of_index k) = k" haftmann@26140: by (rule nat_of_index_inverse) haftmann@24999: haftmann@26140: lemma nat_of_index_index_of_nat [simp]: haftmann@26140: "nat_of_index (index_of_nat n) = n" haftmann@26140: by (rule index_of_nat_inverse) haftmann@26140: (unfold index_def, rule UNIV_I) 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@26140: lemma index_case: haftmann@26140: assumes "\n. k = index_of_nat n \ P" haftmann@26140: shows P haftmann@26140: by (rule assms [of "nat_of_index k"]) simp haftmann@26140: wenzelm@26304: lemma index_induct_raw: haftmann@26140: assumes "\n. P (index_of_nat n)" haftmann@26140: shows "P k" haftmann@26140: proof - haftmann@26140: from assms have "P (index_of_nat (nat_of_index k))" . haftmann@26140: then show ?thesis by simp haftmann@26140: qed haftmann@26140: haftmann@26140: lemma nat_of_index_inject [simp]: haftmann@26140: "nat_of_index k = nat_of_index l \ k = l" haftmann@26140: by (rule nat_of_index_inject) haftmann@26140: haftmann@26140: lemma index_of_nat_inject [simp]: haftmann@26140: "index_of_nat n = index_of_nat m \ n = m" haftmann@26140: by (auto intro!: index_of_nat_inject simp add: index_def) haftmann@26140: haftmann@26140: instantiation index :: zero haftmann@26140: begin haftmann@26140: haftmann@26140: definition [simp, code func del]: haftmann@26140: "0 = index_of_nat 0" haftmann@26140: haftmann@26140: instance .. haftmann@26140: haftmann@26140: end haftmann@26140: haftmann@26140: definition [simp]: haftmann@26140: "Suc_index k = index_of_nat (Suc (nat_of_index 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@26140: assume "P 0" then have init: "P (index_of_nat 0)" by simp haftmann@26140: assume "\k. P k \ P (Suc_index k)" haftmann@27104: then have "\n. P (index_of_nat n) \ P (Suc_index (index_of_nat n))" . haftmann@26140: then have step: "\n. P (index_of_nat n) \ P (index_of_nat (Suc n))" by simp haftmann@26140: from init step have "P (index_of_nat (nat_of_index k))" haftmann@26140: by (induct "nat_of_index k") simp_all haftmann@26140: then show "P k" by simp haftmann@27104: qed simp_all haftmann@26140: haftmann@26140: lemmas [code func del] = index.recs index.cases 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@26140: lemma [code func]: haftmann@26140: "index_size = nat_of_index" haftmann@26140: proof (rule ext) haftmann@26140: fix k haftmann@26140: have "index_size k = nat_size (nat_of_index k)" haftmann@26140: by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) haftmann@26140: also have "nat_size (nat_of_index k) = nat_of_index k" by (induct "nat_of_index k") simp_all haftmann@26140: finally show "index_size k = nat_of_index k" . haftmann@26140: qed haftmann@26140: haftmann@26140: lemma [code func]: haftmann@26140: "size = nat_of_index" haftmann@26140: proof (rule ext) haftmann@26140: fix k haftmann@26140: show "size k = nat_of_index k" haftmann@26140: by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) haftmann@26140: qed haftmann@26140: haftmann@26140: lemma [code func]: haftmann@26140: "k = l \ nat_of_index k = nat_of_index l" haftmann@26140: by (cases k, cases l) simp 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@26264: lemma nat_of_index_number [simp]: haftmann@26264: "nat_of_index (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@25767: instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}" haftmann@25767: begin 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@26140: lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp haftmann@26140: 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: krauss@28042: text {* Measure function (for termination proofs) *} krauss@28042: krauss@28042: lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial) krauss@28042: 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.