src/Sequents/prover.ML

fixed comment;

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


(**** Theorem Packs ****)

(* based largely on LK *)

datatype pack = Pack of thm list * thm list;

(*A theorem pack has the form  (safe rules, unsafe rules)
  An unsafe rule is incomplete or introduces variables in subgoals,
  and is tried only when the safe rules are not applicable.  *)

fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);

val empty_pack = Pack([],[]);

infix 4 add_safes add_unsafes;

fun (Pack(safes,unsafes)) add_safes ths   = 
    Pack(sort (make_ord less) (ths@safes), unsafes);

fun (Pack(safes,unsafes)) add_unsafes ths = 
    Pack(safes, sort (make_ord less) (ths@unsafes));


(*Returns the list of all formulas in the sequent*)
fun forms_of_seq (Const("Sequents.SeqO'",_) $ P $ u) = P :: forms_of_seq u
  | forms_of_seq (H $ u) = forms_of_seq u
  | forms_of_seq _ = [];

(*Tests whether two sequences (left or right sides) could be resolved.
  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
  Assumes each formula in seqc is surrounded by sequence variables
  -- checks that each concl formula looks like some subgoal formula.
  It SHOULD check order as well, using recursion rather than forall/exists*)
fun could_res (seqp,seqc) =
      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
                              (forms_of_seq seqp))
             (forms_of_seq seqc);


(*Tests whether two sequents or pairs of sequents could be resolved*)
fun could_resolve_seq (prem,conc) =
  case (prem,conc) of
      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
    | (_ $ Abs(_,_,leftp) $ rightp,
       _ $ Abs(_,_,leftc) $ rightc) =>
	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
    | _ => false;


(*Like filt_resolve_tac, using could_resolve_seq
  Much faster than resolve_tac when there are many rules.
  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
  in  if length rls > maxr  then  no_tac
	  else (*((rtac derelict 1 THEN rtac impl 1
		 THEN (rtac identity 2 ORELSE rtac ll_mp 2)
		 THEN rtac context1 1)
		 ORELSE *) resolve_tac rls i
  end);


(*Predicate: does the rule have n premises? *)
fun has_prems n rule =  (nprems_of rule = n);

(*Continuation-style tactical for resolution.
  The list of rules is partitioned into 0, 1, 2 premises.
  The resulting tactic, gtac, tries to resolve with rules.
  If successful, it recursively applies nextac to the new subgoals only.
  Else fails.  (Treatment of goals due to Ph. de Groote) 
  Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)

(*Takes rule lists separated in to 0, 1, 2, >2 premises.
  The abstraction over state prevents needless divergence in recursion.
  The 9999 should be a parameter, to delay treatment of flexible goals. *)

fun RESOLVE_THEN rules =
  let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
      fun tac nextac i state = state |>
	     (filseq_resolve_tac rls0 9999 i 
	      ORELSE
	      (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
	      ORELSE
	      (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
					    THEN  TRY(nextac i)))
  in  tac  end;



(*repeated resolution applied to the designated goal*)
fun reresolve_tac rules = 
  let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
      fun gtac i = restac gtac i
  in  gtac  end; 

(*tries the safe rules repeatedly before the unsafe rules. *)
fun repeat_goal_tac (Pack(safes,unsafes)) = 
  let val restac  =    RESOLVE_THEN safes
      and lastrestac = RESOLVE_THEN unsafes;
      fun gtac i = restac gtac i  ORELSE  (print_tac THEN lastrestac gtac i)
  in  gtac  end; 


(*Tries safe rules only*)
fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;

(*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
fun step_tac (thm_pack as Pack(safes,unsafes)) =
    safe_goal_tac thm_pack  ORELSE'
    filseq_resolve_tac unsafes 9999;


(* Tactic for reducing a goal, using Predicate Calculus rules.
   A decision procedure for Propositional Calculus, it is incomplete
   for Predicate-Calculus because of allL_thin and exR_thin.  
   Fails if it can do nothing.      *)
fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));


(*The following two tactics are analogous to those provided by 
  Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
fun fast_tac thm_pack =
  SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));

fun best_tac thm_pack  = 
  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
	       (step_tac thm_pack 1));



signature MODAL_PROVER_RULE =
sig
    val rewrite_rls      : thm list
    val safe_rls         : thm list
    val unsafe_rls       : thm list
    val bound_rls        : thm list
    val aside_rls        : thm list
end;

signature MODAL_PROVER = 
sig
    val rule_tac   : thm list -> int ->tactic
    val step_tac   : int -> tactic
    val solven_tac : int -> int -> tactic
    val solve_tac  : int -> tactic
end;

functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
struct
local open Modal_Rule
in 

(*Returns the list of all formulas in the sequent*)
fun forms_of_seq (Const("Sequents.SeqO",_) $ P $ u) = P :: forms_of_seq u
  | forms_of_seq (H $ u) = forms_of_seq u
  | forms_of_seq _ = [];

(*Tests whether two sequences (left or right sides) could be resolved.
  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
  Assumes each formula in seqc is surrounded by sequence variables
  -- checks that each concl formula looks like some subgoal formula.*)
fun could_res (seqp,seqc) =
      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
                              (forms_of_seq seqp))
             (forms_of_seq seqc);

(*Tests whether two sequents G|-H could be resolved, comparing each side.*)
fun could_resolve_seq (prem,conc) =
  case (prem,conc) of
      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
          could_res (leftp,leftc)  andalso  could_res (rightp,rightc)
    | _ => false;

(*Like filt_resolve_tac, using could_resolve_seq
  Much faster than resolve_tac when there are many rules.
  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
  in  if length rls > maxr  then  no_tac  else resolve_tac rls i
  end);

fun fresolve_tac rls n = filseq_resolve_tac rls 999 n;

(* NB No back tracking possible with aside rules *)

fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));
fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;

val fres_safe_tac = fresolve_tac safe_rls;
val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
val fres_bound_tac = fresolve_tac bound_rls;

fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
                                    else tf(i) THEN tac(i-1)
                    in fn st => tac (nprems_of st) st end;

(* Depth first search bounded by d *)
fun solven_tac d n state = state |>
       (if d<0 then no_tac
        else if (nprems_of state = 0) then all_tac 
        else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
                 ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
                   (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));

fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;

fun step_tac n = 
    COND (has_fewer_prems 1) all_tac 
         (DETERM(fres_safe_tac n) ORELSE 
	  (fres_unsafe_tac n APPEND fres_bound_tac n));

end;
end;