src/Provers/classical.ML
author paulson
Thu Dec 07 16:46:14 2006 +0100 (2006-12-07)
changeset 21689 58abd6d8abd1
parent 21687 f689f729afab
child 21963 416a5338d2bb
permissions -rw-r--r--
Removal of theorem tagging, which the ATP linkup no longer requires,
     1 (*  Title:      Provers/classical.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Theorem prover for classical reasoning, including predicate calculus, set
     7 theory, etc.
     8 
     9 Rules must be classified as intro, elim, safe, hazardous (unsafe).
    10 
    11 A rule is unsafe unless it can be applied blindly without harmful results.
    12 For a rule to be safe, its premises and conclusion should be logically
    13 equivalent.  There should be no variables in the premises that are not in
    14 the conclusion.
    15 *)
    16 
    17 (*higher precedence than := facilitates use of references*)
    18 infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
    19   addSWrapper delSWrapper addWrapper delWrapper
    20   addSbefore addSafter addbefore addafter
    21   addD2 addE2 addSD2 addSE2;
    22 
    23 
    24 (*should be a type abbreviation in signature CLASSICAL*)
    25 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    26 type wrapper = (int -> tactic) -> (int -> tactic);
    27 
    28 signature CLASSICAL_DATA =
    29 sig
    30   val mp        : thm           (* [| P-->Q;  P |] ==> Q *)
    31   val not_elim  : thm           (* [| ~P;  P |] ==> R *)
    32   val classical : thm           (* (~P ==> P) ==> P *)
    33   val sizef     : thm -> int    (* size function for BEST_FIRST *)
    34   val hyp_subst_tacs: (int -> tactic) list
    35 end;
    36 
    37 signature BASIC_CLASSICAL =
    38 sig
    39   type claset
    40   val empty_cs: claset
    41   val print_cs: claset -> unit
    42   val print_claset: theory -> unit
    43   val rep_cs:
    44     claset -> {safeIs: thm list, safeEs: thm list,
    45                  hazIs: thm list, hazEs: thm list,
    46                  swrappers: (string * wrapper) list,
    47                  uwrappers: (string * wrapper) list,
    48                  safe0_netpair: netpair, safep_netpair: netpair,
    49                  haz_netpair: netpair, dup_netpair: netpair,
    50                  xtra_netpair: ContextRules.netpair}
    51   val merge_cs          : claset * claset -> claset
    52   val addDs             : claset * thm list -> claset
    53   val addEs             : claset * thm list -> claset
    54   val addIs             : claset * thm list -> claset
    55   val addSDs            : claset * thm list -> claset
    56   val addSEs            : claset * thm list -> claset
    57   val addSIs            : claset * thm list -> claset
    58   val delrules          : claset * thm list -> claset
    59   val addSWrapper       : claset * (string * wrapper) -> claset
    60   val delSWrapper       : claset *  string            -> claset
    61   val addWrapper        : claset * (string * wrapper) -> claset
    62   val delWrapper        : claset *  string            -> claset
    63   val addSbefore        : claset * (string * (int -> tactic)) -> claset
    64   val addSafter         : claset * (string * (int -> tactic)) -> claset
    65   val addbefore         : claset * (string * (int -> tactic)) -> claset
    66   val addafter          : claset * (string * (int -> tactic)) -> claset
    67   val addD2             : claset * (string * thm) -> claset
    68   val addE2             : claset * (string * thm) -> claset
    69   val addSD2            : claset * (string * thm) -> claset
    70   val addSE2            : claset * (string * thm) -> claset
    71   val appSWrappers      : claset -> wrapper
    72   val appWrappers       : claset -> wrapper
    73 
    74   val change_claset_of: theory -> (claset -> claset) -> unit
    75   val change_claset: (claset -> claset) -> unit
    76   val claset_of: theory -> claset
    77   val claset: unit -> claset
    78   val CLASET: (claset -> tactic) -> tactic
    79   val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
    80   val local_claset_of   : Proof.context -> claset
    81 
    82   val fast_tac          : claset -> int -> tactic
    83   val slow_tac          : claset -> int -> tactic
    84   val weight_ASTAR      : int ref
    85   val astar_tac         : claset -> int -> tactic
    86   val slow_astar_tac    : claset -> int -> tactic
    87   val best_tac          : claset -> int -> tactic
    88   val first_best_tac    : claset -> int -> tactic
    89   val slow_best_tac     : claset -> int -> tactic
    90   val depth_tac         : claset -> int -> int -> tactic
    91   val deepen_tac        : claset -> int -> int -> tactic
    92 
    93   val contr_tac         : int -> tactic
    94   val dup_elim          : thm -> thm
    95   val dup_intr          : thm -> thm
    96   val dup_step_tac      : claset -> int -> tactic
    97   val eq_mp_tac         : int -> tactic
    98   val haz_step_tac      : claset -> int -> tactic
    99   val joinrules         : thm list * thm list -> (bool * thm) list
   100   val mp_tac            : int -> tactic
   101   val safe_tac          : claset -> tactic
   102   val safe_steps_tac    : claset -> int -> tactic
   103   val safe_step_tac     : claset -> int -> tactic
   104   val clarify_tac       : claset -> int -> tactic
   105   val clarify_step_tac  : claset -> int -> tactic
   106   val step_tac          : claset -> int -> tactic
   107   val slow_step_tac     : claset -> int -> tactic
   108   val swapify           : thm list -> thm list
   109   val swap_res_tac      : thm list -> int -> tactic
   110   val inst_step_tac     : claset -> int -> tactic
   111   val inst0_step_tac    : claset -> int -> tactic
   112   val instp_step_tac    : claset -> int -> tactic
   113 
   114   val AddDs             : thm list -> unit
   115   val AddEs             : thm list -> unit
   116   val AddIs             : thm list -> unit
   117   val AddSDs            : thm list -> unit
   118   val AddSEs            : thm list -> unit
   119   val AddSIs            : thm list -> unit
   120   val Delrules          : thm list -> unit
   121   val Safe_tac          : tactic
   122   val Safe_step_tac     : int -> tactic
   123   val Clarify_tac       : int -> tactic
   124   val Clarify_step_tac  : int -> tactic
   125   val Step_tac          : int -> tactic
   126   val Fast_tac          : int -> tactic
   127   val Best_tac          : int -> tactic
   128   val Slow_tac          : int -> tactic
   129   val Slow_best_tac     : int -> tactic
   130   val Deepen_tac        : int -> int -> tactic
   131 end;
   132 
   133 signature CLASSICAL =
   134 sig
   135   include BASIC_CLASSICAL
   136   val swap: thm  (* ~P ==> (~Q ==> P) ==> Q *)
   137   val classical_rule: thm -> thm
   138   val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   139   val del_context_safe_wrapper: string -> theory -> theory
   140   val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   141   val del_context_unsafe_wrapper: string -> theory -> theory
   142   val get_claset: theory -> claset
   143   val print_local_claset: Proof.context -> unit
   144   val get_local_claset: Proof.context -> claset
   145   val put_local_claset: claset -> Proof.context -> Proof.context
   146   val safe_dest: int option -> attribute
   147   val safe_elim: int option -> attribute
   148   val safe_intro: int option -> attribute
   149   val haz_dest: int option -> attribute
   150   val haz_elim: int option -> attribute
   151   val haz_intro: int option -> attribute
   152   val rule_del: attribute
   153   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   154   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   155   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   156   val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
   157   val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
   158   val setup: theory -> theory
   159 end;
   160 
   161 
   162 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
   163 struct
   164 
   165 local open Data in
   166 
   167 (** classical elimination rules **)
   168 
   169 (*
   170 Classical reasoning requires stronger elimination rules.  For
   171 instance, make_elim of Pure transforms the HOL rule injD into
   172 
   173     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
   174 
   175 Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF
   176 FAILED"; classical_rule will strenthen this to
   177 
   178     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
   179 *)
   180 
   181 fun classical_rule rule =
   182   if ObjectLogic.is_elim rule then
   183     let
   184       val rule' = rule RS classical;
   185       val concl' = Thm.concl_of rule';
   186       fun redundant_hyp goal =
   187         concl' aconv Logic.strip_assums_concl goal orelse
   188           (case Logic.strip_assums_hyp goal of
   189             hyp :: hyps => exists (fn t => t aconv hyp) hyps
   190           | _ => false);
   191       val rule'' =
   192         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
   193           if i = 1 orelse redundant_hyp goal
   194           then Tactic.etac thin_rl i
   195           else all_tac))
   196         |> Seq.hd
   197         |> Drule.zero_var_indexes
   198         |> PureThy.put_name_hint (PureThy.get_name_hint rule);
   199     in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
   200   else rule;
   201 
   202 
   203 
   204 (*** Useful tactics for classical reasoning ***)
   205 
   206 val imp_elim = (*cannot use bind_thm within a structure!*)
   207   store_thm ("imp_elim", Thm.transfer (the_context ()) (classical_rule (Tactic.make_elim mp)));
   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, 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, imp_elim] i  THEN  eq_assume_tac i;
   221 
   222 val swap =
   223   store_thm ("swap", Thm.transfer (the_context ())
   224     (rule_by_tactic (etac thin_rl 1) (not_elim RS classical)));
   225 
   226 (*Creates rules to eliminate ~A, from rules to introduce A*)
   227 fun swapify intrs = intrs RLN (2, [swap]);
   228 fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x;
   229 
   230 (*Uses introduction rules in the normal way, or on negated assumptions,
   231   trying rules in order. *)
   232 fun swap_res_tac rls =
   233     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   234     in  assume_tac      ORELSE'
   235         contr_tac       ORELSE'
   236         biresolve_tac (foldr addrl [] rls)
   237     end;
   238 
   239 (*Duplication of hazardous rules, for complete provers*)
   240 fun dup_intr th = zero_var_indexes (th RS classical);
   241 
   242 fun dup_elim th =
   243     rule_by_tactic (TRYALL (etac revcut_rl))
   244       ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
   245 
   246 (**** Classical rule sets ****)
   247 
   248 datatype claset =
   249   CS of {safeIs         : thm list,                (*safe introduction rules*)
   250          safeEs         : thm list,                (*safe elimination rules*)
   251          hazIs          : thm list,                (*unsafe introduction rules*)
   252          hazEs          : thm list,                (*unsafe elimination rules*)
   253          swrappers      : (string * wrapper) list, (*for transforming safe_step_tac*)
   254          uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
   255          safe0_netpair  : netpair,                 (*nets for trivial cases*)
   256          safep_netpair  : netpair,                 (*nets for >0 subgoals*)
   257          haz_netpair    : netpair,                 (*nets for unsafe rules*)
   258          dup_netpair    : netpair,                 (*nets for duplication*)
   259          xtra_netpair   : ContextRules.netpair};   (*nets for extra rules*)
   260 
   261 (*Desired invariants are
   262         safe0_netpair = build safe0_brls,
   263         safep_netpair = build safep_brls,
   264         haz_netpair = build (joinrules(hazIs, hazEs)),
   265         dup_netpair = build (joinrules(map dup_intr hazIs,
   266                                        map dup_elim hazEs))
   267 
   268 where build = build_netpair(Net.empty,Net.empty),
   269       safe0_brls contains all brules that solve the subgoal, and
   270       safep_brls contains all brules that generate 1 or more new subgoals.
   271 The theorem lists are largely comments, though they are used in merge_cs and print_cs.
   272 Nets must be built incrementally, to save space and time.
   273 *)
   274 
   275 val empty_netpair = (Net.empty, Net.empty);
   276 
   277 val empty_cs =
   278   CS{safeIs     = [],
   279      safeEs     = [],
   280      hazIs      = [],
   281      hazEs      = [],
   282      swrappers  = [],
   283      uwrappers  = [],
   284      safe0_netpair = empty_netpair,
   285      safep_netpair = empty_netpair,
   286      haz_netpair   = empty_netpair,
   287      dup_netpair   = empty_netpair,
   288      xtra_netpair  = empty_netpair};
   289 
   290 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
   291   let val pretty_thms = map Display.pretty_thm in
   292     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   293       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   294       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   295       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   296       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
   297       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
   298     |> Pretty.chunks |> Pretty.writeln
   299   end;
   300 
   301 fun rep_cs (CS args) = args;
   302 
   303 local
   304   fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l;
   305 in
   306   fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
   307   fun appWrappers  (CS{uwrappers,...}) = wrap uwrappers;
   308 end;
   309 
   310 
   311 (*** Adding (un)safe introduction or elimination rules.
   312 
   313     In case of overlap, new rules are tried BEFORE old ones!!
   314 ***)
   315 
   316 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   317   assumptions.  Pairs elim rules with true. *)
   318 fun joinrules (intrs, elims) =
   319   (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs;
   320 
   321 fun joinrules' (intrs, elims) =
   322   map (pair true) elims @ map (pair false) intrs;
   323 
   324 (*Priority: prefer rules with fewest subgoals,
   325   then rules added most recently (preferring the head of the list).*)
   326 fun tag_brls k [] = []
   327   | tag_brls k (brl::brls) =
   328       (1000000*subgoals_of_brl brl + k, brl) ::
   329       tag_brls (k+1) brls;
   330 
   331 fun tag_brls' _ _ [] = []
   332   | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
   333 
   334 fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
   335 
   336 (*Insert into netpair that already has nI intr rules and nE elim rules.
   337   Count the intr rules double (to account for swapify).  Negate to give the
   338   new insertions the lowest priority.*)
   339 fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   340 fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
   341 
   342 fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
   343 fun delete x = delete_tagged_list (joinrules x);
   344 fun delete' x = delete_tagged_list (joinrules' x);
   345 
   346 val mem_thm = member Drule.eq_thm_prop
   347 and rem_thm = remove Drule.eq_thm_prop;
   348 
   349 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   350   is still allowed.*)
   351 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   352        if mem_thm safeIs th then
   353          warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
   354   else if mem_thm safeEs th then
   355          warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   356   else if mem_thm hazIs th then
   357          warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
   358   else if mem_thm hazEs th then
   359          warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
   360   else ();
   361 
   362 
   363 (*** Safe rules ***)
   364 
   365 fun addSI w th
   366   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   367              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   368   if mem_thm safeIs th then
   369          (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
   370           cs)
   371   else
   372   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   373           List.partition Thm.no_prems [th]
   374       val nI = length safeIs + 1
   375       and nE = length safeEs
   376   in warn_dup th cs;
   377      CS{safeIs  = th::safeIs,
   378         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   379         safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   380         safeEs  = safeEs,
   381         hazIs   = hazIs,
   382         hazEs   = hazEs,
   383         swrappers    = swrappers,
   384         uwrappers    = uwrappers,
   385         haz_netpair  = haz_netpair,
   386         dup_netpair  = dup_netpair,
   387         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
   388   end;
   389 
   390 fun addSE w th
   391   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   392              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   393   if mem_thm safeEs th then
   394          (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
   395           cs)
   396   else if has_fewer_prems 1 th then
   397     	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   398   else
   399   let
   400       val th' = classical_rule th
   401       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   402           List.partition (fn rl => nprems_of rl=1) [th']
   403       val nI = length safeIs
   404       and nE = length safeEs + 1
   405   in warn_dup th cs;
   406      CS{safeEs  = th::safeEs,
   407         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   408         safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   409         safeIs  = safeIs,
   410         hazIs   = hazIs,
   411         hazEs   = hazEs,
   412         swrappers    = swrappers,
   413         uwrappers    = uwrappers,
   414         haz_netpair  = haz_netpair,
   415         dup_netpair  = dup_netpair,
   416         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   417   end;
   418 
   419 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   420 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   421 
   422 fun make_elim th =
   423     if has_fewer_prems 1 th then
   424     	error("Ill-formed destruction rule\n" ^ string_of_thm th)
   425     else Tactic.make_elim th;
   426 
   427 fun cs addSDs ths = cs addSEs (map make_elim ths);
   428 
   429 
   430 (*** Hazardous (unsafe) rules ***)
   431 
   432 fun addI w th
   433   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   434              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   435   if mem_thm hazIs th then
   436          (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   437           cs)
   438   else
   439   let val nI = length hazIs + 1
   440       and nE = length hazEs
   441   in warn_dup th cs;
   442      CS{hazIs   = th::hazIs,
   443         haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   444         dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   445         safeIs  = safeIs,
   446         safeEs  = safeEs,
   447         hazEs   = hazEs,
   448         swrappers     = swrappers,
   449         uwrappers     = uwrappers,
   450         safe0_netpair = safe0_netpair,
   451         safep_netpair = safep_netpair,
   452         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   453   end
   454   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   455          error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   456 
   457 fun addE w th
   458   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   459             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   460   if mem_thm hazEs th then
   461          (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   462           cs)
   463   else if has_fewer_prems 1 th then
   464     	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   465   else
   466   let
   467       val th' = classical_rule th
   468       val nI = length hazIs
   469       and nE = length hazEs + 1
   470   in warn_dup th cs;
   471      CS{hazEs   = th::hazEs,
   472         haz_netpair = insert (nI,nE) ([], [th']) haz_netpair,
   473         dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair,
   474         safeIs  = safeIs,
   475         safeEs  = safeEs,
   476         hazIs   = hazIs,
   477         swrappers     = swrappers,
   478         uwrappers     = uwrappers,
   479         safe0_netpair = safe0_netpair,
   480         safep_netpair = safep_netpair,
   481         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
   482   end;
   483 
   484 fun cs addIs ths = fold_rev (addI NONE) ths cs;
   485 fun cs addEs ths = fold_rev (addE NONE) ths cs;
   486 
   487 fun cs addDs ths = cs addEs (map make_elim ths);
   488 
   489 
   490 (*** Deletion of rules
   491      Working out what to delete, requires repeating much of the code used
   492         to insert.
   493 ***)
   494 
   495 fun delSI th
   496           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   497                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   498  if mem_thm safeIs th then
   499    let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th]
   500    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   501          safep_netpair = delete (safep_rls, []) safep_netpair,
   502          safeIs = rem_thm th safeIs,
   503          safeEs = safeEs,
   504          hazIs  = hazIs,
   505          hazEs  = hazEs,
   506          swrappers    = swrappers,
   507          uwrappers    = uwrappers,
   508          haz_netpair  = haz_netpair,
   509          dup_netpair  = dup_netpair,
   510          xtra_netpair = delete' ([th], []) xtra_netpair}
   511    end
   512  else cs;
   513 
   514 fun delSE th
   515           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   516                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   517   if mem_thm safeEs th then
   518     let
   519       val th' = classical_rule th
   520       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
   521     in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   522          safep_netpair = delete ([], safep_rls) safep_netpair,
   523          safeIs = safeIs,
   524          safeEs = rem_thm th 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 
   536 fun delI th
   537          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   538                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   539  if mem_thm hazIs th then
   540      CS{haz_netpair = delete ([th], []) haz_netpair,
   541         dup_netpair = delete ([dup_intr th], []) dup_netpair,
   542         safeIs  = safeIs,
   543         safeEs  = safeEs,
   544         hazIs   = rem_thm th hazIs,
   545         hazEs   = hazEs,
   546         swrappers     = swrappers,
   547         uwrappers     = uwrappers,
   548         safe0_netpair = safe0_netpair,
   549         safep_netpair = safep_netpair,
   550         xtra_netpair = delete' ([th], []) xtra_netpair}
   551  else cs
   552  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   553         error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   554 
   555 
   556 fun delE th
   557          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   558                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   559   let val th' = classical_rule th in
   560     if mem_thm hazEs th then
   561      CS{haz_netpair = delete ([], [th']) haz_netpair,
   562         dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   563         safeIs  = safeIs,
   564         safeEs  = safeEs,
   565         hazIs   = hazIs,
   566         hazEs   = rem_thm th 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    end;
   574 
   575 
   576 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   577 fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   578   let val th' = Tactic.make_elim th in
   579     if mem_thm safeIs th orelse mem_thm safeEs th orelse
   580       mem_thm hazIs th orelse mem_thm hazEs th orelse
   581       mem_thm safeEs th' orelse mem_thm hazEs th'
   582     then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   583     else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs)
   584   end;
   585 
   586 fun cs delrules ths = fold delrule ths cs;
   587 
   588 
   589 (*** Modifying the wrapper tacticals ***)
   590 fun update_swrappers
   591 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   592     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   593  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   594     swrappers = f swrappers, uwrappers = uwrappers,
   595     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   596     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   597 
   598 fun update_uwrappers
   599 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   600     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   601  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   602     swrappers = swrappers, uwrappers = f uwrappers,
   603     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   604     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   605 
   606 
   607 (*Add/replace a safe wrapper*)
   608 fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
   609     overwrite_warn (swrappers, new_swrapper)
   610        ("Overwriting safe wrapper " ^ fst new_swrapper));
   611 
   612 (*Add/replace an unsafe wrapper*)
   613 fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
   614     overwrite_warn (uwrappers, new_uwrapper)
   615         ("Overwriting unsafe wrapper "^fst new_uwrapper));
   616 
   617 (*Remove a safe wrapper*)
   618 fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
   619   let val swrappers' = filter_out (equal name o fst) swrappers in
   620     if length swrappers <> length swrappers' then swrappers'
   621     else (warning ("No such safe wrapper in claset: "^ name); swrappers)
   622   end);
   623 
   624 (*Remove an unsafe wrapper*)
   625 fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
   626   let val uwrappers' = filter_out (equal name o fst) uwrappers in
   627     if length uwrappers <> length uwrappers' then uwrappers'
   628     else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers)
   629   end);
   630 
   631 (* compose a safe tactic alternatively before/after safe_step_tac *)
   632 fun cs addSbefore  (name,    tac1) =
   633     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   634 fun cs addSafter   (name,    tac2) =
   635     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   636 
   637 (*compose a tactic alternatively before/after the step tactic *)
   638 fun cs addbefore   (name,    tac1) =
   639     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
   640 fun cs addafter    (name,    tac2) =
   641     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
   642 
   643 fun cs addD2     (name, thm) =
   644     cs addafter  (name, datac thm 1);
   645 fun cs addE2     (name, thm) =
   646     cs addafter  (name, eatac thm 1);
   647 fun cs addSD2    (name, thm) =
   648     cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   649 fun cs addSE2    (name, thm) =
   650     cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   651 
   652 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   653   Merging the term nets may look more efficient, but the rather delicate
   654   treatment of priority might get muddled up.*)
   655 fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
   656      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
   657   let val safeIs' = fold rem_thm safeIs safeIs2
   658       val safeEs' = fold rem_thm safeEs safeEs2
   659       val hazIs' = fold rem_thm hazIs hazIs2
   660       val hazEs' = fold rem_thm hazEs hazEs2
   661       val cs1   = cs addSIs safeIs'
   662                      addSEs safeEs'
   663                      addIs  hazIs'
   664                      addEs  hazEs'
   665       val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers);
   666       val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers);
   667   in cs3
   668   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_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_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_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_tac THEN'
   765   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   766 
   767 fun slow_best_tac cs =
   768   ObjectLogic.atomize_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_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_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 |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   839     |> fold_rev (add_wrapper (op addWrapper)) uwrappers
   840   end;
   841 
   842 fun make_context_cs (swrappers, uwrappers) =
   843   ContextCS {swrappers = swrappers, uwrappers = uwrappers};
   844 
   845 val empty_context_cs = make_context_cs ([], []);
   846 
   847 fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
   848   let
   849     val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
   850     val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
   851 
   852     val swrappers' = merge_alists swrappers1 swrappers2;
   853     val uwrappers' = merge_alists uwrappers1 uwrappers2;
   854   in make_context_cs (swrappers', uwrappers') end;
   855 
   856 
   857 
   858 (** claset data **)
   859 
   860 (* global claset *)
   861 
   862 structure GlobalClaset = TheoryDataFun
   863 (struct
   864   val name = "Provers/claset";
   865   type T = claset ref * context_cs;
   866 
   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   fun print _ (ref cs, _) = print_cs cs;
   873 end);
   874 
   875 val print_claset = GlobalClaset.print;
   876 val get_claset = ! o #1 o GlobalClaset.get;
   877 
   878 val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
   879 fun map_context_cs f = GlobalClaset.map (apsnd
   880   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   881 
   882 val change_claset_of = change o #1 o GlobalClaset.get;
   883 fun change_claset f = change_claset_of (Context.the_context ()) f;
   884 
   885 fun claset_of thy =
   886   let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
   887   in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
   888 val claset = claset_of o Context.the_context;
   889 
   890 fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
   891 fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
   892 
   893 fun AddDs args = change_claset (fn cs => cs addDs args);
   894 fun AddEs args = change_claset (fn cs => cs addEs args);
   895 fun AddIs args = change_claset (fn cs => cs addIs args);
   896 fun AddSDs args = change_claset (fn cs => cs addSDs args);
   897 fun AddSEs args = change_claset (fn cs => cs addSEs args);
   898 fun AddSIs args = change_claset (fn cs => cs addSIs args);
   899 fun Delrules args = change_claset (fn cs => cs delrules args);
   900 
   901 
   902 (* context dependent components *)
   903 
   904 fun add_context_safe_wrapper wrapper = map_context_cs (apfst (merge_alists [wrapper]));
   905 fun del_context_safe_wrapper name = map_context_cs (apfst (filter_out (equal name o #1)));
   906 
   907 fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd (merge_alists [wrapper]));
   908 fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1)));
   909 
   910 
   911 (* local claset *)
   912 
   913 structure LocalClaset = ProofDataFun
   914 (struct
   915   val name = "Provers/claset";
   916   type T = claset;
   917   val init = get_claset;
   918   fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
   919 end);
   920 
   921 val print_local_claset = LocalClaset.print;
   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 
   929 (* attributes *)
   930 
   931 fun attrib f = Thm.declaration_attribute (fn th =>
   932    fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
   933     | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
   934 
   935 fun safe_dest w = attrib (addSE w o make_elim);
   936 val safe_elim = attrib o addSE;
   937 val safe_intro = attrib o addSI;
   938 fun haz_dest w = attrib (addE w o make_elim);
   939 val haz_elim = attrib o addE;
   940 val haz_intro = attrib o addI;
   941 val rule_del = attrib delrule o ContextRules.rule_del;
   942 
   943 
   944 (* tactics referring to the implicit claset *)
   945 
   946 (*the abstraction over the proof state delays the dereferencing*)
   947 fun Safe_tac st           = safe_tac (claset()) st;
   948 fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
   949 fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
   950 fun Clarify_tac i st      = clarify_tac (claset()) i st;
   951 fun Step_tac i st         = step_tac (claset()) i st;
   952 fun Fast_tac i st         = fast_tac (claset()) i st;
   953 fun Best_tac i st         = best_tac (claset()) i st;
   954 fun Slow_tac i st         = slow_tac (claset()) i st;
   955 fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
   956 fun Deepen_tac m          = deepen_tac (claset()) m;
   957 
   958 
   959 end;
   960 
   961 
   962 
   963 (** concrete syntax of attributes **)
   964 
   965 val introN = "intro";
   966 val elimN = "elim";
   967 val destN = "dest";
   968 val ruleN = "rule";
   969 
   970 val setup_attrs = Attrib.add_attributes
   971  [("swapped", swapped, "classical swap of introduction rule"),
   972   (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
   973     "declaration of Classical destruction rule"),
   974   (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
   975     "declaration of Classical elimination rule"),
   976   (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
   977     "declaration of Classical introduction rule"),
   978   (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
   979     "remove declaration of intro/elim/dest rule")];
   980 
   981 
   982 
   983 (** proof methods **)
   984 
   985 fun METHOD_CLASET tac ctxt =
   986   Method.METHOD (tac ctxt (local_claset_of ctxt));
   987 
   988 fun METHOD_CLASET' tac ctxt =
   989   Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
   990 
   991 
   992 local
   993 
   994 fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
   995   let
   996     val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
   997     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
   998     val rules = rules1 @ rules2 @ rules3 @ rules4;
   999     val ruleq = Drule.multi_resolves facts rules;
  1000   in
  1001     Method.trace ctxt rules;
  1002     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
  1003   end)
  1004   THEN_ALL_NEW Goal.norm_hhf_tac;
  1005 
  1006 fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
  1007   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
  1008 
  1009 fun default_tac rules ctxt cs facts =
  1010   HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
  1011   ClassPackage.default_intro_classes_tac facts;
  1012 
  1013 in
  1014   val rule = METHOD_CLASET' o rule_tac;
  1015   val default = METHOD_CLASET o default_tac;
  1016 end;
  1017 
  1018 
  1019 (* contradiction method *)
  1020 
  1021 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
  1022 
  1023 
  1024 (* automatic methods *)
  1025 
  1026 val cla_modifiers =
  1027  [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
  1028   Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
  1029   Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
  1030   Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
  1031   Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
  1032   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
  1033   Args.del -- Args.colon >> K (I, rule_del)];
  1034 
  1035 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
  1036   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
  1037 
  1038 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
  1039   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
  1040 
  1041 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
  1042 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
  1043 
  1044 
  1045 
  1046 (** setup_methods **)
  1047 
  1048 val setup_methods = Method.add_methods
  1049  [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
  1050   ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
  1051   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
  1052   ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
  1053   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
  1054   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
  1055   ("best", cla_method' best_tac, "classical prover (best-first)"),
  1056   ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
  1057   ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
  1058 
  1059 
  1060 
  1061 (** theory setup **)
  1062 
  1063 val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
  1064 
  1065 
  1066 
  1067 (** outer syntax **)
  1068 
  1069 val print_clasetP =
  1070   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
  1071     OuterKeyword.diag
  1072     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
  1073       (Toplevel.node_case
  1074         (Context.cases print_claset print_local_claset)
  1075         (print_local_claset o Proof.context_of)))));
  1076 
  1077 val _ = OuterSyntax.add_parsers [print_clasetP];
  1078 
  1079 
  1080 end;