(* pat.tac *)
signature PAT = sig
type patrules
val make_fpr : side -> thm -> (term -> bool) * thm
val make_fprt : thm list * thm list -> patrules
val make_pr : side -> thm -> (term -> bool) * thm
val make_prt : thm list * thm list -> patrules
val pr_append : patrules * patrules -> patrules
val pr_appl : patrules list -> patrules
val ffpr : patrules -> term -> side -> thm action
val tfpr : patrules -> term -> side -> thm Seq.seq action
val prlors : (thm -> int -> thm -> 'a) ->
((term -> bool) * thm) list -> term -> 'a action
end ;
structure Pat = struct
(* type patrules is pair of lists, one each for antecedent and succedent sides;
list entries are (patfn, thm) where patfn identifies a particular pattern
in a term, and thm is appropriate for terms of that form *)
type patrules = ((term -> bool) * thm) list * ((term -> bool) * thm) list ;
(* prlors : (thm -> int -> thm -> 'a) ->
((term -> bool) * thm) list -> term -> 'a action
prlors ruleact [(patfn, rule), ...] tm
takes the first patfn which tm satisfies and returns Act (ruleact rule) ;
if tm does not satisfy any patfn, then Unc is returned *)
fun prlors _ [] _ = Unc
| prlors ruleact ((patfn, rule) :: patrules) tm =
if patfn tm then Act (ruleact rule)
else prlors ruleact patrules tm ;
(* tfpr : patrules -> thm Seq.seq actfn
in tfpr (apr, spr) tm side, selects apr or spr according as side indicates
antecedent or succedent part, then tests tm agains all the (pattern)
tests, and if rule is the theorem corresponding to the first test which tm
satisfies, returns Act (rtac rule) ; otherwise returns Unc *)
fun tfpr (prs : patrules) tm side = prlors rtac (sidesel side prs) tm ;
(* pr_append : patrules * patrules -> patrules *)
fun pr_append ((apr1, spr1) : patrules, (apr2, spr2) : patrules) =
(apr1 @ apr2, spr1 @ spr2) : patrules ;
(* pr_appl : patrules list -> patrules *)
fun pr_appl (x : patrules list) = foldr1 pr_append x : patrules ;
val pr_none = ( [], [] ) ;
(* Koresfwd : thm -> int -> thm -> thm, forward proof function with extra arg *)
fun Koresfwd thr int th = th RS thr ;
(* ffpr : patrules -> thm actfn
in ffpr (apr, spr) tm side, selects apr or spr according as side indicates
antecedent or succedent part, then tests tm agains all the (pattern)
tests, and if rule is the theorem corresponding to the first test which tm
satisfies, returns Act (Koresfwd rule) ; otherwise returns Unc *)
fun ffpr (prs : patrules) tm side = prlors Koresfwd (sidesel side prs) tm ;
(* could_unify : term * term -> bool
tests whether first could be unified to second, as in source, term.ML,
but substituting for Vars in first only *)
fun could_unify (t,u) =
let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g)
| matchrands _ = true
in case (head_of t , head_of u) of
(Var _, _) => true
| (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u)
| (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u)
| _ => false
end;
(* make patrules just from list of theorems *)
(* make_pr : side -> thm -> (term -> bool) * thm
derives patfn from rule *)
fun make_pr side rule =
let val rtm = seqside side (concl_of rule) ;
fun npf tm = could_unify (rtm, tm) ;
in (npf, rule) end ;
(* make_prt : thm list * thm list -> patrules
uses patfn derived from rule instead of given one *)
fun make_prt (ar, sr) =
(map (make_pr Ant) ar, map (make_pr Suc) sr) : patrules ;
(* make_fpr, make_fprt, as for make_pr, make_prt *)
fun make_fpr side rule =
let val [prem] = prems_of rule
val rtm = seqside side prem
fun npf tm = could_unify (rtm, tm)
in (npf, rule) end
handle _ => raise Fail "make_fpr" ;
(* make_fprt : thm list * thm list -> patrules
uses patfn derived from rule instead of given one *)
fun make_fprt (ar, sr) =
(map (make_fpr Ant) ar, map (make_fpr Suc) sr) : patrules ;
end ; (* functor Pat *)