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