src/Sequents/prover.ML
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (21 months ago)
changeset 66924 b4d4027f743b
parent 64556 851ae0e7b09c
child 69593 3dda49e08b9d
permissions -rw-r--r--
more permissive;
     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 signature CLA =
     9 sig
    10   type pack
    11   val empty_pack: pack
    12   val get_pack: Proof.context -> pack
    13   val put_pack: pack -> Proof.context -> Proof.context
    14   val pretty_pack: Proof.context -> Pretty.T
    15   val add_safe: thm -> Proof.context -> Proof.context
    16   val add_unsafe: thm -> Proof.context -> Proof.context
    17   val safe_add: attribute
    18   val unsafe_add: attribute
    19   val method: (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    20   val trace: bool Config.T
    21   val forms_of_seq: term -> term list
    22   val safe_tac: Proof.context -> int -> tactic
    23   val step_tac: Proof.context -> int -> tactic
    24   val pc_tac: Proof.context -> int -> tactic
    25   val fast_tac: Proof.context -> int -> tactic
    26   val best_tac: Proof.context -> int -> tactic
    27 end;
    28 
    29 structure Cla: CLA =
    30 struct
    31 
    32 (** rule declarations **)
    33 
    34 (*A theorem pack has the form  (safe rules, unsafe rules)
    35   An unsafe rule is incomplete or introduces variables in subgoals,
    36   and is tried only when the safe rules are not applicable.  *)
    37 
    38 fun less (rl1, rl2) = Thm.nprems_of rl1 < Thm.nprems_of rl2;
    39 val sort_rules = sort (make_ord less);
    40 
    41 datatype pack = Pack of thm list * thm list;
    42 
    43 val empty_pack = Pack ([], []);
    44 
    45 structure Pack = Generic_Data
    46 (
    47   type T = pack;
    48   val empty = empty_pack;
    49   val extend = I;
    50   fun merge (Pack (safes, unsafes), Pack (safes', unsafes')) =
    51     Pack
    52      (sort_rules (Thm.merge_thms (safes, safes')),
    53       sort_rules (Thm.merge_thms (unsafes, unsafes')));
    54 );
    55 
    56 val put_pack = Context.proof_map o Pack.put;
    57 val get_pack = Pack.get o Context.Proof;
    58 fun get_rules ctxt = let val Pack rules = get_pack ctxt in rules end;
    59 
    60 
    61 (* print pack *)
    62 
    63 fun pretty_pack ctxt =
    64   let val (safes, unsafes) = get_rules ctxt in
    65     Pretty.chunks
    66      [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes),
    67       Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)]
    68   end;
    69 
    70 val _ =
    71   Outer_Syntax.command @{command_keyword print_pack} "print pack of classical rules"
    72     (Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of)));
    73 
    74 
    75 (* declare rules *)
    76 
    77 fun add_rule which th context = context |> Pack.map (fn Pack rules =>
    78   Pack (rules |> which (fn ths =>
    79     if member Thm.eq_thm_prop ths th then
    80       let
    81         val _ =
    82           (case context of
    83             Context.Proof ctxt =>
    84               if Context_Position.is_really_visible ctxt then
    85                 warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th)
    86               else ()
    87           | _ => ());
    88       in ths end
    89     else sort_rules (th :: ths))));
    90 
    91 val add_safe = Context.proof_map o add_rule apfst;
    92 val add_unsafe = Context.proof_map o add_rule apsnd;
    93 
    94 
    95 (* attributes *)
    96 
    97 val safe_add = Thm.declaration_attribute (add_rule apfst);
    98 val unsafe_add = Thm.declaration_attribute (add_rule apsnd);
    99 
   100 val _ = Theory.setup
   101   (Attrib.setup @{binding safe} (Scan.succeed safe_add) "" #>
   102    Attrib.setup @{binding unsafe} (Scan.succeed unsafe_add) "");
   103 
   104 
   105 (* proof method syntax *)
   106 
   107 fun method tac =
   108   Method.sections
   109    [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add \<^here>),
   110     Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add \<^here>)]
   111   >> K (SIMPLE_METHOD' o tac);
   112 
   113 
   114 (** tactics **)
   115 
   116 val trace = Attrib.setup_config_bool @{binding cla_trace} (K false);
   117 
   118 
   119 (*Returns the list of all formulas in the sequent*)
   120 fun forms_of_seq (Const(@{const_name "SeqO'"},_) $ P $ u) = P :: forms_of_seq u
   121   | forms_of_seq (H $ u) = forms_of_seq u
   122   | forms_of_seq _ = [];
   123 
   124 (*Tests whether two sequences (left or right sides) could be resolved.
   125   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
   126   Assumes each formula in seqc is surrounded by sequence variables
   127   -- checks that each concl formula looks like some subgoal formula.
   128   It SHOULD check order as well, using recursion rather than forall/exists*)
   129 fun could_res (seqp,seqc) =
   130       forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
   131                               (forms_of_seq seqp))
   132              (forms_of_seq seqc);
   133 
   134 (*Tests whether two sequents or pairs of sequents could be resolved*)
   135 fun could_resolve_seq (prem,conc) =
   136   case (prem,conc) of
   137       (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
   138        _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
   139           could_res (leftp,leftc) andalso could_res (rightp,rightc)
   140     | (_ $ Abs(_,_,leftp) $ rightp,
   141        _ $ Abs(_,_,leftc) $ rightc) =>
   142           could_res (leftp,leftc)  andalso  Term.could_unify (rightp,rightc)
   143     | _ => false;
   144 
   145 
   146 (*Like filt_resolve_tac, using could_resolve_seq
   147   Much faster than resolve_tac when there are many rules.
   148   Resolve subgoal i using the rules, unless more than maxr are compatible. *)
   149 fun filseq_resolve_tac ctxt rules maxr = SUBGOAL(fn (prem,i) =>
   150   let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
   151   in  if length rls > maxr  then  no_tac
   152           else (*((rtac derelict 1 THEN rtac impl 1
   153                  THEN (rtac identity 2 ORELSE rtac ll_mp 2)
   154                  THEN rtac context1 1)
   155                  ORELSE *) resolve_tac ctxt rls i
   156   end);
   157 
   158 
   159 (*Predicate: does the rule have n premises? *)
   160 fun has_prems n rule = (Thm.nprems_of rule = n);
   161 
   162 (*Continuation-style tactical for resolution.
   163   The list of rules is partitioned into 0, 1, 2 premises.
   164   The resulting tactic, gtac, tries to resolve with rules.
   165   If successful, it recursively applies nextac to the new subgoals only.
   166   Else fails.  (Treatment of goals due to Ph. de Groote)
   167   Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
   168 
   169 (*Takes rule lists separated in to 0, 1, 2, >2 premises.
   170   The abstraction over state prevents needless divergence in recursion.
   171   The 9999 should be a parameter, to delay treatment of flexible goals. *)
   172 
   173 fun RESOLVE_THEN ctxt rules =
   174   let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
   175       fun tac nextac i state = state |>
   176              (filseq_resolve_tac ctxt rls0 9999 i
   177               ORELSE
   178               (DETERM(filseq_resolve_tac ctxt rls1 9999 i) THEN  TRY(nextac i))
   179               ORELSE
   180               (DETERM(filseq_resolve_tac ctxt rls2 9999 i) THEN  TRY(nextac(i+1))
   181                                             THEN  TRY(nextac i)))
   182   in  tac  end;
   183 
   184 
   185 
   186 (*repeated resolution applied to the designated goal*)
   187 fun reresolve_tac ctxt rules =
   188   let
   189     val restac = RESOLVE_THEN ctxt rules;  (*preprocessing done now*)
   190     fun gtac i = restac gtac i;
   191   in gtac end;
   192 
   193 (*tries the safe rules repeatedly before the unsafe rules. *)
   194 fun repeat_goal_tac ctxt =
   195   let
   196     val (safes, unsafes) = get_rules ctxt;
   197     val restac = RESOLVE_THEN ctxt safes;
   198     val lastrestac = RESOLVE_THEN ctxt unsafes;
   199     fun gtac i =
   200       restac gtac i ORELSE
   201        (if Config.get ctxt trace then print_tac ctxt "" THEN lastrestac gtac i
   202         else lastrestac gtac i)
   203   in gtac end;
   204 
   205 
   206 (*Tries safe rules only*)
   207 fun safe_tac ctxt = reresolve_tac ctxt (#1 (get_rules ctxt));
   208 
   209 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
   210 fun step_tac ctxt =
   211   safe_tac ctxt ORELSE' filseq_resolve_tac ctxt (#2 (get_rules ctxt)) 9999;
   212 
   213 
   214 (* Tactic for reducing a goal, using Predicate Calculus rules.
   215    A decision procedure for Propositional Calculus, it is incomplete
   216    for Predicate-Calculus because of allL_thin and exR_thin.
   217    Fails if it can do nothing.      *)
   218 fun pc_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac ctxt 1));
   219 
   220 
   221 (*The following two tactics are analogous to those provided by
   222   Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
   223 fun fast_tac ctxt =
   224   SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
   225 
   226 fun best_tac ctxt  =
   227   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
   228 
   229 val _ = Theory.setup
   230   (Method.setup @{binding safe} (method safe_tac) "" #>
   231    Method.setup @{binding step} (method step_tac) "" #>
   232    Method.setup @{binding pc} (method pc_tac) "" #>
   233    Method.setup @{binding fast} (method fast_tac) "" #>
   234    Method.setup @{binding best} (method best_tac) "");
   235 
   236 end;
   237