--- a/doc-src/Codegen/Thy/Adaptation.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Mon Sep 27 14:54:10 2010 +0200
@@ -190,9 +190,9 @@
"bool"}, we may use \qn{custom serialisations}:
*}
-code_type %quotett bool
+code_type %quote %tt bool
(SML "bool")
-code_const %quotett True and False and "op \<and>"
+code_const %quote %tt True and False and "op \<and>"
(SML "true" and "false" and "_ andalso _")
text {*
@@ -218,7 +218,7 @@
precedences which may be used here:
*}
-code_const %quotett "op \<and>"
+code_const %quote %tt "op \<and>"
(SML infixl 1 "andalso")
text %quote %typewriter {*
@@ -247,9 +247,9 @@
code_const %invisible Pair
(SML)
(*>*)
-code_type %quotett prod
+code_type %quote %tt prod
(SML infix 2 "*")
-code_const %quotett Pair
+code_const %quote %tt Pair
(SML "!((_),/ (_))")
text {*
@@ -283,10 +283,10 @@
@{command_def code_class}) and its operation @{const [source] HOL.equal}
*}
-code_class %quotett equal
+code_class %quote %tt equal
(Haskell "Eq")
-code_const %quotett "HOL.equal"
+code_const %quote %tt "HOL.equal"
(Haskell infixl 4 "==")
text {*
@@ -307,7 +307,7 @@
end %quote (*<*)
-(*>*) code_type %quotett bar
+(*>*) code_type %quote %tt bar
(Haskell "Integer")
text {*
@@ -316,7 +316,7 @@
suppress this additional instance, use @{command_def "code_instance"}:
*}
-code_instance %quotett bar :: equal
+code_instance %quote %tt bar :: equal
(Haskell -)
@@ -328,10 +328,10 @@
"code_include"} command:
*}
-code_include %quotett Haskell "Errno"
+code_include %quote %tt Haskell "Errno"
{*errno i = error ("Error number: " ++ show i)*}
-code_reserved %quotett Haskell Errno
+code_reserved %quote %tt Haskell Errno
text {*
\noindent Such named @{text include}s are then prepended to every
--- a/doc-src/Codegen/Thy/Evaluation.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy Mon Sep 27 14:54:10 2010 +0200
@@ -206,7 +206,7 @@
datatype %quote form = T | F | And form form | Or form form (*<*)
-(*>*) ML %quotett {*
+(*>*) ML %tt %quote {*
fun eval_form @{code T} = true
| eval_form @{code F} = false
| eval_form (@{code And} (p, q)) =
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Mon Sep 27 14:34:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Mon Sep 27 14:54:10 2010 +0200
@@ -281,23 +281,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bool\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} command takes a type constructor
@@ -354,20 +354,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\isadelimtypewriter
%
@@ -447,23 +447,23 @@
%
\endisadeliminvisible
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ prod\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ Pair\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent The initial bang ``\verb|!|'' tells the serialiser
@@ -499,11 +499,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
\ equal\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -511,12 +511,12 @@
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}HOL{\isachardot}equal{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent A problem now occurs whenever a type which is an instance
@@ -553,20 +553,20 @@
%
\endisadelimquote
%
-\isadelimquotett
+\isadelimtt
\ %
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bar\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent The code generator would produce an additional instance,
@@ -575,20 +575,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
\ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline
\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
}
@@ -600,23 +600,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}include}\isamarkupfalse%
\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
\isanewline
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
\ Haskell\ Errno%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent Such named \isa{include}s are then prepended to every
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Mon Sep 27 14:34:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Mon Sep 27 14:54:10 2010 +0200
@@ -269,20 +269,7 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimquotett
-\ %
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
\ {\isacharverbatimopen}\isanewline
\ \ fun\ eval{\isacharunderscore}form\ %
\isaantiq
@@ -307,12 +294,12 @@
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquotett
+\isadelimquote
%
-\endisadelimquotett
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent \isa{code} takes as argument the name of a constant;
--- a/doc-src/Codegen/style.sty Mon Sep 27 14:34:55 2010 +0200
+++ b/doc-src/Codegen/style.sty Mon Sep 27 14:54:10 2010 +0200
@@ -37,9 +37,8 @@
\renewcommand{\isatagtypewriter}{\begin{typewriter}}
\renewcommand{\endisatagtypewriter}{\end{typewriter}}
-\isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quote}}
+\isakeeptag{tt}
+\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
%% a trick
\newcommand{\isasymSML}{SML}
--- a/src/HOL/HOL.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/HOL.thy Mon Sep 27 14:54:10 2010 +0200
@@ -1915,7 +1915,7 @@
and infixl 1 "andalso" and infixl 0 "orelse"
and "!(if (_)/ then (_)/ else (_))")
(OCaml "true" and "false" and "not"
- and infixl 4 "&&" and infixl 2 "||"
+ and infixl 3 "&&" and infixl 2 "||"
and "!(if (_)/ then (_)/ else (_))")
(Haskell "True" and "False" and "not"
and infixl 3 "&&" and infixl 2 "||"
@@ -1980,9 +1980,11 @@
*} "solve goal by normalization"
+(*
subsection {* Try *}
setup {* Try.setup *}
+*)
subsection {* Counterexample Search Units *}
--- a/src/HOL/Imperative_HOL/Array.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Mon Sep 27 14:54:10 2010 +0200
@@ -449,6 +449,7 @@
code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (SML infixl 6 "=")
code_reserved SML Array
@@ -464,6 +465,7 @@
code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (OCaml infixl 4 "=")
code_reserved OCaml Array
@@ -478,6 +480,8 @@
code_const Array.len' (Haskell "Heap.lengthArray")
code_const Array.nth' (Haskell "Heap.readArray")
code_const Array.upd' (Haskell "Heap.writeArray")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Haskell infix 4 "==")
+code_instance array :: HOL.equal (Haskell -)
text {* Scala *}
@@ -490,5 +494,6 @@
code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Scala infixl 5 "==")
end
--- a/src/HOL/Imperative_HOL/Overview.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy Mon Sep 27 14:54:10 2010 +0200
@@ -138,6 +138,9 @@
Provided proof rules are such that they reduce monad operations to
operations on bare heaps.
+
+ Note that HOL equality coincides with reference equality and may be
+ used as primitive executable operation.
*}
subsection {* Arrays *}
--- a/src/HOL/Imperative_HOL/Ref.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Mon Sep 27 14:54:10 2010 +0200
@@ -282,6 +282,7 @@
code_const ref' (Eval "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (SML infixl 6 "=")
code_reserved Eval Unsynchronized
@@ -293,6 +294,7 @@
code_const ref' (OCaml "(fun/ ()/ ->/ ref/ _)")
code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (OCaml infixl 4 "=")
code_reserved OCaml ref
@@ -304,6 +306,8 @@
code_const ref' (Haskell "Heap.newSTRef")
code_const Ref.lookup (Haskell "Heap.readSTRef")
code_const Ref.update (Haskell "Heap.writeSTRef")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Haskell infix 4 "==")
+code_instance ref :: HOL.equal (Haskell -)
text {* Scala *}
@@ -313,5 +317,6 @@
code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Scala infixl 5 "==")
end
--- a/src/HOL/IsaMakefile Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Sep 27 14:54:10 2010 +0200
@@ -316,8 +316,7 @@
Tools/recdef.ML \
Tools/record.ML \
Tools/semiring_normalizer.ML \
- Tools/Sledgehammer/clausifier.ML \
- Tools/Sledgehammer/meson_tactic.ML \
+ Tools/Sledgehammer/meson_clausifier.ML \
Tools/Sledgehammer/metis_reconstruct.ML \
Tools/Sledgehammer/metis_translate.ML \
Tools/Sledgehammer/metis_tactics.ML \
--- a/src/HOL/Library/Dlist.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Sep 27 14:54:10 2010 +0200
@@ -35,6 +35,10 @@
"list_of_dlist (Dlist xs) = remdups xs"
by (simp add: Dlist_def Abs_dlist_inverse)
+lemma remdups_list_of_dlist [simp]:
+ "remdups (list_of_dlist dxs) = list_of_dlist dxs"
+ by simp
+
lemma Dlist_list_of_dlist [simp, code abstype]:
"Dlist (list_of_dlist dxs) = dxs"
by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)
--- a/src/HOL/List.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/List.thy Mon Sep 27 14:54:10 2010 +0200
@@ -2862,6 +2862,10 @@
with `distinct xs` show ?thesis by simp
qed
+lemma remdups_map_remdups:
+ "remdups (map f (remdups xs)) = remdups (map f xs)"
+ by (induct xs) simp_all
+
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Sep 27 14:54:10 2010 +0200
@@ -102,7 +102,7 @@
{ensure_groundness = true,
limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
- (["accepts", "acceptsaux", "acceptsauxauxa", "acceptsauxaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
+ (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
replacing =
[(("repP", "limited_repP"), "lim_repIntPa"),
(("subP", "limited_subP"), "repIntP"),
--- a/src/HOL/Sledgehammer.thy Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Sep 27 14:54:10 2010 +0200
@@ -14,8 +14,7 @@
("Tools/ATP/atp_proof.ML")
("Tools/ATP/atp_systems.ML")
("~~/src/Tools/Metis/metis.ML")
- ("Tools/Sledgehammer/clausifier.ML")
- ("Tools/Sledgehammer/meson_tactic.ML")
+ ("Tools/Sledgehammer/meson_clausifier.ML")
("Tools/Sledgehammer/metis_translate.ML")
("Tools/Sledgehammer/metis_reconstruct.ML")
("Tools/Sledgehammer/metis_tactics.ML")
@@ -99,9 +98,8 @@
setup ATP_Systems.setup
use "~~/src/Tools/Metis/metis.ML"
-use "Tools/Sledgehammer/clausifier.ML"
-use "Tools/Sledgehammer/meson_tactic.ML"
-setup Meson_Tactic.setup
+use "Tools/Sledgehammer/meson_clausifier.ML"
+setup Meson_Clausifier.setup
use "Tools/Sledgehammer/metis_translate.ML"
use "Tools/Sledgehammer/metis_reconstruct.ML"
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Sep 27 14:54:10 2010 +0200
@@ -315,8 +315,9 @@
val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
in clause end
- val res = (map translate_intro intros', constant_table')
- in res end
+ in
+ (map translate_intro intros', constant_table')
+ end
fun depending_preds_of (key, intros) =
fold Term.add_const_names (map Thm.prop_of intros) []
@@ -669,7 +670,9 @@
|> (if #ensure_groundness options then
add_ground_predicates ctxt (#limited_types options)
else I)
+ |> tap (fn _ => tracing "Adding limited predicates...")
|> add_limited_predicates (#limited_predicates options)
+ |> tap (fn _ => tracing "Replacing predicates...")
|> apfst (fold replace (#replacing options))
|> apfst (reorder_manually (#manual_reorder options))
|> apfst rename_vars_program
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 27 14:54:10 2010 +0200
@@ -94,6 +94,56 @@
error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false
+fun try_destruct_case thy names atom =
+ case find_split_thm thy (fst (strip_comb atom)) of
+ NONE => NONE
+ | SOME raw_split_thm =>
+ let
+ val case_name = fst (dest_Const (fst (strip_comb atom)))
+ val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
+ (* TODO: contextify things - this line is to unvarify the split_thm *)
+ (*val ((_, [isplit_thm]), _) =
+ Variable.import true [split_thm] (ProofContext.init_global thy)*)
+ val (assms, concl) = Logic.strip_horn (prop_of split_thm)
+ val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val Tcons = datatype_names_of_case_name thy case_name
+ val ths = maps (instantiated_case_rewrites thy) Tcons
+ val atom' = MetaSimplifier.rewrite_term thy
+ (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
+ val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
+ val names' = Term.add_free_names atom' names
+ fun mk_subst_rhs assm =
+ let
+ val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
+ val var_names = Name.variant_list names' (map fst vTs)
+ val vars = map Free (var_names ~~ (map snd vTs))
+ val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
+ fun partition_prem_subst prem =
+ case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
+ (Free (x, T), r) => (NONE, SOME ((x, T), r))
+ | _ => (SOME prem, NONE)
+ fun partition f xs =
+ let
+ fun partition' acc1 acc2 [] = (rev acc1, rev acc2)
+ | partition' acc1 acc2 (x :: xs) =
+ let
+ val (y, z) = f x
+ val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1
+ val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2
+ in partition' acc1' acc2' xs end
+ in partition' [] [] xs end
+ val (prems'', subst) = partition partition_prem_subst prems'
+ val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
+ val pre_rhs =
+ fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t
+ val rhs = Envir.expand_term_frees subst pre_rhs
+ in
+ case try_destruct_case thy (var_names @ names') rhs of
+ NONE => [(subst, rhs)]
+ | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs
+ end
+ in SOME (atom', maps mk_subst_rhs assms) end
+
fun flatten constname atom (defs, thy) =
if is_compound atom then
let
@@ -124,62 +174,20 @@
flatten constname atom' (defs, thy)
end
| _ =>
- case find_split_thm thy (fst (strip_comb atom)) of
+ case try_destruct_case thy [] atom of
NONE => (atom, (defs, thy))
- | SOME raw_split_thm =>
- let
- val (f, args) = strip_comb atom
- val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
- (* TODO: contextify things - this line is to unvarify the split_thm *)
- (*val ((_, [isplit_thm]), _) =
- Variable.import true [split_thm] (ProofContext.init_global thy)*)
- val (assms, concl) = Logic.strip_horn (prop_of split_thm)
- val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
- val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
- val ths = maps (instantiated_case_rewrites thy) Tcons
- val atom = MetaSimplifier.rewrite_term thy
- (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
- val (f, args) = strip_comb atom
- val subst = Pattern.match thy (split_t, atom) (Vartab.empty, Vartab.empty)
- val (_, split_args) = strip_comb split_t
- val match = split_args ~~ args
- val names = Term.add_free_names atom []
- val frees = map Free (Term.add_frees atom [])
+ | SOME (atom', srs) =>
+ let
+ val frees = map Free (Term.add_frees atom' [])
val constname = Name.variant (map (Long_Name.base_name o fst) defs)
- ((Long_Name.base_name constname) ^ "_aux")
+ ((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
val constT = map fastype_of frees ---> HOLogic.boolT
val lhs = list_comb (Const (full_constname, constT), frees)
- fun new_def assm =
- let
- val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
- val var_names = Name.variant_list names (map fst vTs)
- val vars = map Free (var_names ~~ (map snd vTs))
- val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
- fun partition_prem_subst prem =
- case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
- (Free (x, T), r) => (NONE, SOME ((x, T), r))
- | _ => (SOME prem, NONE)
- fun partition f xs =
- let
- fun partition' acc1 acc2 [] = (rev acc1, rev acc2)
- | partition' acc1 acc2 (x :: xs) =
- let
- val (y, z) = f x
- val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1
- val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2
- in partition' acc1' acc2' xs end
- in partition' [] [] xs end
- val (prems'', subst) = partition partition_prem_subst prems'
- val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
- val pre_def = Logic.mk_equals (lhs,
- fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t)
- val def = Envir.expand_term_frees subst pre_def
- in
- def
- end
- val new_defs = map new_def assms
- val (definition, thy') = thy
+ fun mk_def (subst, rhs) =
+ Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
+ val new_defs = map mk_def srs
+ val (definition, thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
|> fold_map Specification.axiom (map_index
(fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 27 14:34:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,254 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/clausifier.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-Transformation of axiom rules (elim/intro/etc) into CNF forms.
-*)
-
-signature CLAUSIFIER =
-sig
- val extensionalize_theorem : thm -> thm
- val introduce_combinators_in_cterm : cterm -> thm
- val introduce_combinators_in_theorem : thm -> thm
- val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
- val cnf_axiom : theory -> thm -> thm list
-end;
-
-structure Clausifier : CLAUSIFIER =
-struct
-
-(**** 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. (Cf. "transform_elim_term" in
- "Sledgehammer_Util".) *)
-fun transform_elim_theorem 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
-
-
-(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
-
-fun mk_skolem t =
- let val T = fastype_of t in
- Const (@{const_name skolem}, T --> T) $ t
- end
-
-fun beta_eta_under_lambdas (Abs (s, T, t')) =
- Abs (s, T, beta_eta_under_lambdas t')
- | beta_eta_under_lambdas t = Envir.beta_eta_contract t
-
-(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs th =
- let
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val args = OldTerm.term_frees body
- (* Forms a lambda-abstraction over the formal parameters *)
- val rhs =
- list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ beta_eta_under_lambdas body)
- |> mk_skolem
- val comb = list_comb (rhs, args)
- in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
- | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
- (*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)) rhss end
- | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
- | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
- | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
- | dec_sko _ rhss = rhss
- in dec_sko (prop_of th) [] end;
-
-
-(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
-
-val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
-
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
-fun extensionalize_theorem th =
- case prop_of th of
- _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
- $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
- | _ => th
-
-fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = 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
- val 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 introduce_combinators_in_cterm 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 = introduce_combinators_in_cterm 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 (introduce_combinators_in_cterm ct1)
- (introduce_combinators_in_cterm ct2)
- end
-
-fun introduce_combinators_in_theorem th =
- if is_quasi_lambda_free (prop_of th) then
- th
- else
- let
- val th = Drule.eta_contraction_rule th
- val eqth = introduce_combinators_in_cterm (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 = cterm_of @{theory HOL} HOLogic.Trueprop;
-
-(*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);
-
-val skolem_def_raw = @{thms skolem_def_raw}
-
-(* 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 thy rhs0 =
- let
- val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
- val rhs' = rhs |> Thm.dest_comb |> snd
- val (ch, frees) = c_variant_abs_multi (rhs', [])
- val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
- val T =
- case hilbert of
- Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
- | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
- val cex = cterm_of thy (HOLogic.exists_const T)
- val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
- val conc =
- Drule.list_comb (rhs, frees)
- |> Drule.beta_conv cabs |> Thm.capply cTrueprop
- fun tacf [prem] =
- rewrite_goals_tac skolem_def_raw
- THEN rtac ((prem |> rewrite_rule skolem_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_theorem |> zero_var_indexes
- val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize_theorem
- |> Meson.make_nnf ctxt
- in (th3, ctxt) end
-
-fun to_definitional_cnf_with_quantifiers thy th =
- let
- val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
- val eqth = eqth RS @{thm eq_reflection}
- val eqth = eqth RS @{thm TruepropI}
- in Thm.equal_elim eqth th end
-
-(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
-fun cnf_axiom thy th =
- let
- val ctxt0 = Variable.global_thm_context th
- val (nnf_th, ctxt) = to_nnf th ctxt0
- fun aux th =
- Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
- th ctxt
- val (cnf_ths, ctxt) =
- aux nnf_th
- |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
- | p => p)
- in
- cnf_ths |> map introduce_combinators_in_theorem
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation
- end
- handle THM _ => []
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Mon Sep 27 14:54:10 2010 +0200
@@ -0,0 +1,267 @@
+(* Title: HOL/Tools/Sledgehammer/clausifier.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
+ Author: Jasmin Blanchette, TU Muenchen
+
+Transformation of axiom rules (elim/intro/etc) into CNF forms.
+*)
+
+signature MESON_CLAUSIFIER =
+sig
+ val extensionalize_theorem : thm -> thm
+ val introduce_combinators_in_cterm : cterm -> thm
+ val introduce_combinators_in_theorem : thm -> thm
+ val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
+ val meson_cnf_axiom : theory -> thm -> thm list
+ val meson_general_tac : Proof.context -> thm list -> int -> tactic
+ val setup: theory -> theory
+end;
+
+structure Meson_Clausifier : MESON_CLAUSIFIER =
+struct
+
+(**** 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. (Cf. "transform_elim_term" in
+ "Sledgehammer_Util".) *)
+fun transform_elim_theorem 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
+
+
+(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
+
+fun mk_skolem t =
+ let val T = fastype_of t in
+ Const (@{const_name skolem}, T --> T) $ t
+ end
+
+fun beta_eta_under_lambdas (Abs (s, T, t')) =
+ Abs (s, T, beta_eta_under_lambdas t')
+ | beta_eta_under_lambdas t = Envir.beta_eta_contract t
+
+(*Traverse a theorem, accumulating Skolem function definitions.*)
+fun assume_skolem_funs th =
+ let
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val args = OldTerm.term_frees body
+ (* Forms a lambda-abstraction over the formal parameters *)
+ val rhs =
+ list_abs_free (map dest_Free args,
+ HOLogic.choice_const T $ beta_eta_under_lambdas body)
+ |> mk_skolem
+ val comb = list_comb (rhs, args)
+ in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
+ (*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)) rhss end
+ | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
+ | dec_sko _ rhss = rhss
+ in dec_sko (prop_of th) [] end;
+
+
+(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
+
+val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
+fun extensionalize_theorem th =
+ case prop_of th of
+ _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
+ $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
+ | _ => th
+
+fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = 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
+ val 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 introduce_combinators_in_cterm 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 = introduce_combinators_in_cterm 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 (introduce_combinators_in_cterm ct1)
+ (introduce_combinators_in_cterm ct2)
+ end
+
+fun introduce_combinators_in_theorem th =
+ if is_quasi_lambda_free (prop_of th) then
+ th
+ else
+ let
+ val th = Drule.eta_contraction_rule th
+ val eqth = introduce_combinators_in_cterm (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 = cterm_of @{theory HOL} HOLogic.Trueprop;
+
+(*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);
+
+val skolem_def_raw = @{thms skolem_def_raw}
+
+(* 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 thy rhs0 =
+ let
+ val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
+ val rhs' = rhs |> Thm.dest_comb |> snd
+ val (ch, frees) = c_variant_abs_multi (rhs', [])
+ val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
+ val T =
+ case hilbert of
+ Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
+ val cex = cterm_of thy (HOLogic.exists_const T)
+ val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
+ val conc =
+ Drule.list_comb (rhs, frees)
+ |> Drule.beta_conv cabs |> Thm.capply cTrueprop
+ fun tacf [prem] =
+ rewrite_goals_tac skolem_def_raw
+ THEN rtac ((prem |> rewrite_rule skolem_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_theorem |> zero_var_indexes
+ val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize_theorem
+ |> Meson.make_nnf ctxt
+ in (th3, ctxt) end
+
+fun to_definitional_cnf_with_quantifiers thy th =
+ let
+ val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
+ val eqth = eqth RS @{thm eq_reflection}
+ val eqth = eqth RS @{thm TruepropI}
+ in Thm.equal_elim eqth th end
+
+(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
+fun meson_cnf_axiom thy th =
+ let
+ val ctxt0 = Variable.global_thm_context th
+ val (nnf_th, ctxt) = to_nnf th ctxt0
+ fun aux th =
+ Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
+ th ctxt
+ val (cnf_ths, ctxt) =
+ aux nnf_th
+ |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
+ | p => p)
+ in
+ cnf_ths |> map introduce_combinators_in_theorem
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation
+ end
+ handle THM _ => []
+
+fun meson_general_tac ctxt ths =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ctxt0 = Classical.put_claset HOL_cs ctxt
+ in Meson.meson_tac ctxt0 (maps (meson_cnf_axiom thy) ths) end
+
+val setup =
+ Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
+ SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+ "MESON resolution proof procedure";
+
+end;
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Sep 27 14:34:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-MESON general tactic and proof method.
-*)
-
-signature MESON_TACTIC =
-sig
- val meson_general_tac : Proof.context -> thm list -> int -> tactic
- val setup: theory -> theory
-end;
-
-structure Meson_Tactic : MESON_TACTIC =
-struct
-
-fun meson_general_tac ctxt ths =
- let
- val thy = ProofContext.theory_of ctxt
- val ctxt0 = Classical.put_claset HOL_cs ctxt
- in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
-
-val setup =
- Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
- SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
- "MESON resolution proof procedure";
-
-end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 27 14:54:10 2010 +0200
@@ -56,7 +56,8 @@
let val thy = ProofContext.theory_of ctxt
val type_lits = Config.get ctxt type_lits
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0
+ map (fn th => (Thm.get_name_hint th,
+ Meson_Clausifier.meson_cnf_axiom thy th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
@@ -116,7 +117,7 @@
does, but also keep an unextensionalized version of "th" for backward
compatibility. *)
fun also_extensionalize_theorem th =
- let val th' = Clausifier.extensionalize_theorem th in
+ let val th' = Meson_Clausifier.extensionalize_theorem th in
if Thm.eq_thm (th, th') then [th]
else th :: Meson.make_clauses_unsorted [th']
end
@@ -125,7 +126,7 @@
single
#> Meson.make_clauses_unsorted
#> maps also_extensionalize_theorem
- #> map Clausifier.introduce_combinators_in_theorem
+ #> map Meson_Clausifier.introduce_combinators_in_theorem
#> Meson.finish_cnf
fun preskolem_tac ctxt st0 =
--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Mon Sep 27 14:54:10 2010 +0200
@@ -554,7 +554,8 @@
Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
(*The fully-typed translation, to avoid type errors*)
-fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
+fun wrap_type (tm, ty) =
+ Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
| hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 27 14:54:10 2010 +0200
@@ -740,8 +740,7 @@
let
val multi = length ths > 1
fun backquotify th =
- "`" ^ Print_Mode.setmp (Print_Mode.input ::
- filter (curry (op =) Symbol.xsymbolsN)
+ "`" ^ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ()))
(Syntax.string_of_term ctxt) (close_form (prop_of th)) ^ "`"
|> String.translate (fn c => if Char.isPrint c then str c else "")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Sep 27 14:54:10 2010 +0200
@@ -228,8 +228,8 @@
| NONE => ~1
in if k >= 0 then [k] else [] end
-val is_axiom = not o null oo resolve_axiom
-val is_conjecture = not o null oo resolve_conjecture
+fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
+fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
fun raw_label_for_name conjecture_shape name =
case resolve_conjecture conjecture_shape name of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Sep 27 14:54:10 2010 +0200
@@ -94,7 +94,7 @@
(0 upto length Ts - 1 ~~ Ts))
(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Clausifier".) *)
+ (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *)
fun extensionalize_term t =
let
fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
@@ -141,7 +141,7 @@
t |> conceal_bounds Ts
|> Envir.eta_contract
|> cterm_of thy
- |> Clausifier.introduce_combinators_in_cterm
+ |> Meson_Clausifier.introduce_combinators_in_cterm
|> prop_of |> Logic.dest_equals |> snd
|> reveal_bounds Ts
val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 27 14:54:10 2010 +0200
@@ -98,7 +98,7 @@
(* 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. (Cf. "transform_elim_theorem" in
- "Clausifier".) *)
+ "Meson_Clausifier".) *)
fun transform_elim_term t =
case Logic.strip_imp_concl t of
@{const Trueprop} $ Var (z, @{typ bool}) =>
--- a/src/HOL/Tools/try.ML Mon Sep 27 14:34:55 2010 +0200
+++ b/src/HOL/Tools/try.ML Mon Sep 27 14:54:10 2010 +0200
@@ -2,18 +2,25 @@
Author: Jasmin Blanchette, TU Muenchen
Try a combination of proof methods.
+
+FIXME: reintroduce or remove commented code (see also HOL.thy)
*)
signature TRY =
sig
+(*
val auto : bool Unsynchronized.ref
+*)
val invoke_try : Time.time option -> Proof.state -> bool
+(*
val setup : theory -> theory
+*)
end;
structure Try : TRY =
struct
+(*
val auto = Unsynchronized.ref false
val _ =
@@ -21,6 +28,7 @@
(Unsynchronized.setmp auto true (fn () =>
Preferences.bool_pref auto
"auto-try" "Try standard proof methods.") ());
+*)
val default_timeout = Time.fromSeconds 5
@@ -108,8 +116,10 @@
(Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
o Toplevel.proof_of)))
+(*
fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
val setup = Auto_Tools.register_tool (tryN, auto_try)
+*)
end;
--- a/src/Tools/Code/lib/Tools/codegen Mon Sep 27 14:34:55 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Mon Sep 27 14:54:10 2010 +0200
@@ -50,8 +50,8 @@
## invoke code generation
-FORMAL_CMD="Toplevel.program (fn () => use_thy thyname; ML_Context.eval_text_in \
- (SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd) \
+FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
+ (SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
handle _ => OS.Process.exit OS.Process.failure;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \