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