1structure mp_then :> mp_then =
2struct
3
4open HolKernel Drule Conv Parse boolTheory boolSyntax
5
6open thmpos_dtype
7
8fun match_subterm pat = find_term (can (match_term pat))
9
10val op$ = Portable.$
11val notT = el 2 (CONJUNCTS NOT_CLAUSES)
12val imp_clauses = IMP_CLAUSES |> SPEC_ALL |> CONJUNCTS
13val Timp = el 1 imp_clauses
14val impF = last imp_clauses
15
16fun mp_then pos (ttac : thm_tactic) ith0 rth (g as (asl,w)) =
17  let
18    val ith = MP_CANON (GEN_ALL ith0)
19    val rth_eqT = EQT_INTRO rth
20    val rth_eq = EQF_INTRO rth handle HOL_ERR _ => rth_eqT
21    fun m f k t =
22      let
23        val th0 = PART_MATCH' f ith t
24        val th =
25            CONV_RULE
26              (STRIP_QUANT_CONV
27                 (FORK_CONV (EVERY_CONJ_CONV $ TRY_CONV $ REWR_CONV rth_eqT,
28                             (REWR_CONV rth_eq ORELSEC
29                              TRY_CONV (RAND_CONV (REWR_CONV rth_eq) THENC
30                                        REWR_CONV notT))) THENC
31                  TRY_CONV (REWR_CONV Timp) THENC
32                  TRY_CONV (REWR_CONV impF)))
33              th0
34      in
35        ttac th g
36      end handle HOL_ERR _ => k()
37    fun conj f t = t |> dest_imp |> #1 |> strip_conj |> f
38    val max = ith |> concl |> strip_forall |> #2 |> conj length
39    val fail = mk_HOL_ERR "mp_then" "mp_then" "No match"
40    val t = concl rth
41  in
42    case pos of
43        Any =>
44        let
45          fun doit (n:int) =
46            if n > max then raise fail
47            else m (conj (el n)) (fn _ => doit (n + 1)) t
48        in
49          doit 1
50        end
51      | Pos f => m (conj f) (fn _ => raise fail) t
52      | Pat q =>
53        let
54          open TermParse
55          val pats =
56              prim_ctxt_termS Parse.Absyn (term_grammar())
57                              (HOLset.listItems (FVL (w::asl) empty_tmset))
58                              q
59          fun doit ps n =
60            if n > max then raise fail
61            else
62              case seq.cases ps of
63                  NONE => doit pats (n + 1)
64                | SOME (pat, rest) =>
65                    m (fn t => let val subterm = conj (el n) t
66                               in
67                                 if can (match_subterm pat) subterm then
68                                   subterm
69                                 else raise fail
70                               end)
71                      (fn _ => doit rest n)
72                   t
73        in
74          doit pats 1
75        end
76      | Concl => m (fn t => t |> dest_imp |> #2)
77                   (fn _ => raise fail)
78                   (dest_neg t handle HOL_ERR _ => mk_neg t)
79  end
80
81end
82