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