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