# HG changeset patch # User blanchet # Date 1360926609 -3600 # Node ID 65b7ccb1d96a8c8a0ce029f6bd90e5c04da12b41 # Parent 43502299c9350167002f82ad8d1b0a3aee48bf5c# Parent 0ede9e2266a8cd60f66fbad15ace387ce368d1c1 merge diff -r 43502299c935 -r 65b7ccb1d96a NEWS --- a/NEWS Fri Feb 15 11:36:34 2013 +0100 +++ b/NEWS Fri Feb 15 12:10:09 2013 +0100 @@ -170,6 +170,18 @@ *** HOL *** +* Numeric types mapped by default to target language numerals: +natural (replaces former code_numeral) and integer (replaces +former code_int). Conversions are available as integer_of_natural / +natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and +Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ML). +INCOMPATIBILITY. + +* Discontinued theories Code_Integer and Efficient_Nat by a more +fine-grain stack of theories Code_Target_Int, Code_Binary_Nat, +Code_Target_Nat and Code_Target_Numeral. See the tutorial on +code generation for details. INCOMPATIBILITY. + * Sledgehammer: - Added MaSh relevance filter based on machine-learning; see the diff -r 43502299c935 -r 65b7ccb1d96a src/Doc/Classes/Classes.thy --- a/src/Doc/Classes/Classes.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/Doc/Classes/Classes.thy Fri Feb 15 12:10:09 2013 +0100 @@ -600,7 +600,6 @@ text {* \noindent This maps to Haskell as follows: *} -(*<*)code_include %invisible Haskell "Natural" -(*>*) text %quotetypewriter {* @{code_stmts example (Haskell)} *} @@ -616,7 +615,6 @@ text {* \noindent In Scala, implicts are used as dictionaries: *} -(*<*)code_include %invisible Scala "Natural" -(*>*) text %quotetypewriter {* @{code_stmts example (Scala)} *} @@ -640,3 +638,4 @@ *} end + diff -r 43502299c935 -r 65b7ccb1d96a src/Doc/Classes/Setup.thy --- a/src/Doc/Classes/Setup.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/Doc/Classes/Setup.thy Fri Feb 15 12:10:09 2013 +0100 @@ -1,5 +1,5 @@ theory Setup -imports Main "~~/src/HOL/Library/Code_Integer" +imports Main begin ML_file "../antiquote_setup.ML" @@ -37,4 +37,4 @@ end *} -end \ No newline at end of file +end diff -r 43502299c935 -r 65b7ccb1d96a src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/Doc/Codegen/Adaptation.thy Fri Feb 15 12:10:09 2013 +0100 @@ -125,11 +125,30 @@ \begin{description} - \item[@{text "Code_Integer"}] represents @{text HOL} integers by - big integer literals in target languages. + \item[@{theory "Code_Numeral"}] provides additional numeric + types @{typ integer} and @{typ natural} isomorphic to types + @{typ int} and @{typ nat} respectively. Type @{typ integer} + is mapped to target-language built-in integers; @{typ natural} + is implemented as abstract type over @{typ integer}. + Useful for code setups which involve e.g.~indexing + of target-language arrays. Part of @{text "HOL-Main"}. + + \item[@{text "Code_Target_Int"}] implements type @{typ int} + by @{typ integer} and thus by target-language built-in integers. - \item[@{text "Code_Char"}] represents @{text HOL} characters by - character literals in target languages. + \item[@{text "Code_Binary_Nat"}] \label{eff_nat} implements type + @{typ nat} using a binary rather than a linear representation, + which yields a considerable speedup for computations. + Pattern matching with @{term "0\nat"} / @{const "Suc"} is eliminated + by a preprocessor. + + \item[@{text "Code_Target_Nat"}] implements type @{typ int} + by @{typ integer} and thus by target-language built-in integers; + contains @{text "Code_Binary_Nat"} as a prerequisite. + + \item[@{text "Code_Target_Numeral"}] is a convenience node + containing both @{text "Code_Target_Nat"} and + @{text "Code_Target_Int"}. \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but also offers treatment of character codes; includes @{text @@ -141,10 +160,8 @@ @{const "Suc"} is eliminated; includes @{text "Code_Integer"} and @{text "Code_Numeral"}. - \item[@{theory "Code_Numeral"}] provides an additional datatype - @{typ index} which is mapped to target-language built-in - integers. Useful for code setups which involve e.g.~indexing - of target-language arrays. Part of @{text "HOL-Main"}. + \item[@{text "Code_Char"}] represents @{text HOL} characters by + character literals in target languages. \item[@{theory "String"}] provides an additional datatype @{typ String.literal} which is isomorphic to strings; @{typ diff -r 43502299c935 -r 65b7ccb1d96a src/Doc/Codegen/Foundations.thy --- a/src/Doc/Codegen/Foundations.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/Doc/Codegen/Foundations.thy Fri Feb 15 12:10:09 2013 +0100 @@ -117,7 +117,7 @@ interface, transforming a list of function theorems to another list of function theorems, provided that neither the heading constant nor its type change. The @{term "0\nat"} / @{const Suc} pattern - elimination implemented in theory @{text Efficient_Nat} (see + elimination implemented in theory @{text Code_Binary_Nat} (see \secref{eff_nat}) uses this interface. \noindent The current setup of the preprocessor may be inspected diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Code_Evaluation.thy Fri Feb 15 12:10:09 2013 +0100 @@ -133,44 +133,15 @@ (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))" and "Term.Free/ ((_), (_))") +code_const "term_of \ integer \ term" + (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT") + code_const "term_of \ String.literal \ term" (Eval "HOLogic.mk'_literal") code_reserved Eval HOLogic -subsubsection {* Numeric types *} - -definition term_of_num_semiring :: "'a\semiring_div \ 'a \ term" where - "term_of_num_semiring two = (\_. dummy_term)" - -lemma (in term_syntax) term_of_num_semiring_code [code]: - "term_of_num_semiring two k = ( - if k = 1 then termify Num.One - else (if k mod two = 0 - then termify Num.Bit0 <\> term_of_num_semiring two (k div two) - else termify Num.Bit1 <\> term_of_num_semiring two (k div two)))" - by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def) - -lemma (in term_syntax) term_of_nat_code [code]: - "term_of (n::nat) = ( - if n = 0 then termify (0 :: nat) - else termify (numeral :: num \ nat) <\> term_of_num_semiring (2::nat) n)" - by (simp only: term_of_anything) - -lemma (in term_syntax) term_of_code_numeral_code [code]: - "term_of (k::code_numeral) = ( - if k = 0 then termify (0 :: code_numeral) - else termify (numeral :: num \ code_numeral) <\> term_of_num_semiring (2::code_numeral) k)" - by (simp only: term_of_anything) - -lemma (in term_syntax) term_of_int_code [code]: - "term_of (k::int) = (if k = 0 then termify (0 :: int) - else if k < 0 then termify (neg_numeral :: num \ int) <\> term_of_num_semiring (2::int) (- k) - else termify (numeral :: num \ int) <\> term_of_num_semiring (2::int) k)" - by (simp only: term_of_anything) - - subsubsection {* Obfuscation *} print_translation {* @@ -196,6 +167,7 @@ hide_const dummy_term valapp -hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring tracing +hide_const (open) Const App Abs Free termify valtermify term_of tracing end + diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Code_Numeral.thy Fri Feb 15 12:10:09 2013 +0100 @@ -1,337 +1,614 @@ -(* Author: Florian Haftmann, TU Muenchen *) +(* Title: HOL/Code_Numeral.thy + Author: Florian Haftmann, TU Muenchen +*) -header {* Type of target language numerals *} +header {* Numeric types for code generation onto target language numerals only *} theory Code_Numeral -imports Nat_Transfer Divides +imports Nat_Transfer Divides Lifting +begin + +subsection {* Type of target language integers *} + +typedef integer = "UNIV \ int set" + morphisms int_of_integer integer_of_int .. + +setup_lifting (no_code) type_definition_integer + +lemma integer_eq_iff: + "k = l \ int_of_integer k = int_of_integer l" + by transfer rule + +lemma integer_eqI: + "int_of_integer k = int_of_integer l \ k = l" + using integer_eq_iff [of k l] by simp + +lemma int_of_integer_integer_of_int [simp]: + "int_of_integer (integer_of_int k) = k" + by transfer rule + +lemma integer_of_int_int_of_integer [simp]: + "integer_of_int (int_of_integer k) = k" + by transfer rule + +instantiation integer :: ring_1 begin -text {* - Code numerals are isomorphic to HOL @{typ nat} but - mapped to target-language builtin numerals. -*} +lift_definition zero_integer :: integer + is "0 :: int" + . + +declare zero_integer.rep_eq [simp] -subsection {* Datatype of target language numerals *} +lift_definition one_integer :: integer + is "1 :: int" + . + +declare one_integer.rep_eq [simp] -typedef code_numeral = "UNIV \ nat set" - morphisms nat_of of_nat .. +lift_definition plus_integer :: "integer \ integer \ integer" + is "plus :: int \ int \ int" + . + +declare plus_integer.rep_eq [simp] -lemma of_nat_nat_of [simp]: - "of_nat (nat_of k) = k" - by (rule nat_of_inverse) +lift_definition uminus_integer :: "integer \ integer" + is "uminus :: int \ int" + . + +declare uminus_integer.rep_eq [simp] -lemma nat_of_of_nat [simp]: - "nat_of (of_nat n) = n" - by (rule of_nat_inverse) (rule UNIV_I) +lift_definition minus_integer :: "integer \ integer \ integer" + is "minus :: int \ int \ int" + . + +declare minus_integer.rep_eq [simp] -lemma [measure_function]: - "is_measure nat_of" by (rule is_measure_trivial) +lift_definition times_integer :: "integer \ integer \ integer" + is "times :: int \ int \ int" + . + +declare times_integer.rep_eq [simp] -lemma code_numeral: - "(\n\code_numeral. PROP P n) \ (\n\nat. PROP P (of_nat n))" -proof - fix n :: nat - assume "\n\code_numeral. PROP P n" - then show "PROP P (of_nat n)" . -next - fix n :: code_numeral - assume "\n\nat. PROP P (of_nat n)" - then have "PROP P (of_nat (nat_of n))" . - then show "PROP P n" by simp +instance proof +qed (transfer, simp add: algebra_simps)+ + +end + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (of_nat :: nat \ int) (of_nat :: nat \ integer)" + by (unfold of_nat_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (\k :: int. k :: int) (of_int :: int \ integer)" +proof - + have "fun_rel HOL.eq cr_integer (of_int :: int \ int) (of_int :: int \ integer)" + by (unfold of_int_of_nat [abs_def]) transfer_prover + then show ?thesis by (simp add: id_def) qed -lemma code_numeral_case: - assumes "\n. k = of_nat n \ P" - shows P - by (rule assms [of "nat_of k"]) simp - -lemma code_numeral_induct_raw: - assumes "\n. P (of_nat n)" - shows "P k" +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (numeral :: num \ int) (numeral :: num \ integer)" proof - - from assms have "P (of_nat (nat_of k))" . + have "fun_rel HOL.eq cr_integer (numeral :: num \ int) (\n. of_int (numeral n))" + by transfer_prover then show ?thesis by simp qed -lemma nat_of_inject [simp]: - "nat_of k = nat_of l \ k = l" - by (rule nat_of_inject) +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer (neg_numeral :: num \ int) (neg_numeral :: num \ integer)" + by (unfold neg_numeral_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \ _ \ int) (Num.sub :: _ \ _ \ integer)" + by (unfold Num.sub_def [abs_def]) transfer_prover + +lemma int_of_integer_of_nat [simp]: + "int_of_integer (of_nat n) = of_nat n" + by transfer rule + +lift_definition integer_of_nat :: "nat \ integer" + is "of_nat :: nat \ int" + . + +lemma integer_of_nat_eq_of_nat [code]: + "integer_of_nat = of_nat" + by transfer rule + +lemma int_of_integer_integer_of_nat [simp]: + "int_of_integer (integer_of_nat n) = of_nat n" + by transfer rule + +lift_definition nat_of_integer :: "integer \ nat" + is Int.nat + . -lemma of_nat_inject [simp]: - "of_nat n = of_nat m \ n = m" - by (rule of_nat_inject) (rule UNIV_I)+ +lemma nat_of_integer_of_nat [simp]: + "nat_of_integer (of_nat n) = n" + by transfer simp + +lemma int_of_integer_of_int [simp]: + "int_of_integer (of_int k) = k" + by transfer simp + +lemma nat_of_integer_integer_of_nat [simp]: + "nat_of_integer (integer_of_nat n) = n" + by transfer simp + +lemma integer_of_int_eq_of_int [simp, code_abbrev]: + "integer_of_int = of_int" + by transfer (simp add: fun_eq_iff) -instantiation code_numeral :: zero +lemma of_int_integer_of [simp]: + "of_int (int_of_integer k) = (k :: integer)" + by transfer rule + +lemma int_of_integer_numeral [simp]: + "int_of_integer (numeral k) = numeral k" + by transfer rule + +lemma int_of_integer_neg_numeral [simp]: + "int_of_integer (neg_numeral k) = neg_numeral k" + by transfer rule + +lemma int_of_integer_sub [simp]: + "int_of_integer (Num.sub k l) = Num.sub k l" + by transfer rule + +instantiation integer :: "{ring_div, equal, linordered_idom}" begin -definition [simp, code del]: - "0 = of_nat 0" +lift_definition div_integer :: "integer \ integer \ integer" + is "Divides.div :: int \ int \ int" + . + +declare div_integer.rep_eq [simp] + +lift_definition mod_integer :: "integer \ integer \ integer" + is "Divides.mod :: int \ int \ int" + . + +declare mod_integer.rep_eq [simp] + +lift_definition abs_integer :: "integer \ integer" + is "abs :: int \ int" + . + +declare abs_integer.rep_eq [simp] -instance .. +lift_definition sgn_integer :: "integer \ integer" + is "sgn :: int \ int" + . + +declare sgn_integer.rep_eq [simp] + +lift_definition less_eq_integer :: "integer \ integer \ bool" + is "less_eq :: int \ int \ bool" + . + +lift_definition less_integer :: "integer \ integer \ bool" + is "less :: int \ int \ bool" + . + +lift_definition equal_integer :: "integer \ integer \ bool" + is "HOL.equal :: int \ int \ bool" + . + +instance proof +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+ end -definition Suc where [simp]: - "Suc k = of_nat (Nat.Suc (nat_of k))" +lemma [transfer_rule]: + "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \ _ \ int) (min :: _ \ _ \ integer)" + by (unfold min_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \ _ \ int) (max :: _ \ _ \ integer)" + by (unfold max_def [abs_def]) transfer_prover + +lemma int_of_integer_min [simp]: + "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)" + by transfer rule + +lemma int_of_integer_max [simp]: + "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)" + by transfer rule -rep_datatype "0 \ code_numeral" Suc -proof - - fix P :: "code_numeral \ bool" - fix k :: code_numeral - assume "P 0" then have init: "P (of_nat 0)" by simp - assume "\k. P k \ P (Suc k)" - then have "\n. P (of_nat n) \ P (Suc (of_nat n))" . - then have step: "\n. P (of_nat n) \ P (of_nat (Nat.Suc n))" by simp - from init step have "P (of_nat (nat_of k))" - by (induct ("nat_of k")) simp_all - then show "P k" by simp -qed simp_all +lemma nat_of_integer_non_positive [simp]: + "k \ 0 \ nat_of_integer k = 0" + by transfer simp + +lemma of_nat_of_integer [simp]: + "of_nat (nat_of_integer k) = max 0 k" + by transfer auto + -declare code_numeral_case [case_names nat, cases type: code_numeral] -declare code_numeral.induct [case_names nat, induct type: code_numeral] +subsection {* Code theorems for target language integers *} + +text {* Constructors *} -lemma code_numeral_decr [termination_simp]: - "k \ of_nat 0 \ nat_of k - Nat.Suc 0 < nat_of k" - by (cases k) simp +definition Pos :: "num \ integer" +where + [simp, code_abbrev]: "Pos = numeral" + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer numeral Pos" + by simp transfer_prover -lemma [simp, code]: - "code_numeral_size = nat_of" -proof (rule ext) - fix k - have "code_numeral_size k = nat_size (nat_of k)" - by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_def, simp_all) - also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all - finally show "code_numeral_size k = nat_of k" . -qed +definition Neg :: "num \ integer" +where + [simp, code_abbrev]: "Neg = neg_numeral" + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_integer neg_numeral Neg" + by simp transfer_prover + +code_datatype "0::integer" Pos Neg + + +text {* Auxiliary operations *} + +lift_definition dup :: "integer \ integer" + is "\k::int. k + k" + . -lemma [simp, code]: - "size = nat_of" -proof (rule ext) - fix k - show "size k = nat_of k" - by (induct k) (simp_all del: zero_code_numeral_def Suc_def, simp_all) -qed +lemma dup_code [code]: + "dup 0 = 0" + "dup (Pos n) = Pos (Num.Bit0 n)" + "dup (Neg n) = Neg (Num.Bit0 n)" + by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+ + +lift_definition sub :: "num \ num \ integer" + is "\m n. numeral m - numeral n :: int" + . -lemmas [code del] = code_numeral.recs code_numeral.cases - -lemma [code]: - "HOL.equal k l \ HOL.equal (nat_of k) (nat_of l)" - by (cases k, cases l) (simp add: equal) - -lemma [code nbe]: - "HOL.equal (k::code_numeral) k \ True" - by (rule equal_refl) +lemma sub_code [code]: + "sub Num.One Num.One = 0" + "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" + "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" + "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" + "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" + "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" + "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" + "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" + "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" + by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+ -subsection {* Basic arithmetic *} +text {* Implementations *} -instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}" -begin - -definition [simp, code del]: - "(1\code_numeral) = of_nat 1" +lemma one_integer_code [code, code_unfold]: + "1 = Pos Num.One" + by simp -definition [simp, code del]: - "n + m = of_nat (nat_of n + nat_of m)" - -definition [simp, code del]: - "n - m = of_nat (nat_of n - nat_of m)" - -definition [simp, code del]: - "n * m = of_nat (nat_of n * nat_of m)" - -definition [simp, code del]: - "n div m = of_nat (nat_of n div nat_of m)" +lemma plus_integer_code [code]: + "k + 0 = (k::integer)" + "0 + l = (l::integer)" + "Pos m + Pos n = Pos (m + n)" + "Pos m + Neg n = sub m n" + "Neg m + Pos n = sub n m" + "Neg m + Neg n = Neg (m + n)" + by (transfer, simp)+ -definition [simp, code del]: - "n mod m = of_nat (nat_of n mod nat_of m)" - -definition [simp, code del]: - "n \ m \ nat_of n \ nat_of m" - -definition [simp, code del]: - "n < m \ nat_of n < nat_of m" - -instance proof -qed (auto simp add: code_numeral distrib_right intro: mult_commute) +lemma uminus_integer_code [code]: + "uminus 0 = (0::integer)" + "uminus (Pos m) = Neg m" + "uminus (Neg m) = Pos m" + by simp_all -end - -lemma nat_of_numeral [simp]: "nat_of (numeral k) = numeral k" - by (induct k rule: num_induct) (simp_all add: numeral_inc) +lemma minus_integer_code [code]: + "k - 0 = (k::integer)" + "0 - l = uminus (l::integer)" + "Pos m - Pos n = sub m n" + "Pos m - Neg n = Pos (m + n)" + "Neg m - Pos n = Neg (m + n)" + "Neg m - Neg n = sub n m" + by (transfer, simp)+ -definition Num :: "num \ code_numeral" - where [simp, code_abbrev]: "Num = numeral" +lemma abs_integer_code [code]: + "\k\ = (if (k::integer) < 0 then - k else k)" + by simp -code_datatype "0::code_numeral" Num - -lemma one_code_numeral_code [code]: - "(1\code_numeral) = Numeral1" +lemma sgn_integer_code [code]: + "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)" by simp -lemma [code_abbrev]: "Numeral1 = (1\code_numeral)" - using one_code_numeral_code .. +lemma times_integer_code [code]: + "k * 0 = (0::integer)" + "0 * l = (0::integer)" + "Pos m * Pos n = Pos (m * n)" + "Pos m * Neg n = Neg (m * n)" + "Neg m * Pos n = Neg (m * n)" + "Neg m * Neg n = Pos (m * n)" + by simp_all + +definition divmod_integer :: "integer \ integer \ integer \ integer" +where + "divmod_integer k l = (k div l, k mod l)" + +lemma fst_divmod [simp]: + "fst (divmod_integer k l) = k div l" + by (simp add: divmod_integer_def) + +lemma snd_divmod [simp]: + "snd (divmod_integer k l) = k mod l" + by (simp add: divmod_integer_def) + +definition divmod_abs :: "integer \ integer \ integer \ integer" +where + "divmod_abs k l = (\k\ div \l\, \k\ mod \l\)" + +lemma fst_divmod_abs [simp]: + "fst (divmod_abs k l) = \k\ div \l\" + by (simp add: divmod_abs_def) + +lemma snd_divmod_abs [simp]: + "snd (divmod_abs k l) = \k\ mod \l\" + by (simp add: divmod_abs_def) -lemma plus_code_numeral_code [code nbe]: - "of_nat n + of_nat m = of_nat (n + m)" - by simp +lemma divmod_abs_terminate_code [code]: + "divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)" + "divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)" + "divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)" + "divmod_abs j 0 = (0, \j\)" + "divmod_abs 0 j = (0, 0)" + by (simp_all add: prod_eq_iff) + +lemma divmod_abs_rec_code [code]: + "divmod_abs (Pos k) (Pos l) = + (let j = sub k l in + if j < 0 then (0, Pos k) + else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))" + apply (simp add: prod_eq_iff Let_def prod_case_beta) + apply transfer + apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq) + done -lemma minus_code_numeral_code [code nbe]: - "of_nat n - of_nat m = of_nat (n - m)" +lemma divmod_integer_code [code]: + "divmod_integer k l = + (if k = 0 then (0, 0) else if l = 0 then (0, k) else + (apsnd \ times \ sgn) l (if sgn k = sgn l + then divmod_abs k l + else (let (r, s) = divmod_abs k l in + if s = 0 then (- r, 0) else (- r - 1, \l\ - s))))" +proof - + have aux1: "\k l::int. sgn k = sgn l \ k = 0 \ l = 0 \ 0 < l \ 0 < k \ l < 0 \ k < 0" + by (auto simp add: sgn_if) + have aux2: "\q::int. - int_of_integer k = int_of_integer l * q \ int_of_integer k = int_of_integer l * - q" by auto + show ?thesis + by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1) + (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) +qed + +lemma div_integer_code [code]: + "k div l = fst (divmod_integer k l)" by simp -lemma times_code_numeral_code [code nbe]: - "of_nat n * of_nat m = of_nat (n * m)" - by simp - -lemma less_eq_code_numeral_code [code nbe]: - "of_nat n \ of_nat m \ n \ m" - by simp - -lemma less_code_numeral_code [code nbe]: - "of_nat n < of_nat m \ n < m" +lemma mod_integer_code [code]: + "k mod l = snd (divmod_integer k l)" by simp -lemma code_numeral_zero_minus_one: - "(0::code_numeral) - 1 = 0" - by simp +lemma equal_integer_code [code]: + "HOL.equal 0 (0::integer) \ True" + "HOL.equal 0 (Pos l) \ False" + "HOL.equal 0 (Neg l) \ False" + "HOL.equal (Pos k) 0 \ False" + "HOL.equal (Pos k) (Pos l) \ HOL.equal k l" + "HOL.equal (Pos k) (Neg l) \ False" + "HOL.equal (Neg k) 0 \ False" + "HOL.equal (Neg k) (Pos l) \ False" + "HOL.equal (Neg k) (Neg l) \ HOL.equal k l" + by (simp_all add: equal) + +lemma equal_integer_refl [code nbe]: + "HOL.equal (k::integer) k \ True" + by (fact equal_refl) -lemma Suc_code_numeral_minus_one: - "Suc n - 1 = n" - by simp +lemma less_eq_integer_code [code]: + "0 \ (0::integer) \ True" + "0 \ Pos l \ True" + "0 \ Neg l \ False" + "Pos k \ 0 \ False" + "Pos k \ Pos l \ k \ l" + "Pos k \ Neg l \ False" + "Neg k \ 0 \ True" + "Neg k \ Pos l \ True" + "Neg k \ Neg l \ l \ k" + by simp_all + +lemma less_integer_code [code]: + "0 < (0::integer) \ False" + "0 < Pos l \ True" + "0 < Neg l \ False" + "Pos k < 0 \ False" + "Pos k < Pos l \ k < l" + "Pos k < Neg l \ False" + "Neg k < 0 \ True" + "Neg k < Pos l \ True" + "Neg k < Neg l \ l < k" + by simp_all -lemma of_nat_code [code]: - "of_nat = Nat.of_nat" -proof - fix n :: nat - have "Nat.of_nat n = of_nat n" - by (induct n) simp_all - then show "of_nat n = Nat.of_nat n" - by (rule sym) +lift_definition integer_of_num :: "num \ integer" + is "numeral :: num \ int" + . + +lemma integer_of_num [code]: + "integer_of_num num.One = 1" + "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)" + "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" + by (transfer, simp only: numeral.simps Let_def)+ + +lift_definition num_of_integer :: "integer \ num" + is "num_of_nat \ nat" + . + +lemma num_of_integer_code [code]: + "num_of_integer k = (if k \ 1 then Num.One + else let + (l, j) = divmod_integer k 2; + l' = num_of_integer l; + l'' = l' + l' + in if j = 0 then l'' else l'' + Num.One)" +proof - + { + assume "int_of_integer k mod 2 = 1" + then have "nat (int_of_integer k mod 2) = nat 1" by simp + moreover assume *: "1 < int_of_integer k" + ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib) + have "num_of_nat (nat (int_of_integer k)) = + num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" + by simp + then have "num_of_nat (nat (int_of_integer k)) = + num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" + by (simp add: mult_2) + with ** have "num_of_nat (nat (int_of_integer k)) = + num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" + by simp + } + note aux = this + show ?thesis + by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta + not_le integer_eq_iff less_eq_integer_def + nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib + mult_2 [where 'a=nat] aux add_One) qed -lemma code_numeral_not_eq_zero: "i \ of_nat 0 \ i \ 1" - by (cases i) auto - -definition nat_of_aux :: "code_numeral \ nat \ nat" where - "nat_of_aux i n = nat_of i + n" - -lemma nat_of_aux_code [code]: - "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Nat.Suc n))" - by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero) - -lemma nat_of_code [code]: - "nat_of i = nat_of_aux i 0" - by (simp add: nat_of_aux_def) - -definition div_mod :: "code_numeral \ code_numeral \ code_numeral \ code_numeral" where - [code del]: "div_mod n m = (n div m, n mod m)" - -lemma [code]: - "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))" - unfolding div_mod_def by auto - -lemma [code]: - "n div m = fst (div_mod n m)" - unfolding div_mod_def by simp - -lemma [code]: - "n mod m = snd (div_mod n m)" - unfolding div_mod_def by simp - -definition int_of :: "code_numeral \ int" where - "int_of = Nat.of_nat o nat_of" - -lemma int_of_code [code]: - "int_of k = (if k = 0 then 0 - else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" +lemma nat_of_integer_code [code]: + "nat_of_integer k = (if k \ 0 then 0 + else let + (l, j) = divmod_integer k 2; + l' = nat_of_integer l; + l'' = l' + l' + in if j = 0 then l'' else l'' + 1)" proof - - have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k" - by (rule mod_div_equality) - then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" - by simp - then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" - unfolding of_nat_mult of_nat_add by simp - then show ?thesis by (auto simp add: int_of_def mult_ac) + obtain j where "k = integer_of_int j" + proof + show "k = integer_of_int (int_of_integer k)" by simp + qed + moreover have "2 * (j div 2) = j - j mod 2" + by (simp add: zmult_div_cancel mult_commute) + ultimately show ?thesis + by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le + nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1) + (auto simp add: mult_2 [symmetric]) qed +lemma int_of_integer_code [code]: + "int_of_integer k = (if k < 0 then - (int_of_integer (- k)) + else if k = 0 then 0 + else let + (l, j) = divmod_integer k 2; + l' = 2 * int_of_integer l + in if j = 0 then l' else l' + 1)" + by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) -hide_const (open) of_nat nat_of Suc int_of +lemma integer_of_int_code [code]: + "integer_of_int k = (if k < 0 then - (integer_of_int (- k)) + else if k = 0 then 0 + else let + (l, j) = divmod_int k 2; + l' = 2 * integer_of_int l + in if j = 0 then l' else l' + 1)" + by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) + +hide_const (open) Pos Neg sub dup divmod_abs -subsection {* Code generator setup *} +subsection {* Serializer setup for target language integers *} -text {* Implementation of code numerals by bounded integers *} +code_reserved Eval int Integer abs -code_type code_numeral - (SML "int") +code_type integer + (SML "IntInf.int") (OCaml "Big'_int.big'_int") (Haskell "Integer") (Scala "BigInt") + (Eval "int") -code_instance code_numeral :: equal +code_instance integer :: equal (Haskell -) -setup {* - Numeral.add_code @{const_name Num} - false Code_Printer.literal_naive_numeral "SML" - #> fold (Numeral.add_code @{const_name Num} - false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"] -*} - -code_reserved SML Int int -code_reserved Eval Integer - -code_const "0::code_numeral" +code_const "0::integer" (SML "0") (OCaml "Big'_int.zero'_big'_int") (Haskell "0") (Scala "BigInt(0)") -code_const "plus \ code_numeral \ code_numeral \ code_numeral" - (SML "Int.+/ ((_),/ (_))") +setup {* + fold (Numeral.add_code @{const_name Code_Numeral.Pos} + false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] +*} + +setup {* + fold (Numeral.add_code @{const_name Code_Numeral.Neg} + true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] +*} + +code_const "plus :: integer \ _ \ _" + (SML "IntInf.+ ((_), (_))") (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") (Scala infixl 7 "+") (Eval infixl 8 "+") -code_const "minus \ code_numeral \ code_numeral \ code_numeral" - (SML "Int.max/ (0 : int,/ Int.-/ ((_),/ (_)))") - (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)") - (Haskell "Prelude.max/ (0 :: Integer)/ (_/ -/ _)") - (Scala "!(_/ -/ _).max(0)") - (Eval "Integer.max/ 0/ (_/ -/ _)") +code_const "uminus :: integer \ _" + (SML "IntInf.~") + (OCaml "Big'_int.minus'_big'_int") + (Haskell "negate") + (Scala "!(- _)") + (Eval "~/ _") + +code_const "minus :: integer \ _" + (SML "IntInf.- ((_), (_))") + (OCaml "Big'_int.sub'_big'_int") + (Haskell infixl 6 "-") + (Scala infixl 7 "-") + (Eval infixl 8 "-") -code_const "times \ code_numeral \ code_numeral \ code_numeral" - (SML "Int.*/ ((_),/ (_))") +code_const Code_Numeral.dup + (SML "IntInf.*/ (2,/ (_))") + (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)") + (Haskell "!(2 * _)") + (Scala "!(2 * _)") + (Eval "!(2 * _)") + +code_const Code_Numeral.sub + (SML "!(raise/ Fail/ \"sub\")") + (OCaml "failwith/ \"sub\"") + (Haskell "error/ \"sub\"") + (Scala "!sys.error(\"sub\")") + +code_const "times :: integer \ _ \ _" + (SML "IntInf.* ((_), (_))") (OCaml "Big'_int.mult'_big'_int") (Haskell infixl 7 "*") (Scala infixl 8 "*") - (Eval infixl 8 "*") + (Eval infixl 9 "*") -code_const Code_Numeral.div_mod - (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))") +code_const Code_Numeral.divmod_abs + (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") - (Haskell "divMod") + (Haskell "divMod/ (abs _)/ (abs _)") (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") - (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))") + (Eval "Integer.div'_mod/ (abs _)/ (abs _)") -code_const "HOL.equal \ code_numeral \ code_numeral \ bool" - (SML "!((_ : Int.int) = _)") +code_const "HOL.equal :: integer \ _ \ bool" + (SML "!((_ : IntInf.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infix 4 "==") (Scala infixl 5 "==") - (Eval "!((_ : int) = _)") + (Eval infixl 6 "=") -code_const "less_eq \ code_numeral \ code_numeral \ bool" - (SML "Int.<=/ ((_),/ (_))") +code_const "less_eq :: integer \ _ \ bool" + (SML "IntInf.<= ((_), (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") (Scala infixl 4 "<=") (Eval infixl 6 "<=") -code_const "less \ code_numeral \ code_numeral \ bool" - (SML "Int. _ \ bool" + (SML "IntInf.< ((_), (_))") (OCaml "Big'_int.lt'_big'_int") (Haskell infix 4 "<") (Scala infixl 4 "<") @@ -346,5 +623,321 @@ code_modulename Haskell Code_Numeral Arith + +subsection {* Type of target language naturals *} + +typedef natural = "UNIV \ nat set" + morphisms nat_of_natural natural_of_nat .. + +setup_lifting (no_code) type_definition_natural + +lemma natural_eq_iff [termination_simp]: + "m = n \ nat_of_natural m = nat_of_natural n" + by transfer rule + +lemma natural_eqI: + "nat_of_natural m = nat_of_natural n \ m = n" + using natural_eq_iff [of m n] by simp + +lemma nat_of_natural_of_nat_inverse [simp]: + "nat_of_natural (natural_of_nat n) = n" + by transfer rule + +lemma natural_of_nat_of_natural_inverse [simp]: + "natural_of_nat (nat_of_natural n) = n" + by transfer rule + +instantiation natural :: "{comm_monoid_diff, semiring_1}" +begin + +lift_definition zero_natural :: natural + is "0 :: nat" + . + +declare zero_natural.rep_eq [simp] + +lift_definition one_natural :: natural + is "1 :: nat" + . + +declare one_natural.rep_eq [simp] + +lift_definition plus_natural :: "natural \ natural \ natural" + is "plus :: nat \ nat \ nat" + . + +declare plus_natural.rep_eq [simp] + +lift_definition minus_natural :: "natural \ natural \ natural" + is "minus :: nat \ nat \ nat" + . + +declare minus_natural.rep_eq [simp] + +lift_definition times_natural :: "natural \ natural \ natural" + is "times :: nat \ nat \ nat" + . + +declare times_natural.rep_eq [simp] + +instance proof +qed (transfer, simp add: algebra_simps)+ + +end + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_natural (\n::nat. n) (of_nat :: nat \ natural)" +proof - + have "fun_rel HOL.eq cr_natural (of_nat :: nat \ nat) (of_nat :: nat \ natural)" + by (unfold of_nat_def [abs_def]) transfer_prover + then show ?thesis by (simp add: id_def) +qed + +lemma [transfer_rule]: + "fun_rel HOL.eq cr_natural (numeral :: num \ nat) (numeral :: num \ natural)" +proof - + have "fun_rel HOL.eq cr_natural (numeral :: num \ nat) (\n. of_nat (numeral n))" + by transfer_prover + then show ?thesis by simp +qed + +lemma nat_of_natural_of_nat [simp]: + "nat_of_natural (of_nat n) = n" + by transfer rule + +lemma natural_of_nat_of_nat [simp, code_abbrev]: + "natural_of_nat = of_nat" + by transfer rule + +lemma of_nat_of_natural [simp]: + "of_nat (nat_of_natural n) = n" + by transfer rule + +lemma nat_of_natural_numeral [simp]: + "nat_of_natural (numeral k) = numeral k" + by transfer rule + +instantiation natural :: "{semiring_div, equal, linordered_semiring}" +begin + +lift_definition div_natural :: "natural \ natural \ natural" + is "Divides.div :: nat \ nat \ nat" + . + +declare div_natural.rep_eq [simp] + +lift_definition mod_natural :: "natural \ natural \ natural" + is "Divides.mod :: nat \ nat \ nat" + . + +declare mod_natural.rep_eq [simp] + +lift_definition less_eq_natural :: "natural \ natural \ bool" + is "less_eq :: nat \ nat \ bool" + . + +declare less_eq_natural.rep_eq [termination_simp] + +lift_definition less_natural :: "natural \ natural \ bool" + is "less :: nat \ nat \ bool" + . + +declare less_natural.rep_eq [termination_simp] + +lift_definition equal_natural :: "natural \ natural \ bool" + is "HOL.equal :: nat \ nat \ bool" + . + +instance proof +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+ + end +lemma [transfer_rule]: + "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \ _ \ nat) (min :: _ \ _ \ natural)" + by (unfold min_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \ _ \ nat) (max :: _ \ _ \ natural)" + by (unfold max_def [abs_def]) transfer_prover + +lemma nat_of_natural_min [simp]: + "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)" + by transfer rule + +lemma nat_of_natural_max [simp]: + "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)" + by transfer rule + +lift_definition natural_of_integer :: "integer \ natural" + is "nat :: int \ nat" + . + +lift_definition integer_of_natural :: "natural \ integer" + is "of_nat :: nat \ int" + . + +lemma natural_of_integer_of_natural [simp]: + "natural_of_integer (integer_of_natural n) = n" + by transfer simp + +lemma integer_of_natural_of_integer [simp]: + "integer_of_natural (natural_of_integer k) = max 0 k" + by transfer auto + +lemma int_of_integer_of_natural [simp]: + "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)" + by transfer rule + +lemma integer_of_natural_of_nat [simp]: + "integer_of_natural (of_nat n) = of_nat n" + by transfer rule + +lemma [measure_function]: + "is_measure nat_of_natural" + by (rule is_measure_trivial) + + +subsection {* Inductive represenation of target language naturals *} + +lift_definition Suc :: "natural \ natural" + is Nat.Suc + . + +declare Suc.rep_eq [simp] + +rep_datatype "0::natural" Suc + by (transfer, fact nat.induct nat.inject nat.distinct)+ + +lemma natural_case [case_names nat, cases type: natural]: + fixes m :: natural + assumes "\n. m = of_nat n \ P" + shows P + using assms by transfer blast + +lemma [simp, code]: + "natural_size = nat_of_natural" +proof (rule ext) + fix n + show "natural_size n = nat_of_natural n" + by (induct n) simp_all +qed + +lemma [simp, code]: + "size = nat_of_natural" +proof (rule ext) + fix n + show "size n = nat_of_natural n" + by (induct n) simp_all +qed + +lemma natural_decr [termination_simp]: + "n \ 0 \ nat_of_natural n - Nat.Suc 0 < nat_of_natural n" + by transfer simp + +lemma natural_zero_minus_one: + "(0::natural) - 1 = 0" + by simp + +lemma Suc_natural_minus_one: + "Suc n - 1 = n" + by transfer simp + +hide_const (open) Suc + + +subsection {* Code refinement for target language naturals *} + +lift_definition Nat :: "integer \ natural" + is nat + . + +lemma [code_post]: + "Nat 0 = 0" + "Nat 1 = 1" + "Nat (numeral k) = numeral k" + by (transfer, simp)+ + +lemma [code abstype]: + "Nat (integer_of_natural n) = n" + by transfer simp + +lemma [code abstract]: + "integer_of_natural (natural_of_nat n) = of_nat n" + by simp + +lemma [code abstract]: + "integer_of_natural (natural_of_integer k) = max 0 k" + by simp + +lemma [code_abbrev]: + "natural_of_integer (Code_Numeral.Pos k) = numeral k" + by transfer simp + +lemma [code abstract]: + "integer_of_natural 0 = 0" + by transfer simp + +lemma [code abstract]: + "integer_of_natural 1 = 1" + by transfer simp + +lemma [code abstract]: + "integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1" + by transfer simp + +lemma [code]: + "nat_of_natural = nat_of_integer \ integer_of_natural" + by transfer (simp add: fun_eq_iff) + +lemma [code, code_unfold]: + "natural_case f g n = (if n = 0 then f else g (n - 1))" + by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def) + +declare natural.recs [code del] + +lemma [code abstract]: + "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" + by transfer simp + +lemma [code abstract]: + "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)" + by transfer simp + +lemma [code abstract]: + "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" + by transfer (simp add: of_nat_mult) + +lemma [code abstract]: + "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" + by transfer (simp add: zdiv_int) + +lemma [code abstract]: + "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" + by transfer (simp add: zmod_int) + +lemma [code]: + "HOL.equal m n \ HOL.equal (integer_of_natural m) (integer_of_natural n)" + by transfer (simp add: equal) + +lemma [code nbe]: + "HOL.equal n (n::natural) \ True" + by (simp add: equal) + +lemma [code]: + "m \ n \ integer_of_natural m \ integer_of_natural n" + by transfer simp + +lemma [code]: + "m < n \ integer_of_natural m < integer_of_natural n" + by transfer simp + +hide_const (open) Nat + + +code_reflect Code_Numeral + datatypes natural = _ + functions integer_of_natural natural_of_integer + +end + diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Codegenerator_Test/Candidates_Pretty.thy --- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Fri Feb 15 12:10:09 2013 +0100 @@ -4,7 +4,7 @@ header {* Generating code using pretty literals and natural number literals *} theory Candidates_Pretty -imports Candidates Code_Char_ord Efficient_Nat +imports Candidates Code_Char_ord Code_Target_Numeral begin end diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Codegenerator_Test/Generate_Pretty.thy --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Fri Feb 15 12:10:09 2013 +0100 @@ -10,9 +10,6 @@ lemma [code, code del]: "nat_of_char = nat_of_char" .. lemma [code, code del]: "char_of_nat = char_of_nat" .. -declare Quickcheck_Narrowing.one_code_int_code [code del] -declare Quickcheck_Narrowing.int_of_code [code del] - subsection {* Check whether generated code compiles *} text {* diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Fri Feb 15 12:10:09 2013 +0100 @@ -9,7 +9,7 @@ "~~/src/HOL/Library/Float" "~~/src/HOL/Library/Reflection" "~~/src/HOL/Decision_Procs/Dense_Linear_Order" - "~~/src/HOL/Library/Efficient_Nat" + "~~/src/HOL/Library/Code_Target_Numeral" begin declare powr_numeral[simp] @@ -3329,8 +3329,11 @@ fun term_of_bool true = @{term True} | term_of_bool false = @{term False}; + val mk_int = HOLogic.mk_number @{typ int} o @{code integer_of_int}; + val dest_int = @{code int_of_integer} o snd o HOLogic.dest_number; + fun term_of_float (@{code Float} (k, l)) = - @{term Float} $ HOLogic.mk_number @{typ int} k $ HOLogic.mk_number @{typ int} l; + @{term Float} $ mk_int k $ mk_int l; fun term_of_float_float_option NONE = @{term "None :: (float \ float) option"} | term_of_float_float_option (SOME ff) = @{term "Some :: float \ float \ _"} @@ -3339,10 +3342,11 @@ val term_of_float_float_option_list = HOLogic.mk_list @{typ "(float \ float) option"} o map term_of_float_float_option; - fun nat_of_term t = HOLogic.dest_nat t handle TERM _ => snd (HOLogic.dest_number t); + fun nat_of_term t = @{code nat_of_integer} + (HOLogic.dest_nat t handle TERM _ => snd (HOLogic.dest_number t)); fun float_of_term (@{term Float} $ k $ l) = - @{code Float} (snd (HOLogic.dest_number k), snd (HOLogic.dest_number l)) + @{code Float} (dest_int k, dest_int l) | float_of_term t = bad t; fun floatarith_of_term (@{term Add} $ a $ b) = @{code Add} (floatarith_of_term a, floatarith_of_term b) diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Fri Feb 15 12:10:09 2013 +0100 @@ -3,7 +3,7 @@ *) theory Cooper -imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" +imports Complex_Main "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" begin (* Periodicity of dvd *) @@ -1996,21 +1996,23 @@ ML {* @{code cooper_test} () *} -(* code_reflect Cooper_Procedure +(*code_reflect Cooper_Procedure functions pa - file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML" *) + file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*) oracle linzqe_oracle = {* let fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t of NONE => error "Variable not found in the list!" - | SOME n => @{code Bound} n) - | num_of_term vs @{term "0::int"} = @{code C} 0 - | num_of_term vs @{term "1::int"} = @{code C} 1 - | num_of_term vs (@{term "numeral :: _ \ int"} $ t) = @{code C} (HOLogic.dest_num t) - | num_of_term vs (@{term "neg_numeral :: _ \ int"} $ t) = @{code C} (~(HOLogic.dest_num t)) - | num_of_term vs (Bound i) = @{code Bound} i + | SOME n => @{code Bound} (@{code nat_of_integer} n)) + | num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0) + | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1) + | num_of_term vs (@{term "numeral :: _ \ int"} $ t) = + @{code C} (@{code int_of_integer} (HOLogic.dest_num t)) + | num_of_term vs (@{term "neg_numeral :: _ \ int"} $ t) = + @{code C} (@{code int_of_integer} (~(HOLogic.dest_num t))) + | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i) | num_of_term vs (@{term "uminus :: int \ int"} $ t') = @{code Neg} (num_of_term vs t') | num_of_term vs (@{term "op + :: int \ int \ int"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2) @@ -2018,9 +2020,9 @@ @{code Sub} (num_of_term vs t1, num_of_term vs t2) | num_of_term vs (@{term "op * :: int \ int \ int"} $ t1 $ t2) = (case try HOLogic.dest_number t1 - of SOME (_, i) => @{code Mul} (i, num_of_term vs t2) + of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2) | NONE => (case try HOLogic.dest_number t2 - of SOME (_, i) => @{code Mul} (i, num_of_term vs t1) + of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t1) | NONE => error "num_of_term: unsupported multiplication")) | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t); @@ -2034,7 +2036,7 @@ @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) | fm_of_term ps vs (@{term "op dvd :: int \ int \ bool"} $ t1 $ t2) = (case try HOLogic.dest_number t1 - of SOME (_, i) => @{code Dvd} (i, num_of_term vs t2) + of SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2) | NONE => error "num_of_term: unsupported dvd") | fm_of_term ps vs (@{term "op = :: bool \ bool \ bool"} $ t1 $ t2) = @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2) @@ -2058,8 +2060,11 @@ in @{code A} (fm_of_term ps vs' p) end | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); -fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT i - | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs)) +fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i) + | term_of_num vs (@{code Bound} n) = + let + val q = @{code integer_of_nat} n + in fst (the (find_first (fn (_, m) => q = m) vs)) end | term_of_num vs (@{code Neg} t') = @{term "uminus :: int \ int"} $ term_of_num vs t' | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: int \ int \ int"} $ term_of_num vs t1 $ term_of_num vs t2 @@ -2097,7 +2102,10 @@ HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (@{code Iff} (t1, t2)) = @{term "op = :: bool \ bool \ bool"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 - | term_of_fm ps vs (@{code Closed} n) = (fst o the) (find_first (fn (_, m) => m = n) ps) + | term_of_fm ps vs (@{code Closed} n) = + let + val q = @{code integer_of_nat} n + in (fst o the) (find_first (fn (_, m) => m = q) ps) end | term_of_fm ps vs (@{code NClosed} n) = term_of_fm ps vs (@{code NOT} (@{code Closed} n)); fun term_bools acc t = diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Feb 15 12:10:09 2013 +0100 @@ -4,7 +4,7 @@ theory Ferrack imports Complex_Main Dense_Linear_Order DP_Library - "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" + "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" begin section {* Quantifier elimination for @{text "\ (0, 1, +, <)"} *} @@ -1818,7 +1818,7 @@ with usubst_I[OF lp mnp stnb, where x="x" and bs="bs"] tnU smU show ?lhs by blast qed -lemma ferrack: +lemma ferrack: assumes qf: "qfree p" shows "qfree (ferrack p) \ ((Ifm bs (ferrack p)) = (\ x. Ifm (x#bs) p))" (is "_ \ (?rhs = ?lhs)") @@ -1922,12 +1922,15 @@ oracle linr_oracle = {* let -fun num_of_term vs (Free vT) = @{code Bound} (find_index (fn vT' => vT = vT') vs) - | num_of_term vs @{term "real (0::int)"} = @{code C} 0 - | num_of_term vs @{term "real (1::int)"} = @{code C} 1 - | num_of_term vs @{term "0::real"} = @{code C} 0 - | num_of_term vs @{term "1::real"} = @{code C} 1 - | num_of_term vs (Bound i) = @{code Bound} i +val mk_C = @{code C} o @{code int_of_integer}; +val mk_Bound = @{code Bound} o @{code nat_of_integer}; + +fun num_of_term vs (Free vT) = mk_Bound (find_index (fn vT' => vT = vT') vs) + | num_of_term vs @{term "real (0::int)"} = mk_C 0 + | num_of_term vs @{term "real (1::int)"} = mk_C 1 + | num_of_term vs @{term "0::real"} = mk_C 0 + | num_of_term vs @{term "1::real"} = mk_C 1 + | num_of_term vs (Bound i) = mk_Bound i | num_of_term vs (@{term "uminus :: real \ real"} $ t') = @{code Neg} (num_of_term vs t') | num_of_term vs (@{term "op + :: real \ real \ real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2) @@ -1937,10 +1940,10 @@ of @{code C} i => @{code Mul} (i, num_of_term vs t2) | _ => error "num_of_term: unsupported multiplication") | num_of_term vs (@{term "real :: int \ real"} $ t') = - (@{code C} (snd (HOLogic.dest_number t')) + (mk_C (snd (HOLogic.dest_number t')) handle TERM _ => error ("num_of_term: unknown term")) | num_of_term vs t' = - (@{code C} (snd (HOLogic.dest_number t')) + (mk_C (snd (HOLogic.dest_number t')) handle TERM _ => error ("num_of_term: unknown term")); fun fm_of_term vs @{term True} = @{code T} @@ -1963,8 +1966,9 @@ @{code A} (fm_of_term (("", dummyT) :: vs) p) | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); -fun term_of_num vs (@{code C} i) = @{term "real :: int \ real"} $ HOLogic.mk_number HOLogic.intT i - | term_of_num vs (@{code Bound} n) = Free (nth vs n) +fun term_of_num vs (@{code C} i) = @{term "real :: int \ real"} $ + HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i) + | term_of_num vs (@{code Bound} n) = Free (nth vs (@{code integer_of_nat} n)) | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \ real"} $ term_of_num vs t' | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: real \ real \ real"} $ term_of_num vs t1 $ term_of_num vs t2 @@ -2026,3 +2030,4 @@ by rferrack end + diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Fri Feb 15 12:10:09 2013 +0100 @@ -4,7 +4,7 @@ theory MIR imports Complex_Main Dense_Linear_Order DP_Library - "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" + "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" begin section {* Quantifier elimination for @{text "\ (0, 1, +, floor, <)"} *} @@ -5521,14 +5521,18 @@ oracle mirfr_oracle = {* fn (proofs, ct) => let +val mk_C = @{code C} o @{code int_of_integer}; +val mk_Dvd = @{code Dvd} o apfst @{code int_of_integer}; +val mk_Bound = @{code Bound} o @{code nat_of_integer}; + fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t of NONE => error "Variable not found in the list!" - | SOME n => @{code Bound} n) - | num_of_term vs @{term "real (0::int)"} = @{code C} 0 - | num_of_term vs @{term "real (1::int)"} = @{code C} 1 - | num_of_term vs @{term "0::real"} = @{code C} 0 - | num_of_term vs @{term "1::real"} = @{code C} 1 - | num_of_term vs (Bound i) = @{code Bound} i + | SOME n => mk_Bound n) + | num_of_term vs @{term "real (0::int)"} = mk_C 0 + | num_of_term vs @{term "real (1::int)"} = mk_C 1 + | num_of_term vs @{term "0::real"} = mk_C 0 + | num_of_term vs @{term "1::real"} = mk_C 1 + | num_of_term vs (Bound i) = mk_Bound i | num_of_term vs (@{term "uminus :: real \ real"} $ t') = @{code Neg} (num_of_term vs t') | num_of_term vs (@{term "op + :: real \ real \ real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2) @@ -5539,17 +5543,17 @@ of @{code C} i => @{code Mul} (i, num_of_term vs t2) | _ => error "num_of_term: unsupported Multiplication") | num_of_term vs (@{term "real :: int \ real"} $ (@{term "numeral :: _ \ int"} $ t')) = - @{code C} (HOLogic.dest_num t') + mk_C (HOLogic.dest_num t') | num_of_term vs (@{term "real :: int \ real"} $ (@{term "neg_numeral :: _ \ int"} $ t')) = - @{code C} (~ (HOLogic.dest_num t')) + mk_C (~ (HOLogic.dest_num t')) | num_of_term vs (@{term "real :: int \ real"} $ (@{term "floor :: real \ int"} $ t')) = @{code Floor} (num_of_term vs t') | num_of_term vs (@{term "real :: int \ real"} $ (@{term "ceiling :: real \ int"} $ t')) = @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t'))) | num_of_term vs (@{term "numeral :: _ \ real"} $ t') = - @{code C} (HOLogic.dest_num t') + mk_C (HOLogic.dest_num t') | num_of_term vs (@{term "neg_numeral :: _ \ real"} $ t') = - @{code C} (~ (HOLogic.dest_num t')) + mk_C (~ (HOLogic.dest_num t')) | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t); fun fm_of_term vs @{term True} = @{code T} @@ -5561,9 +5565,9 @@ | fm_of_term vs (@{term "op = :: real \ real \ bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \ real"} $ (@{term "numeral :: _ \ int"} $ t1)) $ t2) = - @{code Dvd} (HOLogic.dest_num t1, num_of_term vs t2) + mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2) | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \ real"} $ (@{term "neg_numeral :: _ \ int"} $ t1)) $ t2) = - @{code Dvd} (~ (HOLogic.dest_num t1), num_of_term vs t2) + mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2) | fm_of_term vs (@{term "op = :: bool \ bool \ bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2) | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) = @@ -5580,8 +5584,12 @@ @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); -fun term_of_num vs (@{code C} i) = @{term "real :: int \ real"} $ HOLogic.mk_number HOLogic.intT i - | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs)) +fun term_of_num vs (@{code C} i) = @{term "real :: int \ real"} $ + HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i) + | term_of_num vs (@{code Bound} n) = + let + val m = @{code integer_of_nat} n; + in fst (the (find_first (fn (_, q) => m = q) vs)) end | term_of_num vs (@{code Neg} (@{code Floor} (@{code Neg} t'))) = @{term "real :: int \ real"} $ (@{term "ceiling :: real \ int"} $ term_of_num vs t') | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \ real"} $ term_of_num vs t' @@ -5660,3 +5668,4 @@ by mir end + diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Feb 15 12:10:09 2013 +0100 @@ -6,7 +6,7 @@ theory Parametric_Ferrante_Rackoff imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library - "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" + "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" begin subsection {* Terms *} @@ -2795,6 +2795,10 @@ fun binopT T = T --> T --> T; fun relT T = T --> T --> @{typ bool}; +val mk_C = @{code C} o pairself @{code int_of_integer}; +val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer}; +val mk_Bound = @{code Bound} o @{code nat_of_integer}; + val dest_num = snd o HOLogic.dest_number; fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t) @@ -2812,19 +2816,19 @@ | num_of_term ps (Const (@{const_name Groups.plus}, _) $ a $ b) = @{code poly.Add} (num_of_term ps a, num_of_term ps b) | num_of_term ps (Const (@{const_name Groups.minus}, _) $ a $ b) = @{code poly.Sub} (num_of_term ps a, num_of_term ps b) | num_of_term ps (Const (@{const_name Groups.times}, _) $ a $ b) = @{code poly.Mul} (num_of_term ps a, num_of_term ps b) - | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, dest_nat n) - | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = @{code poly.C} (dest_num a, dest_num b) + | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n)) + | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = mk_C (dest_num a, dest_num b) | num_of_term ps t = (case try_dest_num t - of SOME k => @{code poly.C} (k, 1) - | NONE => @{code poly.Bound} (the_index ps t)); + of SOME k => mk_C (k, 1) + | NONE => mk_poly_Bound (the_index ps t)); fun tm_of_term fs ps (Const(@{const_name Groups.uminus}, _) $ t) = @{code Neg} (tm_of_term fs ps t) | tm_of_term fs ps (Const(@{const_name Groups.plus}, _) $ a $ b) = @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b) | tm_of_term fs ps (Const(@{const_name Groups.minus}, _) $ a $ b) = @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b) | tm_of_term fs ps (Const(@{const_name Groups.times}, _) $ a $ b) = @{code Mul} (num_of_term ps a, tm_of_term fs ps b) | tm_of_term fs ps t = (@{code CP} (num_of_term ps t) - handle TERM _ => @{code Bound} (the_index fs t) - | General.Subscript => @{code Bound} (the_index fs t)); + handle TERM _ => mk_Bound (the_index fs t) + | General.Subscript => mk_Bound (the_index fs t)); fun fm_of_term fs ps @{term True} = @{code T} | fm_of_term fs ps @{term False} = @{code F} @@ -2850,21 +2854,25 @@ | fm_of_term fs ps _ = error "fm_of_term"; fun term_of_num T ps (@{code poly.C} (a, b)) = - (if b = 1 then HOLogic.mk_number T a - else if b = 0 then Const (@{const_name Groups.zero}, T) - else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T a $ HOLogic.mk_number T b) - | term_of_num T ps (@{code poly.Bound} i) = nth ps i + let + val (c, d) = pairself (@{code integer_of_int}) (a, b) + in + (if d = 1 then HOLogic.mk_number T c + else if d = 0 then Const (@{const_name Groups.zero}, T) + else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T c $ HOLogic.mk_number T d) + end + | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i) | term_of_num T ps (@{code poly.Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b | term_of_num T ps (@{code poly.Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_num T ps b | term_of_num T ps (@{code poly.Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b | term_of_num T ps (@{code poly.Neg} a) = Const (@{const_name Groups.uminus}, T --> T) $ term_of_num T ps a - | term_of_num T ps (@{code poly.Pw} (a, n)) = - Const (@{const_name Power.power}, T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT n + | term_of_num T ps (@{code poly.Pw} (a, n)) = Const (@{const_name Power.power}, + T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n) | term_of_num T ps (@{code poly.CN} (c, n, p)) = term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p))); fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p - | term_of_tm T fs ps (@{code Bound} i) = nth fs i + | term_of_tm T fs ps (@{code Bound} i) = nth fs (@{code integer_of_nat} i) | term_of_tm T fs ps (@{code Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b | term_of_tm T fs ps (@{code Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b | term_of_tm T fs ps (@{code Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b @@ -2993,3 +3001,4 @@ *) end + diff -r 43502299c935 -r 65b7ccb1d96a src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Fri Feb 15 11:36:34 2013 +0100 +++ b/src/HOL/Imperative_HOL/Array.thy Fri Feb 15 12:10:09 2013 +0100 @@ -361,38 +361,38 @@ subsubsection {* Logical intermediate layer *} definition new' where - [code del]: "new' = Array.new o Code_Numeral.nat_of" + [code del]: "new' = Array.new o nat_of_integer" lemma [code]: - "Array.new = new' o Code_Numeral.of_nat" + "Array.new = new' o of_nat" by (simp add: new'_def o_def) definition make' where - [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" + [code del]: "make' i f = Array.make (nat_of_integer i) (f o of_nat)" lemma [code]: - "Array.make n f = make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" + "Array.make n f = make' (of_nat n) (f o nat_of_integer)" by (simp add: make'_def o_def) definition len' where - [code del]: "len' a = Array.len a \= (\n. return (Code_Numeral.of_nat n))" + [code del]: "len' a = Array.len a \= (\n. return (of_nat n))" lemma [code]: - "Array.len a = len' a \= (\i. return (Code_Numeral.nat_of i))" + "Array.len a = len' a \= (\i. return (nat_of_integer i))" by (simp add: len'_def) definition nth' where - [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" + [code del]: "nth' a = Array.nth a o nat_of_integer" lemma [code]: - "Array.nth a n = nth' a (Code_Numeral.of_nat n)" + "Array.nth a n = nth' a (of_nat n)" by (simp add: nth'_def) definition upd' where - [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \ return ()" + [code del]: "upd' a i x = Array.upd (nat_of_integer i) x a \ return ()" lemma [code]: - "Array.upd i x a = upd' a (Code_Numeral.of_nat i) x \ return a" + "Array.upd i x a = upd' a (of_nat i) x \ return a" by (simp add: upd'_def upd_return) lemma [code]: @@ -501,3 +501,4 @@ code_const "HOL.equal :: 'a array \