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