src/Provers/classical.ML
author wenzelm
Sat Apr 16 16:15:37 2011 +0200 (2011-04-16)
changeset 42361 23f352990944
parent 41581 72a02e3dec7e
child 42439 9efdd0af15ac
permissions -rw-r--r--
modernized structure Proof_Context;
     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: Context_Rules.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) -> Proof.context -> Proof.method
   129   val cla_meth': (claset -> int -> tactic) -> 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 is_some (Object_Logic.elim_concl 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 Object_Logic.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 (fold_rev 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   let
   212     val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
   213     val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
   214   in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
   215 
   216 
   217 (**** Classical rule sets ****)
   218 
   219 datatype claset =
   220   CS of {safeIs         : thm list,                (*safe introduction rules*)
   221          safeEs         : thm list,                (*safe elimination rules*)
   222          hazIs          : thm list,                (*unsafe introduction rules*)
   223          hazEs          : thm list,                (*unsafe elimination rules*)
   224          swrappers      : (string * wrapper) list, (*for transforming safe_step_tac*)
   225          uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
   226          safe0_netpair  : netpair,                 (*nets for trivial cases*)
   227          safep_netpair  : netpair,                 (*nets for >0 subgoals*)
   228          haz_netpair    : netpair,                 (*nets for unsafe rules*)
   229          dup_netpair    : netpair,                 (*nets for duplication*)
   230          xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
   231 
   232 (*Desired invariants are
   233         safe0_netpair = build safe0_brls,
   234         safep_netpair = build safep_brls,
   235         haz_netpair = build (joinrules(hazIs, hazEs)),
   236         dup_netpair = build (joinrules(map dup_intr hazIs,
   237                                        map dup_elim hazEs))
   238 
   239 where build = build_netpair(Net.empty,Net.empty),
   240       safe0_brls contains all brules that solve the subgoal, and
   241       safep_brls contains all brules that generate 1 or more new subgoals.
   242 The theorem lists are largely comments, though they are used in merge_cs and print_cs.
   243 Nets must be built incrementally, to save space and time.
   244 *)
   245 
   246 val empty_netpair = (Net.empty, Net.empty);
   247 
   248 val empty_cs =
   249   CS{safeIs     = [],
   250      safeEs     = [],
   251      hazIs      = [],
   252      hazEs      = [],
   253      swrappers  = [],
   254      uwrappers  = [],
   255      safe0_netpair = empty_netpair,
   256      safep_netpair = empty_netpair,
   257      haz_netpair   = empty_netpair,
   258      dup_netpair   = empty_netpair,
   259      xtra_netpair  = empty_netpair};
   260 
   261 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
   262   let val pretty_thms = map Display.pretty_thm_without_context in
   263     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   264       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   265       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   266       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   267       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
   268       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
   269     |> Pretty.chunks |> Pretty.writeln
   270   end;
   271 
   272 fun rep_cs (CS args) = args;
   273 
   274 fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
   275 fun appWrappers  (CS {uwrappers, ...}) = fold snd uwrappers;
   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 rls = fold_rev Tactic.insert_tagged_brl rls;
   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 rls = fold_rev Tactic.delete_tagged_brl rls;
   310 fun delete x = delete_tagged_list (joinrules x);
   311 fun delete' x = delete_tagged_list (joinrules' x);
   312 
   313 val mem_thm = member Thm.eq_thm_prop
   314 and rem_thm = remove Thm.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 safeIs th then
   320     warning ("Rule already declared as safe introduction (intro!)\n" ^
   321       Display.string_of_thm_without_context th)
   322   else if mem_thm safeEs th then
   323     warning ("Rule already declared as safe elimination (elim!)\n" ^
   324       Display.string_of_thm_without_context th)
   325   else if mem_thm hazIs th then
   326     warning ("Rule already declared as introduction (intro)\n" ^
   327       Display.string_of_thm_without_context th)
   328   else if mem_thm hazEs th then
   329     warning ("Rule already declared as elimination (elim)\n" ^
   330       Display.string_of_thm_without_context th)
   331   else ();
   332 
   333 
   334 (*** Safe rules ***)
   335 
   336 fun addSI w th
   337   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   338              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   339   if mem_thm safeIs th then
   340     (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
   341       Display.string_of_thm_without_context th); cs)
   342   else
   343   let val th' = flat_rule th
   344       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   345           List.partition Thm.no_prems [th']
   346       val nI = length safeIs + 1
   347       and nE = length safeEs
   348   in warn_dup th cs;
   349      CS{safeIs  = th::safeIs,
   350         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   351         safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   352         safeEs  = safeEs,
   353         hazIs   = hazIs,
   354         hazEs   = hazEs,
   355         swrappers    = swrappers,
   356         uwrappers    = uwrappers,
   357         haz_netpair  = haz_netpair,
   358         dup_netpair  = dup_netpair,
   359         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
   360   end;
   361 
   362 fun addSE w th
   363   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   364              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   365   if mem_thm safeEs th then
   366     (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
   367         Display.string_of_thm_without_context th); cs)
   368   else if has_fewer_prems 1 th then
   369         error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   370   else
   371   let
   372       val th' = classical_rule (flat_rule th)
   373       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   374           List.partition (fn rl => nprems_of rl=1) [th']
   375       val nI = length safeIs
   376       and nE = length safeEs + 1
   377   in warn_dup th cs;
   378      CS{safeEs  = th::safeEs,
   379         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   380         safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   381         safeIs  = safeIs,
   382         hazIs   = hazIs,
   383         hazEs   = hazEs,
   384         swrappers    = swrappers,
   385         uwrappers    = uwrappers,
   386         haz_netpair  = haz_netpair,
   387         dup_netpair  = dup_netpair,
   388         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   389   end;
   390 
   391 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   392 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   393 
   394 fun make_elim th =
   395     if has_fewer_prems 1 th then
   396           error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
   397     else Tactic.make_elim th;
   398 
   399 fun cs addSDs ths = cs addSEs (map make_elim ths);
   400 
   401 
   402 (*** Hazardous (unsafe) rules ***)
   403 
   404 fun addI w th
   405   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   406              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   407   if mem_thm hazIs th then
   408     (warning ("Ignoring duplicate introduction (intro)\n" ^
   409         Display.string_of_thm_without_context th); cs)
   410   else
   411   let val th' = flat_rule th
   412       val nI = length hazIs + 1
   413       and nE = length hazEs
   414   in warn_dup th cs;
   415      CS{hazIs   = th::hazIs,
   416         haz_netpair = insert (nI,nE) ([th'], []) haz_netpair,
   417         dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair,
   418         safeIs  = safeIs,
   419         safeEs  = safeEs,
   420         hazEs   = hazEs,
   421         swrappers     = swrappers,
   422         uwrappers     = uwrappers,
   423         safe0_netpair = safe0_netpair,
   424         safep_netpair = safep_netpair,
   425         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   426   end
   427   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   428     error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   429 
   430 fun addE w th
   431   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   432             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   433   if mem_thm hazEs th then
   434     (warning ("Ignoring duplicate elimination (elim)\n" ^
   435         Display.string_of_thm_without_context th); cs)
   436   else if has_fewer_prems 1 th then
   437         error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   438   else
   439   let
   440       val th' = classical_rule (flat_rule th)
   441       val nI = length hazIs
   442       and nE = length hazEs + 1
   443   in warn_dup th cs;
   444      CS{hazEs   = th::hazEs,
   445         haz_netpair = insert (nI,nE) ([], [th']) haz_netpair,
   446         dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair,
   447         safeIs  = safeIs,
   448         safeEs  = safeEs,
   449         hazIs   = hazIs,
   450         swrappers     = swrappers,
   451         uwrappers     = uwrappers,
   452         safe0_netpair = safe0_netpair,
   453         safep_netpair = safep_netpair,
   454         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
   455   end;
   456 
   457 fun cs addIs ths = fold_rev (addI NONE) ths cs;
   458 fun cs addEs ths = fold_rev (addE NONE) ths cs;
   459 
   460 fun cs addDs ths = cs addEs (map make_elim ths);
   461 
   462 
   463 (*** Deletion of rules
   464      Working out what to delete, requires repeating much of the code used
   465         to insert.
   466 ***)
   467 
   468 fun delSI 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 safeIs th then
   472    let val th' = flat_rule th
   473        val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']
   474    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   475          safep_netpair = delete (safep_rls, []) safep_netpair,
   476          safeIs = rem_thm th safeIs,
   477          safeEs = safeEs,
   478          hazIs  = hazIs,
   479          hazEs  = hazEs,
   480          swrappers    = swrappers,
   481          uwrappers    = uwrappers,
   482          haz_netpair  = haz_netpair,
   483          dup_netpair  = dup_netpair,
   484          xtra_netpair = delete' ([th], []) xtra_netpair}
   485    end
   486  else cs;
   487 
   488 fun delSE 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 safeEs th then
   492     let
   493       val th' = classical_rule (flat_rule th)
   494       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
   495     in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   496          safep_netpair = delete ([], safep_rls) safep_netpair,
   497          safeIs = safeIs,
   498          safeEs = rem_thm th safeEs,
   499          hazIs  = hazIs,
   500          hazEs  = hazEs,
   501          swrappers    = swrappers,
   502          uwrappers    = uwrappers,
   503          haz_netpair  = haz_netpair,
   504          dup_netpair  = dup_netpair,
   505          xtra_netpair = delete' ([], [th]) xtra_netpair}
   506     end
   507   else cs;
   508 
   509 
   510 fun delI th
   511          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   512                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   513  if mem_thm hazIs th then
   514     let val th' = flat_rule th
   515     in CS{haz_netpair = delete ([th'], []) haz_netpair,
   516         dup_netpair = delete ([dup_intr th'], []) dup_netpair,
   517         safeIs  = safeIs,
   518         safeEs  = safeEs,
   519         hazIs   = rem_thm th hazIs,
   520         hazEs   = hazEs,
   521         swrappers     = swrappers,
   522         uwrappers     = uwrappers,
   523         safe0_netpair = safe0_netpair,
   524         safep_netpair = safep_netpair,
   525         xtra_netpair = delete' ([th], []) xtra_netpair}
   526     end
   527  else cs
   528  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   529    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   530 
   531 
   532 fun delE th
   533          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   534                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   535  if mem_thm hazEs th then
   536    let val th' = classical_rule (flat_rule th)
   537    in CS{haz_netpair = delete ([], [th']) haz_netpair,
   538         dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   539         safeIs  = safeIs,
   540         safeEs  = safeEs,
   541         hazIs   = hazIs,
   542         hazEs   = rem_thm th hazEs,
   543         swrappers     = swrappers,
   544         uwrappers     = uwrappers,
   545         safe0_netpair = safe0_netpair,
   546         safep_netpair = safep_netpair,
   547         xtra_netpair = delete' ([], [th]) xtra_netpair}
   548    end
   549  else cs;
   550 
   551 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   552 fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   553   let val th' = Tactic.make_elim th in
   554     if mem_thm safeIs th orelse mem_thm safeEs th orelse
   555       mem_thm hazIs th orelse mem_thm hazEs th orelse
   556       mem_thm safeEs th' orelse mem_thm hazEs th'
   557     then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   558     else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
   559   end;
   560 
   561 fun cs delrules ths = fold delrule ths cs;
   562 
   563 
   564 (*** Modifying the wrapper tacticals ***)
   565 fun map_swrappers f
   566   (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   567     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   568   CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   569     swrappers = f swrappers, uwrappers = uwrappers,
   570     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   571     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   572 
   573 fun map_uwrappers f
   574   (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   575     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   576   CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   577     swrappers = swrappers, uwrappers = f uwrappers,
   578     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   579     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   580 
   581 fun update_warn msg (p as (key : string, _)) xs =
   582   (if AList.defined (op =) xs key then warning msg else ();
   583     AList.update (op =) p xs);
   584 
   585 fun delete_warn msg (key : string) xs =
   586   if AList.defined (op =) xs key then AList.delete (op =) key xs
   587     else (warning msg; xs);
   588 
   589 (*Add/replace a safe wrapper*)
   590 fun cs addSWrapper new_swrapper = map_swrappers
   591   (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
   592 
   593 (*Add/replace an unsafe wrapper*)
   594 fun cs addWrapper new_uwrapper = map_uwrappers
   595   (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
   596 
   597 (*Remove a safe wrapper*)
   598 fun cs delSWrapper name = map_swrappers
   599   (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
   600 
   601 (*Remove an unsafe wrapper*)
   602 fun cs delWrapper name = map_uwrappers
   603   (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
   604 
   605 (* compose a safe tactic alternatively before/after safe_step_tac *)
   606 fun cs addSbefore  (name,    tac1) =
   607     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   608 fun cs addSafter   (name,    tac2) =
   609     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   610 
   611 (*compose a tactic alternatively before/after the step tactic *)
   612 fun cs addbefore   (name,    tac1) =
   613     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
   614 fun cs addafter    (name,    tac2) =
   615     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
   616 
   617 fun cs addD2     (name, thm) =
   618     cs addafter  (name, datac thm 1);
   619 fun cs addE2     (name, thm) =
   620     cs addafter  (name, eatac thm 1);
   621 fun cs addSD2    (name, thm) =
   622     cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   623 fun cs addSE2    (name, thm) =
   624     cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   625 
   626 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   627   Merging the term nets may look more efficient, but the rather delicate
   628   treatment of priority might get muddled up.*)
   629 fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
   630     cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
   631       swrappers, uwrappers, ...}) =
   632   if pointer_eq (cs, cs') then cs
   633   else
   634     let
   635       val safeIs' = fold rem_thm safeIs safeIs2;
   636       val safeEs' = fold rem_thm safeEs safeEs2;
   637       val hazIs' = fold rem_thm hazIs hazIs2;
   638       val hazEs' = fold rem_thm hazEs hazEs2;
   639       val cs1   = cs addSIs safeIs'
   640                      addSEs safeEs'
   641                      addIs  hazIs'
   642                      addEs  hazEs';
   643       val cs2 = map_swrappers
   644         (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
   645       val cs3 = map_uwrappers
   646         (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
   647     in cs3 end;
   648 
   649 
   650 (**** Simple tactics for theorem proving ****)
   651 
   652 (*Attack subgoals using safe inferences -- matching, not resolution*)
   653 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   654   appSWrappers cs (FIRST' [
   655         eq_assume_tac,
   656         eq_mp_tac,
   657         bimatch_from_nets_tac safe0_netpair,
   658         FIRST' hyp_subst_tacs,
   659         bimatch_from_nets_tac safep_netpair]);
   660 
   661 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   662 fun safe_steps_tac cs = REPEAT_DETERM1 o
   663         (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   664 
   665 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   666 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   667 
   668 
   669 (*** Clarify_tac: do safe steps without causing branching ***)
   670 
   671 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   672 
   673 (*version of bimatch_from_nets_tac that only applies rules that
   674   create precisely n subgoals.*)
   675 fun n_bimatch_from_nets_tac n =
   676     biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
   677 
   678 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   679 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   680 
   681 (*Two-way branching is allowed only if one of the branches immediately closes*)
   682 fun bimatch2_tac netpair i =
   683     n_bimatch_from_nets_tac 2 netpair i THEN
   684     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   685 
   686 (*Attack subgoals using safe inferences -- matching, not resolution*)
   687 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   688   appSWrappers cs (FIRST' [
   689         eq_assume_contr_tac,
   690         bimatch_from_nets_tac safe0_netpair,
   691         FIRST' hyp_subst_tacs,
   692         n_bimatch_from_nets_tac 1 safep_netpair,
   693         bimatch2_tac safep_netpair]);
   694 
   695 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   696 
   697 
   698 (*** Unsafe steps instantiate variables or lose information ***)
   699 
   700 (*Backtracking is allowed among the various these unsafe ways of
   701   proving a subgoal.  *)
   702 fun inst0_step_tac (CS {safe0_netpair, ...}) =
   703   assume_tac APPEND'
   704   contr_tac APPEND'
   705   biresolve_from_nets_tac safe0_netpair;
   706 
   707 (*These unsafe steps could generate more subgoals.*)
   708 fun instp_step_tac (CS {safep_netpair, ...}) =
   709   biresolve_from_nets_tac safep_netpair;
   710 
   711 (*These steps could instantiate variables and are therefore unsafe.*)
   712 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   713 
   714 fun haz_step_tac (CS{haz_netpair,...}) =
   715   biresolve_from_nets_tac haz_netpair;
   716 
   717 (*Single step for the prover.  FAILS unless it makes progress. *)
   718 fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
   719         (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   720 
   721 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   722   allows backtracking from "safe" rules to "unsafe" rules here.*)
   723 fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
   724         (inst_step_tac cs APPEND' haz_step_tac cs) i;
   725 
   726 (**** The following tactics all fail unless they solve one goal ****)
   727 
   728 (*Dumb but fast*)
   729 fun fast_tac cs =
   730   Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   731 
   732 (*Slower but smarter than fast_tac*)
   733 fun best_tac cs =
   734   Object_Logic.atomize_prems_tac THEN'
   735   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   736 
   737 (*even a bit smarter than best_tac*)
   738 fun first_best_tac cs =
   739   Object_Logic.atomize_prems_tac THEN'
   740   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   741 
   742 fun slow_tac cs =
   743   Object_Logic.atomize_prems_tac THEN'
   744   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   745 
   746 fun slow_best_tac cs =
   747   Object_Logic.atomize_prems_tac THEN'
   748   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   749 
   750 
   751 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   752 val weight_ASTAR = Unsynchronized.ref 5;
   753 
   754 fun astar_tac cs =
   755   Object_Logic.atomize_prems_tac THEN'
   756   SELECT_GOAL
   757     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   758       (step_tac cs 1));
   759 
   760 fun slow_astar_tac cs =
   761   Object_Logic.atomize_prems_tac THEN'
   762   SELECT_GOAL
   763     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   764       (slow_step_tac cs 1));
   765 
   766 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   767   of much experimentation!  Changing APPEND to ORELSE below would prove
   768   easy theorems faster, but loses completeness -- and many of the harder
   769   theorems such as 43. ****)
   770 
   771 (*Non-deterministic!  Could always expand the first unsafe connective.
   772   That's hard to implement and did not perform better in experiments, due to
   773   greater search depth required.*)
   774 fun dup_step_tac (CS {dup_netpair, ...}) =
   775   biresolve_from_nets_tac dup_netpair;
   776 
   777 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   778 local
   779 fun slow_step_tac' cs = appWrappers cs
   780         (instp_step_tac cs APPEND' dup_step_tac cs);
   781 in fun depth_tac cs m i state = SELECT_GOAL
   782    (safe_steps_tac cs 1 THEN_ELSE
   783         (DEPTH_SOLVE (depth_tac cs m 1),
   784          inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   785                 (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   786         )) i state;
   787 end;
   788 
   789 (*Search, with depth bound m.
   790   This is the "entry point", which does safe inferences first.*)
   791 fun safe_depth_tac cs m =
   792   SUBGOAL
   793     (fn (prem,i) =>
   794       let val deti =
   795           (*No Vars in the goal?  No need to backtrack between goals.*)
   796           if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
   797       in  SELECT_GOAL (TRY (safe_tac cs) THEN
   798                        DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   799       end);
   800 
   801 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   802 
   803 
   804 
   805 (** context dependent claset components **)
   806 
   807 datatype context_cs = ContextCS of
   808  {swrappers: (string * (Proof.context -> wrapper)) list,
   809   uwrappers: (string * (Proof.context -> wrapper)) list};
   810 
   811 fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
   812   let
   813     fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
   814   in
   815     cs
   816     |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   817     |> fold_rev (add_wrapper (op addWrapper)) uwrappers
   818   end;
   819 
   820 fun make_context_cs (swrappers, uwrappers) =
   821   ContextCS {swrappers = swrappers, uwrappers = uwrappers};
   822 
   823 val empty_context_cs = make_context_cs ([], []);
   824 
   825 fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
   826   if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
   827   else
   828     let
   829       val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
   830       val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
   831       val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
   832       val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
   833     in make_context_cs (swrappers', uwrappers') end;
   834 
   835 
   836 
   837 (** claset data **)
   838 
   839 (* global clasets *)
   840 
   841 structure GlobalClaset = Theory_Data
   842 (
   843   type T = claset * context_cs;
   844   val empty = (empty_cs, empty_context_cs);
   845   val extend = I;
   846   fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
   847     (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
   848 );
   849 
   850 val get_global_claset = #1 o GlobalClaset.get;
   851 val map_global_claset = GlobalClaset.map o apfst;
   852 
   853 val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
   854 fun map_context_cs f = GlobalClaset.map (apsnd
   855   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   856 
   857 fun global_claset_of thy =
   858   let val (cs, ctxt_cs) = GlobalClaset.get thy
   859   in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
   860 
   861 
   862 (* context dependent components *)
   863 
   864 fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
   865 fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
   866 
   867 fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
   868 fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
   869 
   870 
   871 (* local clasets *)
   872 
   873 structure LocalClaset = Proof_Data
   874 (
   875   type T = claset;
   876   val init = get_global_claset;
   877 );
   878 
   879 val get_claset = LocalClaset.get;
   880 val put_claset = LocalClaset.put;
   881 
   882 fun claset_of ctxt =
   883   context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
   884 
   885 
   886 (* generic clasets *)
   887 
   888 val get_cs = Context.cases global_claset_of claset_of;
   889 fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
   890 
   891 
   892 (* attributes *)
   893 
   894 fun attrib f = Thm.declaration_attribute (fn th =>
   895   Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
   896 
   897 fun safe_dest w = attrib (addSE w o make_elim);
   898 val safe_elim = attrib o addSE;
   899 val safe_intro = attrib o addSI;
   900 fun haz_dest w = attrib (addE w o make_elim);
   901 val haz_elim = attrib o addE;
   902 val haz_intro = attrib o addI;
   903 val rule_del = attrib delrule o Context_Rules.rule_del;
   904 
   905 
   906 end;
   907 
   908 
   909 
   910 (** concrete syntax of attributes **)
   911 
   912 val introN = "intro";
   913 val elimN = "elim";
   914 val destN = "dest";
   915 
   916 val setup_attrs =
   917   Attrib.setup @{binding swapped} (Scan.succeed swapped)
   918     "classical swap of introduction rule" #>
   919   Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
   920     "declaration of Classical destruction rule" #>
   921   Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
   922     "declaration of Classical elimination rule" #>
   923   Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
   924     "declaration of Classical introduction rule" #>
   925   Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
   926     "remove declaration of intro/elim/dest rule";
   927 
   928 
   929 
   930 (** proof methods **)
   931 
   932 local
   933 
   934 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
   935   let
   936     val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
   937     val CS {xtra_netpair, ...} = claset_of ctxt;
   938     val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
   939     val rules = rules1 @ rules2 @ rules3 @ rules4;
   940     val ruleq = Drule.multi_resolves facts rules;
   941   in
   942     Method.trace ctxt rules;
   943     fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
   944   end)
   945   THEN_ALL_NEW Goal.norm_hhf_tac;
   946 
   947 in
   948 
   949 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
   950   | rule_tac _ rules facts = Method.rule_tac rules facts;
   951 
   952 fun default_tac ctxt rules facts =
   953   HEADGOAL (rule_tac ctxt rules facts) ORELSE
   954   Class.default_intro_tac ctxt facts;
   955 
   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 NONE): Method.modifier),
   968   Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
   969   Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
   970   Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
   971   Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
   972   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
   973   Args.del -- Args.colon >> K (I, rule_del)];
   974 
   975 fun cla_meth tac ctxt = METHOD (fn facts =>
   976   ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
   977 
   978 fun cla_meth' tac ctxt = METHOD (fn facts =>
   979   HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
   980 
   981 fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
   982 fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
   983 
   984 
   985 
   986 (** setup_methods **)
   987 
   988 val setup_methods =
   989   Method.setup @{binding default}
   990    (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
   991     "apply some intro/elim rule (potentially classical)" #>
   992   Method.setup @{binding rule}
   993     (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
   994     "apply some intro/elim rule (potentially classical)" #>
   995   Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
   996     "proof by contradiction" #>
   997   Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
   998     "repeatedly apply safe steps" #>
   999   Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
  1000   Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
  1001   Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
  1002   Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
  1003     "classical prover (iterative deepening)" #>
  1004   Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
  1005     "classical prover (apply safe rules)";
  1006 
  1007 
  1008 
  1009 (** theory setup **)
  1010 
  1011 val setup = setup_attrs #> setup_methods;
  1012 
  1013 
  1014 
  1015 (** outer syntax **)
  1016 
  1017 val _ =
  1018   Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
  1019     Keyword.diag
  1020     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
  1021       Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
  1022 
  1023 end;