src/Sequents/prover.ML
author wenzelm
Fri Dec 19 10:13:47 1997 +0100 (1997-12-19)
changeset 4440 9ed4098074bc
parent 3948 3428c0a88449
child 6054 4a4f6ad607a1
permissions -rw-r--r--
adapted to new sort function;
     1 (*  Title:      LK/LK.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 *)
     6 
     7 
     8 (**** Theorem Packs ****)
     9 
    10 (* based largely on LK *)
    11 
    12 datatype pack = Pack of thm list * thm list;
    13 
    14 (*A theorem pack has the form  (safe rules, unsafe rules)
    15   An unsafe rule is incomplete or introduces variables in subgoals,
    16   and is tried only when the safe rules are not applicable.  *)
    17 
    18 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
    19 
    20 val empty_pack = Pack([],[]);
    21 
    22 infix 4 add_safes add_unsafes;
    23 
    24 fun (Pack(safes,unsafes)) add_safes ths   = 
    25     Pack(sort (make_ord less) (ths@safes), unsafes);
    26 
    27 fun (Pack(safes,unsafes)) add_unsafes ths = 
    28     Pack(safes, sort (make_ord less) (ths@unsafes));
    29 
    30 
    31 (*Returns the list of all formulas in the sequent*)
    32 fun forms_of_seq (Const("Sequents.SeqO'",_) $ P $ u) = P :: forms_of_seq u
    33   | forms_of_seq (H $ u) = forms_of_seq u
    34   | forms_of_seq _ = [];
    35 
    36 (*Tests whether two sequences (left or right sides) could be resolved.
    37   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
    38   Assumes each formula in seqc is surrounded by sequence variables
    39   -- checks that each concl formula looks like some subgoal formula.
    40   It SHOULD check order as well, using recursion rather than forall/exists*)
    41 fun could_res (seqp,seqc) =
    42       forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
    43                               (forms_of_seq seqp))
    44              (forms_of_seq seqc);
    45 
    46 
    47 (*Tests whether two sequents or pairs of sequents could be resolved*)
    48 fun could_resolve_seq (prem,conc) =
    49   case (prem,conc) of
    50       (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
    51        _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
    52 	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
    53     | (_ $ Abs(_,_,leftp) $ rightp,
    54        _ $ Abs(_,_,leftc) $ rightc) =>
    55 	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
    56     | _ => false;
    57 
    58 
    59 (*Like filt_resolve_tac, using could_resolve_seq
    60   Much faster than resolve_tac when there are many rules.
    61   Resolve subgoal i using the rules, unless more than maxr are compatible. *)
    62 fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
    63   let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
    64   in  if length rls > maxr  then  no_tac
    65 	  else (*((rtac derelict 1 THEN rtac impl 1
    66 		 THEN (rtac identity 2 ORELSE rtac ll_mp 2)
    67 		 THEN rtac context1 1)
    68 		 ORELSE *) resolve_tac rls i
    69   end);
    70 
    71 
    72 (*Predicate: does the rule have n premises? *)
    73 fun has_prems n rule =  (nprems_of rule = n);
    74 
    75 (*Continuation-style tactical for resolution.
    76   The list of rules is partitioned into 0, 1, 2 premises.
    77   The resulting tactic, gtac, tries to resolve with rules.
    78   If successful, it recursively applies nextac to the new subgoals only.
    79   Else fails.  (Treatment of goals due to Ph. de Groote) 
    80   Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
    81 
    82 (*Takes rule lists separated in to 0, 1, 2, >2 premises.
    83   The abstraction over state prevents needless divergence in recursion.
    84   The 9999 should be a parameter, to delay treatment of flexible goals. *)
    85 
    86 fun RESOLVE_THEN rules =
    87   let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
    88       fun tac nextac i state = state |>
    89 	     (filseq_resolve_tac rls0 9999 i 
    90 	      ORELSE
    91 	      (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
    92 	      ORELSE
    93 	      (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
    94 					    THEN  TRY(nextac i)))
    95   in  tac  end;
    96 
    97 
    98 
    99 (*repeated resolution applied to the designated goal*)
   100 fun reresolve_tac rules = 
   101   let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
   102       fun gtac i = restac gtac i
   103   in  gtac  end; 
   104 
   105 (*tries the safe rules repeatedly before the unsafe rules. *)
   106 fun repeat_goal_tac (Pack(safes,unsafes)) = 
   107   let val restac  =    RESOLVE_THEN safes
   108       and lastrestac = RESOLVE_THEN unsafes;
   109       fun gtac i = restac gtac i  ORELSE  (print_tac THEN lastrestac gtac i)
   110   in  gtac  end; 
   111 
   112 
   113 (*Tries safe rules only*)
   114 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
   115 
   116 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
   117 fun step_tac (thm_pack as Pack(safes,unsafes)) =
   118     safe_goal_tac thm_pack  ORELSE'
   119     filseq_resolve_tac unsafes 9999;
   120 
   121 
   122 (* Tactic for reducing a goal, using Predicate Calculus rules.
   123    A decision procedure for Propositional Calculus, it is incomplete
   124    for Predicate-Calculus because of allL_thin and exR_thin.  
   125    Fails if it can do nothing.      *)
   126 fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
   127 
   128 
   129 (*The following two tactics are analogous to those provided by 
   130   Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
   131 fun fast_tac thm_pack =
   132   SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
   133 
   134 fun best_tac thm_pack  = 
   135   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
   136 	       (step_tac thm_pack 1));
   137 
   138 
   139 
   140 signature MODAL_PROVER_RULE =
   141 sig
   142     val rewrite_rls      : thm list
   143     val safe_rls         : thm list
   144     val unsafe_rls       : thm list
   145     val bound_rls        : thm list
   146     val aside_rls        : thm list
   147 end;
   148 
   149 signature MODAL_PROVER = 
   150 sig
   151     val rule_tac   : thm list -> int ->tactic
   152     val step_tac   : int -> tactic
   153     val solven_tac : int -> int -> tactic
   154     val solve_tac  : int -> tactic
   155 end;
   156 
   157 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
   158 struct
   159 local open Modal_Rule
   160 in 
   161 
   162 (*Returns the list of all formulas in the sequent*)
   163 fun forms_of_seq (Const("Sequents.SeqO",_) $ P $ u) = P :: forms_of_seq u
   164   | forms_of_seq (H $ u) = forms_of_seq u
   165   | forms_of_seq _ = [];
   166 
   167 (*Tests whether two sequences (left or right sides) could be resolved.
   168   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
   169   Assumes each formula in seqc is surrounded by sequence variables
   170   -- checks that each concl formula looks like some subgoal formula.*)
   171 fun could_res (seqp,seqc) =
   172       forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
   173                               (forms_of_seq seqp))
   174              (forms_of_seq seqc);
   175 
   176 (*Tests whether two sequents G|-H could be resolved, comparing each side.*)
   177 fun could_resolve_seq (prem,conc) =
   178   case (prem,conc) of
   179       (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
   180        _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
   181           could_res (leftp,leftc)  andalso  could_res (rightp,rightc)
   182     | _ => false;
   183 
   184 (*Like filt_resolve_tac, using could_resolve_seq
   185   Much faster than resolve_tac when there are many rules.
   186   Resolve subgoal i using the rules, unless more than maxr are compatible. *)
   187 fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
   188   let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
   189   in  if length rls > maxr  then  no_tac  else resolve_tac rls i
   190   end);
   191 
   192 fun fresolve_tac rls n = filseq_resolve_tac rls 999 n;
   193 
   194 (* NB No back tracking possible with aside rules *)
   195 
   196 fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));
   197 fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
   198 
   199 val fres_safe_tac = fresolve_tac safe_rls;
   200 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
   201 val fres_bound_tac = fresolve_tac bound_rls;
   202 
   203 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
   204                                     else tf(i) THEN tac(i-1)
   205                     in fn st => tac (nprems_of st) st end;
   206 
   207 (* Depth first search bounded by d *)
   208 fun solven_tac d n state = state |>
   209        (if d<0 then no_tac
   210         else if (nprems_of state = 0) then all_tac 
   211         else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
   212                  ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
   213                    (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
   214 
   215 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
   216 
   217 fun step_tac n = 
   218     COND (has_fewer_prems 1) all_tac 
   219          (DETERM(fres_safe_tac n) ORELSE 
   220 	  (fres_unsafe_tac n APPEND fres_bound_tac n));
   221 
   222 end;
   223 end;