refer to theory instead of low-level tsig;
authorwenzelm
Wed Aug 31 15:46:44 2005 +0200 (2005-08-31)
changeset 172058994750ae33c
parent 17204 6f0f8b6cd3f3
child 17206 83c15aa6a8c2
refer to theory instead of low-level tsig;
use Thm.full_prop_of instead of Thm.prop_of;
tuned use of map/filter/fold;
src/Pure/Isar/find_theorems.ML
     1.1 --- a/src/Pure/Isar/find_theorems.ML	Wed Aug 31 15:46:43 2005 +0200
     1.2 +++ b/src/Pure/Isar/find_theorems.ML	Wed Aug 31 15:46:44 2005 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  (** search criterion filters **)
     1.5  
     1.6  (*generated filters are to be of the form
     1.7 -  input: (PureThy.thmref * Thm.thm)
     1.8 +  input: (thmref * thm)
     1.9    output: (p:int, s:int) option, where
    1.10      NONE indicates no match
    1.11      p is the primary sorting criterion
    1.12 @@ -79,7 +79,7 @@
    1.13  
    1.14  (* matching theorems *)
    1.15  
    1.16 -fun is_nontrivial thy = is_Const o head_of o ObjectLogic.drop_judgment thy;
    1.17 +fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
    1.18  
    1.19  (*extract terms from term_src, refine them to the parts that concern us,
    1.20    if po try match them against obj else vice versa.
    1.21 @@ -88,20 +88,17 @@
    1.22  fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
    1.23    let
    1.24      val thy = ProofContext.theory_of ctxt;
    1.25 -    val tsig = Sign.tsig_of thy;
    1.26  
    1.27      fun matches pat =
    1.28        is_nontrivial thy pat andalso
    1.29 -      Pattern.matches tsig (if po then (pat,obj) else (obj,pat));
    1.30 +      Pattern.matches thy (if po then (pat, obj) else (obj, pat));
    1.31  
    1.32      fun substsize pat =
    1.33 -      let
    1.34 -        val (_,subst) = Pattern.match tsig (if po then (pat,obj) else (obj,pat))
    1.35 -      in Vartab.foldl (op + o apsnd (size_of_term o snd o snd)) (0, subst)
    1.36 -      end;
    1.37 +      let val (_, subst) = Pattern.match thy (if po then (pat, obj) else (obj, pat))
    1.38 +      in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
    1.39  
    1.40      fun bestmatch [] = NONE
    1.41 -     |  bestmatch (x :: xs) = SOME (foldl Int.min x xs);
    1.42 +     |  bestmatch xs = SOME (foldr1 Int.min xs);
    1.43  
    1.44      val match_thm = matches o refine_term;
    1.45    in
    1.46 @@ -122,45 +119,41 @@
    1.47    substring match only (no regexps are performed)*)
    1.48  fun filter_name str_pat (thmref, _) =
    1.49    if is_substring str_pat (PureThy.name_of_thmref thmref)
    1.50 -  then SOME (0,0) else NONE;
    1.51 +  then SOME (0, 0) else NONE;
    1.52  
    1.53  
    1.54  (* filter intro/elim/dest rules *)
    1.55  
    1.56 -fun filter_dest ctxt goal (_,thm) =
    1.57 +fun filter_dest ctxt goal (_, thm) =
    1.58    let
    1.59      val extract_dest =
    1.60 -     (fn thm => if Thm.no_prems thm then [] else [prop_of thm],
    1.61 +     (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm],
    1.62        hd o Logic.strip_imp_prems);
    1.63      val prems = Logic.prems_of_goal goal 1;
    1.64  
    1.65      fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
    1.66 -
    1.67 -    (*keep successful substitutions*)
    1.68 -    val ss = prems |> List.map try_subst
    1.69 -             |> List.filter isSome
    1.70 -             |> List.map valOf;
    1.71 +    val successful = prems |> List.mapPartial try_subst;
    1.72    in
    1.73      (*if possible, keep best substitution (one with smallest size)*)
    1.74      (*dest rules always have assumptions, so a dest with one
    1.75        assumption is as good as an intro rule with none*)
    1.76 -    if not (null ss)
    1.77 -    then SOME (nprems_of thm - 1, foldl Int.min (hd ss) (tl ss)) else NONE
    1.78 +    if not (null successful)
    1.79 +    then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
    1.80    end;
    1.81  
    1.82 -fun filter_intro ctxt goal (_,thm) =
    1.83 +fun filter_intro ctxt goal (_, thm) =
    1.84    let
    1.85 -    val extract_intro = (single o prop_of, Logic.strip_imp_concl);
    1.86 +    val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
    1.87      val concl = Logic.concl_of_goal goal 1;
    1.88      val ss = is_matching_thm extract_intro ctxt true concl thm;
    1.89    in
    1.90 -    if is_some ss then SOME (nprems_of thm, valOf ss) else NONE
    1.91 +    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
    1.92    end;
    1.93  
    1.94 -fun filter_elim ctxt goal (_,thm) =
    1.95 +fun filter_elim ctxt goal (_, thm) =
    1.96    if not (Thm.no_prems thm) then
    1.97      let
    1.98 -      val rule = prop_of thm;
    1.99 +      val rule = Thm.full_prop_of thm;
   1.100        val prems = Logic.prems_of_goal goal 1;
   1.101        val goal_concl = Logic.concl_of_goal goal 1;
   1.102        val rule_mp = (hd o Logic.strip_imp_prems) rule;
   1.103 @@ -170,40 +163,37 @@
   1.104        fun goal_tree prem = (combine prem goal_concl);
   1.105        fun try_subst prem =
   1.106          is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
   1.107 -      (*keep successful substitutions*)
   1.108 -      val ss = prems |> List.map try_subst
   1.109 -               |> List.filter isSome
   1.110 -               |> List.map valOf;
   1.111 +      val successful = prems |> List.mapPartial try_subst;
   1.112      in
   1.113      (*elim rules always have assumptions, so an elim with one
   1.114        assumption is as good as an intro rule with none*)
   1.115        if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
   1.116 -        andalso not (null ss)
   1.117 -      then SOME (nprems_of thm - 1, foldl Int.min (hd ss) (tl ss)) else NONE
   1.118 +        andalso not (null successful)
   1.119 +      then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
   1.120      end
   1.121    else NONE
   1.122  
   1.123  
   1.124  (* filter_simp *)
   1.125  
   1.126 -fun filter_simp ctxt t (_,thm) =
   1.127 +fun filter_simp ctxt t (_, thm) =
   1.128    let
   1.129      val (_, {mk_rews = {mk, ...}, ...}) =
   1.130        MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt);
   1.131      val extract_simp =
   1.132 -      ((List.map prop_of) o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   1.133 +      (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   1.134      val ss = is_matching_thm extract_simp ctxt false t thm
   1.135    in
   1.136 -    if is_some ss then SOME (nprems_of thm, valOf ss) else NONE
   1.137 +    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
   1.138    end;
   1.139  
   1.140  
   1.141  (* filter_pattern *)
   1.142  
   1.143  fun filter_pattern ctxt pat (_, thm) =
   1.144 -  let val tsig = Sign.tsig_of (ProofContext.theory_of ctxt)
   1.145 -  in if Pattern.matches_subterm tsig (pat, Thm.prop_of thm) then SOME (0,0)
   1.146 -     else NONE end;
   1.147 +  if Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
   1.148 +  then SOME (0, 0) else NONE;
   1.149 +
   1.150  
   1.151  (* interpret criteria as filters *)
   1.152  
   1.153 @@ -222,10 +212,10 @@
   1.154    | filter_crit ctxt _ (Simp pat) = filter_simp ctxt pat
   1.155    | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
   1.156  
   1.157 -fun opt_not x = if isSome x then NONE else SOME (0,0);
   1.158 +fun opt_not x = if isSome x then NONE else SOME (0, 0);
   1.159  
   1.160 -fun opt_add (SOME (a,x), SOME (b,y)) = SOME ((Int.max (a,b)), (x + y))
   1.161 - |  opt_add _ = NONE;
   1.162 +fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y)
   1.163 + |  opt_add _ _ = NONE;
   1.164  
   1.165  in
   1.166  
   1.167 @@ -235,18 +225,17 @@
   1.168  fun all_filters filters thms =
   1.169    let
   1.170      fun eval_filters filters thm =
   1.171 -      map (fn f => f thm) filters |> List.foldl opt_add (SOME (0,0));
   1.172 +      fold opt_add (map (fn f => f thm) filters) (SOME (0, 0));
   1.173  
   1.174      (*filters return: (number of assumptions, substitution size) option, so
   1.175        sort (desc. in both cases) according to number of assumptions first,
   1.176        then by the substitution size*)
   1.177 -    fun thm_ord (((p0,s0),_),((p1,s1),_)) =
   1.178 -      prod_ord int_ord int_ord ((p1,s1),(p0,s0));
   1.179 -
   1.180 -    val processed = List.map (fn t => (eval_filters filters t, t)) thms;
   1.181 -    val filtered = List.filter (isSome o #1) processed;
   1.182 +    fun thm_ord (((p0, s0), _), ((p1, s1), _)) =
   1.183 +      prod_ord int_ord int_ord ((p1, s1), (p0, s0));
   1.184    in
   1.185 -    filtered |> List.map (apfst valOf) |> sort thm_ord |> map #2
   1.186 +    map (`(eval_filters filters)) thms
   1.187 +    |> List.mapPartial (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
   1.188 +    |> sort thm_ord |> map #2
   1.189    end;
   1.190  
   1.191  end;