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