src/Provers/classical.ML
author wenzelm
Sun May 15 16:40:24 2011 +0200 (2011-05-15)
changeset 42812 dda4aef7cba4
parent 42810 2425068fe13a
child 42817 7e819eb7dabb
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, 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 *)
    28   val hyp_subst_tacs: (int -> tactic) list
    29 end;
    30 
    31 signature BASIC_CLASSICAL =
    32 sig
    33   type wrapper = (int -> tactic) -> int -> tactic
    34   type claset
    35   val print_claset: Proof.context -> unit
    36   val addDs: Proof.context * thm list -> Proof.context
    37   val addEs: Proof.context * thm list -> Proof.context
    38   val addIs: Proof.context * thm list -> Proof.context
    39   val addSDs: Proof.context * thm list -> Proof.context
    40   val addSEs: Proof.context * thm list -> Proof.context
    41   val addSIs: Proof.context * thm list -> Proof.context
    42   val delrules: Proof.context * thm list -> Proof.context
    43   val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
    44   val delSWrapper: claset *  string -> claset
    45   val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
    46   val delWrapper: claset *  string -> claset
    47   val addSbefore: claset * (string * (int -> tactic)) -> claset
    48   val addSafter: claset * (string * (int -> tactic)) -> claset
    49   val addbefore: claset * (string * (int -> tactic)) -> claset
    50   val addafter: claset * (string * (int -> tactic)) -> claset
    51   val addD2: claset * (string * thm) -> claset
    52   val addE2: claset * (string * thm) -> claset
    53   val addSD2: claset * (string * thm) -> claset
    54   val addSE2: claset * (string * thm) -> claset
    55   val appSWrappers: Proof.context -> wrapper
    56   val appWrappers: Proof.context -> wrapper
    57 
    58   val global_claset_of: theory -> claset
    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) =
   298       Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
   299 
   300 fun make_elim context th =
   301   if has_fewer_prems 1 th then
   302     error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   303   else Tactic.make_elim th;
   304 
   305 fun warn_thm context msg th =
   306   if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
   307   then warning (msg ^ string_of_thm context th)
   308   else ();
   309 
   310 fun warn_rules context msg rules th =
   311   Item_Net.member rules th andalso (warn_thm context msg th; true);
   312 
   313 fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   314   warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
   315   warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
   316   warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse
   317   warn_rules context "Rule already declared as elimination (elim)\n" hazEs th;
   318 
   319 
   320 (*** Safe rules ***)
   321 
   322 fun addSI w context th
   323     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   324       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   325   if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   326   else
   327     let
   328       val th' = flat_rule th;
   329       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   330         List.partition Thm.no_prems [th'];
   331       val nI = Item_Net.length safeIs + 1;
   332       val nE = Item_Net.length safeEs;
   333       val _ = warn_claset context th cs;
   334     in
   335       CS
   336        {safeIs = Item_Net.update th safeIs,
   337         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   338         safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   339         safeEs = safeEs,
   340         hazIs = hazIs,
   341         hazEs = hazEs,
   342         swrappers = swrappers,
   343         uwrappers = uwrappers,
   344         haz_netpair = haz_netpair,
   345         dup_netpair = dup_netpair,
   346         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
   347     end;
   348 
   349 fun addSE w context th
   350     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   351       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   352   if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
   353   else if has_fewer_prems 1 th then
   354     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   355   else
   356     let
   357       val th' = classical_rule (flat_rule th);
   358       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   359         List.partition (fn rl => nprems_of rl=1) [th'];
   360       val nI = Item_Net.length safeIs;
   361       val nE = Item_Net.length safeEs + 1;
   362       val _ = warn_claset context th cs;
   363     in
   364       CS
   365        {safeEs = Item_Net.update th safeEs,
   366         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   367         safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   368         safeIs = safeIs,
   369         hazIs = hazIs,
   370         hazEs = hazEs,
   371         swrappers = swrappers,
   372         uwrappers = uwrappers,
   373         haz_netpair = haz_netpair,
   374         dup_netpair = dup_netpair,
   375         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   376     end;
   377 
   378 fun addSD w context th = addSE w context (make_elim context th);
   379 
   380 
   381 (*** Hazardous (unsafe) rules ***)
   382 
   383 fun addI w context th
   384     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   385       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   386   if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   387   else
   388     let
   389       val th' = flat_rule th;
   390       val nI = Item_Net.length hazIs + 1;
   391       val nE = Item_Net.length hazEs;
   392       val _ = warn_claset context th cs;
   393     in
   394       CS
   395        {hazIs = Item_Net.update th hazIs,
   396         haz_netpair = insert (nI, nE) ([th'], []) haz_netpair,
   397         dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair,
   398         safeIs = safeIs,
   399         safeEs = safeEs,
   400         hazEs = hazEs,
   401         swrappers = swrappers,
   402         uwrappers = uwrappers,
   403         safe0_netpair = safe0_netpair,
   404         safep_netpair = safep_netpair,
   405         xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
   406     end
   407     handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
   408       error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
   409 
   410 fun addE w context th
   411     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   412       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   413   if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
   414   else if has_fewer_prems 1 th then
   415     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   416   else
   417     let
   418       val th' = classical_rule (flat_rule th);
   419       val nI = Item_Net.length hazIs;
   420       val nE = Item_Net.length hazEs + 1;
   421       val _ = warn_claset context th cs;
   422     in
   423       CS
   424        {hazEs = Item_Net.update th hazEs,
   425         haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
   426         dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair,
   427         safeIs = safeIs,
   428         safeEs = safeEs,
   429         hazIs = hazIs,
   430         swrappers = swrappers,
   431         uwrappers = uwrappers,
   432         safe0_netpair = safe0_netpair,
   433         safep_netpair = safep_netpair,
   434         xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
   435     end;
   436 
   437 fun addD w context th = addE w context (make_elim context th);
   438 
   439 
   440 
   441 (*** Deletion of rules
   442      Working out what to delete, requires repeating much of the code used
   443         to insert.
   444 ***)
   445 
   446 fun delSI th
   447     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   448       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   449   if Item_Net.member safeIs th then
   450     let
   451       val th' = flat_rule th;
   452       val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
   453     in
   454       CS
   455        {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   456         safep_netpair = delete (safep_rls, []) safep_netpair,
   457         safeIs = Item_Net.remove th safeIs,
   458         safeEs = safeEs,
   459         hazIs = hazIs,
   460         hazEs = hazEs,
   461         swrappers = swrappers,
   462         uwrappers = uwrappers,
   463         haz_netpair = haz_netpair,
   464         dup_netpair = dup_netpair,
   465         xtra_netpair = delete' ([th], []) xtra_netpair}
   466     end
   467   else cs;
   468 
   469 fun delSE th
   470     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   471       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   472   if Item_Net.member safeEs th then
   473     let
   474       val th' = classical_rule (flat_rule th);
   475       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
   476     in
   477       CS
   478        {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   479         safep_netpair = delete ([], safep_rls) safep_netpair,
   480         safeIs = safeIs,
   481         safeEs = Item_Net.remove th safeEs,
   482         hazIs = hazIs,
   483         hazEs = hazEs,
   484         swrappers = swrappers,
   485         uwrappers = uwrappers,
   486         haz_netpair = haz_netpair,
   487         dup_netpair = dup_netpair,
   488         xtra_netpair = delete' ([], [th]) xtra_netpair}
   489     end
   490   else cs;
   491 
   492 fun delI context th
   493     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   494       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   495   if Item_Net.member hazIs th then
   496     let val th' = flat_rule th in
   497       CS
   498        {haz_netpair = delete ([th'], []) haz_netpair,
   499         dup_netpair = delete ([dup_intr th'], []) dup_netpair,
   500         safeIs = safeIs,
   501         safeEs = safeEs,
   502         hazIs = Item_Net.remove th hazIs,
   503         hazEs = hazEs,
   504         swrappers = swrappers,
   505         uwrappers = uwrappers,
   506         safe0_netpair = safe0_netpair,
   507         safep_netpair = safep_netpair,
   508         xtra_netpair = delete' ([th], []) xtra_netpair}
   509     end
   510   else cs
   511   handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
   512     error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
   513 
   514 fun delE th
   515     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   516       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   517   if Item_Net.member hazEs th then
   518     let val th' = classical_rule (flat_rule th) in
   519       CS
   520        {haz_netpair = delete ([], [th']) haz_netpair,
   521         dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   522         safeIs = safeIs,
   523         safeEs = safeEs,
   524         hazIs = hazIs,
   525         hazEs = Item_Net.remove th hazEs,
   526         swrappers = swrappers,
   527         uwrappers = uwrappers,
   528         safe0_netpair = safe0_netpair,
   529         safep_netpair = safep_netpair,
   530         xtra_netpair = delete' ([], [th]) xtra_netpair}
   531     end
   532   else cs;
   533 
   534 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   535 fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   536   let val th' = Tactic.make_elim th in
   537     if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
   538       Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
   539       Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
   540     then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
   541     else (warn_thm context "Undeclared classical rule\n" th; cs)
   542   end;
   543 
   544 
   545 
   546 (** claset data **)
   547 
   548 (* wrappers *)
   549 
   550 fun map_swrappers f
   551   (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   552     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   553   CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   554     swrappers = f swrappers, uwrappers = uwrappers,
   555     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   556     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   557 
   558 fun map_uwrappers f
   559   (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   560     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   561   CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   562     swrappers = swrappers, uwrappers = f uwrappers,
   563     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   564     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   565 
   566 
   567 (* merge_cs *)
   568 
   569 (*Merge works by adding all new rules of the 2nd claset into the 1st claset,
   570   in order to preserve priorities reliably.*)
   571 
   572 fun merge_thms add thms1 thms2 =
   573   fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2);
   574 
   575 fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
   576     cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
   577       swrappers, uwrappers, ...}) =
   578   if pointer_eq (cs, cs') then cs
   579   else
   580     cs
   581     |> merge_thms (addSI NONE NONE) safeIs safeIs2
   582     |> merge_thms (addSE NONE NONE) safeEs safeEs2
   583     |> merge_thms (addI NONE NONE) hazIs hazIs2
   584     |> merge_thms (addE NONE NONE) hazEs hazEs2
   585     |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
   586     |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers));
   587 
   588 
   589 (* data *)
   590 
   591 structure Claset = Generic_Data
   592 (
   593   type T = claset;
   594   val empty = empty_cs;
   595   val extend = I;
   596   val merge = merge_cs;
   597 );
   598 
   599 val global_claset_of = Claset.get o Context.Theory;
   600 val claset_of = Claset.get o Context.Proof;
   601 val rep_claset_of = rep_cs o claset_of;
   602 
   603 val get_cs = Claset.get;
   604 val map_cs = Claset.map;
   605 
   606 fun map_claset f = Context.proof_map (map_cs f);
   607 fun put_claset cs = map_claset (K cs);
   608 
   609 fun print_claset ctxt =
   610   let
   611     val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
   612     val pretty_thms = map (Display.pretty_thm ctxt) o Item_Net.content;
   613   in
   614     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   615       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   616       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   617       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   618       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
   619       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
   620     |> Pretty.chunks |> Pretty.writeln
   621   end;
   622 
   623 
   624 (* old-style declarations *)
   625 
   626 fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt;
   627 
   628 val op addSIs = decl (addSI NONE);
   629 val op addSEs = decl (addSE NONE);
   630 val op addSDs = decl (addSD NONE);
   631 val op addIs = decl (addI NONE);
   632 val op addEs = decl (addE NONE);
   633 val op addDs = decl (addD NONE);
   634 val op delrules = decl delrule;
   635 
   636 
   637 
   638 (*** Modifying the wrapper tacticals ***)
   639 
   640 fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt));
   641 fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt));
   642 
   643 fun update_warn msg (p as (key : string, _)) xs =
   644   (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
   645 
   646 fun delete_warn msg (key : string) xs =
   647   if AList.defined (op =) xs key then AList.delete (op =) key xs
   648   else (warning msg; xs);
   649 
   650 (*Add/replace a safe wrapper*)
   651 fun cs addSWrapper new_swrapper =
   652   map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
   653 
   654 (*Add/replace an unsafe wrapper*)
   655 fun cs addWrapper new_uwrapper =
   656   map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
   657 
   658 (*Remove a safe wrapper*)
   659 fun cs delSWrapper name =
   660   map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
   661 
   662 (*Remove an unsafe wrapper*)
   663 fun cs delWrapper name =
   664   map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
   665 
   666 (* compose a safe tactic alternatively before/after safe_step_tac *)
   667 fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
   668 fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
   669 
   670 (*compose a tactic alternatively before/after the step tactic *)
   671 fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
   672 fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
   673 
   674 fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
   675 fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
   676 fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   677 fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   678 
   679 
   680 
   681 (**** Simple tactics for theorem proving ****)
   682 
   683 (*Attack subgoals using safe inferences -- matching, not resolution*)
   684 fun safe_step_tac ctxt =
   685   let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
   686     appSWrappers ctxt
   687       (FIRST'
   688        [eq_assume_tac,
   689         eq_mp_tac,
   690         bimatch_from_nets_tac safe0_netpair,
   691         FIRST' Data.hyp_subst_tacs,
   692         bimatch_from_nets_tac safep_netpair])
   693   end;
   694 
   695 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   696 fun safe_steps_tac ctxt =
   697   REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i));
   698 
   699 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   700 fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt));
   701 
   702 
   703 (*** Clarify_tac: do safe steps without causing branching ***)
   704 
   705 fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n);
   706 
   707 (*version of bimatch_from_nets_tac that only applies rules that
   708   create precisely n subgoals.*)
   709 fun n_bimatch_from_nets_tac n =
   710   biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
   711 
   712 fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i;
   713 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   714 
   715 (*Two-way branching is allowed only if one of the branches immediately closes*)
   716 fun bimatch2_tac netpair i =
   717   n_bimatch_from_nets_tac 2 netpair i THEN
   718   (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
   719 
   720 (*Attack subgoals using safe inferences -- matching, not resolution*)
   721 fun clarify_step_tac ctxt =
   722   let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
   723     appSWrappers ctxt
   724      (FIRST'
   725        [eq_assume_contr_tac,
   726         bimatch_from_nets_tac safe0_netpair,
   727         FIRST' Data.hyp_subst_tacs,
   728         n_bimatch_from_nets_tac 1 safep_netpair,
   729         bimatch2_tac safep_netpair])
   730   end;
   731 
   732 fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
   733 
   734 
   735 (*** Unsafe steps instantiate variables or lose information ***)
   736 
   737 (*Backtracking is allowed among the various these unsafe ways of
   738   proving a subgoal.  *)
   739 fun inst0_step_tac ctxt =
   740   assume_tac APPEND'
   741   contr_tac APPEND'
   742   biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
   743 
   744 (*These unsafe steps could generate more subgoals.*)
   745 fun instp_step_tac ctxt =
   746   biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
   747 
   748 (*These steps could instantiate variables and are therefore unsafe.*)
   749 fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
   750 
   751 fun haz_step_tac ctxt =
   752   biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
   753 
   754 (*Single step for the prover.  FAILS unless it makes progress. *)
   755 fun step_tac ctxt i =
   756   safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i;
   757 
   758 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   759   allows backtracking from "safe" rules to "unsafe" rules here.*)
   760 fun slow_step_tac ctxt i =
   761   safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i;
   762 
   763 
   764 (**** The following tactics all fail unless they solve one goal ****)
   765 
   766 (*Dumb but fast*)
   767 fun fast_tac ctxt =
   768   Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
   769 
   770 (*Slower but smarter than fast_tac*)
   771 fun best_tac ctxt =
   772   Object_Logic.atomize_prems_tac THEN'
   773   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
   774 
   775 (*even a bit smarter than best_tac*)
   776 fun first_best_tac ctxt =
   777   Object_Logic.atomize_prems_tac THEN'
   778   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
   779 
   780 fun slow_tac ctxt =
   781   Object_Logic.atomize_prems_tac THEN'
   782   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
   783 
   784 fun slow_best_tac ctxt =
   785   Object_Logic.atomize_prems_tac THEN'
   786   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
   787 
   788 
   789 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   790 
   791 val weight_ASTAR = 5;
   792 
   793 fun astar_tac ctxt =
   794   Object_Logic.atomize_prems_tac THEN'
   795   SELECT_GOAL
   796     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
   797       (step_tac ctxt 1));
   798 
   799 fun slow_astar_tac ctxt =
   800   Object_Logic.atomize_prems_tac THEN'
   801   SELECT_GOAL
   802     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
   803       (slow_step_tac ctxt 1));
   804 
   805 
   806 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   807   of much experimentation!  Changing APPEND to ORELSE below would prove
   808   easy theorems faster, but loses completeness -- and many of the harder
   809   theorems such as 43. ****)
   810 
   811 (*Non-deterministic!  Could always expand the first unsafe connective.
   812   That's hard to implement and did not perform better in experiments, due to
   813   greater search depth required.*)
   814 fun dup_step_tac ctxt =
   815   biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
   816 
   817 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   818 local
   819   fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt);
   820 in
   821   fun depth_tac ctxt m i state = SELECT_GOAL
   822     (safe_steps_tac ctxt 1 THEN_ELSE
   823       (DEPTH_SOLVE (depth_tac ctxt m 1),
   824         inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
   825           (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state;
   826 end;
   827 
   828 (*Search, with depth bound m.
   829   This is the "entry point", which does safe inferences first.*)
   830 fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) =>
   831   let
   832     val deti = (*No Vars in the goal?  No need to backtrack between goals.*)
   833       if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I;
   834   in
   835     SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i
   836   end);
   837 
   838 fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt);
   839 
   840 
   841 (* attributes *)
   842 
   843 fun attrib f =
   844   Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context);
   845 
   846 val safe_elim = attrib o addSE;
   847 val safe_intro = attrib o addSI;
   848 val safe_dest = attrib o addSD;
   849 val haz_elim = attrib o addE;
   850 val haz_intro = attrib o addI;
   851 val haz_dest = attrib o addD;
   852 val rule_del = attrib delrule o Context_Rules.rule_del;
   853 
   854 
   855 
   856 (** concrete syntax of attributes **)
   857 
   858 val introN = "intro";
   859 val elimN = "elim";
   860 val destN = "dest";
   861 
   862 val setup_attrs =
   863   Attrib.setup @{binding swapped} (Scan.succeed swapped)
   864     "classical swap of introduction rule" #>
   865   Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
   866     "declaration of Classical destruction rule" #>
   867   Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
   868     "declaration of Classical elimination rule" #>
   869   Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
   870     "declaration of Classical introduction rule" #>
   871   Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
   872     "remove declaration of intro/elim/dest rule";
   873 
   874 
   875 
   876 (** proof methods **)
   877 
   878 local
   879 
   880 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
   881   let
   882     val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
   883     val {xtra_netpair, ...} = rep_claset_of ctxt;
   884     val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
   885     val rules = rules1 @ rules2 @ rules3 @ rules4;
   886     val ruleq = Drule.multi_resolves facts rules;
   887   in
   888     Method.trace ctxt rules;
   889     fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
   890   end)
   891   THEN_ALL_NEW Goal.norm_hhf_tac;
   892 
   893 in
   894 
   895 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
   896   | rule_tac _ rules facts = Method.rule_tac rules facts;
   897 
   898 fun default_tac ctxt rules facts =
   899   HEADGOAL (rule_tac ctxt rules facts) ORELSE
   900   Class.default_intro_tac ctxt facts;
   901 
   902 end;
   903 
   904 
   905 (* contradiction method *)
   906 
   907 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
   908 
   909 
   910 (* automatic methods *)
   911 
   912 val cla_modifiers =
   913  [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
   914   Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
   915   Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
   916   Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
   917   Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
   918   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
   919   Args.del -- Args.colon >> K (I, rule_del)];
   920 
   921 fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
   922 fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
   923 
   924 
   925 
   926 (** setup_methods **)
   927 
   928 val setup_methods =
   929   Method.setup @{binding default}
   930    (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
   931     "apply some intro/elim rule (potentially classical)" #>
   932   Method.setup @{binding rule}
   933     (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
   934     "apply some intro/elim rule (potentially classical)" #>
   935   Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
   936     "proof by contradiction" #>
   937   Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
   938     "repeatedly apply safe steps" #>
   939   Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
   940   Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
   941   Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
   942   Method.setup @{binding deepen}
   943     (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
   944       >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
   945     "classical prover (iterative deepening)" #>
   946   Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
   947     "classical prover (apply safe rules)";
   948 
   949 
   950 
   951 (** theory setup **)
   952 
   953 val setup = setup_attrs #> setup_methods;
   954 
   955 
   956 
   957 (** outer syntax **)
   958 
   959 val _ =
   960   Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
   961     Keyword.diag
   962     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   963       Toplevel.keep (fn state =>
   964         let val ctxt = Toplevel.context_of state
   965         in print_claset ctxt end)));
   966 
   967 end;