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