src/Provers/classical.ML
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 32952 aeb1e44fbc19
child 33317 b4534348b8fd
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
     1 (*  Title:      Provers/classical.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 
     4 Theorem prover for classical reasoning, including predicate calculus, set
     5 theory, etc.
     6 
     7 Rules must be classified as intro, elim, safe, hazardous (unsafe).
     8 
     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 *)
    14 
    15 (*higher precedence than := facilitates use of references*)
    16 infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
    17   addSWrapper delSWrapper addWrapper delWrapper
    18   addSbefore addSafter addbefore addafter
    19   addD2 addE2 addSD2 addSE2;
    20 
    21 
    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);
    25 
    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;
    35 
    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
    71 
    72   val global_claset_of  : theory -> claset
    73   val claset_of         : Proof.context -> claset
    74 
    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
    85 
    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;
   107 
   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;
   134 
   135 
   136 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
   137 struct
   138 
   139 local open Data in
   140 
   141 (** classical elimination rules **)
   142 
   143 (*
   144 Classical reasoning requires stronger elimination rules.  For
   145 instance, make_elim of Pure transforms the HOL rule injD into
   146 
   147     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
   148 
   149 Such rules can cause fast_tac to fail and blast_tac to report "PROOF
   150 FAILED"; classical_rule will strenthen this to
   151 
   152     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
   153 *)
   154 
   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;
   174 
   175 (*flatten nested meta connectives in prems*)
   176 val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
   177 
   178 
   179 (*** Useful tactics for classical reasoning ***)
   180 
   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);
   186 
   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;
   190 
   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;
   193 
   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));
   197 
   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;
   206 
   207 (*Duplication of hazardous rules, for complete provers*)
   208 fun dup_intr th = zero_var_indexes (th RS classical);
   209 
   210 fun dup_elim th =
   211     rule_by_tactic (TRYALL (etac revcut_rl))
   212       ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
   213 
   214 (**** Classical rule sets ****)
   215 
   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*)
   228 
   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))
   235 
   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 *)
   242 
   243 val empty_netpair = (Net.empty, Net.empty);
   244 
   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};
   257 
   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;
   268 
   269 fun rep_cs (CS args) = args;
   270 
   271 fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
   272 fun appWrappers  (CS {uwrappers, ...}) = fold snd uwrappers;
   273 
   274 
   275 (*** Adding (un)safe introduction or elimination rules.
   276 
   277     In case of overlap, new rules are tried BEFORE old ones!!
   278 ***)
   279 
   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;
   284 
   285 fun joinrules' (intrs, elims) =
   286   map (pair true) elims @ map (pair false) intrs;
   287 
   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;
   294 
   295 fun tag_brls' _ _ [] = []
   296   | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
   297 
   298 fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls;
   299 
   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';
   305 
   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);
   309 
   310 val mem_thm = member Thm.eq_thm_prop
   311 and rem_thm = remove Thm.eq_thm_prop;
   312 
   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 ();
   329 
   330 
   331 (*** Safe rules ***)
   332 
   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;
   358 
   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;
   387 
   388 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   389 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   390 
   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;
   395 
   396 fun cs addSDs ths = cs addSEs (map make_elim ths);
   397 
   398 
   399 (*** Hazardous (unsafe) rules ***)
   400 
   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);
   426 
   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;
   453 
   454 fun cs addIs ths = fold_rev (addI NONE) ths cs;
   455 fun cs addEs ths = fold_rev (addE NONE) ths cs;
   456 
   457 fun cs addDs ths = cs addEs (map make_elim ths);
   458 
   459 
   460 (*** Deletion of rules
   461      Working out what to delete, requires repeating much of the code used
   462         to insert.
   463 ***)
   464 
   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;
   484 
   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;
   505 
   506 
   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);
   527 
   528 
   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;
   547 
   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;
   557 
   558 fun cs delrules ths = fold delrule ths cs;
   559 
   560 
   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};
   569 
   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};
   577 
   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);
   581 
   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);
   585 
   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;
   589 
   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;
   593 
   594 (*Remove a safe wrapper*)
   595 fun cs delSWrapper name = map_swrappers
   596   (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
   597 
   598 (*Remove an unsafe wrapper*)
   599 fun cs delWrapper name = map_uwrappers
   600   (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
   601 
   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);
   607 
   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);
   613 
   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);
   622 
   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'
   637                      addSEs safeEs'
   638                      addIs  hazIs'
   639                      addEs  hazEs';
   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;
   645 
   646 
   647 (**** Simple tactics for theorem proving ****)
   648 
   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]);
   657 
   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));
   661 
   662 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   663 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   664 
   665 
   666 (*** Clarify_tac: do safe steps without causing branching ***)
   667 
   668 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   669 
   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;
   674 
   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;
   677 
   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));
   682 
   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]);
   691 
   692 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   693 
   694 
   695 (*** Unsafe steps instantiate variables or lose information ***)
   696 
   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;
   703 
   704 (*These unsafe steps could generate more subgoals.*)
   705 fun instp_step_tac (CS {safep_netpair, ...}) =
   706   biresolve_from_nets_tac safep_netpair;
   707 
   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;
   710 
   711 fun haz_step_tac (CS{haz_netpair,...}) =
   712   biresolve_from_nets_tac haz_netpair;
   713 
   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;
   717 
   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;
   722 
   723 (**** The following tactics all fail unless they solve one goal ****)
   724 
   725 (*Dumb but fast*)
   726 fun fast_tac cs =
   727   ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   728 
   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));
   733 
   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)));
   738 
   739 fun slow_tac cs =
   740   ObjectLogic.atomize_prems_tac THEN'
   741   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   742 
   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));
   746 
   747 
   748 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   749 val weight_ASTAR = Unsynchronized.ref 5;
   750 
   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));
   756 
   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));
   762 
   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. ****)
   767 
   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;
   773 
   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;
   785 
   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);
   797 
   798 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   799 
   800 
   801 
   802 (** context dependent claset components **)
   803 
   804 datatype context_cs = ContextCS of
   805  {swrappers: (string * (Proof.context -> wrapper)) list,
   806   uwrappers: (string * (Proof.context -> wrapper)) list};
   807 
   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;
   816 
   817 fun make_context_cs (swrappers, uwrappers) =
   818   ContextCS {swrappers = swrappers, uwrappers = uwrappers};
   819 
   820 val empty_context_cs = make_context_cs ([], []);
   821 
   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;
   831 
   832 
   833 
   834 (** claset data **)
   835 
   836 (* global clasets *)
   837 
   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 );
   847 
   848 val get_global_claset = #1 o GlobalClaset.get;
   849 val map_global_claset = GlobalClaset.map o apfst;
   850 
   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))));
   854 
   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;
   858 
   859 
   860 (* context dependent components *)
   861 
   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)));
   864 
   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)));
   867 
   868 
   869 (* local clasets *)
   870 
   871 structure LocalClaset = ProofDataFun
   872 (
   873   type T = claset;
   874   val init = get_global_claset;
   875 );
   876 
   877 val get_claset = LocalClaset.get;
   878 val put_claset = LocalClaset.put;
   879 
   880 fun claset_of ctxt =
   881   context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
   882 
   883 
   884 (* generic clasets *)
   885 
   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);
   888 
   889 
   890 (* attributes *)
   891 
   892 fun attrib f = Thm.declaration_attribute (fn th =>
   893   Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
   894 
   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;
   902 
   903 
   904 end;
   905 
   906 
   907 
   908 (** concrete syntax of attributes **)
   909 
   910 val introN = "intro";
   911 val elimN = "elim";
   912 val destN = "dest";
   913 
   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";
   925 
   926 
   927 
   928 (** proof methods **)
   929 
   930 local
   931 
   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;
   944 
   945 in
   946 
   947 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
   948   | rule_tac _ rules facts = Method.rule_tac rules facts;
   949 
   950 fun default_tac ctxt rules facts =
   951   HEADGOAL (rule_tac ctxt rules facts) ORELSE
   952   Class.default_intro_tac ctxt facts;
   953 
   954 end;
   955 
   956 
   957 (* contradiction method *)
   958 
   959 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
   960 
   961 
   962 (* automatic methods *)
   963 
   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)];
   972 
   973 fun cla_meth tac prems ctxt = METHOD (fn facts =>
   974   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
   975 
   976 fun cla_meth' tac prems ctxt = METHOD (fn facts =>
   977   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
   978 
   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);
   981 
   982 
   983 
   984 (** setup_methods **)
   985 
   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)";
  1004 
  1005 
  1006 
  1007 (** theory setup **)
  1008 
  1009 val setup = setup_attrs #> setup_methods;
  1010 
  1011 
  1012 
  1013 (** outer syntax **)
  1014 
  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)));
  1020 
  1021 end;