src/Sequents/prover.ML
changeset 7097 5ab37ed3d53c
parent 6054 4a4f6ad607a1
child 7122 87b233b31889
equal deleted inserted replaced
7096:8c9278991d9c 7097:5ab37ed3d53c
     1 (*  Title:      LK/LK.ML
     1 (*  Title:      LK/LK.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
       
     5 
       
     6 Simple classical reasoner for the sequent calculus, based on "theorem packs"
     5 *)
     7 *)
     6 
     8 
     7 
     9 
     8 (**** Theorem Packs ****)
       
     9 
    10 
    10 (* based largely on LK *)
    11 (*Higher precedence than := facilitates use of references*)
       
    12 infix 4 add_safes add_unsafes;
    11 
    13 
    12 datatype pack = Pack of thm list * thm list;
    14 datatype pack = Pack of thm list * thm list;
    13 
    15 
    14 (*A theorem pack has the form  (safe rules, unsafe rules)
    16 (*A theorem pack has the form  (safe rules, unsafe rules)
    15   An unsafe rule is incomplete or introduces variables in subgoals,
    17   An unsafe rule is incomplete or introduces variables in subgoals,
    17 
    19 
    18 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
    20 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
    19 
    21 
    20 val empty_pack = Pack([],[]);
    22 val empty_pack = Pack([],[]);
    21 
    23 
    22 infix 4 add_safes add_unsafes;
    24 fun warn_duplicates [] = []
       
    25   | warn_duplicates dups =
       
    26       (warning (String.concat ("Ignoring duplicate theorems:\n"::
       
    27 			       map (suffix "\n" o string_of_thm) dups));
       
    28        dups);
    23 
    29 
    24 fun (Pack(safes,unsafes)) add_safes ths   = 
    30 fun (Pack(safes,unsafes)) add_safes ths   = 
    25     Pack(sort (make_ord less) (ths@safes), unsafes);
    31     let val dups = warn_duplicates (gen_inter eq_thm (ths,safes))
       
    32 	val ths' = gen_rems eq_thm (ths,dups)
       
    33     in
       
    34         Pack(sort (make_ord less) (ths'@safes), unsafes)
       
    35     end;
    26 
    36 
    27 fun (Pack(safes,unsafes)) add_unsafes ths = 
    37 fun (Pack(safes,unsafes)) add_unsafes ths = 
    28     Pack(safes, sort (make_ord less) (ths@unsafes));
    38     let val dups = warn_duplicates (gen_inter eq_thm (ths,unsafes))
       
    39 	val ths' = gen_rems eq_thm (ths,dups)
       
    40     in
       
    41 	Pack(safes, sort (make_ord less) (ths'@unsafes))
       
    42     end;
       
    43 
       
    44 fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) =
       
    45         Pack(sort (make_ord less) (safes@safes'), 
       
    46 	     sort (make_ord less) (unsafes@unsafes'));
    29 
    47 
    30 
    48 
       
    49 fun print_pack (Pack(safes,unsafes)) =
       
    50     (writeln "Safe rules:";  print_thms safes;
       
    51      writeln "Unsafe rules:"; print_thms unsafes);
       
    52 
    31 (*Returns the list of all formulas in the sequent*)
    53 (*Returns the list of all formulas in the sequent*)
    32 fun forms_of_seq (Const("Sequents.SeqO'",_) $ P $ u) = P :: forms_of_seq u
    54 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
    33   | forms_of_seq (H $ u) = forms_of_seq u
    55   | forms_of_seq (H $ u) = forms_of_seq u
    34   | forms_of_seq _ = [];
    56   | forms_of_seq _ = [];
    35 
    57 
    36 (*Tests whether two sequences (left or right sides) could be resolved.
    58 (*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.
    59   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
   110 	           ORELSE  (print_tac "" THEN lastrestac gtac i)
   132 	           ORELSE  (print_tac "" THEN lastrestac gtac i)
   111   in  gtac  end; 
   133   in  gtac  end; 
   112 
   134 
   113 
   135 
   114 (*Tries safe rules only*)
   136 (*Tries safe rules only*)
   115 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
   137 fun safe_tac (Pack(safes,unsafes)) = reresolve_tac safes;
       
   138 
       
   139 val safe_goal_tac = safe_tac;   (*backwards compatibility*)
   116 
   140 
   117 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
   141 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
   118 fun step_tac (thm_pack as Pack(safes,unsafes)) =
   142 fun step_tac (thm_pack as Pack(safes,unsafes)) =
   119     safe_goal_tac thm_pack  ORELSE'
   143     safe_tac thm_pack  ORELSE'
   120     filseq_resolve_tac unsafes 9999;
   144     filseq_resolve_tac unsafes 9999;
   121 
   145 
   122 
   146 
   123 (* Tactic for reducing a goal, using Predicate Calculus rules.
   147 (* Tactic for reducing a goal, using Predicate Calculus rules.
   124    A decision procedure for Propositional Calculus, it is incomplete
   148    A decision procedure for Propositional Calculus, it is incomplete
   136   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
   160   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
   137 	       (step_tac thm_pack 1));
   161 	       (step_tac thm_pack 1));
   138 
   162 
   139 
   163 
   140 
   164 
   141 signature MODAL_PROVER_RULE =
   165 structure ProverArgs =
   142 sig
   166   struct
   143     val rewrite_rls      : thm list
   167   val name = "Sequents/prover";
   144     val safe_rls         : thm list
   168   type T = pack ref;
   145     val unsafe_rls       : thm list
   169   val empty = ref empty_pack
   146     val bound_rls        : thm list
   170   fun copy (ref pack) = ref pack;
   147     val aside_rls        : thm list
   171   val prep_ext = copy;
   148 end;
   172   fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
       
   173   fun print _ (ref pack) = print_pack pack;
       
   174   end;
   149 
   175 
   150 signature MODAL_PROVER = 
   176 structure ProverData = TheoryDataFun(ProverArgs);
   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 
   177 
   158 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
   178 val prover_setup = [ProverData.init];
   159 struct
       
   160 local open Modal_Rule
       
   161 in 
       
   162 
   179 
   163 (*Returns the list of all formulas in the sequent*)
   180 val print_thm_pack = ProverData.print;
   164 fun forms_of_seq (Const("Sequents.SeqO",_) $ P $ u) = P :: forms_of_seq u
   181 val thm_pack_ref_of_sg = ProverData.get_sg;
   165   | forms_of_seq (H $ u) = forms_of_seq u
   182 val thm_pack_ref_of = ProverData.get;
   166   | forms_of_seq _ = [];
       
   167 
   183 
   168 (*Tests whether two sequences (left or right sides) could be resolved.
   184 (* access global thm_pack *)
   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 
   185 
   177 (*Tests whether two sequents G|-H could be resolved, comparing each side.*)
   186 val thm_pack_of_sg = ! o thm_pack_ref_of_sg;
   178 fun could_resolve_seq (prem,conc) =
   187 val thm_pack_of = thm_pack_of_sg o sign_of;
   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 
   188 
   185 (*Like filt_resolve_tac, using could_resolve_seq
   189 val thm_pack = thm_pack_of o Context.the_context;
   186   Much faster than resolve_tac when there are many rules.
   190 val thm_pack_ref = thm_pack_ref_of_sg o sign_of o Context.the_context;
   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 
   191 
   193 fun fresolve_tac rls n = filseq_resolve_tac rls 999 n;
       
   194 
   192 
   195 (* NB No back tracking possible with aside rules *)
   193 (* change global thm_pack *)
   196 
   194 
   197 fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));
   195 fun change_thm_pack f x = thm_pack_ref () := (f (thm_pack (), x));
   198 fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
       
   199 
   196 
   200 val fres_safe_tac = fresolve_tac safe_rls;
   197 val Add_safes = change_thm_pack (op add_safes);
   201 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
   198 val Add_unsafes = change_thm_pack (op add_unsafes);
   202 val fres_bound_tac = fresolve_tac bound_rls;
       
   203 
   199 
   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;