src/Sequents/LK.ML

auto_bind_goal, auto_bind_facts;

(*  Title:      LK/LK.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)  
*)

open LK;

(*Higher precedence than := facilitates use of references*)
infix 4 add_safes add_unsafes;

(*Cut and thin, replacing the right-side formula*)
fun cutR_tac (sP: string) i = 
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;

(*Cut and thin, replacing the left-side formula*)
fun cutL_tac (sP: string) i = 
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);


(** If-and-only-if rules **)
qed_goalw "iffR" LK.thy [iff_def]
    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);

qed_goalw "iffL" LK.thy [iff_def]
   "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);

qed_goalw "TrueR" LK.thy [True_def]
    "$H |- $E, True, $F"
 (fn _=> [ rtac impR 1, rtac basic 1 ]);


(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)

qed_goal "allL_thin" LK.thy 
    "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
 (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);

qed_goal "exR_thin" LK.thy 
    "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
 (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);

(* Symmetry of equality in hypotheses *)
qed_goal "symL" LK.thy 
    "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
 (fn prems=>
  [ (rtac cut 1),
    (rtac thinL 2),
    (resolve_tac prems 2),
    (resolve_tac [basic RS sym] 1) ]);




(*The rules of LK*)
val prop_pack = empty_pack add_safes 
                [basic, refl, conjL, conjR, disjL, disjR, impL, impR, 
                 notL, notR, iffL, iffR];

val LK_pack = prop_pack add_safes   [allR, exL] 
                        add_unsafes [allL_thin, exR_thin];

val LK_dup_pack = prop_pack add_safes   [allR, exL] 
                            add_unsafes [allL, exR];



(** Contraction.  Useful since some rules are not complete. **)

qed_goal "conR" LK.thy 
    "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
 (fn prems=>
  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);

qed_goal "conL" LK.thy 
    "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
 (fn prems=>
  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);