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