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