# HG changeset patch # User oheimb # Date 888418284 -3600 # Node ID 70dd492a1698619920326ead8056ede901782d7b # Parent 91af1ef45d68041c02ceed6aee7bd0f9721a8ac3 changed wrapper mechanism of classical reasoner diff -r 91af1ef45d68 -r 70dd492a1698 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/HOL/Auth/Message.ML Wed Feb 25 15:51:24 1998 +0100 @@ -316,7 +316,7 @@ by (blast_tac (claset() addSEs [add_leE]) 2); (*Nonce case*) by (res_inst_tac [("x","N + Suc nat")] exI 1); -by (fast_tac (claset() addSEs [add_leE] addaltern trans_tac) 1); +by (fast_tac (claset() addSEs [add_leE] addaltern ("trans_tac",trans_tac)) 1); qed "msg_Nonce_supply"; diff -r 91af1ef45d68 -r 70dd492a1698 src/HOL/IMP/Transition.ML --- a/src/HOL/IMP/Transition.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/HOL/IMP/Transition.ML Wed Feb 25 15:51:24 1998 +0100 @@ -200,7 +200,7 @@ "(c,s) -*-> (c',s') ==> -c-> t --> -c-> t"; by (rtac (major RS rtrancl_induct2) 1); by (Fast_tac 1); -by (fast_tac (claset() addIs [FB_lemma3] addbefore split_all_tac) 1); +by (fast_tac (claset() addIs [FB_lemma3]) 1); qed_spec_mp "FB_lemma2"; goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> -c-> t"; diff -r 91af1ef45d68 -r 70dd492a1698 src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/HOL/IOA/Solve.ML Wed Feb 25 15:51:24 1998 +0100 @@ -73,7 +73,7 @@ \ %i. fst (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) by (Simp_tac 1); - by (Fast_tac 1); + by (fast_tac (claset() delWrapper "split_all_tac") 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac (simpset() addsimps [executions_def,is_execution_fragment_def, @@ -93,7 +93,7 @@ \ %i. snd (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) by (Simp_tac 1); - by (Fast_tac 1); + by (fast_tac (claset() delWrapper "split_all_tac") 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac (simpset() addsimps [executions_def,is_execution_fragment_def, diff -r 91af1ef45d68 -r 70dd492a1698 src/HOL/TLA/TLA.ML --- a/src/HOL/TLA/TLA.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/HOL/TLA/TLA.ML Wed Feb 25 15:51:24 1998 +0100 @@ -46,8 +46,8 @@ AddSIs [tempI]; AddDs [tempD]; -val temp_cs = action_cs addSIs [tempI] addDs [tempD]; -val temp_css = (temp_cs,simpset()); +val temp_css = action_css addSIs2 [tempI] addDs2 [tempD]; +val temp_cs = op addss temp_css; (* ========================================================================= *) section "Init"; @@ -340,7 +340,7 @@ (* Make these rewrites active by default *) Addsimps temp_simps; val temp_css = temp_css addsimps2 temp_simps; -val temp_cs = temp_cs addss (empty_ss addsimps temp_simps); +val temp_cs = op addss temp_css; (* ------------------------ Further rewrites ----------------------------------------- *) diff -r 91af1ef45d68 -r 70dd492a1698 src/HOL/TLA/cladata.ML --- a/src/HOL/TLA/cladata.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/HOL/TLA/cladata.ML Wed Feb 25 15:51:24 1998 +0100 @@ -42,10 +42,11 @@ Add the new hyp_subst_tac to the wrapper (also for the default claset). **) -val action_cs = (HOL_cs addSIs [actionI,intI] addSEs [exE_prop] addDs [actionD,intD] - addss simpset()) - addSaltern action_hyp_subst_tac; -val action_css = (action_cs, simpset()); +val action_css = (HOL_cs addSIs [actionI,intI] addSEs [exE_prop] + addDs [actionD,intD] + addSaltern ("action_hyp_subst_tac", action_hyp_subst_tac), + simpset()); +val action_cs = op addss action_css; AddSIs [actionI,intI]; diff -r 91af1ef45d68 -r 70dd492a1698 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/HOL/simpdata.ML Wed Feb 25 15:51:24 1998 +0100 @@ -447,8 +447,9 @@ (*Add a simpset to a classical set!*) infix 4 addSss addss; -fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss)); -fun cs addss ss = cs addbefore asm_full_simp_tac ss; +fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac", + CHANGED o (safe_asm_more_full_simp_tac ss)); +fun cs addss ss = cs addbefore ("asm_full_simp_tac", asm_full_simp_tac ss); fun Addss ss = (claset_ref() := claset() addss ss); @@ -485,7 +486,7 @@ with dup_step_tac when they are combined by auto_tac *) fun nodup_depth_tac cs m i state = SELECT_GOAL - (getWrapper cs + (appWrappers cs (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac (safe_step_tac cs i)) THEN_ELSE (DEPTH_SOLVE (nodup_depth_tac cs m i), diff -r 91af1ef45d68 -r 70dd492a1698 src/Provers/blast.ML --- a/src/Provers/blast.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/Provers/blast.ML Wed Feb 25 15:51:24 1998 +0100 @@ -11,7 +11,8 @@ Blast_tac is often more powerful than fast_tac, but has some limitations. Blast_tac... - * ignores addss, addbefore, addafter; this restriction is intrinsic + * ignores wrappers (addss, addbefore, addafter, addWrapper, ...); + this restriction is intrinsic * ignores elimination rules that don't have the correct format (conclusion must be a formula variable) * ignores types, which can make HOL proofs fail @@ -60,11 +61,11 @@ val dup_intr : thm -> thm val hyp_subst_tac : bool ref -> int -> tactic val claset : unit -> claset - val rep_claset : + val rep_claset : (* dependent on classical.ML *) claset -> {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, - uwrapper: (int -> tactic) -> (int -> tactic), - swrapper: (int -> tactic) -> (int -> tactic), + swrappers: (string * wrapper) list, + uwrappers: (string * wrapper) list, safe0_netpair: netpair, safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair} end; diff -r 91af1ef45d68 -r 70dd492a1698 src/Provers/classical.ML --- a/src/Provers/classical.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/Provers/classical.ML Wed Feb 25 15:51:24 1998 +0100 @@ -16,12 +16,13 @@ (*higher precedence than := facilitates use of references*) infix 4 addSIs addSEs addSDs addIs addEs addDs delrules - setSWrapper compSWrapper setWrapper compWrapper + addSWrapper delSWrapper addWrapper delWrapper addSbefore addSaltern addbefore addaltern; (*should be a type abbreviation in signature CLASSICAL*) type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; +type wrapper = (int -> tactic) -> (int -> tactic); signature CLASET_THY_DATA = sig @@ -48,11 +49,11 @@ val empty_cs: claset val print_cs: claset -> unit val print_claset: theory -> unit - val rep_claset: + val rep_claset: (* BLAST_DATA in blast.ML dependent on this *) claset -> {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, - uwrapper: (int -> tactic) -> (int -> tactic), - swrapper: (int -> tactic) -> (int -> tactic), + swrappers: (string * wrapper) list, + uwrappers: (string * wrapper) list, safe0_netpair: netpair, safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair} val merge_cs : claset * claset -> claset @@ -63,16 +64,16 @@ val addSEs : claset * thm list -> claset val addSIs : claset * thm list -> claset val delrules : claset * thm list -> claset - val setSWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset - val compSWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset - val setWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset - val compWrapper : claset * ((int -> tactic) -> (int -> tactic)) ->claset - val addSbefore : claset * (int -> tactic) -> claset - val addSaltern : claset * (int -> tactic) -> claset - val addbefore : claset * (int -> tactic) -> claset - val addaltern : claset * (int -> tactic) -> claset - val getWrapper : claset -> (int -> tactic) -> (int -> tactic) - val getSWrapper : claset -> (int -> tactic) -> (int -> tactic) + val addSWrapper : claset * (string * wrapper) -> claset + val delSWrapper : claset * string -> claset + val addWrapper : claset * (string * wrapper) -> claset + val delWrapper : claset * string -> claset + val addSbefore : claset * (string * (int -> tactic)) -> claset + val addSaltern : claset * (string * (int -> tactic)) -> claset + val addbefore : claset * (string * (int -> tactic)) -> claset + val addaltern : claset * (string * (int -> tactic)) -> claset + val appWrappers : claset -> wrapper + val appSWrappers : claset -> wrapper val claset_ref_of_sg: Sign.sg -> claset ref val claset_ref_of: theory -> claset ref @@ -218,10 +219,8 @@ safeEs : thm list, (*safe elimination rules*) hazIs : thm list, (*unsafe introduction rules*) hazEs : thm list, (*unsafe elimination rules*) - uwrapper : (int -> tactic) -> - (int -> tactic), (*for transforming step_tac*) - swrapper : (int -> tactic) -> - (int -> tactic), (*for safe_step_tac*) + swrappers : (string * wrapper) list, (*for transf. 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*) @@ -246,8 +245,8 @@ safeEs = [], hazIs = [], hazEs = [], - uwrapper = I, - swrapper = I, + swrappers = [], + uwrappers = [], safe0_netpair = (Net.empty,Net.empty), safep_netpair = (Net.empty,Net.empty), haz_netpair = (Net.empty,Net.empty), @@ -263,11 +262,12 @@ fun rep_claset (CS args) = args; - -fun getWrapper (CS{uwrapper,...}) = uwrapper; - -fun getSWrapper (CS{swrapper,...}) = swrapper; - +local + fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac); +in + fun appSWrappers (CS{swrappers,...}) = calc_wrap swrappers; + fun appWrappers (CS{uwrappers,...}) = calc_wrap uwrappers; +end; (*** Adding (un)safe introduction or elimination rules. @@ -317,7 +317,7 @@ (*** Safe rules ***) -fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, +fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = if mem_thm (th, safeIs) then @@ -335,13 +335,13 @@ safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair} end; -fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, +fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = if mem_thm (th, safeEs) then @@ -359,8 +359,8 @@ safeIs = safeIs, hazIs = hazIs, hazEs = hazEs, - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair} end; @@ -375,7 +375,7 @@ (*** Hazardous (unsafe) rules ***) -fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, +fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th)= if mem_thm (th, hazIs) then @@ -391,13 +391,13 @@ safeIs = safeIs, safeEs = safeEs, hazEs = hazEs, - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair} end; -fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, +fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, th) = if mem_thm (th, hazEs) then @@ -413,8 +413,8 @@ safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair} end; @@ -433,7 +433,7 @@ ***) fun delSI th - (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, + (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = if mem_thm (th, safeIs) then let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] @@ -443,15 +443,15 @@ safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair} end else cs; fun delSE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, + (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = if mem_thm (th, safeEs) then let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] @@ -461,8 +461,8 @@ safeEs = rem_thm (safeEs,th), hazIs = hazIs, hazEs = hazEs, - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, haz_netpair = haz_netpair, dup_netpair = dup_netpair} end @@ -470,7 +470,7 @@ fun delI th - (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, + (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = if mem_thm (th, hazIs) then CS{haz_netpair = delete ([th], []) haz_netpair, @@ -479,14 +479,14 @@ safeEs = safeEs, hazIs = rem_thm (hazIs,th), hazEs = hazEs, - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair} else cs; fun delE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, + (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = if mem_thm (th, hazEs) then CS{haz_netpair = delete ([], [th]) haz_netpair, @@ -495,8 +495,8 @@ safeEs = safeEs, hazIs = hazIs, hazEs = rem_thm (hazEs,th), - uwrapper = uwrapper, - swrapper = swrapper, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair} else cs; @@ -514,49 +514,85 @@ (*** Setting or modifying the wrapper tacticals ***) -(*Set a new uwrapper*) -fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, +(*Add/replace a safe wrapper*) +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) - setWrapper new_uwrapper = + addSWrapper new_swrapper = CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, - uwrapper = new_uwrapper, - swrapper = swrapper, + swrappers = (case assoc_string (swrappers,(fst new_swrapper)) of None =>() + | Some x => warning("overwriting safe wrapper "^fst new_swrapper); + overwrite (swrappers, new_swrapper)), + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair}; + +(*Add/replace an unsafe wrapper*) +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) + addWrapper new_uwrapper = + CS{safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>() + | Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper); + overwrite (uwrappers, new_uwrapper)), safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, haz_netpair = haz_netpair, dup_netpair = dup_netpair}; -(*Set a new swrapper*) -fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, +(*Remove a safe wrapper*) +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) - setSWrapper new_swrapper = + delSWrapper name = CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, - uwrapper = uwrapper, - swrapper = new_swrapper, + swrappers = (case assoc_string (swrappers, name) of None => + warning("safe wrapper "^ name ^" not in claset") | Some x => (); + filter_out (fn (n,f) => n = name) swrappers), + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, haz_netpair = haz_netpair, dup_netpair = dup_netpair}; -(*Compose a tactical with the existing uwrapper*) -fun cs compWrapper uwrapper' = cs setWrapper (uwrapper' o getWrapper cs); - -(*Compose a tactical with the existing swrapper*) -fun cs compSWrapper swrapper' = cs setSWrapper (swrapper' o getSWrapper cs); +(*Remove an unsafe wrapper*) +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) + delWrapper name = + CS{safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = (case assoc_string (uwrappers, name) of None => + warning("unsafe wrapper "^ name ^" not in claset") | Some x => (); + filter_out (fn (n,f) => n = name) uwrappers), + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair}; (*compose a safe tactic sequentially before/alternatively after safe_step_tac*) -fun cs addSbefore tac1 = cs compSWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); -fun cs addSaltern tac2 = cs compSWrapper (fn tac1 => tac1 ORELSE' tac2); +fun cs addSbefore (name,tac1) = cs addSWrapper (name, + fn tac2 => tac1 THEN_MAYBE' tac2); +fun cs addSaltern (name,tac2) = cs addSWrapper (name, + fn tac1 => tac1 ORELSE' tac2); (*compose a tactic sequentially before/alternatively after the step tactic*) -fun cs addbefore tac1 = cs compWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); -fun cs addaltern tac2 = cs compWrapper (fn tac1 => tac1 APPEND' tac2); +fun cs addbefore (name,tac1) = cs addWrapper (name, + fn tac2 => tac1 THEN_MAYBE' tac2); +fun cs addaltern (name,tac2) = cs addWrapper (name, + fn tac1 => tac1 APPEND' tac2); (*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 @@ -579,7 +615,7 @@ (*Attack subgoals using safe inferences -- matching, not resolution*) fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = - getSWrapper cs (FIRST' [ + appSWrappers cs (FIRST' [ eq_assume_tac, eq_mp_tac, bimatch_from_nets_tac safe0_netpair, @@ -610,7 +646,7 @@ (*Attack subgoals using safe inferences -- matching, not resolution*) fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = - getSWrapper cs (FIRST' [ + appSWrappers cs (FIRST' [ eq_assume_contr_tac, bimatch_from_nets_tac safe0_netpair, FIRST' hyp_subst_tacs, @@ -640,12 +676,12 @@ biresolve_from_nets_tac haz_netpair; (*Single step for the prover. FAILS unless it makes progress. *) -fun step_tac cs i = getWrapper cs +fun step_tac cs i = appWrappers cs (K (safe_tac cs) ORELSE' (inst_step_tac cs ORELSE' haz_step_tac cs)) 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 = getWrapper cs +fun slow_step_tac cs i = appWrappers cs (K (safe_tac cs) ORELSE' (inst_step_tac cs APPEND' haz_step_tac cs)) i; (**** The following tactics all fail unless they solve one goal ****) @@ -690,7 +726,7 @@ (*Searching to depth m.*) fun depth_tac cs m i state = SELECT_GOAL - (getWrapper cs + (appWrappers cs (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac (safe_step_tac cs i)) THEN_ELSE (DEPTH_SOLVE (depth_tac cs m i),