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