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