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