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;