(* SSL.tac *)
(* the logical introduction rules are used here in the form where
logical operators are introduced on one side, and all premises and the
conclusion have the same single structure variable on the other side *)
val pr_bintr = make_prt ([ anda_int, ora, tA, fA RS EfqI, notbutA, butnotA ],
[ ands, ors_int, fS, tS RS VerI, rarrS, larrS ]) ;
val pr_rintr = make_prt ([], []) ;
val pr_intr = pr_append (pr_bintr, pr_rintr) ;
(* test
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
goal thy "*I, @( **A, I, **B) |- *@(I, **C), I, *( *@ D, I)" ;
goal thy "~(F -> A) & ~B |- ~C & D -> ~H v G" ;
goal thy "~(F v A) & ~B |- ~C & D v ~H v G" ; (* syntax error *)
goal thy "-(F + A) & -B |- C^ o D v -H" ;
goal thy "~(~C & D) & ( ~H v G) |- ~(F -> A) v ~B" ;
goal thy "~(-C & D) & ( -H v G) |- ~(F v A) v -B" ;
by (glob_tac (tfpr pr_intr) 1) ;
by (ALLGOALS (glob_tac (tfpr pr_ss))) ;
goal thy "~C & D -> ~E v G |- ~(F -> A) & ~B" ;
*)
(* test
goal thy "P -> (Q -> R) |- P & Q -> R";
bgt pr_intr ;
by (ALLGOALS weak_tac) ;
goal thy "P -> (Q -> R) |- ~( ~P & P)";
bgt pr_intr ;
by (ALLGOALS weak_tac) ;
*)