(* ML functions for unifying sequents as HOL terms *)
fun assoc (x, l) = (AList.lookup (op =)) x l ;
(* consNew : ''a -> ''a list -> ''a list
adds x to head of list xs if not already in xs *)
fun consNew x xs = if x mem xs then xs else x :: xs ;
type free_vars = {fv : string list, sv : string list} ;
(* tmVars' :
term -> {fv:term list, sv:term list} -> {fv:term list, sv:term list}
as for tmVars (below), but using Isabelle terms *)
fun tmVars' (Const ("GDC.formula.FV", _) $ hstr) {fv = fvs, sv = svs} =
{fv = consNew hstr fvs, sv = svs}
| tmVars' (Const ("GDC.structr.SV", _) $ hstr) {fv = fvs, sv = svs} =
{fv = fvs, sv = consNew hstr svs}
| tmVars' (f $ a) fsvs = tmVars' f (tmVars' a fsvs)
| tmVars' (Const _) fsvs = fsvs
| tmVars' tm fsvs = raise TERM ("tmVars': non-Const atom found", [tm]) ;
val ar = ref [] : term list ref ;
(* tmVars : term -> free_vars -> free_vars
collect free variables (ie FV and SV), augmenting the free_vars argument *)
fun tmVars (Const ("GDC.formula.FV", _) $ hstr) {fv = fvs, sv = svs} =
(ar := [hstr] ;
{fv = consNew (h2ml_str hstr) fvs, sv = svs}
)
| tmVars (Const ("GDC.structr.SV", _) $ hstr) {fv = fvs, sv = svs} =
(ar := [hstr] ;
{fv = fvs, sv = consNew (h2ml_str hstr) svs}
)
| tmVars (f $ a) fsvs = tmVars f (tmVars a fsvs)
| tmVars (Const _) fsvs = fsvs
| tmVars tm fsvs = raise TERM ("tmVars: non-Const atom found", [tm]) ;
(* variant_pairs :
string list -> string list -> (string * string) list * string list
change strings in list1 to be different from anything in list2
(or other changed ones), return list of substitutions and list1,
with the substitutions applied *)
fun variant_pairs l1 l2 =
let
(* get union, intersection, difference of l1 and l2 *)
fun uid [] = (l2, [], [])
| uid (x :: xs) =
let val (u, i, d) = uid xs
in if x mem l2 then (u, x :: i, d)
else (x :: u, i, x :: d) end ;
val (un, int, diff) = uid l1 ;
(* get substitutions for variables in int, augmenting un and diff *)
fun sud [] = ([], un, diff)
| sud (y :: ys) =
let val (s, u, d) = sud ys
val y' = variant u y
in ((y, y') :: s, y' :: u, y' :: d) end
val (subs, _, nv1) = sud int
in (subs, nv1) end ;
(* free_ren - type for renaming variables, first FVs, then SVs *)
type free_ren = {fv : (string * string) list, sv : (string * string) list} ;
fun ml2h_ren XV (s1, s2) = (ml2h_str s1, XV (ml2h_str s2)) ;
(* ml2h_rens : typ * (term -> term) -> (string * string) list -> term
turns list of string pairs into fSubst or sSubst,
first arg is (fmlT, FV) or (strT, SV) *)
fun ml2h_rens (ty, XV) stringPairs =
ml2h_list (pairT (stringT, ty)) (map (ml2h_pair o ml2h_ren XV) stringPairs) ;
(* both_rens : free_ren -> term
turns two lists of string pairs into a HOL substitution (type fsSubst) *)
fun both_rens {fv = fvRens, sv = svRens} =
ml2h_pair (ml2h_rens (fmlT, FV) fvRens, ml2h_rens (strT, SV) svRens) ;
(* sub - type of substitutions, two lists are substitutions for formula
and structure variables (ie, FV and SV) respectively;
each list is of pairs of (HOL) string and replacement term *)
type sub = {fv : (term * term) list, sv : (term * term) list} ;
val fsvEmpty = {fv = [], sv = []} ;
fun fsvmap f {fv, sv} = {fv = f fv, sv = f sv} ;
fun fsvcomp f {fv = p1, sv = p2} {fv = q1, sv = q2} =
{fv = f p1 q1, sv = f p2 q2} ;
fun mkfvs fv sv = {fv = fv, sv = sv} ;
fun fvs {fv, sv} = fv ;
(* sub2pfsSubst : sub -> term *)
fun sub2pfsSubst {fv = fvSubs, sv = svSubs} = ml2h_pair
(ml2h_pair (ml2h_list (pairT (stringT, stringT)) [],
ml2h_list (pairT (stringT, fmlT)) (map ml2h_pair fvSubs)),
ml2h_list (pairT (stringT, strT)) (map ml2h_pair svSubs)) ;
(* ruleSubst_ML : free_ren -> term -> cterm
in ML, do substitution of HOL IsDerivableB theorem *)
(*
fun ruleSubst_ML hsubs isprb =
let
isprb RS IsDerivableB_sub
val rs = ruleSubst $ hsubs $ rule
val crs = cterm_of (sign_of HOL_Sub.thy) rs
val res = Simplifier.rewrite (simpset_of HOL_Sub.thy) crs
val nrule1 = snd (dest_comb (cprop_of res))
in nrule1 end ;
*)
(* substt : sub -> term -> term
substitute for FVs and SVs in HOL term (rule, sequent, etc) *)
fun substt {fv = fvSubs, sv = svSubs} t =
let
fun sub (fv as Const ("GDC.formula.FV", _) $ hstr) =
(case assoc (fvSubs, hstr) of NONE => fv | SOME rep => rep)
| sub (sv as Const ("GDC.structr.SV", _) $ hstr) =
(case assoc (svSubs, hstr) of NONE => sv | SOME rep => rep)
| sub (f $ a) = sub f $ sub a
| sub (cf as Const _) = cf
| sub tm = raise TERM ("substt: non-Const atom found", [tm]) ;
in sub t end ;
(* rens2subs : free_ren -> sub
to get argument for substt from lists of pairs of ML strings *)
fun rens2subs {fv = fvRens, sv = svRens} =
{fv = map (ml2h_ren FV) fvRens, sv = map (ml2h_ren SV) svRens} ;
(* sub_apply : ('a -> 'b) -> {fv:('a * 'a) list, sv:('a * 'a) list} ->
{fv:('b * 'b) list, sv:('b * 'b) list}
map function for sub, eg, to get nicer printing,
sub_apply (cterm_of (sign_of GDC.thy)) sub ; *)
fun sub_apply f = fsvmap (map (pairself f)) ;
(* cterm_subs : sub -> [same, but cterms]
useful for getting sub in printable form *)
val cterm_subs = sub_apply (cterm_of (sign_of GDC.thy)) ;
(** unification, where terms have no common variables **)
(* compsubs : sub -> sub -> sub
compose substitutions; assumes no variable is on lhs in both subs1 and subs2 ;
assumes no variable on a lhs is in a rhs, in either subs1 or subs2 ;
assumes no variable in a rhs of subs2 is a lhs in subs1 ;
ie just applies subs2 to each rhs in subs1, and concatenates *)
(* ignoring the fact that a formula cannot contain a structure variable *)
fun compsubs {fv = fs1, sv = ss1} (subs2 as {fv = fs2, sv = ss2}) =
let val fs1' = map (apsnd (substt subs2)) fs1
val ss1' = map (apsnd (substt subs2)) ss1
in {fv = fs1' @ fs2, sv = ss1' @ ss2} end ;
(* occurs : term -> term -> bool, tells if variable occurs in term *)
fun occurs var (tm as Const ("GDC.formula.FV", _) $ _) = var = tm
| occurs var (tm as Const ("GDC.structr.SV", _) $ _) = var = tm
| occurs var (f $ a) = occurs var f orelse occurs var a
| occurs var (Const _) = false
| occurs var tm = raise TERM ("occurs: non-Const atom found", [tm]) ;
exception Clash of term * term ;
exception Occurs of term * term ;
(* unify : term * term -> sub
unifyl : term list * term list -> sub -> sub
unifies two terms, or two lists of terms, arg2 of unifyl is list of
substitutions already determined *)
fun unify (Const ("GDC.formula.FV", _) $ hstr1,
fv2 as Const ("GDC.formula.FV", _) $ hstr2) =
if hstr1 = hstr2 then fsvEmpty
else {fv = [(hstr1, fv2)], sv = []}
| unify (Const ("GDC.structr.SV", _) $ hstr1,
sv2 as Const ("GDC.structr.SV", _) $ hstr2) =
if hstr1 = hstr2 then fsvEmpty
else {sv = [(hstr1, sv2)], fv = []}
| unify (fv1 as Const ("GDC.formula.FV", _) $ hstr1, tm) =
if occurs fv1 tm then raise Occurs (fv1, tm)
else {fv = [(hstr1, tm)], sv = []}
| unify (tm, fv2 as Const ("GDC.formula.FV", _) $ hstr2) =
if occurs fv2 tm then raise Occurs (fv2, tm)
else {fv = [(hstr2, tm)], sv = []}
| unify (sv1 as Const ("GDC.structr.SV", _) $ hstr1, tm) =
if occurs sv1 tm then raise Occurs (sv1, tm)
else {fv = [], sv = [(hstr1, tm)]}
| unify (tm, sv2 as Const ("GDC.structr.SV", _) $ hstr2) =
if occurs sv2 tm then raise Occurs (sv2, tm)
else {fv = [], sv = [(hstr2, tm)]}
| unify (f1 $ a1, f2 $ a2) = unifyl ([f1, a1], [f2, a2]) fsvEmpty
| unify (tms as (tm1, tm2)) = if tm1 = tm2 then fsvEmpty else raise Clash tms
and unifyl (t1 :: tl1, t2 :: tl2) subsf =
let val st1 = substt subsf t1
val st2 = substt subsf t2
val tsubs = unify (st1, st2)
val csubs = compsubs subsf tsubs
in unifyl (tl1, tl2) csubs end
| unifyl ([], []) subsf = subsf ;
(* findXV : term -> {tm1:string list, tm2:string list} -> bool
determines which of two lists of strings a given HOL string is in,
checking that it is in exactly one of the two lists *)
fun findXV hstr {tm1 = strl1, tm2 = strl2} =
let val mlstr = h2ml_str hstr
val in1 = mlstr mem strl1
val in2 = mlstr mem strl2
val false = in1 = in2
in in1 end ;
(* splitp : (term * term) list -> {tm1:string list, tm2:string list} ->
{tm1: (term * term) list, tm2: (term * term) list}
splits a single list of substitutions (for either FV or SV) into
two lists, according to the var name being substituted for *)
fun splitp [] strl12 = {tm1 = [], tm2 = []}
| splitp ((hsub as (hstr, _)) :: hsubs) strl12 =
let val {tm1 = subs1, tm2 = subs2} = splitp hsubs strl12
in if findXV hstr strl12 then {tm1 = hsub :: subs1, tm2 = subs2}
else {tm1 = subs1, tm2 = hsub :: subs2} end ;
fun tmmap f {tm1, tm2} = {tm1 = f tm1, tm2 = f tm2} ;
fun tmcomp f {tm1 = p1, tm2 = p2} {tm1 = q1, tm2 = q2} =
{tm1 = f p1 q1, tm2 = f p2 q2} ;
(* split2 : sub -> {tm1: free_vars, tm2: free_vars} -> {tm1: sub, tm2: sub}
after unifying two terms, splits single list of substitutions into two,
according to the lists showing which variable was in which term originally *)
fun split2 {fv = fvSubs, sv = svSubs} rv12 =
let
val fvsplit = splitp fvSubs (tmmap fvs rv12)
val svsplit = splitp svSubs (tmmap #sv rv12)
in tmcomp mkfvs fvsplit svsplit end ;
(* delnv : ''a list -> (''a * 'b) list -> (''a * 'b) list
deletes substitutions from vsubs where item substituted is in newvs *)
fun delnv newvs vsubs =
let fun actsOnOld (var, _) = not (var mem newvs)
in filter actsOnOld vsubs end ;
(** perform matching of FVs and SVs, one way only **)
(* appSubs : (''a * term) list -> (''a * term) list -> (''a * term) list
append lists of substitutions, but eliminating duplications and
raising error where different replacement terms for one ''a value *)
fun appSubs [] subs2 = subs2
| appSubs ((v, tm) :: rsubs1) subs2 =
case assoc (subs2, v) of NONE =>
(v, tm) :: appSubs rsubs1 subs2
| SOME tm' =>
if tm = tm' then appSubs rsubs1 subs2 else raise Clash (tm, tm') ;
(* appfvSubs : sub -> sub -> sub
as for appSubs, append substitutions *)
fun appfvSubs subs1 subs2 = fsvcomp appSubs subs1 subs2 ;
(* match : term * term -> sub
matchl : term list * term list -> sub
matches two terms, or two lists of terms, ie works out substitutions
for FVs and SVs in arg1 only *)
fun match (Const ("GDC.formula.FV", _) $ hstr1, fml) =
{fv = [(hstr1, fml)], sv = []}
| match (Const ("GDC.structr.SV", _) $ hstr1, str) =
{sv = [(hstr1, str)], fv = []}
| match (f1 $ a1, f2 $ a2) = matchl ([f1, a1], [f2, a2])
| match (tms as (tm1, tm2)) = if tm1 = tm2 then fsvEmpty else raise Clash tms
and matchl (t1 :: tl1, t2 :: tl2) =
let val m = match (t1, t2)
val ml = matchl (tl1, tl2)
in appfvSubs m ml end
| matchl ([], []) = fsvEmpty ;
(** ML versions of HOL function **)
(* conclDT : term -> term *)
fun conclDT (Const ("HOL_DT.dertree.Der", _) $ seq $ rule $ dtl) = seq
| conclDT (Const ("HOL_DT.dertree.Unf", _) $ seq) = seq ;
(* conclRule : term -> term *)
fun conclRule (Const ("GDC.rule.Rule", _) $ prems $ concl) = concl
| conclRule (Const ("GDC.rule.Bidi", _) $ prem $ concl) = concl
| conclRule (Const ("GDC.rule.InvBidi", _) $ prem $ concl) = prem
| conclRule (Const ("HOL_Sub.invert", _) $ rule) =
let val [concl] = premsRule rule in concl end
(* premsRule : term -> term list *)
and premsRule (Const ("GDC.rule.Rule", _) $ prems $ concl) = h2ml_list prems
| premsRule (Const ("GDC.rule.Bidi", _) $ prem $ concl) = [prem]
| premsRule (Const ("GDC.rule.InvBidi", _) $ prem $ concl) = [concl]
| premsRule (Const ("HOL_Sub.invert", _) $ rule) = [conclRule rule] ;
(* findDTPCSub : term -> sub
finds substitution for rule at bottom of dertree, using premises
and conclusion of instantiated rule *)
fun findDTPCSub (Const ("HOL_DT.dertree.Der", _) $ seq $ rule $ dtl) = matchl
(conclRule rule :: premsRule rule, seq :: map conclDT (h2ml_list dtl)) ;
(* findSubSR : term -> term -> int ref -> sub * term list
finds the substitution needed for rule to get its conclusion to match seq,
and calculate the correspondingly substituted premises of rule ;
where FV or SV is in premises but not conclusion of rule,
create Isabelle variables for the replacement term *)
fun findSubSR seq rule maxref =
let
(* determine substitution to get seq from concl of rule *)
val sub = match (conclRule rule, seq) ;
(* extend with unknowns to cover all remaining variables in rule *)
val ruleVars = tmVars' rule fsvEmpty ; (* vars in rule *)
val subVars = fsvmap (map fst) sub ; (* vars in sub *)
val {fv = fdiffs, sv = sdiffs} = fsvcomp (curry (op \\)) ruleVars subVars ;
(* mkVarSub : typ -> term -> term * term
for an Isabelle/HOL string, make a pair of the string with a Var *)
fun mkVarSub ty hstr =
let val mlstr = h2ml_str hstr ;
val () = maxref := !maxref + 1 ;
val var = Var ((mlstr, !maxref), ty) ;
in (hstr, var) end ;
(* get pairs for all FVs or SVs in rule but not in seq *)
val vss = {fv = map (mkVarSub fmlT) fdiffs,
sv = map (mkVarSub strT) sdiffs} ;
val extSub = fsvcomp append vss sub ;
val subPrems = map (substt extSub) (premsRule rule) ;
in (extSub, subPrems) end ;