(* ML functions to imitate dRA derivations in HOL *) uses "unify.ML" ; (* subPrR, subPrB : sub -> thm -> thm performs substitution in theorem of form "IsDerivableR/B ..." *) fun subPr th subs rule = let val varSub = (left' o right' o arg' o right') (cprop_of th) ; val hsub = sub2pfsSubst subs ; val chsub = cterm_of (sign_of HOL_Sub.thy) hsub ; val isprb = cterm_instantiate [(varSub, chsub)] th ; val issp = simplify (simpset_of HOL_Sub.thy) (rule RS isprb) ; in issp end ; val subPrB = subPr IsDerivableB_sub ; val subPrR = subPr IsDerivableR_sub ; fun prsub sub = prin (sub2pfsSubst sub) ; (* sort_rules : thm -> thm -> thm in a theorem of form "IsDerivableR/B rules ...", where rules are given by name, sort them and remove duplicates; thrb is IsDerivableR_rmono or IsDerivableB_rmono *) fun sort_rules thrb isprb = let val hrules = (left o funct o arg) (concl_of isprb) ; fun comp (Const (str1, _), Const (str2, _)) = string_ord (str1, str2) ; val srules = msort (mergeElimDup comp) (h2ml_set hrules) ; val hsr = ml2h_set ruleT srules ; val g = Trueprop $ subset' ruleT hrules hsr ; val cg = cterm_of (sign_of HOL_Rls.thy) g ; val sth = prove_goalw_cterm [] cg (fn _ => [Simp_tac 1]) ; val rth = [sth, isprb] MRS thrb ; in rth end ; val sort_rulesB = sort_rules IsDerivableB_rmono ; val sort_rulesR = sort_rules IsDerivableR_rmono ; (* sepRules : term -> term -> term * free_ren * {tm1 : free_vars, tm2 : free_vars} returns first rule with variables different from second rule, also returns the substitutions used, and the free variables of the new rule1, and of rule2 *) fun sepRules rule1 rule2 = let val rv1 as {fv = fv1, sv = sv1} = tmVars rule1 fsvEmpty ; val rv2 as {fv = fv2, sv = sv2} = tmVars rule2 fsvEmpty ; val (fvRens, fv1') = variant_pairs fv1 fv2 ; val (svRens, sv1') = variant_pairs sv1 sv2 ; val rens = {fv = fvRens, sv = svRens} ; val rv1' = {fv = fv1', sv = sv1'} ; val subs = rens2subs rens ; val rule1' = substt subs rule1 ; in (rule1', rens, {tm1 = rv1', tm2 = rv2}) end ; (* getsubs : sub -> term * free_ren * {tm1 : free_vars, tm2 : free_vars} -> {tm1 : sub, tm2 : sub} takes result of unification and result of separating two original rules and returns separate substitutions for two original rules *) fun getsubs usubs (_, rens1, rv12) = let val {tm1 = subs1, tm2 = subs2} = split2 usubs rv12 ; (* incorporate original renaming of vars *) val rensubs1 = (rens2subs rens1) ; val subs1' = compsubs rensubs1 subs1 ; (* delete substitutions that act on renamed vars *) val newvars = fsvmap (map (ml2h_str o snd)) rens1 ; val subs1'' = fsvcomp delnv newvars subs1' ; in {tm1 = subs1'', tm2 = subs2} end ; structure StdDers = struct val op MRS = op MRS ; val op RS = op RS ; val op RSN = op RSN ; val bind_st_thm = bind_st_thm ; (* val conj = conj ; *) val md1 = md1 ; val md2 = md2 ; val mii = mii ; (* val mrsn = mrsn ; *) val symmetric = symmetric ; (* val tn = tn ; val tn2 = tn2 ; *) end ; structure LocalDers = struct (* tn2 : thm -> thm -> thm for r1, r2 both thms of form "IsDerivableB rulesi pi ci", combines them transitively to give "IsDerivableB ... p1 c2" *) fun tn2 r1 r2 = let val t1 = concl_of r1 ; val t2 = concl_of r2 ; val srr as (t1', rens1, rv12) = sepRules t1 t2 ; val c1 = right (arg t1') ; val p2 = left (arg t2) ; val usubs = unify (c1, p2) ; val {tm1 = subs1'', tm2 = subs2} = getsubs usubs srr ; val th = [subPrB subs1'' r1, subPrB subs2 r2] MRS IsDerivableB_trans' ; in sort_rulesB th end ; (* code to imitate derivations done in dRA, where a bidirectional rule (using ==) becomes an IsDerivableB theorem, and an ordinary rule (using ==>) becomes an IsDerivableR theorem *) (* val isPrBi' = prove_goal HOL_DT.thy "Ball concls (IsDerivableR rules prems) ==> \ \ Ball (insert seq concls) (IsDerivableR rules (insert seq prems))" (fn [prem] => [ Safe_tac, rtac IsDerivableR_refl' 1, rtac insertI1 1, dtac (prem RS bspec) 1, (etac (reop rev IsDerivableR_mono) 1), rtac subset_insertI 1]) ; *) local open Drule val thr = ([Un_upper1, IsDerivableR_mono] MRS IsDerivableR_rmono) ; val bi = conjI RS (nth (ball_simps, 6) RS iffD2) ; val bem = TrueI RS (ball_empty RS iffD2) ; val isPrUnTr = Un_upper2 RS IsDerivableR_rmono RS IsDerivableR_trans ; val tac = EVERY [rtac bi 1, rtac IsDerivableR_refl' 1, Simp_tac 1] ; val bi' = read_instantiate_sg (sign_of HOL_DT.thy) [("P1", "IsDerivableR ?r ?p")] bi ; val isPrBi = IsDerivableR_refl' RS bi' ; val tac = EVERY [rtac isPrBi 1, Simp_tac 1] ; in fun thm1 RSN (n, thm2) = let val r1 = mkIsPrR thm1 ; val r2 = mkIsPrR thm2 ; val t1 = concl_of r1 ; val t2 = concl_of r2 ; val srr as (t1', rens1, rv12) = sepRules t1 t2 ; val c1 = right (arg t1') ; val p2 = hset_nth (n-1) (left (arg t2)) ; val usubs = unify (c1, p2) ; val {tm1 = subs1'', tm2 = subs2} = getsubs usubs srr ; val th1 = subPrR subs1'' r1 ; val th2 = subPrR subs2 r2 ; val tp $ (isp $ rules1 $ ps1 $ c1) = (concl_of th1) ; val _ $ (_ $ rules2 $ ps2 $ c2) = (concl_of th2) ; val newps = hset_sub (n-1) ps2 ps1 ; val urules = Un ruleT rules1 rules2 ; val g = tp $ (isp $ urules $ newps $ c2) ; val cg = cterm_of (sign_of meta_proofs.thy) g ; val thr1 = Drule.RSN (th1, (2, thr)) ; val tacn = EVERY (replicate (n-1) tac) ; val th = prove_goalw_cterm [] cg (fn _ => [ rtac isPrUnTr 1, rtac (th2) 1, tacn, EVERY [rtac bi 1, rtac thr1 1, Simp_tac 1], REPEAT tac, (rtac bem 1)]) ; in sort_rulesR th end ; end ; (* local for defining RSN *) (* cut RSN (1, cut) ; cut RSN (2, cut) ; *) fun th1 RS th2 = th1 RSN (1, th2) ; (* mrsn : int -> thm list -> thm -> thm like MRS but starting on premise number n of thl *) fun mrsn n [] thl = thl | mrsn n (th :: ths) thl = th RSN (n, mrsn (n+1) ths thl) ; fun ths MRS thl = mrsn 1 ths thl ; (* tn : thm list -> thm combines a list of theorems in transitive style, theorems may be "IsDerivableB ..." or definition of a Bidi *) fun tn [th] = mkIsPrB th | tn (th :: ths) = tn2 (mkIsPrB th) (tn ths) ; local open Drule ; val brr = IsDerivableB_def RS def_imp_eq RS iffD1 ; in fun symmetric th = mkIsPrB th RS IsDerivableB_sym ; fun conj sym thm = tn [sym, thm, symmetric sym] ; fun bind_st_thm (name, stmt, thm) = bind_thm (name, thm) ; fun md1 isprb = mkIsPrB isprb RS brr RS conjunct1 ; fun md2 isprb = mkIsPrB isprb RS brr RS conjunct2 ; fun mii thm1 thm2 = let val r1 = mkIsPrR thm1 ; val r2 = mkIsPrR thm2 ; val t1 = concl_of r1 ; val t2 = concl_of r2 ; val srr as (t1', rens1, rv12) = sepRules t1 t2 ; val _ $ (_ $ (Const ("insert", _) $ p1 $ Const ("{}", _)) $ c1) = t1' ; val _ $ (_ $ (Const ("insert", _) $ p2 $ Const ("{}", _)) $ c2) = t2 ; val usubs = unifyl ([p1, c1], [c2, p2]) fsvEmpty ; val {tm1 = subs1'', tm2 = subs2} = getsubs usubs srr ; val th1 = subPrR subs1'' r1 ; val th2 = subPrR subs2 r2 ; val uth = [th1, th2] MRS IsDerivableBI' ; in sort_rulesB uth end ; end ; (* local *) end ; (* structure LocalDers *)