author wenzelm Wed Aug 31 15:46:44 2005 +0200 (2005-08-31) changeset 17205 8994750ae33c parent 17204 6f0f8b6cd3f3 child 17206 83c15aa6a8c2
refer to theory instead of low-level tsig;
tuned use of map/filter/fold;
```     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;
```