1structure mp_then =
2struct
3
4local
5  open HolKernel Drule Conv Parse boolTheory boolSyntax
6
7fun avSPEC_ALL avds th =
8  let
9    fun recurse avds acc th =
10      case Lib.total dest_forall (concl th) of
11          SOME (v,bod) =>
12          let
13            val v' = variant avds v
14          in
15            recurse (v'::avds) (v'::acc) (SPEC v' th)
16          end
17        | NONE => (List.rev acc, th)
18  in
19    recurse avds [] th
20  end
21
22fun PART_MATCH' f th t =
23  let
24    val (vs, _) = strip_forall (concl th)
25    val hypfvs_set = hyp_frees th
26    val hypfvs = HOLset.listItems hypfvs_set
27    val hyptyvs = HOLset.listItems (hyp_tyvars th)
28    val tfvs = free_vars t
29    val dontspec = union tfvs hypfvs
30    val (vs, speccedth) = avSPEC_ALL dontspec th
31    val s as (tmsig,tysig) =
32        match_terml hyptyvs hypfvs_set (f (concl speccedth)) t
33    val dontgen = op_union aconv (map #redex tmsig) dontspec
34  in
35    GENL (op_set_diff aconv (map (Term.inst tysig) vs) dontgen)
36         (INST_TY_TERM s speccedth)
37  end
38
39fun match_subterm pat = find_term (can (match_term pat))
40
41val op$ = Portable.$
42val notT = el 2 (CONJUNCTS NOT_CLAUSES)
43val imp_clauses = IMP_CLAUSES |> SPEC_ALL |> CONJUNCTS
44val Timp = el 1 imp_clauses
45val impF = last imp_clauses
46
47in
48
49datatype match_position =
50  Any
51| Pat of term quotation
52| Pos of (term list -> term)
53| Concl
54
55fun mp_then pos (ttac : thm_tactic) ith0 rth (g as (asl,w)) =
56  let
57    val ith = MP_CANON ith0
58    val rth_eqT = EQT_INTRO rth
59    val rth_eq = EQF_INTRO rth handle HOL_ERR _ => rth_eqT
60    fun m f k t =
61      let
62        val th0 = PART_MATCH' f ith t
63        val th =
64            CONV_RULE
65              (STRIP_QUANT_CONV
66                 (FORK_CONV (EVERY_CONJ_CONV $ TRY_CONV $ REWR_CONV rth_eqT,
67                             (REWR_CONV rth_eq ORELSEC
68                              TRY_CONV (RAND_CONV (REWR_CONV rth_eq) THENC
69                                        REWR_CONV notT))) THENC
70                  TRY_CONV (REWR_CONV Timp) THENC
71                  TRY_CONV (REWR_CONV impF)))
72              th0
73      in
74        ttac th g
75      end handle HOL_ERR _ => k()
76    fun conj f t = t |> dest_imp |> #1 |> strip_conj |> f
77    val max = ith |> concl |> strip_forall |> #2 |> conj length
78    val fail = mk_HOL_ERR "mp_then" "mp_then" "No match"
79    val t = concl rth
80  in
81    case pos of
82        Any =>
83        let
84          fun doit (n:int) =
85            if n > max then raise fail
86            else m (conj (el n)) (fn _ => doit (n + 1)) t
87        in
88          doit 1
89        end
90      | Pos f => m (conj f) (fn _ => raise fail) t
91      | Pat q =>
92        let
93          open TermParse
94          val pats =
95              prim_ctxt_termS Parse.Absyn (term_grammar())
96                              (HOLset.listItems (FVL (w::asl) empty_tmset))
97                              q
98          fun doit ps n =
99            if n > max then raise fail
100            else
101              case seq.cases ps of
102                  NONE => doit pats (n + 1)
103                | SOME (pat, rest) =>
104                    m (fn t => let val subterm = conj (el n) t
105                               in
106                                 if can (match_subterm pat) subterm then
107                                   subterm
108                                 else raise fail
109                               end)
110                      (fn _ => doit rest n)
111                   t
112        in
113          doit pats 1
114        end
115      | Concl => m (fn t => t |> dest_imp |> #2)
116                   (fn _ => raise fail)
117                   (dest_neg t handle HOL_ERR _ => mk_neg t)
118  end
119
120end (* local *)
121
122end
123