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