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