(* mkIsPrB' : thm -> thm mkIsPrB' turns, eg, "rssA == Bidi prem concl" into "IsDerivableB {rssA} prem concl" mkIsPrB does that and also leaves "IsDerivableB rules prem concl" unchanged *) local val ai = read_instantiate_sg (sign_of GDT.thy) [("f", "%r. IsDerivableB {r}")] arg_cong ; val ip_cong = def_imp_eq RS ai RS fun_cong RS fun_cong RS iffD2 ; val tipc = transfer meta_proofs.thy ip_cong ; in fun mkIsPrB' def = IsDerivable_Bidi RS (def RS tipc) end ; fun mkIsPrB rule = case concl_of rule of Const ("==", _) $ name $ (Const ("GDC.rule.Bidi", _) $ p $ c) => mkIsPrB' rule | Const ("Trueprop", _) $ (Const ("GDT.IsDerivableB", _) $ r $ p $ c) => rule ; (* mkIsPrR' : thm -> thm mkIsPrR' turns, eg, "ors == Rule prems concl" into "IsDerivableR {ors} (set prems) concl" mkIsPrR does that and also leaves "IsDerivableR rules prs concl" unchanged *) local val ai = read_instantiate_sg (sign_of GDT.thy) [("f", "%r. IsDerivableR {r}")] arg_cong ; val ip_cong = def_imp_eq RS ai RS fun_cong RS fun_cong RS iffD2 ; val tipc = transfer meta_proofs.thy ip_cong ; in fun mkIsPrR' def = IsDerivable_Rule RS (def RS tipc) end ; fun mkIsPrR rule = case concl_of rule of Const ("==", _) $ name $ (Const ("GDC.rule.Rule", _) $ p $ c) => (* simplify to turn set [...] into {...} *) simplify (simpset_of List_thy) (mkIsPrR' rule) | Const ("Trueprop", _) $ (Const ("GDT.IsDerivableR", _) $ r $ p $ c) => rule ; use "unify.ML" ; use "derivs.ML" ; open RA_Rls ; (* as rules like rssA also defined in RA_Ind *) use "derrls.ML" ; (* push_proof() ; goal thy "PROP ?P" ; handle e => print_exn e ; val m = #mss (rep_ss (simpset())) ; val s = #simps (dest_mss m) ; *)