# HG changeset patch # User wenzelm # Date 1285592050 -7200 # Node ID 6a64f04cb648b96dde8487e33dbffa7d2fabef51 # Parent 832c42be723e09933bc884376c0bf73bc601eede# Parent 1fa4c5c7d53412b630ca72e72c9724115d69512d merged diff -r 1fa4c5c7d534 -r 6a64f04cb648 doc-src/Codegen/Thy/Adaptation.thy --- 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 \" +code_const %quote %tt True and False and "op \" (SML "true" and "false" and "_ andalso _") text {* @@ -218,7 +218,7 @@ precedences which may be used here: *} -code_const %quotett "op \" +code_const %quote %tt "op \" (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 diff -r 1fa4c5c7d534 -r 6a64f04cb648 doc-src/Codegen/Thy/Evaluation.thy --- 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)) = diff -r 1fa4c5c7d534 -r 6a64f04cb648 doc-src/Codegen/Thy/document/Adaptation.tex --- 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 diff -r 1fa4c5c7d534 -r 6a64f04cb648 doc-src/Codegen/Thy/document/Evaluation.tex --- 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; diff -r 1fa4c5c7d534 -r 6a64f04cb648 doc-src/Codegen/style.sty --- 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} diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/HOL.thy --- 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 *} diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Imperative_HOL/Array.thy --- 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 \ 'a array \ 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 \ 'a array \ 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 \ 'a array \ 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 \ 'a array \ bool" (Scala infixl 5 "==") end diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Imperative_HOL/Overview.thy --- 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 *} diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Imperative_HOL/Ref.thy --- 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 \ 'a ref \ 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 \ 'a ref \ 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 \ 'a ref \ 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 \ 'a ref \ bool" (Scala infixl 5 "==") end diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/IsaMakefile --- 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 \ diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Library/Dlist.thy --- 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) diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/List.thy --- 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"\"}*} diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- 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"), diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Sledgehammer.thy --- 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" diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Predicate_Compile/code_prolog.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 diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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) diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/clausifier.ML --- 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; diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/meson_clausifier.ML --- /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; diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/meson_tactic.ML --- 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; diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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 = diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/metis_translate.ML --- 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, _)) = diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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 "") diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- 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 diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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}) => diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/HOL/Tools/try.ML --- 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; diff -r 1fa4c5c7d534 -r 6a64f04cb648 src/Tools/Code/lib/Tools/codegen --- 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\"; \