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