val derivableR_trans' = fold_rule dRdefs (prove_goalw GDT.thy dRdefs "prems' <= derivableR rules prems --> ?P" (fn _ => [ (rtac impI 1), (etac derrec_trans' 1)])) RS mp ; val [derivableR_trans, derivableRs_trans] = msc derivableR_trans' ; val IsDerivableR_trans = standard (rotate_prems 1 ( rewrite_rule [subset_def, symmetric (mk_eq IsDer_derR)] derivableR_trans)) ; (* ; val prems = it ; *) val Rmonos = [Un_upper1, Un_upper2] RL [IsDerivableR_rmono] ; val rmts = Rmonos RL [IsDerivableR_trans] ; val IsDerivableB_trans' = prove_goalw GDT.thy [IsDerivableB_def] "[| IsDerivableB rules prem inter ; IsDerivableB rules' inter concl |] \ \ ==> IsDerivableB (rules Un rules') prem concl" (fn prems => [(cut_facts_tac prems 1), (TRYALL (eresolve_tac rmts THEN' Simp_tac THEN' eresolve_tac Rmonos))]) ; val IsDerivableB_trans = IsDerivableB_trans' RS (Un_absorb RS equalityD1 RS IsDerivableB_rmono) ; (* NOT NEEDED val IsDerivableR_recur' = prove_goalw GDT.thy (map mk_eq [IsDer_derR, IsDer_derRs] @ drs.unfoldr :: dRdefs) "IsDerivableR rules prems concl = (concl : prems | (EX rule. \ \ concl = conclRule rule & rule : rulefs rules & \ \ IsDerivableRs rules prems (premsRule rule)))" (fn _ => [ (simp_tac (esimps [PC_def, image_iff]) 1), Fast_tac 1]) ; val IsDerivableR_recur = rewrite_rule [mk_eq IsDerRs_all] IsDerivableR_recur' ; *) val dts = derRs_all RS iffD1 RS derivableR_trans ; val isde = rewrite_rule [mk_eq IsDer_derR] IsDerivableE ; (* NOT NEEDED val [derivableR_deriv, derivableRs_deriv] = [prove_goalw GDT.thy dRdefs "(ALL rule:rules'. IsDerivable rules rule) --> \ \ (concl : derivableR rules' prems --> concl : derivableR rules prems) & \ \ (concls : derivableRs rules' prems --> concls : derivableRs rules prems)" (fn _ => [ (rtac impI 1), (rtac drs.induct 1), (TRYALL Fast_tac), (fold_tac dRdefs), (etac dts 1), (rotate_tac ~1 1), (etac thin_rl 1), (etac imageE 1), (etac rulefs.elim 1), (datac isde 1 1), (asm_full_simp_tac (esimps [PC_def, conclSub, premsSub]) 1), (etac derR_sub 1)]) RS mp] RL conjuncts RL [mp] ; val _ = bind_thm ("IsDerivableR_deriv", standard (fold_rule [mk_eq IsDer_derR] derivableR_deriv)) ; (* alternative proof *) val _ = qed_goalw "IsDerivableR_deriv" GDT.thy (mk_eq IsDer_derR :: dRdefs) "(ALL rule:rules'. IsDerivable rules rule) --> \ \ IsDerivableR rules' prems concl --> IsDerivableR rules prems concl" (fn _ => [ Safe_tac, (rtac derrec_deriv 1), atac 2, (chop_tac 1 (etac thin_rl 1)), Safe_tac, (etac rulefs.elim 1), (datac isde 1 1), (chop_tac 2 (etac thin_rl 1)), (asm_full_simp_tac (esimps [PC_def, conclSub, premsSub]) 1), (etac thin_rl 1), (etac thin_rl 1), (rewrite_tac (gderl_derrc :: symmetric derl_rr :: dRdefs)), (rtac der_mono 1), (rtac subset_refl 3), Simp_tac 1, (etac pscmap_derrec 1), (simp_tac (esimps [PC_rulefs_sub']) 1) ]) ; *)