# HG changeset patch # User wenzelm # Date 1285000109 -7200 # Node ID 0fa447d9aa2ede3850ea301c421a1b5215e5c6bf # Parent be44a81ca5abe022c88c4dfbf64b819971639923# Parent fe5722fce758ef2b2a8cd2fcb4f40bd982d6c712 merged diff -r fe5722fce758 -r 0fa447d9aa2e doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Mon Sep 20 16:05:25 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Mon Sep 20 18:28:29 2010 +0200 @@ -103,7 +103,7 @@ interpretation %quote fun_power: power "\n (f :: 'a \ 'a). f ^^ n" where "power.powers (\n f. f ^^ n) = funpows" by unfold_locales - (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def) + (simp_all add: fun_eq_iff funpow_mult mult_commute funpows_def) text {* \noindent This additional equation is trivially proved by the definition diff -r fe5722fce758 -r 0fa447d9aa2e doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Mon Sep 20 16:05:25 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Mon Sep 20 18:28:29 2010 +0200 @@ -191,7 +191,7 @@ \ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline \ \ \isacommand{by}\isamarkupfalse% \ unfold{\isacharunderscore}locales\isanewline -\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}% +\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fun{\isacharunderscore}eq{\isacharunderscore}iff\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}% \endisatagquote {\isafoldquote}% % diff -r fe5722fce758 -r 0fa447d9aa2e src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 20 16:05:25 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 20 18:28:29 2010 +0200 @@ -34,9 +34,6 @@ Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th | _ => th -(*To enforce single-threading*) -exception Clausify_failure of theory; - (**** SKOLEMIZATION BY INFERENCE (lcp) ****) diff -r fe5722fce758 -r 0fa447d9aa2e src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 20 16:05:25 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Sep 20 18:28:29 2010 +0200 @@ -138,7 +138,8 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -val preproc_ss = HOL_basic_ss addsimps @{thms all_simps [symmetric]} +val preproc_ss = + HOL_basic_ss addsimps @{thms all_simps[symmetric] ex_simps[symmetric]} fun generic_metis_tac mode ctxt ths i st0 = let @@ -149,13 +150,12 @@ (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) else Tactical.SOLVED' - ((TRY o Simplifier.simp_tac preproc_ss) - THEN' - (REPEAT_DETERM o match_tac @{thms allI}) - THEN' - TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) - (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) - ctxt) i st0 + ((TRY o Simplifier.full_simp_tac preproc_ss) + THEN' (REPEAT_DETERM o match_tac @{thms allI}) + THEN' (REPEAT_DETERM o ematch_tac @{thms exE}) + THEN' (TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) + (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) + ctxt)) i st0 end val metis_tac = generic_metis_tac HO diff -r fe5722fce758 -r 0fa447d9aa2e src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Mon Sep 20 16:05:25 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Mon Sep 20 18:28:29 2010 +0200 @@ -130,32 +130,30 @@ fun markup_stmt name = Print_Mode.setmp [code_presentationN] (Pretty.mark (code_presentationN, [(stmt_nameN, name)])); -fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) = - implode (map (filter_presentation presentation_names - (selected orelse (name = code_presentationN - andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs) - | filter_presentation presentation_names selected (XML.Text s) = - if selected then s else ""; - -fun maps_string s f [] = "" - | maps_string s f (x :: xs) = +fun filter_presentation [] tree = + Buffer.empty + |> fold XML.add_content tree + |> Buffer.add "\n" + | filter_presentation presentation_names tree = let - val s1 = f x; - val s2 = maps_string s f xs; - in if s1 = "" then s2 - else if s2 = "" then s1 - else s1 ^ s ^ s2 - end; - -fun plain_text (XML.Elem (_, xs)) = maps_string "" plain_text xs - | plain_text (XML.Text s) = s + fun is_selected (name, attrs) = + name = code_presentationN + andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN)); + fun add_content_with_space tree (is_first, buf) = + buf + |> not is_first ? Buffer.add "\n\n" + |> XML.add_content tree + |> pair false; + fun filter (XML.Elem (name_attrs, xs)) = + fold (if is_selected name_attrs then add_content_with_space else filter) xs + | filter (XML.Text s) = I; + in snd (fold filter tree (true, Buffer.empty)) end; fun format presentation_names width = Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) #> YXML.parse_body - #> (if null presentation_names then maps_string "" plain_text - else maps_string "\n\n" (filter_presentation presentation_names false)) - #> suffix "\n"; + #> filter_presentation presentation_names + #> Buffer.content; (** names and variable name contexts **)