--- 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 ***
--- 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 \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+function (*<*)(domintros)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> 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 \<Longrightarrow> findzero_dom (f, x)"
- "findzero_dom (f, Suc x) \<Longrightarrow> 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 \<ge> n \<and> 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 \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> 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 {*
--- 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%
--- 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 \<notin> f_dom"}.
-
\end{description}
*}
--- 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%
--- 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
--- 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)),
--- 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.$$$ ")") [])
--- 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)
--- 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 =
--- 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;