Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/README Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,8 @@
+Isabelle application bundle for MacOS
+=====================================
+
+Requirements:
+
+* CocoaDialog http://cocoadialog.sourceforge.net/
+
+* Platypus http://www.sveinbjorn.org/platypus
Binary file Admin/MacOS/isabelle.icns has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/mk Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,19 @@
+#!/bin/bash
+#
+# Make Isabelle application bundle
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+
+PLATYPUS_APP="/Applications/Platypus-4.0/Platypus.app"
+COCOADIALOG_APP="/Applications/CocoaDialog.app"
+
+"$PLATYPUS_APP/Contents/Resources/platypus" \
+ -a Isabelle -u Isabelle \
+ -I "de.tum.in.isabelle" \
+ -i "$THIS/isabelle.icns" \
+ -D -X .thy \
+ -p /bin/bash \
+ -c "$THIS/script" \
+ -o None \
+ -f "$COCOADIALOG_APP" \
+ "$THIS/Isabelle.app"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/script Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,59 @@
+#!/bin/bash
+#
+# Author: Makarius
+#
+# Isabelle application wrapper
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+
+
+# global defaults
+ISABELLE_TOOL=""
+ISABELLE_INTERFACE="emacs"
+#ISABELLE_INTERFACE="jedit"
+
+
+# sane environment defaults
+PATH="$PATH:/opt/local/bin"
+cd "$HOME"
+
+
+# Isabelle location
+
+if [ -z "$ISABELLE_TOOL" ]; then
+ if [ -e "$THIS/Isabelle/bin/isabelle" ]; then
+ ISABELLE_TOOL="$THIS/Isabelle/bin/isabelle"
+ elif [ -e "$HOME/bin/isabelle" ]; then
+ ISABELLE_TOOL="$HOME/bin/isabelle"
+ else
+ ISABELLE_TOOL=isabelle
+ fi
+fi
+
+
+# run interface
+
+OUTPUT="/tmp/isabelle$$.out"
+
+( "$HOME/bin/isabelle" "$ISABELLE_INTERFACE" "$@" ) > "$OUTPUT" 2>&1
+RC=$?
+
+if [ "$RC" != 0 ]; then
+ echo >> "$OUTPUT"
+ echo "Return code: $RC" >> "$OUTPUT"
+fi
+
+
+# error feedback
+
+if [ -n "$OUTPUT" ]; then
+ "$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" textbox \
+ --title "Isabelle" \
+ --informative-text "Isabelle output" \
+ --text-from-file "$OUTPUT" \
+ --button1 "OK"
+fi
+
+rm -f "$OUTPUT"
+
+exit "$RC"
Binary file Admin/MacOS/theory.icns has changed
--- a/NEWS Mon Dec 15 10:40:52 2008 +0000
+++ b/NEWS Fri Dec 19 11:49:08 2008 +0000
@@ -239,6 +239,9 @@
mechanisms may be specified (currently, [SML], [code] or [nbe]). See
further src/HOL/ex/Eval_Examples.thy.
+* New method "sizechange" to automate termination proofs using (a
+modification of) the size-change principle. Requires SAT solver.
+
* HOL/Orderings: class "wellorder" moved here, with explicit induction
rule "less_induct" as assumption. For instantiation of "wellorder" by
means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Dec 19 11:49:08 2008 +0000
@@ -804,12 +804,15 @@
@{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
@{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
@{method_def (HOL) metis} & : & @{text method} \\
\end{matharray}
\begin{rail}
'sledgehammer' (nameref *)
;
+ 'atp\_messages' ('(' nat ')')?
+ ;
'metis' thmrefs
;
@@ -842,6 +845,12 @@
\item @{command (HOL) atp_kill} terminates all presently running
provers.
+ \item @{command (HOL) atp_messages} displays recent messages issued
+ by automated theorem provers. This allows to examine results that
+ might have got lost due to the asynchronous nature of default
+ @{command (HOL) sledgehammer} output. An optional message limit may
+ be specified (default 5).
+
\item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
with the given facts. Metis is an automated proof tool of medium
strength, but is fully integrated into Isabelle/HOL, with explicit
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 15 10:40:52 2008 +0000
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Dec 19 11:49:08 2008 +0000
@@ -814,12 +814,15 @@
\indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
\end{matharray}
\begin{rail}
'sledgehammer' (nameref *)
;
+ 'atp\_messages' ('(' nat ')')?
+ ;
'metis' thmrefs
;
@@ -850,6 +853,12 @@
\item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
provers.
+ \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
+ by automated theorem provers. This allows to examine results that
+ might have got lost due to the asynchronous nature of default
+ \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. An optional message limit may
+ be specified (default 5).
+
\item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
with the given facts. Metis is an automated proof tool of medium
strength, but is fully integrated into Isabelle/HOL, with explicit
--- a/etc/isar-keywords-ZF.el Mon Dec 15 10:40:52 2008 +0000
+++ b/etc/isar-keywords-ZF.el Fri Dec 19 11:49:08 2008 +0000
@@ -200,7 +200,6 @@
"use"
"use_thy"
"using"
- "value"
"welcome"
"with"
"{"
@@ -323,7 +322,6 @@
"typ"
"unused_thms"
"use_thy"
- "value"
"welcome"))
(defconst isar-keywords-theory-begin
--- a/etc/isar-keywords.el Mon Dec 15 10:40:52 2008 +0000
+++ b/etc/isar-keywords.el Fri Dec 19 11:49:08 2008 +0000
@@ -32,6 +32,7 @@
"atom_decl"
"atp_info"
"atp_kill"
+ "atp_messages"
"automaton"
"ax_specification"
"axclass"
@@ -331,6 +332,7 @@
"ML_val"
"atp_info"
"atp_kill"
+ "atp_messages"
"cd"
"class_deps"
"code_deps"
--- a/lib/jedit/isabelle.xml Mon Dec 15 10:40:52 2008 +0000
+++ b/lib/jedit/isabelle.xml Fri Dec 19 11:49:08 2008 +0000
@@ -56,6 +56,7 @@
<OPERATOR>atom_decl</OPERATOR>
<LABEL>atp_info</LABEL>
<LABEL>atp_kill</LABEL>
+ <LABEL>atp_messages</LABEL>
<KEYWORD4>attach</KEYWORD4>
<OPERATOR>automaton</OPERATOR>
<KEYWORD4>avoids</KEYWORD4>
@@ -154,7 +155,6 @@
<KEYWORD4>if</KEYWORD4>
<KEYWORD4>imports</KEYWORD4>
<KEYWORD4>in</KEYWORD4>
- <KEYWORD4>includes</KEYWORD4>
<KEYWORD4>induction</KEYWORD4>
<OPERATOR>inductive</OPERATOR>
<KEYWORD1>inductive_cases</KEYWORD1>
@@ -286,6 +286,7 @@
<OPERATOR>statespace</OPERATOR>
<KEYWORD4>structure</KEYWORD4>
<OPERATOR>subclass</OPERATOR>
+ <OPERATOR>sublocale</OPERATOR>
<OPERATOR>subsect</OPERATOR>
<OPERATOR>subsection</OPERATOR>
<OPERATOR>subsubsect</OPERATOR>
--- a/src/HOL/FunDef.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/FunDef.thy Fri Dec 19 11:49:08 2008 +0000
@@ -3,11 +3,13 @@
Author: Alexander Krauss, TU Muenchen
*)
-header {* General recursive function definitions *}
+header {* Function Definitions and Termination Proofs *}
theory FunDef
imports Wellfounded
uses
+ "Tools/prop_logic.ML"
+ "Tools/sat_solver.ML"
("Tools/function_package/fundef_lib.ML")
("Tools/function_package/fundef_common.ML")
("Tools/function_package/inductive_wrap.ML")
@@ -22,9 +24,14 @@
("Tools/function_package/lexicographic_order.ML")
("Tools/function_package/fundef_datatype.ML")
("Tools/function_package/induction_scheme.ML")
+ ("Tools/function_package/termination.ML")
+ ("Tools/function_package/decompose.ML")
+ ("Tools/function_package/descent.ML")
+ ("Tools/function_package/scnp_solve.ML")
+ ("Tools/function_package/scnp_reconstruct.ML")
begin
-text {* Definitions with default value. *}
+subsection {* Definitions with default value. *}
definition
THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
@@ -97,9 +104,6 @@
"wf R \<Longrightarrow> wfP (in_rel R)"
by (simp add: wfP_def)
-inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
-where is_measure_trivial: "is_measure f"
-
use "Tools/function_package/fundef_lib.ML"
use "Tools/function_package/fundef_common.ML"
use "Tools/function_package/inductive_wrap.ML"
@@ -110,19 +114,37 @@
use "Tools/function_package/pattern_split.ML"
use "Tools/function_package/auto_term.ML"
use "Tools/function_package/fundef_package.ML"
-use "Tools/function_package/measure_functions.ML"
-use "Tools/function_package/lexicographic_order.ML"
use "Tools/function_package/fundef_datatype.ML"
use "Tools/function_package/induction_scheme.ML"
setup {*
FundefPackage.setup
+ #> FundefDatatype.setup
#> InductionScheme.setup
- #> MeasureFunctions.setup
- #> LexicographicOrder.setup
- #> FundefDatatype.setup
*}
+subsection {* Measure Functions *}
+
+inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
+where is_measure_trivial: "is_measure f"
+
+use "Tools/function_package/measure_functions.ML"
+setup MeasureFunctions.setup
+
+lemma measure_size[measure_function]: "is_measure size"
+by (rule is_measure_trivial)
+
+lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
+by (rule is_measure_trivial)
+lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
+by (rule is_measure_trivial)
+
+use "Tools/function_package/lexicographic_order.ML"
+setup LexicographicOrder.setup
+
+
+subsection {* Congruence Rules *}
+
lemma let_cong [fundef_cong]:
"M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
unfolding Let_def by blast
@@ -140,17 +162,7 @@
"f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
unfolding o_apply .
-subsection {* Setup for termination proofs *}
-
-text {* Rules for generating measure functions *}
-
-lemma [measure_function]: "is_measure size"
-by (rule is_measure_trivial)
-
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
-by (rule is_measure_trivial)
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
-by (rule is_measure_trivial)
+subsection {* Simp rules for termination proofs *}
lemma termination_basic_simps[termination_simp]:
"x < (y::nat) \<Longrightarrow> x < y + z"
@@ -166,5 +178,150 @@
"prod_size f g p = f (fst p) + g (snd p) + Suc 0"
by (induct p) auto
+subsection {* Decomposition *}
+
+lemma less_by_empty:
+ "A = {} \<Longrightarrow> A \<subseteq> B"
+and union_comp_emptyL:
+ "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
+and union_comp_emptyR:
+ "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
+and wf_no_loop:
+ "R O R = {} \<Longrightarrow> wf R"
+by (auto simp add: wf_comp_self[of R])
+
+
+subsection {* Reduction Pairs *}
+
+definition
+ "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
+
+lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
+unfolding reduction_pair_def by auto
+
+lemma reduction_pair_lemma:
+ assumes rp: "reduction_pair P"
+ assumes "R \<subseteq> fst P"
+ assumes "S \<subseteq> snd P"
+ assumes "wf S"
+ shows "wf (R \<union> S)"
+proof -
+ from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
+ unfolding reduction_pair_def by auto
+ with `wf S` have "wf (fst P \<union> S)"
+ by (auto intro: wf_union_compatible)
+ moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
+ ultimately show ?thesis by (rule wf_subset)
+qed
+
+definition
+ "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
+
+lemma rp_inv_image_rp:
+ "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
+ unfolding reduction_pair_def rp_inv_image_def split_def
+ by force
+
+
+subsection {* Concrete orders for SCNP termination proofs *}
+
+definition "pair_less = less_than <*lex*> less_than"
+definition "pair_leq = pair_less^="
+definition "max_strict = max_ext pair_less"
+definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition "min_strict = min_ext pair_less"
+definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
+
+lemma wf_pair_less[simp]: "wf pair_less"
+ by (auto simp: pair_less_def)
+
+text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
+lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
+ and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
+ and pair_lessI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
+ and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
+ unfolding pair_leq_def pair_less_def by auto
+
+text {* Introduction rules for max *}
+lemma smax_emptyI:
+ "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
+ and smax_insertI:
+ "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
+ and wmax_emptyI:
+ "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
+ and wmax_insertI:
+ "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
+unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
+
+text {* Introduction rules for min *}
+lemma smin_emptyI:
+ "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
+ and smin_insertI:
+ "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
+ and wmin_emptyI:
+ "(X, {}) \<in> min_weak"
+ and wmin_insertI:
+ "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
+by (auto simp: min_strict_def min_weak_def min_ext_def)
+
+text {* Reduction Pairs *}
+
+lemma max_ext_compat:
+ assumes "S O R \<subseteq> R"
+ shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
+using assms
+apply auto
+apply (elim max_ext.cases)
+apply rule
+apply auto[3]
+apply (drule_tac x=xa in meta_spec)
+apply simp
+apply (erule bexE)
+apply (drule_tac x=xb in meta_spec)
+by auto
+
+lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
+ unfolding max_strict_def max_weak_def
+apply (intro reduction_pairI max_ext_wf)
+apply simp
+apply (rule max_ext_compat)
+by (auto simp: pair_less_def pair_leq_def)
+
+lemma min_ext_compat:
+ assumes "S O R \<subseteq> R"
+ shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
+using assms
+apply (auto simp: min_ext_def)
+apply (drule_tac x=ya in bspec, assumption)
+apply (erule bexE)
+apply (drule_tac x=xc in bspec)
+apply assumption
+by auto
+
+lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
+ unfolding min_strict_def min_weak_def
+apply (intro reduction_pairI min_ext_wf)
+apply simp
+apply (rule min_ext_compat)
+by (auto simp: pair_less_def pair_leq_def)
+
+
+subsection {* Tool setup *}
+
+use "Tools/function_package/termination.ML"
+use "Tools/function_package/decompose.ML"
+use "Tools/function_package/descent.ML"
+use "Tools/function_package/scnp_solve.ML"
+use "Tools/function_package/scnp_reconstruct.ML"
+
+setup {* ScnpReconstruct.setup *}
+(*
+setup {*
+ Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp
+ [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
+*}
+*)
+
+
end
--- a/src/HOL/IsaMakefile Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/IsaMakefile Fri Dec 19 11:49:08 2008 +0000
@@ -112,6 +112,8 @@
Tools/dseq.ML \
Tools/function_package/auto_term.ML \
Tools/function_package/context_tree.ML \
+ Tools/function_package/decompose.ML \
+ Tools/function_package/descent.ML \
Tools/function_package/fundef_common.ML \
Tools/function_package/fundef_core.ML \
Tools/function_package/fundef_datatype.ML \
@@ -123,8 +125,11 @@
Tools/function_package/measure_functions.ML \
Tools/function_package/mutual.ML \
Tools/function_package/pattern_split.ML \
+ Tools/function_package/scnp_reconstruct.ML \
+ Tools/function_package/scnp_solve.ML \
Tools/function_package/size.ML \
Tools/function_package/sum_tree.ML \
+ Tools/function_package/termination.ML \
Tools/hologic.ML \
Tools/inductive_codegen.ML \
Tools/inductive_package.ML \
--- a/src/HOL/Library/Multiset.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/Library/Multiset.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1481,4 +1481,155 @@
@{term "{#x+x|x:#M. x<c#}"}.
*}
+
+subsection {* Termination proofs with multiset orders *}
+
+lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
+ and multi_member_this: "x \<in># {# x #} + XS"
+ and multi_member_last: "x \<in># {# x #}"
+ by auto
+
+definition "ms_strict = mult pair_less"
+definition "ms_weak = ms_strict \<union> Id"
+
+lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
+unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
+by (auto intro: wf_mult1 wf_trancl simp: mult_def)
+
+lemma smsI:
+ "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
+ unfolding ms_strict_def
+by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
+
+lemma wmsI:
+ "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
+ \<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
+unfolding ms_weak_def ms_strict_def
+by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
+
+inductive pw_leq
+where
+ pw_leq_empty: "pw_leq {#} {#}"
+| pw_leq_step: "\<lbrakk>(x,y) \<in> pair_leq; pw_leq X Y \<rbrakk> \<Longrightarrow> pw_leq ({#x#} + X) ({#y#} + Y)"
+
+lemma pw_leq_lstep:
+ "(x, y) \<in> pair_leq \<Longrightarrow> pw_leq {#x#} {#y#}"
+by (drule pw_leq_step) (rule pw_leq_empty, simp)
+
+lemma pw_leq_split:
+ assumes "pw_leq X Y"
+ shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+ using assms
+proof (induct)
+ case pw_leq_empty thus ?case by auto
+next
+ case (pw_leq_step x y X Y)
+ then obtain A B Z where
+ [simp]: "X = A + Z" "Y = B + Z"
+ and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
+ by auto
+ from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
+ unfolding pair_leq_def by auto
+ thus ?case
+ proof
+ assume [simp]: "x = y"
+ have
+ "{#x#} + X = A + ({#y#}+Z)
+ \<and> {#y#} + Y = B + ({#y#}+Z)
+ \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+ by (auto simp: add_ac)
+ thus ?case by (intro exI)
+ next
+ assume A: "(x, y) \<in> pair_less"
+ let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
+ have "{#x#} + X = ?A' + Z"
+ "{#y#} + Y = ?B' + Z"
+ by (auto simp add: add_ac)
+ moreover have
+ "(set_of ?A', set_of ?B') \<in> max_strict"
+ using 1 A unfolding max_strict_def
+ by (auto elim!: max_ext.cases)
+ ultimately show ?thesis by blast
+ qed
+qed
+
+lemma
+ assumes pwleq: "pw_leq Z Z'"
+ shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
+ and ms_weakI1: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
+ and ms_weakI2: "(Z + {#}, Z' + {#}) \<in> ms_weak"
+proof -
+ from pw_leq_split[OF pwleq]
+ obtain A' B' Z''
+ where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
+ and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
+ by blast
+ {
+ assume max: "(set_of A, set_of B) \<in> max_strict"
+ from mx_or_empty
+ have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
+ proof
+ assume max': "(set_of A', set_of B') \<in> max_strict"
+ with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
+ by (auto simp: max_strict_def intro: max_ext_additive)
+ thus ?thesis by (rule smsI)
+ next
+ assume [simp]: "A' = {#} \<and> B' = {#}"
+ show ?thesis by (rule smsI) (auto intro: max)
+ qed
+ thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
+ thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
+ }
+ from mx_or_empty
+ have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
+ thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
+qed
+
+lemma empty_idemp: "{#} + x = x" "x + {#} = x"
+and nonempty_plus: "{# x #} + rs \<noteq> {#}"
+and nonempty_single: "{# x #} \<noteq> {#}"
+by auto
+
+setup {*
+let
+ fun msetT T = Type ("Multiset.multiset", [T]);
+
+ fun mk_mset T [] = Const (@{const_name Mempty}, msetT T)
+ | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
+ | mk_mset T (x :: xs) =
+ Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
+ mk_mset T [x] $ mk_mset T xs
+
+ fun mset_member_tac m i =
+ (if m <= 0 then
+ rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i
+ else
+ rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i)
+
+ val mset_nonempty_tac =
+ rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
+
+ val regroup_munion_conv =
+ FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+ (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
+
+ fun unfold_pwleq_tac i =
+ (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
+ ORELSE (rtac @{thm pw_leq_lstep} i)
+ ORELSE (rtac @{thm pw_leq_empty} i)
+
+ val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
+ @{thm Un_insert_left}, @{thm Un_empty_left}]
+in
+ ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
+ {
+ msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
+ mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
+ mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
+ smsI'=@{thm ms_strictI}, wmsI2''=@{thm ms_weakI2}, wmsI1=@{thm ms_weakI1},
+ reduction_pair=@{thm ms_reduction_pair}
+ })
end
+*}
+
+end
--- a/src/HOL/Nominal/Nominal.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/Nominal/Nominal.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1262,19 +1262,21 @@
apply (simp add: pt_rev_pi [OF pt at])
done
-lemma insert_eqvt:
+lemma pt_insert_eqvt:
+ fixes pi::"'x prm"
+ and x::"'a"
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
- shows "(pi::'x prm)\<bullet>(insert (x::'a) X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+ shows "(pi\<bullet>(insert x X)) = insert (pi\<bullet>x) (pi\<bullet>X)"
by (auto simp add: perm_set_eq [OF pt at])
-lemma set_eqvt:
+lemma pt_set_eqvt:
fixes pi :: "'x prm"
and xs :: "'a list"
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs) (auto simp add: empty_eqvt insert_eqvt [OF pt at])
+by (induct xs) (auto simp add: empty_eqvt pt_insert_eqvt [OF pt at])
lemma supp_singleton:
assumes pt: "pt TYPE('a) TYPE('x)"
@@ -1568,10 +1570,10 @@
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
apply(drule_tac x="pi\<bullet>xa" in bspec)
apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt [OF ptb at])
+apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
done
--- a/src/HOL/Nominal/nominal_atoms.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/Nominal/nominal_atoms.ML Fri Dec 19 11:49:08 2008 +0000
@@ -798,8 +798,8 @@
val pt_perm_supp_ineq = @{thm "Nominal.pt_perm_supp_ineq"};
val pt_perm_supp = @{thm "Nominal.pt_perm_supp"};
val subseteq_eqvt = @{thm "Nominal.pt_subseteq_eqvt"};
- val insert_eqvt = @{thm "Nominal.insert_eqvt"};
- val set_eqvt = @{thm "Nominal.set_eqvt"};
+ val insert_eqvt = @{thm "Nominal.pt_insert_eqvt"};
+ val set_eqvt = @{thm "Nominal.pt_set_eqvt"};
val perm_set_eq = @{thm "Nominal.perm_set_eq"};
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
--- a/src/HOL/Tools/atp_manager.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/Tools/atp_manager.ML Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/atp_manager.ML
- ID: $Id$
Author: Fabian Immler, TU Muenchen
ATP threads are registered here.
@@ -19,6 +18,7 @@
val set_timeout: int -> unit
val kill: unit -> unit
val info: unit -> unit
+ val messages: int option -> unit
type prover = int -> Proof.state -> bool * string
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
@@ -30,6 +30,9 @@
(** preferences **)
+val message_store_limit = 20;
+val message_display_limit = 5;
+
local
val atps = ref "e";
@@ -85,13 +88,14 @@
{timeout_heap: ThreadHeap.T,
oldest_heap: ThreadHeap.T,
active: (Thread.thread * (Time.time * Time.time * string)) list,
- cancelling: (Thread.thread * (Time.time * Time.time * string)) list};
+ cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
+ messages: string list};
-fun make_state timeout_heap oldest_heap active cancelling =
+fun make_state timeout_heap oldest_heap active cancelling messages =
State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
- active = active, cancelling = cancelling};
+ active = active, cancelling = cancelling, messages = messages};
-val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] []);
+val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] []);
(* the managing thread *)
@@ -103,7 +107,7 @@
(* unregister thread from thread manager -- move to cancelling *)
fun unregister (success, message) thread = Synchronized.change_result state
- (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+ (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
let
val info = lookup_thread active thread
@@ -127,7 +131,12 @@
| SOME (_, _, desc) => "Sledgehammer: " ^ desc ^ "\n" ^ message ^
(if null group_threads then ""
else "\nInterrupted " ^ string_of_int (length group_threads - 1) ^ " other group members")
- in (message', make_state timeout_heap oldest_heap active'' cancelling'') end);
+
+ val messages' = case info of NONE => messages
+ | SOME (_, _, desc) => desc ^ "\n" ^ message ::
+ (if length messages <= message_store_limit then messages
+ else #1 (chop message_store_limit messages))
+ in (message', make_state timeout_heap oldest_heap active'' cancelling'' messages') end);
(* kill excessive atp threads *)
@@ -140,12 +149,13 @@
fun kill_oldest () =
let exception Unchanged in
- Synchronized.change_result state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+ Synchronized.change_result state
+ (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
then raise Unchanged
else
let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
- in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling) end)
+ in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages) end)
|> (priority o unregister (false, "Interrupted (maximum number of ATPs exceeded)"))
handle Unchanged => ()
end;
@@ -175,7 +185,7 @@
| SOME (time, _) => SOME time)
(* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *)
- fun action (State {timeout_heap, oldest_heap, active, cancelling}) =
+ fun action (State {timeout_heap, oldest_heap, active, cancelling, messages}) =
let val (timeout_threads, timeout_heap') =
ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
in
@@ -185,7 +195,7 @@
let
val _ = List.app (SimpleThread.interrupt o #1) cancelling
val cancelling' = filter (Thread.isActive o #1) cancelling
- val state' = make_state timeout_heap' oldest_heap active cancelling'
+ val state' = make_state timeout_heap' oldest_heap active cancelling' messages
in SOME (map #2 timeout_threads, state') end
end
in
@@ -203,12 +213,13 @@
fun register birthtime deadtime (thread, desc) =
(check_thread_manager ();
- Synchronized.change state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
- let
- val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
- val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
- val active' = update_thread (thread, (birthtime, deadtime, desc)) active
- in make_state timeout_heap' oldest_heap' active' cancelling end));
+ Synchronized.change state
+ (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+ let
+ val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
+ val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
+ val active' = update_thread (thread, (birthtime, deadtime, desc)) active
+ in make_state timeout_heap' oldest_heap' active' cancelling messages end));
@@ -217,16 +228,17 @@
(* kill: move all threads to cancelling *)
fun kill () = Synchronized.change state
- (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+ (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
- in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) end);
+ in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages end);
-(* info: information on running threads *)
+(* ATP info *)
fun info () =
let
- val State {timeout_heap, oldest_heap, active, cancelling} = Synchronized.value state
+ val State {active, cancelling, ...} = Synchronized.value state
+
fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), birth_time))
^ " s -- "
@@ -235,6 +247,7 @@
fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), dead_time))
^ " s:\n" ^ desc
+
val running =
if null active then "No ATPs running."
else space_implode "\n\n" ("Running ATPs:" :: map running_info active)
@@ -242,8 +255,17 @@
if null cancelling then ""
else space_implode "\n\n"
("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling)
+
in writeln (running ^ "\n" ^ interrupting) end;
+fun messages opt_limit =
+ let
+ val limit = the_default message_display_limit opt_limit;
+ val State {messages = msgs, ...} = Synchronized.value state
+ val header = "Recent ATP messages" ^
+ (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
+ in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
+
(** The Sledgehammer **)
@@ -322,6 +344,11 @@
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
val _ =
+ OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
+ (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+ (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+
+val _ =
OuterSyntax.improper_command "print_atps" "print external provers" K.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
Toplevel.keep (print_provers o Toplevel.theory_of)));
@@ -329,7 +356,7 @@
val _ =
OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
(Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
+ Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/decompose.ML Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,105 @@
+(* Title: HOL/Tools/function_package/decompose.ML
+ Author: Alexander Krauss, TU Muenchen
+
+Graph decomposition using "Shallow Dependency Pairs".
+*)
+
+signature DECOMPOSE =
+sig
+
+ val derive_chains : Proof.context -> tactic
+ -> (Termination.data -> int -> tactic)
+ -> Termination.data -> int -> tactic
+
+ val decompose_tac : Proof.context -> tactic
+ -> Termination.ttac
+
+end
+
+structure Decompose : DECOMPOSE =
+struct
+
+structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
+
+
+fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+
+ fun prove_chain c1 c2 D =
+ if is_some (Termination.get_chain D c1 c2) then D else
+ let
+ val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
+ Const (@{const_name "{}"}, fastype_of c1))
+ |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
+
+ val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
+ FundefLib.Solved thm => SOME thm
+ | _ => NONE
+ in
+ Termination.note_chain c1 c2 chain D
+ end
+ in
+ cont (fold_product prove_chain cs cs D) i
+ end)
+
+
+fun mk_dgraph D cs =
+ TermGraph.empty
+ |> fold (fn c => TermGraph.new_node (c,())) cs
+ |> fold_product (fn c1 => fn c2 =>
+ if is_none (Termination.get_chain D c1 c2 |> the_default NONE)
+ then TermGraph.add_edge (c1, c2) else I)
+ cs cs
+
+
+fun ucomp_empty_tac T =
+ REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
+ ORELSE' rtac @{thm union_comp_emptyL}
+ ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
+
+fun regroup_calls_tac cs = Termination.CALLS (fn (cs', i) =>
+ let
+ val is = map (fn c => find_index (curry op aconv c) cs') cs
+ in
+ CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
+ end)
+
+
+fun solve_trivial_tac D = Termination.CALLS
+(fn ([c], i) =>
+ (case Termination.get_chain D c c of
+ SOME (SOME thm) => rtac @{thm wf_no_loop} i
+ THEN rtac thm i
+ | _ => no_tac)
+ | _ => no_tac)
+
+fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+ let
+ val G = mk_dgraph D cs
+ val sccs = TermGraph.strong_conn G
+
+ fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
+ | split (SCC::rest) i =
+ regroup_calls_tac SCC i
+ THEN rtac @{thm wf_union_compatible} i
+ THEN rtac @{thm less_by_empty} (i + 2)
+ THEN ucomp_empty_tac (the o the oo Termination.get_chain D) (i + 2)
+ THEN split rest (i + 1)
+ THEN (solve_trivial_tac D i ORELSE cont D i)
+ in
+ if length sccs > 1 then split sccs i
+ else solve_trivial_tac D i ORELSE err_cont D i
+ end)
+
+fun decompose_tac ctxt chain_tac cont err_cont =
+ derive_chains ctxt chain_tac
+ (decompose_tac' ctxt cont err_cont)
+
+fun auto_decompose_tac ctxt =
+ Termination.TERMINATION ctxt
+ (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
+ (K (K all_tac)) (K (K no_tac)))
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/descent.ML Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,44 @@
+(* Title: HOL/Tools/function_package/descent.ML
+ Author: Alexander Krauss, TU Muenchen
+
+Descent proofs for termination
+*)
+
+
+signature DESCENT =
+sig
+
+ val derive_diag : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+ -> Termination.data -> int -> tactic
+
+ val derive_all : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+ -> Termination.data -> int -> tactic
+
+end
+
+
+structure Descent : DESCENT =
+struct
+
+fun gen_descent diag ctxt tac cont D = Termination.CALLS (fn (cs, i) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val measures_of = Termination.get_measures D
+
+ fun derive c D =
+ let
+ val (_, p, _, q, _, _) = Termination.dest_call D c
+ in
+ if diag andalso p = q
+ then fold (fn m => Termination.derive_descent thy tac c m m) (measures_of p) D
+ else fold_product (Termination.derive_descent thy tac c)
+ (measures_of p) (measures_of q) D
+ end
+ in
+ cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
+ end)
+
+val derive_diag = gen_descent true
+val derive_all = gen_descent false
+
+end
--- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Fri Dec 19 11:49:08 2008 +0000
@@ -130,4 +130,50 @@
| SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
+fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) =
+ if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
+ | dest_binop_list _ t = [ t ]
+
+
+(* separate two parts in a +-expression:
+ "a + b + c + d + e" --> "(a + b + d) + (c + e)"
+
+ Here, + can be any binary operation that is AC.
+
+ cn - The name of the binop-constructor (e.g. @{const_name "op Un"})
+ ac - the AC rewrite rules for cn
+ is - the list of indices of the expressions that should become the first part
+ (e.g. [0,1,3] in the above example)
+*)
+
+fun regroup_conv neu cn ac is ct =
+ let
+ val mk = HOLogic.mk_binop cn
+ val t = term_of ct
+ val xs = dest_binop_list cn t
+ val js = 0 upto (length xs) - 1 \\ is
+ val ty = fastype_of t
+ val thy = theory_of_cterm ct
+ in
+ Goal.prove_internal []
+ (cterm_of thy
+ (Logic.mk_equals (t,
+ if is = []
+ then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
+ else if js = []
+ then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
+ else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
+ (K (MetaSimplifier.rewrite_goals_tac ac
+ THEN rtac Drule.reflexive_thm 1))
+ end
+
+(* instance for unions *)
+fun regroup_union_conv t =
+ regroup_conv (@{const_name "{}"})
+ @{const_name "op Un"}
+ (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
+ @{thms "Un_empty_right"} @
+ @{thms "Un_empty_left"})) t
+
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,426 @@
+(* Title: HOL/Tools/function_package/scnp_reconstruct.ML
+ Author: Armin Heller, TU Muenchen
+ Author: Alexander Krauss, TU Muenchen
+
+Proof reconstruction for SCNP
+*)
+
+signature SCNP_RECONSTRUCT =
+sig
+
+ val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
+
+ val setup : theory -> theory
+
+ datatype multiset_setup =
+ Multiset of
+ {
+ msetT : typ -> typ,
+ mk_mset : typ -> term list -> term,
+ mset_regroup_conv : int list -> conv,
+ mset_member_tac : int -> int -> tactic,
+ mset_nonempty_tac : int -> tactic,
+ mset_pwleq_tac : int -> tactic,
+ set_of_simps : thm list,
+ smsI' : thm,
+ wmsI2'' : thm,
+ wmsI1 : thm,
+ reduction_pair : thm
+ }
+
+
+ val multiset_setup : multiset_setup -> theory -> theory
+
+end
+
+structure ScnpReconstruct : SCNP_RECONSTRUCT =
+struct
+
+val PROFILE = FundefCommon.PROFILE
+fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
+
+open ScnpSolve
+
+val natT = HOLogic.natT
+val nat_pairT = HOLogic.mk_prodT (natT, natT)
+
+(* Theory dependencies *)
+
+datatype multiset_setup =
+ Multiset of
+ {
+ msetT : typ -> typ,
+ mk_mset : typ -> term list -> term,
+ mset_regroup_conv : int list -> conv,
+ mset_member_tac : int -> int -> tactic,
+ mset_nonempty_tac : int -> tactic,
+ mset_pwleq_tac : int -> tactic,
+ set_of_simps : thm list,
+ smsI' : thm,
+ wmsI2'' : thm,
+ wmsI1 : thm,
+ reduction_pair : thm
+ }
+
+structure MultisetSetup = TheoryDataFun
+(
+ type T = multiset_setup option
+ val empty = NONE
+ val copy = I;
+ val extend = I;
+ fun merge _ (v1, v2) = if is_some v2 then v2 else v1
+)
+
+val multiset_setup = MultisetSetup.put o SOME
+
+fun undef x = error "undef"
+fun get_multiset_setup thy = MultisetSetup.get thy
+ |> the_default (Multiset
+{ msetT = undef, mk_mset=undef,
+ mset_regroup_conv=undef, mset_member_tac = undef,
+ mset_nonempty_tac = undef, mset_pwleq_tac = undef,
+ set_of_simps = [],reduction_pair = refl,
+ smsI'=refl, wmsI2''=refl, wmsI1=refl })
+
+fun order_rpair _ MAX = @{thm max_rpair_set}
+ | order_rpair msrp MS = msrp
+ | order_rpair _ MIN = @{thm min_rpair_set}
+
+fun ord_intros_max true =
+ (@{thm smax_emptyI}, @{thm smax_insertI})
+ | ord_intros_max false =
+ (@{thm wmax_emptyI}, @{thm wmax_insertI})
+fun ord_intros_min true =
+ (@{thm smin_emptyI}, @{thm smin_insertI})
+ | ord_intros_min false =
+ (@{thm wmin_emptyI}, @{thm wmin_insertI})
+
+fun gen_probl D cs =
+ let
+ val n = Termination.get_num_points D
+ val arity = length o Termination.get_measures D
+ fun measure p i = nth (Termination.get_measures D p) i
+
+ fun mk_graph c =
+ let
+ val (_, p, _, q, _, _) = Termination.dest_call D c
+
+ fun add_edge i j =
+ case Termination.get_descent D c (measure p i) (measure q j)
+ of SOME (Termination.Less _) => cons (i, GTR, j)
+ | SOME (Termination.LessEq _) => cons (i, GEQ, j)
+ | _ => I
+
+ val edges =
+ fold_product add_edge (0 upto arity p - 1) (0 upto arity q - 1) []
+ in
+ G (p, q, edges)
+ end
+ in
+ GP (map arity (0 upto n - 1), map mk_graph cs)
+ end
+
+(* General reduction pair application *)
+fun rem_inv_img ctxt =
+ let
+ val unfold_tac = LocalDefs.unfold_tac ctxt
+ in
+ rtac @{thm subsetI} 1
+ THEN etac @{thm CollectE} 1
+ THEN REPEAT (etac @{thm exE} 1)
+ THEN unfold_tac @{thms inv_image_def}
+ THEN rtac @{thm CollectI} 1
+ THEN etac @{thm conjE} 1
+ THEN etac @{thm ssubst} 1
+ THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
+ @ @{thms Sum_Type.sum_cases})
+ end
+
+(* Sets *)
+
+val setT = HOLogic.mk_setT
+
+fun mk_set T [] = Const (@{const_name "{}"}, setT T)
+ | mk_set T (x :: xs) =
+ Const (@{const_name insert}, T --> setT T --> setT T) $
+ x $ mk_set T xs
+
+fun set_member_tac m i =
+ if m = 0 then rtac @{thm insertI1} i
+ else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
+
+val set_nonempty_tac = rtac @{thm insert_not_empty}
+
+fun set_finite_tac i =
+ rtac @{thm finite.emptyI} i
+ ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
+
+
+(* Reconstruction *)
+
+fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val Multiset
+ { msetT, mk_mset,
+ mset_regroup_conv, mset_member_tac,
+ mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
+ smsI', wmsI2'', wmsI1, reduction_pair=ms_rp }
+ = get_multiset_setup thy
+
+ fun measure_fn p = nth (Termination.get_measures D p)
+
+ fun get_desc_thm cidx m1 m2 bStrict =
+ case Termination.get_descent D (nth cs cidx) m1 m2
+ of SOME (Termination.Less thm) =>
+ if bStrict then thm
+ else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
+ | SOME (Termination.LessEq (thm, _)) =>
+ if not bStrict then thm
+ else sys_error "get_desc_thm"
+ | _ => sys_error "get_desc_thm"
+
+ val (label, lev, sl, covering) = certificate
+
+ fun prove_lev strict g =
+ let
+ val G (p, q, el) = nth gs g
+
+ fun less_proof strict (j, b) (i, a) =
+ let
+ val tag_flag = b < a orelse (not strict andalso b <= a)
+
+ val stored_thm =
+ get_desc_thm g (measure_fn p i) (measure_fn q j)
+ (not tag_flag)
+ |> Conv.fconv_rule (Thm.beta_conversion true)
+
+ val rule = if strict
+ then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
+ else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
+ in
+ rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
+ THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
+ end
+
+ fun steps_tac MAX strict lq lp =
+ let
+ val (empty, step) = ord_intros_max strict
+ in
+ if length lq = 0
+ then rtac empty 1 THEN set_finite_tac 1
+ THEN (if strict then set_nonempty_tac 1 else all_tac)
+ else
+ let
+ val (j, b) :: rest = lq
+ val (i, a) = the (covering g strict j)
+ fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
+ val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
+ in
+ rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
+ end
+ end
+ | steps_tac MIN strict lq lp =
+ let
+ val (empty, step) = ord_intros_min strict
+ in
+ if length lp = 0
+ then rtac empty 1
+ THEN (if strict then set_nonempty_tac 1 else all_tac)
+ else
+ let
+ val (i, a) :: rest = lp
+ val (j, b) = the (covering g strict i)
+ fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
+ val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
+ in
+ rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
+ end
+ end
+ | steps_tac MS strict lq lp =
+ let
+ fun get_str_cover (j, b) =
+ if is_some (covering g true j) then SOME (j, b) else NONE
+ fun get_wk_cover (j, b) = the (covering g false j)
+
+ val qs = lq \\ map_filter get_str_cover lq
+ val ps = map get_wk_cover qs
+
+ fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
+ val iqs = indices lq qs
+ val ips = indices lp ps
+
+ local open Conv in
+ fun t_conv a C =
+ params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
+ val goal_rewrite =
+ t_conv arg1_conv (mset_regroup_conv iqs)
+ then_conv t_conv arg_conv (mset_regroup_conv ips)
+ end
+ in
+ CONVERSION goal_rewrite 1
+ THEN (if strict then rtac smsI' 1
+ else if qs = lq then rtac wmsI2'' 1
+ else rtac wmsI1 1)
+ THEN mset_pwleq_tac 1
+ THEN EVERY (map2 (less_proof false) qs ps)
+ THEN (if strict orelse qs <> lq
+ then LocalDefs.unfold_tac ctxt set_of_simps
+ THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
+ else all_tac)
+ end
+ in
+ rem_inv_img ctxt
+ THEN steps_tac label strict (nth lev q) (nth lev p)
+ end
+
+ val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (mk_set, setT)
+
+ fun tag_pair p (i, tag) =
+ HOLogic.pair_const natT natT $
+ (measure_fn p i $ Bound 0) $ HOLogic.mk_number natT tag
+
+ fun pt_lev (p, lm) = Abs ("x", Termination.get_types D p,
+ mk_set nat_pairT (map (tag_pair p) lm))
+
+ val level_mapping =
+ map_index pt_lev lev
+ |> Termination.mk_sumcases D (setT nat_pairT)
+ |> cterm_of thy
+ in
+ PROFILE "Proof Reconstruction"
+ (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
+ THEN (rtac @{thm reduction_pair_lemma} 1)
+ THEN (rtac @{thm rp_inv_image_rp} 1)
+ THEN (rtac (order_rpair ms_rp label) 1)
+ THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
+ THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy)
+ THEN LocalDefs.unfold_tac ctxt
+ (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
+ THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
+ THEN EVERY (map (prove_lev true) sl)
+ THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
+ end
+
+
+
+local open Termination in
+fun print_cell (SOME (Less _)) = "<"
+ | print_cell (SOME (LessEq _)) = "\<le>"
+ | print_cell (SOME (None _)) = "-"
+ | print_cell (SOME (False _)) = "-"
+ | print_cell (NONE) = "?"
+
+fun print_error ctxt D = CALLS (fn (cs, i) =>
+ let
+ val np = get_num_points D
+ val ms = map (get_measures D) (0 upto np - 1)
+ val tys = map (get_types D) (0 upto np - 1)
+ fun index xs = (1 upto length xs) ~~ xs
+ fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
+ val ims = index (map index ms)
+ val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
+ fun print_call (k, c) =
+ let
+ val (_, p, _, q, _, _) = dest_call D c
+ val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^
+ Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
+ val caller_ms = nth ms p
+ val callee_ms = nth ms q
+ val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
+ fun print_ln (i : int, l) = concat (Int.toString i :: " " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
+ val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
+ " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n"
+ ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
+ in
+ true
+ end
+ fun list_call (k, c) =
+ let
+ val (_, p, _, q, _, _) = dest_call D c
+ val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
+ Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^
+ (Syntax.string_of_term ctxt c))
+ in true end
+ val _ = forall list_call ((1 upto length cs) ~~ cs)
+ val _ = forall print_call ((1 upto length cs) ~~ cs)
+ in
+ all_tac
+ end)
+end
+
+
+fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+ let
+ val gp = gen_probl D cs
+(* val _ = TRACE ("SCNP instance: " ^ makestring gp)*)
+ val certificate = generate_certificate use_tags orders gp
+(* val _ = TRACE ("Certificate: " ^ makestring certificate)*)
+
+ val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
+ in
+ case certificate
+ of NONE => err_cont D i
+ | SOME cert =>
+ if not ms_configured andalso #1 cert = MS
+ then err_cont D i
+ else SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
+ THEN (rtac @{thm wf_empty} i ORELSE cont D i)
+ end)
+
+fun decomp_scnp_tac orders autom_tac ctxt err_cont =
+ let
+ open Termination
+ val derive_diag = Descent.derive_diag ctxt autom_tac
+ val derive_all = Descent.derive_all ctxt autom_tac
+ val decompose = Decompose.decompose_tac ctxt autom_tac
+ val scnp_no_tags = single_scnp_tac false orders ctxt
+ val scnp_full = single_scnp_tac true orders ctxt
+
+ fun first_round c e =
+ derive_diag (REPEAT scnp_no_tags c e)
+
+ val second_round =
+ REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
+
+ val third_round =
+ derive_all oo
+ REPEAT (fn c => fn e =>
+ scnp_full (decompose c c) e)
+
+ fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
+
+ val strategy = Then (Then first_round second_round) third_round
+
+ in
+ TERMINATION ctxt (strategy err_cont err_cont)
+ end
+
+fun decomp_scnp orders ctxt =
+ let
+ val extra_simps = FundefCommon.TerminationSimps.get ctxt
+ val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
+ in
+ Method.SIMPLE_METHOD
+ (TRY (FundefCommon.apply_termination_rule ctxt 1)
+ THEN TRY Termination.wf_union_tac
+ THEN
+ (rtac @{thm wf_empty} 1
+ ORELSE decomp_scnp_tac orders autom_tac ctxt (print_error ctxt) 1))
+ end
+
+
+(* Method setup *)
+
+val orders =
+ (Scan.repeat1
+ ((Args.$$$ "max" >> K MAX) ||
+ (Args.$$$ "min" >> K MIN) ||
+ (Args.$$$ "ms" >> K MS))
+ || Scan.succeed [MAX, MS, MIN])
+
+val setup = Method.add_method
+ ("sizechange", Method.sectioned_args (Scan.lift orders) clasimp_modifiers decomp_scnp,
+ "termination prover with graph decomposition and the NP subset of size change termination")
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/scnp_solve.ML Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,257 @@
+(* Title: HOL/Tools/function_package/scnp_solve.ML
+ Author: Armin Heller, TU Muenchen
+ Author: Alexander Krauss, TU Muenchen
+
+Generate certificates for SCNP using a SAT solver
+*)
+
+
+signature SCNP_SOLVE =
+sig
+
+ datatype edge = GTR | GEQ
+ datatype graph = G of int * int * (int * edge * int) list
+ datatype graph_problem = GP of int list * graph list
+
+ datatype label = MIN | MAX | MS
+
+ type certificate =
+ label (* which order *)
+ * (int * int) list list (* (multi)sets *)
+ * int list (* strictly ordered calls *)
+ * (int -> bool -> int -> (int * int) option) (* covering function *)
+
+ val generate_certificate : bool -> label list -> graph_problem -> certificate option
+
+ val solver : string ref
+end
+
+structure ScnpSolve : SCNP_SOLVE =
+struct
+
+(** Graph problems **)
+
+datatype edge = GTR | GEQ ;
+datatype graph = G of int * int * (int * edge * int) list ;
+datatype graph_problem = GP of int list * graph list ;
+
+datatype label = MIN | MAX | MS ;
+type certificate =
+ label
+ * (int * int) list list
+ * int list
+ * (int -> bool -> int -> (int * int) option)
+
+fun graph_at (GP (_, gs), i) = nth gs i ;
+fun num_prog_pts (GP (arities, _)) = length arities ;
+fun num_graphs (GP (_, gs)) = length gs ;
+fun arity (GP (arities, gl)) i = nth arities i ;
+fun ndigits (GP (arities, _)) = IntInf.log2 (foldl (op +) 0 arities) + 1
+
+
+(** Propositional formulas **)
+
+val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
+val BoolVar = PropLogic.BoolVar
+fun Implies (p, q) = Or (Not p, q)
+fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
+val all = PropLogic.all
+
+(* finite indexed quantifiers:
+
+iforall n f <==> /\
+ / \ f i
+ 0<=i<n
+ *)
+fun iforall n f = all (map f (0 upto n - 1))
+fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
+fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
+
+fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
+fun exactly_one n f = iexists n (the_one f n)
+
+(* SAT solving *)
+val solver = ref "auto";
+fun sat_solver x =
+ FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
+
+(* "Virtual constructors" for various propositional variables *)
+fun var_constrs (gp as GP (arities, gl)) =
+ let
+ val n = Int.max (num_graphs gp, num_prog_pts gp)
+ val k = foldl Int.max 1 arities
+
+ (* Injective, provided a < 8, x < n, and i < k. *)
+ fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
+
+ fun ES (g, i, j) = BoolVar (prod 0 g i j)
+ fun EW (g, i, j) = BoolVar (prod 1 g i j)
+ fun WEAK g = BoolVar (prod 2 g 0 0)
+ fun STRICT g = BoolVar (prod 3 g 0 0)
+ fun P (p, i) = BoolVar (prod 4 p i 0)
+ fun GAM (g, i, j)= BoolVar (prod 5 g i j)
+ fun EPS (g, i) = BoolVar (prod 6 g i 0)
+ fun TAG (p, i) b = BoolVar (prod 7 p i b)
+ in
+ (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
+ end
+
+
+fun graph_info gp g =
+ let
+ val G (p, q, edgs) = graph_at (gp, g)
+ in
+ (g, p, q, arity gp p, arity gp q, edgs)
+ end
+
+
+(* Order-independent part of encoding *)
+
+fun encode_graphs bits gp =
+ let
+ val ng = num_graphs gp
+ val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
+
+ fun encode_constraint_strict 0 (x, y) = PropLogic.False
+ | encode_constraint_strict k (x, y) =
+ Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
+ And (Equiv (TAG x (k - 1), TAG y (k - 1)),
+ encode_constraint_strict (k - 1) (x, y)))
+
+ fun encode_constraint_weak k (x, y) =
+ Or (encode_constraint_strict k (x, y),
+ iforall k (fn i => Equiv (TAG x i, TAG y i)))
+
+ fun encode_graph (g, p, q, n, m, edges) =
+ let
+ fun encode_edge i j =
+ if exists (fn x => x = (i, GTR, j)) edges then
+ And (ES (g, i, j), EW (g, i, j))
+ else if not (exists (fn x => x = (i, GEQ, j)) edges) then
+ And (Not (ES (g, i, j)), Not (EW (g, i, j)))
+ else
+ And (
+ Equiv (ES (g, i, j),
+ encode_constraint_strict bits ((p, i), (q, j))),
+ Equiv (EW (g, i, j),
+ encode_constraint_weak bits ((p, i), (q, j))))
+ in
+ iforall2 n m encode_edge
+ end
+ in
+ iforall ng (encode_graph o graph_info gp)
+ end
+
+
+(* Order-specific part of encoding *)
+
+fun encode bits gp mu =
+ let
+ val ng = num_graphs gp
+ val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
+
+ fun encode_graph MAX (g, p, q, n, m, _) =
+ all [
+ Equiv (WEAK g,
+ iforall m (fn j =>
+ Implies (P (q, j),
+ iexists n (fn i =>
+ And (P (p, i), EW (g, i, j)))))),
+ Equiv (STRICT g,
+ iforall m (fn j =>
+ Implies (P (q, j),
+ iexists n (fn i =>
+ And (P (p, i), ES (g, i, j)))))),
+ iexists n (fn i => P (p, i))
+ ]
+ | encode_graph MIN (g, p, q, n, m, _) =
+ all [
+ Equiv (WEAK g,
+ iforall n (fn i =>
+ Implies (P (p, i),
+ iexists m (fn j =>
+ And (P (q, j), EW (g, i, j)))))),
+ Equiv (STRICT g,
+ iforall n (fn i =>
+ Implies (P (p, i),
+ iexists m (fn j =>
+ And (P (q, j), ES (g, i, j)))))),
+ iexists m (fn j => P (q, j))
+ ]
+ | encode_graph MS (g, p, q, n, m, _) =
+ all [
+ Equiv (WEAK g,
+ iforall m (fn j =>
+ Implies (P (q, j),
+ iexists n (fn i => GAM (g, i, j))))),
+ Equiv (STRICT g,
+ iexists n (fn i =>
+ And (P (p, i), Not (EPS (g, i))))),
+ iforall2 n m (fn i => fn j =>
+ Implies (GAM (g, i, j),
+ all [
+ P (p, i),
+ P (q, j),
+ EW (g, i, j),
+ Equiv (Not (EPS (g, i)), ES (g, i, j))])),
+ iforall n (fn i =>
+ Implies (And (P (p, i), EPS (g, i)),
+ exactly_one m (fn j => GAM (g, i, j))))
+ ]
+ in
+ all [
+ encode_graphs bits gp,
+ iforall ng (encode_graph mu o graph_info gp),
+ iforall ng (fn x => WEAK x),
+ iexists ng (fn x => STRICT x)
+ ]
+ end
+
+
+(*Generieren des level-mapping und diverser output*)
+fun mk_certificate bits label gp f =
+ let
+ val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
+ fun assign (PropLogic.BoolVar v) = the_default false (f v)
+ fun assignTag i j =
+ (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
+ (bits - 1 downto 0) 0)
+
+ val level_mapping =
+ let fun prog_pt_mapping p =
+ map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
+ (0 upto (arity gp p) - 1)
+ in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
+
+ val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
+
+ fun covering_pair g bStrict j =
+ let
+ val (_, p, q, n, m, _) = graph_info gp g
+
+ fun cover MAX j = find_index (fn i => assign (P (p, i)) andalso assign (EW (g, i, j))) (0 upto n - 1)
+ | cover MS k = find_index (fn i => assign (GAM (g, i, k))) (0 upto n - 1)
+ | cover MIN i = find_index (fn j => assign (P (q, j)) andalso assign (EW (g, i, j))) (0 upto m - 1)
+ fun cover_strict MAX j = find_index (fn i => assign (P (p, i)) andalso assign (ES (g, i, j))) (0 upto n - 1)
+ | cover_strict MS k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i) ))) (0 upto n - 1)
+ | cover_strict MIN i = find_index (fn j => assign (P (q, j)) andalso assign (ES (g, i, j))) (0 upto m - 1)
+ val i = if bStrict then cover_strict label j else cover label j
+ in
+ find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
+ end
+ in
+ (label, level_mapping, strict_list, covering_pair)
+ end
+
+(*interface for the proof reconstruction*)
+fun generate_certificate use_tags labels gp =
+ let
+ val bits = if use_tags then ndigits gp else 0
+ in
+ get_first
+ (fn l => case sat_solver (encode bits gp l) of
+ SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
+ | _ => NONE)
+ labels
+ end
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/termination.ML Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,324 @@
+(* Title: HOL/Tools/function_package/termination_data.ML
+ Author: Alexander Krauss, TU Muenchen
+
+Context data for termination proofs
+*)
+
+
+signature TERMINATION =
+sig
+
+ type data
+ datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
+
+ val mk_sumcases : data -> typ -> term list -> term
+
+ val note_measure : int -> term -> data -> data
+ val note_chain : term -> term -> thm option -> data -> data
+ val note_descent : term -> term -> term -> cell -> data -> data
+
+ val get_num_points : data -> int
+ val get_types : data -> int -> typ
+ val get_measures : data -> int -> term list
+
+ (* read from cache *)
+ val get_chain : data -> term -> term -> thm option option
+ val get_descent : data -> term -> term -> term -> cell option
+
+ (* writes *)
+ val derive_descent : theory -> tactic -> term -> term -> term -> data -> data
+ val derive_descents : theory -> tactic -> term -> data -> data
+
+ val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term)
+
+ val CALLS : (term list * int -> tactic) -> int -> tactic
+
+ (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
+ type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+
+ val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
+
+ val REPEAT : ttac -> ttac
+
+ val wf_union_tac : tactic
+end
+
+
+
+structure Termination : TERMINATION =
+struct
+
+open FundefLib
+
+val term2_ord = prod_ord Term.fast_term_ord Term.fast_term_ord
+structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
+structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord Term.fast_term_ord term2_ord);
+
+(** Analyzing binary trees **)
+
+(* Skeleton of a tree structure *)
+
+datatype skel =
+ SLeaf of int (* index *)
+| SBranch of (skel * skel)
+
+
+(* abstract make and dest functions *)
+fun mk_tree leaf branch =
+ let fun mk (SLeaf i) = leaf i
+ | mk (SBranch (s, t)) = branch (mk s, mk t)
+ in mk end
+
+
+fun dest_tree split =
+ let fun dest (SLeaf i) x = [(i, x)]
+ | dest (SBranch (s, t)) x =
+ let val (l, r) = split x
+ in dest s l @ dest t r end
+ in dest end
+
+
+(* concrete versions for sum types *)
+fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
+ | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
+ | is_inj _ = false
+
+fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
+ | dest_inl _ = NONE
+
+fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
+ | dest_inr _ = NONE
+
+
+fun mk_skel ps =
+ let
+ fun skel i ps =
+ if forall is_inj ps andalso not (null ps)
+ then let
+ val (j, s) = skel i (map_filter dest_inl ps)
+ val (k, t) = skel j (map_filter dest_inr ps)
+ in (k, SBranch (s, t)) end
+ else (i + 1, SLeaf i)
+ in
+ snd (skel 0 ps)
+ end
+
+(* compute list of types for nodes *)
+fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
+
+(* find index and raw term *)
+fun dest_inj (SLeaf i) trm = (i, trm)
+ | dest_inj (SBranch (s, t)) trm =
+ case dest_inl trm of
+ SOME trm' => dest_inj s trm'
+ | _ => dest_inj t (the (dest_inr trm))
+
+
+
+(** Matrix cell datatype **)
+
+datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+
+
+type data =
+ skel (* structure of the sum type encoding "program points" *)
+ * (int -> typ) (* types of program points *)
+ * (term list Inttab.table) (* measures for program points *)
+ * (thm option Term2tab.table) (* which calls form chains? *)
+ * (cell Term3tab.table) (* local descents *)
+
+
+fun map_measures f (p, T, M, C, D) = (p, T, f M, C, D)
+fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D)
+fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D)
+
+fun note_measure p m = map_measures (Inttab.insert_list (op aconv) (p, m))
+fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
+fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
+
+(* Build case expression *)
+fun mk_sumcases (sk, _, _, _, _) T fs =
+ mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
+ (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
+ sk
+ |> fst
+
+fun mk_sum_skel rel =
+ let
+ val cs = FundefLib.dest_binop_list @{const_name "op Un"} rel
+ fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
+ let
+ val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+ = Term.strip_qnt_body "Ex" c
+ in cons r o cons l end
+ in
+ mk_skel (fold collect_pats cs [])
+ end
+
+fun create ctxt T rel =
+ let
+ val sk = mk_sum_skel rel
+ val Ts = node_types sk T
+ val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
+ in
+ (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
+ end
+
+fun get_num_points (sk, _, _, _, _) =
+ let
+ fun num (SLeaf i) = i + 1
+ | num (SBranch (s, t)) = num t
+ in num sk end
+
+fun get_types (_, T, _, _, _) = T
+fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
+
+fun get_chain (_, _, _, C, _) c1 c2 =
+ Term2tab.lookup C (c1, c2)
+
+fun get_descent (_, _, _, _, D) c m1 m2 =
+ Term3tab.lookup D (c, (m1, m2))
+
+fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
+ let
+ val n = get_num_points D
+ val (sk, _, _, _, _) = D
+ val vs = Term.strip_qnt_vars "Ex" c
+
+ (* FIXME: throw error "dest_call" for malformed terms *)
+ val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+ = Term.strip_qnt_body "Ex" c
+ val (p, l') = dest_inj sk l
+ val (q, r') = dest_inj sk r
+ in
+ (vs, p, l', q, r', Gam)
+ end
+ | dest_call D t = error "dest_call"
+
+
+fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
+ case get_descent D c m1 m2 of
+ SOME _ => D
+ | NONE => let
+ fun cgoal rel =
+ Term.list_all (vs,
+ Logic.mk_implies (HOLogic.mk_Trueprop Gam,
+ HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
+ $ (m2 $ r') $ (m1 $ l'))))
+ |> cterm_of thy
+ in
+ note_descent c m1 m2
+ (case try_proof (cgoal @{const_name HOL.less}) tac of
+ Solved thm => Less thm
+ | Stuck thm =>
+ (case try_proof (cgoal @{const_name HOL.less_eq}) tac of
+ Solved thm2 => LessEq (thm2, thm)
+ | Stuck thm2 =>
+ if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
+ then False thm2 else None (thm2, thm)
+ | _ => raise Match) (* FIXME *)
+ | _ => raise Match) D
+ end
+
+fun derive_descent thy tac c m1 m2 D =
+ derive_desc_aux thy tac c (dest_call D c) m1 m2 D
+
+(* all descents in one go *)
+fun derive_descents thy tac c D =
+ let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
+ in fold_product (derive_desc_aux thy tac c cdesc)
+ (get_measures D p) (get_measures D q) D
+ end
+
+fun CALLS tac i st =
+ if Thm.no_prems st then all_tac st
+ else case Thm.term_of (Thm.cprem_of st i) of
+ (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name "op Un"} rel, i) st
+ |_ => no_tac st
+
+type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+
+fun TERMINATION ctxt tac =
+ SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
+ let
+ val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
+ in
+ tac (create ctxt T rel) i
+ end)
+
+
+(* A tactic to convert open to closed termination goals *)
+local
+fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
+ let
+ val (vars, prop) = FundefLib.dest_all_all t
+ val (prems, concl) = Logic.strip_horn prop
+ val (lhs, rhs) = concl
+ |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_mem |> fst
+ |> HOLogic.dest_prod
+ in
+ (vars, prems, lhs, rhs)
+ end
+
+fun mk_pair_compr (T, qs, l, r, conds) =
+ let
+ val pT = HOLogic.mk_prodT (T, T)
+ val n = length qs
+ val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
+ val conds' = if null conds then [HOLogic.true_const] else conds
+ in
+ HOLogic.Collect_const pT $
+ Abs ("uu_", pT,
+ (foldr1 HOLogic.mk_conj (peq :: conds')
+ |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
+ end
+
+in
+
+fun wf_union_tac st =
+ let
+ val thy = theory_of_thm st
+ val cert = cterm_of (theory_of_thm st)
+ val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
+
+ fun mk_compr ineq =
+ let
+ val (vars, prems, lhs, rhs) = dest_term ineq
+ in
+ mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
+ end
+
+ val relation =
+ if null ineqs then
+ Const (@{const_name "{}"}, fastype_of rel)
+ else
+ foldr1 (HOLogic.mk_binop @{const_name "op Un"}) (map mk_compr ineqs)
+
+ fun solve_membership_tac i =
+ (EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *)
+ THEN' (fn j => TRY (rtac @{thm UnI1} j))
+ THEN' (rtac @{thm CollectI}) (* unfold comprehension *)
+ THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *)
+ THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
+ ORELSE' ((rtac @{thm conjI})
+ THEN' (rtac @{thm refl})
+ THEN' (CLASET' blast_tac))) (* Solve rest of context... not very elegant *)
+ ) i
+ in
+ ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
+ THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
+ end
+
+
+end
+
+
+(* continuation passing repeat combinator *)
+fun REPEAT ttac cont err_cont =
+ ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
+
+
+
+
+end
--- a/src/HOL/Wellfounded.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/Wellfounded.thy Fri Dec 19 11:49:08 2008 +0000
@@ -842,6 +842,11 @@
qed
qed
+lemma max_ext_additive:
+ "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
+ (A \<union> C, B \<union> D) \<in> max_ext R"
+by (force elim!: max_ext.cases)
+
definition
min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
--- a/src/HOL/ex/ExecutableContent.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/ex/ExecutableContent.thy Fri Dec 19 11:49:08 2008 +0000
@@ -24,4 +24,11 @@
"~~/src/HOL/ex/Records"
begin
+text {* However, some aren't executable *}
+
+declare pair_leq_def[code del]
+declare max_weak_def[code del]
+declare min_weak_def[code del]
+declare ms_weak_def[code del]
+
end
--- a/src/HOL/ex/Quickcheck.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOL/ex/Quickcheck.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,11 +1,9 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
+(* Author: Florian Haftmann, TU Muenchen *)
header {* A simple counterexample generator *}
theory Quickcheck
-imports Random Code_Eval
+imports Random Code_Eval Map
begin
subsection {* The @{text random} class *}
@@ -25,166 +23,6 @@
end
-text {* Datatypes *}
-
-definition
- collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
- "collapse f = (do g \<leftarrow> f; g done)"
-
-ML {*
-structure StateMonad =
-struct
-
-fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-fun liftT' sT = sT --> sT;
-
-fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
-
-fun scomp T1 T2 sT f g = Const (@{const_name scomp},
- liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-
-end;
-*}
-
-lemma random'_if:
- fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
- assumes "random' 0 j = (\<lambda>s. undefined)"
- and "\<And>i. random' (Suc_index 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)
-
-setup {*
-let
- exception REC of string;
- fun mk_collapse thy ty = Sign.mk_const thy
- (@{const_name collapse}, [@{typ seed}, ty]);
- fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
- fun mk_split thy ty ty' = Sign.mk_const thy
- (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
- fun mk_scomp_split thy ty ty' t t' =
- StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
- (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
- fun mk_cons thy this_ty (c, args) =
- let
- val tys = map (fst o fst) args;
- val c_ty = tys ---> this_ty;
- val c = Const (c, tys ---> this_ty);
- val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
- val c_indices = map (curry ( op + ) 1) t_indices;
- val c_t = list_comb (c, map Bound c_indices);
- val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep
- (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
- |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
- val return = StateMonad.return (term_ty this_ty) @{typ seed}
- (HOLogic.mk_prod (c_t, t_t));
- val t = fold_rev (fn ((ty, _), random) =>
- mk_scomp_split thy ty this_ty random)
- args return;
- val is_rec = exists (snd o fst) args;
- in (is_rec, t) end;
- fun mk_conss thy ty [] = NONE
- | mk_conss thy ty [(_, t)] = SOME t
- | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
- (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
- HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts)));
- fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) =
- let
- val SOME t_atom = mk_conss thy ty ts_atom;
- in case mk_conss thy ty ts_rec
- of SOME t_rec => mk_collapse thy (term_ty ty) $
- (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
- @{term "i\<Colon>index"} $ t_rec $ t_atom)
- | NONE => t_atom
- end;
- fun mk_random_eqs thy vs tycos =
- let
- val this_ty = Type (hd tycos, map TFree vs);
- val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
- val random_name = NameSpace.base @{const_name random};
- 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');
- fun atom ty = ((ty, false), random ty $ @{term "j\<Colon>index"});
- fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"});
- fun rtyp tyco tys = raise REC
- ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
- val rhss = DatatypePackage.construction_interpretation thy
- { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
- |> (map o apsnd o map) (mk_cons thy this_ty)
- |> (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 seed},
- Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
- (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
- ]))) rhss;
- in eqss end;
- fun random_inst [tyco] thy =
- let
- val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
- val vs = (map o apsnd)
- (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
- val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;
- 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 "i\<Colon>index"} $ @{term "i\<Colon>index"})
- val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
- (fn thm => Context.mapping (Code.del_eqn thm) I));
- fun add_code simps lthy =
- let
- val thy = ProofContext.theory_of lthy;
- val thm = @{thm random'_if}
- |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')]
- |> (fn thm => thm OF simps)
- |> singleton (ProofContext.export lthy (ProofContext.init thy));
- val c = (fst o dest_Const o fst o strip_comb o fst
- o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
- in
- lthy
- |> LocalTheory.theory (Code.del_eqns c
- #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
- #-> Code.add_eqn)
- end;
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
- |> PrimrecPackage.add_primrec
- [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
- (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
- |-> add_code
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit_global
- end
- | random_inst tycos thy = raise REC
- ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
- fun add_random_inst tycos thy = random_inst tycos thy
- handle REC msg => (warning msg; thy);
-in DatatypePackage.interpretation add_random_inst end
-*}
-
-text {* Type @{typ int} *}
-
-instantiation int :: random
-begin
-
-definition
- "random n = (do
- (b, _) \<leftarrow> random n;
- (m, t) \<leftarrow> random n;
- return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
- else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
- (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
- done)"
-
-instance ..
-
-end
-
text {* Type @{typ "'a \<Rightarrow> 'b"} *}
ML {*
@@ -240,6 +78,170 @@
code_reserved SML Random_Engine
+text {* Datatypes *}
+
+definition
+ collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+ "collapse f = (do g \<leftarrow> f; g done)"
+
+ML {*
+structure StateMonad =
+struct
+
+fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+fun liftT' sT = sT --> sT;
+
+fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
+
+fun scomp T1 T2 sT f g = Const (@{const_name scomp},
+ liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+
+end;
+*}
+
+lemma random'_if:
+ fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
+ assumes "random' 0 j = (\<lambda>s. undefined)"
+ and "\<And>i. random' (Suc_index 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)
+
+setup {*
+let
+ exception REC of string;
+ exception TYP of string;
+ fun mk_collapse thy ty = Sign.mk_const thy
+ (@{const_name collapse}, [@{typ seed}, ty]);
+ fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
+ fun mk_split thy ty ty' = Sign.mk_const thy
+ (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
+ fun mk_scomp_split thy ty ty' t t' =
+ StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
+ (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
+ fun mk_cons thy this_ty (c, args) =
+ let
+ val tys = map (fst o fst) args;
+ val c_ty = tys ---> this_ty;
+ val c = Const (c, tys ---> this_ty);
+ val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
+ val c_indices = map (curry ( op + ) 1) t_indices;
+ val c_t = list_comb (c, map Bound c_indices);
+ val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep
+ (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
+ |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
+ val return = StateMonad.return (term_ty this_ty) @{typ seed}
+ (HOLogic.mk_prod (c_t, t_t));
+ val t = fold_rev (fn ((ty, _), random) =>
+ mk_scomp_split thy ty this_ty random)
+ args return;
+ val is_rec = exists (snd o fst) args;
+ in (is_rec, t) end;
+ fun mk_conss thy ty [] = NONE
+ | mk_conss thy ty [(_, t)] = SOME t
+ | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
+ (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
+ HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts)));
+ fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) =
+ let
+ val SOME t_atom = mk_conss thy ty ts_atom;
+ in case mk_conss thy ty ts_rec
+ of SOME t_rec => mk_collapse thy (term_ty ty) $
+ (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
+ @{term "i\<Colon>index"} $ t_rec $ t_atom)
+ | NONE => t_atom
+ end;
+ fun mk_random_eqs thy vs tycos =
+ let
+ val this_ty = Type (hd tycos, map TFree vs);
+ val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
+ val random_name = NameSpace.base @{const_name random};
+ 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');
+ fun atom ty = if Sign.of_sort thy (ty, @{sort random})
+ then ((ty, false), random ty $ @{term "j\<Colon>index"})
+ 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 rtyp tyco tys = raise REC
+ ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
+ val rhss = DatatypePackage.construction_interpretation thy
+ { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
+ |> (map o apsnd o map) (mk_cons thy this_ty)
+ |> (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 seed},
+ Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
+ (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
+ ]))) rhss;
+ in eqss end;
+ fun random_inst [tyco] thy =
+ let
+ val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
+ val vs = (map o apsnd)
+ (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 "i\<Colon>index"} $ @{term "i\<Colon>index"})
+ val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
+ (fn thm => Context.mapping (Code.del_eqn thm) I));
+ fun add_code simps lthy =
+ let
+ val thy = ProofContext.theory_of lthy;
+ val thm = @{thm random'_if}
+ |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')]
+ |> (fn thm => thm OF simps)
+ |> singleton (ProofContext.export lthy (ProofContext.init thy));
+ val c = (fst o dest_Const o fst o strip_comb o fst
+ o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
+ in
+ lthy
+ |> LocalTheory.theory (Code.del_eqns c
+ #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
+ #-> Code.add_eqn)
+ end;
+ in
+ thy
+ |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+ |> PrimrecPackage.add_primrec
+ [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
+ (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
+ |-> add_code
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
+ |> snd
+ |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+ |> LocalTheory.exit_global
+ end
+ | random_inst tycos thy = raise REC
+ ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
+ fun add_random_inst tycos thy = random_inst tycos thy
+ handle REC msg => (warning msg; thy)
+ | TYP msg => (warning msg; thy)
+in DatatypePackage.interpretation add_random_inst end
+*}
+
+text {* Type @{typ int} *}
+
+instantiation int :: random
+begin
+
+definition
+ "random n = (do
+ (b, _) \<leftarrow> random n;
+ (m, t) \<leftarrow> random n;
+ return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
+ else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
+ (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
+ done)"
+
+instance ..
+
+end
+
subsection {* Quickcheck generator *}
--- a/src/HOLCF/Adm.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Adm.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Adm.thy
- ID: $Id$
Author: Franz Regensburger and Brian Huffman
*)
--- a/src/HOLCF/Algebraic.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Algebraic.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Algebraic.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Bifinite.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Bifinite.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Bifinite.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Cfun.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Cfun.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Cfun.thy
- ID: $Id$
Author: Franz Regensburger
Definition of the type -> of continuous functions.
--- a/src/HOLCF/CompactBasis.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/CompactBasis.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/CompactBasis.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Completion.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Completion.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Completion.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Cont.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Cont.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Cont.thy
- ID: $Id$
Author: Franz Regensburger
-
-Results about continuity and monotonicity.
*)
header {* Continuity and monotonicity *}
--- a/src/HOLCF/ConvexPD.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/ConvexPD.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/ConvexPD.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Cprod.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Cprod.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Cprod.thy
- ID: $Id$
Author: Franz Regensburger
-
-Partial ordering for cartesian product of HOL products.
*)
header {* The cpo of cartesian products *}
--- a/src/HOLCF/Deflation.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Deflation.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Deflation.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Discrete.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Discrete.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Discrete.thy
- ID: $Id$
Author: Tobias Nipkow
-
-Discrete CPOs.
*)
header {* Discrete cpo types *}
--- a/src/HOLCF/Domain.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Domain.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Domain.thy
- ID: $Id$
Author: Brian Huffman
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Dsum.thy Fri Dec 19 11:49:08 2008 +0000
@@ -0,0 +1,251 @@
+(* Title: HOLCF/Dsum.thy
+ Author: Brian Huffman
+*)
+
+header {* The cpo of disjoint sums *}
+
+theory Dsum
+imports Bifinite
+begin
+
+subsection {* Ordering on type @{typ "'a + 'b"} *}
+
+instantiation "+" :: (sq_ord, sq_ord) sq_ord
+begin
+
+definition
+ less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
+ Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
+ Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
+
+instance ..
+end
+
+lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+unfolding less_sum_def by simp
+
+lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+unfolding less_sum_def by simp
+
+lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
+unfolding less_sum_def by simp
+
+lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
+unfolding less_sum_def by simp
+
+lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
+by simp
+
+lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
+by simp
+
+lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+by (cases x, simp_all)
+
+lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+by (cases x, simp_all)
+
+lemmas sum_less_elims = Inl_lessE Inr_lessE
+
+lemma sum_less_cases:
+ "\<lbrakk>x \<sqsubseteq> y;
+ \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
+ \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
+ \<Longrightarrow> R"
+by (cases x, safe elim!: sum_less_elims, auto)
+
+subsection {* Sum type is a complete partial order *}
+
+instance "+" :: (po, po) po
+proof
+ fix x :: "'a + 'b"
+ show "x \<sqsubseteq> x"
+ by (induct x, simp_all)
+next
+ fix x y :: "'a + 'b"
+ assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
+ by (induct x, auto elim!: sum_less_elims intro: antisym_less)
+next
+ fix x y z :: "'a + 'b"
+ assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+ by (induct x, auto elim!: sum_less_elims intro: trans_less)
+qed
+
+lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
+by (rule monofunI, erule sum_less_cases, simp_all)
+
+lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
+by (rule monofunI, erule sum_less_cases, simp_all)
+
+lemma sum_chain_cases:
+ assumes Y: "chain Y"
+ assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
+ assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
+ shows "R"
+ apply (cases "Y 0")
+ apply (rule A)
+ apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
+ apply (rule ext)
+ apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (erule Inl_lessE, simp)
+ apply (rule B)
+ apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
+ apply (rule ext)
+ apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (erule Inr_lessE, simp)
+done
+
+lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
+ apply (rule is_lubI)
+ apply (rule ub_rangeI)
+ apply (simp add: is_ub_lub)
+ apply (frule ub_rangeD [where i=arbitrary])
+ apply (erule Inl_lessE, simp)
+ apply (erule is_lub_lub)
+ apply (rule ub_rangeI)
+ apply (drule ub_rangeD, simp)
+done
+
+lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
+ apply (rule is_lubI)
+ apply (rule ub_rangeI)
+ apply (simp add: is_ub_lub)
+ apply (frule ub_rangeD [where i=arbitrary])
+ apply (erule Inr_lessE, simp)
+ apply (erule is_lub_lub)
+ apply (rule ub_rangeI)
+ apply (drule ub_rangeD, simp)
+done
+
+instance "+" :: (cpo, cpo) cpo
+ apply intro_classes
+ apply (erule sum_chain_cases, safe)
+ apply (rule exI)
+ apply (rule is_lub_Inl)
+ apply (erule cpo_lubI)
+ apply (rule exI)
+ apply (rule is_lub_Inr)
+ apply (erule cpo_lubI)
+done
+
+subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
+
+lemma cont2cont_Inl [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inl (f x))"
+by (fast intro: contI is_lub_Inl elim: contE)
+
+lemma cont2cont_Inr [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inr (f x))"
+by (fast intro: contI is_lub_Inr elim: contE)
+
+lemma cont_Inl: "cont Inl"
+by (rule cont2cont_Inl [OF cont_id])
+
+lemma cont_Inr: "cont Inr"
+by (rule cont2cont_Inr [OF cont_id])
+
+lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
+lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
+
+lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
+lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
+
+lemma cont_sum_case1:
+ assumes f: "\<And>a. cont (\<lambda>x. f x a)"
+ assumes g: "\<And>b. cont (\<lambda>x. g x b)"
+ shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+by (induct y, simp add: f, simp add: g)
+
+lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
+apply (rule contI)
+apply (erule sum_chain_cases)
+apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
+apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
+done
+
+lemma cont2cont_sum_case [simp]:
+ assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
+ assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
+ assumes h: "cont (\<lambda>x. h x)"
+ shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+apply (rule cont2cont_app2 [OF cont2cont_lambda _ h])
+apply (rule cont_sum_case1 [OF f1 g1])
+apply (rule cont_sum_case2 [OF f2 g2])
+done
+
+subsection {* Compactness and chain-finiteness *}
+
+lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
+apply (rule compactI2)
+apply (erule sum_chain_cases, safe)
+apply (simp add: lub_Inl)
+apply (erule (2) compactD2)
+apply (simp add: lub_Inr)
+done
+
+lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
+apply (rule compactI2)
+apply (erule sum_chain_cases, safe)
+apply (simp add: lub_Inl)
+apply (simp add: lub_Inr)
+apply (erule (2) compactD2)
+done
+
+lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
+unfolding compact_def
+by (drule adm_subst [OF cont_Inl], simp)
+
+lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
+unfolding compact_def
+by (drule adm_subst [OF cont_Inr], simp)
+
+lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
+by (safe elim!: compact_Inl compact_Inl_rev)
+
+lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
+by (safe elim!: compact_Inr compact_Inr_rev)
+
+instance "+" :: (chfin, chfin) chfin
+apply intro_classes
+apply (erule compact_imp_max_in_chain)
+apply (case_tac "\<Squnion>i. Y i", simp_all)
+done
+
+instance "+" :: (finite_po, finite_po) finite_po ..
+
+instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
+by intro_classes (simp add: less_sum_def split: sum.split)
+
+subsection {* Sum type is a bifinite domain *}
+
+instantiation "+" :: (profinite, profinite) profinite
+begin
+
+definition
+ approx_sum_def: "approx =
+ (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))"
+
+lemma approx_Inl [simp]: "approx n\<cdot>(Inl x) = Inl (approx n\<cdot>x)"
+ unfolding approx_sum_def by simp
+
+lemma approx_Inr [simp]: "approx n\<cdot>(Inr x) = Inr (approx n\<cdot>x)"
+ unfolding approx_sum_def by simp
+
+instance proof
+ fix i :: nat and x :: "'a + 'b"
+ show "chain (approx :: nat \<Rightarrow> 'a + 'b \<rightarrow> 'a + 'b)"
+ unfolding approx_sum_def
+ by (rule ch2ch_LAM, case_tac x, simp_all)
+ show "(\<Squnion>i. approx i\<cdot>x) = x"
+ by (induct x, simp_all add: lub_Inl lub_Inr)
+ show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+ by (induct x, simp_all)
+ have "{x::'a + 'b. approx i\<cdot>x = x} \<subseteq>
+ {x::'a. approx i\<cdot>x = x} <+> {x::'b. approx i\<cdot>x = x}"
+ by (rule subsetI, case_tac x, simp_all add: InlI InrI)
+ thus "finite {x::'a + 'b. approx i\<cdot>x = x}"
+ by (rule finite_subset,
+ intro finite_Plus finite_fixes_approx)
+qed
+
+end
+
+end
--- a/src/HOLCF/Ffun.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Ffun.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,10 +1,5 @@
(* Title: HOLCF/FunCpo.thy
- ID: $Id$
Author: Franz Regensburger
-
-Definition of the partial ordering for the type of all functions => (fun)
-
-Class instance of => (fun) for class pcpo.
*)
header {* Class instances for the full function space *}
--- a/src/HOLCF/Fix.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Fix.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Fix.thy
- ID: $Id$
Author: Franz Regensburger
-
-Definitions for fixed point operator and admissibility.
*)
header {* Fixed point operator and admissibility *}
--- a/src/HOLCF/Fixrec.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Fixrec.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Fixrec.thy
- ID: $Id$
Author: Amber Telfer and Brian Huffman
*)
--- a/src/HOLCF/HOLCF.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/HOLCF.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,12 +1,12 @@
(* Title: HOLCF/HOLCF.thy
- ID: $Id$
Author: Franz Regensburger
HOLCF -- a semantic extension of HOL by the LCF logic.
*)
theory HOLCF
-imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Algebraic Universal Main
+imports
+ Domain ConvexPD Algebraic Universal Dsum Main
uses
"holcf_logic.ML"
"Tools/cont_consts.ML"
--- a/src/HOLCF/IsaMakefile Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/IsaMakefile Fri Dec 19 11:49:08 2008 +0000
@@ -41,6 +41,7 @@
Discrete.thy \
Deflation.thy \
Domain.thy \
+ Dsum.thy \
Eventual.thy \
Ffun.thy \
Fixrec.thy \
--- a/src/HOLCF/Lift.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Lift.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Lift.thy
- ID: $Id$
Author: Olaf Mueller
*)
--- a/src/HOLCF/LowerPD.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/LowerPD.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/LowerPD.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/One.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/One.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/One.thy
- ID: $Id$
Author: Oscar Slotosch
-
-The unit domain.
*)
header {* The unit domain *}
--- a/src/HOLCF/Pcpo.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Pcpo.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Pcpo.thy
- ID: $Id$
Author: Franz Regensburger
*)
--- a/src/HOLCF/Pcpodef.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Pcpodef.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Pcpodef.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Porder.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Porder.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Porder.thy
- ID: $Id$
Author: Franz Regensburger and Brian Huffman
*)
--- a/src/HOLCF/Sprod.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Sprod.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Sprod.thy
- ID: $Id$
Author: Franz Regensburger and Brian Huffman
-
-Strict product with typedef.
*)
header {* The type of strict products *}
--- a/src/HOLCF/Ssum.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Ssum.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Ssum.thy
- ID: $Id$
Author: Franz Regensburger and Brian Huffman
-
-Strict sum with typedef.
*)
header {* The type of strict sums *}
--- a/src/HOLCF/Tr.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Tr.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Tr.thy
- ID: $Id$
Author: Franz Regensburger
-
-Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
*)
header {* The type of lifted booleans *}
--- a/src/HOLCF/Universal.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Universal.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/Universal.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/Up.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/Up.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,8 +1,5 @@
(* Title: HOLCF/Up.thy
- ID: $Id$
Author: Franz Regensburger and Brian Huffman
-
-Lifting.
*)
header {* The type of lifted values *}
--- a/src/HOLCF/UpperPD.thy Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/UpperPD.thy Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: HOLCF/UpperPD.thy
- ID: $Id$
Author: Brian Huffman
*)
--- a/src/HOLCF/document/root.tex Mon Dec 15 10:40:52 2008 +0000
+++ b/src/HOLCF/document/root.tex Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,5 @@
-% $Id$
+% HOLCF/document/root.tex
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
@@ -21,7 +21,7 @@
\tableofcontents
\begin{center}
- \includegraphics[scale=0.7]{session_graph}
+ \includegraphics[scale=0.5]{session_graph}
\end{center}
\newpage
--- a/src/Pure/Concurrent/ROOT.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Concurrent/ROOT.ML Fri Dec 19 11:49:08 2008 +0000
@@ -1,15 +1,12 @@
(* Title: Pure/Concurrent/ROOT.ML
- ID: $Id$
+ Author: Makarius
Concurrency within the ML runtime.
*)
-val future_scheduler = ref true;
-
use "simple_thread.ML";
use "synchronized.ML";
use "mailbox.ML";
-use "schedule.ML";
use "task_queue.ML";
use "future.ML";
use "par_list.ML";
--- a/src/Pure/Concurrent/future.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Concurrent/future.ML Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: Pure/Concurrent/future.ML
- ID: $Id$
Author: Makarius
Future values.
@@ -28,8 +27,8 @@
signature FUTURE =
sig
val enabled: unit -> bool
- type task = TaskQueue.task
- type group = TaskQueue.group
+ type task = Task_Queue.task
+ type group = Task_Queue.group
val thread_data: unit -> (string * task) option
type 'a future
val task_of: 'a future -> task
@@ -40,12 +39,11 @@
val fork: (unit -> 'a) -> 'a future
val fork_group: group -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
- val fork_background: (unit -> 'a) -> 'a future
+ val fork_pri: int -> (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
val map: ('a -> 'b) -> 'a future -> 'b future
- val focus: task list -> unit
val interrupt_task: string -> unit
val cancel: 'a future -> unit
val shutdown: unit -> unit
@@ -57,14 +55,14 @@
(** future values **)
fun enabled () =
- ! future_scheduler andalso Multithreading.enabled () andalso
+ Multithreading.enabled () andalso
not (Multithreading.self_critical ());
(* identifiers *)
-type task = TaskQueue.task;
-type group = TaskQueue.group;
+type task = Task_Queue.task;
+type group = Task_Queue.group;
local val tag = Universal.tag () : (string * task) option Universal.tag in
fun thread_data () = the_default NONE (Thread.getLocal tag);
@@ -86,8 +84,8 @@
fun is_finished x = is_some (peek x);
fun value x = Future
- {task = TaskQueue.new_task (),
- group = TaskQueue.new_group (),
+ {task = Task_Queue.new_task 0,
+ group = Task_Queue.new_group (),
result = ref (SOME (Exn.Result x))};
@@ -96,12 +94,12 @@
(* global state *)
-val queue = ref TaskQueue.empty;
+val queue = ref Task_Queue.empty;
val next = ref 0;
val workers = ref ([]: (Thread.thread * bool) list);
val scheduler = ref (NONE: Thread.thread option);
val excessive = ref 0;
-val canceled = ref ([]: TaskQueue.group list);
+val canceled = ref ([]: Task_Queue.group list);
val do_shutdown = ref false;
@@ -114,15 +112,11 @@
fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
-fun wait name = (*requires SYNCHRONIZED*)
- (Multithreading.tracing 3 (fn () => name ^ ": wait ...");
+fun wait () = (*requires SYNCHRONIZED*)
ConditionVar.wait (cond, lock);
- Multithreading.tracing 3 (fn () => name ^ ": ... continue"));
-fun wait_timeout name timeout = (*requires SYNCHRONIZED*)
- (Multithreading.tracing 3 (fn () => name ^ ": wait ...");
+fun wait_timeout timeout = (*requires SYNCHRONIZED*)
ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout));
- Multithreading.tracing 3 (fn () => name ^ ": ... continue"));
fun notify_all () = (*requires SYNCHRONIZED*)
ConditionVar.broadcast cond;
@@ -150,9 +144,9 @@
val _ = trace_active ();
val ok = setmp_thread_data (name, task) run ();
val _ = SYNCHRONIZED "execute" (fn () =>
- (change queue (TaskQueue.finish task);
+ (change queue (Task_Queue.finish task);
if ok then ()
- else if TaskQueue.cancel (! queue) group then ()
+ else if Task_Queue.cancel (! queue) group then ()
else change canceled (cons group);
notify_all ()));
in () end;
@@ -160,23 +154,23 @@
(* worker threads *)
-fun worker_wait name = (*requires SYNCHRONIZED*)
- (change_active false; wait name; change_active true);
+fun worker_wait () = (*requires SYNCHRONIZED*)
+ (change_active false; wait (); change_active true);
-fun worker_next name = (*requires SYNCHRONIZED*)
+fun worker_next () = (*requires SYNCHRONIZED*)
if ! excessive > 0 then
(dec excessive;
change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
notify_all ();
NONE)
else
- (case change_result queue TaskQueue.dequeue of
- NONE => (worker_wait name; worker_next name)
+ (case change_result queue Task_Queue.dequeue of
+ NONE => (worker_wait (); worker_next ())
| some => some);
fun worker_loop name =
- (case SYNCHRONIZED name (fn () => worker_next name) of
- NONE => Multithreading.tracing 3 (fn () => name ^ ": exit")
+ (case SYNCHRONIZED name worker_next of
+ NONE => ()
| SOME work => (execute name work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
@@ -204,27 +198,25 @@
else ();
(*canceled groups*)
- val _ = change canceled (filter_out (TaskQueue.cancel (! queue)));
+ val _ = change canceled (filter_out (Task_Queue.cancel (! queue)));
(*shutdown*)
val continue = not (! do_shutdown andalso null (! workers));
val _ = if continue then () else scheduler := NONE;
val _ = notify_all ();
- val _ = wait_timeout "scheduler" (Time.fromSeconds 3);
+ val _ = wait_timeout (Time.fromSeconds 3);
in continue end;
fun scheduler_loop () =
- (while SYNCHRONIZED "scheduler" scheduler_next do ();
- Multithreading.tracing 3 (fn () => "scheduler: exit"));
+ while SYNCHRONIZED "scheduler" scheduler_next do ();
fun scheduler_active () = (*requires SYNCHRONIZED*)
(case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
fun scheduler_check name = SYNCHRONIZED name (fn () =>
if not (scheduler_active ()) then
- (Multithreading.tracing 3 (fn () => "scheduler: fork");
- do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop))
+ (do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop))
else if ! do_shutdown then error "Scheduler shutdown in progress"
else ());
@@ -235,7 +227,7 @@
let
val _ = scheduler_check "future check";
- val group = (case opt_group of SOME group => group | NONE => TaskQueue.new_group ());
+ val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
val result = ref (NONE: 'a Exn.result option);
val run = Multithreading.with_attributes (Thread.getAttributes ())
@@ -246,18 +238,18 @@
val res_ok =
(case res of
Exn.Result _ => true
- | Exn.Exn Exn.Interrupt => (TaskQueue.invalidate_group group; true)
+ | Exn.Exn Exn.Interrupt => (Task_Queue.invalidate_group group; true)
| _ => false);
in res_ok end);
val task = SYNCHRONIZED "future" (fn () =>
- change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());
+ change_result queue (Task_Queue.enqueue group deps pri run) before notify_all ());
in Future {task = task, group = group, result = result} end;
-fun fork e = future NONE [] true e;
-fun fork_group group e = future (SOME group) [] true e;
-fun fork_deps deps e = future NONE (map task_of deps) true e;
-fun fork_background e = future NONE [] false e;
+fun fork e = future NONE [] 0 e;
+fun fork_group group e = future (SOME group) [] 0 e;
+fun fork_deps deps e = future NONE (map task_of deps) 0 e;
+fun fork_pri pri e = future NONE [] pri e;
(* join: retrieve results *)
@@ -273,7 +265,7 @@
fun join_loop _ [] = ()
| join_loop name tasks =
(case SYNCHRONIZED name (fn () =>
- change_result queue (TaskQueue.dequeue_towards tasks)) of
+ change_result queue (Task_Queue.dequeue_towards tasks)) of
NONE => ()
| SOME (work, tasks') => (execute name work; join_loop name tasks'));
val _ =
@@ -281,18 +273,18 @@
NONE =>
(*alien thread -- refrain from contending for resources*)
while exists (not o is_finished) xs
- do SYNCHRONIZED "join_thread" (fn () => wait "join_thread")
+ do SYNCHRONIZED "join_thread" (fn () => wait ())
| SOME (name, task) =>
(*proper task -- actively work towards results*)
let
val unfinished = xs |> map_filter
(fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
val _ = SYNCHRONIZED "join" (fn () =>
- (change queue (TaskQueue.depend unfinished task); notify_all ()));
+ (change queue (Task_Queue.depend unfinished task); notify_all ()));
val _ = join_loop ("join_loop: " ^ name) unfinished;
val _ =
while exists (not o is_finished) xs
- do SYNCHRONIZED "join_task" (fn () => worker_wait "join_task");
+ do SYNCHRONIZED "join_task" (fn () => worker_wait ());
in () end);
in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
@@ -300,18 +292,16 @@
fun join_result x = singleton join_results x;
fun join x = Exn.release (join_result x);
-fun map f x = fork_deps [x] (fn () => f (join x));
+fun map f x =
+ let val task = task_of x
+ in future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x)) end;
(* misc operations *)
-(*focus: collection of high-priority task*)
-fun focus tasks = SYNCHRONIZED "focus" (fn () =>
- change queue (TaskQueue.focus tasks));
-
(*interrupt: permissive signal, may get ignored*)
fun interrupt_task id = SYNCHRONIZED "interrupt"
- (fn () => TaskQueue.interrupt_external (! queue) id);
+ (fn () => Task_Queue.interrupt_external (! queue) id);
(*cancel: present and future group members will be interrupted eventually*)
fun cancel x =
@@ -324,12 +314,12 @@
if Multithreading.available then
(scheduler_check "shutdown check";
SYNCHRONIZED "shutdown" (fn () =>
- (while not (scheduler_active ()) do wait "shutdown: scheduler inactive";
- while not (TaskQueue.is_empty (! queue)) do wait "shutdown: join";
+ (while not (scheduler_active ()) do wait ();
+ while not (Task_Queue.is_empty (! queue)) do wait ();
do_shutdown := true;
notify_all ();
- while not (null (! workers)) do wait "shutdown: workers";
- while scheduler_active () do wait "shutdown: scheduler still active";
+ while not (null (! workers)) do wait ();
+ while scheduler_active () do wait ();
OS.Process.sleep (Time.fromMilliseconds 300))))
else ();
--- a/src/Pure/Concurrent/par_list.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Concurrent/par_list.ML Fri Dec 19 11:49:08 2008 +0000
@@ -30,7 +30,7 @@
fun raw_map f xs =
if Future.enabled () then
let
- val group = TaskQueue.new_group ();
+ val group = Task_Queue.new_group ();
val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
val _ = List.app (ignore o Future.join_result) futures;
in Future.join_results futures end
--- a/src/Pure/Concurrent/schedule.ML Mon Dec 15 10:40:52 2008 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* Title: Pure/Concurrent/schedule.ML
- ID: $Id$
- Author: Makarius
-
-Scheduling -- multiple threads working on a queue of tasks.
-*)
-
-signature SCHEDULE =
-sig
- datatype 'a task =
- Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
- val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
-end;
-
-structure Schedule: SCHEDULE =
-struct
-
-datatype 'a task =
- Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
-
-fun schedule n next_task = uninterruptible (fn restore_attributes => fn tasks =>
- let
- (*synchronized execution*)
- val lock = Mutex.mutex ();
- fun SYNCHRONIZED e =
- let
- val _ = Mutex.lock lock;
- val res = Exn.capture e ();
- val _ = Mutex.unlock lock;
- in Exn.release res end;
-
- (*wakeup condition*)
- val wakeup = ConditionVar.conditionVar ();
- fun wakeup_all () = ConditionVar.broadcast wakeup;
- fun wait () = ConditionVar.wait (wakeup, lock);
- fun wait_timeout () =
- ConditionVar.waitUntil (wakeup, lock, Time.+ (Time.now (), Time.fromSeconds 1));
-
- (*queue of tasks*)
- val queue = ref tasks;
- val active = ref 0;
- fun trace_active () = Multithreading.tracing 1 (fn () =>
- "SCHEDULE: " ^ string_of_int (! active) ^ " active");
- fun dequeue () =
- (case change_result queue next_task of
- Wait =>
- (dec active; trace_active ();
- wait ();
- inc active; trace_active ();
- dequeue ())
- | next => next);
-
- (*pool of running threads*)
- val status = ref ([]: exn list);
- val running = ref ([]: Thread.thread list);
- fun start f = (inc active; change running (cons (SimpleThread.fork false f)));
- fun stop () = (dec active; change running (remove Thread.equal (Thread.self ())));
-
- (*worker thread*)
- fun worker () =
- (case SYNCHRONIZED dequeue of
- Task {body, cont, fail} =>
- (case Exn.capture (restore_attributes body) () of
- Exn.Result () =>
- (SYNCHRONIZED (fn () => (change queue cont; wakeup_all ())); worker ())
- | Exn.Exn exn =>
- SYNCHRONIZED (fn () =>
- (change status (cons exn); change queue fail; stop (); wakeup_all ())))
- | Terminate => SYNCHRONIZED (fn () => (stop (); wakeup_all ())));
-
- (*main control: fork and wait*)
- fun fork 0 = ()
- | fork k = (start worker; fork (k - 1));
- val _ = SYNCHRONIZED (fn () =>
- (fork (Int.max (n, 1));
- while not (null (! running)) do
- (trace_active ();
- if not (null (! status))
- then (List.app SimpleThread.interrupt (! running))
- else ();
- wait_timeout ())));
-
- in ! status end);
-
-end;
--- a/src/Pure/Concurrent/task_queue.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Concurrent/task_queue.ML Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: Pure/Concurrent/task_queue.ML
- ID: $Id$
Author: Makarius
Ordered queue of grouped tasks.
@@ -8,7 +7,8 @@
signature TASK_QUEUE =
sig
eqtype task
- val new_task: unit -> task
+ val new_task: int -> task
+ val pri_of_task: task -> int
val str_of_task: task -> string
eqtype group
val new_group: unit -> group
@@ -17,9 +17,8 @@
type queue
val empty: queue
val is_empty: queue -> bool
- val enqueue: group -> task list -> bool -> (bool -> bool) -> queue -> task * queue
+ val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
val depend: task list -> task -> queue -> queue
- val focus: task list -> queue -> queue
val dequeue: queue -> (task * group * (unit -> bool)) option * queue
val dequeue_towards: task list -> queue ->
(((task * group * (unit -> bool)) * task list) option * queue)
@@ -29,20 +28,27 @@
val cancel: queue -> group -> bool
end;
-structure TaskQueue: TASK_QUEUE =
+structure Task_Queue: TASK_QUEUE =
struct
-(* identifiers *)
+(* tasks *)
+
+datatype task = Task of int * serial;
+fun new_task pri = Task (pri, serial ());
-datatype task = Task of serial;
-fun new_task () = Task (serial ());
+fun pri_of_task (Task (pri, _)) = pri;
+fun str_of_task (Task (_, i)) = string_of_int i;
-fun str_of_task (Task i) = string_of_int i;
+fun task_ord (Task t1, Task t2) = prod_ord (rev_order o int_ord) int_ord (t1, t2);
+structure Task_Graph = GraphFun(type key = task val ord = task_ord);
+(* groups *)
+
datatype group = Group of serial * bool ref;
fun new_group () = Group (serial (), ref true);
+
fun invalidate_group (Group (_, ok)) = ok := false;
fun str_of_group (Group (i, ref ok)) =
@@ -52,50 +58,46 @@
(* jobs *)
datatype job =
- Job of bool * (bool -> bool) | (*priority, job: status -> status*)
+ Job of bool -> bool |
Running of Thread.thread;
-type jobs = (group * job) IntGraph.T;
+type jobs = (group * job) Task_Graph.T;
-fun get_group (jobs: jobs) (Task id) = #1 (IntGraph.get_node jobs id);
-fun get_job (jobs: jobs) (Task id) = #2 (IntGraph.get_node jobs id);
-fun map_job (Task id) f (jobs: jobs) = IntGraph.map_node id (apsnd f) jobs;
+fun get_group (jobs: jobs) task = #1 (Task_Graph.get_node jobs task);
+fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task);
+fun map_job task f (jobs: jobs) = Task_Graph.map_node task (apsnd f) jobs;
-fun add_job (Task id) (Task dep) (jobs: jobs) =
- IntGraph.add_edge_acyclic (dep, id) jobs handle IntGraph.UNDEF _ => jobs;
+fun add_job task dep (jobs: jobs) =
+ Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
-fun check_job (jobs: jobs) (task as Task id) =
- if can (IntGraph.get_node jobs) id then SOME task else NONE;
+fun add_job_acyclic task dep (jobs: jobs) =
+ Task_Graph.add_edge_acyclic (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
(* queue of grouped jobs *)
datatype queue = Queue of
{groups: task list Inttab.table, (*groups with presently active members*)
- jobs: jobs, (*job dependency graph*)
- focus: task list}; (*particular collection of high-priority tasks*)
+ jobs: jobs}; (*job dependency graph*)
-fun make_queue groups jobs focus = Queue {groups = groups, jobs = jobs, focus = focus};
+fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
-val empty = make_queue Inttab.empty IntGraph.empty [];
-fun is_empty (Queue {jobs, ...}) = IntGraph.is_empty jobs;
+val empty = make_queue Inttab.empty Task_Graph.empty;
+fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs;
(* enqueue *)
-fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
+fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs}) =
let
- val task as Task id = new_task ();
+ val task = new_task pri;
val groups' = Inttab.cons_list (gid, task) groups;
val jobs' = jobs
- |> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;
- in (task, make_queue groups' jobs' focus) end;
+ |> Task_Graph.new_node (task, (group, Job job)) |> fold (add_job task) deps;
+ in (task, make_queue groups' jobs') end;
-fun depend deps task (Queue {groups, jobs, focus}) =
- make_queue groups (fold (add_job task) deps jobs) focus;
-
-fun focus tasks (Queue {groups, jobs, ...}) =
- make_queue groups jobs (map_filter (check_job jobs) tasks);
+fun depend deps task (Queue {groups, jobs}) =
+ make_queue groups (fold (add_job_acyclic task) deps jobs);
(* dequeue *)
@@ -103,38 +105,30 @@
local
fun dequeue_result NONE queue = (NONE, queue)
- | dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs, focus}) =
- (SOME result, make_queue groups (map_job task (K (Running (Thread.self ()))) jobs) focus);
-
-fun dequeue_global req_pri (queue as Queue {jobs, ...}) =
- let
- fun ready (id, ((group as Group (_, ref ok), Job (pri, job)), ([], _))) =
- if pri = req_pri then SOME (Task id, group, (fn () => job ok)) else NONE
- | ready _ = NONE;
- in dequeue_result (IntGraph.get_first ready jobs) queue end;
-
-fun dequeue_local focus (queue as Queue {jobs, ...}) =
- let
- fun ready id =
- (case IntGraph.get_node jobs id of
- (group as Group (_, ref ok), Job (_, job)) =>
- if null (IntGraph.imm_preds jobs id) then SOME (Task id, group, (fn () => job ok))
- else NONE
- | _ => NONE);
- val ids = map (fn Task id => id) focus;
- in dequeue_result (get_first ready (IntGraph.all_preds jobs ids)) queue end;
+ | dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs}) =
+ (SOME result, make_queue groups (map_job task (K (Running (Thread.self ()))) jobs));
in
-fun dequeue (queue as Queue {focus, ...}) =
- (case dequeue_local focus queue of
- (NONE, _) =>
- (case dequeue_global true queue of (NONE, _) => dequeue_global false queue | res => res)
- | res => res);
+fun dequeue (queue as Queue {jobs, ...}) =
+ let
+ fun ready (task, ((group as Group (_, ref ok), Job job), ([], _))) =
+ SOME (task, group, (fn () => job ok))
+ | ready _ = NONE;
+ in dequeue_result (Task_Graph.get_first ready jobs) queue end;
fun dequeue_towards tasks (queue as Queue {jobs, ...}) =
- let val tasks' = map_filter (check_job jobs) tasks in
- (case dequeue_local tasks' queue of
+ let
+ val tasks' = filter (can (Task_Graph.get_node jobs)) tasks;
+
+ fun ready task =
+ (case Task_Graph.get_node jobs task of
+ (group as Group (_, ref ok), Job job) =>
+ if null (Task_Graph.imm_preds jobs task) then SOME (task, group, (fn () => job ok))
+ else NONE
+ | _ => NONE);
+ in
+ (case dequeue_result (get_first ready (Task_Graph.all_preds jobs tasks')) queue of
(NONE, queue') => (NONE, queue')
| (SOME work, queue') => (SOME (work, tasks'), queue'))
end;
@@ -147,8 +141,13 @@
fun interrupt (Queue {jobs, ...}) task =
(case try (get_job jobs) task of SOME (Running thread) => SimpleThread.interrupt thread | _ => ());
-fun interrupt_external queue str =
- (case Int.fromString str of SOME id => interrupt queue (Task id) | NONE => ());
+fun interrupt_external (queue as Queue {jobs, ...}) str =
+ (case Int.fromString str of
+ SOME i =>
+ (case Task_Graph.get_first
+ (fn (task as Task (_, j), _) => if i = j then SOME task else NONE) jobs
+ of SOME task => interrupt queue task | NONE => ())
+ | NONE => ());
(* misc operations *)
@@ -161,12 +160,11 @@
val _ = List.app SimpleThread.interrupt running;
in null running end;
-fun finish (task as Task id) (Queue {groups, jobs, focus}) =
+fun finish task (Queue {groups, jobs}) =
let
val Group (gid, _) = get_group jobs task;
val groups' = Inttab.remove_list (op =) (gid, task) groups;
- val jobs' = IntGraph.del_node id jobs;
- val focus' = remove (op =) task focus;
- in make_queue groups' jobs' focus' end;
+ val jobs' = Task_Graph.del_node task jobs;
+ in make_queue groups' jobs' end;
end;
--- a/src/Pure/IsaMakefile Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/IsaMakefile Fri Dec 19 11:49:08 2008 +0000
@@ -23,26 +23,24 @@
$(OUT)/Pure: Concurrent/ROOT.ML Concurrent/future.ML \
Concurrent/mailbox.ML Concurrent/par_list.ML \
- Concurrent/par_list_dummy.ML Concurrent/schedule.ML \
- Concurrent/simple_thread.ML Concurrent/synchronized.ML \
- Concurrent/task_queue.ML General/ROOT.ML General/alist.ML \
- General/balanced_tree.ML General/basics.ML General/buffer.ML \
- General/file.ML General/graph.ML General/heap.ML General/integer.ML \
- General/lazy.ML General/markup.ML General/name_space.ML \
- General/ord_list.ML General/output.ML General/path.ML \
- General/position.ML General/pretty.ML General/print_mode.ML \
- General/properties.ML General/queue.ML General/scan.ML \
- General/secure.ML General/seq.ML General/source.ML General/stack.ML \
- General/symbol.ML General/symbol_pos.ML General/table.ML \
- General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML \
- Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
- Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML \
- Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
- Isar/expression.ML \
- Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML \
- Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
- Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
- Isar/new_locale.ML \
+ Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
+ Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \
+ General/alist.ML General/balanced_tree.ML General/basics.ML \
+ General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
+ General/integer.ML General/lazy.ML General/markup.ML \
+ General/name_space.ML General/ord_list.ML General/output.ML \
+ General/path.ML General/position.ML General/pretty.ML \
+ General/print_mode.ML General/properties.ML General/queue.ML \
+ General/scan.ML General/secure.ML General/seq.ML General/source.ML \
+ General/stack.ML General/symbol.ML General/symbol_pos.ML \
+ General/table.ML General/url.ML General/xml.ML General/yxml.ML \
+ Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \
+ Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML \
+ Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \
+ Isar/element.ML Isar/expression.ML Isar/find_theorems.ML \
+ Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
+ Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
+ Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/new_locale.ML \
Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
@@ -76,17 +74,16 @@
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
- Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
- Tools/isabelle_process.ML Tools/named_thms.ML \
- Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \
- conjunction.ML consts.ML context.ML context_position.ML conv.ML \
- defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \
- interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \
- morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML \
- proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \
- simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
- term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \
- variable.ML ../Tools/quickcheck.ML
+ Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
+ Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \
+ assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
+ consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
+ drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML \
+ logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \
+ old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML \
+ pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \
+ tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \
+ type_infer.ML unify.ML variable.ML ../Tools/quickcheck.ML
@./mk
--- a/src/Pure/Isar/class.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Isar/class.ML Fri Dec 19 11:49:08 2008 +0000
@@ -60,6 +60,59 @@
structure Class : CLASS =
struct
+(*temporary adaption code to mediate between old and new locale code*)
+
+structure Old_Locale =
+struct
+
+val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
+
+val interpretation = Locale.interpretation;
+val interpretation_in_locale = Locale.interpretation_in_locale;
+val get_interpret_morph = Locale.get_interpret_morph;
+val Locale = Locale.Locale;
+val extern = Locale.extern;
+val intros = Locale.intros;
+val dests = Locale.dests;
+val init = Locale.init;
+val Merge = Locale.Merge;
+val parameters_of_expr = Locale.parameters_of_expr;
+val empty = Locale.empty;
+val cert_expr = Locale.cert_expr;
+val read_expr = Locale.read_expr;
+val parameters_of = Locale.parameters_of;
+val add_locale = Locale.add_locale;
+
+end;
+
+structure New_Locale =
+struct
+
+val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
+
+val interpretation = Locale.interpretation; (*!*)
+val interpretation_in_locale = Locale.interpretation_in_locale; (*!*)
+val get_interpret_morph = Locale.get_interpret_morph; (*!*)
+fun Locale loc = ([(loc, ("", Expression.Positional []))], []);
+val extern = NewLocale.extern;
+val intros = Locale.intros; (*!*)
+val dests = Locale.dests; (*!*)
+val init = NewLocale.init;
+fun Merge locs = (map (fn loc => (loc, ("", Expression.Positional []))) locs, []);
+val parameters_of_expr = Locale.parameters_of_expr; (*!*)
+val empty = ([], []);
+val cert_expr = Locale.cert_expr; (*!"*)
+val read_expr = Locale.read_expr; (*!"*)
+val parameters_of = NewLocale.params_of; (*why typ option?*)
+val add_locale = Expression.add_locale;
+
+end;
+
+structure Locale = Old_Locale;
+
+(*proper code again*)
+
+
(** auxiliary **)
fun prove_interpretation tac prfx_atts expr inst =
@@ -542,7 +595,7 @@
val suplocales = map Locale.Locale sups;
val supexpr = Locale.Merge suplocales;
val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
- val mergeexpr = Locale.Merge (suplocales);
+ val mergeexpr = Locale.Merge suplocales;
val constrain = Element.Constrains ((map o apsnd o map_atyps)
(K (TFree (Name.aT, base_sort))) supparams);
fun fork_syn (Element.Fixes xs) =
--- a/src/Pure/Isar/local_theory.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Isar/local_theory.ML Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/local_theory.ML
- ID: $Id$
Author: Makarius
Local theory operations, with abstract target context.
--- a/src/Pure/Isar/toplevel.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Isar/toplevel.ML Fri Dec 19 11:49:08 2008 +0000
@@ -718,7 +718,7 @@
val future_proof = Proof.future_proof
(fn prf =>
- Future.fork_background (fn () =>
+ Future.fork_pri 1 (fn () =>
let val (states, State (result_node, _)) =
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
=> State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
--- a/src/Pure/Syntax/syntax.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Syntax/syntax.ML Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/syntax.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Standard Isabelle syntax, based on arbitrary context-free grammars
--- a/src/Pure/Thy/thy_info.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/Thy/thy_info.ML Fri Dec 19 11:49:08 2008 +0000
@@ -315,7 +315,13 @@
datatype task = Task of (unit -> unit) | Finished | Running;
fun task_finished Finished = true | task_finished _ = false;
-fun future_schedule task_graph =
+local
+
+fun schedule_seq tasks =
+ Graph.topological_order tasks
+ |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
+
+fun schedule_futures task_graph =
let
val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
(case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
@@ -339,45 +345,14 @@
val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
in ignore (Exn.release_all (thy_results @ proof_results)) end;
-local
-
-fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m))
- | max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) =
- if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task'
- | max_task _ task' = task';
-
-fun next_task G =
- let
- val tasks = Graph.minimals G |> map (fn name =>
- (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
- val finished = filter (task_finished o fst o snd) tasks;
- in
- if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
- else if null tasks then (Schedule.Terminate, G)
- else
- (case fold max_task tasks NONE of
- NONE => (Schedule.Wait, G)
- | SOME (name, (body, _)) =>
- (Schedule.Task {body = PrintMode.closure body,
- cont = Graph.del_nodes [name], fail = K Graph.empty},
- Graph.map_node name (K Running) G))
- end;
-
-fun schedule_seq tasks =
- Graph.topological_order tasks
- |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
-
in
fun schedule_tasks tasks n =
- let val m = Multithreading.max_threads_value () in
- if m <= 1 then schedule_seq tasks
- else if Multithreading.self_critical () then
+ if not (Multithreading.enabled ()) then schedule_seq tasks
+ else if Multithreading.self_critical () then
(warning (loader_msg "no multithreading within critical section" []);
schedule_seq tasks)
- else if Future.enabled () then future_schedule tasks
- else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
- end;
+ else schedule_futures tasks;
end;
--- a/src/Pure/goal.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/goal.ML Fri Dec 19 11:49:08 2008 +0000
@@ -179,7 +179,7 @@
val res =
if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
then result ()
- else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
+ else future_result ctxt' (Future.fork_pri 1 result) (Thm.term_of stmt);
in
Conjunction.elim_balanced (length props) res
|> map (Assumption.export false ctxt' ctxt)
--- a/src/Pure/pure_setup.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Pure/pure_setup.ML Fri Dec 19 11:49:08 2008 +0000
@@ -1,5 +1,4 @@
(* Title: Pure/pure_setup.ML
- ID: $Id$
Author: Makarius
Pure theory and ML toplevel setup.
@@ -28,8 +27,8 @@
(* ML toplevel pretty printing *)
-install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task));
-install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group));
+install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
+install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
--- a/src/Tools/code/code_haskell.ML Mon Dec 15 10:40:52 2008 +0000
+++ b/src/Tools/code/code_haskell.ML Fri Dec 19 11:49:08 2008 +0000
@@ -414,7 +414,10 @@
o NameSpace.explode) modlname;
val pathname = Path.append destination filename;
val _ = File.mkdir (Path.dir pathname);
- in File.write pathname (Code_Target.code_of_pretty content) end
+ in File.write pathname
+ ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
+ ^ Code_Target.code_of_pretty content)
+ end
in
Code_Target.mk_serialization target NONE
(fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module file))