(* things in Genrules specific to the sort of structure *) structure Genrules_nested = struct local open Genrules_structr in val Const (NSVname, _) = term_of (read_cterm GDC.thy ("NSV", TypeInfer.logicT)) ; type free_vars = {fv : string list, nsv : string list} ; (* tmVars : term -> free_vars -> free_vars collect free variables (ie FV and SV), augmenting the free_vars argument *) fun tmVars (Const (name, _) $ hstr) (fsvs as {fv = fvs, nsv = svs}) = if name = FVname then {fv = consNew (h2ml_str hstr) fvs, nsv = svs} else if name = NSVname then {fv = fvs, nsv = consNew (h2ml_str hstr) svs} else tmVars hstr fsvs | tmVars (f $ a) fsvs = tmVars f (tmVars a fsvs) | tmVars (Const _) fsvs = fsvs | tmVars (Var _) fsvs = fsvs | tmVars (Free _) fsvs = fsvs | tmVars tm fsvs = raise TERM ("tmVars: non-Const/Var/Free atom found", [tm]) ; val fnsvEmpty = {fv = [], nsv = []} ; (* NB this is different from the one in gen/HOLinML.ML *) (* note - fmlT, strT, etc, defined 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) ; (* val u = mksubs (tvar "'nseq") svstrs ; val t = tm_nFind ; *) fun mkfssubs {fv = fvstrs, nsv = svstrs} = let fun f $ x = apply_unify GSub.thy f x ; val pfsub = ml2h_pair (tm_pFind $ mksubs (tvar "'string") [], tm_fFind $ mksubs (tvar "'fml") fvstrs) ; in ml2h_pair (pfsub, tm_nFind $ mksubs (tvar "'nseq") svstrs) end ; (* TO CHANGE FROM rulefs to nrulefs *) (* this is copied from ind_rls.ML and changed *) (* 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 nrulefs.iisubI) ; val Const ("Trueprop", _) $ (Const ("op :", _) $ rtm $ rset) = concl_of sthm ; val sub = cterm_of (sign_of GSub.thy) (mkfssubs (tmVars rtm fnsvEmpty)) ; val cti = cterm_instantiate [(sub1, sub)] (sthm RS nrulefs.iisubI) ; val ss = simpset_of GSub.thy addsimps ([pFind_def, fFind_def, nFind_def, Bidi_def'] @ conn_defs) ; val sres = simplify ss cti ; in sres end ; val def_to_in = def_imp_eq RS (prove_goal Main.thy "(x = y) --> y : {x}" fn_at RS mp) ; (* 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) ; val pcfs_mono' = mk_mono nrulefs_mono RSN (2, mk_mono' image_mono) ; fun mk_pc_mono fth = fth RS nrulefs_mono ; val mk_gpcm = mk_pc_mono o mk_gen_def ; fun mk_dgpcm th = mk_gpcm th RS drl.singleI ; end ; (* local open Genrules_structr *) end ; (* structure Genrules_nested *) (* val rdef = ands ; val rdef = cs1 ; val sthm = rdef RS def_to_in ; mk_gen_def rdef ; mk_Ivar_rule sthm ; set show_sorts ; reset show_sorts ; (prin it, type_of it) ; *)