--- a/src/Pure/Tools/find_theorems.ML Fri Aug 09 15:14:59 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Aug 09 15:49:50 2013 +0200
@@ -9,31 +9,17 @@
sig
datatype 'term criterion =
Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
-
- datatype theorem =
- Internal of Facts.ref * thm | External of Facts.ref * term
-
type 'term query = {
goal: thm option,
limit: int option,
rem_dups: bool,
criteria: (bool * 'term criterion) list
}
-
- val read_criterion: Proof.context -> string criterion -> term criterion
val read_query: Position.T -> string -> (bool * string criterion) list
-
val find_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * term criterion) list -> int option * (Facts.ref * thm) list
val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> int option * (Facts.ref * thm) list
-
- val filter_theorems: Proof.context -> theorem list -> term query ->
- int option * theorem list
- val filter_theorems_cmd: Proof.context -> theorem list -> string query ->
- int option * theorem list
-
- val pretty_theorem: Proof.context -> theorem -> Pretty.T
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
end;
@@ -169,13 +155,13 @@
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
- fun bestmatch [] = NONE
- | bestmatch xs = SOME (foldl1 Int.min xs);
+ fun best_match [] = NONE
+ | best_match xs = SOME (foldl1 Int.min xs);
val match_thm = matches o refine_term;
in
map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
- |> bestmatch
+ |> best_match
end;
@@ -222,7 +208,7 @@
val goal_concl = Logic.concl_of_goal goal 1;
val rule_mp = hd (Logic.strip_imp_prems rule);
val rule_concl = Logic.strip_imp_concl rule;
- fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);
+ fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2); (* FIXME ?? *)
val rule_tree = combine rule_mp rule_concl;
fun goal_tree prem = combine prem goal_concl;
fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
@@ -244,11 +230,11 @@
val ctxt' = Proof_Context.transfer thy' ctxt;
val goal' = Thm.transfer thy' goal;
- fun etacn thm i =
+ fun limited_etac thm i =
Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
fun try_thm thm =
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';
+ else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
in
fn Internal (_, thm) =>
if is_some (Seq.pull (try_thm thm))
@@ -416,7 +402,10 @@
end;
-(* pretty_theorems *)
+
+(** main operations **)
+
+(* filter_theorems *)
fun all_facts_of ctxt =
let
@@ -455,8 +444,12 @@
in find theorems end;
fun filter_theorems_cmd ctxt theorems raw_query =
- filter_theorems ctxt theorems (map_criteria
- (map (apsnd (read_criterion ctxt))) raw_query);
+ filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
+
+
+(* find_theorems *)
+
+local
fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
let
@@ -471,9 +464,18 @@
|> apsnd (map (fn Internal f => f))
end;
+in
+
val find_theorems = gen_find_theorems filter_theorems;
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
+end;
+
+
+(* pretty_theorems *)
+
+local
+
fun pretty_ref ctxt thmref =
let
val (name, sel) =
@@ -490,11 +492,16 @@
| pretty_theorem ctxt (External (thmref, prop)) =
Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
+in
+
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
-fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun pretty_theorems state opt_limit rem_dups raw_criteria =
let
+ val ctxt = Proof.context_of state;
+ val opt_goal = try Proof.simple_goal state |> Option.map #goal;
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
+
val (opt_found, theorems) =
filter_theorems ctxt (map Internal (all_facts_of ctxt))
{goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
@@ -517,16 +524,17 @@
grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) theorems)
end |> Pretty.fbreaks |> curry Pretty.blk 0;
-fun pretty_theorems_cmd state opt_lim rem_dups spec =
- let
- val ctxt = Toplevel.context_of state;
- val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
- in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
+end;
(** Isar command syntax **)
+fun proof_state st =
+ (case try Toplevel.proof_of st of
+ SOME state => state
+ | NONE => Proof.init (Toplevel.context_of st));
+
local
val criterion =
@@ -558,8 +566,8 @@
Outer_Syntax.improper_command @{command_spec "find_theorems"}
"find theorems meeting specified criteria"
(options -- query >> (fn ((opt_lim, rem_dups), spec) =>
- Toplevel.keep (fn state =>
- Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
+ Toplevel.keep (fn st =>
+ Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
end;
@@ -569,8 +577,9 @@
val _ =
Query_Operation.register "find_theorems" (fn st => fn args =>
- if can Toplevel.theory_of st then
- Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args))
- else error "Unknown theory context");
+ if can Toplevel.context_of st then
+ Pretty.string_of
+ (pretty_theorems (proof_state st) NONE false (maps (read_query Position.none) args))
+ else error "Unknown context");
end;