haftmann@29815: (* Author: Florian Haftmann, TU Muenchen *) haftmann@24999: haftmann@31205: header {* Type of target language numerals *} haftmann@24999: haftmann@31205: theory Code_Numeral haftmann@33318: imports Nat_Numeral Nat_Transfer Divides haftmann@24999: begin haftmann@24999: haftmann@24999: text {* haftmann@31205: Code numerals are isomorphic to HOL @{typ nat} but haftmann@31205: mapped to target-language builtin numerals. haftmann@24999: *} haftmann@24999: haftmann@31205: subsection {* Datatype of target language numerals *} haftmann@24999: haftmann@31205: typedef (open) code_numeral = "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@31205: lemma code_numeral: haftmann@31205: "(\n\code_numeral. PROP P n) \ (\n\nat. PROP P (of_nat n))" haftmann@24999: proof haftmann@25767: fix n :: nat haftmann@31205: assume "\n\code_numeral. PROP P n" haftmann@29815: then show "PROP P (of_nat n)" . haftmann@24999: next haftmann@31205: fix n :: code_numeral 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@31205: lemma code_numeral_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: haftmann@31205: lemma code_numeral_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@31205: instantiation code_numeral :: 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@31205: "Suc_code_numeral k = of_nat (Suc (nat_of k))" haftmann@26140: haftmann@31205: rep_datatype "0 \ code_numeral" Suc_code_numeral haftmann@26140: proof - haftmann@31205: fix P :: "code_numeral \ bool" haftmann@31205: fix k :: code_numeral haftmann@29815: assume "P 0" then have init: "P (of_nat 0)" by simp haftmann@31205: assume "\k. P k \ P (Suc_code_numeral k)" haftmann@31205: then have "\n. P (of_nat n) \ P (Suc_code_numeral (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@31205: declare code_numeral_case [case_names nat, cases type: code_numeral] haftmann@31205: declare code_numeral.induct [case_names nat, induct type: code_numeral] haftmann@26140: haftmann@31205: lemma code_numeral_decr [termination_simp]: haftmann@31205: "k \ of_nat 0 \ nat_of k - Suc 0 < nat_of k" haftmann@30245: by (cases k) simp haftmann@30245: haftmann@30245: lemma [simp, code]: haftmann@31205: "code_numeral_size = nat_of" haftmann@26140: proof (rule ext) haftmann@26140: fix k haftmann@31205: have "code_numeral_size k = nat_size (nat_of k)" haftmann@31205: by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all) haftmann@29815: also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all haftmann@31205: finally show "code_numeral_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@31205: by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all) haftmann@26140: qed haftmann@26140: haftmann@31205: lemmas [code del] = code_numeral.recs code_numeral.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@31205: "eq_class.eq (k::code_numeral) k \ True" haftmann@28351: by (rule HOL.eq_refl) haftmann@28351: haftmann@24999: haftmann@25767: subsection {* Indices as datatype of ints *} haftmann@25767: haftmann@31205: instantiation code_numeral :: 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@31205: by (simp add: number_of_code_numeral_def nat_number_of_def number_of_is_id) haftmann@26264: haftmann@31205: code_datatype "number_of \ int \ code_numeral" haftmann@24999: haftmann@24999: haftmann@24999: subsection {* Basic arithmetic *} haftmann@24999: haftmann@31205: instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}" haftmann@25767: begin haftmann@24999: haftmann@28562: definition [simp, code del]: haftmann@31205: "(1\code_numeral) = 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@33340: qed (auto simp add: code_numeral left_distrib intro: mult_commute) haftmann@28708: haftmann@28708: end haftmann@28708: haftmann@32069: lemma zero_code_numeral_code [code, code_unfold]: haftmann@31205: "(0\code_numeral) = Numeral0" haftmann@31205: by (simp add: number_of_code_numeral_def Pls_def) haftmann@31998: lemma [code_post]: "Numeral0 = (0\code_numeral)" haftmann@31205: using zero_code_numeral_code .. haftmann@28708: haftmann@32069: lemma one_code_numeral_code [code, code_unfold]: haftmann@31205: "(1\code_numeral) = Numeral1" haftmann@31205: by (simp add: number_of_code_numeral_def Pls_def Bit1_def) haftmann@31998: lemma [code_post]: "Numeral1 = (1\code_numeral)" haftmann@31205: using one_code_numeral_code .. haftmann@28708: haftmann@31205: lemma plus_code_numeral_code [code nbe]: haftmann@29815: "of_nat n + of_nat m = of_nat (n + m)" haftmann@28708: by simp haftmann@28708: haftmann@31205: definition subtract_code_numeral :: "code_numeral \ code_numeral \ code_numeral" where haftmann@31205: [simp, code del]: "subtract_code_numeral = op -" haftmann@28708: haftmann@31205: lemma subtract_code_numeral_code [code nbe]: haftmann@31205: "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)" haftmann@28708: by simp haftmann@28708: haftmann@31205: lemma minus_code_numeral_code [code]: haftmann@31205: "n - m = subtract_code_numeral n m" haftmann@28708: by simp haftmann@28708: haftmann@31205: lemma times_code_numeral_code [code nbe]: haftmann@29815: "of_nat n * of_nat m = of_nat (n * m)" haftmann@28708: by simp haftmann@28708: haftmann@31205: lemma less_eq_code_numeral_code [code nbe]: haftmann@29815: "of_nat n \ of_nat m \ n \ m" haftmann@25767: by simp haftmann@24999: haftmann@31205: lemma less_code_numeral_code [code nbe]: haftmann@29815: "of_nat n < of_nat m \ n < m" haftmann@25767: by simp haftmann@24999: haftmann@31266: lemma code_numeral_zero_minus_one: haftmann@31266: "(0::code_numeral) - 1 = 0" haftmann@31266: by simp haftmann@31266: haftmann@31266: lemma Suc_code_numeral_minus_one: haftmann@31266: "Suc_code_numeral n - 1 = n" haftmann@31266: 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@31205: lemma code_numeral_not_eq_zero: "i \ of_nat 0 \ i \ 1" haftmann@25928: by (cases i) auto haftmann@25928: haftmann@31205: definition nat_of_aux :: "code_numeral \ 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@31205: by (auto simp add: nat_of_aux_def code_numeral_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@31205: definition div_mod_code_numeral :: "code_numeral \ code_numeral \ code_numeral \ code_numeral" where haftmann@31205: [code del]: "div_mod_code_numeral n m = (n div m, n mod m)" haftmann@26009: haftmann@28562: lemma [code]: haftmann@31205: "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))" haftmann@31205: unfolding div_mod_code_numeral_def by auto haftmann@26009: haftmann@28562: lemma [code]: haftmann@31205: "n div m = fst (div_mod_code_numeral n m)" haftmann@31205: unfolding div_mod_code_numeral_def by simp haftmann@26009: haftmann@28562: lemma [code]: haftmann@31205: "n mod m = snd (div_mod_code_numeral n m)" haftmann@31205: unfolding div_mod_code_numeral_def by simp haftmann@26009: haftmann@31205: definition int_of :: "code_numeral \ 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@33340: proof - haftmann@33340: have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k" haftmann@33340: by (rule mod_div_equality) haftmann@33340: then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" haftmann@33340: by simp haftmann@33340: then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" haftmann@33340: unfolding int_mult zadd_int [symmetric] by simp haftmann@33340: then show ?thesis by (auto simp add: int_of_def mult_ac) haftmann@33340: qed 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@31205: code_type code_numeral haftmann@24999: (SML "int") haftmann@31377: (OCaml "Big'_int.big'_int") haftmann@25967: (Haskell "Int") haftmann@24999: haftmann@31205: code_instance code_numeral :: eq haftmann@24999: (Haskell -) haftmann@24999: haftmann@24999: setup {* haftmann@31205: fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} haftmann@31377: false false) ["SML", "Haskell"] haftmann@31377: #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml" haftmann@24999: *} haftmann@24999: haftmann@25918: code_reserved SML Int int haftmann@31377: code_reserved OCaml Big_int haftmann@24999: haftmann@31205: code_const "op + \ code_numeral \ code_numeral \ code_numeral" haftmann@25928: (SML "Int.+/ ((_),/ (_))") haftmann@31377: (OCaml "Big'_int.add'_big'_int") haftmann@24999: (Haskell infixl 6 "+") haftmann@24999: haftmann@31205: code_const "subtract_code_numeral \ code_numeral \ code_numeral \ code_numeral" haftmann@25918: (SML "Int.max/ (_/ -/ _,/ 0 : int)") haftmann@31377: (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int") haftmann@25918: (Haskell "max/ (_/ -/ _)/ (0 :: Int)") haftmann@24999: haftmann@31205: code_const "op * \ code_numeral \ code_numeral \ code_numeral" haftmann@25928: (SML "Int.*/ ((_),/ (_))") haftmann@31377: (OCaml "Big'_int.mult'_big'_int") haftmann@24999: (Haskell infixl 7 "*") haftmann@24999: haftmann@31205: code_const div_mod_code_numeral haftmann@29823: (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))") haftmann@31377: (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))") haftmann@26009: (Haskell "divMod") haftmann@25928: haftmann@31205: code_const "eq_class.eq \ code_numeral \ code_numeral \ bool" haftmann@24999: (SML "!((_ : Int.int) = _)") haftmann@31377: (OCaml "Big'_int.eq'_big'_int") haftmann@24999: (Haskell infixl 4 "==") haftmann@24999: haftmann@31205: code_const "op \ \ code_numeral \ code_numeral \ bool" haftmann@25928: (SML "Int.<=/ ((_),/ (_))") haftmann@31377: (OCaml "Big'_int.le'_big'_int") haftmann@24999: (Haskell infix 4 "<=") haftmann@24999: haftmann@31205: code_const "op < \ code_numeral \ code_numeral \ bool" haftmann@25928: (SML "Int.