(* derivations in dRA *) val () = qed_goal_spec_mp "bidiB" Ipfs.thy "RAbidi <= derB RArls" (fn _ => [ (simp_tac (esimps [derB.unfold]) 1), Safe_tac, (REPEAT (rtac exI 1)), Safe_tac, (REPEAT (rtac refl 1)), (ALLGOALS (rtac drl.singleI)), (ALLGOALS (eresolve_tac rls_intrs))]) ; fun mk_B bidi = bidi RS (bidiB RS subsetD) handle _ => bidi ; fun md1' th = mk_B th RS derBD1 ; fun md2' th = mk_B th RS derBD2 ; fun symm th = mk_B th RS derB_sym ; fun mk_rls rl = let val [th] = [rl] RL rls_intrs' in th end handle Bind => raise THM ("mk_rls", 0, [rl]) ; (* turn psc : pscrel into psc : derl pscrel but leave psc : derl pscrel alone *) val singleI = transfer Ipfs.thy drl.singleI ; val derl_derl = singleI RS derl_deriv ; fun mk_dr th = th RS derl_derl handle _ => mk_rls th RS singleI ; fun mii' th1 th2 = [mk_dr th1, mk_dr th2] MRS derB.derBI ; fun dsl_thm r1 n = prove_goal Ipfs.thy "(?qs, ?ps :: sequent list) : dersl ?r" let open drl in (fn _ => [ (EVERY (replicate (n-1) (rtac (asmI RS dtCons) 1))), (rtac dtCons 1), (rtac r1 1), (rtac asmsI 1)]) end ; infix RS' RSN' MRS' ; fun thm1 RSN' (n, thm2) = let val r1 = mk_dr thm1 ; val r2 = mk_dr thm2 ; val dt = simplify (simpset ()) (dsl_thm r1 n) ; val res = [r2, dt] MRS derl_trans ; in res end ; fun (th1 RS' th2) = th1 RSN' (1, th2) ; fun rls MRS' bottom_rl = let fun rs_aux i [] = bottom_rl | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls) in rs_aux 1 rls end; fun tn2 th1 th2 = [th1, th2] MRS derB_trans ; (* tn : thm list -> thm combines a list of bidirectional theorems *) fun tn [th] = mk_B th | tn (th :: ths) = tn2 (mk_B th) (tn ths) ; fun conj sym thm = tn [sym, thm, symm sym] ; (* much quicker than version using substitution defined in Isabelle *) open RAbidi RAlil RAlir RAbsru ; (* doesn't work use "derrls.ML" ; *)