src/Provers/classical.ML
 author wenzelm Thu Oct 15 23:28:10 2009 +0200 (2009-10-15) changeset 32952 aeb1e44fbc19 parent 32863 5e8cef567042 child 32960 69916a850301 permissions -rw-r--r--
replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;
1 (*  Title:      Provers/classical.ML
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4 Theorem prover for classical reasoning, including predicate calculus, set
5 theory, etc.
7 Rules must be classified as intro, elim, safe, hazardous (unsafe).
9 A rule is unsafe unless it can be applied blindly without harmful results.
10 For a rule to be safe, its premises and conclusion should be logically
11 equivalent.  There should be no variables in the premises that are not in
12 the conclusion.
13 *)
15 (*higher precedence than := facilitates use of references*)
22 (*should be a type abbreviation in signature CLASSICAL*)
23 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
24 type wrapper = (int -> tactic) -> (int -> tactic);
26 signature CLASSICAL_DATA =
27 sig
28   val imp_elim  : thm           (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
29   val not_elim  : thm           (* ~P ==> P ==> R *)
30   val swap      : thm           (* ~ P ==> (~ R ==> P) ==> R *)
31   val classical : thm           (* (~ P ==> P) ==> P *)
32   val sizef     : thm -> int    (* size function for BEST_FIRST *)
33   val hyp_subst_tacs: (int -> tactic) list
34 end;
36 signature BASIC_CLASSICAL =
37 sig
38   type claset
39   val empty_cs: claset
40   val print_cs: claset -> unit
41   val rep_cs:
42     claset -> {safeIs: thm list, safeEs: thm list,
43                  hazIs: thm list, hazEs: thm list,
44                  swrappers: (string * wrapper) list,
45                  uwrappers: (string * wrapper) list,
46                  safe0_netpair: netpair, safep_netpair: netpair,
47                  haz_netpair: netpair, dup_netpair: netpair,
48                  xtra_netpair: ContextRules.netpair}
49   val merge_cs          : claset * claset -> claset
50   val addDs             : claset * thm list -> claset
51   val addEs             : claset * thm list -> claset
52   val addIs             : claset * thm list -> claset
53   val addSDs            : claset * thm list -> claset
54   val addSEs            : claset * thm list -> claset
55   val addSIs            : claset * thm list -> claset
56   val delrules          : claset * thm list -> claset
57   val addSWrapper       : claset * (string * wrapper) -> claset
58   val delSWrapper       : claset *  string            -> claset
59   val addWrapper        : claset * (string * wrapper) -> claset
60   val delWrapper        : claset *  string            -> claset
61   val addSbefore        : claset * (string * (int -> tactic)) -> claset
62   val addSafter         : claset * (string * (int -> tactic)) -> claset
63   val addbefore         : claset * (string * (int -> tactic)) -> claset
64   val addafter          : claset * (string * (int -> tactic)) -> claset
65   val addD2             : claset * (string * thm) -> claset
66   val addE2             : claset * (string * thm) -> claset
67   val addSD2            : claset * (string * thm) -> claset
68   val addSE2            : claset * (string * thm) -> claset
69   val appSWrappers      : claset -> wrapper
70   val appWrappers       : claset -> wrapper
72   val global_claset_of  : theory -> claset
73   val claset_of         : Proof.context -> claset
75   val fast_tac          : claset -> int -> tactic
76   val slow_tac          : claset -> int -> tactic
77   val weight_ASTAR      : int Unsynchronized.ref
78   val astar_tac         : claset -> int -> tactic
79   val slow_astar_tac    : claset -> int -> tactic
80   val best_tac          : claset -> int -> tactic
81   val first_best_tac    : claset -> int -> tactic
82   val slow_best_tac     : claset -> int -> tactic
83   val depth_tac         : claset -> int -> int -> tactic
84   val deepen_tac        : claset -> int -> int -> tactic
86   val contr_tac         : int -> tactic
87   val dup_elim          : thm -> thm
88   val dup_intr          : thm -> thm
89   val dup_step_tac      : claset -> int -> tactic
90   val eq_mp_tac         : int -> tactic
91   val haz_step_tac      : claset -> int -> tactic
92   val joinrules         : thm list * thm list -> (bool * thm) list
93   val mp_tac            : int -> tactic
94   val safe_tac          : claset -> tactic
95   val safe_steps_tac    : claset -> int -> tactic
96   val safe_step_tac     : claset -> int -> tactic
97   val clarify_tac       : claset -> int -> tactic
98   val clarify_step_tac  : claset -> int -> tactic
99   val step_tac          : claset -> int -> tactic
100   val slow_step_tac     : claset -> int -> tactic
101   val swapify           : thm list -> thm list
102   val swap_res_tac      : thm list -> int -> tactic
103   val inst_step_tac     : claset -> int -> tactic
104   val inst0_step_tac    : claset -> int -> tactic
105   val instp_step_tac    : claset -> int -> tactic
106 end;
108 signature CLASSICAL =
109 sig
110   include BASIC_CLASSICAL
111   val classical_rule: thm -> thm
112   val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
113   val del_context_safe_wrapper: string -> theory -> theory
114   val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
115   val del_context_unsafe_wrapper: string -> theory -> theory
116   val get_claset: Proof.context -> claset
117   val put_claset: claset -> Proof.context -> Proof.context
118   val get_cs: Context.generic -> claset
119   val map_cs: (claset -> claset) -> Context.generic -> Context.generic
120   val safe_dest: int option -> attribute
121   val safe_elim: int option -> attribute
122   val safe_intro: int option -> attribute
123   val haz_dest: int option -> attribute
124   val haz_elim: int option -> attribute
125   val haz_intro: int option -> attribute
126   val rule_del: attribute
127   val cla_modifiers: Method.modifier parser list
128   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
129   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
130   val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
131   val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
132   val setup: theory -> theory
133 end;
136 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
137 struct
139 local open Data in
141 (** classical elimination rules **)
143 (*
144 Classical reasoning requires stronger elimination rules.  For
145 instance, make_elim of Pure transforms the HOL rule injD into
147     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
149 Such rules can cause fast_tac to fail and blast_tac to report "PROOF
150 FAILED"; classical_rule will strenthen this to
152     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
153 *)
155 fun classical_rule rule =
156   if ObjectLogic.is_elim rule then
157     let
158       val rule' = rule RS classical;
159       val concl' = Thm.concl_of rule';
160       fun redundant_hyp goal =
161         concl' aconv Logic.strip_assums_concl goal orelse
162           (case Logic.strip_assums_hyp goal of
163             hyp :: hyps => exists (fn t => t aconv hyp) hyps
164           | _ => false);
165       val rule'' =
166         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
167           if i = 1 orelse redundant_hyp goal
168           then Tactic.etac thin_rl i
169           else all_tac))
170         |> Seq.hd
171         |> Drule.zero_var_indexes;
172     in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
173   else rule;
175 (*flatten nested meta connectives in prems*)
176 val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
179 (*** Useful tactics for classical reasoning ***)
181 (*Prove goal that assumes both P and ~P.
182   No backtracking if it finds an equal assumption.  Perhaps should call
183   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
184 val contr_tac = eresolve_tac [not_elim]  THEN'
185                 (eq_assume_tac ORELSE' assume_tac);
187 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
188   Could do the same thing for P<->Q and P... *)
189 fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i  THEN  assume_tac i;
191 (*Like mp_tac but instantiates no variables*)
192 fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i  THEN  eq_assume_tac i;
194 (*Creates rules to eliminate ~A, from rules to introduce A*)
195 fun swapify intrs = intrs RLN (2, [Data.swap]);
196 val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
198 (*Uses introduction rules in the normal way, or on negated assumptions,
199   trying rules in order. *)
200 fun swap_res_tac rls =
201     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
202     in  assume_tac      ORELSE'
203         contr_tac       ORELSE'
204         biresolve_tac (List.foldr addrl [] rls)
205     end;
207 (*Duplication of hazardous rules, for complete provers*)
208 fun dup_intr th = zero_var_indexes (th RS classical);
210 fun dup_elim th =
211     rule_by_tactic (TRYALL (etac revcut_rl))
212       ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
214 (**** Classical rule sets ****)
216 datatype claset =
217   CS of {safeIs         : thm list,                (*safe introduction rules*)
218          safeEs         : thm list,                (*safe elimination rules*)
219          hazIs          : thm list,                (*unsafe introduction rules*)
220          hazEs          : thm list,                (*unsafe elimination rules*)
221          swrappers      : (string * wrapper) list, (*for transforming safe_step_tac*)
222          uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
223          safe0_netpair  : netpair,                 (*nets for trivial cases*)
224          safep_netpair  : netpair,                 (*nets for >0 subgoals*)
225          haz_netpair    : netpair,                 (*nets for unsafe rules*)
226          dup_netpair    : netpair,                 (*nets for duplication*)
227          xtra_netpair   : ContextRules.netpair};   (*nets for extra rules*)
229 (*Desired invariants are
230         safe0_netpair = build safe0_brls,
231         safep_netpair = build safep_brls,
232         haz_netpair = build (joinrules(hazIs, hazEs)),
233         dup_netpair = build (joinrules(map dup_intr hazIs,
234                                        map dup_elim hazEs))
236 where build = build_netpair(Net.empty,Net.empty),
237       safe0_brls contains all brules that solve the subgoal, and
238       safep_brls contains all brules that generate 1 or more new subgoals.
239 The theorem lists are largely comments, though they are used in merge_cs and print_cs.
240 Nets must be built incrementally, to save space and time.
241 *)
243 val empty_netpair = (Net.empty, Net.empty);
245 val empty_cs =
246   CS{safeIs     = [],
247      safeEs     = [],
248      hazIs      = [],
249      hazEs      = [],
250      swrappers  = [],
251      uwrappers  = [],
252      safe0_netpair = empty_netpair,
253      safep_netpair = empty_netpair,
254      haz_netpair   = empty_netpair,
255      dup_netpair   = empty_netpair,
256      xtra_netpair  = empty_netpair};
258 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
259   let val pretty_thms = map Display.pretty_thm_without_context in
260     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
261       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
262       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
263       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
264       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
265       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
266     |> Pretty.chunks |> Pretty.writeln
267   end;
269 fun rep_cs (CS args) = args;
271 fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
272 fun appWrappers  (CS {uwrappers, ...}) = fold snd uwrappers;
275 (*** Adding (un)safe introduction or elimination rules.
277     In case of overlap, new rules are tried BEFORE old ones!!
278 ***)
280 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
281   assumptions.  Pairs elim rules with true. *)
282 fun joinrules (intrs, elims) =
283   (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs;
285 fun joinrules' (intrs, elims) =
286   map (pair true) elims @ map (pair false) intrs;
288 (*Priority: prefer rules with fewest subgoals,
289   then rules added most recently (preferring the head of the list).*)
290 fun tag_brls k [] = []
291   | tag_brls k (brl::brls) =
292       (1000000*subgoals_of_brl brl + k, brl) ::
293       tag_brls (k+1) brls;
295 fun tag_brls' _ _ [] = []
296   | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
298 fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls;
300 (*Insert into netpair that already has nI intr rules and nE elim rules.
301   Count the intr rules double (to account for swapify).  Negate to give the
302   new insertions the lowest priority.*)
303 fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
304 fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
306 fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
307 fun delete x = delete_tagged_list (joinrules x);
308 fun delete' x = delete_tagged_list (joinrules' x);
310 val mem_thm = member Thm.eq_thm_prop
311 and rem_thm = remove Thm.eq_thm_prop;
313 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
314   is still allowed.*)
315 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
316   if mem_thm safeIs th then
317     warning ("Rule already declared as safe introduction (intro!)\n" ^
318       Display.string_of_thm_without_context th)
319   else if mem_thm safeEs th then
320     warning ("Rule already declared as safe elimination (elim!)\n" ^
321       Display.string_of_thm_without_context th)
322   else if mem_thm hazIs th then
323     warning ("Rule already declared as introduction (intro)\n" ^
324       Display.string_of_thm_without_context th)
325   else if mem_thm hazEs th then
326     warning ("Rule already declared as elimination (elim)\n" ^
327       Display.string_of_thm_without_context th)
328   else ();
331 (*** Safe rules ***)
333 fun addSI w th
334   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
335              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
336   if mem_thm safeIs th then
337     (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
338       Display.string_of_thm_without_context th); cs)
339   else
340   let val th' = flat_rule th
341       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
342           List.partition Thm.no_prems [th']
343       val nI = length safeIs + 1
344       and nE = length safeEs
345   in warn_dup th cs;
346      CS{safeIs  = th::safeIs,
347         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
348         safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
349         safeEs  = safeEs,
350         hazIs   = hazIs,
351         hazEs   = hazEs,
352         swrappers    = swrappers,
353         uwrappers    = uwrappers,
354         haz_netpair  = haz_netpair,
355         dup_netpair  = dup_netpair,
356         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
357   end;
359 fun addSE w th
360   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
361              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
362   if mem_thm safeEs th then
363     (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
364         Display.string_of_thm_without_context th); cs)
365   else if has_fewer_prems 1 th then
366     	error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
367   else
368   let
369       val th' = classical_rule (flat_rule th)
370       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
371           List.partition (fn rl => nprems_of rl=1) [th']
372       val nI = length safeIs
373       and nE = length safeEs + 1
374   in warn_dup th cs;
375      CS{safeEs  = th::safeEs,
376         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
377         safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
378         safeIs  = safeIs,
379         hazIs   = hazIs,
380         hazEs   = hazEs,
381         swrappers    = swrappers,
382         uwrappers    = uwrappers,
383         haz_netpair  = haz_netpair,
384         dup_netpair  = dup_netpair,
385         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
386   end;
388 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
389 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
391 fun make_elim th =
392     if has_fewer_prems 1 th then
393     	  error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
394     else Tactic.make_elim th;
396 fun cs addSDs ths = cs addSEs (map make_elim ths);
399 (*** Hazardous (unsafe) rules ***)
401 fun addI w th
402   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
403              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
404   if mem_thm hazIs th then
405     (warning ("Ignoring duplicate introduction (intro)\n" ^
406         Display.string_of_thm_without_context th); cs)
407   else
408   let val th' = flat_rule th
409       val nI = length hazIs + 1
410       and nE = length hazEs
411   in warn_dup th cs;
412      CS{hazIs   = th::hazIs,
413         haz_netpair = insert (nI,nE) ([th'], []) haz_netpair,
414         dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair,
415         safeIs  = safeIs,
416         safeEs  = safeEs,
417         hazEs   = hazEs,
418         swrappers     = swrappers,
419         uwrappers     = uwrappers,
420         safe0_netpair = safe0_netpair,
421         safep_netpair = safep_netpair,
422         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
423   end
424   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
425     error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
427 fun addE w th
428   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
429             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
430   if mem_thm hazEs th then
431     (warning ("Ignoring duplicate elimination (elim)\n" ^
432         Display.string_of_thm_without_context th); cs)
433   else if has_fewer_prems 1 th then
434     	error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
435   else
436   let
437       val th' = classical_rule (flat_rule th)
438       val nI = length hazIs
439       and nE = length hazEs + 1
440   in warn_dup th cs;
441      CS{hazEs   = th::hazEs,
442         haz_netpair = insert (nI,nE) ([], [th']) haz_netpair,
443         dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair,
444         safeIs  = safeIs,
445         safeEs  = safeEs,
446         hazIs   = hazIs,
447         swrappers     = swrappers,
448         uwrappers     = uwrappers,
449         safe0_netpair = safe0_netpair,
450         safep_netpair = safep_netpair,
451         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
452   end;
454 fun cs addIs ths = fold_rev (addI NONE) ths cs;
455 fun cs addEs ths = fold_rev (addE NONE) ths cs;
457 fun cs addDs ths = cs addEs (map make_elim ths);
460 (*** Deletion of rules
461      Working out what to delete, requires repeating much of the code used
462         to insert.
463 ***)
465 fun delSI th
466           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
467                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
468  if mem_thm safeIs th then
469    let val th' = flat_rule th
470        val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']
471    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
472          safep_netpair = delete (safep_rls, []) safep_netpair,
473          safeIs = rem_thm th safeIs,
474          safeEs = safeEs,
475          hazIs  = hazIs,
476          hazEs  = hazEs,
477          swrappers    = swrappers,
478          uwrappers    = uwrappers,
479          haz_netpair  = haz_netpair,
480          dup_netpair  = dup_netpair,
481          xtra_netpair = delete' ([th], []) xtra_netpair}
482    end
483  else cs;
485 fun delSE th
486           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
487                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
488   if mem_thm safeEs th then
489     let
490       val th' = classical_rule (flat_rule th)
491       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
492     in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
493          safep_netpair = delete ([], safep_rls) safep_netpair,
494          safeIs = safeIs,
495          safeEs = rem_thm th safeEs,
496          hazIs  = hazIs,
497          hazEs  = hazEs,
498          swrappers    = swrappers,
499          uwrappers    = uwrappers,
500          haz_netpair  = haz_netpair,
501          dup_netpair  = dup_netpair,
502          xtra_netpair = delete' ([], [th]) xtra_netpair}
503     end
504   else cs;
507 fun delI th
508          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
509                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
510  if mem_thm hazIs th then
511     let val th' = flat_rule th
512     in CS{haz_netpair = delete ([th'], []) haz_netpair,
513         dup_netpair = delete ([dup_intr th'], []) dup_netpair,
514         safeIs  = safeIs,
515         safeEs  = safeEs,
516         hazIs   = rem_thm th hazIs,
517         hazEs   = hazEs,
518         swrappers     = swrappers,
519         uwrappers     = uwrappers,
520         safe0_netpair = safe0_netpair,
521         safep_netpair = safep_netpair,
522         xtra_netpair = delete' ([th], []) xtra_netpair}
523     end
524  else cs
525  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
526    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
529 fun delE th
530          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
531                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
532  if mem_thm hazEs th then
533    let val th' = classical_rule (flat_rule th)
534    in CS{haz_netpair = delete ([], [th']) haz_netpair,
535         dup_netpair = delete ([], [dup_elim th']) dup_netpair,
536         safeIs  = safeIs,
537         safeEs  = safeEs,
538         hazIs   = hazIs,
539         hazEs   = rem_thm th hazEs,
540         swrappers     = swrappers,
541         uwrappers     = uwrappers,
542         safe0_netpair = safe0_netpair,
543         safep_netpair = safep_netpair,
544         xtra_netpair = delete' ([], [th]) xtra_netpair}
545    end
546  else cs;
548 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
549 fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
550   let val th' = Tactic.make_elim th in
551     if mem_thm safeIs th orelse mem_thm safeEs th orelse
552       mem_thm hazIs th orelse mem_thm hazEs th orelse
553       mem_thm safeEs th' orelse mem_thm hazEs th'
554     then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
555     else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
556   end;
558 fun cs delrules ths = fold delrule ths cs;
561 (*** Modifying the wrapper tacticals ***)
562 fun map_swrappers f
563   (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
564     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
565   CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
566     swrappers = f swrappers, uwrappers = uwrappers,
567     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
568     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
570 fun map_uwrappers f
571   (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
572     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
573   CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
574     swrappers = swrappers, uwrappers = f uwrappers,
575     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
576     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
578 fun update_warn msg (p as (key : string, _)) xs =
579   (if AList.defined (op =) xs key then warning msg else ();
580     AList.update (op =) p xs);
582 fun delete_warn msg (key : string) xs =
583   if AList.defined (op =) xs key then AList.delete (op =) key xs
584     else (warning msg; xs);
586 (*Add/replace a safe wrapper*)
587 fun cs addSWrapper new_swrapper = map_swrappers
588   (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
590 (*Add/replace an unsafe wrapper*)
591 fun cs addWrapper new_uwrapper = map_uwrappers
592   (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
594 (*Remove a safe wrapper*)
595 fun cs delSWrapper name = map_swrappers
596   (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
598 (*Remove an unsafe wrapper*)
599 fun cs delWrapper name = map_uwrappers
600   (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
602 (* compose a safe tactic alternatively before/after safe_step_tac *)
603 fun cs addSbefore  (name,    tac1) =
604     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
605 fun cs addSafter   (name,    tac2) =
606     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
608 (*compose a tactic alternatively before/after the step tactic *)
609 fun cs addbefore   (name,    tac1) =
610     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
611 fun cs addafter    (name,    tac2) =
612     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
614 fun cs addD2     (name, thm) =
615     cs addafter  (name, datac thm 1);
616 fun cs addE2     (name, thm) =
617     cs addafter  (name, eatac thm 1);
618 fun cs addSD2    (name, thm) =
619     cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
620 fun cs addSE2    (name, thm) =
621     cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
623 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
624   Merging the term nets may look more efficient, but the rather delicate
625   treatment of priority might get muddled up.*)
626 fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
627     cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
628       swrappers, uwrappers, ...}) =
629   if pointer_eq (cs, cs') then cs
630   else
631     let
632       val safeIs' = fold rem_thm safeIs safeIs2;
633       val safeEs' = fold rem_thm safeEs safeEs2;
634       val hazIs' = fold rem_thm hazIs hazIs2;
635       val hazEs' = fold rem_thm hazEs hazEs2;
636       val cs1   = cs addSIs safeIs'
640       val cs2 = map_swrappers
641         (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
642       val cs3 = map_uwrappers
643         (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
644     in cs3 end;
647 (**** Simple tactics for theorem proving ****)
649 (*Attack subgoals using safe inferences -- matching, not resolution*)
650 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
651   appSWrappers cs (FIRST' [
652         eq_assume_tac,
653         eq_mp_tac,
654         bimatch_from_nets_tac safe0_netpair,
655         FIRST' hyp_subst_tacs,
656         bimatch_from_nets_tac safep_netpair]);
658 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
659 fun safe_steps_tac cs = REPEAT_DETERM1 o
660         (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
662 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
663 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
666 (*** Clarify_tac: do safe steps without causing branching ***)
668 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
670 (*version of bimatch_from_nets_tac that only applies rules that
671   create precisely n subgoals.*)
672 fun n_bimatch_from_nets_tac n =
673     biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true;
675 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
676 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
678 (*Two-way branching is allowed only if one of the branches immediately closes*)
679 fun bimatch2_tac netpair i =
680     n_bimatch_from_nets_tac 2 netpair i THEN
681     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
683 (*Attack subgoals using safe inferences -- matching, not resolution*)
684 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
685   appSWrappers cs (FIRST' [
686         eq_assume_contr_tac,
687         bimatch_from_nets_tac safe0_netpair,
688         FIRST' hyp_subst_tacs,
689         n_bimatch_from_nets_tac 1 safep_netpair,
690         bimatch2_tac safep_netpair]);
692 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
695 (*** Unsafe steps instantiate variables or lose information ***)
697 (*Backtracking is allowed among the various these unsafe ways of
698   proving a subgoal.  *)
699 fun inst0_step_tac (CS {safe0_netpair, ...}) =
700   assume_tac APPEND'
701   contr_tac APPEND'
702   biresolve_from_nets_tac safe0_netpair;
704 (*These unsafe steps could generate more subgoals.*)
705 fun instp_step_tac (CS {safep_netpair, ...}) =
706   biresolve_from_nets_tac safep_netpair;
708 (*These steps could instantiate variables and are therefore unsafe.*)
709 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
711 fun haz_step_tac (CS{haz_netpair,...}) =
712   biresolve_from_nets_tac haz_netpair;
714 (*Single step for the prover.  FAILS unless it makes progress. *)
715 fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
716         (inst_step_tac cs ORELSE' haz_step_tac cs) i;
718 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
719   allows backtracking from "safe" rules to "unsafe" rules here.*)
720 fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
721         (inst_step_tac cs APPEND' haz_step_tac cs) i;
723 (**** The following tactics all fail unless they solve one goal ****)
725 (*Dumb but fast*)
726 fun fast_tac cs =
727   ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
729 (*Slower but smarter than fast_tac*)
730 fun best_tac cs =
731   ObjectLogic.atomize_prems_tac THEN'
732   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
734 (*even a bit smarter than best_tac*)
735 fun first_best_tac cs =
736   ObjectLogic.atomize_prems_tac THEN'
737   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
739 fun slow_tac cs =
740   ObjectLogic.atomize_prems_tac THEN'
741   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
743 fun slow_best_tac cs =
744   ObjectLogic.atomize_prems_tac THEN'
745   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
748 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
749 val weight_ASTAR = Unsynchronized.ref 5;
751 fun astar_tac cs =
752   ObjectLogic.atomize_prems_tac THEN'
753   SELECT_GOAL
754     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
755       (step_tac cs 1));
757 fun slow_astar_tac cs =
758   ObjectLogic.atomize_prems_tac THEN'
759   SELECT_GOAL
760     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
761       (slow_step_tac cs 1));
763 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
764   of much experimentation!  Changing APPEND to ORELSE below would prove
765   easy theorems faster, but loses completeness -- and many of the harder
766   theorems such as 43. ****)
768 (*Non-deterministic!  Could always expand the first unsafe connective.
769   That's hard to implement and did not perform better in experiments, due to
770   greater search depth required.*)
771 fun dup_step_tac (CS {dup_netpair, ...}) =
772   biresolve_from_nets_tac dup_netpair;
774 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
775 local
776 fun slow_step_tac' cs = appWrappers cs
777         (instp_step_tac cs APPEND' dup_step_tac cs);
778 in fun depth_tac cs m i state = SELECT_GOAL
779    (safe_steps_tac cs 1 THEN_ELSE
780         (DEPTH_SOLVE (depth_tac cs m 1),
781          inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
782                 (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
783         )) i state;
784 end;
786 (*Search, with depth bound m.
787   This is the "entry point", which does safe inferences first.*)
788 fun safe_depth_tac cs m =
789   SUBGOAL
790     (fn (prem,i) =>
791       let val deti =
792           (*No Vars in the goal?  No need to backtrack between goals.*)
793           if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
794       in  SELECT_GOAL (TRY (safe_tac cs) THEN
795                        DEPTH_SOLVE (deti (depth_tac cs m 1))) i
796       end);
798 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
802 (** context dependent claset components **)
804 datatype context_cs = ContextCS of
805  {swrappers: (string * (Proof.context -> wrapper)) list,
806   uwrappers: (string * (Proof.context -> wrapper)) list};
808 fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
809   let
810     fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
811   in
812     cs
813     |> fold_rev (add_wrapper (op addSWrapper)) swrappers
814     |> fold_rev (add_wrapper (op addWrapper)) uwrappers
815   end;
817 fun make_context_cs (swrappers, uwrappers) =
818   ContextCS {swrappers = swrappers, uwrappers = uwrappers};
820 val empty_context_cs = make_context_cs ([], []);
822 fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
823   if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
824   else
825     let
826       val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
827       val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
828       val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
829       val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
830     in make_context_cs (swrappers', uwrappers') end;
834 (** claset data **)
836 (* global clasets *)
838 structure GlobalClaset = TheoryDataFun
839 (
840   type T = claset * context_cs;
841   val empty = (empty_cs, empty_context_cs);
842   val copy = I;
843   val extend = I;
844   fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
845     (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
846 );
848 val get_global_claset = #1 o GlobalClaset.get;
849 val map_global_claset = GlobalClaset.map o apfst;
851 val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
852 fun map_context_cs f = GlobalClaset.map (apsnd
853   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
855 fun global_claset_of thy =
856   let val (cs, ctxt_cs) = GlobalClaset.get thy
857   in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
860 (* context dependent components *)
862 fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
863 fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
865 fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
866 fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
869 (* local clasets *)
871 structure LocalClaset = ProofDataFun
872 (
873   type T = claset;
874   val init = get_global_claset;
875 );
877 val get_claset = LocalClaset.get;
878 val put_claset = LocalClaset.put;
880 fun claset_of ctxt =
881   context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
884 (* generic clasets *)
886 val get_cs = Context.cases global_claset_of claset_of;
887 fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
890 (* attributes *)
892 fun attrib f = Thm.declaration_attribute (fn th =>
893   Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
895 fun safe_dest w = attrib (addSE w o make_elim);
896 val safe_elim = attrib o addSE;
897 val safe_intro = attrib o addSI;
898 fun haz_dest w = attrib (addE w o make_elim);
899 val haz_elim = attrib o addE;
900 val haz_intro = attrib o addI;
901 val rule_del = attrib delrule o ContextRules.rule_del;
904 end;
908 (** concrete syntax of attributes **)
910 val introN = "intro";
911 val elimN = "elim";
912 val destN = "dest";
914 val setup_attrs =
915   Attrib.setup @{binding swapped} (Scan.succeed swapped)
916     "classical swap of introduction rule" #>
917   Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
918     "declaration of Classical destruction rule" #>
919   Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
920     "declaration of Classical elimination rule" #>
921   Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
922     "declaration of Classical introduction rule" #>
923   Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
924     "remove declaration of intro/elim/dest rule";
928 (** proof methods **)
930 local
932 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
933   let
934     val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
935     val CS {xtra_netpair, ...} = claset_of ctxt;
936     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
937     val rules = rules1 @ rules2 @ rules3 @ rules4;
938     val ruleq = Drule.multi_resolves facts rules;
939   in
940     Method.trace ctxt rules;
941     fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
942   end)
943   THEN_ALL_NEW Goal.norm_hhf_tac;
945 in
947 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
948   | rule_tac _ rules facts = Method.rule_tac rules facts;
950 fun default_tac ctxt rules facts =
951   HEADGOAL (rule_tac ctxt rules facts) ORELSE
952   Class.default_intro_tac ctxt facts;
954 end;
957 (* contradiction method *)
959 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
962 (* automatic methods *)
964 val cla_modifiers =
965  [Args.\$\$\$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
966   Args.\$\$\$ destN -- Args.colon >> K (I, haz_dest NONE),
967   Args.\$\$\$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
968   Args.\$\$\$ elimN -- Args.colon >> K (I, haz_elim NONE),
969   Args.\$\$\$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
970   Args.\$\$\$ introN -- Args.colon >> K (I, haz_intro NONE),
971   Args.del -- Args.colon >> K (I, rule_del)];
973 fun cla_meth tac prems ctxt = METHOD (fn facts =>
974   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
976 fun cla_meth' tac prems ctxt = METHOD (fn facts =>
977   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
979 fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
980 fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
984 (** setup_methods **)
986 val setup_methods =
987   Method.setup @{binding default}
988    (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
989     "apply some intro/elim rule (potentially classical)" #>
990   Method.setup @{binding rule}
991     (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
992     "apply some intro/elim rule (potentially classical)" #>
993   Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
994     "proof by contradiction" #>
995   Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
996     "repeatedly apply safe steps" #>
997   Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
998   Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
999   Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
1000   Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
1001     "classical prover (iterative deepening)" #>
1002   Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
1003     "classical prover (apply safe rules)";
1007 (** theory setup **)
1009 val setup = setup_attrs #> setup_methods;
1013 (** outer syntax **)
1015 val _ =
1016   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
1017     OuterKeyword.diag
1018     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
1019       Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
1021 end;