tuned signature;
authorwenzelm
Fri Aug 09 15:49:50 2013 +0200 (2013-08-09)
changeset 5294128407b5f1c72
parent 52940 6fce81e92e7c
child 52942 07093b66fc9d
tuned signature;
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:14:59 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:49:50 2013 +0200
     1.3 @@ -9,31 +9,17 @@
     1.4  sig
     1.5    datatype 'term criterion =
     1.6      Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
     1.7 -
     1.8 -  datatype theorem =
     1.9 -    Internal of Facts.ref * thm | External of Facts.ref * term
    1.10 -
    1.11    type 'term query = {
    1.12      goal: thm option,
    1.13      limit: int option,
    1.14      rem_dups: bool,
    1.15      criteria: (bool * 'term criterion) list
    1.16    }
    1.17 -
    1.18 -  val read_criterion: Proof.context -> string criterion -> term criterion
    1.19    val read_query: Position.T -> string -> (bool * string criterion) list
    1.20 -
    1.21    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.22      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    1.23    val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    1.24      (bool * string criterion) list -> int option * (Facts.ref * thm) list
    1.25 -
    1.26 -  val filter_theorems: Proof.context -> theorem list -> term query ->
    1.27 -    int option * theorem list
    1.28 -  val filter_theorems_cmd: Proof.context -> theorem list -> string query ->
    1.29 -    int option * theorem list
    1.30 -
    1.31 -  val pretty_theorem: Proof.context -> theorem -> Pretty.T
    1.32    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    1.33  end;
    1.34  
    1.35 @@ -169,13 +155,13 @@
    1.36          Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
    1.37        in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
    1.38  
    1.39 -    fun bestmatch [] = NONE
    1.40 -      | bestmatch xs = SOME (foldl1 Int.min xs);
    1.41 +    fun best_match [] = NONE
    1.42 +      | best_match xs = SOME (foldl1 Int.min xs);
    1.43  
    1.44      val match_thm = matches o refine_term;
    1.45    in
    1.46      map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
    1.47 -    |> bestmatch
    1.48 +    |> best_match
    1.49    end;
    1.50  
    1.51  
    1.52 @@ -222,7 +208,7 @@
    1.53        val goal_concl = Logic.concl_of_goal goal 1;
    1.54        val rule_mp = hd (Logic.strip_imp_prems rule);
    1.55        val rule_concl = Logic.strip_imp_concl rule;
    1.56 -      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);
    1.57 +      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?? *)
    1.58        val rule_tree = combine rule_mp rule_concl;
    1.59        fun goal_tree prem = combine prem goal_concl;
    1.60        fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
    1.61 @@ -244,11 +230,11 @@
    1.62      val ctxt' = Proof_Context.transfer thy' ctxt;
    1.63      val goal' = Thm.transfer thy' goal;
    1.64  
    1.65 -    fun etacn thm i =
    1.66 +    fun limited_etac thm i =
    1.67        Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
    1.68      fun try_thm thm =
    1.69        if Thm.no_prems thm then rtac thm 1 goal'
    1.70 -      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
    1.71 +      else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
    1.72    in
    1.73      fn Internal (_, thm) =>
    1.74          if is_some (Seq.pull (try_thm thm))
    1.75 @@ -416,7 +402,10 @@
    1.76  end;
    1.77  
    1.78  
    1.79 -(* pretty_theorems *)
    1.80 +
    1.81 +(** main operations **)
    1.82 +
    1.83 +(* filter_theorems *)
    1.84  
    1.85  fun all_facts_of ctxt =
    1.86    let
    1.87 @@ -455,8 +444,12 @@
    1.88    in find theorems end;
    1.89  
    1.90  fun filter_theorems_cmd ctxt theorems raw_query =
    1.91 -  filter_theorems ctxt theorems (map_criteria
    1.92 -    (map (apsnd (read_criterion ctxt))) raw_query);
    1.93 +  filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
    1.94 +
    1.95 +
    1.96 +(* find_theorems *)
    1.97 +
    1.98 +local
    1.99  
   1.100  fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
   1.101    let
   1.102 @@ -471,9 +464,18 @@
   1.103      |> apsnd (map (fn Internal f => f))
   1.104    end;
   1.105  
   1.106 +in
   1.107 +
   1.108  val find_theorems = gen_find_theorems filter_theorems;
   1.109  val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
   1.110  
   1.111 +end;
   1.112 +
   1.113 +
   1.114 +(* pretty_theorems *)
   1.115 +
   1.116 +local
   1.117 +
   1.118  fun pretty_ref ctxt thmref =
   1.119    let
   1.120      val (name, sel) =
   1.121 @@ -490,11 +492,16 @@
   1.122    | pretty_theorem ctxt (External (thmref, prop)) =
   1.123        Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
   1.124  
   1.125 +in
   1.126 +
   1.127  fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
   1.128  
   1.129 -fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   1.130 +fun pretty_theorems state opt_limit rem_dups raw_criteria =
   1.131    let
   1.132 +    val ctxt = Proof.context_of state;
   1.133 +    val opt_goal = try Proof.simple_goal state |> Option.map #goal;
   1.134      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   1.135 +
   1.136      val (opt_found, theorems) =
   1.137        filter_theorems ctxt (map Internal (all_facts_of ctxt))
   1.138          {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
   1.139 @@ -517,16 +524,17 @@
   1.140          grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) theorems)
   1.141    end |> Pretty.fbreaks |> curry Pretty.blk 0;
   1.142  
   1.143 -fun pretty_theorems_cmd state opt_lim rem_dups spec =
   1.144 -  let
   1.145 -    val ctxt = Toplevel.context_of state;
   1.146 -    val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
   1.147 -  in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
   1.148 +end;
   1.149  
   1.150  
   1.151  
   1.152  (** Isar command syntax **)
   1.153  
   1.154 +fun proof_state st =
   1.155 +  (case try Toplevel.proof_of st of
   1.156 +    SOME state => state
   1.157 +  | NONE => Proof.init (Toplevel.context_of st));
   1.158 +
   1.159  local
   1.160  
   1.161  val criterion =
   1.162 @@ -558,8 +566,8 @@
   1.163    Outer_Syntax.improper_command @{command_spec "find_theorems"}
   1.164      "find theorems meeting specified criteria"
   1.165      (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
   1.166 -      Toplevel.keep (fn state =>
   1.167 -        Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
   1.168 +      Toplevel.keep (fn st =>
   1.169 +        Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
   1.170  
   1.171  end;
   1.172  
   1.173 @@ -569,8 +577,9 @@
   1.174  
   1.175  val _ =
   1.176    Query_Operation.register "find_theorems" (fn st => fn args =>
   1.177 -    if can Toplevel.theory_of st then
   1.178 -      Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args))
   1.179 -    else error "Unknown theory context");
   1.180 +    if can Toplevel.context_of st then
   1.181 +      Pretty.string_of
   1.182 +        (pretty_theorems (proof_state st) NONE false (maps (read_query Position.none) args))
   1.183 +    else error "Unknown context");
   1.184  
   1.185  end;