(* weak.tac - for Kt *)
(* tactics for completing a proof by weakening *)
(* type sti : sub-term info; in (term, (side, ol), ast)
term is the formula, without initial Structform (_),
(side, ol) indicates the location in the sequent,
ast = Ant (Suc) for antecedent (succedent) part *)
type sti = (term * (side * oppos list) * side) ;
(* flaux : term -> (side * oppos list) -> side -> sti list -> sti list
auxiliary function for form_list,
flaux tm (side, rloc) ast sofar looks at subterm tm, whose location in the
sequent is indicated by side and reverse of rloc,
with ast indicating whether it is antecedent or succedent,
and sofar is the list of formulae already found *)
fun flaux (Const ("KS.,", _) $ L $ R) (side, rloc) ast sofar =
flaux R (side, Right :: rloc) ast (flaux L (side, Left :: rloc) ast sofar)
| flaux (Const ("KS.*", _) $ U) (side, rloc) ast sofar =
flaux U (side, Un :: rloc) (oppside ast) sofar
| flaux (Const ("DL.Structform", _) $ F) (side, rloc) ast sofar =
(F, (side, rev rloc), ast) :: sofar
| flaux tm _ _ sofar = sofar ;
(* form_list : term -> sti list
creates list of formulae in a sequent, list is of sti tuples
Note - doesn't look underneath ;, because it is for doing simple proof
by weakening and identity of formulae *)
fun form_list (Const ("DL.Sequent", _) $ L $ R) =
flaux R (Suc, []) Suc (flaux L (Ant, []) Ant []) ;
(* tm_cmp : term -> term -> bool, true if terms compare equal *)
fun tm_cmp (O1 $ U1) (O2 $ U2) = tm_cmp O1 O2 andalso tm_cmp U1 U2
| tm_cmp op1 op2 = (op1 = op2) ;
(* tsi_cmp : sti -> sti -> bool
true if two terms tm1 and tm2 equal
and one each antecedent and succedent (as shown by side) *)
fun tsi_cmp (tm1, _, side1) (tm2, _, side2) =
tm_cmp tm1 tm2 andalso (side1 = oppside side2) ;
(* tsi_match : sti -> sti list -> (sti * sti) option
finds the first entry in the list which matches (in the sense of tsi_cmp) tsi
*)
fun tsi_match tsi (tsil::tsis) =
(if tsi_cmp tsi tsil then SOME (tsi, tsil) else tsi_match tsi tsis)
| tsi_match tsi [] = NONE ;
(* first_match : sti list -> (sti * sti) option
finds the first two entries in the list which match (in the sense of tsi_cmp)
*)
fun first_match (tsi::tsis) =
(case tsi_match tsi tsis of NONE => first_match tsis
| tsim => tsim)
| first_match [] = NONE ;
fun simp_thm (stmt, thm) =
prove_goal (theory_of_thm thm) stmt
(fn prems => [rtac (prems MRS thm) 1]) ;
val sxI = simp_thm ("$I |- $X ==> *$X |- $I", exs RS md1 sA) ;
val Isx = simp_thm ("$X |- $I ==> $I |- *$X", exa RS md1 sS) ;
open KSKeep ;
(* test
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@l*", "-r*"] 1) ;
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@l*", "-l*"] 1) ;
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@r*", "-r*"] 1) ;
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@r*", "-l*"] 1) ;
*)
(* weak_tac : tactic
performs weakening to get A |- A or similar *)
fun weak_tac sg state =
case first_match (form_list (nth (prems_of state, sg-1))) of
NONE => all_tac state
| SOME ((_, sol1, _), (_, sol2, _)) =>
(keep_tac_sol [sol1, sol2] sg
(* next step converts @($X, $Y) |- $I, $I |- *($X, $Y), etc *)
(* was
THEN REPEAT (rtac sxI, Isx, bxI, Ibx] sg) *)
THEN bup_tac (tfpr pr_dist) sg
(* next steps converts $X, $Y |- $I or $I |- $X, $Y *)
THEN TRY (rtac (mra RS md2 cs1) sg)
THEN TRY (rtac (mls RS md2 ca1) sg)
(* bup_tac needed for * @ @ * - is one enough ? *)
THEN bup_tac (tfpr pr_dbl) sg
THEN TRY (rtac (md1 dcp) sg)
THEN rtac idf sg)
state ;