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