--- a/NEWS Mon Jun 28 15:32:27 2010 +0200
+++ b/NEWS Tue Jun 29 07:55:18 2010 +0200
@@ -4,8 +4,23 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
+a Unicode character is treated as a single symbol, not a sequence of
+non-ASCII bytes as before. Since Isabelle/ML string literals may
+contain symbols without further backslash escapes, Unicode can now be
+used here as well. Recall that Symbol.explode in ML provides a
+consistent view on symbols, while raw explode (or String.explode)
+merely give a byte-oriented representation.
+
+
*** HOL ***
+* Constant "split" has been merged with constant "prod_case"; names
+of ML functions, facts etc. involving split have been retained so far,
+though. INCOMPATIBILITY.
+
* Dropped old infix syntax "mem" for List.member; use "in set"
instead. INCOMPATIBILITY.
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Tue Jun 29 07:55:18 2010 +0200
@@ -527,8 +527,10 @@
\begin{enumerate}
- \item a single ASCII character ``@{text "c"}'' or raw byte in the
- range of 128\dots 255, for example ``\verb,a,'',
+ \item a single ASCII character ``@{text "c"}'', for example
+ ``\verb,a,'',
+
+ \item a codepoint according to UTF8 (non-ASCII byte sequence),
\item a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',
@@ -555,19 +557,17 @@
``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
may occur within regular Isabelle identifiers.
- Since the character set underlying Isabelle symbols is 7-bit ASCII
- and 8-bit characters are passed through transparently, Isabelle can
- also process Unicode/UCS data in UTF-8 encoding.\footnote{When
- counting precise source positions internally, bytes in the range of
- 128\dots 191 are ignored. In UTF-8 encoding, this interval covers
- the additional trailer bytes, so Isabelle happens to count Unicode
- characters here, not bytes in memory. In ISO-Latin encoding, the
- ignored range merely includes some extra punctuation characters that
- even have replacements within the standard collection of Isabelle
- symbols; the accented letters range is counted properly.} Unicode
- provides its own collection of mathematical symbols, but within the
- core Isabelle/ML world there is no link to the standard collection
- of Isabelle regular symbols.
+ The character set underlying Isabelle symbols is 7-bit ASCII, but
+ 8-bit character sequences are passed-through unchanged. Unicode/UCS
+ data in UTF-8 encoding is processed in a non-strict fashion, such
+ that well-formed code sequences are recognized
+ accordingly.\footnote{Note that ISO-Latin-1 differs from UTF-8 only
+ in some special punctuation characters that even have replacements
+ within the standard collection of Isabelle symbols. Text consisting
+ of ASCII plus accented letters can be processed in either encoding.}
+ Unicode provides its own collection of mathematical symbols, but
+ within the core Isabelle/ML world there is no link to the standard
+ collection of Isabelle regular symbols.
\medskip Output of Isabelle symbols depends on the print mode
(\secref{print-mode}). For example, the standard {\LaTeX} setup of
@@ -612,8 +612,8 @@
\item @{ML_type "Symbol.sym"} is a concrete datatype that represents
the different kinds of symbols explicitly, with constructors @{ML
- "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML
- "Symbol.Raw"}.
+ "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.UTF8"}, @{ML
+ "Symbol.Ctrl"}, @{ML "Symbol.Raw"}.
\item @{ML "Symbol.decode"} converts the string representation of a
symbol into the datatype version.
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Jun 28 15:32:27 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue Jun 29 07:55:18 2010 +0200
@@ -648,8 +648,10 @@
\begin{enumerate}
- \item a single ASCII character ``\isa{c}'' or raw byte in the
- range of 128\dots 255, for example ``\verb,a,'',
+ \item a single ASCII character ``\isa{c}'', for example
+ ``\verb,a,'',
+
+ \item a codepoint according to UTF8 (non-ASCII byte sequence),
\item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',
@@ -673,19 +675,17 @@
``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
may occur within regular Isabelle identifiers.
- Since the character set underlying Isabelle symbols is 7-bit ASCII
- and 8-bit characters are passed through transparently, Isabelle can
- also process Unicode/UCS data in UTF-8 encoding.\footnote{When
- counting precise source positions internally, bytes in the range of
- 128\dots 191 are ignored. In UTF-8 encoding, this interval covers
- the additional trailer bytes, so Isabelle happens to count Unicode
- characters here, not bytes in memory. In ISO-Latin encoding, the
- ignored range merely includes some extra punctuation characters that
- even have replacements within the standard collection of Isabelle
- symbols; the accented letters range is counted properly.} Unicode
- provides its own collection of mathematical symbols, but within the
- core Isabelle/ML world there is no link to the standard collection
- of Isabelle regular symbols.
+ The character set underlying Isabelle symbols is 7-bit ASCII, but
+ 8-bit character sequences are passed-through unchanged. Unicode/UCS
+ data in UTF-8 encoding is processed in a non-strict fashion, such
+ that well-formed code sequences are recognized
+ accordingly.\footnote{Note that ISO-Latin-1 differs from UTF-8 only
+ in some special punctuation characters that even have replacements
+ within the standard collection of Isabelle symbols. Text consisting
+ of ASCII plus accented letters can be processed in either encoding.}
+ Unicode provides its own collection of mathematical symbols, but
+ within the core Isabelle/ML world there is no link to the standard
+ collection of Isabelle regular symbols.
\medskip Output of Isabelle symbols depends on the print mode
(\secref{print-mode}). For example, the standard {\LaTeX} setup of
@@ -733,7 +733,7 @@
\cite{isabelle-isar-ref}.
\item \verb|Symbol.sym| is a concrete datatype that represents
- the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
+ the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.UTF8|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
\item \verb|Symbol.decode| converts the string representation of a
symbol into the datatype version.
--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 28 15:32:27 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 29 07:55:18 2010 +0200
@@ -448,13 +448,6 @@
should be considered particularly relevant. Enabling this option tends to lead
to larger problems and typically slows down the ATPs.
-\optrue{respect\_no\_atp}{ignore\_no\_atp}
-Specifies whether Sledgehammer should honor the \textit{no\_atp} attributes. The
-\textit{no\_atp} attributes marks theorems that tend to confuse ATPs, typically
-because they can lead to unsound ATP proofs \cite{boehme-nipkow-2010}. It is
-normally a good idea to leave this option enabled, unless you are debugging
-Sledgehammer.
-
\end{enum}
\subsection{Output Format}
--- a/src/HOL/Hoare/Hoare_Logic.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Jun 29 07:55:18 2010 +0200
@@ -68,7 +68,7 @@
fun mk_abstuple [x] body = abs (x, body)
| mk_abstuple (x::xs) body =
- Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
+ Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
| mk_fbody a e ((b,_)::xs) =
@@ -128,21 +128,21 @@
(*** print translations ***)
ML{*
-fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
subst_bound (Syntax.free v, dest_abstuple body)
| dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
| dest_abstuple trm = trm;
-fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
| abs2list (Abs(x,T,t)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
| mk_ts (Abs(x,_,t)) = mk_ts t
| mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
| mk_ts t = [t];
-fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
((Syntax.free x)::(abs2list t), mk_ts t)
| mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
| mk_vts t = raise Match;
@@ -152,7 +152,7 @@
if t = Bound i then find_ch vts (i-1) xs
else (true, (v, subst_bounds (xs, t)));
-fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
+fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
| is_f (Abs(x,_,t)) = true
| is_f t = false;
*}
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Jun 29 07:55:18 2010 +0200
@@ -70,7 +70,7 @@
fun mk_abstuple [x] body = abs (x, body)
| mk_abstuple (x::xs) body =
- Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
+ Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
| mk_fbody a e ((b,_)::xs) =
@@ -130,21 +130,21 @@
(*** print translations ***)
ML{*
-fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
subst_bound (Syntax.free v, dest_abstuple body)
| dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
| dest_abstuple trm = trm;
-fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
| abs2list (Abs(x,T,t)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
| mk_ts (Abs(x,_,t)) = mk_ts t
| mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
| mk_ts t = [t];
-fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
((Syntax.free x)::(abs2list t), mk_ts t)
| mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
| mk_vts t = raise Match;
@@ -154,7 +154,7 @@
if t = Bound i then find_ch vts (i-1) xs
else (true, (v, subst_bounds (xs,t)));
-fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
+fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
| is_f (Abs(x,_,t)) = true
| is_f t = false;
*}
--- a/src/HOL/Hoare/hoare_tac.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Tue Jun 29 07:55:18 2010 +0200
@@ -16,7 +16,7 @@
local open HOLogic in
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
| abs2list (Abs (x, T, t)) = [Free (x, T)]
| abs2list _ = [];
@@ -32,7 +32,7 @@
else let val z = mk_abstupleC w body;
val T2 = case z of Abs(_,T,_) => T
| Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
- in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
+ in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
$ absfree (n, T, z) end end;
(** maps [x1,...,xn] to (x1,...,xn) and types**)
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 29 07:55:18 2010 +0200
@@ -379,7 +379,7 @@
from this Inl 1(1) exec_f mrec show ?thesis
proof (cases "ret_mrec")
case (Inl aaa)
- from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
+ from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
show ?thesis
apply auto
apply (rule rec_case)
--- a/src/HOL/Import/HOL/pair.imp Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Import/HOL/pair.imp Tue Jun 29 07:55:18 2010 +0200
@@ -10,8 +10,8 @@
"prod" > "Product_Type.*"
const_maps
- "pair_case" > "Product_Type.split"
- "UNCURRY" > "Product_Type.split"
+ "pair_case" > "Product_Type.prod_case"
+ "UNCURRY" > "Product_Type.prod_case"
"FST" > "Product_Type.fst"
"SND" > "Product_Type.snd"
"RPROD" > "HOL4Base.pair.RPROD"
--- a/src/HOL/IsaMakefile Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Jun 29 07:55:18 2010 +0200
@@ -267,6 +267,7 @@
$(SRC)/Provers/Arith/extract_common_term.ML \
$(SRC)/Tools/cache_io.ML \
$(SRC)/Tools/Metis/metis.ML \
+ Tools/ATP_Manager/async_manager.ML \
Tools/ATP_Manager/atp_manager.ML \
Tools/ATP_Manager/atp_systems.ML \
Tools/choice_specification.ML \
@@ -313,13 +314,12 @@
Tools/Quotient/quotient_typ.ML \
Tools/recdef.ML \
Tools/semiring_normalizer.ML \
+ Tools/Sledgehammer/clausifier.ML \
Tools/Sledgehammer/meson_tactic.ML \
+ Tools/Sledgehammer/metis_clauses.ML \
Tools/Sledgehammer/metis_tactics.ML \
Tools/Sledgehammer/sledgehammer_fact_filter.ML \
Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
- Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
- Tools/Sledgehammer/sledgehammer_fol_clause.ML \
- Tools/Sledgehammer/sledgehammer_hol_clause.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
Tools/Sledgehammer/sledgehammer_tptp_format.ML \
--- a/src/HOL/Library/AssocList.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Tue Jun 29 07:55:18 2010 +0200
@@ -427,8 +427,7 @@
lemma merge_updates:
"merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
- by (simp add: merge_def updates_def split_prod_case
- foldr_fold_rev zip_rev zip_map_fst_snd)
+ by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -449,7 +448,7 @@
More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
then show ?thesis
- by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq)
+ by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
qed
corollary merge_conv:
--- a/src/HOL/Library/Nat_Bijection.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy Tue Jun 29 07:55:18 2010 +0200
@@ -213,6 +213,7 @@
termination list_decode
apply (relation "measure id", simp_all)
apply (drule arg_cong [where f="prod_encode"])
+apply (drule sym)
apply (simp add: le_imp_less_Suc le_prod_encode_2)
done
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Jun 29 07:55:18 2010 +0200
@@ -18,7 +18,7 @@
section {* Pairs *}
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
section {* Bounded quantifiers *}
--- a/src/HOL/Library/RBT_Impl.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Tue Jun 29 07:55:18 2010 +0200
@@ -1076,7 +1076,7 @@
from this Empty_is_rbt have
"lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
by (simp add: `ys = rev xs`)
- then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
+ then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
qed
hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
--- a/src/HOL/Library/Transitive_Closure_Table.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Jun 29 07:55:18 2010 +0200
@@ -189,7 +189,7 @@
declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
-code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp
+code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastsimp
subsection {* A simple example *}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 29 07:55:18 2010 +0200
@@ -325,7 +325,7 @@
NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
- handle Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
+ handle Metis_Clauses.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
@@ -382,7 +382,7 @@
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
- open Sledgehammer_Fact_Minimizer
+ open Metis_Clauses
open Sledgehammer_Isar
val thy = Proof.theory_of st
val n0 = length (these (!named_thms))
@@ -393,7 +393,8 @@
|> the_default 5
val params = default_params thy
[("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
- val minimize = minimize_theorems params 1 (subgoal_count st)
+ val minimize =
+ Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Jun 29 07:55:18 2010 +0200
@@ -323,7 +323,7 @@
let val VarAbs = Syntax.variant_abs(s,tp,trm);
in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
end
- | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
+ | get_decls sign Clist ((Const (@{const_name prod_case}, _)) $ trm) = get_decls sign Clist trm
| get_decls sign Clist trm = (Clist,trm);
fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
@@ -389,7 +389,7 @@
val t2 = t1 $ ParamDeclTerm
in t2 end;
-fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
+fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name prod_case}, _) $ _)) = true
| is_fundef (Const("==", _) $ _ $ Abs _) = true
| is_fundef _ = false;
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Jun 29 07:55:18 2010 +0200
@@ -17,11 +17,11 @@
subsection {* Curry in a Hurry *}
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
by auto
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
by auto
lemma "split (curry f) = f"
@@ -61,12 +61,12 @@
by auto
lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
apply (rule ext)+
by auto
lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
apply (rule ext)+
by auto
--- a/src/HOL/Predicate.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Predicate.thy Tue Jun 29 07:55:18 2010 +0200
@@ -645,7 +645,7 @@
lemma "f () = False \<or> f () = True"
by simp
-lemma closure_of_bool_cases:
+lemma closure_of_bool_cases [no_atp]:
assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
assumes "f = (%u. True) \<Longrightarrow> P f"
shows "P f"
--- a/src/HOL/Probability/Borel.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Tue Jun 29 07:55:18 2010 +0200
@@ -203,7 +203,7 @@
by (metis surj_def)
from Fract i j n show ?thesis
- by (metis prod.cases prod_case_split)
+ by (metis prod.cases)
qed
qed
--- a/src/HOL/Probability/Caratheodory.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Tue Jun 29 07:55:18 2010 +0200
@@ -829,7 +829,7 @@
with sbBB [of i] obtain j where "x \<in> BB i j"
by blast
thus "\<exists>i. x \<in> split BB (prod_decode i)"
- by (metis prod_encode_inverse prod.cases prod_case_split)
+ by (metis prod_encode_inverse prod.cases)
qed
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
by (rule ext) (auto simp add: C_def)
--- a/src/HOL/Product_Type.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Product_Type.thy Tue Jun 29 07:55:18 2010 +0200
@@ -163,8 +163,8 @@
subsubsection {* Tuple syntax *}
-definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- split_prod_case: "split == prod_case"
+abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+ "split \<equiv> prod_case"
text {*
Patterns -- extends pre-defined type @{typ pttrn} used in
@@ -185,8 +185,8 @@
translations
"(x, y)" == "CONST Pair x y"
"_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
- "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
- "%(x, y). b" == "CONST split (%x y. b)"
+ "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
+ "%(x, y). b" == "CONST prod_case (%x y. b)"
"_abs (CONST Pair x y) t" => "%(x, y). t"
-- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
@@ -204,7 +204,7 @@
Syntax.const @{syntax_const "_abs"} $
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end
- | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
+ | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
(* split (%x. (split (%y z. t))) => %(x,y,z). t *)
let
val Const (@{syntax_const "_abs"}, _) $
@@ -215,7 +215,7 @@
(Syntax.const @{syntax_const "_pattern"} $ x' $
(Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
end
- | split_tr' [Const (@{const_syntax split}, _) $ t] =
+ | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
(* split (split (%x y z. t)) => %((x, y), z). t *)
split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
| split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
@@ -225,7 +225,7 @@
(Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
end
| split_tr' _ = raise Match;
-in [(@{const_syntax split}, split_tr')] end
+in [(@{const_syntax prod_case}, split_tr')] end
*}
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
@@ -234,7 +234,7 @@
fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
| split_guess_names_tr' _ T [Abs (x, xT, t)] =
(case (head_of t) of
- Const (@{const_syntax split}, _) => raise Match
+ Const (@{const_syntax prod_case}, _) => raise Match
| _ =>
let
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -246,7 +246,7 @@
end)
| split_guess_names_tr' _ T [t] =
(case head_of t of
- Const (@{const_syntax split}, _) => raise Match
+ Const (@{const_syntax prod_case}, _) => raise Match
| _ =>
let
val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -257,21 +257,12 @@
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
| split_guess_names_tr' _ _ _ = raise Match;
-in [(@{const_syntax split}, split_guess_names_tr')] end
+in [(@{const_syntax prod_case}, split_guess_names_tr')] end
*}
subsubsection {* Code generator setup *}
-lemma split_case_cert:
- assumes "CASE \<equiv> split f"
- shows "CASE (a, b) \<equiv> f a b"
- using assms by (simp add: split_prod_case)
-
-setup {*
- Code.add_case @{thm split_case_cert}
-*}
-
code_type *
(SML infix 2 "*")
(OCaml infix 2 "*")
@@ -315,7 +306,7 @@
val s' = Codegen.new_name t s;
val v = Free (s', T)
in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
- | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
+ | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) =
(case strip_abs_split (i+1) t of
(v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
| _ => ([], u))
@@ -357,7 +348,7 @@
| _ => NONE);
fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
- (t1 as Const (@{const_name split}, _), t2 :: ts) =>
+ (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
let
val ([p], u) = strip_abs_split 1 (t1 $ t2);
val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
@@ -421,7 +412,7 @@
by (simp add: Pair_fst_snd_eq)
lemma split_conv [simp, code]: "split f (a, b) = f a b"
- by (simp add: split_prod_case)
+ by (fact prod.cases)
lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
by (rule split_conv [THEN iffD2])
@@ -430,11 +421,11 @@
by (rule split_conv [THEN iffD1])
lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
- by (simp add: split_prod_case expand_fun_eq split: prod.split)
+ by (simp add: expand_fun_eq split: prod.split)
lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
-- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
- by (simp add: split_prod_case expand_fun_eq split: prod.split)
+ by (simp add: expand_fun_eq split: prod.split)
lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
by (cases x) simp
@@ -443,7 +434,7 @@
by (cases p) simp
lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
- by (simp add: split_prod_case prod_case_unfold)
+ by (simp add: prod_case_unfold)
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
-- {* Prevents simplification of @{term c}: much faster *}
@@ -529,7 +520,7 @@
| no_args k i (Bound m) = m < k orelse m > k + i
| no_args _ _ _ = true;
fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
- | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
+ | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
| split_pat tp i _ = NONE;
fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
@@ -546,12 +537,12 @@
if Pair_pat k i (t $ u) then incr_boundvars k arg
else (subst arg k i t $ subst arg k i u)
| subst arg k i t = t;
- fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
+ fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
| NONE => NONE)
| beta_proc _ _ = NONE;
- fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
+ fun eta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
(case split_pat eta_term_pat 1 t of
SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
| NONE => NONE)
@@ -598,10 +589,10 @@
done
lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
- by (induct p) (auto simp add: split_prod_case)
+ by (induct p) auto
lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
- by (induct p) (auto simp add: split_prod_case)
+ by (induct p) auto
lemma splitE2:
"[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
@@ -627,14 +618,14 @@
assumes major: "z \<in> split c p"
and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
shows Q
- by (rule major [unfolded split_prod_case prod_case_unfold] cases surjective_pairing)+
+ by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+
declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
ML {*
local (* filtering with exists_p_split is an essential optimization *)
- fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
+ fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
| exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
| exists_p_split (Abs (_, _, t)) = exists_p_split t
| exists_p_split _ = false;
@@ -712,13 +703,9 @@
declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
declare prod_caseE' [elim!] prod_caseE [elim!]
-lemma prod_case_split:
- "prod_case = split"
- by (auto simp add: expand_fun_eq)
-
lemma prod_case_beta:
"prod_case f p = f (fst p) (snd p)"
- unfolding prod_case_split split_beta ..
+ by (fact split_beta)
lemma prod_cases3 [cases type]:
obtains (fields) a b c where "y = (a, b, c)"
@@ -762,7 +749,7 @@
lemma split_def:
"split = (\<lambda>c p. c (fst p) (snd p))"
- unfolding split_prod_case prod_case_unfold ..
+ by (fact prod_case_unfold)
definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
"internal_split == split"
--- a/src/HOL/Quotient.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Quotient.thy Tue Jun 29 07:55:18 2010 +0200
@@ -764,13 +764,23 @@
subsection {* Methods / Interface *}
method_setup lifting =
- {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
+ {* Attrib.thms >> (fn thms => fn ctxt =>
+ SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
{* lifts theorems to quotient types *}
method_setup lifting_setup =
- {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
+ {* Attrib.thm >> (fn thm => fn ctxt =>
+ SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
{* sets up the three goals for the quotient lifting procedure *}
+method_setup descending =
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
+ {* decends theorems to the raw level *}
+
+method_setup descending_setup =
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
+ {* sets up the three goals for the decending theorems *}
+
method_setup regularize =
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
{* proves the regularization goals from the quotient lifting procedure *}
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Jun 29 07:55:18 2010 +0200
@@ -114,43 +114,6 @@
apply(assumption)
done
-lemma plus_assoc_raw:
- shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
- by (cases i, cases j, cases k) (simp)
-
-lemma plus_sym_raw:
- shows "plus_int_raw i j \<approx> plus_int_raw j i"
- by (cases i, cases j) (simp)
-
-lemma plus_zero_raw:
- shows "plus_int_raw (0, 0) i \<approx> i"
- by (cases i) (simp)
-
-lemma plus_minus_zero_raw:
- shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
- by (cases i) (simp)
-
-lemma times_assoc_raw:
- shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
- by (cases i, cases j, cases k)
- (simp add: algebra_simps)
-
-lemma times_sym_raw:
- shows "times_int_raw i j \<approx> times_int_raw j i"
- by (cases i, cases j) (simp add: algebra_simps)
-
-lemma times_one_raw:
- shows "times_int_raw (1, 0) i \<approx> i"
- by (cases i) (simp)
-
-lemma times_plus_comm_raw:
- shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
-by (cases i, cases j, cases k)
- (simp add: algebra_simps)
-
-lemma one_zero_distinct:
- shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
- by simp
text{* The integers form a @{text comm_ring_1}*}
@@ -158,25 +121,25 @@
proof
fix i j k :: int
show "(i + j) + k = i + (j + k)"
- by (lifting plus_assoc_raw)
+ by (descending) (auto)
show "i + j = j + i"
- by (lifting plus_sym_raw)
+ by (descending) (auto)
show "0 + i = (i::int)"
- by (lifting plus_zero_raw)
+ by (descending) (auto)
show "- i + i = 0"
- by (lifting plus_minus_zero_raw)
+ by (descending) (auto)
show "i - j = i + - j"
by (simp add: minus_int_def)
show "(i * j) * k = i * (j * k)"
- by (lifting times_assoc_raw)
+ by (descending) (auto simp add: algebra_simps)
show "i * j = j * i"
- by (lifting times_sym_raw)
+ by (descending) (auto)
show "1 * i = i"
- by (lifting times_one_raw)
+ by (descending) (auto)
show "(i + j) * k = i * k + j * k"
- by (lifting times_plus_comm_raw)
+ by (descending) (auto simp add: algebra_simps)
show "0 \<noteq> (1::int)"
- by (lifting one_zero_distinct)
+ by (descending) (auto)
qed
lemma plus_int_raw_rsp_aux:
@@ -211,36 +174,19 @@
by (induct m)
(simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
-lemma le_antisym_raw:
- shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
- by (cases i, cases j) (simp)
-
-lemma le_refl_raw:
- shows "le_int_raw i i"
- by (cases i) (simp)
-
-lemma le_trans_raw:
- shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
- by (cases i, cases j, cases k) (simp)
-
-lemma le_cases_raw:
- shows "le_int_raw i j \<or> le_int_raw j i"
- by (cases i, cases j)
- (simp add: linorder_linear)
-
instance int :: linorder
proof
fix i j k :: int
show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
- by (lifting le_antisym_raw)
+ by (descending) (auto)
show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
by (auto simp add: less_int_def dest: antisym)
show "i \<le> i"
- by (lifting le_refl_raw)
+ by (descending) (auto)
show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
- by (lifting le_trans_raw)
+ by (descending) (auto)
show "i \<le> j \<or> j \<le> i"
- by (lifting le_cases_raw)
+ by (descending) (auto)
qed
instantiation int :: distrib_lattice
@@ -258,15 +204,11 @@
end
-lemma le_plus_int_raw:
- shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
- by (cases i, cases j, cases k) (simp)
-
instance int :: ordered_cancel_ab_semigroup_add
proof
fix i j k :: int
show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (lifting le_plus_int_raw)
+ by (descending) (auto)
qed
abbreviation
@@ -296,7 +238,7 @@
fixes k::int
shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
unfolding less_int_def int_of_nat
- by (lifting zero_le_imp_eq_int_raw)
+ by (descending) (rule zero_le_imp_eq_int_raw)
lemma zmult_zless_mono2:
fixes i j k::int
@@ -365,16 +307,10 @@
shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
by (auto iff: int_to_nat_raw_def)
-lemma nat_le_eq_zle_raw:
- assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
- shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
- using a
- by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
-
lemma nat_le_eq_zle:
fixes w z::"int"
shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
unfolding less_int_def
- by (lifting nat_le_eq_zle_raw)
+ by (descending) (auto simp add: int_to_nat_raw_def)
end
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Jun 29 07:55:18 2010 +0200
@@ -32,7 +32,7 @@
text{*Proving that it is an equivalence relation*}
lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
+by (induct X) (auto intro: msgrel.intros)
theorem equiv_msgrel: "equivp msgrel"
proof (rule equivpI)
@@ -263,68 +263,47 @@
subsection{*Injectivity Properties of Some Constructors*}
-lemma NONCE_imp_eq:
- shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
- by (drule msgrel_imp_eq_freenonces, simp)
-
text{*Can also be proved using the function @{term nonces}*}
lemma Nonce_Nonce_eq [iff]:
shows "(Nonce m = Nonce n) = (m = n)"
proof
assume "Nonce m = Nonce n"
- then show "m = n" by (lifting NONCE_imp_eq)
+ then show "m = n"
+ by (descending) (drule msgrel_imp_eq_freenonces, simp)
next
assume "m = n"
then show "Nonce m = Nonce n" by simp
qed
-lemma MPAIR_imp_eqv_left:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
- by (drule msgrel_imp_eqv_freeleft) (simp)
-
lemma MPair_imp_eq_left:
assumes eq: "MPair X Y = MPair X' Y'"
shows "X = X'"
- using eq by (lifting MPAIR_imp_eqv_left)
-
-lemma MPAIR_imp_eqv_right:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
- by (drule msgrel_imp_eqv_freeright) (simp)
+ using eq
+ by (descending) (drule msgrel_imp_eqv_freeleft, simp)
lemma MPair_imp_eq_right:
shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
- by (lifting MPAIR_imp_eqv_right)
+ by (descending) (drule msgrel_imp_eqv_freeright, simp)
theorem MPair_MPair_eq [iff]:
shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
-lemma NONCE_neqv_MPAIR:
- shows "\<not>(NONCE m \<sim> MPAIR X Y)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
theorem Nonce_neq_MPair [iff]:
shows "Nonce N \<noteq> MPair X Y"
- by (lifting NONCE_neqv_MPAIR)
+ by (descending) (auto dest: msgrel_imp_eq_freediscrim)
text{*Example suggested by a referee*}
-lemma CRYPT_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
theorem Crypt_Nonce_neq_Nonce:
shows "Crypt K (Nonce M) \<noteq> Nonce N"
- by (lifting CRYPT_NONCE_neq_NONCE)
+ by (descending) (auto dest: msgrel_imp_eq_freediscrim)
text{*...and many similar results*}
-lemma CRYPT2_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
theorem Crypt2_Nonce_neq_Nonce:
shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
- by (lifting CRYPT2_NONCE_neq_NONCE)
+ by (descending) (auto dest: msgrel_imp_eq_freediscrim)
theorem Crypt_Crypt_eq [iff]:
shows "(Crypt K X = Crypt K X') = (X=X')"
--- a/src/HOL/Sledgehammer.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Jun 29 07:55:18 2010 +0200
@@ -11,19 +11,19 @@
imports Plain Hilbert_Choice
uses
"~~/src/Tools/Metis/metis.ML"
- "Tools/Sledgehammer/sledgehammer_util.ML"
- ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
- ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
- ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
- ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
+ ("Tools/Sledgehammer/clausifier.ML")
+ ("Tools/Sledgehammer/meson_tactic.ML")
+ ("Tools/Sledgehammer/metis_clauses.ML")
+ ("Tools/Sledgehammer/metis_tactics.ML")
+ ("Tools/Sledgehammer/sledgehammer_util.ML")
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
+ ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
+ ("Tools/ATP_Manager/async_manager.ML")
("Tools/ATP_Manager/atp_manager.ML")
("Tools/ATP_Manager/atp_systems.ML")
("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
("Tools/Sledgehammer/sledgehammer_isar.ML")
- ("Tools/Sledgehammer/meson_tactic.ML")
- ("Tools/Sledgehammer/metis_tactics.ML")
begin
definition skolem_id :: "'a \<Rightarrow> 'a" where
@@ -85,32 +85,25 @@
apply (simp add: COMBC_def)
done
-
-subsection {* Setup of external ATPs *}
+use "Tools/Sledgehammer/clausifier.ML"
+setup Clausifier.setup
-use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
-use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
-setup Sledgehammer_Fact_Preprocessor.setup
-use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
-use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
+use "Tools/Sledgehammer/meson_tactic.ML"
+setup Meson_Tactic.setup
+
+use "Tools/Sledgehammer/metis_clauses.ML"
+use "Tools/Sledgehammer/metis_tactics.ML"
+
+use "Tools/Sledgehammer/sledgehammer_util.ML"
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
+use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
+use "Tools/ATP_Manager/async_manager.ML"
use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_systems.ML"
setup ATP_Systems.setup
use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
-
-
-subsection {* The MESON prover *}
-
-use "Tools/Sledgehammer/meson_tactic.ML"
-setup Meson_Tactic.setup
-
-
-subsection {* The Metis prover *}
-
-use "Tools/Sledgehammer/metis_tactics.ML"
setup Metis_Tactics.setup
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/async_manager.ML Tue Jun 29 07:55:18 2010 +0200
@@ -0,0 +1,241 @@
+(* Title: HOL/Tools/ATP_Manager/async_manager.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Central manager for asynchronous diagnosis tool threads.
+*)
+
+signature ASYNC_MANAGER =
+sig
+ val launch :
+ string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
+ -> unit
+ val kill_threads : string -> string -> unit
+ val running_threads : string -> string -> unit
+ val thread_messages : string -> string -> int option -> unit
+end;
+
+structure Async_Manager : ASYNC_MANAGER =
+struct
+
+(** preferences **)
+
+val message_store_limit = 20;
+val message_display_limit = 5;
+
+
+(** thread management **)
+
+(* data structures over threads *)
+
+structure Thread_Heap = Heap
+(
+ type elem = Time.time * Thread.thread;
+ fun ord ((a, _), (b, _)) = Time.compare (a, b);
+);
+
+fun lookup_thread xs = AList.lookup Thread.equal xs;
+fun delete_thread xs = AList.delete Thread.equal xs;
+fun update_thread xs = AList.update Thread.equal xs;
+
+
+(* state of thread manager *)
+
+type state =
+ {manager: Thread.thread option,
+ timeout_heap: Thread_Heap.T,
+ active: (Thread.thread * (string * Time.time * Time.time * string)) list,
+ canceling: (Thread.thread * (string * Time.time * string)) list,
+ messages: (string * string) list,
+ store: (string * string) list}
+
+fun make_state manager timeout_heap active canceling messages store : state =
+ {manager = manager, timeout_heap = timeout_heap, active = active,
+ canceling = canceling, messages = messages, store = store}
+
+val global_state = Synchronized.var "async_manager"
+ (make_state NONE Thread_Heap.empty [] [] [] []);
+
+
+(* unregister thread *)
+
+fun unregister verbose message thread =
+ Synchronized.change global_state
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ (case lookup_thread active thread of
+ SOME (tool, birth_time, _, desc) =>
+ let
+ val active' = delete_thread thread active;
+ val now = Time.now ()
+ val canceling' = (thread, (tool, now, desc)) :: canceling
+ val message' =
+ desc ^ "\n" ^ message ^
+ (if verbose then
+ "Total time: " ^ Int.toString (Time.toMilliseconds
+ (Time.- (now, birth_time))) ^ " ms.\n"
+ else
+ "")
+ val messages' = (tool, message') :: messages;
+ val store' = (tool, message') ::
+ (if length store <= message_store_limit then store
+ else #1 (chop message_store_limit store));
+ in make_state manager timeout_heap active' canceling' messages' store' end
+ | NONE => state));
+
+
+(* main manager thread -- only one may exist *)
+
+val min_wait_time = Time.fromMilliseconds 300;
+val max_wait_time = Time.fromSeconds 10;
+
+fun replace_all bef aft =
+ let
+ fun aux seen "" = String.implode (rev seen)
+ | aux seen s =
+ if String.isPrefix bef s then
+ aux seen "" ^ aft ^ aux [] (unprefix bef s)
+ else
+ aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
+ in aux [] end
+
+(* This is a workaround for Proof General's off-by-a-few sendback display bug,
+ whereby "pr" in "proof" is not highlighted. *)
+val break_into_chunks =
+ maps (space_explode "\000" o replace_all "\n\n" "\000" o snd)
+
+fun print_new_messages () =
+ case Synchronized.change_result global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ (messages, make_state manager timeout_heap active canceling []
+ store)) of
+ [] => ()
+ | msgs as (tool, _) :: _ =>
+ let val ss = break_into_chunks msgs in
+ List.app priority (tool ^ ": " ^ hd ss :: tl ss)
+ end
+
+fun check_thread_manager verbose = Synchronized.change global_state
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
+ else let val manager = SOME (Toplevel.thread false (fn () =>
+ let
+ fun time_limit timeout_heap =
+ (case try Thread_Heap.min timeout_heap of
+ NONE => Time.+ (Time.now (), max_wait_time)
+ | SOME (time, _) => time);
+
+ (*action: find threads whose timeout is reached, and interrupt canceling threads*)
+ fun action {manager, timeout_heap, active, canceling, messages, store} =
+ let val (timeout_threads, timeout_heap') =
+ Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
+ in
+ if null timeout_threads andalso null canceling then
+ NONE
+ else
+ let
+ val _ = List.app (Simple_Thread.interrupt o #1) canceling
+ val canceling' = filter (Thread.isActive o #1) canceling
+ val state' = make_state manager timeout_heap' active canceling' messages store;
+ in SOME (map #2 timeout_threads, state') end
+ end;
+ in
+ while Synchronized.change_result global_state
+ (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
+ if null active andalso null canceling andalso null messages
+ then (false, make_state NONE timeout_heap active canceling messages store)
+ else (true, state))
+ do
+ (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
+ |> these
+ |> List.app (unregister verbose "Timed out.\n");
+ print_new_messages ();
+ (*give threads some time to respond to interrupt*)
+ OS.Process.sleep min_wait_time)
+ end))
+ in make_state manager timeout_heap active canceling messages store end)
+
+
+(* register thread *)
+
+fun register tool verbose birth_time death_time desc thread =
+ (Synchronized.change global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ let
+ val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
+ val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
+ val state' = make_state manager timeout_heap' active' canceling messages store;
+ in state' end);
+ check_thread_manager verbose);
+
+
+fun launch tool verbose birth_time death_time desc f =
+ (Toplevel.thread true
+ (fn () =>
+ let
+ val self = Thread.self ()
+ val _ = register tool verbose birth_time death_time desc self
+ val message = f ()
+ in unregister verbose message self end);
+ ())
+
+
+(** user commands **)
+
+(* kill threads *)
+
+fun kill_threads tool workers = Synchronized.change global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ let
+ val killing =
+ map_filter (fn (th, (tool', _, _, desc)) =>
+ if tool' = tool then SOME (th, (tool', Time.now (), desc))
+ else NONE) active
+ val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
+ val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
+ in state' end);
+
+
+(* running threads *)
+
+fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
+
+fun running_threads tool workers =
+ let
+ val {active, canceling, ...} = Synchronized.value global_state;
+
+ val now = Time.now ();
+ fun running_info (_, (tool', birth_time, death_time, desc)) =
+ if tool' = tool then
+ SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
+ seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
+ else
+ NONE
+ fun canceling_info (_, (tool', death_time, desc)) =
+ if tool' = tool then
+ SOME ("Trying to interrupt thread since " ^
+ seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
+ else
+ NONE
+ val running =
+ case map_filter running_info active of
+ [] => ["No " ^ workers ^ " running."]
+ | ss => "Running " ^ workers ^ ":" :: ss
+ val interrupting =
+ case map_filter canceling_info canceling of
+ [] => []
+ | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
+ in priority (space_implode "\n\n" (running @ interrupting)) end
+
+fun thread_messages tool worker opt_limit =
+ let
+ val limit = the_default message_display_limit opt_limit;
+ val tool_store = Synchronized.value global_state
+ |> #store |> filter (curry (op =) tool o fst)
+ val header =
+ "Recent " ^ worker ^ " messages" ^
+ (if length tool_store <= limit then ":"
+ else " (" ^ string_of_int limit ^ " displayed):");
+ in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
+
+end;
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 07:55:18 2010 +0200
@@ -8,8 +8,8 @@
signature ATP_MANAGER =
sig
- type name_pool = Sledgehammer_FOL_Clause.name_pool
- type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
+ type cnf_thm = Clausifier.cnf_thm
+ type name_pool = Metis_Clauses.name_pool
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
@@ -19,7 +19,6 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- respect_no_atp: bool,
relevance_threshold: real,
relevance_convergence: real,
theory_relevant: bool option,
@@ -57,19 +56,26 @@
val add_prover: string * prover -> theory -> theory
val get_prover: theory -> string -> prover
val available_atps: theory -> unit
- val start_prover_thread:
- params -> Time.time -> Time.time -> int -> int -> relevance_override
- -> (string -> minimize_command) -> Proof.state -> string -> unit
+ val start_prover_thread :
+ params -> int -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> string -> unit
end;
structure ATP_Manager : ATP_MANAGER =
struct
-open Sledgehammer_Util
+open Metis_Clauses
open Sledgehammer_Fact_Filter
-open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
+(** The Sledgehammer **)
+
+val das_Tool = "Sledgehammer"
+
+fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
+fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
+val messages = Async_Manager.thread_messages das_Tool "ATP"
+
(** problems, results, provers, etc. **)
type params =
@@ -79,7 +85,6 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- respect_no_atp: bool,
relevance_threshold: real,
relevance_convergence: real,
theory_relevant: bool option,
@@ -115,221 +120,24 @@
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
-
-(** preferences **)
-
-val message_store_limit = 20;
-val message_display_limit = 5;
-
-
-(** thread management **)
-
-(* data structures over threads *)
-
-structure Thread_Heap = Heap
-(
- type elem = Time.time * Thread.thread;
- fun ord ((a, _), (b, _)) = Time.compare (a, b);
-);
-
-fun lookup_thread xs = AList.lookup Thread.equal xs;
-fun delete_thread xs = AList.delete Thread.equal xs;
-fun update_thread xs = AList.update Thread.equal xs;
-
-
-(* state of thread manager *)
-
-type state =
- {manager: Thread.thread option,
- timeout_heap: Thread_Heap.T,
- active: (Thread.thread * (Time.time * Time.time * string)) list,
- cancelling: (Thread.thread * (Time.time * string)) list,
- messages: string list,
- store: string list};
-
-fun make_state manager timeout_heap active cancelling messages store : state =
- {manager = manager, timeout_heap = timeout_heap, active = active,
- cancelling = cancelling, messages = messages, store = store};
-
-val global_state = Synchronized.var "atp_manager"
- (make_state NONE Thread_Heap.empty [] [] [] []);
-
-
-(* unregister ATP thread *)
-
-fun unregister ({verbose, ...} : params) message thread =
- Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
- (case lookup_thread active thread of
- SOME (birth_time, _, desc) =>
- let
- val active' = delete_thread thread active;
- val now = Time.now ()
- val cancelling' = (thread, (now, desc)) :: cancelling;
- val message' =
- desc ^ "\n" ^ message ^
- (if verbose then
- "Total time: " ^ Int.toString (Time.toMilliseconds
- (Time.- (now, birth_time))) ^ " ms.\n"
- else
- "")
- val messages' = message' :: messages;
- val store' = message' ::
- (if length store <= message_store_limit then store
- else #1 (chop message_store_limit store));
- in make_state manager timeout_heap active' cancelling' messages' store' end
- | NONE => state));
-
-
-(* main manager thread -- only one may exist *)
-
-val min_wait_time = Time.fromMilliseconds 300;
-val max_wait_time = Time.fromSeconds 10;
-
-(* This is a workaround for Proof General's off-by-a-few sendback display bug,
- whereby "pr" in "proof" is not highlighted. *)
-val break_into_chunks =
- map (replace_all "\n\n" "\000") #> maps (space_explode "\000")
-
-fun print_new_messages () =
- case Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- (messages, make_state manager timeout_heap active cancelling []
- store)) of
- [] => ()
- | msgs =>
- msgs |> break_into_chunks
- |> (fn msg :: msgs => "Sledgehammer: " ^ msg :: msgs)
- |> List.app priority
-
-fun check_thread_manager params = Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
- if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
- else let val manager = SOME (Toplevel.thread false (fn () =>
- let
- fun time_limit timeout_heap =
- (case try Thread_Heap.min timeout_heap of
- NONE => Time.+ (Time.now (), max_wait_time)
- | SOME (time, _) => time);
-
- (*action: find threads whose timeout is reached, and interrupt cancelling threads*)
- fun action {manager, timeout_heap, active, cancelling, messages, store} =
- let val (timeout_threads, timeout_heap') =
- Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
- in
- if null timeout_threads andalso null cancelling
- then NONE
- else
- let
- val _ = List.app (Simple_Thread.interrupt o #1) cancelling;
- val cancelling' = filter (Thread.isActive o #1) cancelling;
- val state' = make_state manager timeout_heap' active cancelling' messages store;
- in SOME (map #2 timeout_threads, state') end
- end;
- in
- while Synchronized.change_result global_state
- (fn state as {timeout_heap, active, cancelling, messages, store, ...} =>
- if null active andalso null cancelling andalso null messages
- then (false, make_state NONE timeout_heap active cancelling messages store)
- else (true, state))
- do
- (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
- |> these
- |> List.app (unregister params "Timed out.\n");
- print_new_messages ();
- (*give threads some time to respond to interrupt*)
- OS.Process.sleep min_wait_time)
- end))
- in make_state manager timeout_heap active cancelling messages store end);
-
-
-(* register ATP thread *)
-
-fun register params birth_time death_time (thread, desc) =
- (Synchronized.change global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- let
- val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
- val active' = update_thread (thread, (birth_time, death_time, desc)) active;
- val state' = make_state manager timeout_heap' active' cancelling messages store;
- in state' end);
- check_thread_manager params);
-
-
-
-(** user commands **)
-
-(* kill ATPs *)
-
-fun kill_atps () = Synchronized.change global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- let
- val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
- val state' = make_state manager timeout_heap [] (killing @ cancelling) messages store;
- val _ = if null active then ()
- else priority "Killed active Sledgehammer threads."
- in state' end);
-
-
-(* running_atps *)
-
-fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
-
-fun running_atps () =
- let
- val {active, cancelling, ...} = Synchronized.value global_state;
-
- val now = Time.now ();
- fun running_info (_, (birth_time, death_time, desc)) =
- "Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
- seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc;
- fun cancelling_info (_, (deadth_time, desc)) =
- "Trying to interrupt thread since " ^ seconds (Time.- (now, deadth_time)) ^ ":\n" ^ desc;
-
- val running =
- if null active then "No ATPs running."
- else space_implode "\n\n" ("Running ATPs:" :: map running_info active);
- val interrupting =
- if null cancelling then ""
- else
- space_implode "\n\n"
- ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling);
-
- in priority (running ^ "\n" ^ interrupting) end;
-
-fun messages opt_limit =
- let
- val limit = the_default message_display_limit opt_limit;
- val {store, ...} = Synchronized.value global_state;
- val header =
- "Recent ATP messages" ^
- (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
- in List.app priority (header :: break_into_chunks (#1 (chop limit store))) end
-
-
-(** The Sledgehammer **)
-
(* named provers *)
-fun err_dup_prover name = error ("Duplicate prover: " ^ quote name ^ ".");
-
structure Data = Theory_Data
(
type T = (prover * stamp) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (eq_snd op =) data
- handle Symtab.DUP name => err_dup_prover name;
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
);
fun add_prover (name, prover) thy =
Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
- handle Symtab.DUP name => err_dup_prover name;
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
fun get_prover thy name =
- case Symtab.lookup (Data.get thy) name of
- SOME (prover, _) => prover
- | NONE => error ("Unknown ATP: " ^ name)
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
fun available_atps thy =
priority ("Available ATPs: " ^
@@ -338,28 +146,29 @@
(* start prover thread *)
-fun start_prover_thread (params as {full_types, timeout, ...}) birth_time
- death_time i n relevance_override minimize_command
- proof_state name =
+fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
+ relevance_override minimize_command proof_state name =
let
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
val prover = get_prover (Proof.theory_of proof_state) name
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
"ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
- val _ = Toplevel.thread true (fn () =>
- let
- val _ = register params birth_time death_time (Thread.self (), desc)
- val problem =
- {subgoal = i, goal = (ctxt, (facts, goal)),
- relevance_override = relevance_override, axiom_clauses = NONE,
- filtered_clauses = NONE}
- val message =
- #message (prover params (minimize_command name) timeout problem)
- handle TRIVIAL () => metis_line full_types i n []
- | ERROR message => "Error: " ^ message ^ "\n"
- val _ = unregister params message (Thread.self ());
- in () end)
- in () end
+ in
+ Async_Manager.launch das_Tool verbose birth_time death_time desc
+ (fn () =>
+ let
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ in
+ prover params (minimize_command name) timeout problem |> #message
+ handle TRIVIAL () => metis_line full_types i n []
+ | ERROR message => "Error: " ^ message ^ "\n"
+ end)
+ end
end;
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 07:55:18 2010 +0200
@@ -22,12 +22,12 @@
structure ATP_Systems : ATP_SYSTEMS =
struct
+open Clausifier
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
+open Sledgehammer_TPTP_Format
open Sledgehammer_Proof_Reconstruct
-open Sledgehammer_TPTP_Format
open ATP_Manager
(** generic ATP **)
@@ -126,9 +126,9 @@
fun generic_tptp_prover
(name, {home_var, executable, arguments, proof_delims, known_failures,
max_axiom_clauses, prefers_theory_relevant})
- ({debug, overlord, full_types, explicit_apply, respect_no_atp,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor, ...} : params)
+ ({debug, overlord, full_types, explicit_apply, relevance_threshold,
+ relevance_convergence, theory_relevant, defs_relevant, isar_proof,
+ isar_shrink_factor, ...} : params)
minimize_command timeout
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
@@ -140,7 +140,7 @@
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
(case filtered_clauses of
- NONE => relevant_facts full_types respect_no_atp relevance_threshold
+ NONE => relevant_facts full_types relevance_threshold
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
@@ -223,7 +223,7 @@
val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
val result =
do_run false
- |> (fn (_, msecs0, _, SOME IncompleteUnprovable) =>
+ |> (fn (_, msecs0, _, SOME _) =>
do_run true
|> (fn (output, msecs, proof, outcome) =>
(output, msecs0 + msecs, proof, outcome))
@@ -298,9 +298,11 @@
val spass_config : prover_config =
{home_var = "SPASS_HOME",
executable = "SPASS",
+ (* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
+ \-VarWeight=3 -TimeLimit=" ^
+ string_of_int (to_generous_secs timeout div 2))
|> not complete ? prefix "-SOS=1 ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 29 07:55:18 2010 +0200
@@ -2080,7 +2080,7 @@
list_abs (outer,
Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
$ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
- $ (Const (@{const_name split}, curried_T --> uncurried_T)
+ $ (Const (@{const_name prod_case}, curried_T --> uncurried_T)
$ list_comb (Const step_x, outer_bounds)))
$ list_comb (Const base_x, outer_bounds)
|> ap_curry tuple_arg_Ts tuple_T)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Jun 29 07:55:18 2010 +0200
@@ -2015,7 +2015,7 @@
| split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
| split_lambda t _ = raise (TERM ("split_lambda", [t]))
-fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t
+fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
@@ -2535,8 +2535,8 @@
THEN (rtac pred_intro_rule
(* How to handle equality correctly? *)
THEN_ALL_NEW (K (print_tac options "state before assumption matching")
- THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i)
- THEN print_tac options "state after pre-simplification:")))
+ THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
+ THEN' (K (print_tac options "state after pre-simplification:"))
THEN' (K (print_tac options "state after assumption matching:")))) 1)
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Jun 29 07:55:18 2010 +0200
@@ -179,7 +179,7 @@
|> maps (fn (res, (names, prems)) =>
flatten' (betapply (g, res)) (names, prems))
end)
- | Const (@{const_name split}, _) =>
+ | Const (@{const_name prod_case}, _) =>
(let
val (_, g :: res :: args) = strip_comb t
val [res1, res2] = Name.variant_list names ["res1", "res2"]
--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Jun 29 07:55:18 2010 +0200
@@ -12,7 +12,7 @@
val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
local_theory -> Quotient_Info.qconsts_info * local_theory
- val lift_raw_const: typ list -> string * term -> local_theory ->
+ val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
Quotient_Info.qconsts_info * local_theory
end;
@@ -50,6 +50,7 @@
let
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+ val _ = if is_Const rhs then () else warning "The definiens is not a constant"
fun sanity_test NONE _ = true
| sanity_test (SOME bind) str =
@@ -88,13 +89,13 @@
end
(* a wrapper for automatically lifting a raw constant *)
-fun lift_raw_const qtys (qconst_name, rconst) ctxt =
+fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
let
val rty = fastype_of rconst
val qty = derive_qtyp qtys rty ctxt
+ val lhs = Free (qconst_name, qty)
in
- quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
- (Free (qconst_name, qty), rconst))) ctxt
+ quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
end
(* parser and command *)
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Jun 29 07:55:18 2010 +0200
@@ -11,10 +11,13 @@
val injection_tac: Proof.context -> int -> tactic
val all_injection_tac: Proof.context -> int -> tactic
val clean_tac: Proof.context -> int -> tactic
- val procedure_tac: Proof.context -> thm -> int -> tactic
+
+ val descend_procedure_tac: Proof.context -> int -> tactic
+ val descend_tac: Proof.context -> int -> tactic
+
+ val lift_procedure_tac: Proof.context -> thm -> int -> tactic
val lift_tac: Proof.context -> thm list -> int -> tactic
- val quotient_tac: Proof.context -> int -> tactic
- val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
+
val lifted: typ list -> Proof.context -> thm -> thm
val lifted_attrib: attribute
end;
@@ -615,8 +618,39 @@
SOME (cterm_of thy inj_goal)] lifting_procedure_thm
end
+
+(** descending as tactic **)
+
+fun descend_procedure_tac ctxt =
+ Object_Logic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ THEN' SUBGOAL (fn (goal, i) =>
+ let
+ val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+ val rtrm = derive_rtrm qtys goal ctxt
+ val rule = procedure_inst ctxt rtrm goal
+ in
+ rtac rule i
+ end)
+
+fun descend_tac ctxt =
+let
+ val mk_tac_raw =
+ descend_procedure_tac ctxt
+ THEN' RANGE
+ [Object_Logic.rulify_tac THEN' (K all_tac),
+ regularize_tac ctxt,
+ all_injection_tac ctxt,
+ clean_tac ctxt]
+in
+ Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
+end
+
+
+(** lifting as tactic **)
+
(* the tactic leaves three subgoals to be proved *)
-fun procedure_tac ctxt rthm =
+fun lift_procedure_tac ctxt rthm =
Object_Logic.full_atomize_tac
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
@@ -627,35 +661,39 @@
(rtac rule THEN' rtac rthm') i
end)
-
-(* Automatic Proofs *)
-
fun lift_tac ctxt rthms =
let
fun mk_tac rthm =
- procedure_tac ctxt rthm
+ lift_procedure_tac ctxt rthm
THEN' RANGE
- [regularize_tac ctxt,
- all_injection_tac ctxt,
- clean_tac ctxt]
+ [ regularize_tac ctxt,
+ all_injection_tac ctxt,
+ clean_tac ctxt ]
in
- simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
- THEN' RANGE (map mk_tac rthms)
+ Goal.conjunction_tac THEN' RANGE (map mk_tac rthms)
end
+
+(** lifting as attribute **)
+
fun lifted qtys ctxt thm =
let
(* When the theorem is atomized, eta redexes are contracted,
so we do it both in the original theorem *)
val thm' = Drule.eta_contraction_rule thm
val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
- val goal = (quotient_lift_all qtys ctxt' o prop_of) thm''
+ val goal = derive_qtrm qtys (prop_of thm'') ctxt'
in
Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
|> singleton (ProofContext.export ctxt' ctxt)
end;
-(* An Attribute which automatically constructs the qthm *)
-val lifted_attrib = Thm.rule_attribute (fn ctxt => lifted [] (Context.proof_of ctxt))
+val lifted_attrib = Thm.rule_attribute (fn context =>
+ let
+ val ctxt = Context.proof_of context
+ val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+ in
+ lifted qtys ctxt
+ end)
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Tue Jun 29 07:55:18 2010 +0200
@@ -27,7 +27,9 @@
val inj_repabs_trm_chk: Proof.context -> term * term -> term
val derive_qtyp: typ list -> typ -> Proof.context -> typ
- val quotient_lift_all: typ list -> Proof.context -> term -> term
+ val derive_qtrm: typ list -> term -> Proof.context -> term
+ val derive_rtyp: typ list -> typ -> Proof.context -> typ
+ val derive_rtrm: typ list -> term -> Proof.context -> term
end;
structure Quotient_Term: QUOTIENT_TERM =
@@ -560,12 +562,12 @@
end
end
- | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
- ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
+ | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+ ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
- | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)),
- ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) =>
+ | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
+ ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
| (t1 $ t2, t1' $ t2') =>
@@ -690,96 +692,95 @@
(*** Wrapper for automatically transforming an rthm into a qthm ***)
-(* subst_tys takes a list of (rty, qty) substitution pairs
- and replaces all occurences of rty in the given type
- by appropriate qty, with substitution *)
-fun subst_ty thy ty (rty, qty) r =
- if r <> NONE then r else
- case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
- SOME inst => SOME (Envir.subst_type inst qty)
- | NONE => NONE
-fun subst_tys thy substs ty =
- case fold (subst_ty thy ty) substs NONE of
- SOME ty => ty
- | NONE =>
- (case ty of
- Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
- | x => x)
+(* substitutions functions for r/q-types and
+ r/q-constants, respectively
+*)
+fun subst_typ ctxt ty_subst rty =
+ case rty of
+ Type (s, rtys) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
+
+ fun matches [] = rty'
+ | matches ((rty, qty)::tail) =
+ case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
+ NONE => matches tail
+ | SOME inst => Envir.subst_type inst qty
+ in
+ matches ty_subst
+ end
+ | _ => rty
+
+fun subst_trm ctxt ty_subst trm_subst rtrm =
+ case rtrm of
+ t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2)
+ | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t)
+ | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
+ | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
+ | Bound i => Bound i
+ | Const (a, ty) =>
+ let
+ val thy = ProofContext.theory_of ctxt
-(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
- and if the given term matches any of the raw terms it
- returns the appropriate qtrm instantiated. If none of
- them matched it returns NONE. *)
-fun subst_trm thy t (rtrm, qtrm) s =
- if s <> NONE then s else
- case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
- SOME inst => SOME (Envir.subst_term inst qtrm)
- | NONE => NONE;
-fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
+ fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
+ | matches ((rconst, qconst)::tail) =
+ case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
+ NONE => matches tail
+ | SOME inst => Envir.subst_term inst qconst
+ in
+ matches trm_subst
+ end
-(* prepares type and term substitution pairs to be used by above
- functions that let replace all raw constructs by appropriate
- lifted counterparts. *)
-fun get_ty_trm_substs qtys ctxt =
+(* generate type and term substitutions out of the
+ qtypes involved in a quotient; the direction flag
+ indicates in which direction the substitution work:
+
+ true: quotient -> raw
+ false: raw -> quotient
+*)
+fun mk_ty_subst qtys direction ctxt =
+ Quotient_Info.quotdata_dest ctxt
+ |> map (fn x => (#rtyp x, #qtyp x))
+ |> filter (fn (_, qty) => member (op =) qtys qty)
+ |> map (if direction then swap else I)
+
+fun mk_trm_subst qtys direction ctxt =
let
- val thy = ProofContext.theory_of ctxt
- val quot_infos = Quotient_Info.quotdata_dest ctxt
- val const_infos = Quotient_Info.qconsts_dest ctxt
- val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
- val ty_substs =
- if qtys = [] then all_ty_substs else
- filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs
- val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
- fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
- val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
- fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt)
- val all_trm_substs = const_substs @ rel_substs
+ val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
+ fun proper (t1, t2) = (subst_typ' (fastype_of t1) = fastype_of t2)
+
+ val const_substs =
+ Quotient_Info.qconsts_dest ctxt
+ |> map (fn x => (#rconst x, #qconst x))
+ |> map (if direction then swap else I)
+
+ val rel_substs =
+ Quotient_Info.quotdata_dest ctxt
+ |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
+ |> map (if direction then swap else I)
in
- (ty_substs, filter valid_trm_subst all_trm_substs)
+ filter proper (const_substs @ rel_substs)
end
-fun derive_qtyp qtys rty ctxt =
-let
- val thy = ProofContext.theory_of ctxt
- val (ty_substs, _) = get_ty_trm_substs qtys ctxt
-in
- subst_tys thy ty_substs rty
-end
-(*
-Takes a term and
-
-* replaces raw constants by the quotient constants
+(* derives a qtyp and qtrm out of a rtyp and rtrm,
+ respectively
+*)
+fun derive_qtyp qtys rty ctxt =
+ subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
-* replaces equivalence relations by equalities
-
-* replaces raw types by the quotient types
-
-*)
+fun derive_qtrm qtys rtrm ctxt =
+ subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
-fun quotient_lift_all qtys ctxt t =
-let
- val thy = ProofContext.theory_of ctxt
- val (ty_substs, substs) = get_ty_trm_substs qtys ctxt
- fun lift_aux t =
- case subst_trms thy substs t of
- SOME x => x
- | NONE =>
- (case t of
- a $ b => lift_aux a $ lift_aux b
- | Abs(a, ty, s) =>
- let
- val (y, s') = Term.dest_abs (a, ty, s)
- val nty = subst_tys thy ty_substs ty
- in
- Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
- end
- | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
- | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
- | Bound i => Bound i
- | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
-in
- lift_aux t
-end
+(* derives a rtyp and rtrm out of a qtyp and qtrm,
+ respectively
+*)
+fun derive_rtyp qtys qty ctxt =
+ subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
+
+fun derive_rtrm qtys qtrm ctxt =
+ subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
+
end; (* structure *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jun 29 07:55:18 2010 +0200
@@ -0,0 +1,571 @@
+(* Title: HOL/Tools/Sledgehammer/clausifier.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+Transformation of axiom rules (elim/intro/etc) into CNF forms.
+*)
+
+signature CLAUSIFIER =
+sig
+ type cnf_thm = thm * ((string * int) * thm)
+
+ val sledgehammer_prefix: string
+ val chained_prefix: string
+ val trace: bool Unsynchronized.ref
+ val trace_msg: (unit -> string) -> unit
+ val name_thms_pair_from_ref :
+ Proof.context -> thm list -> Facts.ref -> string * thm list
+ val skolem_theory_name: string
+ val skolem_prefix: string
+ val skolem_infix: string
+ val is_skolem_const_name: string -> bool
+ val num_type_args: theory -> string -> int
+ val cnf_axiom: theory -> thm -> thm list
+ val multi_base_blacklist: string list
+ val is_theorem_bad_for_atps: thm -> bool
+ val type_has_topsort: typ -> bool
+ val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
+ val saturate_cache: theory -> theory option
+ val auto_saturate_cache: bool Unsynchronized.ref
+ val neg_clausify: thm -> thm list
+ val neg_conjecture_clauses:
+ Proof.context -> thm -> int -> thm list list * (string * typ) list
+ val setup: theory -> theory
+end;
+
+structure Clausifier : CLAUSIFIER =
+struct
+
+type cnf_thm = thm * ((string * int) * thm)
+
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+
+(* Used to label theorems chained into the goal. *)
+val chained_prefix = sledgehammer_prefix ^ "chained_"
+
+val trace = Unsynchronized.ref false;
+fun trace_msg msg = if !trace then tracing (msg ()) else ();
+
+fun name_thms_pair_from_ref ctxt chained_ths xref =
+ let
+ val ths = ProofContext.get_fact ctxt xref
+ val name = Facts.string_of_ref xref
+ |> forall (member Thm.eq_thm chained_ths) ths
+ ? prefix chained_prefix
+ in (name, ths) end
+
+val skolem_theory_name = sledgehammer_prefix ^ "Sko"
+val skolem_prefix = "sko_"
+val skolem_infix = "$"
+
+val type_has_topsort = Term.exists_subtype
+ (fn TFree (_, []) => true
+ | TVar (_, []) => true
+ | _ => false);
+
+
+(**** Transformation of Elimination Rules into First-Order Formulas****)
+
+val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
+val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
+
+(*Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate the
+ conclusion variable to False.*)
+fun transform_elim th =
+ case concl_of th of (*conclusion variable*)
+ @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
+ | v as Var(_, @{typ prop}) =>
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
+ | _ => th;
+
+(*To enforce single-threading*)
+exception Clausify_failure of theory;
+
+
+(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
+
+(*Keep the full complexity of the original name*)
+fun flatten_name s = space_implode "_X" (Long_Name.explode s);
+
+fun skolem_name thm_name j var_name =
+ skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
+ skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
+
+(* Hack: Could return false positives (e.g., a user happens to declare a
+ constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+ Long_Name.base_name
+ #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
+fun num_type_args thy s =
+ if String.isPrefix skolem_theory_name s then
+ s |> unprefix skolem_theory_name
+ |> space_explode skolem_infix |> hd
+ |> space_explode "_" |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+
+fun rhs_extra_types lhsT rhs =
+ let val lhs_vars = Term.add_tfreesT lhsT []
+ fun add_new_TFrees (TFree v) =
+ if member (op =) lhs_vars v then I else insert (op =) (TFree v)
+ | add_new_TFrees _ = I
+ val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
+ in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
+
+fun skolem_type_and_args bound_T body =
+ let
+ val args1 = OldTerm.term_frees body
+ val Ts1 = map type_of args1
+ val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
+ val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
+ in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
+
+(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
+ suggested prefix for the Skolem constants. *)
+fun declare_skolem_funs s th thy =
+ let
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
+ (axs, thy) =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val (cT, args) = skolem_type_and_args T body
+ val rhs = list_abs_free (map dest_Free args,
+ HOLogic.choice_const T $ body)
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val (c, thy) =
+ Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
+ val cdef = id ^ "_def"
+ val ((_, ax), thy) =
+ Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
+ val ax' = Drule.export_without_context ax
+ in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
+ | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
+ in dec_sko (subst_bound (Free (fname, T), p)) thx end
+ | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
+ | dec_sko _ thx = thx
+ in dec_sko (prop_of th) ([], thy) end
+
+fun mk_skolem_id t =
+ let val T = fastype_of t in
+ Const (@{const_name skolem_id}, T --> T) $ t
+ end
+
+fun quasi_beta_eta_contract (Abs (s, T, t')) =
+ Abs (s, T, quasi_beta_eta_contract t')
+ | quasi_beta_eta_contract t = Envir.beta_eta_contract t
+
+(*Traverse a theorem, accumulating Skolem function definitions.*)
+fun assume_skolem_funs s th =
+ let
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
+ val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
+ val Ts = map type_of args
+ val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val c = Free (id, cT) (* FIXME: needed? ### *)
+ (* Forms a lambda-abstraction over the formal parameters *)
+ val rhs =
+ list_abs_free (map dest_Free args,
+ HOLogic.choice_const T
+ $ quasi_beta_eta_contract body)
+ |> mk_skolem_id
+ val def = Logic.mk_equals (c, rhs)
+ val comb = list_comb (rhs, args)
+ in dec_sko (subst_bound (comb, p)) (def :: defs) end
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+ in dec_sko (subst_bound (Free(fname,T), p)) defs end
+ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
+ | dec_sko _ defs = defs
+ in dec_sko (prop_of th) [] end;
+
+
+(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
+
+(*Returns the vars of a theorem*)
+fun vars_of_thm th =
+ map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
+
+val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
+
+(* Removes the lambdas from an equation of the form t = (%x. u). *)
+fun extensionalize th =
+ case prop_of th of
+ _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+ $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+ | _ => th
+
+fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
+ | is_quasi_lambda_free (t1 $ t2) =
+ is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
+ | is_quasi_lambda_free (Abs _) = false
+ | is_quasi_lambda_free _ = true
+
+val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
+
+(*FIXME: requires more use of cterm constructors*)
+fun abstract ct =
+ let
+ val thy = theory_of_cterm ct
+ val Abs(x,_,body) = term_of ct
+ val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
+ val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
+ fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
+ in
+ case body of
+ Const _ => makeK()
+ | Free _ => makeK()
+ | Var _ => makeK() (*though Var isn't expected*)
+ | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
+ | rator$rand =>
+ if loose_bvar1 (rator,0) then (*C or S*)
+ if loose_bvar1 (rand,0) then (*S*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val crand = cterm_of thy (Abs(x,xT,rand))
+ val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
+ in
+ Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
+ end
+ else (*C*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
+ in
+ Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
+ end
+ else if loose_bvar1 (rand,0) then (*B or eta*)
+ if rand = Bound 0 then Thm.eta_conversion ct
+ else (*B*)
+ let val crand = cterm_of thy (Abs(x,xT,rand))
+ val crator = cterm_of thy rator
+ val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
+ in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
+ else makeK()
+ | _ => raise Fail "abstract: Bad term"
+ end;
+
+(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
+fun do_introduce_combinators ct =
+ if is_quasi_lambda_free (term_of ct) then
+ Thm.reflexive ct
+ else case term_of ct of
+ Abs _ =>
+ let
+ val (cv, cta) = Thm.dest_abs NONE ct
+ val (v, _) = dest_Free (term_of cv)
+ val u_th = do_introduce_combinators cta
+ val cu = Thm.rhs_of u_th
+ val comb_eq = abstract (Thm.cabs cv cu)
+ in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
+ | _ $ _ =>
+ let val (ct1, ct2) = Thm.dest_comb ct in
+ Thm.combination (do_introduce_combinators ct1)
+ (do_introduce_combinators ct2)
+ end
+
+fun introduce_combinators th =
+ if is_quasi_lambda_free (prop_of th) then
+ th
+ else
+ let
+ val th = Drule.eta_contraction_rule th
+ val eqth = do_introduce_combinators (cprop_of th)
+ in Thm.equal_elim eqth th end
+ handle THM (msg, _, _) =>
+ (warning ("Error in the combinator translation of " ^
+ Display.string_of_thm_without_context th ^
+ "\nException message: " ^ msg ^ ".");
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ TrueI)
+
+(*cterms are used throughout for efficiency*)
+val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
+
+(*cterm version of mk_cTrueprop*)
+fun c_mkTrueprop A = Thm.capply cTrueprop A;
+
+(*Given an abstraction over n variables, replace the bound variables by free
+ ones. Return the body, along with the list of free variables.*)
+fun c_variant_abs_multi (ct0, vars) =
+ let val (cv,ct) = Thm.dest_abs NONE ct0
+ in c_variant_abs_multi (ct, cv::vars) end
+ handle CTERM _ => (ct0, rev vars);
+
+(*Given the definition of a Skolem function, return a theorem to replace
+ an existential formula by a use of that function.
+ Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
+fun skolem_theorem_of_def inline def =
+ let
+ val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of
+ |> Thm.dest_equals
+ val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
+ val (ch, frees) = c_variant_abs_multi (rhs', [])
+ val (chilbert, cabs) = ch |> Thm.dest_comb
+ val thy = Thm.theory_of_cterm chilbert
+ val t = Thm.term_of chilbert
+ val T =
+ case t of
+ Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
+ val cex = Thm.cterm_of thy (HOLogic.exists_const T)
+ val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
+ and conc =
+ Drule.list_comb (if inline then rhs else c, frees)
+ |> Drule.beta_conv cabs |> c_mkTrueprop
+ fun tacf [prem] =
+ (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
+ else rewrite_goals_tac [def])
+ THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
+ RS @{thm someI_ex}) 1
+ in Goal.prove_internal [ex_tm] conc tacf
+ |> forall_intr_list frees
+ |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
+ |> Thm.varifyT_global
+ end;
+
+
+(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
+fun to_nnf th ctxt0 =
+ let val th1 = th |> transform_elim |> zero_var_indexes
+ val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize
+ |> Meson.make_nnf ctxt
+ in (th3, ctxt) end;
+
+(*Generate Skolem functions for a theorem supplied in nnf*)
+fun skolem_theorems_of_assume s th =
+ map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th))
+ (assume_skolem_funs s th)
+
+
+(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
+
+val max_lambda_nesting = 3
+
+fun term_has_too_many_lambdas max (t1 $ t2) =
+ exists (term_has_too_many_lambdas max) [t1, t2]
+ | term_has_too_many_lambdas max (Abs (_, _, t)) =
+ max = 0 orelse term_has_too_many_lambdas (max - 1) t
+ | term_has_too_many_lambdas _ _ = false
+
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
+
+(* Don't count nested lambdas at the level of formulas, since they are
+ quantifiers. *)
+fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
+ formula_has_too_many_lambdas (T :: Ts) t
+ | formula_has_too_many_lambdas Ts t =
+ if is_formula_type (fastype_of1 (Ts, t)) then
+ exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
+ else
+ term_has_too_many_lambdas max_lambda_nesting t
+
+(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
+ was 11. *)
+val max_apply_depth = 15
+
+fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
+ | apply_depth (Abs (_, _, t)) = apply_depth t
+ | apply_depth _ = 0
+
+fun is_formula_too_complex t =
+ apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
+ formula_has_too_many_lambdas [] t
+
+fun is_strange_thm th =
+ case head_of (concl_of th) of
+ Const (a, _) => (a <> @{const_name Trueprop} andalso
+ a <> @{const_name "=="})
+ | _ => false;
+
+fun is_theorem_bad_for_atps thm =
+ let val t = prop_of thm in
+ is_formula_too_complex t orelse exists_type type_has_topsort t orelse
+ is_strange_thm thm
+ end
+
+(* FIXME: put other record thms here, or declare as "no_atp" *)
+val multi_base_blacklist =
+ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+ "split_asm", "cases", "ext_cases"];
+
+fun fake_name th =
+ if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
+ else gensym "unknown_thm_";
+
+(*Skolemize a named theorem, with Skolem functions as additional premises.*)
+fun skolemize_theorem s th =
+ if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
+ is_theorem_bad_for_atps th then
+ []
+ else
+ let
+ val ctxt0 = Variable.global_thm_context th
+ val (nnfth, ctxt) = to_nnf th ctxt0
+ val defs = skolem_theorems_of_assume s nnfth
+ val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
+ in
+ cnfs |> map introduce_combinators
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ end
+ handle THM _ => []
+
+(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
+ Skolem functions.*)
+structure ThmCache = Theory_Data
+(
+ type T = thm list Thmtab.table * unit Symtab.table;
+ val empty = (Thmtab.empty, Symtab.empty);
+ val extend = I;
+ fun merge ((cache1, seen1), (cache2, seen2)) : T =
+ (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
+);
+
+val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
+val already_seen = Symtab.defined o #2 o ThmCache.get;
+
+val update_cache = ThmCache.map o apfst o Thmtab.update;
+fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
+
+(* Convert Isabelle theorems into axiom clauses. *)
+fun cnf_axiom thy th0 =
+ let val th = Thm.transfer thy th0 in
+ case lookup_cache thy th of
+ SOME cls => cls
+ | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
+ end;
+
+
+(**** Translate a set of theorems into CNF ****)
+
+(*The combination of rev and tail recursion preserves the original order*)
+fun cnf_rules_pairs thy =
+ let
+ fun do_one _ [] = []
+ | do_one ((name, k), th) (cls :: clss) =
+ (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
+ fun do_all pairs [] = pairs
+ | do_all pairs ((name, th) :: ths) =
+ let
+ val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
+ handle THM _ => []
+ in do_all (new_pairs @ pairs) ths end
+ in do_all [] o rev end
+
+
+(**** Convert all facts of the theory into FOL or HOL clauses ****)
+
+local
+
+fun skolem_def (name, th) thy =
+ let val ctxt0 = Variable.global_thm_context th in
+ case try (to_nnf th) ctxt0 of
+ NONE => (NONE, thy)
+ | SOME (nnfth, ctxt) =>
+ let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
+ in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
+ end;
+
+fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
+ let
+ val (cnfs, ctxt) =
+ Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
+ val cnfs' = cnfs
+ |> map introduce_combinators
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation;
+ in (th, cnfs') end;
+
+in
+
+fun saturate_cache thy =
+ let
+ val facts = PureThy.facts_of thy;
+ val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
+ if Facts.is_concealed facts name orelse already_seen thy name then I
+ else cons (name, ths));
+ val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
+ if member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ I
+ else
+ fold_index (fn (i, th) =>
+ if is_theorem_bad_for_atps th orelse
+ is_some (lookup_cache thy th) then
+ I
+ else
+ cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
+ in
+ if null new_facts then
+ NONE
+ else
+ let
+ val (defs, thy') = thy
+ |> fold (mark_seen o #1) new_facts
+ |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
+ |>> map_filter I;
+ val cache_entries = Par_List.map skolem_cnfs defs;
+ in SOME (fold update_cache cache_entries thy') end
+ end;
+
+end;
+
+(* For emergency use where the Skolem cache causes problems. *)
+val auto_saturate_cache = Unsynchronized.ref true
+
+fun conditionally_saturate_cache thy =
+ if !auto_saturate_cache then saturate_cache thy else NONE
+
+
+(*** Converting a subgoal into negated conjecture clauses. ***)
+
+fun neg_skolemize_tac ctxt =
+ EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
+
+val neg_clausify =
+ single
+ #> Meson.make_clauses_unsorted
+ #> map introduce_combinators
+ #> Meson.finish_cnf
+
+fun neg_conjecture_clauses ctxt st0 n =
+ let
+ (* "Option" is thrown if the assumptions contain schematic variables. *)
+ val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
+ val ({params, prems, ...}, _) =
+ Subgoal.focus (Variable.set_body false ctxt) n st
+ in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
+
+
+(** setup **)
+
+val setup =
+ perhaps conditionally_saturate_cache
+ #> Theory.at_end conditionally_saturate_cache
+
+end;
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jun 29 07:55:18 2010 +0200
@@ -14,11 +14,9 @@
structure Meson_Tactic : MESON_TACTIC =
struct
-open Sledgehammer_Fact_Preprocessor
-
(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
- String.isPrefix skolem_prefix a
+ String.isPrefix Clausifier.skolem_prefix a
| is_absko _ = false;
fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*)
@@ -43,7 +41,10 @@
let
val thy = ProofContext.theory_of ctxt
val ctxt0 = Classical.put_claset HOL_cs ctxt
- in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
+ in
+ (Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) i
+ THEN expand_defs_tac st0) st0
+ end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 07:55:18 2010 +0200
@@ -0,0 +1,685 @@
+(* Title: HOL/Tools/Sledgehammer/metis_clauses.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+Storing/printing FOL clauses and arity clauses. Typed equality is
+treated differently.
+*)
+
+signature METIS_CLAUSES =
+sig
+ type cnf_thm = Clausifier.cnf_thm
+ type name = string * string
+ type name_pool = string Symtab.table * string Symtab.table
+ datatype kind = Axiom | Conjecture
+ datatype type_literal =
+ TyLitVar of string * name |
+ TyLitFree of string * name
+ datatype arLit =
+ TConsLit of class * string * string list
+ | TVarLit of class * string
+ datatype arity_clause = ArityClause of
+ {axiom_name: string, conclLit: arLit, premLits: arLit list}
+ datatype classrel_clause = ClassrelClause of
+ {axiom_name: string, subclass: class, superclass: class}
+ datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
+ datatype combterm =
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
+ CombApp of combterm * combterm
+ datatype literal = Literal of bool * combterm
+ datatype hol_clause =
+ HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: literal list, ctypes_sorts: typ list}
+ exception TRIVIAL of unit
+
+ val type_wrapper_name : string
+ val schematic_var_prefix: string
+ val fixed_var_prefix: string
+ val tvar_prefix: string
+ val tfree_prefix: string
+ val const_prefix: string
+ val tconst_prefix: string
+ val class_prefix: string
+ val union_all: ''a list list -> ''a list
+ val invert_const: string -> string
+ val ascii_of: string -> string
+ val undo_ascii_of: string -> string
+ val strip_prefix: string -> string -> string option
+ val make_schematic_var : string * int -> string
+ val make_fixed_var : string -> string
+ val make_schematic_type_var : string * int -> string
+ val make_fixed_type_var : string -> string
+ val make_fixed_const : string -> string
+ val make_fixed_type_const : string -> string
+ val make_type_class : string -> string
+ val empty_name_pool : bool -> name_pool option
+ val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
+ val nice_name : name -> name_pool option -> string * name_pool option
+ val type_literals_for_types : typ list -> type_literal list
+ val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
+ val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
+ val type_of_combterm : combterm -> combtyp
+ val strip_combterm_comb : combterm -> combterm * combterm list
+ val literals_of_term : theory -> term -> literal list * typ list
+ val conceal_skolem_somes :
+ int -> (string * term) list -> term -> (string * term) list * term
+ val is_quasi_fol_theorem : theory -> thm -> bool
+ val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
+ val tfree_classes_of_terms : term list -> string list
+ val tvar_classes_of_terms : term list -> string list
+ val type_consts_of_terms : theory -> term list -> string list
+ val prepare_clauses :
+ bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
+ -> string vector
+ * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
+ * classrel_clause list * arity_clause list)
+end
+
+structure Metis_Clauses : METIS_CLAUSES =
+struct
+
+open Clausifier
+
+val type_wrapper_name = "ti"
+
+val schematic_var_prefix = "V_";
+val fixed_var_prefix = "v_";
+
+val tvar_prefix = "T_";
+val tfree_prefix = "t_";
+
+val classrel_clause_prefix = "clsrel_";
+
+val const_prefix = "c_";
+val tconst_prefix = "tc_";
+val class_prefix = "class_";
+
+fun union_all xss = fold (union (op =)) xss []
+
+(* Readable names for the more common symbolic functions. Do not mess with the
+ last nine entries of the table unless you know what you are doing. *)
+val const_trans_table =
+ Symtab.make [(@{const_name "op ="}, "equal"),
+ (@{const_name "op &"}, "and"),
+ (@{const_name "op |"}, "or"),
+ (@{const_name "op -->"}, "implies"),
+ (@{const_name "op :"}, "in"),
+ (@{const_name fequal}, "fequal"),
+ (@{const_name COMBI}, "COMBI"),
+ (@{const_name COMBK}, "COMBK"),
+ (@{const_name COMBB}, "COMBB"),
+ (@{const_name COMBC}, "COMBC"),
+ (@{const_name COMBS}, "COMBS"),
+ (@{const_name True}, "True"),
+ (@{const_name False}, "False"),
+ (@{const_name If}, "If"),
+ (@{type_name "*"}, "prod"),
+ (@{type_name "+"}, "sum")]
+
+(* Invert the table of translations between Isabelle and ATPs. *)
+val const_trans_table_inv =
+ Symtab.update ("fequal", @{const_name "op ="})
+ (Symtab.make (map swap (Symtab.dest const_trans_table)))
+
+val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
+
+(*Escaping of special characters.
+ Alphanumeric characters are left unchanged.
+ The character _ goes to __
+ Characters in the range ASCII space to / go to _A to _P, respectively.
+ Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
+val A_minus_space = Char.ord #"A" - Char.ord #" ";
+
+fun stringN_of_int 0 _ = ""
+ | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
+
+fun ascii_of_c c =
+ if Char.isAlphaNum c then String.str c
+ else if c = #"_" then "__"
+ else if #" " <= c andalso c <= #"/"
+ then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
+ else if Char.isPrint c
+ then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
+ else ""
+
+val ascii_of = String.translate ascii_of_c;
+
+(** Remove ASCII armouring from names in proof files **)
+
+(*We don't raise error exceptions because this code can run inside the watcher.
+ Also, the errors are "impossible" (hah!)*)
+fun undo_ascii_aux rcs [] = String.implode(rev rcs)
+ | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
+ (*Three types of _ escapes: __, _A to _P, _nnn*)
+ | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
+ | undo_ascii_aux rcs (#"_" :: c :: cs) =
+ if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
+ then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
+ else
+ let val digits = List.take (c::cs, 3) handle Subscript => []
+ in
+ case Int.fromString (String.implode digits) of
+ NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
+ | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
+ end
+ | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
+
+val undo_ascii_of = undo_ascii_aux [] o String.explode;
+
+(* If string s has the prefix s1, return the result of deleting it,
+ un-ASCII'd. *)
+fun strip_prefix s1 s =
+ if String.isPrefix s1 s then
+ SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
+ else
+ NONE
+
+(*Remove the initial ' character from a type variable, if it is present*)
+fun trim_type_var s =
+ if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
+ else error ("trim_type: Malformed type variable encountered: " ^ s);
+
+fun ascii_of_indexname (v,0) = ascii_of v
+ | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
+
+fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
+fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
+
+fun make_schematic_type_var (x,i) =
+ tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
+fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
+
+fun lookup_const c =
+ case Symtab.lookup const_trans_table c of
+ SOME c' => c'
+ | NONE => ascii_of c
+
+(* "op =" MUST BE "equal" because it's built into ATPs. *)
+fun make_fixed_const @{const_name "op ="} = "equal"
+ | make_fixed_const c = const_prefix ^ lookup_const c
+
+fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
+
+fun make_type_class clas = class_prefix ^ ascii_of clas;
+
+
+(**** name pool ****)
+
+type name = string * string
+type name_pool = string Symtab.table * string Symtab.table
+
+fun empty_name_pool readable_names =
+ if readable_names then SOME (`I Symtab.empty) else NONE
+
+fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
+fun pool_map f xs =
+ pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+
+fun add_nice_name full_name nice_prefix j the_pool =
+ let
+ val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
+ in
+ case Symtab.lookup (snd the_pool) nice_name of
+ SOME full_name' =>
+ if full_name = full_name' then (nice_name, the_pool)
+ else add_nice_name full_name nice_prefix (j + 1) the_pool
+ | NONE =>
+ (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
+ Symtab.update_new (nice_name, full_name) (snd the_pool)))
+ end
+
+fun translate_first_char f s =
+ String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+
+fun readable_name full_name s =
+ let
+ val s = s |> Long_Name.base_name |> Name.desymbolize false
+ val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
+ val s' =
+ (s' |> rev
+ |> implode
+ |> String.translate
+ (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
+ else ""))
+ ^ replicate_string (String.size s - length s') "_"
+ val s' =
+ if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
+ else s'
+ (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
+ ("op &", "op |", etc.). *)
+ val s' = if s' = "equal" orelse s' = "op" then full_name else s'
+ in
+ case (Char.isLower (String.sub (full_name, 0)),
+ Char.isLower (String.sub (s', 0))) of
+ (true, false) => translate_first_char Char.toLower s'
+ | (false, true) => translate_first_char Char.toUpper s'
+ | _ => s'
+ end
+
+fun nice_name (full_name, _) NONE = (full_name, NONE)
+ | nice_name (full_name, desired_name) (SOME the_pool) =
+ case Symtab.lookup (fst the_pool) full_name of
+ SOME nice_name => (nice_name, SOME the_pool)
+ | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
+ the_pool
+ |> apsnd SOME
+
+(**** Definitions and functions for FOL clauses for TPTP format output ****)
+
+datatype kind = Axiom | Conjecture
+
+(**** Isabelle FOL clauses ****)
+
+(* The first component is the type class; the second is a TVar or TFree. *)
+datatype type_literal =
+ TyLitVar of string * name |
+ TyLitFree of string * name
+
+exception CLAUSE of string * term;
+
+(*Make literals for sorted type variables*)
+fun sorts_on_typs_aux (_, []) = []
+ | sorts_on_typs_aux ((x,i), s::ss) =
+ let val sorts = sorts_on_typs_aux ((x,i), ss)
+ in
+ if s = "HOL.type" then sorts
+ else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
+ else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
+ end;
+
+fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
+ | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
+
+(*Given a list of sorted type variables, return a list of type literals.*)
+fun type_literals_for_types Ts =
+ fold (union (op =)) (map sorts_on_typs Ts) []
+
+(** make axiom and conjecture clauses. **)
+
+(**** Isabelle arities ****)
+
+datatype arLit = TConsLit of class * string * string list
+ | TVarLit of class * string;
+
+datatype arity_clause =
+ ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+
+
+fun gen_TVars 0 = []
+ | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
+
+fun pack_sort(_,[]) = []
+ | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*)
+ | pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
+
+(*Arity of type constructor tcon :: (arg1,...,argN)res*)
+fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
+ let val tvars = gen_TVars (length args)
+ val tvars_srts = ListPair.zip (tvars,args)
+ in
+ ArityClause {axiom_name = axiom_name,
+ conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
+ premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
+ end;
+
+
+(**** Isabelle class relations ****)
+
+datatype classrel_clause =
+ ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
+
+(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
+fun class_pairs _ [] _ = []
+ | class_pairs thy subs supers =
+ let
+ val class_less = Sorts.class_less (Sign.classes_of thy)
+ fun add_super sub super = class_less (sub, super) ? cons (sub, super)
+ fun add_supers sub = fold (add_super sub) supers
+ in fold add_supers subs [] end
+
+fun make_classrel_clause (sub,super) =
+ ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
+ ascii_of super,
+ subclass = make_type_class sub,
+ superclass = make_type_class super};
+
+fun make_classrel_clauses thy subs supers =
+ map make_classrel_clause (class_pairs thy subs supers);
+
+
+(** Isabelle arities **)
+
+fun arity_clause _ _ (_, []) = []
+ | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
+ arity_clause seen n (tcons,ars)
+ | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
+ if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
+ arity_clause seen (n+1) (tcons,ars)
+ else
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
+ arity_clause (class::seen) n (tcons,ars)
+
+fun multi_arity_clause [] = []
+ | multi_arity_clause ((tcons, ars) :: tc_arlists) =
+ arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
+
+(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
+ provided its arguments have the corresponding sorts.*)
+fun type_class_pairs thy tycons classes =
+ let val alg = Sign.classes_of thy
+ fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
+ fun add_class tycon class =
+ cons (class, domain_sorts tycon class)
+ handle Sorts.CLASS_ERROR _ => I
+ fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
+ in map try_classes tycons end;
+
+(*Proving one (tycon, class) membership may require proving others, so iterate.*)
+fun iter_type_class_pairs _ _ [] = ([], [])
+ | iter_type_class_pairs thy tycons classes =
+ let val cpairs = type_class_pairs thy tycons classes
+ val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
+ |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
+ val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
+ in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
+
+fun make_arity_clauses thy tycons classes =
+ let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
+ in (classes', multi_arity_clause cpairs) end;
+
+datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
+
+datatype combterm =
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
+ CombApp of combterm * combterm
+
+datatype literal = Literal of bool * combterm
+
+datatype hol_clause =
+ HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: literal list, ctypes_sorts: typ list}
+
+(*********************************************************************)
+(* convert a clause with type Term.term to a clause with type clause *)
+(*********************************************************************)
+
+(*Result of a function type; no need to check that the argument type matches.*)
+fun result_type (TyConstr (_, [_, tp2])) = tp2
+ | result_type _ = raise Fail "non-function type"
+
+fun type_of_combterm (CombConst (_, tp, _)) = tp
+ | type_of_combterm (CombVar (_, tp)) = tp
+ | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
+
+(*gets the head of a combinator application, along with the list of arguments*)
+fun strip_combterm_comb u =
+ let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
+ | stripc x = x
+ in stripc(u,[]) end
+
+fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
+ (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
+ | isFalse _ = false;
+
+fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
+ (pol andalso c = "c_True") orelse
+ (not pol andalso c = "c_False")
+ | isTrue _ = false;
+
+fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
+
+fun type_of (Type (a, Ts)) =
+ let val (folTypes,ts) = types_of Ts in
+ (TyConstr (`make_fixed_type_const a, folTypes), ts)
+ end
+ | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+ | type_of (tp as TVar (x, _)) =
+ (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
+and types_of Ts =
+ let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
+ (folTyps, union_all ts)
+ end
+
+(* same as above, but no gathering of sort information *)
+fun simp_type_of (Type (a, Ts)) =
+ TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
+ | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+ | simp_type_of (TVar (x, _)) =
+ TyVar (make_schematic_type_var x, string_of_indexname x)
+
+(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
+fun combterm_of thy (Const (c, T)) =
+ let
+ val (tp, ts) = type_of T
+ val tvar_list =
+ (if String.isPrefix skolem_theory_name c then
+ [] |> Term.add_tvarsT T |> map TVar
+ else
+ (c, T) |> Sign.const_typargs thy)
+ |> map simp_type_of
+ val c' = CombConst (`make_fixed_const c, tp, tvar_list)
+ in (c',ts) end
+ | combterm_of _ (Free(v, T)) =
+ let val (tp,ts) = type_of T
+ val v' = CombConst (`make_fixed_var v, tp, [])
+ in (v',ts) end
+ | combterm_of _ (Var(v, T)) =
+ let val (tp,ts) = type_of T
+ val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
+ in (v',ts) end
+ | combterm_of thy (P $ Q) =
+ let val (P', tsP) = combterm_of thy P
+ val (Q', tsQ) = combterm_of thy Q
+ in (CombApp (P', Q'), union (op =) tsP tsQ) end
+ | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
+
+fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
+ | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
+
+fun literals_of_term1 args thy (@{const Trueprop} $ P) =
+ literals_of_term1 args thy P
+ | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
+ literals_of_term1 (literals_of_term1 args thy P) thy Q
+ | literals_of_term1 (lits, ts) thy P =
+ let val ((pred, ts'), pol) = predicate_of thy (P, true) in
+ (Literal (pol, pred) :: lits, union (op =) ts ts')
+ end
+val literals_of_term = literals_of_term1 ([], [])
+
+fun skolem_name i j num_T_args =
+ skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
+ skolem_infix ^ "g"
+
+fun conceal_skolem_somes i skolem_somes t =
+ if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
+ let
+ fun aux skolem_somes
+ (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
+ let
+ val (skolem_somes, s) =
+ if i = ~1 then
+ (skolem_somes, @{const_name undefined})
+ else case AList.find (op aconv) skolem_somes t of
+ s :: _ => (skolem_somes, s)
+ | [] =>
+ let
+ val s = skolem_theory_name ^ "." ^
+ skolem_name i (length skolem_somes)
+ (length (Term.add_tvarsT T []))
+ in ((s, t) :: skolem_somes, s) end
+ in (skolem_somes, Const (s, T)) end
+ | aux skolem_somes (t1 $ t2) =
+ let
+ val (skolem_somes, t1) = aux skolem_somes t1
+ val (skolem_somes, t2) = aux skolem_somes t2
+ in (skolem_somes, t1 $ t2) end
+ | aux skolem_somes (Abs (s, T, t')) =
+ let val (skolem_somes, t') = aux skolem_somes t' in
+ (skolem_somes, Abs (s, T, t'))
+ end
+ | aux skolem_somes t = (skolem_somes, t)
+ in aux skolem_somes t end
+ else
+ (skolem_somes, t)
+
+fun is_quasi_fol_theorem thy =
+ Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
+
+(* Trivial problem, which resolution cannot handle (empty clause) *)
+exception TRIVIAL of unit
+
+(* making axiom and conjecture clauses *)
+fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
+ let
+ val (skolem_somes, t) =
+ th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
+ val (lits, ctypes_sorts) = literals_of_term thy t
+ in
+ if forall isFalse lits then
+ raise TRIVIAL ()
+ else
+ (skolem_somes,
+ HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+ kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
+ end
+
+fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
+ let
+ val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
+ in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
+
+fun make_axiom_clauses thy clauses =
+ ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
+
+fun make_conjecture_clauses thy =
+ let
+ fun aux _ _ [] = []
+ | aux n skolem_somes (th :: ths) =
+ let
+ val (skolem_somes, cls) =
+ make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
+ in cls :: aux (n + 1) skolem_somes ths end
+ in aux 0 [] end
+
+(** Helper clauses **)
+
+fun count_combterm (CombConst ((c, _), _, _)) =
+ Symtab.map_entry c (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
+fun count_literal (Literal (_, t)) = count_combterm t
+fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+
+fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
+fun cnf_helper_thms thy raw =
+ map (`Thm.get_name_hint)
+ #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
+
+val optional_helpers =
+ [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
+ (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
+ (["c_COMBS"], (false, @{thms COMBS_def}))]
+val optional_typed_helpers =
+ [(["c_True", "c_False"], (true, @{thms True_or_False})),
+ (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+
+val init_counters =
+ Symtab.make (maps (maps (map (rpair 0) o fst))
+ [optional_helpers, optional_typed_helpers])
+
+fun get_helper_clauses thy is_FO full_types conjectures axcls =
+ let
+ val axclauses = map snd (make_axiom_clauses thy axcls)
+ val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
+ fun is_needed c = the (Symtab.lookup ct c) > 0
+ val cnfs =
+ (optional_helpers
+ |> full_types ? append optional_typed_helpers
+ |> maps (fn (ss, (raw, ths)) =>
+ if exists is_needed ss then cnf_helper_thms thy raw ths
+ else []))
+ @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
+ in map snd (make_axiom_clauses thy cnfs) end
+
+fun make_clause_table xs =
+ fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
+
+
+(***************************************************************)
+(* Type Classes Present in the Axiom or Conjecture Clauses *)
+(***************************************************************)
+
+fun set_insert (x, s) = Symtab.update (x, ()) s
+
+fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
+
+(*Remove this trivial type class*)
+fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
+
+fun tfree_classes_of_terms ts =
+ let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
+ in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+
+fun tvar_classes_of_terms ts =
+ let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
+ in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+
+(*fold type constructors*)
+fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
+ | fold_type_consts _ _ x = x;
+
+(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
+fun add_type_consts_in_term thy =
+ let
+ val const_typargs = Sign.const_typargs thy
+ fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
+ | aux (Abs (_, _, u)) = aux u
+ | aux (Const (@{const_name skolem_id}, _) $ _) = I
+ | aux (t $ u) = aux t #> aux u
+ | aux _ = I
+ in aux end
+
+fun type_consts_of_terms thy ts =
+ Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
+
+(* Remove existing axiom clauses from the conjecture clauses, as this can
+ dramatically boost an ATP's performance (for some reason). *)
+fun subtract_cls ax_clauses =
+ filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
+
+(* prepare for passing to writer,
+ create additional clauses based on the information from extra_cls *)
+fun prepare_clauses full_types goal_cls axcls extra_cls thy =
+ let
+ val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
+ val ccls = subtract_cls extra_cls goal_cls
+ val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
+ val ccltms = map prop_of ccls
+ and axtms = map (prop_of o #1) extra_cls
+ val subs = tfree_classes_of_terms ccltms
+ and supers = tvar_classes_of_terms axtms
+ and tycons = type_consts_of_terms thy (ccltms @ axtms)
+ (*TFrees in conjecture clauses; TVars in axiom clauses*)
+ val conjectures = make_conjecture_clauses thy ccls
+ val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
+ val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
+ val helper_clauses =
+ get_helper_clauses thy is_FO full_types conjectures extra_cls
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val classrel_clauses = make_classrel_clauses thy subs supers'
+ in
+ (Vector.fromList clnames,
+ (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 07:55:18 2010 +0200
@@ -18,13 +18,8 @@
structure Metis_Tactics : METIS_TACTICS =
struct
-open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
-open Sledgehammer_Proof_Reconstruct
-open Sledgehammer_Fact_Filter
-open Sledgehammer_TPTP_Format
+open Clausifier
+open Metis_Clauses
exception METIS of string * string
@@ -234,7 +229,7 @@
| NONE => make_tvar v)
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
(case strip_prefix tconst_prefix x of
- SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+ SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys)
| NONE =>
case strip_prefix tfree_prefix x of
SOME tf => mk_tfree ctxt tf
@@ -295,7 +290,7 @@
| NONE => (*Not a constant. Is it a type constructor?*)
case strip_prefix tconst_prefix a of
SOME b =>
- Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
case strip_prefix tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
@@ -446,13 +441,15 @@
of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
could then fail. See comment on mk_var.*)
fun resolve_inc_tyvars(tha,i,thb) =
- let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ let
+ val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
in
case distinct Thm.eq_thm ths of
[th] => th
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
- end;
+ end
+ handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
let
@@ -722,6 +719,7 @@
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
+
(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
@@ -735,7 +733,8 @@
val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
+ app (fn TyLitFree (s, (s', _)) =>
+ trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees)
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 29 07:55:18 2010 +0200
@@ -5,10 +5,7 @@
signature SLEDGEHAMMER_FACT_FILTER =
sig
- type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
- type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
- type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type hol_clause = Sledgehammer_HOL_Clause.hol_clause
+ type cnf_thm = Clausifier.cnf_thm
type relevance_override =
{add: Facts.ref list,
@@ -16,29 +13,18 @@
only: bool}
val use_natural_form : bool Unsynchronized.ref
- val name_thms_pair_from_ref :
- Proof.context -> thm list -> Facts.ref -> string * thm list
- val tvar_classes_of_terms : term list -> string list
- val tfree_classes_of_terms : term list -> string list
- val type_consts_of_terms : theory -> term list -> string list
- val is_quasi_fol_theorem : theory -> thm -> bool
val relevant_facts :
- bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
+ bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
- val prepare_clauses :
- bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
- -> string vector
- * (hol_clause list * hol_clause list * hol_clause list
- * hol_clause list * classrel_clause list * arity_clause list)
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
struct
-open Sledgehammer_FOL_Clause
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
+open Clausifier
+open Metis_Clauses
+val respect_no_atp = true
(* Experimental feature: Filter theorems in natural form or in CNF? *)
val use_natural_form = Unsynchronized.ref false
@@ -88,10 +74,11 @@
Symtab.map_default (c, [ctyps])
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
-val fresh_sko_prefix = "Sledgehammer.Skox."
+val fresh_prefix = "Sledgehammer.Fresh."
val flip = Option.map not
+val boring_natural_consts = [@{const_name If}]
(* Including equality in this list might be expected to stop rules like
subset_antisym from being chosen, but for some reason filtering works better
with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
@@ -113,12 +100,15 @@
| Free x => add_const_type_to_table (const_with_typ thy x)
| (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
| t1 $ t2 => do_term t1 #> do_term t2
- | Abs (_, _, t) => do_term t
+ | Abs (_, _, t) =>
+ (* Abstractions lead to combinators, so we add a penalty for them. *)
+ add_const_type_to_table (gensym fresh_prefix, [])
+ #> do_term t
| _ => I
fun do_quantifier sweet_pos pos body_t =
do_formula pos body_t
#> (if pos = SOME sweet_pos then I
- else add_const_type_to_table (gensym fresh_sko_prefix, []))
+ else add_const_type_to_table (gensym fresh_prefix, []))
and do_equality T t1 t2 =
fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
else do_term) [t1, t2]
@@ -148,7 +138,8 @@
in
Symtab.empty
|> (if !use_natural_form then
- fold (do_formula pos) ts
+ fold (Symtab.update o rpair []) boring_natural_consts
+ #> fold (do_formula pos) ts
else
fold (Symtab.update o rpair []) boring_cnf_consts
#> fold do_term ts)
@@ -275,13 +266,13 @@
| _ => false
end;
-type annotated_clause = cnf_thm * ((string * const_typ list) list)
+type annotated_cnf_thm = cnf_thm * ((string * const_typ list) list)
(*For a reverse sort, putting the largest values first.*)
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
(*Limit the number of new clauses, to prevent runaway acceptance.*)
-fun take_best max_new (newpairs : (annotated_clause * real) list) =
+fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) =
let val nnew = length newpairs
in
if nnew <= max_new then (map #1 newpairs, [])
@@ -361,9 +352,15 @@
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
val goal_const_tab = get_consts_typs thy (SOME true) goals
+ val relevance_threshold =
+ if !use_natural_form then 0.9 * relevance_threshold (* experimental *)
+ else relevance_threshold
val _ =
trace_msg (fn () => "Initial constants: " ^
- commas (Symtab.keys goal_const_tab))
+ commas (goal_const_tab
+ |> Symtab.dest
+ |> filter (curry (op <>) [] o snd)
+ |> map fst))
val relevant =
relevant_clauses ctxt relevance_convergence defs_relevant max_new
relevance_override const_tab relevance_threshold
@@ -381,10 +378,6 @@
(*** retrieve lemmas and filter them ***)
-(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
-
-fun setinsert (x,s) = Symtab.update (x,()) s;
-
(*Reject theorems with names like "List.filter.filter_list_def" or
"Accessible_Part.acc.defs", as these are definitions arising from packages.*)
fun is_package_def a =
@@ -395,21 +388,12 @@
String.isSuffix "_def" a orelse String.isSuffix "_defs" a
end;
-fun mk_clause_table xs =
- fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
-
-fun make_unique xs =
- Termtab.fold (cons o snd) (mk_clause_table xs) []
-
-(* Remove existing axiom clauses from the conjecture clauses, as this can
- dramatically boost an ATP's performance (for some reason). *)
-fun subtract_cls ax_clauses =
- filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
+fun make_unique xs = Termtab.fold (cons o snd) (make_clause_table xs) []
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
-fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
+fun all_name_thms_pairs ctxt chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
@@ -453,7 +437,7 @@
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
-fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
+fun name_thm_pairs ctxt respect_no_atp name_thms_pairs =
let
val (mults, singles) = List.partition is_multi name_thms_pairs
val ps = [] |> fold add_names singles |> fold add_names mults
@@ -464,64 +448,16 @@
Display.string_of_thm_without_context th); false)
| is_named _ = true
fun checked_name_thm_pairs respect_no_atp ctxt =
- name_thm_pairs respect_no_atp ctxt
+ name_thm_pairs ctxt respect_no_atp
#> tap (fn ps => trace_msg
(fn () => ("Considering " ^ Int.toString (length ps) ^
" theorems")))
#> filter is_named
-fun name_thms_pair_from_ref ctxt chained_ths xref =
- let
- val ths = ProofContext.get_fact ctxt xref
- val name = Facts.string_of_ref xref
- |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix
- in (name, ths) end
-
-
-(***************************************************************)
-(* Type Classes Present in the Axiom or Conjecture Clauses *)
-(***************************************************************)
-
-fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
-
-(*Remove this trivial type class*)
-fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
-
-fun tvar_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
-
-fun tfree_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
-
-(*fold type constructors*)
-fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
- | fold_type_consts _ _ x = x;
-
-(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
-fun add_type_consts_in_term thy =
- let
- val const_typargs = Sign.const_typargs thy
- fun aux (Const cT) = fold (fold_type_consts setinsert) (const_typargs cT)
- | aux (Abs (_, _, u)) = aux u
- | aux (Const (@{const_name skolem_id}, _) $ _) = I
- | aux (t $ u) = aux t #> aux u
- | aux _ = I
- in aux end
-
-fun type_consts_of_terms thy ts =
- Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
-
-
(***************************************************************)
(* ATP invocation methods setup *)
(***************************************************************)
-fun is_quasi_fol_theorem thy =
- Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
-
(**** Predicates to detect unwanted clauses (prolific or likely to cause
unsoundness) ****)
@@ -570,22 +506,19 @@
(has_typed_var dangerous_types t orelse
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
-fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
-
-fun relevant_facts full_types respect_no_atp relevance_threshold
- relevance_convergence defs_relevant max_new theory_relevant
+fun relevant_facts full_types relevance_threshold relevance_convergence
+ defs_relevant max_new theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
val add_thms = maps (ProofContext.get_fact ctxt) add
val has_override = not (null add) orelse not (null del)
- val is_FO = is_fol_goal thy goal_cls
+ val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
val axioms =
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
(map (name_thms_pair_from_ref ctxt chained_ths) add @
- (if only then []
- else all_name_thms_pairs respect_no_atp ctxt chained_ths))
+ (if only then [] else all_name_thms_pairs ctxt chained_ths))
|> cnf_rules_pairs thy
|> not has_override ? make_unique
|> filter (fn (cnf_thm, (_, orig_thm)) =>
@@ -600,70 +533,4 @@
|> sort (prod_ord string_ord int_ord o pairself (fst o snd))
end
-(** Helper clauses **)
-
-fun count_combterm (CombConst ((c, _), _, _)) =
- Symtab.map_entry c (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (Literal (_, t)) = count_combterm t
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-
-val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
-fun cnf_helper_thms thy raw =
- map (`Thm.get_name_hint)
- #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
-
-val optional_helpers =
- [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
- (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
- (["c_COMBS"], (false, @{thms COMBS_def}))]
-val optional_typed_helpers =
- [(["c_True", "c_False"], (true, @{thms True_or_False})),
- (["c_If"], (true, @{thms if_True if_False True_or_False}))]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
-
-val init_counters =
- Symtab.make (maps (maps (map (rpair 0) o fst))
- [optional_helpers, optional_typed_helpers])
-
-fun get_helper_clauses thy is_FO full_types conjectures axcls =
- let
- val axclauses = map snd (make_axiom_clauses thy axcls)
- val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
- fun is_needed c = the (Symtab.lookup ct c) > 0
- val cnfs =
- (optional_helpers
- |> full_types ? append optional_typed_helpers
- |> maps (fn (ss, (raw, ths)) =>
- if exists is_needed ss then cnf_helper_thms thy raw ths
- else []))
- @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
- in map snd (make_axiom_clauses thy cnfs) end
-
-(* prepare for passing to writer,
- create additional clauses based on the information from extra_cls *)
-fun prepare_clauses full_types goal_cls axcls extra_cls thy =
- let
- val is_FO = is_fol_goal thy goal_cls
- val ccls = subtract_cls extra_cls goal_cls
- val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
- val ccltms = map prop_of ccls
- and axtms = map (prop_of o #1) extra_cls
- val subs = tfree_classes_of_terms ccltms
- and supers = tvar_classes_of_terms axtms
- and tycons = type_consts_of_terms thy (ccltms @ axtms)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = make_conjecture_clauses thy ccls
- val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
- val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
- val helper_clauses =
- get_helper_clauses thy is_FO full_types conjectures extra_cls
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val classrel_clauses = make_classrel_clauses thy subs supers'
- in
- (Vector.fromList clnames,
- (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
- end
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 29 07:55:18 2010 +0200
@@ -18,9 +18,9 @@
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
struct
+open Clausifier
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
open ATP_Manager
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 28 15:32:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,553 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
-
-Transformation of axiom rules (elim/intro/etc) into CNF forms.
-*)
-
-signature SLEDGEHAMMER_FACT_PREPROCESSOR =
-sig
- type cnf_thm = thm * ((string * int) * thm)
-
- val sledgehammer_prefix: string
- val chained_prefix: string
- val trace: bool Unsynchronized.ref
- val trace_msg: (unit -> string) -> unit
- val skolem_theory_name: string
- val skolem_prefix: string
- val skolem_infix: string
- val is_skolem_const_name: string -> bool
- val cnf_axiom: theory -> thm -> thm list
- val multi_base_blacklist: string list
- val is_theorem_bad_for_atps: thm -> bool
- val type_has_topsort: typ -> bool
- val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
- val saturate_skolem_cache: theory -> theory option
- val auto_saturate_skolem_cache: bool Unsynchronized.ref
- val neg_clausify: thm -> thm list
- val neg_conjecture_clauses:
- Proof.context -> thm -> int -> thm list list * (string * typ) list
- val setup: theory -> theory
-end;
-
-structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
-struct
-
-open Sledgehammer_FOL_Clause
-
-type cnf_thm = thm * ((string * int) * thm)
-
-val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-
-(* Used to label theorems chained into the goal. *)
-val chained_prefix = sledgehammer_prefix ^ "chained_"
-
-val trace = Unsynchronized.ref false;
-fun trace_msg msg = if !trace then tracing (msg ()) else ();
-
-val skolem_theory_name = sledgehammer_prefix ^ "Sko"
-val skolem_prefix = "sko_"
-val skolem_infix = "$"
-
-fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
-
-val type_has_topsort = Term.exists_subtype
- (fn TFree (_, []) => true
- | TVar (_, []) => true
- | _ => false);
-
-
-(**** Transformation of Elimination Rules into First-Order Formulas****)
-
-val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
-val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
-
-(*Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate the
- conclusion variable to False.*)
-fun transform_elim th =
- case concl_of th of (*conclusion variable*)
- @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
- Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
- | v as Var(_, @{typ prop}) =>
- Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
- | _ => th;
-
-(*To enforce single-threading*)
-exception Clausify_failure of theory;
-
-
-(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
-
-(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-
-fun skolem_name thm_name j var_name =
- skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
- skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
-
-(* Hack: Could return false positives (e.g., a user happens to declare a
- constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
- Long_Name.base_name
- #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
-fun rhs_extra_types lhsT rhs =
- let val lhs_vars = Term.add_tfreesT lhsT []
- fun add_new_TFrees (TFree v) =
- if member (op =) lhs_vars v then I else insert (op =) (TFree v)
- | add_new_TFrees _ = I
- val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
- in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
-
-fun skolem_type_and_args bound_T body =
- let
- val args1 = OldTerm.term_frees body
- val Ts1 = map type_of args1
- val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
- val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
- in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
-
-(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
- suggested prefix for the Skolem constants. *)
-fun declare_skolem_funs s th thy =
- let
- val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
- (axs, thy) =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val id = skolem_name s (Unsynchronized.inc skolem_count) s'
- val (cT, args) = skolem_type_and_args T body
- val rhs = list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ body)
- (*Forms a lambda-abstraction over the formal parameters*)
- val (c, thy) =
- Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
- val cdef = id ^ "_def"
- val ((_, ax), thy) =
- Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
- val ax' = Drule.export_without_context ax
- in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
- | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
- in dec_sko (subst_bound (Free (fname, T), p)) thx end
- | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
- | dec_sko _ thx = thx
- in dec_sko (prop_of th) ([], thy) end
-
-fun mk_skolem_id t =
- let val T = fastype_of t in
- Const (@{const_name skolem_id}, T --> T) $ t
- end
-
-fun quasi_beta_eta_contract (Abs (s, T, t')) =
- Abs (s, T, quasi_beta_eta_contract t')
- | quasi_beta_eta_contract t = Envir.beta_eta_contract t
-
-(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs s th =
- let
- val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
- val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
- val Ts = map type_of args
- val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
- val id = skolem_name s (Unsynchronized.inc skolem_count) s'
- val c = Free (id, cT) (* FIXME: needed? ### *)
- (* Forms a lambda-abstraction over the formal parameters *)
- val rhs =
- list_abs_free (map dest_Free args,
- HOLogic.choice_const T
- $ quasi_beta_eta_contract body)
- |> mk_skolem_id
- val def = Logic.mk_equals (c, rhs)
- val comb = list_comb (rhs, args)
- in dec_sko (subst_bound (comb, p)) (def :: defs) end
- | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
- | dec_sko _ defs = defs
- in dec_sko (prop_of th) [] end;
-
-
-(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
-
-(*Returns the vars of a theorem*)
-fun vars_of_thm th =
- map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
-
-val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
-
-(* Removes the lambdas from an equation of the form t = (%x. u). *)
-fun extensionalize th =
- case prop_of th of
- _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
- $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
- | _ => th
-
-fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
- | is_quasi_lambda_free (t1 $ t2) =
- is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
- | is_quasi_lambda_free (Abs _) = false
- | is_quasi_lambda_free _ = true
-
-val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
-
-(*FIXME: requires more use of cterm constructors*)
-fun abstract ct =
- let
- val thy = theory_of_cterm ct
- val Abs(x,_,body) = term_of ct
- val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
- val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
- fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
- in
- case body of
- Const _ => makeK()
- | Free _ => makeK()
- | Var _ => makeK() (*though Var isn't expected*)
- | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
- | rator$rand =>
- if loose_bvar1 (rator,0) then (*C or S*)
- if loose_bvar1 (rand,0) then (*S*)
- let val crator = cterm_of thy (Abs(x,xT,rator))
- val crand = cterm_of thy (Abs(x,xT,rand))
- val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
- in
- Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
- end
- else (*C*)
- let val crator = cterm_of thy (Abs(x,xT,rator))
- val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
- in
- Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
- end
- else if loose_bvar1 (rand,0) then (*B or eta*)
- if rand = Bound 0 then Thm.eta_conversion ct
- else (*B*)
- let val crand = cterm_of thy (Abs(x,xT,rand))
- val crator = cterm_of thy rator
- val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
- in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
- else makeK()
- | _ => raise Fail "abstract: Bad term"
- end;
-
-(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
-fun do_introduce_combinators ct =
- if is_quasi_lambda_free (term_of ct) then
- Thm.reflexive ct
- else case term_of ct of
- Abs _ =>
- let
- val (cv, cta) = Thm.dest_abs NONE ct
- val (v, _) = dest_Free (term_of cv)
- val u_th = do_introduce_combinators cta
- val cu = Thm.rhs_of u_th
- val comb_eq = abstract (Thm.cabs cv cu)
- in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
- | _ $ _ =>
- let val (ct1, ct2) = Thm.dest_comb ct in
- Thm.combination (do_introduce_combinators ct1)
- (do_introduce_combinators ct2)
- end
-
-fun introduce_combinators th =
- if is_quasi_lambda_free (prop_of th) then
- th
- else
- let
- val th = Drule.eta_contraction_rule th
- val eqth = do_introduce_combinators (cprop_of th)
- in Thm.equal_elim eqth th end
- handle THM (msg, _, _) =>
- (warning ("Error in the combinator translation of " ^
- Display.string_of_thm_without_context th ^
- "\nException message: " ^ msg ^ ".");
- (* A type variable of sort "{}" will make abstraction fail. *)
- TrueI)
-
-(*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
-
-(*cterm version of mk_cTrueprop*)
-fun c_mkTrueprop A = Thm.capply cTrueprop A;
-
-(*Given an abstraction over n variables, replace the bound variables by free
- ones. Return the body, along with the list of free variables.*)
-fun c_variant_abs_multi (ct0, vars) =
- let val (cv,ct) = Thm.dest_abs NONE ct0
- in c_variant_abs_multi (ct, cv::vars) end
- handle CTERM _ => (ct0, rev vars);
-
-(*Given the definition of a Skolem function, return a theorem to replace
- an existential formula by a use of that function.
- Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_theorem_of_def inline def =
- let
- val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
- val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
- val (ch, frees) = c_variant_abs_multi (rhs', [])
- val (chilbert, cabs) = ch |> Thm.dest_comb
- val thy = Thm.theory_of_cterm chilbert
- val t = Thm.term_of chilbert
- val T =
- case t of
- Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
- | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
- val cex = Thm.cterm_of thy (HOLogic.exists_const T)
- val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
- and conc =
- Drule.list_comb (if inline then rhs else c, frees)
- |> Drule.beta_conv cabs |> c_mkTrueprop
- fun tacf [prem] =
- (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
- else rewrite_goals_tac [def])
- THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
- RS @{thm someI_ex}) 1
- in Goal.prove_internal [ex_tm] conc tacf
- |> forall_intr_list frees
- |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
- |> Thm.varifyT_global
- end;
-
-
-(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
-fun to_nnf th ctxt0 =
- let val th1 = th |> transform_elim |> zero_var_indexes
- val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize
- |> Meson.make_nnf ctxt
- in (th3, ctxt) end;
-
-(*Generate Skolem functions for a theorem supplied in nnf*)
-fun skolem_theorems_of_assume s th =
- map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th))
- (assume_skolem_funs s th)
-
-
-(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
-
-val max_lambda_nesting = 3
-
-fun term_has_too_many_lambdas max (t1 $ t2) =
- exists (term_has_too_many_lambdas max) [t1, t2]
- | term_has_too_many_lambdas max (Abs (_, _, t)) =
- max = 0 orelse term_has_too_many_lambdas (max - 1) t
- | term_has_too_many_lambdas _ _ = false
-
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-
-(* Don't count nested lambdas at the level of formulas, since they are
- quantifiers. *)
-fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
- formula_has_too_many_lambdas (T :: Ts) t
- | formula_has_too_many_lambdas Ts t =
- if is_formula_type (fastype_of1 (Ts, t)) then
- exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
- else
- term_has_too_many_lambdas max_lambda_nesting t
-
-(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
- was 11. *)
-val max_apply_depth = 15
-
-fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
- | apply_depth (Abs (_, _, t)) = apply_depth t
- | apply_depth _ = 0
-
-fun is_formula_too_complex t =
- apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
- formula_has_too_many_lambdas [] t
-
-fun is_strange_thm th =
- case head_of (concl_of th) of
- Const (a, _) => (a <> @{const_name Trueprop} andalso
- a <> @{const_name "=="})
- | _ => false;
-
-fun is_theorem_bad_for_atps thm =
- let val t = prop_of thm in
- is_formula_too_complex t orelse exists_type type_has_topsort t orelse
- is_strange_thm thm
- end
-
-(* FIXME: put other record thms here, or declare as "no_atp" *)
-val multi_base_blacklist =
- ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
- "split_asm", "cases", "ext_cases"];
-
-fun fake_name th =
- if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
- else gensym "unknown_thm_";
-
-(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolemize_theorem s th =
- if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
- is_theorem_bad_for_atps th then
- []
- else
- let
- val ctxt0 = Variable.global_thm_context th
- val (nnfth, ctxt) = to_nnf th ctxt0
- val defs = skolem_theorems_of_assume s nnfth
- val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
- in
- cnfs |> map introduce_combinators
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- end
- handle THM _ => []
-
-(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
- Skolem functions.*)
-structure ThmCache = Theory_Data
-(
- type T = thm list Thmtab.table * unit Symtab.table;
- val empty = (Thmtab.empty, Symtab.empty);
- val extend = I;
- fun merge ((cache1, seen1), (cache2, seen2)) : T =
- (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
-);
-
-val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
-val already_seen = Symtab.defined o #2 o ThmCache.get;
-
-val update_cache = ThmCache.map o apfst o Thmtab.update;
-fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
-
-(* Convert Isabelle theorems into axiom clauses. *)
-fun cnf_axiom thy th0 =
- let val th = Thm.transfer thy th0 in
- case lookup_cache thy th of
- SOME cls => cls
- | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
- end;
-
-
-(**** Translate a set of theorems into CNF ****)
-
-(*The combination of rev and tail recursion preserves the original order*)
-fun cnf_rules_pairs thy =
- let
- fun do_one _ [] = []
- | do_one ((name, k), th) (cls :: clss) =
- (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
- fun do_all pairs [] = pairs
- | do_all pairs ((name, th) :: ths) =
- let
- val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
- handle THM _ => [] |
- CLAUSE _ => []
- in do_all (new_pairs @ pairs) ths end
- in do_all [] o rev end
-
-
-(**** Convert all facts of the theory into FOL or HOL clauses ****)
-
-local
-
-fun skolem_def (name, th) thy =
- let val ctxt0 = Variable.global_thm_context th in
- case try (to_nnf th) ctxt0 of
- NONE => (NONE, thy)
- | SOME (nnfth, ctxt) =>
- let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
- in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
- end;
-
-fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
- let
- val (cnfs, ctxt) =
- Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
- val cnfs' = cnfs
- |> map introduce_combinators
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation;
- in (th, cnfs') end;
-
-in
-
-fun saturate_skolem_cache thy =
- let
- val facts = PureThy.facts_of thy;
- val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
- if Facts.is_concealed facts name orelse already_seen thy name then I
- else cons (name, ths));
- val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
- if member (op =) multi_base_blacklist (Long_Name.base_name name) then
- I
- else
- fold_index (fn (i, th) =>
- if is_theorem_bad_for_atps th orelse
- is_some (lookup_cache thy th) then
- I
- else
- cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
- in
- if null new_facts then
- NONE
- else
- let
- val (defs, thy') = thy
- |> fold (mark_seen o #1) new_facts
- |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
- |>> map_filter I;
- val cache_entries = Par_List.map skolem_cnfs defs;
- in SOME (fold update_cache cache_entries thy') end
- end;
-
-end;
-
-(* For emergency use where the Skolem cache causes problems. *)
-val auto_saturate_skolem_cache = Unsynchronized.ref true
-
-fun conditionally_saturate_skolem_cache thy =
- if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
-
-
-(*** Converting a subgoal into negated conjecture clauses. ***)
-
-fun neg_skolemize_tac ctxt =
- EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
-
-val neg_clausify =
- single
- #> Meson.make_clauses_unsorted
- #> map introduce_combinators
- #> Meson.finish_cnf
-
-fun neg_conjecture_clauses ctxt st0 n =
- let
- (* "Option" is thrown if the assumptions contain schematic variables. *)
- val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
- val ({params, prems, ...}, _) =
- Subgoal.focus (Variable.set_body false ctxt) n st
- in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
-
-
-(** setup **)
-
-val setup =
- perhaps conditionally_saturate_skolem_cache
- #> Theory.at_end conditionally_saturate_skolem_cache
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Jun 28 15:32:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,361 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
-
-Storing/printing FOL clauses and arity clauses. Typed equality is
-treated differently.
-
-FIXME: combine with sledgehammer_hol_clause!
-*)
-
-signature SLEDGEHAMMER_FOL_CLAUSE =
-sig
- val type_wrapper_name : string
- val schematic_var_prefix: string
- val fixed_var_prefix: string
- val tvar_prefix: string
- val tfree_prefix: string
- val const_prefix: string
- val tconst_prefix: string
- val class_prefix: string
- val union_all: ''a list list -> ''a list
- val const_trans_table: string Symtab.table
- val type_const_trans_table: string Symtab.table
- val ascii_of: string -> string
- val undo_ascii_of: string -> string
- val make_schematic_var : string * int -> string
- val make_fixed_var : string -> string
- val make_schematic_type_var : string * int -> string
- val make_fixed_type_var : string -> string
- val make_fixed_const : string -> string
- val make_fixed_type_const : string -> string
- val make_type_class : string -> string
- type name = string * string
- type name_pool = string Symtab.table * string Symtab.table
- val empty_name_pool : bool -> name_pool option
- val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
- val nice_name : name -> name_pool option -> string * name_pool option
- datatype kind = Axiom | Conjecture
- datatype type_literal =
- TyLitVar of string * name |
- TyLitFree of string * name
- exception CLAUSE of string * term
- val type_literals_for_types : typ list -> type_literal list
- datatype arLit =
- TConsLit of class * string * string list
- | TVarLit of class * string
- datatype arity_clause = ArityClause of
- {axiom_name: string, conclLit: arLit, premLits: arLit list}
- datatype classrel_clause = ClassrelClause of
- {axiom_name: string, subclass: class, superclass: class}
- val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
- val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
-end
-
-structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
-struct
-
-open Sledgehammer_Util
-
-val type_wrapper_name = "ti"
-
-val schematic_var_prefix = "V_";
-val fixed_var_prefix = "v_";
-
-val tvar_prefix = "T_";
-val tfree_prefix = "t_";
-
-val classrel_clause_prefix = "clsrel_";
-
-val const_prefix = "c_";
-val tconst_prefix = "tc_";
-val class_prefix = "class_";
-
-fun union_all xss = fold (union (op =)) xss []
-
-(* Readable names for the more common symbolic functions. Do not mess with the
- last nine entries of the table unless you know what you are doing. *)
-val const_trans_table =
- Symtab.make [(@{const_name "op ="}, "equal"),
- (@{const_name "op &"}, "and"),
- (@{const_name "op |"}, "or"),
- (@{const_name "op -->"}, "implies"),
- (@{const_name "op :"}, "in"),
- (@{const_name fequal}, "fequal"),
- (@{const_name COMBI}, "COMBI"),
- (@{const_name COMBK}, "COMBK"),
- (@{const_name COMBB}, "COMBB"),
- (@{const_name COMBC}, "COMBC"),
- (@{const_name COMBS}, "COMBS"),
- (@{const_name True}, "True"),
- (@{const_name False}, "False"),
- (@{const_name If}, "If")]
-
-val type_const_trans_table =
- Symtab.make [(@{type_name "*"}, "prod"),
- (@{type_name "+"}, "sum")]
-
-(*Escaping of special characters.
- Alphanumeric characters are left unchanged.
- The character _ goes to __
- Characters in the range ASCII space to / go to _A to _P, respectively.
- Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
-val A_minus_space = Char.ord #"A" - Char.ord #" ";
-
-fun stringN_of_int 0 _ = ""
- | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
-
-fun ascii_of_c c =
- if Char.isAlphaNum c then String.str c
- else if c = #"_" then "__"
- else if #" " <= c andalso c <= #"/"
- then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
- else if Char.isPrint c
- then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
- else ""
-
-val ascii_of = String.translate ascii_of_c;
-
-(** Remove ASCII armouring from names in proof files **)
-
-(*We don't raise error exceptions because this code can run inside the watcher.
- Also, the errors are "impossible" (hah!)*)
-fun undo_ascii_aux rcs [] = String.implode(rev rcs)
- | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
- (*Three types of _ escapes: __, _A to _P, _nnn*)
- | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
- | undo_ascii_aux rcs (#"_" :: c :: cs) =
- if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
- then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
- else
- let val digits = List.take (c::cs, 3) handle Subscript => []
- in
- case Int.fromString (String.implode digits) of
- NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
- | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
- end
- | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
-
-val undo_ascii_of = undo_ascii_aux [] o String.explode;
-
-(*Remove the initial ' character from a type variable, if it is present*)
-fun trim_type_var s =
- if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
- else error ("trim_type: Malformed type variable encountered: " ^ s);
-
-fun ascii_of_indexname (v,0) = ascii_of v
- | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
-
-fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
-fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
-
-fun make_schematic_type_var (x,i) =
- tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
-fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-
-fun lookup_const c =
- case Symtab.lookup const_trans_table c of
- SOME c' => c'
- | NONE => ascii_of c
-
-fun lookup_type_const c =
- case Symtab.lookup type_const_trans_table c of
- SOME c' => c'
- | NONE => ascii_of c
-
-(* "op =" MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const @{const_name "op ="} = "equal"
- | make_fixed_const c = const_prefix ^ lookup_const c
-
-fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c
-
-fun make_type_class clas = class_prefix ^ ascii_of clas;
-
-
-(**** name pool ****)
-
-type name = string * string
-type name_pool = string Symtab.table * string Symtab.table
-
-fun empty_name_pool readable_names =
- if readable_names then SOME (`I Symtab.empty) else NONE
-
-fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
-fun pool_map f xs =
- pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
-
-fun add_nice_name full_name nice_prefix j the_pool =
- let
- val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
- in
- case Symtab.lookup (snd the_pool) nice_name of
- SOME full_name' =>
- if full_name = full_name' then (nice_name, the_pool)
- else add_nice_name full_name nice_prefix (j + 1) the_pool
- | NONE =>
- (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
- Symtab.update_new (nice_name, full_name) (snd the_pool)))
- end
-
-fun translate_first_char f s =
- String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
-
-fun readable_name full_name s =
- let
- val s = s |> Long_Name.base_name
- |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
- val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
- val s' =
- (s' |> rev
- |> implode
- |> String.translate
- (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
- else ""))
- ^ replicate_string (String.size s - length s') "_"
- val s' =
- if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
- else s'
- (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
- ("op &", "op |", etc.). *)
- val s' = if s' = "equal" orelse s' = "op" then full_name else s'
- in
- case (Char.isLower (String.sub (full_name, 0)),
- Char.isLower (String.sub (s', 0))) of
- (true, false) => translate_first_char Char.toLower s'
- | (false, true) => translate_first_char Char.toUpper s'
- | _ => s'
- end
-
-fun nice_name (full_name, _) NONE = (full_name, NONE)
- | nice_name (full_name, desired_name) (SOME the_pool) =
- case Symtab.lookup (fst the_pool) full_name of
- SOME nice_name => (nice_name, SOME the_pool)
- | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
- the_pool
- |> apsnd SOME
-
-(**** Definitions and functions for FOL clauses for TPTP format output ****)
-
-datatype kind = Axiom | Conjecture;
-
-(**** Isabelle FOL clauses ****)
-
-(* The first component is the type class; the second is a TVar or TFree. *)
-datatype type_literal =
- TyLitVar of string * name |
- TyLitFree of string * name
-
-exception CLAUSE of string * term;
-
-(*Make literals for sorted type variables*)
-fun sorts_on_typs_aux (_, []) = []
- | sorts_on_typs_aux ((x,i), s::ss) =
- let val sorts = sorts_on_typs_aux ((x,i), ss)
- in
- if s = "HOL.type" then sorts
- else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
- else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
- end;
-
-fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
- | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
-
-(*Given a list of sorted type variables, return a list of type literals.*)
-fun type_literals_for_types Ts =
- fold (union (op =)) (map sorts_on_typs Ts) []
-
-(** make axiom and conjecture clauses. **)
-
-(**** Isabelle arities ****)
-
-datatype arLit = TConsLit of class * string * string list
- | TVarLit of class * string;
-
-datatype arity_clause =
- ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
-
-
-fun gen_TVars 0 = []
- | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
-
-fun pack_sort(_,[]) = []
- | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*)
- | pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
-
-(*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
- let val tvars = gen_TVars (length args)
- val tvars_srts = ListPair.zip (tvars,args)
- in
- ArityClause {axiom_name = axiom_name,
- conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
- premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
- end;
-
-
-(**** Isabelle class relations ****)
-
-datatype classrel_clause =
- ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
-
-(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
-fun class_pairs _ [] _ = []
- | class_pairs thy subs supers =
- let
- val class_less = Sorts.class_less (Sign.classes_of thy)
- fun add_super sub super = class_less (sub, super) ? cons (sub, super)
- fun add_supers sub = fold (add_super sub) supers
- in fold add_supers subs [] end
-
-fun make_classrel_clause (sub,super) =
- ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
- ascii_of super,
- subclass = make_type_class sub,
- superclass = make_type_class super};
-
-fun make_classrel_clauses thy subs supers =
- map make_classrel_clause (class_pairs thy subs supers);
-
-
-(** Isabelle arities **)
-
-fun arity_clause _ _ (_, []) = []
- | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
- arity_clause seen n (tcons,ars)
- | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
- if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
- make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
- arity_clause seen (n+1) (tcons,ars)
- else
- make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
- arity_clause (class::seen) n (tcons,ars)
-
-fun multi_arity_clause [] = []
- | multi_arity_clause ((tcons, ars) :: tc_arlists) =
- arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
-
-(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
- provided its arguments have the corresponding sorts.*)
-fun type_class_pairs thy tycons classes =
- let val alg = Sign.classes_of thy
- fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
- fun add_class tycon class =
- cons (class, domain_sorts tycon class)
- handle Sorts.CLASS_ERROR _ => I
- fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
- in map try_classes tycons end;
-
-(*Proving one (tycon, class) membership may require proving others, so iterate.*)
-fun iter_type_class_pairs _ _ [] = ([], [])
- | iter_type_class_pairs thy tycons classes =
- let val cpairs = type_class_pairs thy tycons classes
- val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
- |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
- val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
- in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
-
-fun make_arity_clauses thy tycons classes =
- let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
- in (classes', multi_arity_clause cpairs) end;
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 28 15:32:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,231 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
- Author: Jia Meng, NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-FOL clauses translated from HOL formulas.
-*)
-
-signature SLEDGEHAMMER_HOL_CLAUSE =
-sig
- type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
- type name = Sledgehammer_FOL_Clause.name
- type name_pool = Sledgehammer_FOL_Clause.name_pool
- type kind = Sledgehammer_FOL_Clause.kind
- type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
- type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type polarity = bool
-
- datatype combtyp =
- TyVar of name |
- TyFree of name |
- TyConstr of name * combtyp list
- datatype combterm =
- CombConst of name * combtyp * combtyp list (* Const and Free *) |
- CombVar of name * combtyp |
- CombApp of combterm * combterm
- datatype literal = Literal of polarity * combterm
- datatype hol_clause =
- HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: literal list, ctypes_sorts: typ list}
-
- val type_of_combterm : combterm -> combtyp
- val strip_combterm_comb : combterm -> combterm * combterm list
- val literals_of_term : theory -> term -> literal list * typ list
- val conceal_skolem_somes :
- int -> (string * term) list -> term -> (string * term) list * term
- exception TRIVIAL of unit
- val make_conjecture_clauses : theory -> thm list -> hol_clause list
- val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
-end
-
-structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_Fact_Preprocessor
-
-(******************************************************)
-(* data types for typed combinator expressions *)
-(******************************************************)
-
-type polarity = bool
-
-datatype combtyp =
- TyVar of name |
- TyFree of name |
- TyConstr of name * combtyp list
-
-datatype combterm =
- CombConst of name * combtyp * combtyp list (* Const and Free *) |
- CombVar of name * combtyp |
- CombApp of combterm * combterm
-
-datatype literal = Literal of polarity * combterm;
-
-datatype hol_clause =
- HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: literal list, ctypes_sorts: typ list}
-
-(*********************************************************************)
-(* convert a clause with type Term.term to a clause with type clause *)
-(*********************************************************************)
-
-(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr (_, [_, tp2])) = tp2
- | result_type _ = raise Fail "non-function type"
-
-fun type_of_combterm (CombConst (_, tp, _)) = tp
- | type_of_combterm (CombVar (_, tp)) = tp
- | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
-
-(*gets the head of a combinator application, along with the list of arguments*)
-fun strip_combterm_comb u =
- let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
- | stripc x = x
- in stripc(u,[]) end
-
-fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
- (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
- | isFalse _ = false;
-
-fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
- (pol andalso c = "c_True") orelse
- (not pol andalso c = "c_False")
- | isTrue _ = false;
-
-fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
-
-fun type_of (Type (a, Ts)) =
- let val (folTypes,ts) = types_of Ts in
- (TyConstr (`make_fixed_type_const a, folTypes), ts)
- end
- | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
- | type_of (tp as TVar (x, _)) =
- (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
-and types_of Ts =
- let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
- (folTyps, union_all ts)
- end
-
-(* same as above, but no gathering of sort information *)
-fun simp_type_of (Type (a, Ts)) =
- TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
- | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
- | simp_type_of (TVar (x, _)) =
- TyVar (make_schematic_type_var x, string_of_indexname x)
-
-(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of thy (Const (c, T)) =
- let
- val (tp, ts) = type_of T
- val tvar_list =
- (if String.isPrefix skolem_theory_name c then
- [] |> Term.add_tvarsT T |> map TVar
- else
- (c, T) |> Sign.const_typargs thy)
- |> map simp_type_of
- val c' = CombConst (`make_fixed_const c, tp, tvar_list)
- in (c',ts) end
- | combterm_of _ (Free(v, T)) =
- let val (tp,ts) = type_of T
- val v' = CombConst (`make_fixed_var v, tp, [])
- in (v',ts) end
- | combterm_of _ (Var(v, T)) =
- let val (tp,ts) = type_of T
- val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
- in (v',ts) end
- | combterm_of thy (P $ Q) =
- let val (P', tsP) = combterm_of thy P
- val (Q', tsQ) = combterm_of thy Q
- in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
-
-fun predicate_of thy ((@{const Not} $ P), polarity) =
- predicate_of thy (P, not polarity)
- | predicate_of thy (t, polarity) =
- (combterm_of thy (Envir.eta_contract t), polarity)
-
-fun literals_of_term1 args thy (@{const Trueprop} $ P) =
- literals_of_term1 args thy P
- | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
- literals_of_term1 (literals_of_term1 args thy P) thy Q
- | literals_of_term1 (lits, ts) thy P =
- let val ((pred, ts'), pol) = predicate_of thy (P, true) in
- (Literal (pol, pred) :: lits, union (op =) ts ts')
- end
-val literals_of_term = literals_of_term1 ([], [])
-
-fun skolem_name i j num_T_args =
- skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
- skolem_infix ^ "g"
-
-fun conceal_skolem_somes i skolem_somes t =
- if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
- let
- fun aux skolem_somes
- (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
- let
- val (skolem_somes, s) =
- if i = ~1 then
- (skolem_somes, @{const_name undefined})
- else case AList.find (op aconv) skolem_somes t of
- s :: _ => (skolem_somes, s)
- | [] =>
- let
- val s = skolem_theory_name ^ "." ^
- skolem_name i (length skolem_somes)
- (length (Term.add_tvarsT T []))
- in ((s, t) :: skolem_somes, s) end
- in (skolem_somes, Const (s, T)) end
- | aux skolem_somes (t1 $ t2) =
- let
- val (skolem_somes, t1) = aux skolem_somes t1
- val (skolem_somes, t2) = aux skolem_somes t2
- in (skolem_somes, t1 $ t2) end
- | aux skolem_somes (Abs (s, T, t')) =
- let val (skolem_somes, t') = aux skolem_somes t' in
- (skolem_somes, Abs (s, T, t'))
- end
- | aux skolem_somes t = (skolem_somes, t)
- in aux skolem_somes t end
- else
- (skolem_somes, t)
-
-(* Trivial problem, which resolution cannot handle (empty clause) *)
-exception TRIVIAL of unit
-
-(* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
- let
- val (skolem_somes, t) =
- th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
- val (lits, ctypes_sorts) = literals_of_term thy t
- in
- if forall isFalse lits then
- raise TRIVIAL ()
- else
- (skolem_somes,
- HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
- kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
- end
-
-fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
- let
- val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
- in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
-
-fun make_axiom_clauses thy clauses =
- ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
-
-fun make_conjecture_clauses thy =
- let
- fun aux _ _ [] = []
- | aux n skolem_somes (th :: ths) =
- let
- val (skolem_somes, cls) =
- make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
- in cls :: aux (n + 1) skolem_somes ths end
- in aux 0 [] end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 29 07:55:18 2010 +0200
@@ -17,9 +17,8 @@
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
+open Clausifier
open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Fact_Preprocessor
open ATP_Manager
open ATP_Systems
open Sledgehammer_Fact_Minimizer
@@ -69,7 +68,6 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("respect_no_atp", "true"),
("relevance_threshold", "50"),
("relevance_convergence", "320"),
("theory_relevant", "smart"),
@@ -86,7 +84,6 @@
("no_overlord", "overlord"),
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
- ("ignore_no_atp", "respect_no_atp"),
("theory_irrelevant", "theory_relevant"),
("defs_irrelevant", "defs_relevant"),
("no_isar_proof", "isar_proof")]
@@ -168,7 +165,6 @@
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
- val respect_no_atp = lookup_bool "respect_no_atp"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_convergence =
@@ -182,7 +178,7 @@
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+ relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
@@ -203,13 +199,10 @@
0 => priority "No subgoal!"
| n =>
let
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, timeout)
val _ = kill_atps ()
val _ = priority "Sledgehammering..."
- val _ = app (start_prover_thread params birth_time death_time i n
- relevance_override minimize_command
- state) atps
+ val _ = app (start_prover_thread params i n relevance_override
+ minimize_command state) atps
in () end
fun minimize override_params i refs state =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 29 07:55:18 2010 +0200
@@ -8,12 +8,8 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
type minimize_command = string list -> string
- type name_pool = Sledgehammer_FOL_Clause.name_pool
+ type name_pool = Metis_Clauses.name_pool
- val invert_const: string -> string
- val invert_type_const: string -> string
- val num_type_args: theory -> string -> int
- val strip_prefix: string -> string -> string option
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
@@ -31,10 +27,9 @@
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
struct
+open Clausifier
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_HOL_Clause
-open Sledgehammer_Fact_Preprocessor
type minimize_command = string list -> string
@@ -212,28 +207,13 @@
exception NODE of node list
-(*If string s has the prefix s1, return the result of deleting it.*)
-fun strip_prefix s1 s =
- if String.isPrefix s1 s
- then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
- else NONE;
-
-(*Invert the table of translations between Isabelle and ATPs*)
-val type_const_trans_table_inv =
- Symtab.make (map swap (Symtab.dest type_const_trans_table));
-
-fun invert_type_const c =
- case Symtab.lookup type_const_trans_table_inv c of
- SOME c' => c'
- | NONE => c;
-
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
| type_from_node tfrees (u as StrNode (a, us)) =
let val Ts = map (type_from_node tfrees) us in
case strip_prefix tconst_prefix a of
- SOME b => Type (invert_type_const b, Ts)
+ SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
raise NODE [u] (* only "tconst"s have type arguments *)
@@ -250,24 +230,6 @@
Type_Infer.param 0 (a, HOLogic.typeS)
end
-(*Invert the table of translations between Isabelle and ATPs*)
-val const_trans_table_inv =
- Symtab.update ("fequal", @{const_name "op ="})
- (Symtab.make (map swap (Symtab.dest const_trans_table)))
-
-fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
-
-(* The number of type arguments of a constant, zero if it's monomorphic. For
- (instances of) Skolem pseudoconstants, this information is encoded in the
- constant name. *)
-fun num_type_args thy s =
- if String.isPrefix skolem_theory_name s then
- s |> unprefix skolem_theory_name
- |> space_explode skolem_infix |> hd
- |> space_explode "_" |> List.last |> Int.fromString |> the
- else
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
fun fix_atp_variable_name s =
let
fun subscript_name s n = s ^ nat_subscript n
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jun 29 07:55:18 2010 +0200
@@ -7,11 +7,11 @@
signature SLEDGEHAMMER_TPTP_FORMAT =
sig
- type name_pool = Sledgehammer_FOL_Clause.name_pool
- type type_literal = Sledgehammer_FOL_Clause.type_literal
- type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
- type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type hol_clause = Sledgehammer_HOL_Clause.hol_clause
+ type name_pool = Metis_Clauses.name_pool
+ type type_literal = Metis_Clauses.type_literal
+ type classrel_clause = Metis_Clauses.classrel_clause
+ type arity_clause = Metis_Clauses.arity_clause
+ type hol_clause = Metis_Clauses.hol_clause
val tptp_of_type_literal :
bool -> type_literal -> name_pool option -> string * name_pool option
@@ -25,9 +25,8 @@
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
struct
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_HOL_Clause
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 29 07:55:18 2010 +0200
@@ -8,8 +8,6 @@
sig
val plural_s : int -> string
val serial_commas : string -> string list -> string list
- val replace_all : string -> string -> string -> string
- val remove_all : string -> string -> string
val timestamp : unit -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
@@ -31,17 +29,6 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-fun replace_all bef aft =
- let
- fun aux seen "" = String.implode (rev seen)
- | aux seen s =
- if String.isPrefix bef s then
- aux seen "" ^ aft ^ aux [] (unprefix bef s)
- else
- aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
- in aux [] end
-fun remove_all bef = replace_all bef ""
-
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
fun parse_bool_option option name s =
--- a/src/HOL/Tools/TFL/usyntax.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Tue Jun 29 07:55:18 2010 +0200
@@ -196,7 +196,7 @@
local
fun mk_uncurry (xt, yt, zt) =
- Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
+ Const(@{const_name prod_case}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
@@ -276,7 +276,7 @@
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
-local fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
+local fun ucheck t = (if #Name (dest_const t) = @{const_name prod_case} then t
else raise Match)
in
fun dest_pabs used tm =
--- a/src/HOL/Tools/hologic.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Jun 29 07:55:18 2010 +0200
@@ -315,12 +315,12 @@
end;
fun split_const (A, B, C) =
- Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C);
fun mk_split t =
(case Term.fastype_of t of
T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
- Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t
| _ => raise TERM ("mk_split: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
@@ -427,7 +427,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ t) =
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
| strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
| strip (p :: ps) qs Ts t = strip ps qs
--- a/src/HOL/Tools/quickcheck_generators.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Jun 29 07:55:18 2010 +0200
@@ -374,7 +374,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name split}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
+ (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t
(mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
@@ -414,7 +414,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name split}, [T, @{typ "unit => term"},
+ (@{const_name prod_case}, [T, @{typ "unit => term"},
liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
--- a/src/HOL/Word/Num_Lemmas.thy Mon Jun 28 15:32:27 2010 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy Tue Jun 29 07:55:18 2010 +0200
@@ -11,8 +11,8 @@
lemma contentsI: "y = {x} ==> contents y = x"
unfolding contents_def by auto -- {* FIXME move *}
-lemmas split_split = prod.split [unfolded prod_case_split]
-lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
+lemmas split_split = prod.split
+lemmas split_split_asm = prod.split_asm
lemmas split_splits = split_split split_split_asm
lemmas funpow_0 = funpow.simps(1)
--- a/src/Pure/General/position.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Pure/General/position.ML Tue Jun 29 07:55:18 2010 +0200
@@ -67,8 +67,8 @@
fun advance_count "\n" (i: int, j: int, k: int) =
(if_valid i (i + 1), if_valid j 1, if_valid k (k + 1))
| advance_count s (i, j, k) =
- if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
- then (i, if_valid j (j + 1), if_valid k (k + 1)) else (i, j, k);
+ if Symbol.is_regular s then (i, if_valid j (j + 1), if_valid k (k + 1))
+ else (i, j, k);
fun invalid_count (i, j, k) =
not (valid i orelse valid j orelse valid k);
--- a/src/Pure/General/symbol.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Pure/General/symbol.ML Tue Jun 29 07:55:18 2010 +0200
@@ -15,9 +15,9 @@
val space: symbol
val spaces: int -> string
val is_char: symbol -> bool
+ val is_utf8: symbol -> bool
val is_symbolic: symbol -> bool
val is_printable: symbol -> bool
- val is_utf8_trailer: symbol -> bool
val eof: symbol
val is_eof: symbol -> bool
val not_eof: symbol -> bool
@@ -42,7 +42,7 @@
val is_raw: symbol -> bool
val decode_raw: symbol -> string
val encode_raw: string -> string
- datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string
+ datatype sym = Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string
val decode: symbol -> sym
datatype kind = Letter | Digit | Quasi | Blank | Other
val kind: symbol -> kind
@@ -108,14 +108,14 @@
fun is_char s = size s = 1;
+fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
+
fun is_symbolic s =
String.isPrefix "\\<" s andalso not (String.isPrefix "\\<^" s);
fun is_printable s =
if is_char s then ord space <= ord s andalso ord s <= ord "~"
- else not (String.isPrefix "\\<^" s);
-
-fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
+ else is_utf8 s orelse not (String.isPrefix "\\<^" s);
(* input source control *)
@@ -224,10 +224,12 @@
(* symbol variants *)
-datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string;
+datatype sym =
+ Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string;
fun decode s =
if is_char s then Char s
+ else if is_utf8 s then UTF8 s
else if is_raw s then Raw (decode_raw s)
else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4))
else if String.isPrefix "\\<" s then Sym (String.substring (s, 2, size s - 3))
@@ -426,7 +428,9 @@
local
-fun is_plain s = s <> "\^M" andalso s <> "\\" andalso not_eof s;
+fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\";
+
+fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
val scan_encoded_newline =
$$ "\^M" -- $$ "\n" >> K "\n" ||
@@ -439,6 +443,7 @@
val scan =
Scan.one is_plain ||
+ Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode ||
scan_encoded_newline ||
($$ "\\" ^^ $$ "<" ^^
!! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
@@ -471,7 +476,7 @@
fun no_explode [] = true
| no_explode ("\\" :: "<" :: _) = false
| no_explode ("\^M" :: _) = false
- | no_explode (_ :: cs) = no_explode cs;
+ | no_explode (c :: cs) = is_ascii c andalso no_explode cs;
in
@@ -486,7 +491,11 @@
(* escape *)
-val esc = fn s => if is_char s then s else "\\" ^ s;
+val esc = fn s =>
+ if is_char s then s
+ else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
+ else "\\" ^ s;
+
val escape = implode o map esc o sym_explode;
--- a/src/Pure/General/symbol.scala Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Pure/General/symbol.scala Tue Jun 29 07:55:18 2010 +0200
@@ -31,7 +31,9 @@
/* Symbol regexps */
private val plain = new Regex("""(?xs)
- [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+ [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+
+ private val newline = new Regex("""(?xs) \r\n | \r """)
private val symbol = new Regex("""(?xs)
\\ < (?:
@@ -39,17 +41,17 @@
\^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
// FIXME cover bad surrogates!?
- // FIXME check wrt. ML version
+ // FIXME check wrt. Isabelle/ML version
private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
""" \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
// total pattern
- val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
+ val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .")
/* basic matching */
- def is_plain(c: Char): Boolean = !(c == '\\' || '\ud800' <= c && c <= '\udfff')
+ def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
def is_wellformed(s: CharSequence): Boolean =
s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
--- a/src/Pure/ML/ml_syntax.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Pure/ML/ml_syntax.ML Tue Jun 29 07:55:18 2010 +0200
@@ -26,6 +26,7 @@
val print_sort: sort -> string
val print_typ: typ -> string
val print_term: term -> string
+ val pretty_string: string -> Pretty.T
end;
structure ML_Syntax: ML_SYNTAX =
@@ -92,4 +93,15 @@
"Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
| print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
+
+(* toplevel pretty printing *)
+
+fun pretty_string raw_str =
+ let
+ val str =
+ implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
+ handle Fail _ => raw_str;
+ val syms = Symbol.explode str handle ERROR _ => explode str;
+ in Pretty.str (quote (implode (map print_char syms))) end;
+
end;
--- a/src/Pure/Thy/latex.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Pure/Thy/latex.ML Tue Jun 29 07:55:18 2010 +0200
@@ -77,6 +77,7 @@
fun output_known_sym (known_sym, known_ctrl) sym =
(case Symbol.decode sym of
Symbol.Char s => output_chr s
+ | Symbol.UTF8 s => s
| Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
| Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
| Symbol.Raw s => s);
--- a/src/Pure/pure_setup.ML Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Pure/pure_setup.ML Tue Jun 29 07:55:18 2010 +0200
@@ -18,6 +18,7 @@
(* ML toplevel pretty printing *)
+toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Tue Jun 29 07:55:18 2010 +0200
@@ -56,6 +56,19 @@
class Document_Model(val session: Session, val buffer: Buffer)
{
+ /* visible line end */
+
+ // simplify slightly odd result of TextArea.getLineEndOffset
+ // NB: jEdit already normalizes \r\n and \r to \n
+ def visible_line_end(start: Int, end: Int): Int =
+ {
+ val end1 = end - 1
+ if (start <= end1 && end1 < buffer.getLength &&
+ buffer.getSegment(end1, 1).charAt(0) == '\n') end1
+ else end
+ }
+
+
/* history */
private val document_0 = session.begin_document(buffer.getName)
@@ -127,9 +140,11 @@
/* activation */
+ private val token_marker = new Isabelle_Token_Marker(this)
+
def activate()
{
- buffer.setTokenMarker(new Isabelle_Token_Marker(this))
+ buffer.setTokenMarker(token_marker)
buffer.addBufferListener(buffer_listener)
buffer.propertiesChanged()
@@ -137,6 +152,11 @@
edits_delay()
}
+ def refresh()
+ {
+ buffer.setTokenMarker(token_marker)
+ }
+
def deactivate()
{
buffer.setTokenMarker(buffer.getMode.getTokenMarker)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Jun 29 07:55:18 2010 +0200
@@ -129,16 +129,20 @@
val document = model.recent_document()
def from_current(pos: Int) = model.from_current(document, pos)
def to_current(pos: Int) = model.to_current(document, pos)
- val metrics = text_area.getPainter.getFontMetrics
+
+ val line_end = model.visible_line_end(start, end)
+ val line_height = text_area.getPainter.getFontMetrics.getHeight
+
val saved_color = gfx.getColor
try {
for ((command, command_start) <-
- document.command_range(from_current(start), from_current(end)) if !command.is_ignored)
+ document.command_range(from_current(start), from_current(line_end)) if !command.is_ignored)
{
- val begin = start max to_current(command_start)
- val finish = (end - 1) min to_current(command_start + command.length)
- encolor(gfx, y, metrics.getHeight, begin, finish,
- Document_View.choose_color(document, command), true)
+ val p = text_area.offsetToXY(start max to_current(command_start))
+ val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+ assert(p.y == q.y)
+ gfx.setColor(Document_View.choose_color(document, command))
+ gfx.fillRect(p.x, y, q.x - p.x, line_height)
}
}
finally { gfx.setColor(saved_color) }
@@ -205,26 +209,6 @@
text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
text_area.getLastPhysicalLine)
- private def encolor(gfx: Graphics2D,
- y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
- {
- val start = text_area.offsetToXY(begin)
- val stop =
- if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
- else {
- val p = text_area.offsetToXY(finish - 1)
- val metrics = text_area.getPainter.getFontMetrics
- p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
- p
- }
-
- if (start != null && stop != null) {
- gfx.setColor(color)
- if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
- else gfx.drawRect(start.x, y, stop.x - start.x, height)
- }
- }
-
/* overview of command status left of scrollbar */
--- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Jun 28 15:32:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue Jun 29 07:55:18 2010 +0200
@@ -20,7 +20,7 @@
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
@@ -203,6 +203,13 @@
override def handleMessage(message: EBMessage)
{
message match {
+ case msg: BufferUpdate
+ if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+ Document_Model(msg.getBuffer) match {
+ case Some(model) => model.refresh()
+ case _ =>
+ }
+
case msg: EditPaneUpdate =>
val edit_pane = msg.getEditPane
val buffer = edit_pane.getBuffer