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