--- 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\<Colon>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}
--- 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}
--- 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}
--- 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 \<Rightarrow> typerep \<Rightarrow> term" where
+definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
"Const _ _ = dummy_term"
definition App :: "term \<Rightarrow> term \<Rightarrow> 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 \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
lemma [code, code del]:
"(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> 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 \<Colon> message_string \<Rightarrow> term"
+code_const "term_of \<Colon> String.literal \<Rightarrow> term"
(Eval "HOLogic.mk'_message'_string")
code_reserved Eval HOLogic
@@ -215,6 +209,9 @@
else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> 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 \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
+ by (simp only: term_of_anything)
subsection {* Obfuscate *}
--- 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 \<Colon> 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:
- "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
-proof
- fix n :: nat
- assume "\<And>n\<Colon>index. PROP P n"
- then show "PROP P (of_nat n)" .
-next
- fix n :: index
- assume "\<And>n\<Colon>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 "\<And>n. k = of_nat n \<Longrightarrow> P"
- shows P
- by (rule assms [of "nat_of k"]) simp
-
-lemma index_induct_raw:
- assumes "\<And>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 \<longleftrightarrow> k = l"
- by (rule nat_of_inject)
-
-lemma of_nat_inject [simp]:
- "of_nat n = of_nat m \<longleftrightarrow> 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 \<Colon> index" Suc_index
-proof -
- fix P :: "index \<Rightarrow> bool"
- fix k :: index
- assume "P 0" then have init: "P (of_nat 0)" by simp
- assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
- then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
- then have step: "\<And>n. P (of_nat n) \<Longrightarrow> 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 \<noteq> Code_Index.of_nat 0 \<Longrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<Colon> int \<Rightarrow> index"
-
-
-subsection {* Basic arithmetic *}
-
-instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
-begin
-
-definition [simp, code del]:
- "(1\<Colon>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 \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
-
-definition [simp, code del]:
- "n < m \<longleftrightarrow> 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\<Colon>index) = Numeral0"
- by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
- using zero_index_code ..
-
-lemma one_index_code [code inline, code]:
- "(1\<Colon>index) = Numeral1"
- by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>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 \<Rightarrow> index \<Rightarrow> 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 \<le> of_nat m \<longleftrightarrow> n \<le> m"
- by simp
-
-lemma less_index_code [code nbe]:
- "of_nat n < of_nat m \<longleftrightarrow> 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 \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
- by (cases i) auto
-
-definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> index \<Rightarrow> index \<times> 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 \<Rightarrow> 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 \<Rightarrow> int) <\<cdot>> 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 + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.+/ ((_),/ (_))")
- (OCaml "Pervasives.( + )")
- (Haskell infixl 6 "+")
-
-code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.max/ (_/ -/ _,/ 0 : int)")
- (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
- (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
-
-code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> 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 \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "!((_ : Int.int) = _)")
- (OCaml "!((_ : int) = _)")
- (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.<=/ ((_),/ (_))")
- (OCaml "!((_ : int) <= _)")
- (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.</ ((_),/ (_))")
- (OCaml "!((_ : int) < _)")
- (Haskell infix 4 "<")
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Numeral.thy Fri May 22 13:22:16 2009 -0700
@@ -0,0 +1,325 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Type of target language numerals *}
+
+theory Code_Numeral
+imports Nat_Numeral
+begin
+
+text {*
+ Code numerals are isomorphic to HOL @{typ nat} but
+ mapped to target-language builtin numerals.
+*}
+
+subsection {* Datatype of target language numerals *}
+
+typedef (open) code_numeral = "UNIV \<Colon> 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:
+ "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
+proof
+ fix n :: nat
+ assume "\<And>n\<Colon>code_numeral. PROP P n"
+ then show "PROP P (of_nat n)" .
+next
+ fix n :: code_numeral
+ assume "\<And>n\<Colon>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 "\<And>n. k = of_nat n \<Longrightarrow> P"
+ shows P
+ by (rule assms [of "nat_of k"]) simp
+
+lemma code_numeral_induct_raw:
+ assumes "\<And>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 \<longleftrightarrow> k = l"
+ by (rule nat_of_inject)
+
+lemma of_nat_inject [simp]:
+ "of_nat n = of_nat m \<longleftrightarrow> 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 \<Colon> code_numeral" Suc_code_numeral
+proof -
+ fix P :: "code_numeral \<Rightarrow> bool"
+ fix k :: code_numeral
+ assume "P 0" then have init: "P (of_nat 0)" by simp
+ assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
+ then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
+ then have step: "\<And>n. P (of_nat n) \<Longrightarrow> 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 \<noteq> of_nat 0 \<Longrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<Colon> int \<Rightarrow> code_numeral"
+
+
+subsection {* Basic arithmetic *}
+
+instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}"
+begin
+
+definition [simp, code del]:
+ "(1\<Colon>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 \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
+
+definition [simp, code del]:
+ "n < m \<longleftrightarrow> 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\<Colon>code_numeral) = Numeral0"
+ by (simp add: number_of_code_numeral_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
+ using zero_code_numeral_code ..
+
+lemma one_code_numeral_code [code inline, code]:
+ "(1\<Colon>code_numeral) = Numeral1"
+ by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>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 \<Rightarrow> code_numeral \<Rightarrow> 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 \<le> of_nat m \<longleftrightarrow> n \<le> m"
+ by simp
+
+lemma less_code_numeral_code [code nbe]:
+ "of_nat n < of_nat m \<longleftrightarrow> 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 \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
+ by (cases i) auto
+
+definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> 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 \<Rightarrow> 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 + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.+/ ((_),/ (_))")
+ (OCaml "Pervasives.( + )")
+ (Haskell infixl 6 "+")
+
+code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.max/ (_/ -/ _,/ 0 : int)")
+ (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+ (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+
+code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 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 \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "!((_ : Int.int) = _)")
+ (OCaml "!((_ : int) = _)")
+ (Haskell infixl 4 "==")
+
+code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "Int.<=/ ((_),/ (_))")
+ (OCaml "!((_ : int) <= _)")
+ (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "Int.</ ((_),/ (_))")
+ (OCaml "!((_ : int) < _)")
+ (Haskell infix 4 "<")
+
+end
--- a/src/HOL/Complex_Main.thy Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Complex_Main.thy Fri May 22 13:22:16 2009 -0700
@@ -9,7 +9,6 @@
Ln
Taylor
Integration
- Quickcheck
begin
end
--- a/src/HOL/Fun.thy Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Fun.thy Fri May 22 13:22:16 2009 -0700
@@ -100,6 +100,9 @@
lemma fcomp_id [simp]: "f o> id = f"
by (simp add: fcomp_def)
+code_const fcomp
+ (Eval infixl 1 "#>")
+
no_notation fcomp (infixl "o>" 60)
--- 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 \<guillemotright>== liftM Code_Index.of_nat"
+ [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
hide (open) const length'
lemma [code]:
- "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
+ "Array.length = Array.length' \<guillemotright>== 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 \<guillemotright> return ()"
+ [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
hide (open) const upd'
lemma [code]:
- "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
+ "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def monad_simp upd_return)
--- 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 *}
--- 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 \<Rightarrow> exception"
+ Fail :: "String.literal \<Rightarrow> exception"
where
[code del]: "Fail s = Exn"
--- 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 \
--- 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 \<Rightarrow> y | 1 \<Rightarrow> (case y of 0 \<Rightarrow> 1 | 1 \<Rightarrow> 0))"
+ "x + y = bit_case y (bit_case 1 0 y) x"
definition times_bit_def:
- "x * y = (case x of 0 \<Rightarrow> 0 | 1 \<Rightarrow> y)"
+ "x * y = bit_case 0 y x"
definition uminus_bit_def [simp]:
"- x = (x :: bit)"
--- 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")
--- 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")
--- 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 {*
--- 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 \<equiv> (x = y)"
by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
+ "map f P = P \<guillemotright>= (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
--- 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\<rightarrow> h = f o> (g o\<rightarrow> 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\<rightarrow>" 60)
--- 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 \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+ fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
subsection {* Quickcheck generator *}
@@ -49,7 +49,7 @@
(mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> 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 \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> 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 \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> 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 \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
"random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
- let n = Code_Index.nat_of k
+ let n = Code_Numeral.nat_of k
in (n, \<lambda>_. Code_Eval.term_of n)))"
instance ..
@@ -168,42 +168,66 @@
definition
"random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
- let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
+ let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
in (j, \<lambda>_. Code_Eval.term_of j)))"
instance ..
end
-definition (in term_syntax)
- valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+subsection {* Type copies *}
-instantiation rat :: random
-begin
+setup {*
+let
-definition
- "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
- let j = Code_Index.int_of (denom + 1)
- in valterm_fract num (j, \<lambda>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 \<Rightarrow> 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\<Colon>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 \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
-
-instantiation real :: random
-begin
-
-definition
- "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
-
-instance ..
-
-end
+*}
no_notation fcomp (infixl "o>" 60)
--- 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 \<Rightarrow> index \<Rightarrow> index" where
+definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"inc_shift v k = (if v = k then 1 else k + 1)"
-definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
+definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"minus_shift r k l = (if k < l then r + k - l else k - l)"
-fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
+fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
subsection {* Random seeds *}
-types seed = "index \<times> index"
+types seed = "code_numeral \<times> code_numeral"
-primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
+primrec "next" :: "seed \<Rightarrow> code_numeral \<times> 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 \<Rightarrow> bool" where
"seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> 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 \<Rightarrow> seed \<times> seed" where
"split_seed s = (let
(v, w) = s;
@@ -58,10 +55,10 @@
subsection {* Base selectors *}
-fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
"iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
-definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
"range k = iterate (log 2147483561 k)
(\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
o\<rightarrow> (\<lambda>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 \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
- "select xs = range (Code_Index.of_nat (length xs))
- o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
+ "select xs = range (Code_Numeral.of_nat (length xs))
+ o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
lemma select:
assumes "xs \<noteq> []"
shows "fst (select xs s) \<in> 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 \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
+primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> '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 (\<lambda>(k, _). k > 0) xs) = pick xs"
by (induct xs) (auto simp add: expand_fun_eq)
-definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+lemma pick_same:
+ "l < length xs \<Longrightarrow> 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 \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select_weight xs = range (listsum (map fst xs))
o\<rightarrow> (\<lambda>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 \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+lemma select_weigth_drop_zero:
+ "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
+proof -
+ have "listsum (map fst [(k, _)\<leftarrow>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 \<noteq> []"
+ shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
+proof -
+ have less: "\<And>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 \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
[code del]: "select_default k x y = range k
o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
@@ -127,7 +153,7 @@
else range k o\<rightarrow> (\<lambda>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\<rightarrow> (\<lambda>_. 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\<rightarrow>" 60)
--- 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 \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
+ [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation rat :: random
+begin
+
+definition
+ "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
+ let j = Code_Numeral.int_of (denom + 1)
+ in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
hide (open) const Fract_norm
text {* Setup for SML code generator *}
--- 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 \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
+ [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation real :: random
+begin
+
+definition
+ "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
text {* Setup for SML code generator *}
types_code
--- a/src/HOL/String.thy Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/String.thy Fri May 22 13:22:16 2009 -0700
@@ -85,15 +85,14 @@
subsection {* Strings as dedicated datatype *}
-datatype message_string = STR string
+datatype literal = STR string
-lemmas [code del] =
- message_string.recs message_string.cases
+lemmas [code del] = literal.recs literal.cases
-lemma [code]: "size (s\<Colon>message_string) = 0"
+lemma [code]: "size (s\<Colon>literal) = 0"
by (cases s) simp_all
-lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
+lemma [code]: "literal_size (s\<Colon>literal) = 0"
by (cases s) simp_all
@@ -101,19 +100,19 @@
use "Tools/string_code.ML"
-code_type message_string
+code_type literal
(SML "string")
(OCaml "string")
(Haskell "String")
setup {*
- fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
+ fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
*}
-code_instance message_string :: eq
+code_instance literal :: eq
(Haskell -)
-code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
@@ -147,4 +146,6 @@
in Codegen.add_codegen "char_codegen" char_codegen end
*}
+hide (open) type literal
+
end
\ No newline at end of file
--- a/src/HOL/Tools/datatype_package.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Tools/datatype_package.ML Fri May 22 13:22:16 2009 -0700
@@ -101,7 +101,7 @@
fun put_dt_infos (dt_infos : (string * datatype_info) list) =
map_datatypes (fn {types, constrs, cases} =>
{types = fold Symtab.update dt_infos types,
- constrs = fold Symtab.update
+ constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
(maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
(#3 (the (AList.lookup op = descr index)))) dt_infos) constrs,
cases = fold Symtab.update
--- a/src/HOL/Tools/hologic.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Tools/hologic.ML Fri May 22 13:22:16 2009 -0700
@@ -87,7 +87,7 @@
val dest_nat: term -> int
val class_size: string
val size_const: typ -> term
- val indexT: typ
+ val code_numeralT: typ
val intT: typ
val pls_const: term
val min_const: term
@@ -116,9 +116,9 @@
val stringT: typ
val mk_string: string -> term
val dest_string: term -> string
- val message_stringT: typ
- val mk_message_string: string -> term
- val dest_message_string: term -> string
+ val literalT: typ
+ val mk_literal: string -> term
+ val dest_literal: term -> string
val mk_typerep: typ -> term
val mk_term_of: typ -> term -> term
val reflect_term: term -> term
@@ -461,9 +461,9 @@
fun size_const T = Const ("Nat.size_class.size", T --> natT);
-(* index *)
+(* code numeral *)
-val indexT = Type ("Code_Index.index", []);
+val code_numeralT = Type ("Code_Numeral.code_numeral", []);
(* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
@@ -586,15 +586,15 @@
val dest_string = implode o map (chr o dest_char) o dest_list;
-(* message_string *)
+(* literal *)
-val message_stringT = Type ("String.message_string", []);
+val literalT = Type ("String.literal", []);
-fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
+fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
$ mk_string s;
-fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
+fun dest_literal (Const ("String.literal.STR", _) $ t) =
dest_string t
- | dest_message_string t = raise TERM ("dest_message_string", [t]);
+ | dest_literal t = raise TERM ("dest_literal", [t]);
(* typerep and term *)
@@ -609,8 +609,8 @@
fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
fun reflect_term (Const (c, T)) =
- Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
- $ mk_message_string c $ mk_typerep T
+ Const ("Code_Eval.Const", literalT --> typerepT --> termT)
+ $ mk_literal c $ mk_typerep T
| reflect_term (t1 $ t2) =
Const ("Code_Eval.App", termT --> termT --> termT)
$ reflect_term t1 $ reflect_term t2
--- a/src/HOL/Tools/prop_logic.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Tools/prop_logic.ML Fri May 22 13:22:16 2009 -0700
@@ -1,7 +1,6 @@
(* Title: HOL/Tools/prop_logic.ML
- ID: $Id$
Author: Tjark Weber
- Copyright 2004-2005
+ Copyright 2004-2009
Formulas of propositional logic.
*)
@@ -33,7 +32,6 @@
val nnf : prop_formula -> prop_formula (* negation normal form *)
val cnf : prop_formula -> prop_formula (* conjunctive normal form *)
- val auxcnf : prop_formula -> prop_formula (* cnf with auxiliary variables *)
val defcnf : prop_formula -> prop_formula (* definitional cnf *)
val eval : (int -> bool) -> prop_formula -> bool (* semantics *)
@@ -156,7 +154,7 @@
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
(* ------------------------------------------------------------------------- *)
-(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e. *)
+(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e., *)
(* only variables may be negated, but not subformulas). *)
(* ------------------------------------------------------------------------- *)
@@ -178,7 +176,8 @@
(* ------------------------------------------------------------------------- *)
(* is_cnf: returns 'true' iff the formula is in conjunctive normal form *)
-(* (i.e. a conjunction of disjunctions). *)
+(* (i.e., a conjunction of disjunctions of literals). 'is_cnf' *)
+(* implies 'is_nnf'. *)
(* ------------------------------------------------------------------------- *)
local
@@ -197,170 +196,90 @@
(* ------------------------------------------------------------------------- *)
(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
-(* logic (i.e. only variables may be negated, but not subformulas). *)
-(* Simplification (c.f. 'simplify') is performed as well. *)
+(* logic (i.e., only variables may be negated, but not subformulas). *)
+(* Simplification (cf. 'simplify') is performed as well. Not *)
+(* surprisingly, 'is_nnf o nnf' always returns 'true'. 'nnf fm' returns *)
+(* 'fm' if (and only if) 'is_nnf fm' returns 'true'. *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
- fun
- (* constants *)
- nnf True = True
- | nnf False = False
- (* variables *)
- | nnf (BoolVar i) = (BoolVar i)
- (* 'or' and 'and' as outermost connectives are left untouched *)
- | nnf (Or (fm1, fm2)) = SOr (nnf fm1, nnf fm2)
- | nnf (And (fm1, fm2)) = SAnd (nnf fm1, nnf fm2)
- (* 'not' + constant *)
- | nnf (Not True) = False
- | nnf (Not False) = True
- (* 'not' + variable *)
- | nnf (Not (BoolVar i)) = Not (BoolVar i)
- (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
- | nnf (Not (Or (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
- | nnf (Not (And (fm1, fm2))) = SOr (nnf (SNot fm1), nnf (SNot fm2))
- (* double-negation elimination *)
- | nnf (Not (Not fm)) = nnf fm;
+ fun nnf fm =
+ let
+ fun
+ (* constants *)
+ nnf_aux True = True
+ | nnf_aux False = False
+ (* variables *)
+ | nnf_aux (BoolVar i) = (BoolVar i)
+ (* 'or' and 'and' as outermost connectives are left untouched *)
+ | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2)
+ | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2)
+ (* 'not' + constant *)
+ | nnf_aux (Not True) = False
+ | nnf_aux (Not False) = True
+ (* 'not' + variable *)
+ | nnf_aux (Not (BoolVar i)) = Not (BoolVar i)
+ (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
+ | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
+ | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
+ (* double-negation elimination *)
+ | nnf_aux (Not (Not fm)) = nnf_aux fm
+ in
+ if is_nnf fm then
+ fm
+ else
+ nnf_aux fm
+ end;
(* ------------------------------------------------------------------------- *)
-(* cnf: computes the conjunctive normal form (i.e. a conjunction of *)
-(* disjunctions) of a formula 'fm' of propositional logic. The result *)
-(* formula may be exponentially longer than 'fm'. *)
+(* cnf: computes the conjunctive normal form (i.e., a conjunction of *)
+(* disjunctions of literals) of a formula 'fm' of propositional logic. *)
+(* Simplification (cf. 'simplify') is performed as well. The result *)
+(* is equivalent to 'fm', but may be exponentially longer. Not *)
+(* surprisingly, 'is_cnf o cnf' always returns 'true'. 'cnf fm' returns *)
+(* 'fm' if (and only if) 'is_cnf fm' returns 'true'. *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
fun cnf fm =
let
- fun
- (* constants *)
- cnf_from_nnf True = True
+ (* function to push an 'Or' below 'And's, using distributive laws *)
+ fun cnf_or (And (fm11, fm12), fm2) =
+ And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
+ | cnf_or (fm1, And (fm21, fm22)) =
+ And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
+ (* neither subformula contains 'And' *)
+ | cnf_or (fm1, fm2) =
+ Or (fm1, fm2)
+ fun cnf_from_nnf True = True
| cnf_from_nnf False = False
- (* literals *)
| cnf_from_nnf (BoolVar i) = BoolVar i
- | cnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *)
- (* pushing 'or' inside of 'and' using distributive laws *)
+ (* 'fm' must be a variable since the formula is in NNF *)
+ | cnf_from_nnf (Not fm) = Not fm
+ (* 'Or' may need to be pushed below 'And' *)
| cnf_from_nnf (Or (fm1, fm2)) =
- let
- fun cnf_or (And (fm11, fm12), fm2) =
- And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
- | cnf_or (fm1, And (fm21, fm22)) =
- And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
- (* neither subformula contains 'and' *)
- | cnf_or (fm1, fm2) =
- Or (fm1, fm2)
- in
- cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
- end
- (* 'and' as outermost connective is left untouched *)
- | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
+ cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
+ (* 'And' as outermost connective is left untouched *)
+ | cnf_from_nnf (And (fm1, fm2)) =
+ And (cnf_from_nnf fm1, cnf_from_nnf fm2)
in
- (cnf_from_nnf o nnf) fm
+ if is_cnf fm then
+ fm
+ else
+ (cnf_from_nnf o nnf) fm
end;
(* ------------------------------------------------------------------------- *)
-(* auxcnf: computes the definitional conjunctive normal form of a formula *)
-(* 'fm' of propositional logic, introducing auxiliary variables if *)
-(* necessary to avoid an exponential blowup of the formula. The result *)
-(* formula is satisfiable if and only if 'fm' is satisfiable. *)
-(* Auxiliary variables are introduced as switches for OR-nodes, based *)
-(* on the observation that e.g. "fm1 OR (fm21 AND fm22)" is *)
-(* equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR *)
-(* aux)". *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than *)
-(* 'defcnf' below, but sometimes generates much larger SAT problems *)
-(* overall (hence it must sometimes generate longer clauses than *)
-(* 'defcnf' does). It is currently not quite clear to me if one of the *)
-(* algorithms is clearly superior to the other, but I suggest using *)
-(* 'defcnf' instead. *)
-(* ------------------------------------------------------------------------- *)
-
- (* prop_formula -> prop_formula *)
-
- fun auxcnf fm =
- let
- (* convert formula to NNF first *)
- val fm' = nnf fm
- (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
- (* int ref *)
- val new = ref (maxidx fm' + 1)
- (* unit -> int *)
- fun new_idx () = let val idx = !new in new := idx+1; idx end
- (* prop_formula -> prop_formula *)
- fun
- (* constants *)
- auxcnf_from_nnf True = True
- | auxcnf_from_nnf False = False
- (* literals *)
- | auxcnf_from_nnf (BoolVar i) = BoolVar i
- | auxcnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *)
- (* pushing 'or' inside of 'and' using auxiliary variables *)
- | auxcnf_from_nnf (Or (fm1, fm2)) =
- let
- val fm1' = auxcnf_from_nnf fm1
- val fm2' = auxcnf_from_nnf fm2
- (* prop_formula * prop_formula -> prop_formula *)
- fun auxcnf_or (And (fm11, fm12), fm2) =
- (case fm2 of
- (* do not introduce an auxiliary variable for literals *)
- BoolVar _ =>
- And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
- | Not _ =>
- And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
- | _ =>
- let
- val aux = BoolVar (new_idx ())
- in
- And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
- end)
- | auxcnf_or (fm1, And (fm21, fm22)) =
- (case fm1 of
- (* do not introduce an auxiliary variable for literals *)
- BoolVar _ =>
- And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
- | Not _ =>
- And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
- | _ =>
- let
- val aux = BoolVar (new_idx ())
- in
- And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
- end)
- (* neither subformula contains 'and' *)
- | auxcnf_or (fm1, fm2) =
- Or (fm1, fm2)
- in
- auxcnf_or (fm1', fm2')
- end
- (* 'and' as outermost connective is left untouched *)
- | auxcnf_from_nnf (And (fm1, fm2)) =
- And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
- in
- auxcnf_from_nnf fm'
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* defcnf: computes the definitional conjunctive normal form of a formula *)
-(* 'fm' of propositional logic, introducing auxiliary variables to *)
-(* avoid an exponential blowup of the formula. The result formula is *)
-(* satisfiable if and only if 'fm' is satisfiable. Auxiliary variables *)
-(* are introduced as abbreviations for AND-, OR-, and NOT-nodes, based *)
-(* on the following equisatisfiabilities (+/- indicates polarity): *)
-(* LITERAL+ == LITERAL *)
-(* LITERAL- == NOT LITERAL *)
-(* (NOT fm1)+ == aux AND (NOT aux OR fm1-) *)
-(* (fm1 OR fm2)+ == aux AND (NOT aux OR fm1+ OR fm2+) *)
-(* (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+) *)
-(* (NOT fm1)- == aux AND (NOT aux OR fm1+) *)
-(* (fm1 OR fm2)- == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-) *)
-(* (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-) *)
-(* Example: *)
-(* NOT (a AND b) == aux1 AND (NOT aux1 OR aux2) *)
-(* AND (NOT aux2 OR NOT a OR NOT b) *)
+(* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *)
+(* of propositional logic. Simplification (cf. 'simplify') is performed *)
+(* as well. 'defcnf' may introduce auxiliary Boolean variables to avoid *)
+(* an exponential blowup of the formula. The result is equisatisfiable *)
+(* (i.e., satisfiable if and only if 'fm' is satisfiable), but not *)
+(* necessarily equivalent to 'fm'. Not surprisingly, 'is_cnf o defcnf' *)
+(* always returns 'true'. 'defcnf fm' returns 'fm' if (and only if) *)
+(* 'is_cnf fm' returns 'true'. *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
@@ -368,93 +287,66 @@
fun defcnf fm =
if is_cnf fm then
fm
- else let
- (* simplify formula first *)
- val fm' = simplify fm
+ else
+ let
+ val fm' = nnf fm
(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
(* int ref *)
val new = ref (maxidx fm' + 1)
(* unit -> int *)
fun new_idx () = let val idx = !new in new := idx+1; idx end
- (* optimization for n-ary disjunction/conjunction *)
- (* prop_formula -> prop_formula list *)
- fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
- | disjuncts fm1 = [fm1]
- (* prop_formula -> prop_formula list *)
- fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
- | conjuncts fm1 = [fm1]
- (* polarity -> formula -> (defining clauses, literal) *)
- (* bool -> prop_formula -> prop_formula * prop_formula *)
- fun
- (* constants *)
- defcnf' true True = (True, True)
- | defcnf' false True = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
- | defcnf' true False = (True, False)
- | defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
- (* literals *)
- | defcnf' true (BoolVar i) = (True, BoolVar i)
- | defcnf' false (BoolVar i) = (True, Not (BoolVar i))
- | defcnf' true (Not (BoolVar i)) = (True, Not (BoolVar i))
- | defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
- (* 'not' *)
- | defcnf' polarity (Not fm1) =
+ (* replaces 'And' by an auxiliary variable (and its definition) *)
+ (* prop_formula -> prop_formula * prop_formula list *)
+ fun defcnf_or (And x) =
let
- val (def1, aux1) = defcnf' (not polarity) fm1
- val aux = BoolVar (new_idx ())
- val def = Or (Not aux, aux1)
+ val i = new_idx ()
in
- (SAnd (def1, def), aux)
+ (* Note that definitions are in NNF, but not CNF. *)
+ (BoolVar i, [Or (Not (BoolVar i), And x)])
end
- (* 'or' *)
- | defcnf' polarity (Or (fm1, fm2)) =
+ | defcnf_or (Or (fm1, fm2)) =
let
- val fms = disjuncts (Or (fm1, fm2))
- val (defs, auxs) = split_list (map (defcnf' polarity) fms)
- val aux = BoolVar (new_idx ())
- val def = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
+ val (fm1', defs1) = defcnf_or fm1
+ val (fm2', defs2) = defcnf_or fm2
in
- (SAnd (all defs, def), aux)
+ (Or (fm1', fm2'), defs1 @ defs2)
end
- (* 'and' *)
- | defcnf' polarity (And (fm1, fm2)) =
+ | defcnf_or fm =
+ (fm, [])
+ (* prop_formula -> prop_formula *)
+ fun defcnf_from_nnf True = True
+ | defcnf_from_nnf False = False
+ | defcnf_from_nnf (BoolVar i) = BoolVar i
+ (* 'fm' must be a variable since the formula is in NNF *)
+ | defcnf_from_nnf (Not fm) = Not fm
+ (* 'Or' may need to be pushed below 'And' *)
+ (* 'Or' of literal and 'And': use distributivity *)
+ | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) =
+ And (defcnf_from_nnf (Or (BoolVar i, fm1)),
+ defcnf_from_nnf (Or (BoolVar i, fm2)))
+ | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) =
+ And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)),
+ defcnf_from_nnf (Or (Not (BoolVar i), fm2)))
+ | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) =
+ And (defcnf_from_nnf (Or (fm1, BoolVar i)),
+ defcnf_from_nnf (Or (fm2, BoolVar i)))
+ | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) =
+ And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))),
+ defcnf_from_nnf (Or (fm2, Not (BoolVar i))))
+ (* all other cases: turn the formula into a disjunction of literals, *)
+ (* adding definitions as necessary *)
+ | defcnf_from_nnf (Or x) =
let
- val fms = conjuncts (And (fm1, fm2))
- val (defs, auxs) = split_list (map (defcnf' polarity) fms)
- val aux = BoolVar (new_idx ())
- val def = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
+ val (fm, defs) = defcnf_or (Or x)
+ val cnf_defs = map defcnf_from_nnf defs
in
- (SAnd (all defs, def), aux)
- end
- (* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
- (* prop_formula -> prop_formula * prop_formula *)
- fun defcnf_or (Or (fm1, fm2)) =
- let
- val (def1, aux1) = defcnf_or fm1
- val (def2, aux2) = defcnf_or fm2
- in
- (SAnd (def1, def2), Or (aux1, aux2))
+ all (fm :: cnf_defs)
end
- | defcnf_or fm =
- defcnf' true fm
- (* prop_formula -> prop_formula * prop_formula *)
- fun defcnf_and (And (fm1, fm2)) =
- let
- val (def1, aux1) = defcnf_and fm1
- val (def2, aux2) = defcnf_and fm2
- in
- (SAnd (def1, def2), And (aux1, aux2))
- end
- | defcnf_and (Or (fm1, fm2)) =
- let
- val (def1, aux1) = defcnf_or fm1
- val (def2, aux2) = defcnf_or fm2
- in
- (SAnd (def1, def2), Or (aux1, aux2))
- end
- | defcnf_and fm =
- defcnf' true fm
+ (* 'And' as outermost connective is left untouched *)
+ | defcnf_from_nnf (And (fm1, fm2)) =
+ And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
in
- SAnd (defcnf_and fm')
+ defcnf_from_nnf fm'
end;
(* ------------------------------------------------------------------------- *)
@@ -545,16 +437,16 @@
(* prop_formula -> Term.term *)
fun term_of_prop_formula True =
- HOLogic.true_const
- | term_of_prop_formula False =
- HOLogic.false_const
- | term_of_prop_formula (BoolVar i) =
- Free ("v" ^ Int.toString i, HOLogic.boolT)
- | term_of_prop_formula (Not fm) =
- HOLogic.mk_not (term_of_prop_formula fm)
- | term_of_prop_formula (Or (fm1, fm2)) =
- HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
- | term_of_prop_formula (And (fm1, fm2)) =
- HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
+ HOLogic.true_const
+ | term_of_prop_formula False =
+ HOLogic.false_const
+ | term_of_prop_formula (BoolVar i) =
+ Free ("v" ^ Int.toString i, HOLogic.boolT)
+ | term_of_prop_formula (Not fm) =
+ HOLogic.mk_not (term_of_prop_formula fm)
+ | term_of_prop_formula (Or (fm1, fm2)) =
+ HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
+ | term_of_prop_formula (And (fm1, fm2)) =
+ HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
end;
--- a/src/HOL/Tools/sat_solver.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Tools/sat_solver.ML Fri May 22 13:22:16 2009 -0700
@@ -1,7 +1,6 @@
(* Title: HOL/Tools/sat_solver.ML
- ID: $Id$
Author: Tjark Weber
- Copyright 2004-2006
+ Copyright 2004-2009
Interface to external SAT solvers, and (simple) built-in SAT solvers.
*)
@@ -21,7 +20,8 @@
val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
val read_std_result_file : Path.T -> string * string * string -> result
- val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
+ val make_external_solver : string -> (PropLogic.prop_formula -> unit) ->
+ (unit -> result) -> solver
val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
@@ -102,45 +102,49 @@
| cnf_True_False_elim False =
And (BoolVar 1, Not (BoolVar 1))
| cnf_True_False_elim fm =
- fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *)
+ fm (* since 'fm' is in CNF, either 'fm'='True'/'False',
+ or 'fm' does not contain 'True'/'False' at all *)
(* prop_formula -> int *)
- fun cnf_number_of_clauses (And (fm1,fm2)) =
+ fun cnf_number_of_clauses (And (fm1, fm2)) =
(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
| cnf_number_of_clauses _ =
1
- (* prop_formula -> string list *)
- fun cnf_string fm =
+ (* TextIO.outstream -> unit *)
+ fun write_cnf_file out =
let
- (* prop_formula -> string list -> string list *)
- fun cnf_string_acc True acc =
- error "formula is not in CNF"
- | cnf_string_acc False acc =
- error "formula is not in CNF"
- | cnf_string_acc (BoolVar i) acc =
- (i>=1 orelse error "formula contains a variable index less than 1";
- string_of_int i :: acc)
- | cnf_string_acc (Not (BoolVar i)) acc =
- "-" :: cnf_string_acc (BoolVar i) acc
- | cnf_string_acc (Not _) acc =
- error "formula is not in CNF"
- | cnf_string_acc (Or (fm1,fm2)) acc =
- cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc)
- | cnf_string_acc (And (fm1,fm2)) acc =
- cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
+ (* prop_formula -> unit *)
+ fun write_formula True =
+ error "formula is not in CNF"
+ | write_formula False =
+ error "formula is not in CNF"
+ | write_formula (BoolVar i) =
+ (i>=1 orelse error "formula contains a variable index less than 1";
+ TextIO.output (out, string_of_int i))
+ | write_formula (Not (BoolVar i)) =
+ (TextIO.output (out, "-");
+ write_formula (BoolVar i))
+ | write_formula (Not _) =
+ error "formula is not in CNF"
+ | write_formula (Or (fm1, fm2)) =
+ (write_formula fm1;
+ TextIO.output (out, " ");
+ write_formula fm2)
+ | write_formula (And (fm1, fm2)) =
+ (write_formula fm1;
+ TextIO.output (out, " 0\n");
+ write_formula fm2)
+ val fm' = cnf_True_False_elim fm
+ val number_of_vars = maxidx fm'
+ val number_of_clauses = cnf_number_of_clauses fm'
in
- cnf_string_acc fm []
+ TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_cnf_file\n");
+ TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^
+ string_of_int number_of_clauses ^ "\n");
+ write_formula fm';
+ TextIO.output (out, " 0\n")
end
- val fm' = cnf_True_False_elim fm
- val number_of_vars = maxidx fm'
- val number_of_clauses = cnf_number_of_clauses fm'
in
- File.write path
- ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
- "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n");
- File.append_list path
- (cnf_string fm');
- File.append path
- " 0\n"
+ File.open_output write_cnf_file path
end;
(* ------------------------------------------------------------------------- *)
@@ -154,49 +158,59 @@
fun write_dimacs_sat_file path fm =
let
- (* prop_formula -> string list *)
- fun sat_string fm =
+ (* TextIO.outstream -> unit *)
+ fun write_sat_file out =
let
- (* prop_formula -> string list -> string list *)
- fun sat_string_acc True acc =
- "*()" :: acc
- | sat_string_acc False acc =
- "+()" :: acc
- | sat_string_acc (BoolVar i) acc =
- (i>=1 orelse error "formula contains a variable index less than 1";
- string_of_int i :: acc)
- | sat_string_acc (Not (BoolVar i)) acc =
- "-" :: sat_string_acc (BoolVar i) acc
- | sat_string_acc (Not fm) acc =
- "-(" :: sat_string_acc fm (")" :: acc)
- | sat_string_acc (Or (fm1,fm2)) acc =
- "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc))
- | sat_string_acc (And (fm1,fm2)) acc =
- "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc))
+ (* prop_formula -> unit *)
+ fun write_formula True =
+ TextIO.output (out, "*()")
+ | write_formula False =
+ TextIO.output (out, "+()")
+ | write_formula (BoolVar i) =
+ (i>=1 orelse error "formula contains a variable index less than 1";
+ TextIO.output (out, string_of_int i))
+ | write_formula (Not (BoolVar i)) =
+ (TextIO.output (out, "-");
+ write_formula (BoolVar i))
+ | write_formula (Not fm) =
+ (TextIO.output (out, "-(");
+ write_formula fm;
+ TextIO.output (out, ")"))
+ | write_formula (Or (fm1, fm2)) =
+ (TextIO.output (out, "+(");
+ write_formula_or fm1;
+ TextIO.output (out, " ");
+ write_formula_or fm2;
+ TextIO.output (out, ")"))
+ | write_formula (And (fm1, fm2)) =
+ (TextIO.output (out, "*(");
+ write_formula_and fm1;
+ TextIO.output (out, " ");
+ write_formula_and fm2;
+ TextIO.output (out, ")"))
(* optimization to make use of n-ary disjunction/conjunction *)
- (* prop_formula -> string list -> string list *)
- and sat_string_acc_or (Or (fm1,fm2)) acc =
- sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc)
- | sat_string_acc_or fm acc =
- sat_string_acc fm acc
- (* prop_formula -> string list -> string list *)
- and sat_string_acc_and (And (fm1,fm2)) acc =
- sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc)
- | sat_string_acc_and fm acc =
- sat_string_acc fm acc
+ and write_formula_or (Or (fm1, fm2)) =
+ (write_formula_or fm1;
+ TextIO.output (out, " ");
+ write_formula_or fm2)
+ | write_formula_or fm =
+ write_formula fm
+ and write_formula_and (And (fm1, fm2)) =
+ (write_formula_and fm1;
+ TextIO.output (out, " ");
+ write_formula_and fm2)
+ | write_formula_and fm =
+ write_formula fm
+ val number_of_vars = Int.max (maxidx fm, 1)
in
- sat_string_acc fm []
+ TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_sat_file\n");
+ TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n");
+ TextIO.output (out, "(");
+ write_formula fm;
+ TextIO.output (out, ")\n")
end
- val number_of_vars = Int.max (maxidx fm, 1)
in
- File.write path
- ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
- "p sat " ^ string_of_int number_of_vars ^ "\n" ^
- "(");
- File.append_list path
- (sat_string fm);
- File.append path
- ")\n"
+ File.open_output write_sat_file path
end;
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/string_code.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Tools/string_code.ML Fri May 22 13:22:16 2009 -0700
@@ -7,7 +7,7 @@
sig
val add_literal_list_string: string -> theory -> theory
val add_literal_char: string -> theory -> theory
- val add_literal_message: string -> theory -> theory
+ val add_literal_string: string -> theory -> theory
end;
structure String_Code : STRING_CODE =
@@ -72,7 +72,7 @@
@{const_name Char} (SOME (2, (cs_nibbles, pretty)))
end;
-fun add_literal_message target =
+fun add_literal_string target =
let
fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
case List_Code.implode_list nil' cons' t
--- a/src/HOL/Typerep.thy Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/Typerep.thy Fri May 22 13:22:16 2009 -0700
@@ -6,7 +6,7 @@
imports Plain String
begin
-datatype typerep = Typerep message_string "typerep list"
+datatype typerep = Typerep String.literal "typerep list"
class typerep =
fixes typerep :: "'a itself \<Rightarrow> typerep"
@@ -45,7 +45,7 @@
val ty = Type (tyco, map TFree vs);
val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
$ Free ("T", Term.itselfT ty);
- val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
+ val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
$ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
--- a/src/HOL/ex/Predicate_Compile.thy Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/ex/Predicate_Compile.thy Fri May 22 13:22:16 2009 -0700
@@ -7,39 +7,53 @@
setup {* Predicate_Compile.setup *}
-
text {* Experimental code *}
-definition pred_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'b Predicate.pred" where
- "pred_map f P = Predicate.bind P (Predicate.single o f)"
-
ML {*
-structure Predicate =
+structure Predicate_Compile =
struct
-open Predicate;
-
-val pred_ref = ref (NONE : (unit -> term Predicate.pred) option);
+open Predicate_Compile;
-fun eval_pred thy t =
- Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy (HOLogic.mk_term_of (fastype_of t) t) [];
+fun eval thy t_compr =
+ let
+ val t = Predicate_Compile.analyze_compr thy t_compr;
+ val Type (@{type_name Predicate.pred}, [T]) = fastype_of t;
+ fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
+ val T1 = T --> @{typ term};
+ val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
+ val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
+ $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
+ in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
-fun eval_pred_elems thy t T length =
- t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T;
+fun values ctxt k t_compr =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (T, t') = eval thy t_compr;
+ in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end;
-fun analyze_compr thy t =
+fun values_cmd modes k raw_t state =
let
- val split = case t of (Const (@{const_name Collect}, _) $ t') => t'
- | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t);
- val (body, Ts, fp) = HOLogic.strip_split split;
- val (t_pred, args) = strip_comb body;
- val pred = case t_pred of Const (pred, _) => pred
- | _ => error ("Not a constant: " ^ Syntax.string_of_term_global thy t_pred);
- val mode = map is_Bound args; (*FIXME what about higher-order modes?*)
- val args' = filter_out is_Bound args;
- val T = HOLogic.mk_tupleT fp Ts;
- val mk = HOLogic.mk_tuple' fp T;
- in (((pred, mode), args), (mk, T)) end;
+ val ctxt = Toplevel.context_of state;
+ val t = Syntax.read_term ctxt raw_t;
+ val t' = values ctxt k t;
+ val ty' = Term.type_of t';
+ val ctxt' = Variable.auto_fixes t' ctxt;
+ val p = PrintMode.with_modes modes (fn () =>
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+ in Pretty.writeln p end;
+
+end;
+
+local structure P = OuterParse in
+
+val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
+ (opt_modes -- Scan.optional P.nat ~1 -- P.term
+ >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
+ (Predicate_Compile.values_cmd modes k t)));
end;
*}
--- a/src/HOL/ex/Predicate_Compile_ex.thy Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri May 22 13:22:16 2009 -0700
@@ -12,7 +12,10 @@
thm even.equation
-ML_val {* Predicate.yieldn 10 @{code even_0} *}
+values "{x. even 2}"
+values "{x. odd 2}"
+values 10 "{n. even n}"
+values 10 "{n. odd n}"
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
@@ -24,7 +27,9 @@
thm append.equation
-ML_val {* Predicate.yieldn 10 (@{code append_3} [1, 2, 3]) *}
+values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
+values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
+values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}"
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -38,10 +43,26 @@
thm partition.equation
+(*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
+ [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*)
+
code_pred tranclp
using assms by (rule tranclp.cases)
thm tranclp.equation
+inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "succ 0 1"
+ | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
+
+code_pred succ
+ using assms by (rule succ.cases)
+
+thm succ.equation
+
+values 20 "{n. tranclp succ 10 n}"
+values "{n. tranclp succ n 10}"
+values 20 "{(n, m). tranclp succ n m}"
+
end
\ No newline at end of file
--- a/src/HOL/ex/Quickcheck_Generators.thy Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/ex/Quickcheck_Generators.thy Fri May 22 13:22:16 2009 -0700
@@ -12,11 +12,11 @@
"collapse f = (do g \<leftarrow> f; g done)"
lemma random'_if:
- fixes random' :: "index \<Rightarrow> index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+ fixes random' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
assumes "random' 0 j = (\<lambda>s. undefined)"
- and "\<And>i. random' (Suc_index i) j = rhs2 i"
+ and "\<And>i. random' (Suc_code_numeral i) j = rhs2 i"
shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
- by (cases i rule: index.exhaust) (insert assms, simp_all)
+ by (cases i rule: code_numeral.exhaust) (insert assms, simp_all)
setup {*
let
@@ -62,7 +62,7 @@
in case mk_conss thy ty ts_rec
of SOME t_rec => mk_collapse thy (term_ty ty) $
(Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $
- @{term "i\<Colon>index"} $ t_rec $ t_atom)
+ @{term "i\<Colon>code_numeral"} $ t_rec $ t_atom)
| NONE => t_atom
end;
fun mk_random_eqs thy vs tycos =
@@ -73,12 +73,12 @@
val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
val random' = Free (random'_name,
- @{typ index} --> @{typ index} --> this_ty');
+ @{typ code_numeral} --> @{typ code_numeral} --> this_ty');
fun atom ty = if Sign.of_sort thy (ty, @{sort random})
- then ((ty, false), random ty $ @{term "j\<Colon>index"})
+ then ((ty, false), random ty $ @{term "j\<Colon>code_numeral"})
else raise TYP
("Will not generate random elements for type(s) " ^ quote (hd tycos));
- fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"});
+ fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"});
fun rtyp tyco tys = raise REC
("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
val rhss = DatatypePackage.construction_interpretation thy
@@ -87,9 +87,9 @@
|> (map o apsnd) (List.partition fst)
|> map (mk_clauses thy this_ty)
val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
- (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ Random.seed},
+ (random' $ @{term "0\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"}, Abs ("s", @{typ Random.seed},
Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))),
- (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
+ (random' $ @{term "Suc_code_numeral i"} $ @{term "j\<Colon>code_numeral"}, rhs)
]))) rhss;
in eqss end;
fun random_inst [tyco] thy =
@@ -99,8 +99,8 @@
(curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco;
val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
- (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
- random' $ @{term "max (i\<Colon>index) 1"} $ @{term "i\<Colon>index"})
+ (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>code_numeral"},
+ random' $ @{term "max (i\<Colon>code_numeral) 1"} $ @{term "i\<Colon>code_numeral"})
val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
(fn thm => Context.mapping (Code.del_eqn thm) I));
fun add_code simps lthy =
--- a/src/HOL/ex/predicate_compile.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/HOL/ex/predicate_compile.ML Fri May 22 13:22:16 2009 -0700
@@ -1,4 +1,4 @@
-(* Author: Lukas Bulwahn
+(* Author: Lukas Bulwahn, TU Muenchen
(Prototype of) A compiler from predicates specified by intro/elim rules
to equations.
@@ -13,14 +13,15 @@
val strip_intro_concl: term -> int -> term * (term list * term list)
val modename_of: theory -> string -> mode -> string
val modes_of: theory -> string -> mode list
+ val pred_intros: theory -> string -> thm list
+ val get_nparams: theory -> string -> int
val setup: theory -> theory
val code_pred: string -> Proof.context -> Proof.state
val code_pred_cmd: string -> Proof.context -> Proof.state
val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*)
val do_proofs: bool ref
- val pred_intros : theory -> string -> thm list
- val get_nparams : theory -> string -> int
- val pred_term_of : theory -> term -> term option
+ val analyze_compr: theory -> term -> term
+ val eval_ref: (unit -> term Predicate.pred) option ref
end;
structure Predicate_Compile : PREDICATE_COMPILE =
@@ -1425,29 +1426,37 @@
(*FIXME
- Naming of auxiliary rules necessary?
+- add default code equations P x y z = P_i_i_i x y z
*)
(* transformation for code generation *)
-fun pred_term_of thy t = let
- val (vars, body) = strip_abs t
- val (pred, all_args) = strip_comb body
- val (name, T) = dest_Const pred
- val (params, args) = chop (get_nparams thy name) all_args
- val user_mode = flat (map_index
- (fn (i, t) => case t of Bound j => if j < length vars then [] else [i+1] | _ => [i+1])
- args)
- val (inargs, _) = get_args user_mode args
- val all_modes = Symtab.dest (#modes (IndCodegenData.get thy))
- val modes = filter (fn Mode (_, is, _) => is = user_mode) (modes_of_term all_modes (list_comb (pred, params)))
- fun compile m = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)), inargs)
- in
- case modes of
- [] => (let val _ = error "No mode possible for this term" in NONE end)
- | [m] => SOME (compile m)
- | ms => (let val _ = warning "Multiple modes possible for this term"
- in SOME (compile (hd ms)) end)
- end;
+val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
+
+fun analyze_compr thy t_compr =
+ let
+ val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
+ | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
+ val (body, Ts, fp) = HOLogic.strip_split split;
+ (*FIXME former order of tuple positions must be restored*)
+ val (pred as Const (name, T), all_args) = strip_comb body
+ val (params, args) = chop (get_nparams thy name) all_args
+ val user_mode = map_filter I (map_index
+ (fn (i, t) => case t of Bound j => if j < length Ts then NONE
+ else SOME (i+1) | _ => SOME (i+1)) args) (*FIXME dangling bounds should not occur*)
+ val (inargs, _) = get_args user_mode args;
+ val all_modes = Symtab.dest (#modes (IndCodegenData.get thy));
+ val modes = filter (fn Mode (_, is, _) => is = user_mode)
+ (modes_of_term all_modes (list_comb (pred, params)));
+ val m = case modes
+ of [] => error ("No mode possible for comprehension "
+ ^ Syntax.string_of_term_global thy t_compr)
+ | [m] => m
+ | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
+ ^ Syntax.string_of_term_global thy t_compr); m);
+ val t_eval = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)),
+ inargs)
+ in t_eval end;
end;
--- a/src/Pure/General/table.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/Pure/General/table.ML Fri May 22 13:22:16 2009 -0700
@@ -33,11 +33,11 @@
val max_key: 'a table -> key option
val defined: 'a table -> key -> bool
val lookup: 'a table -> key -> 'a option
- val update: (key * 'a) -> 'a table -> 'a table
- val update_new: (key * 'a) -> 'a table -> 'a table (*exception DUP*)
+ val update: key * 'a -> 'a table -> 'a table
+ val update_new: key * 'a -> 'a table -> 'a table (*exception DUP*)
val default: key * 'a -> 'a table -> 'a table
val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
- val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
+ val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
val make: (key * 'a) list -> 'a table (*exception DUP*)
val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
'a table * 'a table -> 'a table (*exception DUP*)
@@ -48,7 +48,7 @@
val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*)
val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
val lookup_list: 'a list table -> key -> 'a list
- val cons_list: (key * 'a) -> 'a list table -> 'a list table
+ val cons_list: key * 'a -> 'a list table -> 'a list table
val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
--- a/src/Pure/Isar/class_target.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/Pure/Isar/class_target.ML Fri May 22 13:22:16 2009 -0700
@@ -441,8 +441,8 @@
fun synchronize_inst_syntax ctxt =
let
val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
- val thy = ProofContext.theory_of ctxt;
- fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
+ val inst_tyco_of = AxClass.inst_tyco_of (Sign.consts_of (ProofContext.theory_of ctxt));
+ fun subst (c, ty) = case inst_tyco_of (c, ty)
of SOME tyco => (case AList.lookup (op =) params (c, tyco)
of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
| NONE => NONE)
@@ -512,9 +512,11 @@
fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
of NONE => NONE
| SOME ts' => SOME (ts', ctxt);
- fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
+ val inst_tyco_of = AxClass.inst_tyco_of consts;
+ val typ_instance = Type.typ_instance (Sign.tsig_of thy);
+ fun improve (c, ty) = case inst_tyco_of (c, ty)
of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
- of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
+ of SOME (_, ty') => if typ_instance (ty', ty)
then SOME (ty, ty') else NONE
| NONE => NONE)
| NONE => NONE;
--- a/src/Pure/axclass.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/Pure/axclass.ML Fri May 22 13:22:16 2009 -0700
@@ -26,9 +26,9 @@
val axiomatize_arity: arity -> theory -> theory
val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
val instance_name: string * class -> string
+ val inst_tyco_of: Consts.T -> string * typ -> string option
val declare_overloaded: string * typ -> theory -> term * theory
val define_overloaded: binding -> string * term -> theory -> thm * theory
- val inst_tyco_of: theory -> string * typ -> string option
val unoverload: theory -> thm -> thm
val overload: theory -> thm -> thm
val unoverload_conv: theory -> conv
@@ -249,7 +249,8 @@
fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
(get_inst_params thy) [];
-fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy);
+fun inst_tyco_of consts = try (fst o dest_Type o the_single o Consts.typargs consts);
+val inst_tyco_of' = inst_tyco_of o Sign.consts_of;
fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
@@ -259,7 +260,7 @@
fun unoverload_const thy (c_ty as (c, _)) =
case class_of_param thy c
- of SOME class => (case inst_tyco_of thy c_ty
+ of SOME class => (case inst_tyco_of' thy c_ty
of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
| NONE => c)
| NONE => c;
@@ -293,7 +294,7 @@
val class = case class_of_param thy c
of SOME class => class
| NONE => error ("Not a class parameter: " ^ quote c);
- val tyco = case inst_tyco_of thy (c, T)
+ val tyco = case inst_tyco_of' thy (c, T)
of SOME tyco => tyco
| NONE => error ("Illegal type for instantiation of class parameter: "
^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
@@ -318,7 +319,7 @@
fun define_overloaded b (c, t) thy =
let
val T = Term.fastype_of t;
- val SOME tyco = inst_tyco_of thy (c, T);
+ val SOME tyco = inst_tyco_of' thy (c, T);
val (c', eq) = get_inst_param thy (c, tyco);
val prop = Logic.mk_equals (Const (c', T), t);
val b' = Thm.def_binding_optional
--- a/src/Tools/value.ML Fri May 22 13:18:59 2009 -0700
+++ b/src/Tools/value.ML Fri May 22 13:22:16 2009 -0700
@@ -46,7 +46,7 @@
of NONE => value ctxt t
| SOME name => value_select name ctxt t;
val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t ctxt;
+ val ctxt' = Variable.auto_fixes t' ctxt;
val p = PrintMode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();