src/Sequents/prover.ML
author paulson
Wed Jul 28 13:55:02 1999 +0200 (1999-07-28)
changeset 7122 87b233b31889
parent 7097 5ab37ed3d53c
child 7150 d203e2282789
permissions -rw-r--r--
renamed ...thm_pack... to ...pack...
     1 (*  Title:      Sequents/prover
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Simple classical reasoner for the sequent calculus, based on "theorem packs"
     7 *)
     8 
     9 
    10 (*Higher precedence than := facilitates use of references*)
    11 infix 4 add_safes add_unsafes;
    12 
    13 structure Cla =
    14 
    15 struct
    16 
    17 datatype pack = Pack of thm list * thm list;
    18 
    19 val trace = ref false;
    20 
    21 (*A theorem pack has the form  (safe rules, unsafe rules)
    22   An unsafe rule is incomplete or introduces variables in subgoals,
    23   and is tried only when the safe rules are not applicable.  *)
    24 
    25 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
    26 
    27 val empty_pack = Pack([],[]);
    28 
    29 fun warn_duplicates [] = []
    30   | warn_duplicates dups =
    31       (warning (String.concat ("Ignoring duplicate theorems:\n"::
    32 			       map (suffix "\n" o string_of_thm) dups));
    33        dups);
    34 
    35 fun (Pack(safes,unsafes)) add_safes ths   = 
    36     let val dups = warn_duplicates (gen_inter eq_thm (ths,safes))
    37 	val ths' = gen_rems eq_thm (ths,dups)
    38     in
    39         Pack(sort (make_ord less) (ths'@safes), unsafes)
    40     end;
    41 
    42 fun (Pack(safes,unsafes)) add_unsafes ths = 
    43     let val dups = warn_duplicates (gen_inter eq_thm (ths,unsafes))
    44 	val ths' = gen_rems eq_thm (ths,dups)
    45     in
    46 	Pack(safes, sort (make_ord less) (ths'@unsafes))
    47     end;
    48 
    49 fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) =
    50         Pack(sort (make_ord less) (safes@safes'), 
    51 	     sort (make_ord less) (unsafes@unsafes'));
    52 
    53 
    54 fun print_pack (Pack(safes,unsafes)) =
    55     (writeln "Safe rules:";  print_thms safes;
    56      writeln "Unsafe rules:"; print_thms unsafes);
    57 
    58 (*Returns the list of all formulas in the sequent*)
    59 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
    60   | forms_of_seq (H $ u) = forms_of_seq u
    61   | forms_of_seq _ = [];
    62 
    63 (*Tests whether two sequences (left or right sides) could be resolved.
    64   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
    65   Assumes each formula in seqc is surrounded by sequence variables
    66   -- checks that each concl formula looks like some subgoal formula.
    67   It SHOULD check order as well, using recursion rather than forall/exists*)
    68 fun could_res (seqp,seqc) =
    69       forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
    70                               (forms_of_seq seqp))
    71              (forms_of_seq seqc);
    72 
    73 
    74 (*Tests whether two sequents or pairs of sequents could be resolved*)
    75 fun could_resolve_seq (prem,conc) =
    76   case (prem,conc) of
    77       (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
    78        _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
    79 	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
    80     | (_ $ Abs(_,_,leftp) $ rightp,
    81        _ $ Abs(_,_,leftc) $ rightc) =>
    82 	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
    83     | _ => false;
    84 
    85 
    86 (*Like filt_resolve_tac, using could_resolve_seq
    87   Much faster than resolve_tac when there are many rules.
    88   Resolve subgoal i using the rules, unless more than maxr are compatible. *)
    89 fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
    90   let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
    91   in  if length rls > maxr  then  no_tac
    92 	  else (*((rtac derelict 1 THEN rtac impl 1
    93 		 THEN (rtac identity 2 ORELSE rtac ll_mp 2)
    94 		 THEN rtac context1 1)
    95 		 ORELSE *) resolve_tac rls i
    96   end);
    97 
    98 
    99 (*Predicate: does the rule have n premises? *)
   100 fun has_prems n rule =  (nprems_of rule = n);
   101 
   102 (*Continuation-style tactical for resolution.
   103   The list of rules is partitioned into 0, 1, 2 premises.
   104   The resulting tactic, gtac, tries to resolve with rules.
   105   If successful, it recursively applies nextac to the new subgoals only.
   106   Else fails.  (Treatment of goals due to Ph. de Groote) 
   107   Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
   108 
   109 (*Takes rule lists separated in to 0, 1, 2, >2 premises.
   110   The abstraction over state prevents needless divergence in recursion.
   111   The 9999 should be a parameter, to delay treatment of flexible goals. *)
   112 
   113 fun RESOLVE_THEN rules =
   114   let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
   115       fun tac nextac i state = state |>
   116 	     (filseq_resolve_tac rls0 9999 i 
   117 	      ORELSE
   118 	      (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
   119 	      ORELSE
   120 	      (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
   121 					    THEN  TRY(nextac i)))
   122   in  tac  end;
   123 
   124 
   125 
   126 (*repeated resolution applied to the designated goal*)
   127 fun reresolve_tac rules = 
   128   let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
   129       fun gtac i = restac gtac i
   130   in  gtac  end; 
   131 
   132 (*tries the safe rules repeatedly before the unsafe rules. *)
   133 fun repeat_goal_tac (Pack(safes,unsafes)) = 
   134   let val restac  =    RESOLVE_THEN safes
   135       and lastrestac = RESOLVE_THEN unsafes;
   136       fun gtac i = restac gtac i  
   137 	           ORELSE  (if !trace then
   138 				(print_tac "" THEN lastrestac gtac i)
   139 			    else lastrestac gtac i)
   140   in  gtac  end; 
   141 
   142 
   143 (*Tries safe rules only*)
   144 fun safe_tac (Pack(safes,unsafes)) = reresolve_tac safes;
   145 
   146 val safe_goal_tac = safe_tac;   (*backwards compatibility*)
   147 
   148 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
   149 fun step_tac (pack as Pack(safes,unsafes)) =
   150     safe_tac pack  ORELSE'
   151     filseq_resolve_tac unsafes 9999;
   152 
   153 
   154 (* Tactic for reducing a goal, using Predicate Calculus rules.
   155    A decision procedure for Propositional Calculus, it is incomplete
   156    for Predicate-Calculus because of allL_thin and exR_thin.  
   157    Fails if it can do nothing.      *)
   158 fun pc_tac pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac pack 1));
   159 
   160 
   161 (*The following two tactics are analogous to those provided by 
   162   Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
   163 fun fast_tac pack =
   164   SELECT_GOAL (DEPTH_SOLVE (step_tac pack 1));
   165 
   166 fun best_tac pack  = 
   167   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
   168 	       (step_tac pack 1));
   169 
   170 
   171 
   172 structure ProverArgs =
   173   struct
   174   val name = "Sequents/prover";
   175   type T = pack ref;
   176   val empty = ref empty_pack
   177   fun copy (ref pack) = ref pack;
   178   val prep_ext = copy;
   179   fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   180   fun print _ (ref pack) = print_pack pack;
   181   end;
   182 
   183 structure ProverData = TheoryDataFun(ProverArgs);
   184 
   185 val prover_setup = [ProverData.init];
   186 
   187 val print_pack = ProverData.print;
   188 val pack_ref_of_sg = ProverData.get_sg;
   189 val pack_ref_of = ProverData.get;
   190 
   191 (* access global pack *)
   192 
   193 val pack_of_sg = ! o pack_ref_of_sg;
   194 val pack_of = pack_of_sg o sign_of;
   195 
   196 val pack = pack_of o Context.the_context;
   197 val pack_ref = pack_ref_of_sg o sign_of o Context.the_context;
   198 
   199 
   200 (* change global pack *)
   201 
   202 fun change_pack f x = pack_ref () := (f (pack (), x));
   203 
   204 val Add_safes = change_pack (op add_safes);
   205 val Add_unsafes = change_pack (op add_unsafes);
   206 
   207 
   208 fun Fast_tac st = fast_tac (pack()) st;
   209 fun Step_tac st = step_tac (pack()) st;
   210 fun Safe_tac st = safe_tac (pack()) st;
   211 fun Pc_tac st   = pc_tac (pack()) st;
   212 
   213 end;
   214 
   215 
   216 open Cla;