wenzelm@9938: (* Title: Provers/classical.ML wenzelm@9938: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: clasohm@0: Theorem prover for classical reasoning, including predicate calculus, set clasohm@0: theory, etc. clasohm@0: wenzelm@9563: Rules must be classified as intro, elim, safe, hazardous (unsafe). clasohm@0: clasohm@0: A rule is unsafe unless it can be applied blindly without harmful results. clasohm@0: For a rule to be safe, its premises and conclusion should be logically clasohm@0: equivalent. There should be no variables in the premises that are not in clasohm@0: the conclusion. clasohm@0: *) clasohm@0: wenzelm@4079: (*higher precedence than := facilitates use of references*) wenzelm@12376: infix 4 addSIs addSEs addSDs addIs addEs addDs delrules oheimb@4651: addSWrapper delSWrapper addWrapper delWrapper oheimb@11181: addSbefore addSafter addbefore addafter oheimb@5523: addD2 addE2 addSD2 addSE2; wenzelm@4079: clasohm@0: signature CLASSICAL_DATA = wenzelm@4079: sig wenzelm@42790: val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) wenzelm@42790: val not_elim: thm (* ~P ==> P ==> R *) wenzelm@42790: val swap: thm (* ~ P ==> (~ R ==> P) ==> R *) wenzelm@42790: val classical: thm (* (~ P ==> P) ==> P *) wenzelm@50062: val sizef: thm -> int (* size function for BEST_FIRST, typically size_of_thm *) wenzelm@50062: val hyp_subst_tacs: (int -> tactic) list (* optional tactics for substitution in wenzelm@50062: the hypotheses; assumed to be safe! *) wenzelm@4079: end; clasohm@0: wenzelm@5841: signature BASIC_CLASSICAL = wenzelm@4079: sig wenzelm@42812: type wrapper = (int -> tactic) -> int -> tactic clasohm@0: type claset wenzelm@42793: val print_claset: Proof.context -> unit wenzelm@42793: val addDs: Proof.context * thm list -> Proof.context wenzelm@42793: val addEs: Proof.context * thm list -> Proof.context wenzelm@42793: val addIs: Proof.context * thm list -> Proof.context wenzelm@42793: val addSDs: Proof.context * thm list -> Proof.context wenzelm@42793: val addSEs: Proof.context * thm list -> Proof.context wenzelm@42793: val addSIs: Proof.context * thm list -> Proof.context wenzelm@42793: val delrules: Proof.context * thm list -> Proof.context wenzelm@42793: val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset wenzelm@42790: val delSWrapper: claset * string -> claset wenzelm@42793: val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset wenzelm@42790: val delWrapper: claset * string -> claset wenzelm@42790: val addSbefore: claset * (string * (int -> tactic)) -> claset wenzelm@42790: val addSafter: claset * (string * (int -> tactic)) -> claset wenzelm@42790: val addbefore: claset * (string * (int -> tactic)) -> claset wenzelm@42790: val addafter: claset * (string * (int -> tactic)) -> claset wenzelm@42790: val addD2: claset * (string * thm) -> claset wenzelm@42790: val addE2: claset * (string * thm) -> claset wenzelm@42790: val addSD2: claset * (string * thm) -> claset wenzelm@42790: val addSE2: claset * (string * thm) -> claset wenzelm@42793: val appSWrappers: Proof.context -> wrapper wenzelm@42793: val appWrappers: Proof.context -> wrapper lcp@982: wenzelm@42790: val global_claset_of: theory -> claset wenzelm@42790: val claset_of: Proof.context -> claset wenzelm@42793: val map_claset: (claset -> claset) -> Proof.context -> Proof.context wenzelm@42793: val put_claset: claset -> Proof.context -> Proof.context wenzelm@4079: wenzelm@42793: val fast_tac: Proof.context -> int -> tactic wenzelm@42793: val slow_tac: Proof.context -> int -> tactic wenzelm@42793: val astar_tac: Proof.context -> int -> tactic wenzelm@42793: val slow_astar_tac: Proof.context -> int -> tactic wenzelm@42793: val best_tac: Proof.context -> int -> tactic wenzelm@42793: val first_best_tac: Proof.context -> int -> tactic wenzelm@42793: val slow_best_tac: Proof.context -> int -> tactic wenzelm@42793: val depth_tac: Proof.context -> int -> int -> tactic wenzelm@42793: val deepen_tac: Proof.context -> int -> int -> tactic paulson@1587: wenzelm@42790: val contr_tac: int -> tactic wenzelm@42790: val dup_elim: thm -> thm wenzelm@42790: val dup_intr: thm -> thm wenzelm@42793: val dup_step_tac: Proof.context -> int -> tactic wenzelm@42790: val eq_mp_tac: int -> tactic wenzelm@42793: val haz_step_tac: Proof.context -> int -> tactic wenzelm@42790: val joinrules: thm list * thm list -> (bool * thm) list wenzelm@42790: val mp_tac: int -> tactic wenzelm@42793: val safe_tac: Proof.context -> tactic wenzelm@42793: val safe_steps_tac: Proof.context -> int -> tactic wenzelm@42793: val safe_step_tac: Proof.context -> int -> tactic wenzelm@42793: val clarify_tac: Proof.context -> int -> tactic wenzelm@42793: val clarify_step_tac: Proof.context -> int -> tactic wenzelm@42793: val step_tac: Proof.context -> int -> tactic wenzelm@42793: val slow_step_tac: Proof.context -> int -> tactic wenzelm@42790: val swapify: thm list -> thm list wenzelm@42790: val swap_res_tac: thm list -> int -> tactic wenzelm@42793: val inst_step_tac: Proof.context -> int -> tactic wenzelm@42793: val inst0_step_tac: Proof.context -> int -> tactic wenzelm@42793: val instp_step_tac: Proof.context -> int -> tactic wenzelm@4079: end; berghofe@1724: wenzelm@5841: signature CLASSICAL = wenzelm@5841: sig wenzelm@5841: include BASIC_CLASSICAL wenzelm@18534: val classical_rule: thm -> thm wenzelm@42812: type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net wenzelm@42812: val rep_cs: claset -> wenzelm@42812: {safeIs: thm Item_Net.T, wenzelm@42812: safeEs: thm Item_Net.T, wenzelm@42812: hazIs: thm Item_Net.T, wenzelm@42812: hazEs: thm Item_Net.T, wenzelm@42812: swrappers: (string * (Proof.context -> wrapper)) list, wenzelm@42812: uwrappers: (string * (Proof.context -> wrapper)) list, wenzelm@42812: safe0_netpair: netpair, wenzelm@42812: safep_netpair: netpair, wenzelm@42812: haz_netpair: netpair, wenzelm@42812: dup_netpair: netpair, wenzelm@42812: xtra_netpair: Context_Rules.netpair} wenzelm@24021: val get_cs: Context.generic -> claset wenzelm@24021: val map_cs: (claset -> claset) -> Context.generic -> Context.generic wenzelm@18728: val safe_dest: int option -> attribute wenzelm@18728: val safe_elim: int option -> attribute wenzelm@18728: val safe_intro: int option -> attribute wenzelm@18728: val haz_dest: int option -> attribute wenzelm@18728: val haz_elim: int option -> attribute wenzelm@18728: val haz_intro: int option -> attribute wenzelm@18728: val rule_del: attribute wenzelm@30513: val cla_modifiers: Method.modifier parser list wenzelm@42793: val cla_method: wenzelm@42793: (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser wenzelm@42793: val cla_method': wenzelm@42793: (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser wenzelm@18708: val setup: theory -> theory wenzelm@5841: end; wenzelm@5841: clasohm@0: wenzelm@42799: functor Classical(Data: CLASSICAL_DATA): CLASSICAL = clasohm@0: struct clasohm@0: wenzelm@18534: (** classical elimination rules **) wenzelm@18534: wenzelm@18534: (* wenzelm@18534: Classical reasoning requires stronger elimination rules. For wenzelm@18534: instance, make_elim of Pure transforms the HOL rule injD into wenzelm@18534: wenzelm@18534: [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W wenzelm@18534: wenzelm@26938: Such rules can cause fast_tac to fail and blast_tac to report "PROOF wenzelm@18534: FAILED"; classical_rule will strenthen this to wenzelm@18534: wenzelm@18534: [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W wenzelm@18534: *) wenzelm@18534: wenzelm@18534: fun classical_rule rule = wenzelm@41581: if is_some (Object_Logic.elim_concl rule) then wenzelm@18534: let wenzelm@42792: val rule' = rule RS Data.classical; wenzelm@18534: val concl' = Thm.concl_of rule'; wenzelm@18534: fun redundant_hyp goal = wenzelm@19257: concl' aconv Logic.strip_assums_concl goal orelse wenzelm@18534: (case Logic.strip_assums_hyp goal of wenzelm@18534: hyp :: hyps => exists (fn t => t aconv hyp) hyps wenzelm@18534: | _ => false); wenzelm@18534: val rule'' = wenzelm@18534: rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => wenzelm@18534: if i = 1 orelse redundant_hyp goal wenzelm@18534: then Tactic.etac thin_rl i wenzelm@18534: else all_tac)) wenzelm@18534: |> Seq.hd wenzelm@21963: |> Drule.zero_var_indexes; wenzelm@22360: in if Thm.equiv_thm (rule, rule'') then rule else rule'' end wenzelm@18534: else rule; wenzelm@18534: wenzelm@23594: (*flatten nested meta connectives in prems*) wenzelm@35625: val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems); wenzelm@18534: wenzelm@18534: paulson@1800: (*** Useful tactics for classical reasoning ***) clasohm@0: wenzelm@10736: (*Prove goal that assumes both P and ~P. paulson@4392: No backtracking if it finds an equal assumption. Perhaps should call paulson@4392: ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) wenzelm@42792: val contr_tac = wenzelm@42792: eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac); clasohm@0: lcp@681: (*Finds P-->Q and P in the assumptions, replaces implication by Q. lcp@681: Could do the same thing for P<->Q and P... *) wenzelm@42792: fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i; clasohm@0: clasohm@0: (*Like mp_tac but instantiates no variables*) wenzelm@42792: fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; clasohm@0: clasohm@0: (*Creates rules to eliminate ~A, from rules to introduce A*) wenzelm@26412: fun swapify intrs = intrs RLN (2, [Data.swap]); wenzelm@30528: val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap)); clasohm@0: clasohm@0: (*Uses introduction rules in the normal way, or on negated assumptions, clasohm@0: trying rules in order. *) wenzelm@10736: fun swap_res_tac rls = wenzelm@42792: let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in wenzelm@42792: assume_tac ORELSE' wenzelm@42792: contr_tac ORELSE' wenzelm@42792: biresolve_tac (fold_rev addrl rls []) wenzelm@42792: end; clasohm@0: lcp@681: (*Duplication of hazardous rules, for complete provers*) wenzelm@42792: fun dup_intr th = zero_var_indexes (th RS Data.classical); lcp@681: wenzelm@42793: fun dup_elim th = (* FIXME proper context!? *) wenzelm@36546: let wenzelm@36546: val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; wenzelm@42361: val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl); wenzelm@36546: in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; wenzelm@36546: lcp@1073: paulson@1800: (**** Classical rule sets ****) clasohm@0: wenzelm@42812: type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; wenzelm@42812: type wrapper = (int -> tactic) -> int -> tactic; wenzelm@42812: clasohm@0: datatype claset = wenzelm@42793: CS of wenzelm@42810: {safeIs : thm Item_Net.T, (*safe introduction rules*) wenzelm@42810: safeEs : thm Item_Net.T, (*safe elimination rules*) wenzelm@42810: hazIs : thm Item_Net.T, (*unsafe introduction rules*) wenzelm@42810: hazEs : thm Item_Net.T, (*unsafe elimination rules*) wenzelm@42793: swrappers : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*) wenzelm@42793: uwrappers : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*) wenzelm@42793: safe0_netpair : netpair, (*nets for trivial cases*) wenzelm@42793: safep_netpair : netpair, (*nets for >0 subgoals*) wenzelm@42793: haz_netpair : netpair, (*nets for unsafe rules*) wenzelm@42793: dup_netpair : netpair, (*nets for duplication*) wenzelm@42793: xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*) clasohm@0: lcp@1073: (*Desired invariants are wenzelm@9938: safe0_netpair = build safe0_brls, wenzelm@9938: safep_netpair = build safep_brls, wenzelm@9938: haz_netpair = build (joinrules(hazIs, hazEs)), wenzelm@10736: dup_netpair = build (joinrules(map dup_intr hazIs, wenzelm@12376: map dup_elim hazEs)) lcp@1073: wenzelm@10736: where build = build_netpair(Net.empty,Net.empty), lcp@1073: safe0_brls contains all brules that solve the subgoal, and lcp@1073: safep_brls contains all brules that generate 1 or more new subgoals. wenzelm@4079: The theorem lists are largely comments, though they are used in merge_cs and print_cs. lcp@1073: Nets must be built incrementally, to save space and time. lcp@1073: *) clasohm@0: wenzelm@6502: val empty_netpair = (Net.empty, Net.empty); wenzelm@6502: wenzelm@10736: val empty_cs = wenzelm@42793: CS wenzelm@42810: {safeIs = Thm.full_rules, wenzelm@42810: safeEs = Thm.full_rules, wenzelm@42810: hazIs = Thm.full_rules, wenzelm@42810: hazEs = Thm.full_rules, wenzelm@42793: swrappers = [], wenzelm@42793: uwrappers = [], wenzelm@42793: safe0_netpair = empty_netpair, wenzelm@42793: safep_netpair = empty_netpair, wenzelm@42793: haz_netpair = empty_netpair, wenzelm@42793: dup_netpair = empty_netpair, wenzelm@42793: xtra_netpair = empty_netpair}; clasohm@0: oheimb@4653: fun rep_cs (CS args) = args; lcp@1073: wenzelm@4079: paulson@1800: (*** Adding (un)safe introduction or elimination rules. lcp@1073: lcp@1073: In case of overlap, new rules are tried BEFORE old ones!! paulson@1800: ***) clasohm@0: wenzelm@12376: (*For use with biresolve_tac. Combines intro rules with swap to handle negated lcp@1073: assumptions. Pairs elim rules with true. *) wenzelm@12376: fun joinrules (intrs, elims) = paulson@18557: (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs; wenzelm@12376: wenzelm@12401: fun joinrules' (intrs, elims) = paulson@18557: map (pair true) elims @ map (pair false) intrs; lcp@1073: wenzelm@10736: (*Priority: prefer rules with fewest subgoals, paulson@1231: then rules added most recently (preferring the head of the list).*) lcp@1073: fun tag_brls k [] = [] lcp@1073: | tag_brls k (brl::brls) = wenzelm@10736: (1000000*subgoals_of_brl brl + k, brl) :: lcp@1073: tag_brls (k+1) brls; lcp@1073: wenzelm@12401: fun tag_brls' _ _ [] = [] wenzelm@12401: | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; wenzelm@10736: wenzelm@23178: fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls; lcp@1073: lcp@1073: (*Insert into netpair that already has nI intr rules and nE elim rules. lcp@1073: Count the intr rules double (to account for swapify). Negate to give the lcp@1073: new insertions the lowest priority.*) wenzelm@12376: fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; wenzelm@12401: fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules'; lcp@1073: wenzelm@23178: fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; wenzelm@12362: fun delete x = delete_tagged_list (joinrules x); wenzelm@12401: fun delete' x = delete_tagged_list (joinrules' x); paulson@1800: wenzelm@42793: fun string_of_thm NONE = Display.string_of_thm_without_context wenzelm@42817: | string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context); wenzelm@42793: wenzelm@42793: fun make_elim context th = wenzelm@42793: if has_fewer_prems 1 th then wenzelm@42793: error ("Ill-formed destruction rule\n" ^ string_of_thm context th) wenzelm@42793: else Tactic.make_elim th; wenzelm@42790: wenzelm@46874: fun warn_thm opt_context msg th = wenzelm@46874: if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false) wenzelm@46874: then warning (msg ^ string_of_thm opt_context th) wenzelm@42807: else (); wenzelm@42793: wenzelm@42807: fun warn_rules context msg rules th = wenzelm@42810: Item_Net.member rules th andalso (warn_thm context msg th; true); wenzelm@42807: wenzelm@42807: fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) = wenzelm@42807: warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse wenzelm@42807: warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse wenzelm@42807: warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse wenzelm@42807: warn_rules context "Rule already declared as elimination (elim)\n" hazEs th; paulson@1927: wenzelm@12376: paulson@1800: (*** Safe rules ***) lcp@982: wenzelm@42793: fun addSI w context th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42807: if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs paulson@1927: else wenzelm@42790: let wenzelm@42790: val th' = flat_rule th; wenzelm@23594: val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) wenzelm@42790: List.partition Thm.no_prems [th']; wenzelm@42810: val nI = Item_Net.length safeIs + 1; wenzelm@42810: val nE = Item_Net.length safeEs; wenzelm@42807: val _ = warn_claset context th cs; wenzelm@42790: in wenzelm@42790: CS wenzelm@42810: {safeIs = Item_Net.update th safeIs, lcp@1073: safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, wenzelm@9938: safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, wenzelm@42790: safeEs = safeEs, wenzelm@42790: hazIs = hazIs, wenzelm@42790: hazEs = hazEs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@42790: haz_netpair = haz_netpair, wenzelm@42790: dup_netpair = dup_netpair, wenzelm@18691: xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} wenzelm@42790: end; lcp@1073: wenzelm@42793: fun addSE w context th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42807: if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs paulson@18557: else if has_fewer_prems 1 th then wenzelm@42793: error ("Ill-formed elimination rule\n" ^ string_of_thm context th) paulson@1927: else wenzelm@42790: let wenzelm@42790: val th' = classical_rule (flat_rule th); wenzelm@18534: val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) wenzelm@42790: List.partition (fn rl => nprems_of rl=1) [th']; wenzelm@42810: val nI = Item_Net.length safeIs; wenzelm@42810: val nE = Item_Net.length safeEs + 1; wenzelm@42807: val _ = warn_claset context th cs; wenzelm@42790: in wenzelm@42790: CS wenzelm@42810: {safeEs = Item_Net.update th safeEs, lcp@1073: safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, wenzelm@9938: safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, wenzelm@42790: safeIs = safeIs, wenzelm@42790: hazIs = hazIs, wenzelm@42790: hazEs = hazEs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@42790: haz_netpair = haz_netpair, wenzelm@42790: dup_netpair = dup_netpair, wenzelm@18691: xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} wenzelm@42790: end; clasohm@0: wenzelm@42793: fun addSD w context th = addSE w context (make_elim context th); wenzelm@42793: lcp@1073: paulson@1800: (*** Hazardous (unsafe) rules ***) clasohm@0: wenzelm@42793: fun addI w context th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42807: if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs paulson@1927: else wenzelm@42790: let wenzelm@42790: val th' = flat_rule th; wenzelm@42810: val nI = Item_Net.length hazIs + 1; wenzelm@42810: val nE = Item_Net.length hazEs; wenzelm@42807: val _ = warn_claset context th cs; wenzelm@42790: in wenzelm@42790: CS wenzelm@42810: {hazIs = Item_Net.update th hazIs, wenzelm@42790: haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, wenzelm@42790: dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, wenzelm@42790: safeIs = safeIs, wenzelm@42790: safeEs = safeEs, wenzelm@42790: hazEs = hazEs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@9938: safe0_netpair = safe0_netpair, wenzelm@9938: safep_netpair = safep_netpair, wenzelm@42790: xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} wenzelm@42790: end wenzelm@42790: handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) wenzelm@42793: error ("Ill-formed introduction rule\n" ^ string_of_thm context th); lcp@1073: wenzelm@42793: fun addE w context th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42807: if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs paulson@18557: else if has_fewer_prems 1 th then wenzelm@42793: error ("Ill-formed elimination rule\n" ^ string_of_thm context th) paulson@1927: else wenzelm@42790: let wenzelm@42790: val th' = classical_rule (flat_rule th); wenzelm@42810: val nI = Item_Net.length hazIs; wenzelm@42810: val nE = Item_Net.length hazEs + 1; wenzelm@42807: val _ = warn_claset context th cs; wenzelm@42790: in wenzelm@42790: CS wenzelm@42810: {hazEs = Item_Net.update th hazEs, wenzelm@42790: haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, wenzelm@42790: dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair, wenzelm@42790: safeIs = safeIs, wenzelm@42790: safeEs = safeEs, wenzelm@42790: hazIs = hazIs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@9938: safe0_netpair = safe0_netpair, wenzelm@9938: safep_netpair = safep_netpair, wenzelm@42790: xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} wenzelm@42790: end; clasohm@0: wenzelm@42793: fun addD w context th = addE w context (make_elim context th); wenzelm@42793: clasohm@0: lcp@1073: wenzelm@10736: (*** Deletion of rules paulson@1800: Working out what to delete, requires repeating much of the code used wenzelm@9938: to insert. paulson@1800: ***) paulson@1800: wenzelm@10736: fun delSI th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42810: if Item_Net.member safeIs th then wenzelm@18534: let wenzelm@42790: val th' = flat_rule th; wenzelm@42790: val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; wenzelm@42790: in wenzelm@42790: CS wenzelm@42790: {safe0_netpair = delete (safe0_rls, []) safe0_netpair, wenzelm@42790: safep_netpair = delete (safep_rls, []) safep_netpair, wenzelm@42810: safeIs = Item_Net.remove th safeIs, wenzelm@42790: safeEs = safeEs, wenzelm@42790: hazIs = hazIs, wenzelm@42790: hazEs = hazEs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@42790: haz_netpair = haz_netpair, wenzelm@42790: dup_netpair = dup_netpair, wenzelm@42790: xtra_netpair = delete' ([th], []) xtra_netpair} wenzelm@18534: end wenzelm@18534: else cs; paulson@1800: wenzelm@42790: fun delSE th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42810: if Item_Net.member safeEs th then wenzelm@42790: let wenzelm@42790: val th' = classical_rule (flat_rule th); wenzelm@42790: val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th']; wenzelm@42790: in wenzelm@42790: CS wenzelm@42790: {safe0_netpair = delete ([], safe0_rls) safe0_netpair, wenzelm@42790: safep_netpair = delete ([], safep_rls) safep_netpair, wenzelm@42790: safeIs = safeIs, wenzelm@42810: safeEs = Item_Net.remove th safeEs, wenzelm@42790: hazIs = hazIs, wenzelm@42790: hazEs = hazEs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@42790: haz_netpair = haz_netpair, wenzelm@42790: dup_netpair = dup_netpair, wenzelm@42790: xtra_netpair = delete' ([], [th]) xtra_netpair} wenzelm@42790: end wenzelm@42790: else cs; paulson@1800: wenzelm@42793: fun delI context th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42810: if Item_Net.member hazIs th then wenzelm@42790: let val th' = flat_rule th in wenzelm@42790: CS wenzelm@42790: {haz_netpair = delete ([th'], []) haz_netpair, wenzelm@23594: dup_netpair = delete ([dup_intr th'], []) dup_netpair, wenzelm@42790: safeIs = safeIs, wenzelm@42790: safeEs = safeEs, wenzelm@42810: hazIs = Item_Net.remove th hazIs, wenzelm@42790: hazEs = hazEs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@9938: safe0_netpair = safe0_netpair, wenzelm@9938: safep_netpair = safep_netpair, wenzelm@12401: xtra_netpair = delete' ([th], []) xtra_netpair} wenzelm@23594: end wenzelm@42790: else cs wenzelm@42790: handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) wenzelm@42793: error ("Ill-formed introduction rule\n" ^ string_of_thm context th); paulson@1800: paulson@2813: fun delE th wenzelm@42790: (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, wenzelm@42790: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = wenzelm@42810: if Item_Net.member hazEs th then wenzelm@42790: let val th' = classical_rule (flat_rule th) in wenzelm@42790: CS wenzelm@42790: {haz_netpair = delete ([], [th']) haz_netpair, wenzelm@18534: dup_netpair = delete ([], [dup_elim th']) dup_netpair, wenzelm@42790: safeIs = safeIs, wenzelm@42790: safeEs = safeEs, wenzelm@42790: hazIs = hazIs, wenzelm@42810: hazEs = Item_Net.remove th hazEs, wenzelm@42790: swrappers = swrappers, wenzelm@42790: uwrappers = uwrappers, wenzelm@9938: safe0_netpair = safe0_netpair, wenzelm@9938: safep_netpair = safep_netpair, wenzelm@12401: xtra_netpair = delete' ([], [th]) xtra_netpair} wenzelm@42790: end wenzelm@42790: else cs; paulson@1800: paulson@2813: (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) wenzelm@42793: fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = wenzelm@42793: let val th' = Tactic.make_elim th in wenzelm@42810: if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse wenzelm@42810: Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse wenzelm@42810: Item_Net.member safeEs th' orelse Item_Net.member hazEs th' wenzelm@42793: then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs))))) wenzelm@42807: else (warn_thm context "Undeclared classical rule\n" th; cs) wenzelm@9938: end; paulson@1800: paulson@1800: wenzelm@42793: wenzelm@42793: (** claset data **) wenzelm@42790: wenzelm@42793: (* wrappers *) wenzelm@42790: haftmann@22674: fun map_swrappers f haftmann@22674: (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, haftmann@22674: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = haftmann@22674: CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, oheimb@4767: swrappers = f swrappers, uwrappers = uwrappers, oheimb@4767: safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, wenzelm@6955: haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; oheimb@4767: haftmann@22674: fun map_uwrappers f wenzelm@42793: (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, haftmann@22674: safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = haftmann@22674: CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, oheimb@4767: swrappers = swrappers, uwrappers = f uwrappers, oheimb@4767: safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, wenzelm@6955: haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; oheimb@4767: haftmann@22674: wenzelm@42793: (* merge_cs *) lcp@982: wenzelm@42810: (*Merge works by adding all new rules of the 2nd claset into the 1st claset, wenzelm@42810: in order to preserve priorities reliably.*) wenzelm@42810: wenzelm@42810: fun merge_thms add thms1 thms2 = wenzelm@42810: fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2); wenzelm@42810: haftmann@22674: fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, wenzelm@24358: cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, haftmann@22674: swrappers, uwrappers, ...}) = wenzelm@24358: if pointer_eq (cs, cs') then cs wenzelm@24358: else wenzelm@42810: cs wenzelm@42810: |> merge_thms (addSI NONE NONE) safeIs safeIs2 wenzelm@42810: |> merge_thms (addSE NONE NONE) safeEs safeEs2 wenzelm@42810: |> merge_thms (addI NONE NONE) hazIs hazIs2 wenzelm@42810: |> merge_thms (addE NONE NONE) hazEs hazEs2 wenzelm@42810: |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) wenzelm@42810: |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)); wenzelm@42793: wenzelm@42793: wenzelm@42793: (* data *) wenzelm@42793: wenzelm@42793: structure Claset = Generic_Data wenzelm@42793: ( wenzelm@42793: type T = claset; wenzelm@42793: val empty = empty_cs; wenzelm@42793: val extend = I; wenzelm@42793: val merge = merge_cs; wenzelm@42793: ); wenzelm@42793: wenzelm@42793: val global_claset_of = Claset.get o Context.Theory; wenzelm@42793: val claset_of = Claset.get o Context.Proof; wenzelm@42793: val rep_claset_of = rep_cs o claset_of; wenzelm@42793: wenzelm@42793: val get_cs = Claset.get; wenzelm@42793: val map_cs = Claset.map; wenzelm@42793: wenzelm@42793: fun map_claset f = Context.proof_map (map_cs f); wenzelm@42793: fun put_claset cs = map_claset (K cs); wenzelm@42793: wenzelm@42793: fun print_claset ctxt = wenzelm@42793: let wenzelm@42793: val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; wenzelm@51580: val pretty_thms = map (Pretty.item o single o Display.pretty_thm ctxt) o Item_Net.content; wenzelm@42793: in wenzelm@42793: [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), wenzelm@42793: Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), wenzelm@42793: Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), wenzelm@42793: Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), wenzelm@42793: Pretty.strs ("safe wrappers:" :: map #1 swrappers), wenzelm@42793: Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] wenzelm@42793: |> Pretty.chunks |> Pretty.writeln wenzelm@42793: end; wenzelm@42793: wenzelm@42793: wenzelm@42793: (* old-style declarations *) wenzelm@42793: wenzelm@42793: fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt; wenzelm@42793: wenzelm@42793: val op addSIs = decl (addSI NONE); wenzelm@42793: val op addSEs = decl (addSE NONE); wenzelm@42793: val op addSDs = decl (addSD NONE); wenzelm@42793: val op addIs = decl (addI NONE); wenzelm@42793: val op addEs = decl (addE NONE); wenzelm@42793: val op addDs = decl (addD NONE); wenzelm@42793: val op delrules = decl delrule; wenzelm@42793: wenzelm@42793: wenzelm@42793: wenzelm@42793: (*** Modifying the wrapper tacticals ***) wenzelm@42793: wenzelm@42793: fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); wenzelm@42793: fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); wenzelm@42793: wenzelm@42793: fun update_warn msg (p as (key : string, _)) xs = wenzelm@42793: (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); wenzelm@42793: wenzelm@42793: fun delete_warn msg (key : string) xs = wenzelm@42793: if AList.defined (op =) xs key then AList.delete (op =) key xs wenzelm@42793: else (warning msg; xs); wenzelm@42793: wenzelm@42793: (*Add/replace a safe wrapper*) wenzelm@42793: fun cs addSWrapper new_swrapper = wenzelm@42793: map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; wenzelm@42793: wenzelm@42793: (*Add/replace an unsafe wrapper*) wenzelm@42793: fun cs addWrapper new_uwrapper = wenzelm@42793: map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; wenzelm@42793: wenzelm@42793: (*Remove a safe wrapper*) wenzelm@42793: fun cs delSWrapper name = wenzelm@42793: map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; wenzelm@42793: wenzelm@42793: (*Remove an unsafe wrapper*) wenzelm@42793: fun cs delWrapper name = wenzelm@42793: map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; wenzelm@42793: wenzelm@42793: (* compose a safe tactic alternatively before/after safe_step_tac *) wenzelm@42793: fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2); wenzelm@42793: fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2); wenzelm@42793: wenzelm@42793: (*compose a tactic alternatively before/after the step tactic *) wenzelm@42793: fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2); wenzelm@42793: fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2); wenzelm@42793: wenzelm@46459: fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac); wenzelm@46459: fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac); wenzelm@42793: fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); wenzelm@42793: fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); wenzelm@42793: paulson@1711: lcp@982: paulson@1800: (**** Simple tactics for theorem proving ****) clasohm@0: clasohm@0: (*Attack subgoals using safe inferences -- matching, not resolution*) wenzelm@42793: fun safe_step_tac ctxt = wenzelm@42793: let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in wenzelm@42793: appSWrappers ctxt wenzelm@42793: (FIRST' wenzelm@42793: [eq_assume_tac, wenzelm@9938: eq_mp_tac, wenzelm@9938: bimatch_from_nets_tac safe0_netpair, wenzelm@42792: FIRST' Data.hyp_subst_tacs, wenzelm@42793: bimatch_from_nets_tac safep_netpair]) wenzelm@42793: end; clasohm@0: oheimb@5757: (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) wenzelm@42793: fun safe_steps_tac ctxt = wenzelm@42793: REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i)); oheimb@5757: clasohm@0: (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) wenzelm@42793: fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt)); lcp@747: paulson@3705: paulson@3705: (*** Clarify_tac: do safe steps without causing branching ***) paulson@3705: wenzelm@42790: fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n); paulson@3705: paulson@3705: (*version of bimatch_from_nets_tac that only applies rules that paulson@3705: create precisely n subgoals.*) wenzelm@10736: fun n_bimatch_from_nets_tac n = wenzelm@42790: biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true; paulson@3705: wenzelm@42792: fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i; paulson@3705: val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; paulson@3705: paulson@3705: (*Two-way branching is allowed only if one of the branches immediately closes*) paulson@3705: fun bimatch2_tac netpair i = wenzelm@42790: n_bimatch_from_nets_tac 2 netpair i THEN wenzelm@42790: (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1)); paulson@3705: paulson@3705: (*Attack subgoals using safe inferences -- matching, not resolution*) wenzelm@42793: fun clarify_step_tac ctxt = wenzelm@42793: let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in wenzelm@42793: appSWrappers ctxt wenzelm@42793: (FIRST' wenzelm@42793: [eq_assume_contr_tac, wenzelm@9938: bimatch_from_nets_tac safe0_netpair, wenzelm@42792: FIRST' Data.hyp_subst_tacs, wenzelm@9938: n_bimatch_from_nets_tac 1 safep_netpair, wenzelm@42793: bimatch2_tac safep_netpair]) wenzelm@42793: end; paulson@3705: wenzelm@42793: fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1)); paulson@3705: paulson@3705: paulson@3705: (*** Unsafe steps instantiate variables or lose information ***) paulson@3705: paulson@4066: (*Backtracking is allowed among the various these unsafe ways of paulson@4066: proving a subgoal. *) wenzelm@42793: fun inst0_step_tac ctxt = wenzelm@32862: assume_tac APPEND' wenzelm@32862: contr_tac APPEND' wenzelm@42793: biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt)); lcp@747: paulson@4066: (*These unsafe steps could generate more subgoals.*) wenzelm@42793: fun instp_step_tac ctxt = wenzelm@42793: biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt)); clasohm@0: clasohm@0: (*These steps could instantiate variables and are therefore unsafe.*) wenzelm@42793: fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; clasohm@0: wenzelm@42793: fun haz_step_tac ctxt = wenzelm@42793: biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt)); lcp@681: clasohm@0: (*Single step for the prover. FAILS unless it makes progress. *) wenzelm@42793: fun step_tac ctxt i = wenzelm@42793: safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i; clasohm@0: clasohm@0: (*Using a "safe" rule to instantiate variables is unsafe. This tactic clasohm@0: allows backtracking from "safe" rules to "unsafe" rules here.*) wenzelm@42793: fun slow_step_tac ctxt i = wenzelm@42793: safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i; clasohm@0: wenzelm@42791: paulson@1800: (**** The following tactics all fail unless they solve one goal ****) clasohm@0: clasohm@0: (*Dumb but fast*) wenzelm@42793: fun fast_tac ctxt = wenzelm@42793: Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); clasohm@0: clasohm@0: (*Slower but smarter than fast_tac*) wenzelm@42793: fun best_tac ctxt = wenzelm@35625: Object_Logic.atomize_prems_tac THEN' wenzelm@42793: SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); clasohm@0: oheimb@9402: (*even a bit smarter than best_tac*) wenzelm@42793: fun first_best_tac ctxt = wenzelm@35625: Object_Logic.atomize_prems_tac THEN' wenzelm@42793: SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); oheimb@9402: wenzelm@42793: fun slow_tac ctxt = wenzelm@35625: Object_Logic.atomize_prems_tac THEN' wenzelm@42793: SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1)); clasohm@0: wenzelm@42793: fun slow_best_tac ctxt = wenzelm@35625: Object_Logic.atomize_prems_tac THEN' wenzelm@42793: SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); clasohm@0: lcp@681: wenzelm@10736: (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) wenzelm@42791: wenzelm@42791: val weight_ASTAR = 5; paulson@1587: wenzelm@42793: fun astar_tac ctxt = wenzelm@35625: Object_Logic.atomize_prems_tac THEN' wenzelm@10382: SELECT_GOAL wenzelm@42791: (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev) wenzelm@42793: (step_tac ctxt 1)); paulson@1587: wenzelm@42793: fun slow_astar_tac ctxt = wenzelm@35625: Object_Logic.atomize_prems_tac THEN' wenzelm@10382: SELECT_GOAL wenzelm@42791: (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev) wenzelm@42793: (slow_step_tac ctxt 1)); paulson@1587: wenzelm@42790: paulson@1800: (**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome lcp@747: of much experimentation! Changing APPEND to ORELSE below would prove lcp@747: easy theorems faster, but loses completeness -- and many of the harder paulson@1800: theorems such as 43. ****) lcp@681: lcp@747: (*Non-deterministic! Could always expand the first unsafe connective. lcp@747: That's hard to implement and did not perform better in experiments, due to lcp@747: greater search depth required.*) wenzelm@42793: fun dup_step_tac ctxt = wenzelm@42793: biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt)); lcp@681: oheimb@5523: (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) oheimb@5757: local wenzelm@42793: fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt); wenzelm@42790: in wenzelm@42793: fun depth_tac ctxt m i state = SELECT_GOAL wenzelm@42793: (safe_steps_tac ctxt 1 THEN_ELSE wenzelm@42793: (DEPTH_SOLVE (depth_tac ctxt m 1), wenzelm@42793: inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac wenzelm@42793: (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state; oheimb@5757: end; lcp@747: wenzelm@10736: (*Search, with depth bound m. paulson@2173: This is the "entry point", which does safe inferences first.*) wenzelm@42793: fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) => wenzelm@42793: let wenzelm@42793: val deti = (*No Vars in the goal? No need to backtrack between goals.*) wenzelm@42793: if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I; wenzelm@42790: in wenzelm@42793: SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i wenzelm@42790: end); lcp@681: wenzelm@42793: fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); wenzelm@24021: wenzelm@24021: wenzelm@5885: (* attributes *) wenzelm@5885: wenzelm@42793: fun attrib f = wenzelm@42793: Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context); wenzelm@5885: wenzelm@18691: val safe_elim = attrib o addSE; wenzelm@18691: val safe_intro = attrib o addSI; wenzelm@42793: val safe_dest = attrib o addSD; wenzelm@18691: val haz_elim = attrib o addE; wenzelm@18691: val haz_intro = attrib o addI; wenzelm@42793: val haz_dest = attrib o addD; wenzelm@45375: wenzelm@45375: val rule_del = wenzelm@45375: Thm.declaration_attribute (fn th => fn context => wenzelm@45375: context |> map_cs (delrule (SOME context) th) |> wenzelm@45375: Thm.attribute_declaration Context_Rules.rule_del th); wenzelm@5885: wenzelm@5885: wenzelm@5841: wenzelm@5885: (** concrete syntax of attributes **) wenzelm@5841: wenzelm@5841: val introN = "intro"; wenzelm@5841: val elimN = "elim"; wenzelm@5841: val destN = "dest"; wenzelm@5841: wenzelm@30528: val setup_attrs = wenzelm@30528: Attrib.setup @{binding swapped} (Scan.succeed swapped) wenzelm@30528: "classical swap of introduction rule" #> wenzelm@33369: Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query) wenzelm@30528: "declaration of Classical destruction rule" #> wenzelm@33369: Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query) wenzelm@30528: "declaration of Classical elimination rule" #> wenzelm@33369: Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query) wenzelm@30528: "declaration of Classical introduction rule" #> wenzelm@30528: Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) wenzelm@30528: "remove declaration of intro/elim/dest rule"; wenzelm@5841: wenzelm@5841: wenzelm@5841: wenzelm@7230: (** proof methods **) wenzelm@7230: wenzelm@7230: local wenzelm@7230: wenzelm@30609: fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => wenzelm@5841: let wenzelm@33369: val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; wenzelm@42793: val {xtra_netpair, ...} = rep_claset_of ctxt; wenzelm@33369: val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair; wenzelm@12376: val rules = rules1 @ rules2 @ rules3 @ rules4; wenzelm@18223: val ruleq = Drule.multi_resolves facts rules; wenzelm@12376: in wenzelm@12376: Method.trace ctxt rules; wenzelm@32952: fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq wenzelm@18834: end) wenzelm@21687: THEN_ALL_NEW Goal.norm_hhf_tac; wenzelm@5841: wenzelm@30609: in wenzelm@7281: wenzelm@30609: fun rule_tac ctxt [] facts = some_rule_tac ctxt facts wenzelm@30609: | rule_tac _ rules facts = Method.rule_tac rules facts; wenzelm@30609: wenzelm@30609: fun default_tac ctxt rules facts = wenzelm@30609: HEADGOAL (rule_tac ctxt rules facts) ORELSE haftmann@26470: Class.default_intro_tac ctxt facts; wenzelm@10309: wenzelm@7230: end; wenzelm@5841: wenzelm@5841: wenzelm@6502: (* automatic methods *) wenzelm@5841: wenzelm@5927: val cla_modifiers = wenzelm@18728: [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier), wenzelm@18728: Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE), wenzelm@18728: Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE), wenzelm@18728: Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE), wenzelm@18728: Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE), wenzelm@18728: Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE), wenzelm@18728: Args.del -- Args.colon >> K (I, rule_del)]; wenzelm@5927: wenzelm@42793: fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac); wenzelm@42793: fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); wenzelm@5841: wenzelm@5841: wenzelm@5841: wenzelm@5841: (** setup_methods **) wenzelm@5841: wenzelm@30541: val setup_methods = wenzelm@30609: Method.setup @{binding default} wenzelm@30609: (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules))) wenzelm@30541: "apply some intro/elim rule (potentially classical)" #> wenzelm@30609: Method.setup @{binding rule} wenzelm@30609: (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) wenzelm@30541: "apply some intro/elim rule (potentially classical)" #> wenzelm@50112: Method.setup @{binding contradiction} wenzelm@50112: (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))) wenzelm@30541: "proof by contradiction" #> wenzelm@30541: Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac)) wenzelm@30541: "repeatedly apply safe steps" #> wenzelm@30541: Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #> wenzelm@30541: Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #> wenzelm@30541: Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #> wenzelm@42798: Method.setup @{binding deepen} wenzelm@42798: (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers wenzelm@42798: >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n))) wenzelm@30541: "classical prover (iterative deepening)" #> wenzelm@30541: Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) wenzelm@50108: "classical prover (apply safe rules)" #> wenzelm@50108: Method.setup @{binding safe_step} (cla_method' safe_step_tac) wenzelm@50108: "single classical step (safe rules)" #> wenzelm@50108: Method.setup @{binding inst_step} (cla_method' inst_step_tac) wenzelm@50108: "single classical step (safe rules, allow instantiations)" #> wenzelm@50108: Method.setup @{binding step} (cla_method' step_tac) wenzelm@50108: "single classical step (safe and unsafe rules)" #> wenzelm@50108: Method.setup @{binding slow_step} (cla_method' slow_step_tac) wenzelm@50108: "single classical step (safe and unsafe rules, allow backtracking)" #> wenzelm@50108: Method.setup @{binding clarify_step} (cla_method' clarify_step_tac) wenzelm@50108: "single classical step (safe rules, without splitting)"; wenzelm@5841: wenzelm@5841: wenzelm@5841: wenzelm@5841: (** theory setup **) wenzelm@5841: wenzelm@26497: val setup = setup_attrs #> setup_methods; wenzelm@5841: wenzelm@5841: wenzelm@8667: wenzelm@8667: (** outer syntax **) wenzelm@8667: wenzelm@24867: val _ = wenzelm@46961: Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner" wenzelm@26497: (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o wenzelm@42439: Toplevel.keep (fn state => wenzelm@42439: let val ctxt = Toplevel.context_of state wenzelm@42793: in print_claset ctxt end))); wenzelm@8667: wenzelm@5841: end;