1(*  Title:      Sequents/prover.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1992  University of Cambridge
4
5Simple classical reasoner for the sequent calculus, based on "theorem packs".
6*)
7
8signature CLA =
9sig
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
27end;
28
29structure Cla: CLA =
30struct
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
38fun less (rl1, rl2) = Thm.nprems_of rl1 < Thm.nprems_of rl2;
39val sort_rules = sort (make_ord less);
40
41datatype pack = Pack of thm list * thm list;
42
43val empty_pack = Pack ([], []);
44
45structure 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
56val put_pack = Context.proof_map o Pack.put;
57val get_pack = Pack.get o Context.Proof;
58fun get_rules ctxt = let val Pack rules = get_pack ctxt in rules end;
59
60
61(* print pack *)
62
63fun 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
70val _ =
71  Outer_Syntax.command \<^command_keyword>\<open>print_pack\<close> "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
77fun 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
91val add_safe = Context.proof_map o add_rule apfst;
92val add_unsafe = Context.proof_map o add_rule apsnd;
93
94
95(* attributes *)
96
97val safe_add = Thm.declaration_attribute (add_rule apfst);
98val unsafe_add = Thm.declaration_attribute (add_rule apsnd);
99
100val _ = Theory.setup
101  (Attrib.setup \<^binding>\<open>safe\<close> (Scan.succeed safe_add) "" #>
102   Attrib.setup \<^binding>\<open>unsafe\<close> (Scan.succeed unsafe_add) "");
103
104
105(* proof method syntax *)
106
107fun 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
116val trace = Attrib.setup_config_bool \<^binding>\<open>cla_trace\<close> (K false);
117
118
119(*Returns the list of all formulas in the sequent*)
120fun forms_of_seq (Const(\<^const_name>\<open>SeqO'\<close>,_) $ 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*)
129fun 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*)
135fun 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. *)
149fun 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? *)
160fun 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
173fun 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*)
187fun 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. *)
194fun 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*)
207fun 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. *)
210fun 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.      *)
218fun 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!*)
223fun fast_tac ctxt =
224  SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
225
226fun best_tac ctxt  =
227  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
228
229val _ = Theory.setup
230  (Method.setup \<^binding>\<open>safe\<close> (method safe_tac) "" #>
231   Method.setup \<^binding>\<open>step\<close> (method step_tac) "" #>
232   Method.setup \<^binding>\<open>pc\<close> (method pc_tac) "" #>
233   Method.setup \<^binding>\<open>fast\<close> (method fast_tac) "" #>
234   Method.setup \<^binding>\<open>best\<close> (method best_tac) "");
235
236end;
237
238