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