src/Sequents/prover.ML
changeset 2073 fb0655539d05
child 3538 ed9de44032e0
equal deleted inserted replaced
2072:6ac12b9478d5 2073:fb0655539d05
       
     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 less (ths@safes), unsafes);
       
    26 
       
    27 fun (Pack(safes,unsafes)) add_unsafes ths = 
       
    28     Pack(safes, sort less (ths@unsafes));
       
    29 
       
    30 
       
    31 (*Returns the list of all formulas in the sequent*)
       
    32 fun forms_of_seq (Const("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 (fn 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("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 STATE(fn state=> tac(nprems_of state)) end;
       
   206 
       
   207 (* Depth first search bounded by d *)
       
   208 fun solven_tac d n = STATE (fn 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 = STATE (fn state =>  
       
   218       if (nprems_of state = 0) then all_tac 
       
   219       else (DETERM(fres_safe_tac n)) ORELSE 
       
   220            (fres_unsafe_tac n APPEND fres_bound_tac n));
       
   221 
       
   222 end;
       
   223 end;