(* lconv.tac, search-and-replace with HOL-like conversionals, uses record for methods and Ant | Suc for side of sequent, uses special action type to avoid problems found when using exceptions ; generic - applies to general display logics *) signature LCONV = sig val SUBaf : 'a Meth.meth -> 'a actfn -> 'a actfn ; (* uses dptab *) val BUaf : 'a meth -> 'a actfn -> 'a actfn ; val TDFaf : 'a meth -> 'a actfn -> 'a actfn ; val TDaf : 'a meth -> 'a actfn -> 'a actfn ; val fbl_fun : thm actfn -> thm -> thm ; val fbl_s_fun : side -> thm actfn -> thm -> thm ; val fgl_fun : thm actfn -> thm -> thm ; val rep_fbl_fun : thm actfn -> thm -> thm ; val rep_fgl_fun : thm actfn -> thm -> thm ; val bup_tac : thm Seq.seq actfn -> int -> tactic ; val glob_tac : thm Seq.seq actfn -> int -> tactic ; val glob_s_tac : side -> thm Seq.seq actfn -> int -> tactic ; val rep_bup_tac : thm Seq.seq actfn -> int -> tactic ; val rep_glob_tac : thm Seq.seq actfn -> int -> tactic ; val bgt : Pat.patrules -> unit ; val bbt : Pat.patrules -> unit ; end ; functor LConv (Dptab : DPTAB) : LCONV = struct local open Meth in (* SUBaf : 'a meth -> 'a actfn -> 'a actfn applies action function to immediate subterms of term *) fun SUBaf meth actfn tm asp = case tm of (binop $ L $ R) => THENact meth (let val (dp, sdp, newside) = dpassoc (Dptab.dptab, (asp, binop, Left)) in conjact2 meth (dp, sdp) (actfn L newside) end, let val (dp, sdp, newside) = dpassoc (Dptab.dptab, (asp, binop, Right)) in conjact2 meth (dp, sdp) (actfn R newside) end) | (Const ("DL.Structform", _) $ U) => Unc | (unop $ U) => (let val (dp, sdp, newside) = dpassoc (Dptab.dptab, (asp, unop, Un)) in conjact2 meth (dp, sdp) (actfn U newside) end handle _ => raise Fail "LConv.SUBaf,unop") | _ => Unc ; (* TDaf, BUaf : 'a meth -> 'a actfn -> 'a actfn goes through whole structure looking for sub-structures which will be changed by af; TDaf in top-down order, BUaf in bottom-up order *) fun TDaf meth af tm = THENaf meth (REPaf meth af, SUBaf meth (TDaf meth af)) tm ; fun BUaf meth af tm = THENaf meth (SUBaf meth (BUaf meth af), REPaf meth af) tm ; (* TDFaf : 'a meth -> 'a actfn -> 'a actfn goes through whole structure, in top-down order, looking for first sub-structures in any branch which will be changed by af *) fun TDFaf meth af tm = ELSEaf meth (af, SUBaf meth (TDFaf meth af)) tm ; fun unc_af tm asp = Unc ; val glob_tac = afl2tac TDaf ; val bup_tac = afl2tac BUaf ; fun glob_s_tac side = (sidesel side (ant_tac, suc_tac) bwd_methods o TDaf bwd_methods) ; val rep_glob_tac = bs_tac bwd_methods o REPaf bwd_methods o TDaf bwd_methods ; val rep_bup_tac = bs_tac bwd_methods o REPaf bwd_methods o BUaf bwd_methods ; val fgl_fun = afl2fun TDaf ; val fbl_fun = afl2fun BUaf ; (* just to act on one side, use ant_tac or suc_tac, not bs_tac *) fun fbl_s_fun side actfn = (sidesel side (ant_tac, suc_tac) fwd_methods o BUaf fwd_methods) actfn 0 ; fun rep_fgl_fun actfn = (bs_tac fwd_methods o REPaf fwd_methods o TDaf fwd_methods) actfn 0 ; fun rep_fbl_fun actfn = (bs_tac fwd_methods o REPaf fwd_methods o BUaf fwd_methods) actfn 0 ; end ; (* local open Meth *) fun bgt patrules = by (ALLGOALS (glob_tac (Pat.tfpr patrules))) ; fun bbt patrules = by (ALLGOALS (bup_tac (Pat.tfpr patrules))) ; end ; (* functor LConv *) (* structure LConv = LConv (Dptab) ; open LConv LConv.Meth ; *) (* testing, for RA val tt = topthm() ; val (Const ("DL.Sequent", _) $ L $ R) = hd (prems_of tt) ; val nd = mknew (tfpr pr_dbl) ; val ndi = mknew (tfpr pr_dist) ; fun byaf af sg = by (bs_tac bwd_methods af sg) ; val m = bwd_methods ; val gnd = TDaf m nd ; val bnd = BUaf m nd ; val rnd = REPaf m nd ; val snd = SUBaf m nd ; val tnd = TRYaf m nd ; goal thy "@* *@ * * X |- * @@* * * Y" ; chop() ; by (glob_tac (tfpr pr_dbl) 1) ; by (bup_tac (tfpr pr_dbl) 1) ; by (rep_glob_tac (tfpr pr_dbl) 1) ; goal thy "* *@ * * X |- *@@@* * * Y" ; goal thy "* *@@ * * X |- *@@@* * * Y" ; goal thy "* *@@ * * X |- **@@@* * * Y" ; val [p] = goal thy "(@* *@ * * X |- * @@* * * Y) ==> PROP Q" ; val q = fgl_fun (ffpr fpr_dbl) p ; val q = fgl_fun (ffpr fpr_dbl) q ; val q = rep_fgl_fun (ffpr fpr_dbl) p ; val q = fbl_fun (ffpr fpr_dbl) p ; val [p] = goal thy "( * *@ @* * X |- * * *@@ * Y) ==> PROP Q" ; *) (* goal thy "* (( * A, @ * (B; C)); ( * B, @ * (C; A))) |- * -R + -S " ; by (glob_tac (tfpr pr_dd) 1) ; chop() ; by (bup_tac (tfpr pr_dd) 1) ; by (rep_bup_tac (tfpr pr_dd) 1) ; val [p] = goal thy "[|* (( * A, @ * (B; C)); ( * B, @ * (C; A))) |- * -R + -S|] ==> PROP Q" ; val q = fgl_fun (ffpr fpr_dd) p ; val q = fbl_fun (ffpr fpr_dd) p ; val q = fbl_fun (ffpr fpr_dd) q ; val q = rep_fbl_fun (ffpr fpr_dd) p ; *)