(* weak.tac - for relation algebra, where @ is self-inverse *)
(* tactics for completing a proof by weakening *)
(* type sti : sub-term info; in (term, (side, ol), ast, blobs)
term is the formula, without initial Structform (_),
(side, ol) indicates the location in the sequent,
ast = Ant (Suc) for antecedent (succedent) part
blobs = the number of preceding blobs (mod 2) *)
type sti = (term * (side * oppos list) * side * int) ;
(* flaux : term -> (side * oppos list) -> side -> int -> sti list -> sti list
auxiliary function for form_list,
flaux tm (side, rloc) ast blobs 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,
blobs indicating the number of preceding blobs (mod
2), and sofar is the list of formulae already found *)
fun flaux (Const ("RS.,", _) $ L $ R) (side, rloc) ast blobs sofar =
flaux R (side, Right :: rloc) ast blobs
(flaux L (side, Left :: rloc) ast blobs sofar)
| flaux (Const ("RS.@", _) $ U) (side, rloc) ast blobs sofar =
flaux U (side, Un :: rloc) ast (1-blobs) sofar
| flaux (Const ("RS.*", _) $ U) (side, rloc) ast blobs sofar =
flaux U (side, Un :: rloc) (oppside ast) blobs sofar
| flaux (Const ("DL.Structform", _) $ F) (side, rloc) ast blobs sofar =
(F, (side, rev rloc), ast, blobs) :: 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 0 (flaux L (Ant, []) Ant 0 []) ;
(* 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)
and same number of preceding blobs (mod2) (as shown by blobs1 and blobs2) *)
fun tsi_cmp (tm1, _, side1, blobs1) (tm2, _, side2, blobs2) =
tm_cmp tm1 tm2 andalso (side1 = oppside side2) andalso (blobs1 = blobs2) ;
(* 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) ;
val bxI = simp_thm ("$X |- $I ==> @$X |- $I", exa RS md2 mblob) ;
val Ibx = simp_thm ("$I |- $X ==> $I |- @$X", exs RS md1 mblob) ;
open RSKeep ;
(* 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 bsA) sg)
THEN TRY (rtac (md1 bsS) sg)
THEN TRY (rtac (md1 blbl) sg)
THEN TRY (rtac (md1 dcp) sg)
THEN rtac idf sg)
state ;