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