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