(* NB this is different from the one in gen/HOLinML.ML *) fun mksub xT mlstr = ml2h_pair (ml2h_str mlstr, Var ((mlstr, 0), xT)) ; fun mksubs xT mlstrs = ml2h_list (pairT (stringT, xT)) (map (mksub xT) mlstrs) ; (* mkfssubs : {fv:string list, sv:string list} -> term make a HOL substitution, such as (([], [(''A'', ?A), (''B'', ?B)]), [(''X'', ?X), (''Y'', ?Y)]) *) fun mkfssubs {fv = fvstrs, sv = svstrs} = let val pfsub = ml2h_pair (tm_pFind $ mksubs stringT [], tm_fFind $ mksubs fmlT fvstrs) ; in ml2h_pair (pfsub, tm_sFind $ mksubs strT svstrs) end ; (* mkfssubs {fv = ["A", "B"], sv = ["X", "Y", "Z", "W"]} ; cterm_of (sign_of GSub.thy) it ; *) (* an alternative to mkgenR/B, where Isabelle thm is (literal rule <= some set) *) fun mk_Ivar_rule sthm = let val sub1 = (left' o left' o arg' o right') (cprop_of rulefs.iisubI) ; val Const ("Trueprop", _) $ (Const ("op :", _) $ rtm $ rset) = concl_of sthm ; val sub = cterm_of (sign_of GSub.thy) (mkfssubs (tmVars rtm fsvEmpty)) ; val cti = cterm_instantiate [(sub1, sub)] (sthm RS rulefs.iisubI) ; val sres = simplify (simpset_of GSub.thy addsimps (Bidi_def :: conn_defs)) cti ; in sres end ; val def_to_in = def_imp_eq RS (prove_goal Main.thy "(x = y) --> y : {x}" fn_at RS mp) ; val PC_imageI = read_instantiate_sg GDC.thy [("f", "PC")] imageI ; (* mk_gen_def : thm -> thm given a rule definition like "sA == Bidi ( * $''X'' |- $''Y'') ( * $''Y'' |- $''X'')" turns it into "Rule [* $?X |- $?Y] ( * $?Y |- $?X) : rulefs {sA}" mk_pc : thm -> thm turns this into "([...], ...) : PC ` rulefs {sA}" mk_pc_mono : thm -> thm turns this into "{sA} <= rules ==> ([...], ...) : PC ` rulefs rules" *) fun mk_gen_def rdef = mk_Ivar_rule (rdef RS def_to_in) ; fun mk_pc rth = rewrite_rule [mk_eq PC_Rule] (rth RS PC_imageI) ; val pcfs_mono' = mk_mono rulefs_mono RSN (2, mk_mono' image_mono) ; fun mk_pc_mono fth = fth RS pcfs_mono' ; val mk_gpcm = mk_pc_mono o mk_pc o mk_gen_def ; fun mk_dgpcm th = mk_gpcm th RS drl.singleI ; (* can use these funtions with drl.singleI, drl.dtderI, etc val rth = mk_gen_def taga ; val fth = mk_pc rth ; val mth = mk_pc_mono fth ; *)