(** proofs for lkss **) (* inductive proof of weakening *) val () = ListPair.app bind_thm (["lk_weak", "lk_weaks"], msc (prove_goal lkdt.thy "(seq : derrec lkss prems --> \ \ extendb pp seq : derrec lkss (extendb pp ` prems)) & \ \ (seqs : dersrec lkss prems --> \ \ map (extendb pp) seqs : dersrec lkss (extendb pp ` prems))" (fn _ => [ (rtac drs.induct 1), (rtac drs.dpI 1), (dtac lk_ext_ext 2), (rewtac (mk_eq pscmap_def)), (eatac drs.derI 1 2), Auto_tac]))) ; val () = ListPair.app bind_thm (["lk_weakd", "lk_weakds"], msc (prove_goal lkdt.thy "((ps, c) : derl lkss --> \ \ (map (extendb pp) ps, extendb pp c) : derl lkss) & \ \ ((qs, cs) : dersl lkss --> \ \ (map (extendb pp) qs, map (extendb pp) cs) : dersl lkss)" (fn _ => [ (rtac drl.induct 1), (dtac lk_ext_ext 2), (rewtac (mk_eq pscmap_def)), (eatac drl.dtderI 1 2), (ALLGOALS Simp_tac), (eatac drl.dtCons 1 1)]))) ; val lk_weakile = prove_goal lkdt.thy "([], X |- Y) : derl lkss --> ([], A # X |- Y) : derl lkss" (fn _ => [ (rtac impI 1), (dres_inst_tac [("pp", "(([A], []), ([], []))")] lk_weakd 1), (Asm_full_simp_tac 1)]) RS mp ; val lk_weakire = prove_goal lkdt.thy "([], X |- Y) : derl lkss --> ([], X |- A # Y) : derl lkss" (fn _ => [ (rtac impI 1), (dres_inst_tac [("pp", "(([], [A]), ([], []))")] lk_weakd 1), (Asm_full_simp_tac 1)]) RS mp ; val () = qed_goal_spec_mp "lkwa" lkdt.thy "(X |- Y) : derrec lkss {} --> (Xl @ X @ Xr |- Yl @ Y @ Yr) : derrec lkss {}" (fn _ => [ Safe_tac, (dres_inst_tac [("pp", "((Xl, Yl), (Xr, Yr))")] lk_weak 1), Full_simp_tac 1]) ; val lkwal = rewrite_rule [drr_empty] lkwa ; val lk_ax = simplify (simpset ()) (lkne.axiom RS lkss.extI) ; val lk_axd = fold_rule [drr_empty] (transfer lkdt.thy lk_ax RS drl.singleI) ; val () = qed_goal_spec_mp "lkw_ax" lkdt.thy "A mem X --> A mem Y --> (X |- Y) : derrec lkss {}" (fn _ => [ (force_tac (cesimps [mem_alt, lk_axd]) 1)]) ; (* don't think we want this (** derive lks-style rules in lk **) fun dstrans (rl1, rl2) = ([rl2, transfer lkdt.thy rl1] MRS ds_trans) ; fun tryuse2 (rl1, rl2) = let open drl in ([rl2, transfer lkdt.thy rl1 RS singleI RS singleton] MRS dtderI) end ; local open lkil lkir in val [andl1r, andl2r, orr1r, orr2r, impr1r, impr2r] = map (hd o mk_rule_lk o ric) [andl1, andl2, orr1, orr2, impr1, impr2] ; val [andr', orl', impl', negl', negr'] = map (hd o mk_rule_lk o ric) [andr, orl, impl, negl, negr] ; end ; val eqE = transfer lkdt.thy drl.eqE ; val singleI = transfer lkdt.thy drl.singleI ; (* single, rather than paired, introduction rules *) val andl = foldr1 dstrans [andl1r RS singleI, icl RS eqE, andl2r RS singleI, iil RS eqE] ; val orr = foldr1 dstrans [orr1r RS singleI, icr RS eqE, orr2r RS singleI, iir RS eqE] ; val impr = foldr1 dstrans [impr2r RS singleI, impr1r RS singleI, iir RS eqE] ; (* get these rules in an form to use weakening *) val uwsr = [orr, impr] RL [drl.singleton RSN (2, derl_trans)] ; val uwsl = [andl] RL [drl.singleton RSN (2, derl_trans)] ; fun mkw rl = let val th1 = ([transfer lkdt.thy rl, dersl_all RS iffD2] MRS (drl.singleI RS derl_trans)) ; val th2 = full_simplify (simpset ()) th1 ; in meta_std th2 end ; val fwr = map mkw [andr', negr'] ; val fwl = map mkw [orl', impl', negl'] ; val srlsr = (uwsr @ fwr) ; val srlsl = (uwsl @ fwl) ; *)