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