# HG changeset patch # User wenzelm # Date 1376056190 -7200 # Node ID 28407b5f1c72726b5854a0a16a81346ec0fc219e # Parent 6fce81e92e7caa9ca732da128b5e20eb84361971 tuned signature; diff -r 6fce81e92e7c -r 28407b5f1c72 src/Pure/Tools/find_theorems.ML --- 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;