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