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