diff -r 85fb70b0c5e8 -r 88bee9f6eec7 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri May 13 16:03:03 2011 +0200 +++ b/src/Provers/classical.ML Fri May 13 22:55:00 2011 +0200 @@ -37,30 +37,29 @@ sig type claset val empty_cs: claset - val print_cs: Proof.context -> claset -> unit val rep_cs: claset -> {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, - swrappers: (string * wrapper) list, - uwrappers: (string * wrapper) list, + swrappers: (string * (Proof.context -> wrapper)) list, + uwrappers: (string * (Proof.context -> wrapper)) list, safe0_netpair: netpair, safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair} - val merge_cs: claset * claset -> claset - val addDs: claset * thm list -> claset - val addEs: claset * thm list -> claset - val addIs: claset * thm list -> claset - val addSDs: claset * thm list -> claset - val addSEs: claset * thm list -> claset - val addSIs: claset * thm list -> claset - val delrules: claset * thm list -> claset - val addSWrapper: claset * (string * wrapper) -> claset + val print_claset: Proof.context -> unit + val addDs: Proof.context * thm list -> Proof.context + val addEs: Proof.context * thm list -> Proof.context + val addIs: Proof.context * thm list -> Proof.context + val addSDs: Proof.context * thm list -> Proof.context + val addSEs: Proof.context * thm list -> Proof.context + val addSIs: Proof.context * thm list -> Proof.context + val delrules: Proof.context * thm list -> Proof.context + val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset val delSWrapper: claset * string -> claset - val addWrapper: claset * (string * wrapper) -> claset + val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset val delWrapper: claset * string -> claset val addSbefore: claset * (string * (int -> tactic)) -> claset val addSafter: claset * (string * (int -> tactic)) -> claset @@ -70,54 +69,50 @@ val addE2: claset * (string * thm) -> claset val addSD2: claset * (string * thm) -> claset val addSE2: claset * (string * thm) -> claset - val appSWrappers: claset -> wrapper - val appWrappers: claset -> wrapper + val appSWrappers: Proof.context -> wrapper + val appWrappers: Proof.context -> wrapper val global_claset_of: theory -> claset val claset_of: Proof.context -> claset + val map_claset: (claset -> claset) -> Proof.context -> Proof.context + val put_claset: claset -> Proof.context -> Proof.context - val fast_tac: claset -> int -> tactic - val slow_tac: claset -> int -> tactic - val astar_tac: claset -> int -> tactic - val slow_astar_tac: claset -> int -> tactic - val best_tac: claset -> int -> tactic - val first_best_tac: claset -> int -> tactic - val slow_best_tac: claset -> int -> tactic - val depth_tac: claset -> int -> int -> tactic - val deepen_tac: claset -> int -> int -> tactic + val fast_tac: Proof.context -> int -> tactic + val slow_tac: Proof.context -> int -> tactic + val astar_tac: Proof.context -> int -> tactic + val slow_astar_tac: Proof.context -> int -> tactic + val best_tac: Proof.context -> int -> tactic + val first_best_tac: Proof.context -> int -> tactic + val slow_best_tac: Proof.context -> int -> tactic + val depth_tac: Proof.context -> int -> int -> tactic + val deepen_tac: Proof.context -> int -> int -> tactic val contr_tac: int -> tactic val dup_elim: thm -> thm val dup_intr: thm -> thm - val dup_step_tac: claset -> int -> tactic + val dup_step_tac: Proof.context -> int -> tactic val eq_mp_tac: int -> tactic - val haz_step_tac: claset -> int -> tactic + val haz_step_tac: Proof.context -> int -> tactic val joinrules: thm list * thm list -> (bool * thm) list val mp_tac: int -> tactic - val safe_tac: claset -> tactic - val safe_steps_tac: claset -> int -> tactic - val safe_step_tac: claset -> int -> tactic - val clarify_tac: claset -> int -> tactic - val clarify_step_tac: claset -> int -> tactic - val step_tac: claset -> int -> tactic - val slow_step_tac: claset -> int -> tactic + val safe_tac: Proof.context -> tactic + val safe_steps_tac: Proof.context -> int -> tactic + val safe_step_tac: Proof.context -> int -> tactic + val clarify_tac: Proof.context -> int -> tactic + val clarify_step_tac: Proof.context -> int -> tactic + val step_tac: Proof.context -> int -> tactic + val slow_step_tac: Proof.context -> int -> tactic val swapify: thm list -> thm list val swap_res_tac: thm list -> int -> tactic - val inst_step_tac: claset -> int -> tactic - val inst0_step_tac: claset -> int -> tactic - val instp_step_tac: claset -> int -> tactic + val inst_step_tac: Proof.context -> int -> tactic + val inst0_step_tac: Proof.context -> int -> tactic + val instp_step_tac: Proof.context -> int -> tactic end; signature CLASSICAL = sig include BASIC_CLASSICAL val classical_rule: thm -> thm - val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory - val del_context_safe_wrapper: string -> theory -> theory - val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory - val del_context_unsafe_wrapper: string -> theory -> theory - val get_claset: Proof.context -> claset - val put_claset: claset -> Proof.context -> Proof.context val get_cs: Context.generic -> claset val map_cs: (claset -> claset) -> Context.generic -> Context.generic val safe_dest: int option -> attribute @@ -128,10 +123,10 @@ val haz_intro: int option -> attribute val rule_del: attribute val cla_modifiers: Method.modifier parser list - val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method - val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method - val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser - val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser + val cla_method: + (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser + val cla_method': + (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser val setup: theory -> theory end; @@ -208,7 +203,7 @@ (*Duplication of hazardous rules, for complete provers*) fun dup_intr th = zero_var_indexes (th RS Data.classical); -fun dup_elim th = +fun dup_elim th = (* FIXME proper context!? *) let val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl); @@ -218,17 +213,18 @@ (**** Classical rule sets ****) datatype claset = - CS of {safeIs : thm list, (*safe introduction rules*) - safeEs : thm list, (*safe elimination rules*) - hazIs : thm list, (*unsafe introduction rules*) - hazEs : thm list, (*unsafe elimination rules*) - swrappers : (string * wrapper) list, (*for transforming safe_step_tac*) - uwrappers : (string * wrapper) list, (*for transforming step_tac*) - safe0_netpair : netpair, (*nets for trivial cases*) - safep_netpair : netpair, (*nets for >0 subgoals*) - haz_netpair : netpair, (*nets for unsafe rules*) - dup_netpair : netpair, (*nets for duplication*) - xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*) + CS of + {safeIs : thm list, (*safe introduction rules*) + safeEs : thm list, (*safe elimination rules*) + hazIs : thm list, (*unsafe introduction rules*) + hazEs : thm list, (*unsafe elimination rules*) + swrappers : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*) + uwrappers : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*) + safe0_netpair : netpair, (*nets for trivial cases*) + safep_netpair : netpair, (*nets for >0 subgoals*) + haz_netpair : netpair, (*nets for unsafe rules*) + dup_netpair : netpair, (*nets for duplication*) + xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*) (*Desired invariants are safe0_netpair = build safe0_brls, @@ -247,34 +243,21 @@ val empty_netpair = (Net.empty, Net.empty); val empty_cs = - CS{safeIs = [], - safeEs = [], - hazIs = [], - hazEs = [], - swrappers = [], - uwrappers = [], - safe0_netpair = empty_netpair, - safep_netpair = empty_netpair, - haz_netpair = empty_netpair, - dup_netpair = empty_netpair, - xtra_netpair = empty_netpair}; - -fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) = - let val pretty_thms = map (Display.pretty_thm ctxt) in - [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), - Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), - Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), - Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), - Pretty.strs ("safe wrappers:" :: map #1 swrappers), - Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] - |> Pretty.chunks |> Pretty.writeln - end; + CS + {safeIs = [], + safeEs = [], + hazIs = [], + hazEs = [], + swrappers = [], + uwrappers = [], + safe0_netpair = empty_netpair, + safep_netpair = empty_netpair, + haz_netpair = empty_netpair, + dup_netpair = empty_netpair, + xtra_netpair = empty_netpair}; fun rep_cs (CS args) = args; -fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers; -fun appWrappers (CS {uwrappers, ...}) = fold snd uwrappers; - (*** Adding (un)safe introduction or elimination rules. @@ -314,22 +297,31 @@ val mem_thm = member Thm.eq_thm_prop and rem_thm = remove Thm.eq_thm_prop; -fun warn msg rules th = - mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true); +fun string_of_thm NONE = Display.string_of_thm_without_context + | string_of_thm (SOME context) = + Display.string_of_thm (Context.cases Syntax.init_pretty_global I context); + +fun make_elim context th = + if has_fewer_prems 1 th then + error ("Ill-formed destruction rule\n" ^ string_of_thm context th) + else Tactic.make_elim th; -fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = - warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse - warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse - warn "Rule already declared as introduction (intro)\n" hazIs th orelse - warn "Rule already declared as elimination (elim)\n" hazEs th; +fun warn context msg rules th = + mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true); + +fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = + warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse + warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse + warn context "Rule already declared as introduction (intro)\n" hazIs th orelse + warn context "Rule already declared as elimination (elim)\n" hazEs th; (*** Safe rules ***) -fun addSI w th +fun addSI w context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs + if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs else let val th' = flat_rule th; @@ -337,7 +329,7 @@ List.partition Thm.no_prems [th']; val nI = length safeIs + 1; val nE = length safeEs; - val _ = warn_other th cs; + val _ = warn_other context th cs; in CS {safeIs = th::safeIs, @@ -353,12 +345,12 @@ xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} end; -fun addSE w th +fun addSE w context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs + if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs else if has_fewer_prems 1 th then - error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th) + error ("Ill-formed elimination rule\n" ^ string_of_thm context th) else let val th' = classical_rule (flat_rule th); @@ -366,7 +358,7 @@ List.partition (fn rl => nprems_of rl=1) [th']; val nI = length safeIs; val nE = length safeEs + 1; - val _ = warn_other th cs; + val _ = warn_other context th cs; in CS {safeEs = th::safeEs, @@ -382,19 +374,21 @@ xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} end; +fun addSD w context th = addSE w context (make_elim context th); + (*** Hazardous (unsafe) rules ***) -fun addI w th +fun addI w context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn "Ignoring duplicate introduction (intro)\n" hazIs th then cs + if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs else let val th' = flat_rule th; val nI = length hazIs + 1; val nE = length hazEs; - val _ = warn_other th cs; + val _ = warn_other context th cs; in CS {hazIs = th :: hazIs, @@ -410,20 +404,20 @@ xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} end handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) - error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th); + error ("Ill-formed introduction rule\n" ^ string_of_thm context th); -fun addE w th +fun addE w context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn "Ignoring duplicate elimination (elim)\n" hazEs th then cs + if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs else if has_fewer_prems 1 th then - error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th) + error ("Ill-formed elimination rule\n" ^ string_of_thm context th) else let val th' = classical_rule (flat_rule th); val nI = length hazIs; val nE = length hazEs + 1; - val _ = warn_other th cs; + val _ = warn_other context th cs; in CS {hazEs = th :: hazEs, @@ -439,6 +433,8 @@ xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} end; +fun addD w context th = addE w context (make_elim context th); + (*** Deletion of rules @@ -492,7 +488,7 @@ end else cs; -fun delI th +fun delI context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm hazIs th then @@ -512,7 +508,7 @@ end else cs handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) - error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th); + error ("Ill-formed introduction rule\n" ^ string_of_thm context th); fun delE th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, @@ -535,32 +531,21 @@ else cs; (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) -fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = - let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in +fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = + let val th' = Tactic.make_elim th in if mem_thm safeIs th orelse mem_thm safeEs th orelse mem_thm hazIs th orelse mem_thm hazEs th orelse mem_thm safeEs th' orelse mem_thm hazEs th' - then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) - else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs) + then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs))))) + else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs) end; -fun cs delrules ths = fold delrule ths cs; - -fun make_elim th = - if has_fewer_prems 1 th then - error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th) - else Tactic.make_elim th; + +(** claset data **) -fun cs addSIs ths = fold_rev (addSI NONE) ths cs; -fun cs addSEs ths = fold_rev (addSE NONE) ths cs; -fun cs addSDs ths = cs addSEs (map make_elim ths); -fun cs addIs ths = fold_rev (addI NONE) ths cs; -fun cs addEs ths = fold_rev (addE NONE) ths cs; -fun cs addDs ths = cs addEs (map make_elim ths); +(* wrappers *) - -(*** Modifying the wrapper tacticals ***) fun map_swrappers f (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = @@ -570,48 +555,15 @@ haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; fun map_uwrappers f - (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, swrappers = swrappers, uwrappers = f uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; -fun update_warn msg (p as (key : string, _)) xs = - (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); -fun delete_warn msg (key : string) xs = - if AList.defined (op =) xs key then AList.delete (op =) key xs - else (warning msg; xs); - -(*Add/replace a safe wrapper*) -fun cs addSWrapper new_swrapper = map_swrappers - (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; - -(*Add/replace an unsafe wrapper*) -fun cs addWrapper new_uwrapper = map_uwrappers - (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; - -(*Remove a safe wrapper*) -fun cs delSWrapper name = map_swrappers - (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; - -(*Remove an unsafe wrapper*) -fun cs delWrapper name = map_uwrappers - (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; - -(* compose a safe tactic alternatively before/after safe_step_tac *) -fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); -fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); - -(*compose a tactic alternatively before/after the step tactic *) -fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); -fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); - -fun cs addD2 (name, thm) = cs addafter (name, datac thm 1); -fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1); -fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); -fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); +(* merge_cs *) (*Merge works by adding all new rules of the 2nd claset into the 1st claset. Merging the term nets may look more efficient, but the rather delicate @@ -626,29 +578,129 @@ val safeEs' = fold rem_thm safeEs safeEs2; val hazIs' = fold rem_thm hazIs hazIs2; val hazEs' = fold rem_thm hazEs hazEs2; - val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs'; - val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1; - val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2; - in cs3 end; + in + cs + |> fold_rev (addSI NONE NONE) safeIs' + |> fold_rev (addSE NONE NONE) safeEs' + |> fold_rev (addI NONE NONE) hazIs' + |> fold_rev (addE NONE NONE) hazEs' + |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) + |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) + end; + + +(* data *) + +structure Claset = Generic_Data +( + type T = claset; + val empty = empty_cs; + val extend = I; + val merge = merge_cs; +); + +val global_claset_of = Claset.get o Context.Theory; +val claset_of = Claset.get o Context.Proof; +val rep_claset_of = rep_cs o claset_of; + +val get_cs = Claset.get; +val map_cs = Claset.map; + +fun map_claset f = Context.proof_map (map_cs f); +fun put_claset cs = map_claset (K cs); + +fun print_claset ctxt = + let + val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; + val pretty_thms = map (Display.pretty_thm ctxt); + in + [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), + Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), + Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), + Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), + Pretty.strs ("safe wrappers:" :: map #1 swrappers), + Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] + |> Pretty.chunks |> Pretty.writeln + end; + + +(* old-style declarations *) + +fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt; + +val op addSIs = decl (addSI NONE); +val op addSEs = decl (addSE NONE); +val op addSDs = decl (addSD NONE); +val op addIs = decl (addI NONE); +val op addEs = decl (addE NONE); +val op addDs = decl (addD NONE); +val op delrules = decl delrule; + + + +(*** Modifying the wrapper tacticals ***) + +fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); +fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); + +fun update_warn msg (p as (key : string, _)) xs = + (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); + +fun delete_warn msg (key : string) xs = + if AList.defined (op =) xs key then AList.delete (op =) key xs + else (warning msg; xs); + +(*Add/replace a safe wrapper*) +fun cs addSWrapper new_swrapper = + map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; + +(*Add/replace an unsafe wrapper*) +fun cs addWrapper new_uwrapper = + map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; + +(*Remove a safe wrapper*) +fun cs delSWrapper name = + map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; + +(*Remove an unsafe wrapper*) +fun cs delWrapper name = + map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; + +(* compose a safe tactic alternatively before/after safe_step_tac *) +fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2); +fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2); + +(*compose a tactic alternatively before/after the step tactic *) +fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2); +fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2); + +fun cs addD2 (name, thm) = cs addafter (name, datac thm 1); +fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1); +fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); +fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); + (**** Simple tactics for theorem proving ****) (*Attack subgoals using safe inferences -- matching, not resolution*) -fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) = - appSWrappers cs (FIRST' [ - eq_assume_tac, +fun safe_step_tac ctxt = + let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in + appSWrappers ctxt + (FIRST' + [eq_assume_tac, eq_mp_tac, bimatch_from_nets_tac safe0_netpair, FIRST' Data.hyp_subst_tacs, - bimatch_from_nets_tac safep_netpair]); + bimatch_from_nets_tac safep_netpair]) + end; (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) -fun safe_steps_tac cs = - REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); +fun safe_steps_tac ctxt = + REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i)); (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) -fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs)); +fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt)); (*** Clarify_tac: do safe steps without causing branching ***) @@ -669,86 +721,89 @@ (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1)); (*Attack subgoals using safe inferences -- matching, not resolution*) -fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = - appSWrappers cs (FIRST' [ - eq_assume_contr_tac, +fun clarify_step_tac ctxt = + let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in + appSWrappers ctxt + (FIRST' + [eq_assume_contr_tac, bimatch_from_nets_tac safe0_netpair, FIRST' Data.hyp_subst_tacs, n_bimatch_from_nets_tac 1 safep_netpair, - bimatch2_tac safep_netpair]); + bimatch2_tac safep_netpair]) + end; -fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); +fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1)); (*** Unsafe steps instantiate variables or lose information ***) (*Backtracking is allowed among the various these unsafe ways of proving a subgoal. *) -fun inst0_step_tac (CS {safe0_netpair, ...}) = +fun inst0_step_tac ctxt = assume_tac APPEND' contr_tac APPEND' - biresolve_from_nets_tac safe0_netpair; + biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt)); (*These unsafe steps could generate more subgoals.*) -fun instp_step_tac (CS {safep_netpair, ...}) = - biresolve_from_nets_tac safep_netpair; +fun instp_step_tac ctxt = + biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt)); (*These steps could instantiate variables and are therefore unsafe.*) -fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; +fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; -fun haz_step_tac (CS{haz_netpair,...}) = - biresolve_from_nets_tac haz_netpair; +fun haz_step_tac ctxt = + biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt)); (*Single step for the prover. FAILS unless it makes progress. *) -fun step_tac cs i = - safe_tac cs ORELSE appWrappers cs (inst_step_tac cs ORELSE' haz_step_tac cs) i; +fun step_tac ctxt i = + safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i; (*Using a "safe" rule to instantiate variables is unsafe. This tactic allows backtracking from "safe" rules to "unsafe" rules here.*) -fun slow_step_tac cs i = - safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i; +fun slow_step_tac ctxt i = + safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i; (**** The following tactics all fail unless they solve one goal ****) (*Dumb but fast*) -fun fast_tac cs = - Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); +fun fast_tac ctxt = + Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); (*Slower but smarter than fast_tac*) -fun best_tac cs = +fun best_tac ctxt = Object_Logic.atomize_prems_tac THEN' - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac cs 1)); + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); (*even a bit smarter than best_tac*) -fun first_best_tac cs = +fun first_best_tac ctxt = Object_Logic.atomize_prems_tac THEN' - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac cs))); + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); -fun slow_tac cs = +fun slow_tac ctxt = Object_Logic.atomize_prems_tac THEN' - SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); + SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1)); -fun slow_best_tac cs = +fun slow_best_tac ctxt = Object_Logic.atomize_prems_tac THEN' - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac cs 1)); + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) val weight_ASTAR = 5; -fun astar_tac cs = +fun astar_tac ctxt = Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev) - (step_tac cs 1)); + (step_tac ctxt 1)); -fun slow_astar_tac cs = +fun slow_astar_tac ctxt = Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev) - (slow_step_tac cs 1)); + (slow_step_tac ctxt 1)); (**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome @@ -759,132 +814,44 @@ (*Non-deterministic! Could always expand the first unsafe connective. That's hard to implement and did not perform better in experiments, due to greater search depth required.*) -fun dup_step_tac (CS {dup_netpair, ...}) = - biresolve_from_nets_tac dup_netpair; +fun dup_step_tac ctxt = + biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt)); (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) local - fun slow_step_tac' cs = appWrappers cs (instp_step_tac cs APPEND' dup_step_tac cs); + fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt); in - fun depth_tac cs m i state = SELECT_GOAL - (safe_steps_tac cs 1 THEN_ELSE - (DEPTH_SOLVE (depth_tac cs m 1), - inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac - (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m - 1) 1)))) i state; + fun depth_tac ctxt m i state = SELECT_GOAL + (safe_steps_tac ctxt 1 THEN_ELSE + (DEPTH_SOLVE (depth_tac ctxt m 1), + inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac + (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state; end; (*Search, with depth bound m. This is the "entry point", which does safe inferences first.*) -fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) => - let val deti = - (*No Vars in the goal? No need to backtrack between goals.*) - if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I +fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) => + let + val deti = (*No Vars in the goal? No need to backtrack between goals.*) + if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I; in - SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i + SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i end); -fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs); - - - -(** context dependent claset components **) - -datatype context_cs = ContextCS of - {swrappers: (string * (Proof.context -> wrapper)) list, - uwrappers: (string * (Proof.context -> wrapper)) list}; - -fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) = - let - fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt)); - in - cs - |> fold_rev (add_wrapper (op addSWrapper)) swrappers - |> fold_rev (add_wrapper (op addWrapper)) uwrappers - end; - -fun make_context_cs (swrappers, uwrappers) = - ContextCS {swrappers = swrappers, uwrappers = uwrappers}; - -val empty_context_cs = make_context_cs ([], []); - -fun merge_context_cs (ctxt_cs1, ctxt_cs2) = - if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1 - else - let - val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1; - val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2; - val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2); - val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2); - in make_context_cs (swrappers', uwrappers') end; - - - -(** claset data **) - -(* global clasets *) - -structure GlobalClaset = Theory_Data -( - type T = claset * context_cs; - val empty = (empty_cs, empty_context_cs); - val extend = I; - fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) = - (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2)); -); - -val get_global_claset = #1 o GlobalClaset.get; -val map_global_claset = GlobalClaset.map o apfst; - -val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of; -fun map_context_cs f = GlobalClaset.map (apsnd - (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers)))); - -fun global_claset_of thy = - let val (cs, ctxt_cs) = GlobalClaset.get thy - in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end; - - -(* context dependent components *) - -fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper))); -fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name))); - -fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper))); -fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name))); - - -(* local clasets *) - -structure LocalClaset = Proof_Data -( - type T = claset; - val init = get_global_claset; -); - -val get_claset = LocalClaset.get; -val put_claset = LocalClaset.put; - -fun claset_of ctxt = - context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt); - - -(* generic clasets *) - -val get_cs = Context.cases global_claset_of claset_of; -fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f); +fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); (* attributes *) -fun attrib f = Thm.declaration_attribute (fn th => - Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th))); +fun attrib f = + Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context); -fun safe_dest w = attrib (addSE w o make_elim); val safe_elim = attrib o addSE; val safe_intro = attrib o addSI; -fun haz_dest w = attrib (addE w o make_elim); +val safe_dest = attrib o addSD; val haz_elim = attrib o addE; val haz_intro = attrib o addI; +val haz_dest = attrib o addD; val rule_del = attrib delrule o Context_Rules.rule_del; @@ -916,7 +883,7 @@ fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => let val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; - val CS {xtra_netpair, ...} = claset_of ctxt; + val {xtra_netpair, ...} = rep_claset_of ctxt; val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair; val rules = rules1 @ rules2 @ rules3 @ rules4; val ruleq = Drule.multi_resolves facts rules; @@ -954,14 +921,8 @@ Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE), Args.del -- Args.colon >> K (I, rule_del)]; -fun cla_meth tac ctxt = METHOD (fn facts => - ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt)); - -fun cla_meth' tac ctxt = METHOD (fn facts => - HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt))); - -fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac); -fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac); +fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac); +fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); @@ -981,7 +942,7 @@ Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #> Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #> Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #> - Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4)) + Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4)) "classical prover (iterative deepening)" #> Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) "classical prover (apply safe rules)"; @@ -1002,6 +963,6 @@ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state - in print_cs ctxt (claset_of ctxt) end))); + in print_claset ctxt end))); end;