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