src/Provers/classical.ML
author wenzelm
Wed Dec 05 03:12:52 2001 +0100 (2001-12-05 ago)
changeset 12376 480303e3fa08
parent 12362 57cd572103c4
child 12401 4363432ef0cd
permissions -rw-r--r--
simplified (and clarified) integration with Pure/ContextRules;
removed "extra" rules as separate slots, only keep xtra_netpair for
single-step view of plain haz/safe rules;
     1 (*  Title:      Provers/classical.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Theorem prover for classical reasoning, including predicate calculus, set
     7 theory, etc.
     8 
     9 Rules must be classified as intro, elim, safe, hazardous (unsafe).
    10 
    11 A rule is unsafe unless it can be applied blindly without harmful results.
    12 For a rule to be safe, its premises and conclusion should be logically
    13 equivalent.  There should be no variables in the premises that are not in
    14 the conclusion.
    15 *)
    16 
    17 (*higher precedence than := facilitates use of references*)
    18 infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
    19   addSWrapper delSWrapper addWrapper delWrapper
    20   addSbefore addSafter addbefore addafter
    21   addD2 addE2 addSD2 addSE2;
    22 
    23 
    24 (*should be a type abbreviation in signature CLASSICAL*)
    25 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    26 type wrapper = (int -> tactic) -> (int -> tactic);
    27 
    28 signature CLASSICAL_DATA =
    29 sig
    30   val make_elim : thm -> thm    (* Tactic.make_elim or a classical version*)
    31   val mp        : thm           (* [| P-->Q;  P |] ==> Q *)
    32   val not_elim  : thm           (* [| ~P;  P |] ==> R *)
    33   val classical : thm           (* (~P ==> P) ==> P *)
    34   val sizef     : thm -> int    (* size function for BEST_FIRST *)
    35   val hyp_subst_tacs: (int -> tactic) list
    36 end;
    37 
    38 signature BASIC_CLASSICAL =
    39 sig
    40   type claset
    41   val empty_cs: claset
    42   val print_cs: claset -> unit
    43   val print_claset: theory -> unit
    44   val rep_cs: (* BLAST_DATA in blast.ML dependent on this *)
    45     claset -> {safeIs: thm list, safeEs: thm list,
    46                  hazIs: thm list, hazEs: thm list,
    47                  swrappers: (string * wrapper) list,
    48                  uwrappers: (string * wrapper) list,
    49                  safe0_netpair: netpair, safep_netpair: netpair,
    50                  haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
    51   val merge_cs          : claset * claset -> claset
    52   val addDs             : claset * thm list -> claset
    53   val addEs             : claset * thm list -> claset
    54   val addIs             : claset * thm list -> claset
    55   val addSDs            : claset * thm list -> claset
    56   val addSEs            : claset * thm list -> claset
    57   val addSIs            : claset * thm list -> claset
    58   val delrules          : claset * thm list -> claset
    59   val addSWrapper       : claset * (string * wrapper) -> claset
    60   val delSWrapper       : claset *  string            -> claset
    61   val addWrapper        : claset * (string * wrapper) -> claset
    62   val delWrapper        : claset *  string            -> claset
    63   val addSbefore        : claset * (string * (int -> tactic)) -> claset
    64   val addSafter         : claset * (string * (int -> tactic)) -> claset
    65   val addbefore         : claset * (string * (int -> tactic)) -> claset
    66   val addafter          : claset * (string * (int -> tactic)) -> claset
    67   val addD2             : claset * (string * thm) -> claset
    68   val addE2             : claset * (string * thm) -> claset
    69   val addSD2            : claset * (string * thm) -> claset
    70   val addSE2            : claset * (string * thm) -> claset
    71   val appSWrappers      : claset -> wrapper
    72   val appWrappers       : claset -> wrapper
    73 
    74   val claset_ref_of_sg: Sign.sg -> claset ref
    75   val claset_ref_of: theory -> claset ref
    76   val claset_of_sg: Sign.sg -> claset
    77   val claset_of: theory -> claset
    78   val CLASET: (claset -> tactic) -> tactic
    79   val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
    80   val claset: unit -> claset
    81   val claset_ref: unit -> claset ref
    82 
    83   val fast_tac          : claset -> int -> tactic
    84   val slow_tac          : claset -> int -> tactic
    85   val weight_ASTAR      : int ref
    86   val astar_tac         : claset -> int -> tactic
    87   val slow_astar_tac    : claset -> int -> tactic
    88   val best_tac          : claset -> int -> tactic
    89   val first_best_tac    : claset -> int -> tactic
    90   val slow_best_tac     : claset -> int -> tactic
    91   val depth_tac         : claset -> int -> int -> tactic
    92   val deepen_tac        : claset -> int -> int -> tactic
    93 
    94   val contr_tac         : int -> tactic
    95   val dup_elim          : thm -> thm
    96   val dup_intr          : thm -> thm
    97   val dup_step_tac      : claset -> int -> tactic
    98   val eq_mp_tac         : int -> tactic
    99   val haz_step_tac      : claset -> int -> tactic
   100   val joinrules         : thm list * thm list -> (bool * thm) list
   101   val mp_tac            : int -> tactic
   102   val safe_tac          : claset -> tactic
   103   val safe_steps_tac    : claset -> int -> tactic
   104   val safe_step_tac     : claset -> int -> tactic
   105   val clarify_tac       : claset -> int -> tactic
   106   val clarify_step_tac  : claset -> int -> tactic
   107   val step_tac          : claset -> int -> tactic
   108   val slow_step_tac     : claset -> int -> tactic
   109   val swap              : thm                 (* ~P ==> (~Q ==> P) ==> Q *)
   110   val swapify           : thm list -> thm list
   111   val swap_res_tac      : thm list -> int -> tactic
   112   val inst_step_tac     : claset -> int -> tactic
   113   val inst0_step_tac    : claset -> int -> tactic
   114   val instp_step_tac    : claset -> int -> tactic
   115 
   116   val AddDs             : thm list -> unit
   117   val AddEs             : thm list -> unit
   118   val AddIs             : thm list -> unit
   119   val AddSDs            : thm list -> unit
   120   val AddSEs            : thm list -> unit
   121   val AddSIs            : thm list -> unit
   122   val Delrules          : thm list -> unit
   123   val Safe_tac          : tactic
   124   val Safe_step_tac     : int -> tactic
   125   val Clarify_tac       : int -> tactic
   126   val Clarify_step_tac  : int -> tactic
   127   val Step_tac          : int -> tactic
   128   val Fast_tac          : int -> tactic
   129   val Best_tac          : int -> tactic
   130   val Slow_tac          : int -> tactic
   131   val Slow_best_tac     : int -> tactic
   132   val Deepen_tac        : int -> int -> tactic
   133 end;
   134 
   135 signature CLASSICAL =
   136 sig
   137   include BASIC_CLASSICAL
   138   val print_local_claset: Proof.context -> unit
   139   val get_local_claset: Proof.context -> claset
   140   val put_local_claset: claset -> Proof.context -> Proof.context
   141   val safe_dest_global: theory attribute
   142   val safe_elim_global: theory attribute
   143   val safe_intro_global: theory attribute
   144   val haz_dest_global: theory attribute
   145   val haz_elim_global: theory attribute
   146   val haz_intro_global: theory attribute
   147   val rule_del_global: theory attribute
   148   val safe_dest_local: Proof.context attribute
   149   val safe_elim_local: Proof.context attribute
   150   val safe_intro_local: Proof.context attribute
   151   val haz_dest_local: Proof.context attribute
   152   val haz_elim_local: Proof.context attribute
   153   val haz_intro_local: Proof.context attribute
   154   val rule_del_local: Proof.context attribute
   155   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   156   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   157   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   158   val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
   159   val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   160   val setup: (theory -> theory) list
   161 end;
   162 
   163 
   164 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
   165 struct
   166 
   167 local open Data in
   168 
   169 (*** Useful tactics for classical reasoning ***)
   170 
   171 val imp_elim = (*cannot use bind_thm within a structure!*)
   172   store_thm ("imp_elim", Data.make_elim mp);
   173 
   174 (*Prove goal that assumes both P and ~P.
   175   No backtracking if it finds an equal assumption.  Perhaps should call
   176   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
   177 val contr_tac = eresolve_tac [not_elim]  THEN'
   178                 (eq_assume_tac ORELSE' assume_tac);
   179 
   180 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   181   Could do the same thing for P<->Q and P... *)
   182 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   183 
   184 (*Like mp_tac but instantiates no variables*)
   185 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   186 
   187 val swap =
   188   store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));
   189 
   190 (*Creates rules to eliminate ~A, from rules to introduce A*)
   191 fun swapify intrs = intrs RLN (2, [swap]);
   192 
   193 (*Uses introduction rules in the normal way, or on negated assumptions,
   194   trying rules in order. *)
   195 fun swap_res_tac rls =
   196     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   197     in  assume_tac      ORELSE'
   198         contr_tac       ORELSE'
   199         biresolve_tac (foldr addrl (rls,[]))
   200     end;
   201 
   202 (*Duplication of hazardous rules, for complete provers*)
   203 fun dup_intr th = zero_var_indexes (th RS classical);
   204 
   205 fun dup_elim th =
   206   (case try
   207       (rule_by_tactic (TRYALL (etac revcut_rl)))
   208       (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd) of
   209     Some th' => th'
   210   | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
   211 
   212 
   213 (**** Classical rule sets ****)
   214 
   215 datatype claset =
   216   CS of {safeIs         : thm list,             (*safe introduction rules*)
   217          safeEs         : thm list,             (*safe elimination rules*)
   218          hazIs          : thm list,             (*unsafe introduction rules*)
   219          hazEs          : thm list,             (*unsafe elimination rules*)
   220          swrappers      : (string * wrapper) list, (*for transf. safe_step_tac*)
   221          uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
   222          safe0_netpair  : netpair,              (*nets for trivial cases*)
   223          safep_netpair  : netpair,              (*nets for >0 subgoals*)
   224          haz_netpair    : netpair,              (*nets for unsafe rules*)
   225          dup_netpair    : netpair,              (*nets for duplication*)
   226          xtra_netpair   : netpair};             (*nets for extra rules*)
   227 
   228 (*Desired invariants are
   229         safe0_netpair = build safe0_brls,
   230         safep_netpair = build safep_brls,
   231         haz_netpair = build (joinrules(hazIs, hazEs)),
   232         dup_netpair = build (joinrules(map dup_intr hazIs,
   233                                        map dup_elim hazEs))
   234 
   235 where build = build_netpair(Net.empty,Net.empty),
   236       safe0_brls contains all brules that solve the subgoal, and
   237       safep_brls contains all brules that generate 1 or more new subgoals.
   238 The theorem lists are largely comments, though they are used in merge_cs and print_cs.
   239 Nets must be built incrementally, to save space and time.
   240 *)
   241 
   242 val empty_netpair = (Net.empty, Net.empty);
   243 
   244 val empty_cs =
   245   CS{safeIs     = [],
   246      safeEs     = [],
   247      hazIs      = [],
   248      hazEs      = [],
   249      swrappers  = [],
   250      uwrappers  = [],
   251      safe0_netpair = empty_netpair,
   252      safep_netpair = empty_netpair,
   253      haz_netpair   = empty_netpair,
   254      dup_netpair   = empty_netpair,
   255      xtra_netpair  = empty_netpair};
   256 
   257 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   258   let val pretty_thms = map Display.pretty_thm in
   259     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   260       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   261       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   262       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs)]
   263     |> Pretty.chunks |> Pretty.writeln
   264   end;
   265 
   266 fun rep_cs (CS args) = args;
   267 
   268 local
   269   fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac);
   270 in
   271   fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
   272   fun appWrappers  (CS{uwrappers,...}) = wrap uwrappers;
   273 end;
   274 
   275 
   276 (*** Adding (un)safe introduction or elimination rules.
   277 
   278     In case of overlap, new rules are tried BEFORE old ones!!
   279 ***)
   280 
   281 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   282   assumptions.  Pairs elim rules with true. *)
   283 fun joinrules (intrs, elims) =
   284   (map (pair true) (elims @ swapify intrs) @ map (pair false) intrs);
   285 
   286 fun joinrules_simple (intrs, elims) =
   287   (map (pair true) elims @ map (pair false) intrs);
   288 
   289 (*Priority: prefer rules with fewest subgoals,
   290   then rules added most recently (preferring the head of the list).*)
   291 fun tag_brls k [] = []
   292   | tag_brls k (brl::brls) =
   293       (1000000*subgoals_of_brl brl + k, brl) ::
   294       tag_brls (k+1) brls;
   295 
   296 fun tag_brls_simple k [] = []
   297   | tag_brls_simple k (brl::brls) = (k, brl) :: tag_brls_simple (k+1) brls;
   298 
   299 fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl (kbrls, netpr);
   300 
   301 (*Insert into netpair that already has nI intr rules and nE elim rules.
   302   Count the intr rules double (to account for swapify).  Negate to give the
   303   new insertions the lowest priority.*)
   304 fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   305 fun insert_simple (nI, nE) = insert_tagged_list o tag_brls_simple (~(nI + nE)) o joinrules_simple;
   306 
   307 fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl (brls, netpr);
   308 fun delete x = delete_tagged_list (joinrules x);
   309 fun delete_simple x = delete_tagged_list (joinrules_simple x);
   310 
   311 val mem_thm = gen_mem eq_thm
   312 and rem_thm = gen_rem eq_thm;
   313 
   314 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   315   is still allowed.*)
   316 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   317        if mem_thm (th, safeIs) then
   318          warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
   319   else if mem_thm (th, safeEs) then
   320          warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   321   else if mem_thm (th, hazIs) then
   322          warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
   323   else if mem_thm (th, hazEs) then
   324          warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
   325   else ();
   326 
   327 
   328 (*** Safe rules ***)
   329 
   330 fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   331               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   332            th)  =
   333   if mem_thm (th, safeIs) then
   334          (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
   335           cs)
   336   else
   337   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   338           partition Thm.no_prems [th]
   339       val nI = length safeIs + 1
   340       and nE = length safeEs
   341   in warn_dup th cs;
   342      CS{safeIs  = th::safeIs,
   343         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   344         safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   345         safeEs  = safeEs,
   346         hazIs   = hazIs,
   347         hazEs   = hazEs,
   348         swrappers    = swrappers,
   349         uwrappers    = uwrappers,
   350         haz_netpair  = haz_netpair,
   351         dup_netpair  = dup_netpair,
   352         xtra_netpair = insert_simple (nI,nE) ([th], []) xtra_netpair}
   353   end;
   354 
   355 fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   356                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   357            th)  =
   358   if mem_thm (th, safeEs) then
   359          (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
   360           cs)
   361   else
   362   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   363           partition (fn rl => nprems_of rl=1) [th]
   364       val nI = length safeIs
   365       and nE = length safeEs + 1
   366   in warn_dup th cs;
   367      CS{safeEs  = th::safeEs,
   368         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   369         safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   370         safeIs  = safeIs,
   371         hazIs   = hazIs,
   372         hazEs   = hazEs,
   373         swrappers    = swrappers,
   374         uwrappers    = uwrappers,
   375         haz_netpair  = haz_netpair,
   376         dup_netpair  = dup_netpair,
   377         xtra_netpair = insert_simple (nI,nE) ([], [th]) xtra_netpair}
   378   end;
   379 
   380 fun rev_foldl f (e, l) = foldl f (e, rev l);
   381 
   382 val op addSIs = rev_foldl addSI;
   383 val op addSEs = rev_foldl addSE;
   384 
   385 fun cs addSDs ths = cs addSEs (map Data.make_elim ths);
   386 
   387 
   388 (*** Hazardous (unsafe) rules ***)
   389 
   390 fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   391                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   392           th)=
   393   if mem_thm (th, hazIs) then
   394          (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   395           cs)
   396   else
   397   let val nI = length hazIs + 1
   398       and nE = length hazEs
   399   in warn_dup th cs;
   400      CS{hazIs   = th::hazIs,
   401         haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   402         dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   403         safeIs  = safeIs,
   404         safeEs  = safeEs,
   405         hazEs   = hazEs,
   406         swrappers     = swrappers,
   407         uwrappers     = uwrappers,
   408         safe0_netpair = safe0_netpair,
   409         safep_netpair = safep_netpair,
   410         xtra_netpair = insert_simple (nI,nE) ([th], []) xtra_netpair}
   411   end;
   412 
   413 fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   414                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   415           th) =
   416   if mem_thm (th, hazEs) then
   417          (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   418           cs)
   419   else
   420   let val nI = length hazIs
   421       and nE = length hazEs + 1
   422   in warn_dup th cs;
   423      CS{hazEs   = th::hazEs,
   424         haz_netpair = insert (nI,nE) ([], [th]) haz_netpair,
   425         dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair,
   426         safeIs  = safeIs,
   427         safeEs  = safeEs,
   428         hazIs   = hazIs,
   429         swrappers     = swrappers,
   430         uwrappers     = uwrappers,
   431         safe0_netpair = safe0_netpair,
   432         safep_netpair = safep_netpair,
   433         xtra_netpair = insert_simple (nI,nE) ([], [th]) xtra_netpair}
   434   end;
   435 
   436 val op addIs = rev_foldl addI;
   437 val op addEs = rev_foldl addE;
   438 
   439 fun cs addDs ths = cs addEs (map Data.make_elim ths);
   440 
   441 
   442 (*** Deletion of rules
   443      Working out what to delete, requires repeating much of the code used
   444         to insert.
   445      Separate functions delSI, etc., are not exported; instead delrules
   446         searches in all the lists and chooses the relevant delXX functions.
   447 ***)
   448 
   449 fun delSI th
   450           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   451                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   452  if mem_thm (th, safeIs) then
   453    let val (safe0_rls, safep_rls) = partition Thm.no_prems [th]
   454    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   455          safep_netpair = delete (safep_rls, []) safep_netpair,
   456          safeIs = rem_thm (safeIs,th),
   457          safeEs = safeEs,
   458          hazIs  = hazIs,
   459          hazEs  = hazEs,
   460          swrappers    = swrappers,
   461          uwrappers    = uwrappers,
   462          haz_netpair  = haz_netpair,
   463          dup_netpair  = dup_netpair,
   464          xtra_netpair = delete_simple ([th], []) xtra_netpair}
   465    end
   466  else cs;
   467 
   468 fun delSE th
   469           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   470                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   471  if mem_thm (th, safeEs) then
   472    let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
   473    in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   474          safep_netpair = delete ([], safep_rls) safep_netpair,
   475          safeIs = safeIs,
   476          safeEs = rem_thm (safeEs,th),
   477          hazIs  = hazIs,
   478          hazEs  = hazEs,
   479          swrappers    = swrappers,
   480          uwrappers    = uwrappers,
   481          haz_netpair  = haz_netpair,
   482          dup_netpair  = dup_netpair,
   483          xtra_netpair = delete_simple ([], [th]) xtra_netpair}
   484    end
   485  else cs;
   486 
   487 
   488 fun delI th
   489          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   490                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   491  if mem_thm (th, hazIs) then
   492      CS{haz_netpair = delete ([th], []) haz_netpair,
   493         dup_netpair = delete ([dup_intr th], []) dup_netpair,
   494         safeIs  = safeIs,
   495         safeEs  = safeEs,
   496         hazIs   = rem_thm (hazIs,th),
   497         hazEs   = hazEs,
   498         swrappers     = swrappers,
   499         uwrappers     = uwrappers,
   500         safe0_netpair = safe0_netpair,
   501         safep_netpair = safep_netpair,
   502         xtra_netpair = delete_simple ([th], []) xtra_netpair}
   503  else cs;
   504 
   505 fun delE th
   506          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   507                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   508  if mem_thm (th, hazEs) then
   509      CS{haz_netpair = delete ([], [th]) haz_netpair,
   510         dup_netpair = delete ([], [dup_elim th]) dup_netpair,
   511         safeIs  = safeIs,
   512         safeEs  = safeEs,
   513         hazIs   = hazIs,
   514         hazEs   = rem_thm (hazEs,th),
   515         swrappers     = swrappers,
   516         uwrappers     = uwrappers,
   517         safe0_netpair = safe0_netpair,
   518         safep_netpair = safep_netpair,
   519         xtra_netpair = delete_simple ([], [th]) xtra_netpair}
   520  else cs;
   521 
   522 
   523 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   524 fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) =
   525   let val th' = Data.make_elim th in
   526     if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
   527       mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) orelse
   528       mem_thm (th', safeEs) orelse mem_thm (th', hazEs)
   529     then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   530     else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs)
   531   end;
   532 
   533 val op delrules = foldl delrule;
   534 
   535 
   536 (*** Modifying the wrapper tacticals ***)
   537 fun update_swrappers
   538 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   539     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   540  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   541     swrappers = f swrappers, uwrappers = uwrappers,
   542     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   543     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   544 
   545 fun update_uwrappers
   546 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   547     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   548  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   549     swrappers = swrappers, uwrappers = f uwrappers,
   550     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   551     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   552 
   553 
   554 (*Add/replace a safe wrapper*)
   555 fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
   556     overwrite_warn (swrappers, new_swrapper)
   557        ("Overwriting safe wrapper " ^ fst new_swrapper));
   558 
   559 (*Add/replace an unsafe wrapper*)
   560 fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
   561     overwrite_warn (uwrappers, new_uwrapper)
   562         ("Overwriting unsafe wrapper "^fst new_uwrapper));
   563 
   564 (*Remove a safe wrapper*)
   565 fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
   566     let val (del,rest) = partition (fn (n,_) => n=name) swrappers
   567     in if null del then (warning ("No such safe wrapper in claset: "^ name);
   568                          swrappers) else rest end);
   569 
   570 (*Remove an unsafe wrapper*)
   571 fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
   572     let val (del,rest) = partition (fn (n,_) => n=name) uwrappers
   573     in if null del then (warning ("No such unsafe wrapper in claset: " ^ name);
   574                          uwrappers) else rest end);
   575 
   576 (* compose a safe tactic alternatively before/after safe_step_tac *)
   577 fun cs addSbefore  (name,    tac1) =
   578     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   579 fun cs addSafter   (name,    tac2) =
   580     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   581 
   582 (*compose a tactic alternatively before/after the step tactic *)
   583 fun cs addbefore   (name,    tac1) =
   584     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
   585 fun cs addafter    (name,    tac2) =
   586     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
   587 
   588 fun cs addD2     (name, thm) =
   589     cs addafter  (name, datac thm 1);
   590 fun cs addE2     (name, thm) =
   591     cs addafter  (name, eatac thm 1);
   592 fun cs addSD2    (name, thm) =
   593     cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   594 fun cs addSE2    (name, thm) =
   595     cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   596 
   597 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   598   Merging the term nets may look more efficient, but the rather delicate
   599   treatment of priority might get muddled up.*)
   600 fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
   601      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
   602   let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
   603       val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
   604       val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
   605       val  hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
   606       val cs1   = cs addSIs safeIs'
   607                      addSEs safeEs'
   608                      addIs  hazIs'
   609                      addEs  hazEs'
   610       val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers);
   611       val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers);
   612   in cs3
   613   end;
   614 
   615 
   616 (**** Simple tactics for theorem proving ****)
   617 
   618 (*Attack subgoals using safe inferences -- matching, not resolution*)
   619 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   620   appSWrappers cs (FIRST' [
   621         eq_assume_tac,
   622         eq_mp_tac,
   623         bimatch_from_nets_tac safe0_netpair,
   624         FIRST' hyp_subst_tacs,
   625         bimatch_from_nets_tac safep_netpair]);
   626 
   627 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   628 fun safe_steps_tac cs = REPEAT_DETERM1 o
   629         (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   630 
   631 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   632 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   633 
   634 
   635 (*** Clarify_tac: do safe steps without causing branching ***)
   636 
   637 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   638 
   639 (*version of bimatch_from_nets_tac that only applies rules that
   640   create precisely n subgoals.*)
   641 fun n_bimatch_from_nets_tac n =
   642     biresolution_from_nets_tac (Tactic.orderlist o filter (nsubgoalsP n)) true;
   643 
   644 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   645 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   646 
   647 (*Two-way branching is allowed only if one of the branches immediately closes*)
   648 fun bimatch2_tac netpair i =
   649     n_bimatch_from_nets_tac 2 netpair i THEN
   650     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   651 
   652 (*Attack subgoals using safe inferences -- matching, not resolution*)
   653 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   654   appSWrappers cs (FIRST' [
   655         eq_assume_contr_tac,
   656         bimatch_from_nets_tac safe0_netpair,
   657         FIRST' hyp_subst_tacs,
   658         n_bimatch_from_nets_tac 1 safep_netpair,
   659         bimatch2_tac safep_netpair]);
   660 
   661 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   662 
   663 
   664 (*** Unsafe steps instantiate variables or lose information ***)
   665 
   666 (*Backtracking is allowed among the various these unsafe ways of
   667   proving a subgoal.  *)
   668 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   669   assume_tac                      APPEND'
   670   contr_tac                       APPEND'
   671   biresolve_from_nets_tac safe0_netpair;
   672 
   673 (*These unsafe steps could generate more subgoals.*)
   674 fun instp_step_tac (CS{safep_netpair,...}) =
   675   biresolve_from_nets_tac safep_netpair;
   676 
   677 (*These steps could instantiate variables and are therefore unsafe.*)
   678 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   679 
   680 fun haz_step_tac (CS{haz_netpair,...}) =
   681   biresolve_from_nets_tac haz_netpair;
   682 
   683 (*Single step for the prover.  FAILS unless it makes progress. *)
   684 fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
   685         (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   686 
   687 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   688   allows backtracking from "safe" rules to "unsafe" rules here.*)
   689 fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
   690         (inst_step_tac cs APPEND' haz_step_tac cs) i;
   691 
   692 (**** The following tactics all fail unless they solve one goal ****)
   693 
   694 (*Dumb but fast*)
   695 fun fast_tac cs =
   696   ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   697 
   698 (*Slower but smarter than fast_tac*)
   699 fun best_tac cs =
   700   ObjectLogic.atomize_tac THEN'
   701   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   702 
   703 (*even a bit smarter than best_tac*)
   704 fun first_best_tac cs =
   705   ObjectLogic.atomize_tac THEN'
   706   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   707 
   708 fun slow_tac cs =
   709   ObjectLogic.atomize_tac THEN'
   710   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   711 
   712 fun slow_best_tac cs =
   713   ObjectLogic.atomize_tac THEN'
   714   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   715 
   716 
   717 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   718 val weight_ASTAR = ref 5;
   719 
   720 fun astar_tac cs =
   721   ObjectLogic.atomize_tac THEN'
   722   SELECT_GOAL
   723     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   724       (step_tac cs 1));
   725 
   726 fun slow_astar_tac cs =
   727   ObjectLogic.atomize_tac THEN'
   728   SELECT_GOAL
   729     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   730       (slow_step_tac cs 1));
   731 
   732 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   733   of much experimentation!  Changing APPEND to ORELSE below would prove
   734   easy theorems faster, but loses completeness -- and many of the harder
   735   theorems such as 43. ****)
   736 
   737 (*Non-deterministic!  Could always expand the first unsafe connective.
   738   That's hard to implement and did not perform better in experiments, due to
   739   greater search depth required.*)
   740 fun dup_step_tac (cs as (CS{dup_netpair,...})) =
   741   biresolve_from_nets_tac dup_netpair;
   742 
   743 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   744 local
   745 fun slow_step_tac' cs = appWrappers cs
   746         (instp_step_tac cs APPEND' dup_step_tac cs);
   747 in fun depth_tac cs m i state = SELECT_GOAL
   748    (safe_steps_tac cs 1 THEN_ELSE
   749         (DEPTH_SOLVE (depth_tac cs m 1),
   750          inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   751                 (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   752         )) i state;
   753 end;
   754 
   755 (*Search, with depth bound m.
   756   This is the "entry point", which does safe inferences first.*)
   757 fun safe_depth_tac cs m =
   758   SUBGOAL
   759     (fn (prem,i) =>
   760       let val deti =
   761           (*No Vars in the goal?  No need to backtrack between goals.*)
   762           case term_vars prem of
   763               []        => DETERM
   764             | _::_      => I
   765       in  SELECT_GOAL (TRY (safe_tac cs) THEN
   766                        DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   767       end);
   768 
   769 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   770 
   771 
   772 
   773 (** claset theory data **)
   774 
   775 (* theory data kind 'Provers/claset' *)
   776 
   777 structure GlobalClasetArgs =
   778 struct
   779   val name = "Provers/claset";
   780   type T = claset ref;
   781 
   782   val empty = ref empty_cs;
   783   fun copy (ref cs) = (ref cs): T;            (*create new reference!*)
   784   val prep_ext = copy;
   785   fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2));
   786   fun print _ (ref cs) = print_cs cs;
   787 end;
   788 
   789 structure GlobalClaset = TheoryDataFun(GlobalClasetArgs);
   790 val print_claset = GlobalClaset.print;
   791 val claset_ref_of_sg = GlobalClaset.get_sg;
   792 val claset_ref_of = GlobalClaset.get;
   793 
   794 
   795 (* access claset *)
   796 
   797 val claset_of_sg = ! o claset_ref_of_sg;
   798 val claset_of = claset_of_sg o Theory.sign_of;
   799 
   800 fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state;
   801 fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state;
   802 
   803 val claset = claset_of o Context.the_context;
   804 val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context;
   805 
   806 
   807 (* change claset *)
   808 
   809 fun change_claset f x = claset_ref () := (f (claset (), x));
   810 
   811 val AddDs = change_claset (op addDs);
   812 val AddEs = change_claset (op addEs);
   813 val AddIs = change_claset (op addIs);
   814 val AddSDs = change_claset (op addSDs);
   815 val AddSEs = change_claset (op addSEs);
   816 val AddSIs = change_claset (op addSIs);
   817 val Delrules = change_claset (op delrules);
   818 
   819 
   820 (* proof data kind 'Provers/claset' *)
   821 
   822 structure LocalClasetArgs =
   823 struct
   824   val name = "Provers/claset";
   825   type T = claset;
   826   val init = claset_of;
   827   fun print _ cs = print_cs cs;
   828 end;
   829 
   830 structure LocalClaset = ProofDataFun(LocalClasetArgs);
   831 val print_local_claset = LocalClaset.print;
   832 val get_local_claset = LocalClaset.get;
   833 val put_local_claset = LocalClaset.put;
   834 
   835 
   836 (* attributes *)
   837 
   838 fun change_global_cs f (thy, th) =
   839   let val r = claset_ref_of thy
   840   in r := f (! r, [th]); (thy, th) end;
   841 
   842 fun change_local_cs f (ctxt, th) =
   843   let val cs = f (get_local_claset ctxt, [th])
   844   in (put_local_claset cs ctxt, th) end;
   845 
   846 val safe_dest_global = change_global_cs (op addSDs);
   847 val safe_elim_global = change_global_cs (op addSEs);
   848 val safe_intro_global = change_global_cs (op addSIs);
   849 val haz_dest_global = change_global_cs (op addDs);
   850 val haz_elim_global = change_global_cs (op addEs);
   851 val haz_intro_global = change_global_cs (op addIs);
   852 val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
   853 
   854 val safe_dest_local = change_local_cs (op addSDs);
   855 val safe_elim_local = change_local_cs (op addSEs);
   856 val safe_intro_local = change_local_cs (op addSIs);
   857 val haz_dest_local = change_local_cs (op addDs);
   858 val haz_elim_local = change_local_cs (op addEs);
   859 val haz_intro_local = change_local_cs (op addIs);
   860 val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
   861 
   862 
   863 (* tactics referring to the implicit claset *)
   864 
   865 (*the abstraction over the proof state delays the dereferencing*)
   866 fun Safe_tac st           = safe_tac (claset()) st;
   867 fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
   868 fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
   869 fun Clarify_tac i st      = clarify_tac (claset()) i st;
   870 fun Step_tac i st         = step_tac (claset()) i st;
   871 fun Fast_tac i st         = fast_tac (claset()) i st;
   872 fun Best_tac i st         = best_tac (claset()) i st;
   873 fun Slow_tac i st         = slow_tac (claset()) i st;
   874 fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
   875 fun Deepen_tac m          = deepen_tac (claset()) m;
   876 
   877 
   878 end;
   879 
   880 
   881 
   882 (** concrete syntax of attributes **)
   883 
   884 (* add / del rules *)
   885 
   886 val introN = "intro";
   887 val elimN = "elim";
   888 val destN = "dest";
   889 val ruleN = "rule";
   890 
   891 fun add_rule xtra haz safe = Attrib.syntax
   892  (Scan.lift (Args.query |-- Scan.option Args.nat >> xtra || Args.bang >> K safe ||
   893   Scan.succeed haz));
   894 
   895 fun del_rule att = Attrib.syntax (Scan.lift Args.del >> K att);
   896 
   897 
   898 (* setup_attrs *)
   899 
   900 fun elim_format x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
   901 
   902 val setup_attrs = Attrib.add_attributes
   903  [("elim_format", (elim_format, elim_format),
   904     "destruct rule turned into elimination rule format (classical)"),
   905   (destN,
   906    (add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global,
   907     add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local),
   908     "declaration of destruction rule"),
   909   (elimN,
   910    (add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global,
   911     add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local),
   912     "declaration of elimination rule"),
   913   (introN,
   914    (add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global,
   915     add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local),
   916     "declaration of introduction rule"),
   917   (ruleN, (del_rule rule_del_global, del_rule rule_del_local),
   918     "remove declaration of intro/elim/dest rule")];
   919 
   920 
   921 
   922 (** proof methods **)
   923 
   924 (* METHOD_CLASET' *)
   925 
   926 fun METHOD_CLASET' tac ctxt =
   927   Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt));
   928 
   929 
   930 local
   931 
   932 fun may_unify t net = map snd (Tactic.orderlist (Net.unify_term net t));
   933 
   934 fun find_erules [] = K []
   935   | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
   936 fun find_irules goal = may_unify (Logic.strip_assums_concl goal);
   937 fun find_rules (inet, enet) facts goal = find_erules facts enet @ find_irules goal inet;
   938 
   939 fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
   940   let
   941     val [rules1, rules2, rules4] = ContextRules.find_rules ctxt facts goal;
   942     val rules3 = find_rules xtra_netpair facts goal;
   943     val rules = rules1 @ rules2 @ rules3 @ rules4;
   944     val ruleq = Method.multi_resolves facts rules;
   945   in
   946     Method.trace ctxt rules;
   947     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
   948   end);
   949 
   950 fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
   951   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
   952 
   953 fun default_tac rules ctxt cs facts =
   954   rule_tac rules ctxt cs facts ORELSE'
   955   AxClass.default_intro_classes_tac facts;
   956 
   957 in
   958   val rule = METHOD_CLASET' o rule_tac;
   959   val default = METHOD_CLASET' o default_tac;
   960 end;
   961 
   962 
   963 (* contradiction method *)
   964 
   965 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
   966 
   967 
   968 (* automatic methods *)
   969 
   970 val cla_modifiers =
   971  [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest_local): Method.modifier),
   972   Args.$$$ destN -- Args.colon >> K (I, haz_dest_local),
   973   Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local),
   974   Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local),
   975   Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local),
   976   Args.$$$ introN -- Args.colon >> K (I, haz_intro_local),
   977   Args.del -- Args.colon >> K (I, rule_del_local)];
   978 
   979 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   980   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
   981 
   982 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
   983   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
   984 
   985 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
   986 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
   987 
   988 
   989 
   990 (** setup_methods **)
   991 
   992 val setup_methods = Method.add_methods
   993  [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
   994   ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
   995   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
   996   ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
   997   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
   998   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
   999   ("best", cla_method' best_tac, "classical prover (best-first)"),
  1000   ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
  1001 
  1002 
  1003 
  1004 (** theory setup **)
  1005 
  1006 val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
  1007 
  1008 
  1009 
  1010 (** outer syntax **)
  1011 
  1012 val print_clasetP =
  1013   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
  1014     OuterSyntax.Keyword.diag
  1015     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
  1016       (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))));
  1017 
  1018 val _ = OuterSyntax.add_parsers [print_clasetP];
  1019 
  1020 
  1021 end;