# HG changeset patch # User huffman # Date 1243023736 25200 # Node ID c4c1692d4eee7a109d100c177a6f78bc74236840 # Parent 689aa7da48cc16f72aeb64ffe766f2e0c7772cd2# Parent df6945ac4193208197a69cc29ae36755c387e4f2 merged diff -r 689aa7da48cc -r c4c1692d4eee doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Fri May 22 13:18:59 2009 -0700 +++ b/doc-src/Codegen/Thy/Adaptation.thy Fri May 22 13:22:16 2009 -0700 @@ -121,14 +121,14 @@ which in general will result in higher efficiency; pattern matching with @{term "0\nat"} / @{const "Suc"} is eliminated; includes @{theory "Code_Integer"} - and @{theory "Code_Index"}. - \item[@{theory "Code_Index"}] provides an additional datatype + and @{theory "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. \item[@{theory "String"}] provides an additional datatype - @{typ message_string} which is isomorphic to strings; - @{typ message_string}s are mapped to target-language strings. + @{typ String.literal} which is isomorphic to strings; + @{typ String.literal}s are mapped to target-language strings. Useful for code setups which involve e.g. printing (error) messages. \end{description} diff -r 689aa7da48cc -r c4c1692d4eee doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Fri May 22 13:18:59 2009 -0700 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Fri May 22 13:22:16 2009 -0700 @@ -161,14 +161,14 @@ which in general will result in higher efficiency; pattern matching with \isa{{\isadigit{0}}} / \isa{Suc} is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}} - and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}. - \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype + and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}. + \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}] provides an additional datatype \isa{index} which is mapped to target-language built-in integers. Useful for code setups which involve e.g. indexing of target-language arrays. \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype - \isa{message{\isacharunderscore}string} which is isomorphic to strings; - \isa{message{\isacharunderscore}string}s are mapped to target-language strings. + \isa{String{\isachardot}literal} which is isomorphic to strings; + \isa{String{\isachardot}literal}s are mapped to target-language strings. Useful for code setups which involve e.g. printing (error) messages. \end{description} diff -r 689aa7da48cc -r c4c1692d4eee doc-src/Codegen/Thy/document/ML.tex --- a/doc-src/Codegen/Thy/document/ML.tex Fri May 22 13:18:59 2009 -0700 +++ b/doc-src/Codegen/Thy/document/ML.tex Fri May 22 13:22:16 2009 -0700 @@ -124,8 +124,8 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\ - \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\ + \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\ + \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\ \end{mldecls} \begin{description} diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Code_Eval.thy --- a/src/HOL/Code_Eval.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Code_Eval.thy Fri May 22 13:22:16 2009 -0700 @@ -5,7 +5,7 @@ header {* Term evaluation using the generic code generator *} theory Code_Eval -imports Plain Typerep +imports Plain Typerep Code_Numeral begin subsection {* Term representation *} @@ -14,7 +14,7 @@ datatype "term" = dummy_term -definition Const :: "message_string \ typerep \ term" where +definition Const :: "String.literal \ typerep \ term" where "Const _ _ = dummy_term" definition App :: "term \ term \ term" where @@ -63,10 +63,7 @@ let val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}) andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; - in - thy - |> need_inst ? add_term_of tyco raw_vs - end; + in if need_inst then add_term_of tyco raw_vs thy else thy end; in Code.type_interpretation ensure_term_of end @@ -102,10 +99,7 @@ fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = let val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; - in - thy - |> has_inst ? add_term_of_code tyco raw_vs cs - end; + in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; in Code.type_interpretation ensure_term_of_code end @@ -119,7 +113,7 @@ lemma [code, code del]: "(term_of \ typerep \ term) = term_of" .. lemma [code, code del]: "(term_of \ term \ term) = term_of" .. -lemma [code, code del]: "(term_of \ message_string \ term) = term_of" .. +lemma [code, code del]: "(term_of \ String.literal \ term) = term_of" .. lemma [code, code del]: "(Code_Eval.term_of \ 'a::{type, term_of} Predicate.pred \ Code_Eval.term) = Code_Eval.term_of" .. lemma [code, code del]: @@ -137,7 +131,7 @@ code_const Const and App (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)") -code_const "term_of \ message_string \ term" +code_const "term_of \ String.literal \ term" (Eval "HOLogic.mk'_message'_string") code_reserved Eval HOLogic @@ -215,6 +209,9 @@ else termify (uminus :: int \ int) <\> (termify (number_of :: int \ int) <\> term_of_num (2::int) (- k)))" by (simp only: term_of_anything) +lemma (in term_syntax) term_of_code_numeral_code [code]: + "term_of (k::code_numeral) = termify (number_of :: int \ code_numeral) <\> term_of_num (2::code_numeral) k" + by (simp only: term_of_anything) subsection {* Obfuscate *} diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Code_Index.thy --- a/src/HOL/Code_Index.thy Fri May 22 13:18:59 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,330 +0,0 @@ -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Type of indices *} - -theory Code_Index -imports Main -begin - -text {* - Indices are isomorphic to HOL @{typ nat} but - mapped to target-language builtin integers. -*} - -subsection {* Datatype of indices *} - -typedef (open) index = "UNIV \ nat set" - morphisms nat_of of_nat by rule - -lemma of_nat_nat_of [simp]: - "of_nat (nat_of k) = k" - by (rule nat_of_inverse) - -lemma nat_of_of_nat [simp]: - "nat_of (of_nat n) = n" - by (rule of_nat_inverse) (rule UNIV_I) - -lemma [measure_function]: - "is_measure nat_of" by (rule is_measure_trivial) - -lemma index: - "(\n\index. PROP P n) \ (\n\nat. PROP P (of_nat n))" -proof - fix n :: nat - assume "\n\index. PROP P n" - then show "PROP P (of_nat n)" . -next - fix n :: index - assume "\n\nat. PROP P (of_nat n)" - then have "PROP P (of_nat (nat_of n))" . - then show "PROP P n" by simp -qed - -lemma index_case: - assumes "\n. k = of_nat n \ P" - shows P - by (rule assms [of "nat_of k"]) simp - -lemma index_induct_raw: - assumes "\n. P (of_nat n)" - shows "P k" -proof - - from assms have "P (of_nat (nat_of k))" . - 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 of_nat_inject [simp]: - "of_nat n = of_nat m \ n = m" - by (rule of_nat_inject) (rule UNIV_I)+ - -instantiation index :: zero -begin - -definition [simp, code del]: - "0 = of_nat 0" - -instance .. - -end - -definition [simp]: - "Suc_index k = of_nat (Suc (nat_of k))" - -rep_datatype "0 \ index" Suc_index -proof - - fix P :: "index \ bool" - fix k :: index - assume "P 0" then have init: "P (of_nat 0)" by simp - assume "\k. P k \ P (Suc_index k)" - then have "\n. P (of_nat n) \ P (Suc_index (of_nat n))" . - then have step: "\n. P (of_nat n) \ P (of_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 - -declare index_case [case_names nat, cases type: index] -declare index.induct [case_names nat, induct type: index] - -lemma index_decr [termination_simp]: - "k \ Code_Index.of_nat 0 \ Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k" - by (cases k) simp - -lemma [simp, code]: - "index_size = nat_of" -proof (rule ext) - fix k - have "index_size k = nat_size (nat_of k)" - by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all) - also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all - finally show "index_size k = nat_of k" . -qed - -lemma [simp, code]: - "size = nat_of" -proof (rule ext) - fix k - show "size k = nat_of k" - by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all) -qed - -lemmas [code del] = index.recs index.cases - -lemma [code]: - "eq_class.eq k l \ eq_class.eq (nat_of k) (nat_of l)" - by (cases k, cases l) (simp add: eq) - -lemma [code nbe]: - "eq_class.eq (k::index) k \ True" - by (rule HOL.eq_refl) - - -subsection {* Indices as datatype of ints *} - -instantiation index :: number -begin - -definition - "number_of = of_nat o nat" - -instance .. - -end - -lemma nat_of_number [simp]: - "nat_of (number_of k) = number_of k" - by (simp add: number_of_index_def nat_number_of_def number_of_is_id) - -code_datatype "number_of \ int \ index" - - -subsection {* Basic arithmetic *} - -instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}" -begin - -definition [simp, code del]: - "(1\index) = of_nat 1" - -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)" - -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: index left_distrib div_mult_self1) - -end - -lemma zero_index_code [code inline, code]: - "(0\index) = Numeral0" - by (simp add: number_of_index_def Pls_def) -lemma [code post]: "Numeral0 = (0\index)" - using zero_index_code .. - -lemma one_index_code [code inline, code]: - "(1\index) = Numeral1" - by (simp add: number_of_index_def Pls_def Bit1_def) -lemma [code post]: "Numeral1 = (1\index)" - using one_index_code .. - -lemma plus_index_code [code nbe]: - "of_nat n + of_nat m = of_nat (n + m)" - by simp - -definition subtract_index :: "index \ index \ index" where - [simp, code del]: "subtract_index = op -" - -lemma subtract_index_code [code nbe]: - "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)" - by simp - -lemma minus_index_code [code]: - "n - m = subtract_index n m" - by simp - -lemma times_index_code [code nbe]: - "of_nat n * of_nat m = of_nat (n * m)" - by simp - -lemma less_eq_index_code [code nbe]: - "of_nat n \ of_nat m \ n \ m" - by simp - -lemma less_index_code [code nbe]: - "of_nat n < of_nat m \ n < m" - by simp - -lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp - -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) -qed - -lemma index_not_eq_zero: "i \ of_nat 0 \ i \ 1" - by (cases i) auto - -definition nat_of_aux :: "index \ 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) (Suc n))" - by (auto simp add: nat_of_aux_def index_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_index :: "index \ index \ index \ index" where - [code del]: "div_mod_index n m = (n div m, n mod m)" - -lemma [code]: - "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))" - unfolding div_mod_index_def by auto - -lemma [code]: - "n div m = fst (div_mod_index n m)" - unfolding div_mod_index_def by simp - -lemma [code]: - "n mod m = snd (div_mod_index n m)" - unfolding div_mod_index_def by simp - -definition int_of :: "index \ 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))" - by (auto simp add: int_of_def mod_div_equality') - -lemma (in term_syntax) term_of_index_code [code]: - "Code_Eval.term_of k = - Code_Eval.termify (number_of :: int \ int) <\> Code_Eval.term_of_num (2::index) k" - by (simp only: term_of_anything) - -hide (open) const of_nat nat_of int_of - - -subsection {* Code generator setup *} - -text {* Implementation of indices by bounded integers *} - -code_type index - (SML "int") - (OCaml "int") - (Haskell "Int") - -code_instance index :: eq - (Haskell -) - -setup {* - fold (Numeral.add_code @{const_name number_index_inst.number_of_index} - false false) ["SML", "OCaml", "Haskell"] -*} - -code_reserved SML Int int -code_reserved OCaml Pervasives int - -code_const "op + \ index \ index \ index" - (SML "Int.+/ ((_),/ (_))") - (OCaml "Pervasives.( + )") - (Haskell infixl 6 "+") - -code_const "subtract_index \ index \ index \ index" - (SML "Int.max/ (_/ -/ _,/ 0 : int)") - (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") - (Haskell "max/ (_/ -/ _)/ (0 :: Int)") - -code_const "op * \ index \ index \ index" - (SML "Int.*/ ((_),/ (_))") - (OCaml "Pervasives.( * )") - (Haskell infixl 7 "*") - -code_const div_mod_index - (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))") - (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))") - (Haskell "divMod") - -code_const "eq_class.eq \ index \ index \ bool" - (SML "!((_ : Int.int) = _)") - (OCaml "!((_ : int) = _)") - (Haskell infixl 4 "==") - -code_const "op \ \ index \ index \ bool" - (SML "Int.<=/ ((_),/ (_))") - (OCaml "!((_ : int) <= _)") - (Haskell infix 4 "<=") - -code_const "op < \ index \ index \ bool" - (SML "Int. nat set" + morphisms nat_of of_nat by rule + +lemma of_nat_nat_of [simp]: + "of_nat (nat_of k) = k" + by (rule nat_of_inverse) + +lemma nat_of_of_nat [simp]: + "nat_of (of_nat n) = n" + by (rule of_nat_inverse) (rule UNIV_I) + +lemma [measure_function]: + "is_measure nat_of" by (rule is_measure_trivial) + +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 +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" +proof - + from assms have "P (of_nat (nat_of k))" . + 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 of_nat_inject [simp]: + "of_nat n = of_nat m \ n = m" + by (rule of_nat_inject) (rule UNIV_I)+ + +instantiation code_numeral :: zero +begin + +definition [simp, code del]: + "0 = of_nat 0" + +instance .. + +end + +definition [simp]: + "Suc_code_numeral k = of_nat (Suc (nat_of k))" + +rep_datatype "0 \ code_numeral" Suc_code_numeral +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_code_numeral k)" + then have "\n. P (of_nat n) \ P (Suc_code_numeral (of_nat n))" . + then have step: "\n. P (of_nat n) \ P (of_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 + +declare code_numeral_case [case_names nat, cases type: code_numeral] +declare code_numeral.induct [case_names nat, induct type: code_numeral] + +lemma code_numeral_decr [termination_simp]: + "k \ of_nat 0 \ nat_of k - Suc 0 < nat_of k" + by (cases k) simp + +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_code_numeral_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 + +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_code_numeral_def, simp_all) +qed + +lemmas [code del] = code_numeral.recs code_numeral.cases + +lemma [code]: + "eq_class.eq k l \ eq_class.eq (nat_of k) (nat_of l)" + by (cases k, cases l) (simp add: eq) + +lemma [code nbe]: + "eq_class.eq (k::code_numeral) k \ True" + by (rule HOL.eq_refl) + + +subsection {* Indices as datatype of ints *} + +instantiation code_numeral :: number +begin + +definition + "number_of = of_nat o nat" + +instance .. + +end + +lemma nat_of_number [simp]: + "nat_of (number_of k) = number_of k" + by (simp add: number_of_code_numeral_def nat_number_of_def number_of_is_id) + +code_datatype "number_of \ int \ code_numeral" + + +subsection {* Basic arithmetic *} + +instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}" +begin + +definition [simp, code del]: + "(1\code_numeral) = of_nat 1" + +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)" + +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 left_distrib div_mult_self1) + +end + +lemma zero_code_numeral_code [code inline, code]: + "(0\code_numeral) = Numeral0" + by (simp add: number_of_code_numeral_def Pls_def) +lemma [code post]: "Numeral0 = (0\code_numeral)" + using zero_code_numeral_code .. + +lemma one_code_numeral_code [code inline, code]: + "(1\code_numeral) = Numeral1" + by (simp add: number_of_code_numeral_def Pls_def Bit1_def) +lemma [code post]: "Numeral1 = (1\code_numeral)" + using one_code_numeral_code .. + +lemma plus_code_numeral_code [code nbe]: + "of_nat n + of_nat m = of_nat (n + m)" + by simp + +definition subtract_code_numeral :: "code_numeral \ code_numeral \ code_numeral" where + [simp, code del]: "subtract_code_numeral = op -" + +lemma subtract_code_numeral_code [code nbe]: + "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)" + by simp + +lemma minus_code_numeral_code [code]: + "n - m = subtract_code_numeral n m" + 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" + by simp + +lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp + +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) +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) (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 \ code_numeral" where + [code del]: "div_mod_code_numeral n m = (n div m, n mod m)" + +lemma [code]: + "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))" + unfolding div_mod_code_numeral_def by auto + +lemma [code]: + "n div m = fst (div_mod_code_numeral n m)" + unfolding div_mod_code_numeral_def by simp + +lemma [code]: + "n mod m = snd (div_mod_code_numeral n m)" + unfolding div_mod_code_numeral_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))" + by (auto simp add: int_of_def mod_div_equality') + +hide (open) const of_nat nat_of int_of + + +subsection {* Code generator setup *} + +text {* Implementation of indices by bounded integers *} + +code_type code_numeral + (SML "int") + (OCaml "int") + (Haskell "Int") + +code_instance code_numeral :: eq + (Haskell -) + +setup {* + fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} + false false) ["SML", "OCaml", "Haskell"] +*} + +code_reserved SML Int int +code_reserved OCaml Pervasives int + +code_const "op + \ code_numeral \ code_numeral \ code_numeral" + (SML "Int.+/ ((_),/ (_))") + (OCaml "Pervasives.( + )") + (Haskell infixl 6 "+") + +code_const "subtract_code_numeral \ code_numeral \ code_numeral \ code_numeral" + (SML "Int.max/ (_/ -/ _,/ 0 : int)") + (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") + (Haskell "max/ (_/ -/ _)/ (0 :: Int)") + +code_const "op * \ code_numeral \ code_numeral \ code_numeral" + (SML "Int.*/ ((_),/ (_))") + (OCaml "Pervasives.( * )") + (Haskell infixl 7 "*") + +code_const div_mod_code_numeral + (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))") + (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))") + (Haskell "divMod") + +code_const "eq_class.eq \ code_numeral \ code_numeral \ bool" + (SML "!((_ : Int.int) = _)") + (OCaml "!((_ : int) = _)") + (Haskell infixl 4 "==") + +code_const "op \ \ code_numeral \ code_numeral \ bool" + (SML "Int.<=/ ((_),/ (_))") + (OCaml "!((_ : int) <= _)") + (Haskell infix 4 "<=") + +code_const "op < \ code_numeral \ code_numeral \ bool" + (SML "Int. id = f" by (simp add: fcomp_def) +code_const fcomp + (Eval infixl 1 "#>") + no_notation fcomp (infixl "o>" 60) diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Imperative_HOL/Array.thy Fri May 22 13:22:16 2009 -0700 @@ -6,7 +6,7 @@ header {* Monadic arrays *} theory Array -imports Heap_Monad Code_Index +imports Heap_Monad begin subsection {* Primitives *} @@ -115,47 +115,47 @@ subsubsection {* Logical intermediate layer *} definition new' where - [code del]: "new' = Array.new o Code_Index.nat_of" + [code del]: "new' = Array.new o Code_Numeral.nat_of" hide (open) const new' lemma [code]: - "Array.new = Array.new' o Code_Index.of_nat" + "Array.new = Array.new' o Code_Numeral.of_nat" by (simp add: new'_def o_def) definition of_list' where - [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)" + [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)" hide (open) const of_list' lemma [code]: - "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs" + "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs" by (simp add: of_list'_def) definition make' where - [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)" + [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" hide (open) const make' lemma [code]: - "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)" + "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" by (simp add: make'_def o_def) definition length' where - [code del]: "length' = Array.length \== liftM Code_Index.of_nat" + [code del]: "length' = Array.length \== liftM Code_Numeral.of_nat" hide (open) const length' lemma [code]: - "Array.length = Array.length' \== liftM Code_Index.nat_of" + "Array.length = Array.length' \== liftM Code_Numeral.nat_of" by (simp add: length'_def monad_simp', simp add: liftM_def comp_def monad_simp, simp add: monad_simp') definition nth' where - [code del]: "nth' a = Array.nth a o Code_Index.nat_of" + [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" hide (open) const nth' lemma [code]: - "Array.nth a n = Array.nth' a (Code_Index.of_nat n)" + "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)" by (simp add: nth'_def) definition upd' where - [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \ return ()" + [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \ return ()" hide (open) const upd' lemma [code]: - "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \ return a" + "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \ return a" by (simp add: upd'_def monad_simp upd_return) diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Imperative_HOL/Heap.thy Fri May 22 13:22:16 2009 -0700 @@ -28,11 +28,11 @@ instance int :: heap .. -instance message_string :: countable - by (rule countable_classI [of "message_string_case to_nat"]) - (auto split: message_string.splits) +instance String.literal :: countable + by (rule countable_classI [of "String.literal_case to_nat"]) + (auto split: String.literal.splits) -instance message_string :: heap .. +instance String.literal :: heap .. text {* Reflected types themselves are heap-representable *} diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri May 22 13:22:16 2009 -0700 @@ -274,7 +274,7 @@ subsubsection {* Logical intermediate layer *} definition - Fail :: "message_string \ exception" + Fail :: "String.literal \ exception" where [code del]: "Fail s = Exn" diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/IsaMakefile Fri May 22 13:22:16 2009 -0700 @@ -206,21 +206,23 @@ MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ ATP_Linkup.thy \ Code_Eval.thy \ - Code_Index.thy \ + Code_Numeral.thy \ Equiv_Relations.thy \ Groebner_Basis.thy \ Hilbert_Choice.thy \ IntDiv.thy \ Int.thy \ - Typerep.thy \ List.thy \ Main.thy \ Map.thy \ Nat_Numeral.thy \ Presburger.thy \ + Quickcheck.thy \ + Random.thy \ Recdef.thy \ SetInterval.thy \ String.thy \ + Typerep.thy \ $(SRC)/Provers/Arith/assoc_fold.ML \ $(SRC)/Provers/Arith/cancel_numeral_factor.ML \ $(SRC)/Provers/Arith/cancel_numerals.ML \ @@ -287,10 +289,8 @@ Transcendental.thy \ GCD.thy \ Parity.thy \ - Quickcheck.thy \ Lubs.thy \ PReal.thy \ - Random.thy \ Rational.thy \ RComplete.thy \ RealDef.thy \ diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Library/Bit.thy Fri May 22 13:22:16 2009 -0700 @@ -53,10 +53,10 @@ begin definition plus_bit_def: - "x + y = (case x of 0 \ y | 1 \ (case y of 0 \ 1 | 1 \ 0))" + "x + y = bit_case y (bit_case 1 0 y) x" definition times_bit_def: - "x * y = (case x of 0 \ 0 | 1 \ y)" + "x * y = bit_case 0 y x" definition uminus_bit_def [simp]: "- x = (x :: bit)" diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Library/Code_Integer.thy Fri May 22 13:22:16 2009 -0700 @@ -5,7 +5,7 @@ header {* Pretty integer literals for code generation *} theory Code_Integer -imports Main Code_Index +imports Main begin text {* @@ -91,7 +91,7 @@ (OCaml "Big'_int.lt'_big'_int") (Haskell infix 4 "<") -code_const Code_Index.int_of +code_const Code_Numeral.int_of (SML "IntInf.fromInt") (OCaml "Big'_int.big'_int'_of'_int") (Haskell "toEnum") diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Library/Efficient_Nat.thy Fri May 22 13:22:16 2009 -0700 @@ -5,7 +5,7 @@ header {* Implementation of natural numbers by target-language integers *} theory Efficient_Nat -imports Code_Index Code_Integer Main +imports Code_Integer Main begin text {* @@ -369,12 +369,12 @@ text {* Conversion from and to indices. *} -code_const Code_Index.of_nat +code_const Code_Numeral.of_nat (SML "IntInf.toInt") (OCaml "Big'_int.int'_of'_big'_int") (Haskell "fromEnum") -code_const Code_Index.nat_of +code_const Code_Numeral.nat_of (SML "IntInf.fromInt") (OCaml "Big'_int.big'_int'_of'_int") (Haskell "toEnum") diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Main.thy --- a/src/HOL/Main.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Main.thy Fri May 22 13:22:16 2009 -0700 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Code_Eval Map Recdef SAT +imports Plain Quickcheck Map Recdef SAT begin text {* diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Predicate.thy Fri May 22 13:22:16 2009 -0700 @@ -627,6 +627,9 @@ lemma eq_is_eq: "eq x y \ (x = y)" by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) +definition map :: "('a \ 'b) \ 'a pred \ 'b pred" where + "map f P = P \= (single o f)" + ML {* signature PREDICATE = sig @@ -634,6 +637,7 @@ and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq val yield: 'a pred -> ('a * 'a pred) option val yieldn: int -> 'a pred -> 'a list * 'a pred + val map: ('a -> 'b) -> 'a pred -> 'b pred end; structure Predicate : PREDICATE = @@ -658,6 +662,8 @@ fun yieldn P = anamorph yield P; +fun map f = @{code map} f; + end; *} @@ -683,7 +689,7 @@ val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate" OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]]))); -val _ = OuterSyntax.improper_command "values" "evaluate and print enumerations" +val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag ((opt_modes -- P.term) >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep (K ()))); @@ -702,6 +708,6 @@ hide (open) type pred seq hide (open) const Pred eval single bind if_pred not_pred - Empty Insert Join Seq member pred_of_seq "apply" adjunct eq + Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map end diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Product_Type.thy Fri May 22 13:22:16 2009 -0700 @@ -726,6 +726,9 @@ lemma fcomp_scomp: "(f o> g) o\ h = f o> (g o\ h)" by (simp add: expand_fun_eq scomp_apply fcomp_apply) +code_const scomp + (Eval infixl 3 "#->") + no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\" 60) diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Quickcheck.thy Fri May 22 13:22:16 2009 -0700 @@ -3,7 +3,7 @@ header {* A simple counterexample generator *} theory Quickcheck -imports Main Real Random +imports Random Code_Eval begin notation fcomp (infixl "o>" 60) @@ -13,7 +13,7 @@ subsection {* The @{text random} class *} class random = typerep + - fixes random :: "index \ Random.seed \ ('a \ (unit \ term)) \ Random.seed" + fixes random :: "code_numeral \ Random.seed \ ('a \ (unit \ term)) \ Random.seed" subsection {* Quickcheck generator *} @@ -49,7 +49,7 @@ (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \ term"}, t'))); fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i); - in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end; + in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end; fun compile_generator_expr thy t = let @@ -84,7 +84,7 @@ instantiation itself :: (typerep) random begin -definition random_itself :: "index \ Random.seed \ ('a itself \ (unit \ term)) \ Random.seed" where +definition random_itself :: "code_numeral \ Random.seed \ ('a itself \ (unit \ term)) \ Random.seed" where "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))" instance .. @@ -139,7 +139,7 @@ instantiation "fun" :: ("{eq, term_of}", "{type, random}") random begin -definition random_fun :: "index \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ Random.seed" where +definition random_fun :: "code_numeral \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ Random.seed" where "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed" instance .. @@ -154,9 +154,9 @@ instantiation nat :: random begin -definition random_nat :: "index \ Random.seed \ (nat \ (unit \ Code_Eval.term)) \ Random.seed" where +definition random_nat :: "code_numeral \ Random.seed \ (nat \ (unit \ Code_Eval.term)) \ Random.seed" where "random_nat i = Random.range (i + 1) o\ (\k. Pair ( - let n = Code_Index.nat_of k + let n = Code_Numeral.nat_of k in (n, \_. Code_Eval.term_of n)))" instance .. @@ -168,42 +168,66 @@ definition "random i = Random.range (2 * i + 1) o\ (\k. Pair ( - let j = (if k \ i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k)) + let j = (if k \ i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k)) in (j, \_. Code_Eval.term_of j)))" instance .. end -definition (in term_syntax) - valterm_fract :: "int \ (unit \ Code_Eval.term) \ int \ (unit \ Code_Eval.term) \ rat \ (unit \ Code_Eval.term)" where - [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\} k {\} l" +subsection {* Type copies *} -instantiation rat :: random -begin +setup {* +let -definition - "random i = random i o\ (\num. Random.range i o\ (\denom. Pair ( - let j = Code_Index.int_of (denom + 1) - in valterm_fract num (j, \u. Code_Eval.term_of j))))" +fun mk_random_typecopy tyco vs constr typ thy = + let + val Ts = map TFree vs; + val T = Type (tyco, Ts); + fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \ term"}) + val Ttm = mk_termifyT T; + val typtm = mk_termifyT typ; + fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts)); + fun mk_random T = mk_const @{const_name random} [T]; + val size = @{term "k\code_numeral"}; + val v = "x"; + val t_v = Free (v, typtm); + val t_constr = mk_const constr Ts; + val lhs = mk_random T $ size; + val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))] + (HOLogic.mk_return Ttm @{typ Random.seed} + (mk_const "Code_Eval.valapp" [typ, T] + $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v)) + @{typ Random.seed} (SOME Ttm, @{typ Random.seed}); + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + in + thy + |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) + |> snd + |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) + end; -instance .. +fun ensure_random_typecopy tyco thy = + let + val SOME { vs = raw_vs, constr, typ = raw_typ, ... } = + TypecopyPackage.get_info thy tyco; + val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)); + val typ = map_atyps (fn TFree (v, sort) => + TFree (v, constrain sort @{sort random})) raw_typ; + val vs' = Term.add_tfreesT typ []; + val vs = map (fn (v, sort) => + (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs; + val do_inst = Sign.of_sort thy (typ, @{sort random}); + in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end; + +in + +TypecopyPackage.interpretation ensure_random_typecopy end - -definition (in term_syntax) - valterm_ratreal :: "rat \ (unit \ Code_Eval.term) \ real \ (unit \ Code_Eval.term)" where - [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\} k" - -instantiation real :: random -begin - -definition - "random i = random i o\ (\r. Pair (valterm_ratreal r))" - -instance .. - -end +*} no_notation fcomp (infixl "o>" 60) diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Random.thy --- a/src/HOL/Random.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Random.thy Fri May 22 13:22:16 2009 -0700 @@ -3,7 +3,7 @@ header {* A HOL random engine *} theory Random -imports Code_Index +imports Code_Numeral List begin notation fcomp (infixl "o>" 60) @@ -12,21 +12,21 @@ subsection {* Auxiliary functions *} -definition inc_shift :: "index \ index \ index" where +definition inc_shift :: "code_numeral \ code_numeral \ code_numeral" where "inc_shift v k = (if v = k then 1 else k + 1)" -definition minus_shift :: "index \ index \ index \ index" where +definition minus_shift :: "code_numeral \ code_numeral \ code_numeral \ code_numeral" where "minus_shift r k l = (if k < l then r + k - l else k - l)" -fun log :: "index \ index \ index" where +fun log :: "code_numeral \ code_numeral \ code_numeral" where "log b i = (if b \ 1 \ i < b then 1 else 1 + log b (i div b))" subsection {* Random seeds *} -types seed = "index \ index" +types seed = "code_numeral \ code_numeral" -primrec "next" :: "seed \ index \ seed" where +primrec "next" :: "seed \ code_numeral \ seed" where "next (v, w) = (let k = v div 53668; v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211); @@ -42,9 +42,6 @@ primrec seed_invariant :: "seed \ bool" where "seed_invariant (v, w) \ 0 < v \ v < 9438322952 \ 0 < w \ True" -lemma if_same: "(if b then f x else f y) = f (if b then x else y)" - by (cases b) simp_all - definition split_seed :: "seed \ seed \ seed" where "split_seed s = (let (v, w) = s; @@ -58,10 +55,10 @@ subsection {* Base selectors *} -fun iterate :: "index \ ('b \ 'a \ 'b \ 'a) \ 'b \ 'a \ 'b \ 'a" where +fun iterate :: "code_numeral \ ('b \ 'a \ 'b \ 'a) \ 'b \ 'a \ 'b \ 'a" where "iterate k f x = (if k = 0 then Pair x else f x o\ iterate (k - 1) f)" -definition range :: "index \ seed \ index \ seed" where +definition range :: "code_numeral \ seed \ code_numeral \ seed" where "range k = iterate (log 2147483561 k) (\l. next o\ (\v. Pair (v + l * 2147483561))) 1 o\ (\v. Pair (v mod k))" @@ -71,23 +68,23 @@ by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps) definition select :: "'a list \ seed \ 'a \ seed" where - "select xs = range (Code_Index.of_nat (length xs)) - o\ (\k. Pair (nth xs (Code_Index.nat_of k)))" + "select xs = range (Code_Numeral.of_nat (length xs)) + o\ (\k. Pair (nth xs (Code_Numeral.nat_of k)))" lemma select: assumes "xs \ []" shows "fst (select xs s) \ set xs" proof - - from assms have "Code_Index.of_nat (length xs) > 0" by simp + from assms have "Code_Numeral.of_nat (length xs) > 0" by simp with range have - "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best + "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best then have - "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp + "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp then show ?thesis by (simp add: scomp_apply split_beta select_def) qed -primrec pick :: "(index \ 'a) list \ index \ 'a" where +primrec pick :: "(code_numeral \ 'a) list \ code_numeral \ 'a" where "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))" lemma pick_member: @@ -98,7 +95,15 @@ "pick (filter (\(k, _). k > 0) xs) = pick xs" by (induct xs) (auto simp add: expand_fun_eq) -definition select_weight :: "(index \ 'a) list \ seed \ 'a \ seed" where +lemma pick_same: + "l < length xs \ Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l" +proof (induct xs arbitrary: l) + case Nil then show ?case by simp +next + case (Cons x xs) then show ?case by (cases l) simp_all +qed + +definition select_weight :: "(code_numeral \ 'a) list \ seed \ 'a \ seed" where "select_weight xs = range (listsum (map fst xs)) o\ (\k. Pair (pick xs k))" @@ -113,7 +118,28 @@ then show ?thesis by (simp add: select_weight_def scomp_def split_def) qed -definition select_default :: "index \ 'a \ 'a \ seed \ 'a \ seed" where +lemma select_weigth_drop_zero: + "Random.select_weight (filter (\(k, _). k > 0) xs) = Random.select_weight xs" +proof - + have "listsum (map fst [(k, _)\xs . 0 < k]) = listsum (map fst xs)" + by (induct xs) auto + then show ?thesis by (simp only: select_weight_def pick_drop_zero) +qed + +lemma select_weigth_select: + assumes "xs \ []" + shows "Random.select_weight (map (Pair 1) xs) = Random.select xs" +proof - + have less: "\s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" + using assms by (intro range) simp + moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)" + by (induct xs) simp_all + ultimately show ?thesis + by (auto simp add: select_weight_def select_def scomp_def split_def + expand_fun_eq pick_same [symmetric]) +qed + +definition select_default :: "code_numeral \ 'a \ 'a \ seed \ 'a \ seed" where [code del]: "select_default k x y = range k o\ (\l. Pair (if l + 1 < k then x else y))" @@ -127,7 +153,7 @@ else range k o\ (\l. Pair (if l + 1 < k then x else y)))" proof fix s - have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)" + have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)" by (simp add: range_def scomp_Pair scomp_apply split_beta) then show "select_default k x y s = (if k = 0 then range 1 o\ (\_. Pair y) @@ -169,7 +195,6 @@ hide (open) type seed hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed iterate range select pick select_weight select_default -hide (open) fact log_def no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\" 60) diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/Rational.thy --- a/src/HOL/Rational.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/Rational.thy Fri May 22 13:22:16 2009 -0700 @@ -1001,6 +1001,28 @@ "Fract a b / Fract c d = Fract_norm (a * d) (b * c)" by simp +definition (in term_syntax) + valterm_fract :: "int \ (unit \ Code_Eval.term) \ int \ (unit \ Code_Eval.term) \ rat \ (unit \ Code_Eval.term)" where + [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\} k {\} l" + +notation fcomp (infixl "o>" 60) +notation scomp (infixl "o\" 60) + +instantiation rat :: random +begin + +definition + "random i = random i o\ (\num. Random.range i o\ (\denom. Pair ( + let j = Code_Numeral.int_of (denom + 1) + in valterm_fract num (j, \u. Code_Eval.term_of j))))" + +instance .. + +end + +no_notation fcomp (infixl "o>" 60) +no_notation scomp (infixl "o\" 60) + hide (open) const Fract_norm text {* Setup for SML code generator *} diff -r 689aa7da48cc -r c4c1692d4eee src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Fri May 22 13:18:59 2009 -0700 +++ b/src/HOL/RealDef.thy Fri May 22 13:22:16 2009 -0700 @@ -1126,6 +1126,26 @@ lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)" by (simp add: of_rat_divide) +definition (in term_syntax) + valterm_ratreal :: "rat \ (unit \ Code_Eval.term) \ real \ (unit \ Code_Eval.term)" where + [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\} k" + +notation fcomp (infixl "o>" 60) +notation scomp (infixl "o\