src/Sequents/prover.ML
author paulson
Mon Dec 28 17:03:47 1998 +0100 (1998-12-28)
changeset 6054 4a4f6ad607a1
parent 4440 9ed4098074bc
child 7097 5ab37ed3d53c
permissions -rw-r--r--
added new arg for print_tac
     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  
   110 	           ORELSE  (print_tac "" THEN lastrestac gtac i)
   111   in  gtac  end; 
   112 
   113 
   114 (*Tries safe rules only*)
   115 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
   116 
   117 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
   118 fun step_tac (thm_pack as Pack(safes,unsafes)) =
   119     safe_goal_tac thm_pack  ORELSE'
   120     filseq_resolve_tac unsafes 9999;
   121 
   122 
   123 (* Tactic for reducing a goal, using Predicate Calculus rules.
   124    A decision procedure for Propositional Calculus, it is incomplete
   125    for Predicate-Calculus because of allL_thin and exR_thin.  
   126    Fails if it can do nothing.      *)
   127 fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
   128 
   129 
   130 (*The following two tactics are analogous to those provided by 
   131   Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
   132 fun fast_tac thm_pack =
   133   SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
   134 
   135 fun best_tac thm_pack  = 
   136   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
   137 	       (step_tac thm_pack 1));
   138 
   139 
   140 
   141 signature MODAL_PROVER_RULE =
   142 sig
   143     val rewrite_rls      : thm list
   144     val safe_rls         : thm list
   145     val unsafe_rls       : thm list
   146     val bound_rls        : thm list
   147     val aside_rls        : thm list
   148 end;
   149 
   150 signature MODAL_PROVER = 
   151 sig
   152     val rule_tac   : thm list -> int ->tactic
   153     val step_tac   : int -> tactic
   154     val solven_tac : int -> int -> tactic
   155     val solve_tac  : int -> tactic
   156 end;
   157 
   158 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
   159 struct
   160 local open Modal_Rule
   161 in 
   162 
   163 (*Returns the list of all formulas in the sequent*)
   164 fun forms_of_seq (Const("Sequents.SeqO",_) $ P $ u) = P :: forms_of_seq u
   165   | forms_of_seq (H $ u) = forms_of_seq u
   166   | forms_of_seq _ = [];
   167 
   168 (*Tests whether two sequences (left or right sides) could be resolved.
   169   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
   170   Assumes each formula in seqc is surrounded by sequence variables
   171   -- checks that each concl formula looks like some subgoal formula.*)
   172 fun could_res (seqp,seqc) =
   173       forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
   174                               (forms_of_seq seqp))
   175              (forms_of_seq seqc);
   176 
   177 (*Tests whether two sequents G|-H could be resolved, comparing each side.*)
   178 fun could_resolve_seq (prem,conc) =
   179   case (prem,conc) of
   180       (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
   181        _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
   182           could_res (leftp,leftc)  andalso  could_res (rightp,rightc)
   183     | _ => false;
   184 
   185 (*Like filt_resolve_tac, using could_resolve_seq
   186   Much faster than resolve_tac when there are many rules.
   187   Resolve subgoal i using the rules, unless more than maxr are compatible. *)
   188 fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
   189   let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
   190   in  if length rls > maxr  then  no_tac  else resolve_tac rls i
   191   end);
   192 
   193 fun fresolve_tac rls n = filseq_resolve_tac rls 999 n;
   194 
   195 (* NB No back tracking possible with aside rules *)
   196 
   197 fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));
   198 fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
   199 
   200 val fres_safe_tac = fresolve_tac safe_rls;
   201 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
   202 val fres_bound_tac = fresolve_tac bound_rls;
   203 
   204 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
   205                                     else tf(i) THEN tac(i-1)
   206                     in fn st => tac (nprems_of st) st end;
   207 
   208 (* Depth first search bounded by d *)
   209 fun solven_tac d n state = state |>
   210        (if d<0 then no_tac
   211         else if (nprems_of state = 0) then all_tac 
   212         else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
   213                  ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
   214                    (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
   215 
   216 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
   217 
   218 fun step_tac n = 
   219     COND (has_fewer_prems 1) all_tac 
   220          (DETERM(fres_safe_tac n) ORELSE 
   221 	  (fres_unsafe_tac n APPEND fres_bound_tac n));
   222 
   223 end;
   224 end;