src/Pure/Tools/find_theorems.ML

 
 fun map_criteria f {goal, limit, rem_dups, criteria} =
   {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
 
 
-
-(** theorems, either internal or external (without proof) **)
-
-datatype theorem =
-  Internal of Facts.ref * thm |
-  External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *)
-
-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 size_of (Internal (_, thm)) = size_of_term (Thm.prop_of thm)
-  | size_of (External (_, prop)) = size_of_term 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: theorem
+  input: (Facts.ref * thm)
   output: (p:int, s:int, t:int) option, where
     NONE indicates no match
     p is the primary sorting criterion
       (eg. size of term)
     s is the secondary sorting criterion

   end;
 
 
 (* filter_name *)
 
-fun filter_name str_pat theorem =
-  if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem))
+fun filter_name str_pat (thmref, _) =
+  if match_string str_pat (Facts.name_of_ref thmref)
   then SOME (0, 0, 0) else NONE;
 
 
 (* filter intro/elim/dest/solves rules *)
 
-fun filter_dest ctxt goal theorem =
+fun filter_dest ctxt goal (_, thm) =
   let
     val extract_dest =
-     (fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem],
+     (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm],
       hd o Logic.strip_imp_prems);
     val prems = Logic.prems_of_goal goal 1;
 
-    fun try_subst prem = is_matching_thm extract_dest ctxt true prem theorem;
+    fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
     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 (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
-  end;
-
-fun filter_intro ctxt goal theorem =
-  let
-    val extract_intro = (single o prop_of, Logic.strip_imp_concl);
+    if not (null successful) then
+      SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
+    else NONE
+  end;
+
+fun filter_intro ctxt goal (_, thm) =
+  let
+    val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
     val concl = Logic.concl_of_goal goal 1;
-    val ss = is_matching_thm extract_intro ctxt true concl theorem;
-  in
-    if is_some ss then SOME (size_of theorem, nprems_of theorem, the ss) else NONE
-  end;
-
-fun filter_elim ctxt goal theorem =
-  if nprems_of theorem > 0 then
+  in
+    (case is_matching_thm extract_intro ctxt true concl thm of
+      SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
+    | NONE => NONE)
+  end;
+
+fun filter_elim ctxt goal (_, thm) =
+  if Thm.nprems_of thm > 0 then
     let
-      val rule = prop_of theorem;
+      val rule = Thm.full_prop_of thm;
       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);
       val rule_concl = Logic.strip_imp_concl rule;
       fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?? *)

       fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
       val successful = prems |> map_filter try_subst;
     in
       (*elim rules always have assumptions, so an elim with one
         assumption is as good as an intro rule with none*)
-      if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem)
-        andalso not (null successful)
-      then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE
+      if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm)
+          andalso not (null successful) then
+        SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
+      else NONE
     end
   else NONE;
 
 fun filter_solves ctxt goal =
   let

       if Thm.no_prems thm then rtac thm 1 goal'
       else
         (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
           1 goal';
   in
-    fn Internal (_, thm) =>
-        if is_some (Seq.pull (try_thm thm))
-        then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE
-     | External _ => NONE
+    fn (_, thm) =>
+      if is_some (Seq.pull (try_thm thm))
+      then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0)
+      else NONE
   end;
 
 
 (* filter_simp *)
 
-fun filter_simp ctxt t (Internal (_, thm)) =
-      let
-        val mksimps = Simplifier.mksimps 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 extract_simp ctxt false t thm;
-      in
-        if is_some ss
-        then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, the ss)
-        else NONE
-      end
-  | filter_simp _ _ (External _) = NONE;
+fun filter_simp ctxt t (_, thm) =
+  let
+    val mksimps = Simplifier.mksimps ctxt;
+    val extract_simp =
+      (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
+  in
+    (case is_matching_thm extract_simp ctxt false t thm of
+      SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss)
+    | NONE => NONE)
+  end;
 
 
 (* filter_pattern *)
 
 fun get_names t = Term.add_const_names t (Term.add_free_names t []);

 
 fun filter_pattern ctxt pat =
   let
     val pat_consts = get_names pat;
 
-    fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
-      | check (theorem, c as SOME thm_consts) =
+    fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
+      | check ((_, thm), c as SOME thm_consts) =
          (if subset (op =) (pat_consts, thm_consts) andalso
-            Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
-          then SOME (size_of theorem, nprems_of theorem, 0) else NONE, c);
+            Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
+          then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
   in check end;
 
 
 (* interpret criteria as filters *)
 

 in
 
 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 theorems =
-  let
-    fun eval_filters theorem = app_filters theorem (SOME (0, 0, 0), NONE, filters);
+fun sorted_filter filters thms =
+  let
+    fun eval_filters thm = app_filters thm (SOME (0, 0, 0), NONE, filters);
 
     (*filters return: (thm size, number of assumptions, substitution size) option, so
       sort according to size of thm first, then number of assumptions,
       then by the substitution size, then by term order *)
-    fun result_ord (((p0, s0, t0), thm0), ((p1, s1, t1), thm1)) =
-      prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord)) 
-         ((p1, (s1, (t1, prop_of thm1))), (p0, (s0, (t0, prop_of thm0))));
-  in
-    grouped 100 Par_List.map eval_filters theorems
+    fun result_ord (((p0, s0, t0), (_, thm0)), ((p1, s1, t1), (_, thm1))) =
+      prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord))
+         ((p1, (s1, (t1, Thm.full_prop_of thm1))), (p0, (s0, (t0, Thm.full_prop_of thm0))));
+  in
+    grouped 100 Par_List.map eval_filters thms
     |> map_filter I |> sort result_ord |> map #2
   end;
 
 fun lazy_filter filters =
   let

 
 fun rem_cdups nicer xs =
   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 (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);
+      | rem_c rev_seen ((x as ((n, thm), _)) :: (y as ((n', thm'), _)) :: rest) =
+          if Thm.eq_thm_prop (thm, thm')
+          then rem_c rev_seen ((if nicer n n' then x else y) :: rest)
+          else rem_c (x :: rev_seen) (y :: rest);
   in rem_c [] xs end;
 
 in
 
 fun nicer_shortest ctxt =

       | nicer (Facts.Fact _) (Facts.Fact _) = true;
   in nicer end;
 
 fun rem_thm_dups nicer xs =
   (xs ~~ (1 upto length xs))
-  |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
+  |> sort (Term_Ord.fast_term_ord o pairself (Thm.full_prop_of o #2 o #1))
   |> rem_cdups nicer
   |> sort (int_ord o pairself #2)
   |> map #1;
 
 end;

       Proof_Context.get_fact ctxt (Facts.named "local.assms")
         handle ERROR _ => [];
     val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
     val opt_goal' = Option.map add_prems opt_goal;
   in
-    filter ctxt (map Internal (all_facts_of ctxt))
+    filter ctxt (all_facts_of ctxt)
       {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
-    |> apsnd (map (fn Internal f => f))
   end;
 
 in
 
 val find_theorems = gen_find_theorems filter_theorems;

   in
     [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
       Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
   end;
 
-fun pretty_theorem ctxt (Internal (thmref, thm)) =
-      Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
-  | 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_thm ctxt (thmref, thm) =
+  Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]);
 
 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))
+      filter_theorems ctxt (all_facts_of ctxt)
         {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
     val returned = length theorems;
 
     val tally_msg =
       (case opt_found of

     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
     Pretty.str "" ::
     (if null theorems then [Pretty.str "nothing found"]
      else
       [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
-        grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) (rev theorems))
+        grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
   end |> Pretty.fbreaks |> curry Pretty.blk 0;
 
 end;