# HG changeset patch # User nipkow # Date 1298660880 -3600 # Node ID edfc06b8a507b9e89a91fde6ced0b51bb9f3d4ed # Parent f53e0e0baa4f331c9bf4907a44ca14acd0596f05# Parent 1a65b780bd56d80605e498f0a30db7f14a5bd97d merged diff -r 1a65b780bd56 -r edfc06b8a507 NEWS --- a/NEWS Fri Feb 25 20:07:48 2011 +0100 +++ b/NEWS Fri Feb 25 20:08:00 2011 +0100 @@ -27,6 +27,9 @@ - sledgehammer available_provers ~> sledgehammer supported_provers INCOMPATIBILITY. +* Function package: discontinued option "tailrec". +INCOMPATIBILITY. Use partial_function instead. + *** Document preparation *** diff -r 1a65b780bd56 -r edfc06b8a507 doc-src/Functions/Thy/Functions.thy --- a/doc-src/Functions/Thy/Functions.thy Fri Feb 25 20:07:48 2011 +0100 +++ b/doc-src/Functions/Thy/Functions.thy Fri Feb 25 20:08:00 2011 +0100 @@ -702,11 +702,10 @@ for a zero of a given function f. *} -function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \ nat) \ nat \ nat" +function (*<*)(domintros)(*>*)findzero :: "(nat \ nat) \ nat \ nat" where "findzero f n = (if f n = 0 then n else findzero f (Suc n))" by pat_completeness auto -(*<*)declare findzero.simps[simp del](*>*) text {* \noindent Clearly, any attempt of a termination proof must fail. And without @@ -959,79 +958,6 @@ for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}. *} -(*lemma findzero_nicer_domintros: - "f x = 0 \ findzero_dom (f, x)" - "findzero_dom (f, Suc x) \ findzero_dom (f, x)" -by (rule accpI, erule findzero_rel.cases, auto)+ -*) - -subsection {* A Useful Special Case: Tail recursion *} - -text {* - The domain predicate is our trick that allows us to model partiality - in a world of total functions. The downside of this is that we have - to carry it around all the time. The termination proof above allowed - us to replace the abstract @{term "findzero_dom (f, n)"} by the more - concrete @{term "(x \ n \ f x = (0::nat))"}, but the condition is still - there and can only be discharged for special cases. - In particular, the domain predicate guards the unfolding of our - function, since it is there as a condition in the @{text psimp} - rules. - - Now there is an important special case: We can actually get rid - of the condition in the simplification rules, \emph{if the function - is tail-recursive}. The reason is that for all tail-recursive - equations there is a total function satisfying them, even if they - are non-terminating. - -% A function is tail recursive, if each call to the function is either -% equal -% -% So the outer form of the -% -%if it can be written in the following -% form: -% {term[display] "f x = (if COND x then BASE x else f (LOOP x))"} - - - The function package internally does the right construction and can - derive the unconditional simp rules, if we ask it to do so. Luckily, - our @{const "findzero"} function is tail-recursive, so we can just go - back and add another option to the \cmd{function} command: - -\vspace{1ex} -\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \ nat) \ nat \ nat\""}\\% -\cmd{where}\isanewline% -\ \ \ldots\\% - - - \noindent Now, we actually get unconditional simplification rules, even - though the function is partial: -*} - -thm findzero.simps - -text {* - @{thm[display] findzero.simps} - - \noindent Of course these would make the simplifier loop, so we better remove - them from the simpset: -*} - -declare findzero.simps[simp del] - -text {* - Getting rid of the domain conditions in the simplification rules is - not only useful because it simplifies proofs. It is also required in - order to use Isabelle's code generator to generate ML code - from a function definition. - Since the code generator only works with equations, it cannot be - used with @{text "psimp"} rules. Thus, in order to generate code for - partial functions, they must be defined as a tail recursion. - Luckily, many functions have a relatively natural tail recursive - definition. -*} - section {* Nested recursion *} text {* diff -r 1a65b780bd56 -r edfc06b8a507 doc-src/Functions/Thy/document/Functions.tex --- a/doc-src/Functions/Thy/document/Functions.tex Fri Feb 25 20:07:48 2011 +0100 +++ b/doc-src/Functions/Thy/document/Functions.tex Fri Feb 25 20:08:00 2011 +0100 @@ -1464,78 +1464,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{A Useful Special Case: Tail recursion% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The domain predicate is our trick that allows us to model partiality - in a world of total functions. The downside of this is that we have - to carry it around all the time. The termination proof above allowed - us to replace the abstract \isa{findzero{\isaliteral{5F}{\isacharunderscore}}dom\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}} by the more - concrete \isa{n\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}, but the condition is still - there and can only be discharged for special cases. - In particular, the domain predicate guards the unfolding of our - function, since it is there as a condition in the \isa{psimp} - rules. - - Now there is an important special case: We can actually get rid - of the condition in the simplification rules, \emph{if the function - is tail-recursive}. The reason is that for all tail-recursive - equations there is a total function satisfying them, even if they - are non-terminating. - -% A function is tail recursive, if each call to the function is either -% equal -% -% So the outer form of the -% -%if it can be written in the following -% form: -% {term[display] "f x = (if COND x then BASE x else f (LOOP x))"} - - - The function package internally does the right construction and can - derive the unconditional simp rules, if we ask it to do so. Luckily, - our \isa{findzero} function is tail-recursive, so we can just go - back and add another option to the \cmd{function} command: - -\vspace{1ex} -\noindent\cmd{function} \isa{{\isaliteral{28}{\isacharparenleft}}domintros{\isaliteral{2C}{\isacharcomma}}\ tailrec{\isaliteral{29}{\isacharparenright}}\ findzero\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequote}}}\\% -\cmd{where}\isanewline% -\ \ \ldots\\% - - - \noindent Now, we actually get unconditional simplification rules, even - though the function is partial:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{thm}\isamarkupfalse% -\ findzero{\isaliteral{2E}{\isachardot}}simps% -\begin{isamarkuptext}% -\begin{isabelle}% -findzero\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{3F}{\isacharquery}}n\ else\ findzero\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{3F}{\isacharquery}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% -\end{isabelle} - - \noindent Of course these would make the simplifier loop, so we better remove - them from the simpset:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{declare}\isamarkupfalse% -\ findzero{\isaliteral{2E}{\isachardot}}simps{\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}% -\begin{isamarkuptext}% -Getting rid of the domain conditions in the simplification rules is - not only useful because it simplifies proofs. It is also required in - order to use Isabelle's code generator to generate ML code - from a function definition. - Since the code generator only works with equations, it cannot be - used with \isa{psimp} rules. Thus, in order to generate code for - partial functions, they must be defined as a tail recursion. - Luckily, many functions have a relatively natural tail recursive - definition.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Nested recursion% } \isamarkuptrue% diff -r 1a65b780bd56 -r edfc06b8a507 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 25 20:07:48 2011 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 25 20:08:00 2011 +0100 @@ -444,7 +444,7 @@ ; equations: (thmdecl? prop + '|') ; - functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')' + functionopts: '(' (('sequential' | 'domintros') + ',') ')' ; 'termination' ( term )? \end{rail} @@ -515,14 +515,6 @@ introduction rules for the domain predicate. While mostly not needed, they can be helpful in some proofs about partial functions. - \item @{text tailrec} generates the unconstrained recursive - equations even without a termination proof, provided that the - function is tail-recursive. This currently only works - - \item @{text "default d"} allows to specify a default value for a - (partial) function, which will ensure that @{text "f x = d x"} - whenever @{text "x \ f_dom"}. - \end{description} *} diff -r 1a65b780bd56 -r edfc06b8a507 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 25 20:07:48 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 25 20:08:00 2011 +0100 @@ -454,7 +454,7 @@ ; equations: (thmdecl? prop + '|') ; - functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')' + functionopts: '(' (('sequential' | 'domintros') + ',') ')' ; 'termination' ( term )? \end{rail} @@ -523,14 +523,6 @@ introduction rules for the domain predicate. While mostly not needed, they can be helpful in some proofs about partial functions. - \item \isa{tailrec} generates the unconstrained recursive - equations even without a termination proof, provided that the - function is tail-recursive. This currently only works - - \item \isa{{\isaliteral{22}{\isachardoublequote}}default\ d{\isaliteral{22}{\isachardoublequote}}} allows to specify a default value for a - (partial) function, which will ensure that \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{3D}{\isacharequal}}\ d\ x{\isaliteral{22}{\isachardoublequote}}} - whenever \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. - \end{description}% \end{isamarkuptext}% \isamarkuptrue% diff -r 1a65b780bd56 -r edfc06b8a507 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Fri Feb 25 20:07:48 2011 +0100 +++ b/src/HOL/Tools/Function/fun.ML Fri Feb 25 20:08:00 2011 +0100 @@ -137,7 +137,7 @@ val fun_config = FunctionConfig { sequential=true, default=NONE, - domintros=false, partials=false, tailrec=false } + domintros=false, partials=false } fun gen_add_fun add fixes statements config lthy = let diff -r 1a65b780bd56 -r edfc06b8a507 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Feb 25 20:07:48 2011 +0100 +++ b/src/HOL/Tools/Function/function.ML Fri Feb 25 20:08:00 2011 +0100 @@ -85,11 +85,7 @@ val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec val defname = mk_defname fixes - val FunctionConfig {partials, tailrec, default, ...} = config - val _ = - if tailrec then Output.legacy_feature - "'function (tailrec)' command. Use 'partial_function (tailrec)'." - else () + val FunctionConfig {partials, default, ...} = config val _ = if is_some default then Output.legacy_feature "'function (default)'. Use 'partial_function'." @@ -100,7 +96,7 @@ fun afterqed [[proof]] lthy = let - val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, + val FunctionResult {fs, R, psimps, simple_pinducts, termination, domintros, cases, ...} = cont (Thm.close_derivation proof) @@ -115,9 +111,6 @@ lthy |> addsmps (conceal_partial o Binding.qualify false "partial") "psimps" conceal_partial psimp_attribs psimps - ||> (case trsimps of NONE => I | SOME thms => - addsmps I "simps" I simp_attribs thms #> snd - #> Spec_Rules.add Spec_Rules.Equational (fs, thms)) ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), [Attrib.internal (K (Rule_Cases.case_names cnames)), Attrib.internal (K (Rule_Cases.consumes 1)), diff -r 1a65b780bd56 -r edfc06b8a507 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Fri Feb 25 20:07:48 2011 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Fri Feb 25 20:08:00 2011 +0100 @@ -87,10 +87,7 @@ {fs: term list, G: term, R: term, - psimps : thm list, - trsimps : thm list option, - simple_pinducts : thm list, cases : thm, termination : thm, @@ -187,29 +184,25 @@ | Default of string | DomIntros | No_Partials - | Tailrec datatype function_config = FunctionConfig of {sequential: bool, default: string option, domintros: bool, - partials: bool, - tailrec: bool} + partials: bool} -fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) = - FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec} - | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) = - FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, tailrec=tailrec} - | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) = - FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec} - | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) = - FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true} - | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) = - FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true} +fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) = + FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials} + | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) = + FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials} + | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) = + FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials} + | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) = + FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false} val default_config = FunctionConfig { sequential=false, default=NONE, - domintros=false, partials=true, tailrec=false } + domintros=false, partials=true} (* Analyzing function equations *) @@ -344,8 +337,7 @@ ((Parse.reserved "sequential" >> K Sequential) || ((Parse.reserved "default" |-- Parse.term) >> Default) || (Parse.reserved "domintros" >> K DomIntros) - || (Parse.reserved "no_partials" >> K No_Partials) - || (Parse.reserved "tailrec" >> K Tailrec)) + || (Parse.reserved "no_partials" >> K No_Partials)) fun config_parser default = (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) diff -r 1a65b780bd56 -r edfc06b8a507 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Fri Feb 25 20:07:48 2011 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Fri Feb 25 20:08:00 2011 +0100 @@ -817,61 +817,9 @@ -(* Tail recursion (probably very fragile) - * - * FIXME: - * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context. - * - Must we really replace the fvar by f here? - * - Splitting is not configured automatically: Problems with case? - *) -fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps = - let - val Globals {domT, ranT, fvar, ...} = globals - - val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *) - - val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *) - Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))] - (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT))) - (fn {prems=[a], ...} => - ((rtac (G_induct OF [a])) - THEN_ALL_NEW rtac accI - THEN_ALL_NEW etac R_cases - THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1) - - val default_thm = - forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value) - - fun mk_trsimp clause psimp = - let - val ClauseInfo {qglr = (oqs, _, _, _), cdata = - ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause - val thy = ProofContext.theory_of ctxt - val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs - - val trsimp = Logic.list_implies(gs, - HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) - val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) - fun simp_default_tac ss = - asm_full_simp_tac (ss addsimps [default_thm, Let_def]) - in - Goal.prove ctxt [] [] trsimp (fn _ => - rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 - THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 - THEN (simp_default_tac (simpset_of ctxt) 1) - THEN TRY ((etac not_acc_down 1) - THEN ((etac R_cases) - THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)) - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) - end - in - map2 mk_trsimp clauses psimps - end - - fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = let - val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config + val FunctionConfig {domintros, default=default_opt, ...} = config val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) val fvar = Free (fname, fT) @@ -932,9 +880,6 @@ (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm - val mk_trsimps = - mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses - fun mk_partial_rules provedgoal = let val newthy = theory_of_thm provedgoal (*FIXME*) @@ -959,13 +904,10 @@ if domintros then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses) else NONE - val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE - in FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, psimps=psimps, simple_pinducts=[simple_pinduct], - termination=total_intro, trsimps=trsimps, - domintros=dom_intros} + termination=total_intro, domintros=dom_intros} end in ((f, goalstate, mk_partial_rules), lthy) diff -r 1a65b780bd56 -r edfc06b8a507 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Fri Feb 25 20:07:48 2011 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Fri Feb 25 20:08:00 2011 +0100 @@ -249,7 +249,7 @@ fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = let val result = inner_cont proof - val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct], + val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], termination, domintros, ...} = result val (all_f_defs, fs) = @@ -266,7 +266,6 @@ val rew_ss = HOL_basic_ss addsimps all_f_defs val mpsimps = map2 mk_mpsimp fqgars psimps - val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m val mtermination = full_simplify rew_ss termination val mdomintros = Option.map (map (full_simplify rew_ss)) domintros @@ -274,7 +273,7 @@ FunctionResult { fs=fs, G=G, R=R, psimps=mpsimps, simple_pinducts=minducts, cases=cases, termination=mtermination, - domintros=mdomintros, trsimps=mtrsimps} + domintros=mdomintros} end fun prepare_function_mutual config defname fixes eqss lthy = diff -r 1a65b780bd56 -r edfc06b8a507 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Feb 25 20:07:48 2011 +0100 +++ b/src/Pure/Tools/find_theorems.ML Fri Feb 25 20:08:00 2011 +0100 @@ -9,15 +9,21 @@ datatype 'term criterion = Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term | Pattern of 'term + + datatype theorem = + Internal of Facts.ref * thm | External of Facts.ref * term + val tac_limit: int Unsynchronized.ref val limit: int Unsynchronized.ref val find_theorems: Proof.context -> thm option -> int option -> bool -> (bool * string criterion) list -> int option * (Facts.ref * thm) list - val filter_facts: Proof.context -> (Facts.ref * thm) list -> thm option -> + val filter_theorems: Proof.context -> theorem list -> thm option -> int option -> bool -> (bool * string criterion) list -> - int option * (Facts.ref * thm) list + int option * theorem list + val pretty_theorem: Proof.context -> theorem -> Pretty.T val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T + end; structure Find_Theorems: FIND_THEOREMS = @@ -75,11 +81,29 @@ end; +(** theorems, either internal or external (without proof) **) + +datatype theorem = + Internal of Facts.ref * thm | + External of Facts.ref * term; + +fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm + | prop_of (External (_, prop)) = prop; + +fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm + | nprems_of (External (_, prop)) = Logic.count_prems prop; + +fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm + | major_prem_of (External (_, prop)) = + Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop)); + +fun fact_ref_of (Internal (fact_ref, _)) = fact_ref + | fact_ref_of (External (fact_ref, _)) = fact_ref; (** search criterion filters **) (*generated filters are to be of the form - input: (Facts.ref * thm) + input: theorem output: (p:int, s:int) option, where NONE indicates no match p is the primary sorting criterion @@ -142,43 +166,43 @@ (* filter_name *) -fun filter_name str_pat (thmref, _) = - if match_string str_pat (Facts.name_of_ref thmref) +fun filter_name str_pat theorem = + if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem)) then SOME (0, 0) else NONE; (* filter intro/elim/dest/solves rules *) -fun filter_dest ctxt goal (_, thm) = +fun filter_dest ctxt goal theorem = let val extract_dest = - (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm], + (fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem], hd o Logic.strip_imp_prems); val prems = Logic.prems_of_goal goal 1; - fun try_subst prem = is_matching_thm false extract_dest ctxt true prem thm; + fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem; val successful = prems |> map_filter try_subst; in (*if possible, keep best substitution (one with smallest size)*) (*dest rules always have assumptions, so a dest with one assumption is as good as an intro rule with none*) if not (null successful) - then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE + then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE end; -fun filter_intro doiff ctxt goal (_, thm) = +fun filter_intro doiff ctxt goal theorem = let - val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); + val extract_intro = (single o prop_of, Logic.strip_imp_concl); val concl = Logic.concl_of_goal goal 1; - val ss = is_matching_thm doiff extract_intro ctxt true concl thm; + val ss = is_matching_thm doiff extract_intro ctxt true concl theorem; in - if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE + if is_some ss then SOME (nprems_of theorem, the ss) else NONE end; -fun filter_elim ctxt goal (_, thm) = - if not (Thm.no_prems thm) then +fun filter_elim ctxt goal theorem = + if nprems_of theorem > 0 then let - val rule = Thm.full_prop_of thm; + val rule = prop_of theorem; val prems = Logic.prems_of_goal goal 1; val goal_concl = Logic.concl_of_goal goal 1; val rule_mp = hd (Logic.strip_imp_prems rule); @@ -192,9 +216,9 @@ in (*elim rules always have assumptions, so an elim with one assumption is as good as an intro rule with none*) - if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) + if is_nontrivial (ProofContext.theory_of ctxt) (major_prem_of theorem) andalso not (null successful) - then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE + then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE end else NONE @@ -207,29 +231,30 @@ if Thm.no_prems thm then rtac thm 1 goal else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; in - fn (_, thm) => + fn Internal (_, thm) => if is_some (Seq.pull (try_thm thm)) then SOME (Thm.nprems_of thm, 0) else NONE + | External _ => NONE end; (* filter_simp *) -fun filter_simp ctxt t (_, thm) = - let - val mksimps = Simplifier.mksimps (simpset_of ctxt); - val extract_simp = - (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); - val ss = is_matching_thm false extract_simp ctxt false t thm; - in - if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE - end; +fun filter_simp ctxt t (Internal (_, thm)) = + let + val mksimps = Simplifier.mksimps (simpset_of ctxt); + val extract_simp = + (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); + val ss = is_matching_thm false extract_simp ctxt false t thm; + in + if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE + end + | filter_simp _ _ (External _) = NONE; (* filter_pattern *) fun get_names t = Term.add_const_names t (Term.add_free_names t []); -fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm); (*Including all constants and frees is only sound because matching uses higher-order patterns. If full matching @@ -246,10 +271,10 @@ let val pat_consts = get_names pat; - fun check (t, NONE) = check (t, SOME (get_thm_names t)) - | check ((_, thm), c as SOME thm_consts) = + fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem))) + | check (theorem, c as SOME thm_consts) = (if subset (op =) (pat_consts, thm_consts) andalso - Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) + Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, prop_of theorem) then SOME (0, 0) else NONE, c); in check end; @@ -297,16 +322,16 @@ fun filter_criterion ctxt opt_goal (b, c) = (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c; -fun sorted_filter filters thms = +fun sorted_filter filters theorems = let - fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters); + fun eval_filters theorem = app_filters theorem (SOME (0, 0), NONE, filters); (*filters return: (number of assumptions, substitution size) option, so sort (desc. in both cases) according to number of assumptions first, then by the substitution size*) - fun thm_ord (((p0, s0), _), ((p1, s1), _)) = + fun result_ord (((p0, s0), _), ((p1, s1), _)) = prod_ord int_ord int_ord ((p1, s1), (p0, s0)); - in map_filter eval_filters thms |> sort thm_ord |> map #2 end; + in map_filter eval_filters theorems |> sort result_ord |> map #2 end; fun lazy_filter filters = let @@ -342,9 +367,9 @@ let fun rem_c rev_seen [] = rev rev_seen | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] - | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = - if Thm.eq_thm_prop (t, t') - then rem_c rev_seen ((if nicer n n' then x else y) :: xs) + | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) = + if (prop_of t) aconv (prop_of t') + then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs) else rem_c (x :: rev_seen) (y :: xs) in rem_c [] xs end; @@ -367,7 +392,7 @@ fun rem_thm_dups nicer xs = xs ~~ (1 upto length xs) - |> sort (Term_Ord.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) + |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1)) |> rem_cdups nicer |> sort (int_ord o pairself #2) |> map #1; @@ -385,12 +410,14 @@ in maps Facts.selections (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @ + + visible_facts (ProofContext.facts_of ctxt)) end; val limit = Unsynchronized.ref 40; -fun filter_facts ctxt facts opt_goal opt_limit rem_dups raw_criteria = +fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria = let val assms = ProofContext.get_fact ctxt (Facts.named "local.assms") @@ -401,9 +428,9 @@ val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; val filters = map (filter_criterion ctxt opt_goal') criteria; - fun find_all facts = + fun find_all theorems = let - val raw_matches = sorted_filter filters facts; + val raw_matches = sorted_filter filters theorems; val matches = if rem_dups @@ -419,20 +446,30 @@ then find_all else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters; - in find facts end; + in find theorems end; -fun find_theorems ctxt = filter_facts ctxt (all_facts_of ctxt) +fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = + filter_theorems ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit + rem_dups raw_criteria + |> apsnd (map (fn Internal f => f)); -fun pretty_thm ctxt (thmref, thm) = Pretty.block - [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, - Display.pretty_thm ctxt thm]; +fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block + [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, + Display.pretty_thm ctxt thm] + | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block + [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, + Syntax.unparse_term ctxt prop]; -fun print_theorems ctxt (foundo, thms) raw_criteria = +fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm)); + +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let val start = start_timing (); val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; - val returned = length thms; + val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt)) + opt_goal opt_limit rem_dups raw_criteria; + val returned = length theorems; val tally_msg = (case foundo of @@ -447,10 +484,10 @@ in Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" :: - (if null thms then [Pretty.str ("nothing found" ^ end_msg)] + (if null theorems then [Pretty.str ("nothing found" ^ end_msg)] else [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ - map (pretty_thm ctxt) thms) + map (pretty_theorem ctxt) theorems) end |> Pretty.chunks |> Pretty.writeln; @@ -486,8 +523,7 @@ let val ctxt = Toplevel.context_of state; val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal; - val found = find_theorems ctxt opt_goal opt_lim rem_dups spec; - in print_theorems ctxt found spec end))); + in print_theorems ctxt opt_goal opt_lim rem_dups spec end))); end;