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