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