proper context for "net" tactics;
avoid implicit Tactic.build_net -- make its operational behavior explicit in application;
--- a/src/CTT/CTT.thy Sat Dec 20 19:12:41 2014 +0100
+++ b/src/CTT/CTT.thy Sat Dec 20 22:23:37 2014 +0100
@@ -348,26 +348,34 @@
@{thms elimL_rls} @ @{thms refl_elem}
in
-fun routine_tac rls ctxt prems = ASSUME ctxt (filt_resolve_tac (prems @ rls) 4);
+fun routine_tac rls ctxt prems =
+ ASSUME ctxt (filt_resolve_from_net_tac ctxt 4 (Tactic.build_net (prems @ rls)));
(*Solve all subgoals "A type" using formation rules. *)
-fun form_tac ctxt = REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac @{thms form_rls} 1));
+val form_net = Tactic.build_net @{thms form_rls};
+fun form_tac ctxt =
+ REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 form_net));
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
fun typechk_tac ctxt thms =
- let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
+ let val tac =
+ filt_resolve_from_net_tac ctxt 3
+ (Tactic.build_net (thms @ @{thms form_rls} @ @{thms element_rls}))
in REPEAT_FIRST (ASSUME ctxt tac) end
(*Solve a:A (a flexible, A rigid) by introduction rules.
Cannot use stringtrees (filt_resolve_tac) since
goals like ?a:SUM(A,B) have a trivial head-string *)
fun intr_tac ctxt thms =
- let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
+ let val tac =
+ filt_resolve_from_net_tac ctxt 1
+ (Tactic.build_net (thms @ @{thms form_rls} @ @{thms intr_rls}))
in REPEAT_FIRST (ASSUME ctxt tac) end
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
fun equal_tac ctxt thms =
- REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (thms @ equal_rls) 3))
+ REPEAT_FIRST
+ (ASSUME ctxt (filt_resolve_from_net_tac ctxt 3 (Tactic.build_net (thms @ equal_rls))))
end
*}
@@ -404,8 +412,9 @@
ML {*
(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
Uses other intro rules to avoid changing flexible goals.*)
+val eqintr_net = Tactic.build_net @{thms EqI intr_rls}
fun eqintr_tac ctxt =
- REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
+ REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 eqintr_net))
(** Tactics that instantiate CTT-rules.
Vars in the given terms will be incremented!
--- a/src/HOL/Tools/Meson/meson.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Sat Dec 20 22:23:37 2014 +0100
@@ -502,7 +502,7 @@
then Seq.empty else Seq.single st;
-(* net_resolve_tac actually made it slower... *)
+(* resolve_from_net_tac actually made it slower... *)
fun prolog_step_tac ctxt horns i =
(assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
TRYALL_eq_assume_tac;
@@ -744,7 +744,7 @@
fun prolog_step_tac' ctxt horns =
let val (horn0s, _) = (*0 subgoals vs 1 or more*)
take_prefix Thm.no_prems horns
- val nrtac = net_resolve_tac horns
+ val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns)
in fn i => eq_assume_tac i ORELSE
match_tac ctxt horn0s i ORELSE (*no backtracking if unit MATCHES*)
((assume_tac ctxt i APPEND nrtac i) THEN check_tac)
--- a/src/HOL/Tools/record.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/HOL/Tools/record.ML Sat Dec 20 22:23:37 2014 +0100
@@ -59,7 +59,7 @@
typ * typ -> theory -> (term * term) * theory
val mk_cons_tuple: term * term -> term
val dest_cons_tuple: term -> term * term
- val iso_tuple_intros_tac: int -> tactic
+ val iso_tuple_intros_tac: Proof.context -> int -> tactic
val named_cterm_instantiate: (string * cterm) list -> thm -> thm
end;
@@ -165,8 +165,8 @@
((isom, cons $ isom), thm_thy)
end;
-val iso_tuple_intros_tac =
- resolve_from_net_tac iso_tuple_intros THEN'
+fun iso_tuple_intros_tac ctxt =
+ resolve_from_net_tac ctxt iso_tuple_intros THEN'
CSUBGOAL (fn (cgoal, i) =>
let
val thy = Thm.theory_of_cterm cgoal;
@@ -968,7 +968,7 @@
Goal.prove (Proof_Context.init_global thy) [] [] prop
(fn {context = ctxt, ...} =>
simp_tac (put_simpset defset ctxt) 1 THEN
- REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
+ REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN
TRY (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms id_apply id_o o_id}) 1));
val dest =
if is_sel_upd_pair thy acc upd
@@ -992,7 +992,7 @@
Goal.prove (Proof_Context.init_global thy) [] [] prop
(fn {context = ctxt, ...} =>
simp_tac (put_simpset defset ctxt) 1 THEN
- REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
+ REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN
TRY (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms id_apply}) 1));
val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
in Drule.export_without_context (othm RS dest) end;
@@ -1127,7 +1127,7 @@
Goal.prove (Proof_Context.init_global thy) [] [] prop
(fn {context = ctxt, ...} =>
simp_tac (put_simpset ss ctxt) 1 THEN
- REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
+ REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN
TRY (resolve_tac [updacc_cong_idI] 1))
end;
@@ -1595,7 +1595,7 @@
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
REPEAT_DETERM
(rtac @{thm refl_conj_eq} 1 ORELSE
- Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
+ Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
rtac refl 1))));
@@ -1612,7 +1612,7 @@
val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
val tactic1 =
simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
- REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
+ REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1;
val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
val [halfway] = Seq.list_of (tactic1 start);
val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
@@ -1952,7 +1952,7 @@
val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
val tactic =
simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN
- REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
+ REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac ext_ctxt 1 ORELSE terminal);
val updaccs = Seq.list_of (tactic init_thm);
in
(updaccs RL [updacc_accessor_eqE],
@@ -2137,7 +2137,7 @@
[rtac surject_assist_idE 1,
simp_tac (put_simpset HOL_basic_ss ctxt addsimps ext_defs) 1,
REPEAT
- (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
+ (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1 ORELSE
(rtac surject_assistI 1 THEN
simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt
addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))]));
--- a/src/Provers/classical.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Provers/classical.ML Sat Dec 20 22:23:37 2014 +0100
@@ -234,20 +234,6 @@
dup_netpair : netpair, (*nets for duplication*)
xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
-(*Desired invariants are
- safe0_netpair = build safe0_brls,
- safep_netpair = build safep_brls,
- haz_netpair = build (joinrules(hazIs, hazEs)),
- dup_netpair = build (joinrules(map dup_intr hazIs,
- map dup_elim hazEs))
-
-where build = build_netpair(Net.empty,Net.empty),
- safe0_brls contains all brules that solve the subgoal, and
- safep_brls contains all brules that generate 1 or more new subgoals.
-The theorem lists are largely comments, though they are used in merge_cs and print_cs.
-Nets must be built incrementally, to save space and time.
-*)
-
val empty_netpair = (Net.empty, Net.empty);
val empty_cs =
@@ -712,9 +698,9 @@
(FIRST'
[eq_assume_tac,
eq_mp_tac ctxt,
- bimatch_from_nets_tac safe0_netpair,
+ bimatch_from_nets_tac ctxt safe0_netpair,
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
- bimatch_from_nets_tac safep_netpair])
+ bimatch_from_nets_tac ctxt safep_netpair])
end;
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
@@ -731,15 +717,15 @@
(*version of bimatch_from_nets_tac that only applies rules that
create precisely n subgoals.*)
-fun n_bimatch_from_nets_tac n =
- biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
+fun n_bimatch_from_nets_tac ctxt n =
+ biresolution_from_nets_tac ctxt (order_list o filter (nsubgoalsP n)) true;
fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
(*Two-way branching is allowed only if one of the branches immediately closes*)
fun bimatch2_tac ctxt netpair i =
- n_bimatch_from_nets_tac 2 netpair i THEN
+ n_bimatch_from_nets_tac ctxt 2 netpair i THEN
(eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1));
(*Attack subgoals using safe inferences -- matching, not resolution*)
@@ -748,9 +734,9 @@
appSWrappers ctxt
(FIRST'
[eq_assume_contr_tac ctxt,
- bimatch_from_nets_tac safe0_netpair,
+ bimatch_from_nets_tac ctxt safe0_netpair,
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
- n_bimatch_from_nets_tac 1 safep_netpair,
+ n_bimatch_from_nets_tac ctxt 1 safep_netpair,
bimatch2_tac ctxt safep_netpair])
end;
@@ -764,17 +750,17 @@
fun inst0_step_tac ctxt =
assume_tac ctxt APPEND'
contr_tac ctxt APPEND'
- biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
+ biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt));
(*These unsafe steps could generate more subgoals.*)
fun instp_step_tac ctxt =
- biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
+ biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt));
(*These steps could instantiate variables and are therefore unsafe.*)
fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
fun haz_step_tac ctxt =
- biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
+ biresolve_from_nets_tac ctxt (#haz_netpair (rep_claset_of ctxt));
(*Single step for the prover. FAILS unless it makes progress. *)
fun step_tac ctxt i =
@@ -837,7 +823,7 @@
That's hard to implement and did not perform better in experiments, due to
greater search depth required.*)
fun dup_step_tac ctxt =
- biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
+ biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt));
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
local
--- a/src/Provers/typedsimp.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Provers/typedsimp.ML Sat Dec 20 22:23:37 2014 +0100
@@ -8,7 +8,7 @@
*)
signature TSIMP_DATA =
- sig
+sig
val refl: thm (*Reflexive law*)
val sym: thm (*Symmetric law*)
val trans: thm (*Transitive law*)
@@ -19,23 +19,22 @@
val default_rls: thm list
(*Type checking or similar -- solution of routine conditions*)
val routine_tac: Proof.context -> thm list -> int -> tactic
- end;
+end;
signature TSIMP =
- sig
- val asm_res_tac: Proof.context -> thm list -> int -> tactic
+sig
+ val asm_res_tac: Proof.context -> thm list -> int -> tactic
val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic
val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic
val norm_tac: Proof.context -> (thm list * thm list) -> tactic
val process_rules: thm list -> thm list * thm list
- val rewrite_res_tac: int -> tactic
+ val rewrite_res_tac: Proof.context -> int -> tactic
val split_eqn: thm
val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic
- val subconv_res_tac: thm list -> int -> tactic
- end;
+ val subconv_res_tac: Proof.context -> thm list -> int -> tactic
+end;
-
-functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =
+functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =
struct
local open TSimp_data
in
@@ -72,45 +71,46 @@
fun process_rules rls = fold_rev add_rule rls ([], []);
(*Given list of rewrite rules, return list of both forms, reject others*)
-fun process_rewrites rls =
+fun process_rewrites rls =
case process_rules rls of
(simp_rls,[]) => simp_rls
- | (_,others) => raise THM
+ | (_,others) => raise THM
("process_rewrites: Ill-formed rewrite", 0, others);
(*Process the default rewrite rules*)
val simp_rls = process_rewrites default_rls;
+val simp_net = Tactic.build_net simp_rls;
(*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac
will fail! The filter will pass all the rules, and the bound permits
no ambiguity.*)
(*Resolution with rewrite/sub rules. Builds the tree for filt_resolve_tac.*)
-val rewrite_res_tac = filt_resolve_tac simp_rls 2;
+fun rewrite_res_tac ctxt = filt_resolve_from_net_tac ctxt 2 simp_net;
(*The congruence rules for simplifying subterms. If subgoal is too flexible
then only refl,refl_red will be used (if even them!). *)
-fun subconv_res_tac congr_rls =
- filt_resolve_tac (map subconv_rule congr_rls) 2
- ORELSE' filt_resolve_tac [refl,refl_red] 1;
+fun subconv_res_tac ctxt congr_rls =
+ filt_resolve_from_net_tac ctxt 2 (Tactic.build_net (map subconv_rule congr_rls))
+ ORELSE' filt_resolve_from_net_tac ctxt 1 (Tactic.build_net [refl, refl_red]);
(*Resolve with asms, whether rewrites or not*)
fun asm_res_tac ctxt asms =
- let val (xsimp_rls,xother_rls) = process_rules asms
- in routine_tac ctxt xother_rls ORELSE'
- filt_resolve_tac xsimp_rls 2
+ let val (xsimp_rls, xother_rls) = process_rules asms
+ in routine_tac ctxt xother_rls ORELSE'
+ filt_resolve_from_net_tac ctxt 2 (Tactic.build_net xsimp_rls)
end;
(*Single step for simple rewriting*)
-fun step_tac ctxt (congr_rls,asms) =
- asm_res_tac ctxt asms ORELSE' rewrite_res_tac ORELSE'
- subconv_res_tac congr_rls;
+fun step_tac ctxt (congr_rls, asms) =
+ asm_res_tac ctxt asms ORELSE' rewrite_res_tac ctxt ORELSE'
+ subconv_res_tac ctxt congr_rls;
(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) =
- asm_res_tac ctxt asms ORELSE' rewrite_res_tac ORELSE'
- (resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE'
- subconv_res_tac congr_rls;
+ asm_res_tac ctxt asms ORELSE' rewrite_res_tac ctxt ORELSE'
+ (resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE'
+ subconv_res_tac ctxt congr_rls;
(*Unconditional normalization tactic*)
fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg) THEN
@@ -123,4 +123,3 @@
end;
end;
-
--- a/src/Pure/tactic.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Pure/tactic.ML Sat Dec 20 22:23:37 2014 +0100
@@ -35,19 +35,15 @@
val cut_rules_tac: thm list -> int -> tactic
val cut_facts_tac: thm list -> int -> tactic
val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
- val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
- bool -> 'a Net.net * 'a Net.net -> int -> tactic
- val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
- int -> tactic
- val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
- int -> tactic
- val net_biresolve_tac: (bool * thm) list -> int -> tactic
- val net_bimatch_tac: (bool * thm) list -> int -> tactic
- val filt_resolve_tac: thm list -> int -> int -> tactic
- val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
- val match_from_net_tac: (int * thm) Net.net -> int -> tactic
- val net_resolve_tac: thm list -> int -> tactic
- val net_match_tac: thm list -> int -> tactic
+ val biresolution_from_nets_tac: Proof.context ->
+ ('a list -> (bool * thm) list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic
+ val biresolve_from_nets_tac: Proof.context ->
+ (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
+ val bimatch_from_nets_tac: Proof.context ->
+ (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
+ val filt_resolve_from_net_tac: Proof.context -> int -> (int * thm) Net.net -> int -> tactic
+ val resolve_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
+ val match_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
val subgoals_of_brl: bool * thm -> int
val lessb: (bool * thm) * (bool * thm) -> bool
val rename_tac: string list -> int -> tactic
@@ -63,8 +59,6 @@
val insert_tagged_brl: 'a * (bool * thm) ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
- val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
- (bool * thm) list -> (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
val delete_tagged_brl: bool * thm ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
@@ -219,10 +213,6 @@
| NONE => error "insert_tagged_brl: elimination rule with no premises")
else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
-(*build a pair of nets for biresolution*)
-fun build_netpair netpair brls =
- fold_rev insert_tagged_brl (tag_list 1 brls) netpair;
-
(*delete one kbrl from the pair of nets*)
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
@@ -238,24 +228,19 @@
(*biresolution using a pair of nets rather than rules.
function "order" must sort and possibly filter the list of brls.
boolean "match" indicates matching or unification.*)
-fun biresolution_from_nets_tac order match (inet,enet) =
+fun biresolution_from_nets_tac ctxt order match (inet, enet) =
SUBGOAL
- (fn (prem,i) =>
- let val hyps = Logic.strip_assums_hyp prem
- and concl = Logic.strip_assums_concl prem
- val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
- in PRIMSEQ (Thm.biresolution NONE match (order kbrls) i) end);
+ (fn (prem, i) =>
+ let
+ val hyps = Logic.strip_assums_hyp prem;
+ val concl = Logic.strip_assums_concl prem;
+ val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps;
+ in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order kbrls) i) end);
(*versions taking pre-built nets. No filtering of brls*)
-val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
-val bimatch_from_nets_tac = biresolution_from_nets_tac order_list true;
+fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list false;
+fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list true;
-(*fast versions using nets internally*)
-val net_biresolve_tac =
- biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
-
-val net_bimatch_tac =
- bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
@@ -268,27 +253,23 @@
fold_rev insert_krl (tag_list 1 rls) Net.empty;
(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
-fun filt_resolution_from_net_tac match pred net =
- SUBGOAL (fn (prem,i) =>
+fun filt_resolution_from_net_tac ctxt match pred net =
+ SUBGOAL (fn (prem, i) =>
let val krls = Net.unify_term net (Logic.strip_assums_concl prem) in
if pred krls then
- PRIMSEQ (Thm.biresolution NONE match (map (pair false) (order_list krls)) i)
+ PRIMSEQ (Thm.biresolution (SOME ctxt) match (map (pair false) (order_list krls)) i)
else no_tac
end);
(*Resolve the subgoal using the rules (making a net) unless too flexible,
which means more than maxr rules are unifiable. *)
-fun filt_resolve_tac rules maxr =
- let fun pred krls = length krls <= maxr
- in filt_resolution_from_net_tac false pred (build_net rules) end;
+fun filt_resolve_from_net_tac ctxt maxr net =
+ let fun pred krls = length krls <= maxr
+ in filt_resolution_from_net_tac ctxt false pred net end;
(*versions taking pre-built nets*)
-val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
-val match_from_net_tac = filt_resolution_from_net_tac true (K true);
-
-(*fast versions using nets internally*)
-val net_resolve_tac = resolve_from_net_tac o build_net;
-val net_match_tac = match_from_net_tac o build_net;
+fun resolve_from_net_tac ctxt = filt_resolution_from_net_tac ctxt false (K true);
+fun match_from_net_tac ctxt = filt_resolution_from_net_tac ctxt true (K true);
(*** For Natural Deduction using (bires_flg, rule) pairs ***)
--- a/src/Sequents/modal.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Sequents/modal.ML Sat Dec 20 22:23:37 2014 +0100
@@ -7,22 +7,22 @@
signature MODAL_PROVER_RULE =
sig
- val rewrite_rls : thm list
- val safe_rls : thm list
- val unsafe_rls : thm list
- val bound_rls : thm list
- val aside_rls : thm list
+ val rewrite_rls : thm list
+ val safe_rls : thm list
+ val unsafe_rls : thm list
+ val bound_rls : thm list
+ val aside_rls : thm list
end;
-signature MODAL_PROVER =
+signature MODAL_PROVER =
sig
- val rule_tac : thm list -> int ->tactic
- val step_tac : int -> tactic
- val solven_tac : int -> int -> tactic
- val solve_tac : Proof.context -> int -> tactic
+ val rule_tac : Proof.context -> thm list -> int ->tactic
+ val step_tac : Proof.context -> int -> tactic
+ val solven_tac : Proof.context -> int -> int -> tactic
+ val solve_tac : Proof.context -> int -> tactic
end;
-functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER =
+functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER =
struct
(*Returns the list of all formulas in the sequent*)
@@ -35,7 +35,7 @@
Assumes each formula in seqc is surrounded by sequence variables
-- checks that each concl formula looks like some subgoal formula.*)
fun could_res (seqp,seqc) =
- forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
+ forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
(forms_of_seq seqp))
(forms_of_seq seqc);
@@ -59,11 +59,12 @@
(* NB No back tracking possible with aside rules *)
-fun aside_tac n = DETERM(REPEAT (filt_resolve_tac Modal_Rule.aside_rls 999 n));
-fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
+val aside_net = Tactic.build_net Modal_Rule.aside_rls;
+fun aside_tac ctxt n = DETERM (REPEAT (filt_resolve_from_net_tac ctxt 999 aside_net n));
+fun rule_tac ctxt rls n = fresolve_tac rls n THEN aside_tac ctxt n;
val fres_safe_tac = fresolve_tac Modal_Rule.safe_rls;
-val fres_unsafe_tac = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac;
+fun fres_unsafe_tac ctxt = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac ctxt;
val fres_bound_tac = fresolve_tac Modal_Rule.bound_rls;
fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
@@ -71,18 +72,19 @@
in fn st => tac (nprems_of st) st end;
(* Depth first search bounded by d *)
-fun solven_tac d n state = state |>
- (if d<0 then no_tac
- else if (nprems_of state = 0) then all_tac
- else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
- ((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND
- (fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1)))));
+fun solven_tac ctxt d n st = st |>
+ (if d < 0 then no_tac
+ else if nprems_of st = 0 then all_tac
+ else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac ctxt d)) ORELSE
+ ((fres_unsafe_tac ctxt n THEN UPTOGOAL n (solven_tac ctxt d)) APPEND
+ (fres_bound_tac n THEN UPTOGOAL n (solven_tac ctxt (d - 1)))));
-fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1;
+fun solve_tac ctxt d =
+ rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac ctxt d 1;
-fun step_tac n =
- COND (has_fewer_prems 1) all_tac
- (DETERM(fres_safe_tac n) ORELSE
- (fres_unsafe_tac n APPEND fres_bound_tac n));
+fun step_tac ctxt n =
+ COND (has_fewer_prems 1) all_tac
+ (DETERM(fres_safe_tac n) ORELSE
+ (fres_unsafe_tac ctxt n APPEND fres_bound_tac n));
end;
--- a/src/Tools/intuitionistic.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Tools/intuitionistic.ML Sat Dec 20 22:23:37 2014 +0100
@@ -25,18 +25,18 @@
fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
-val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
+fun bires_tac ctxt = Tactic.biresolution_from_nets_tac ctxt Context_Rules.orderlist;
fun safe_step_tac ctxt =
Context_Rules.Swrap ctxt
(eq_assume_tac ORELSE'
- bires_tac true (Context_Rules.netpair_bang ctxt));
+ bires_tac ctxt true (Context_Rules.netpair_bang ctxt));
fun unsafe_step_tac ctxt =
Context_Rules.wrap ctxt
(assume_tac ctxt APPEND'
- bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
- bires_tac false (Context_Rules.netpair ctxt));
+ bires_tac ctxt false (Context_Rules.netpair_bang ctxt) APPEND'
+ bires_tac ctxt false (Context_Rules.netpair ctxt));
fun step_tac ctxt i =
REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
--- a/src/ZF/Tools/typechk.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/ZF/Tools/typechk.ML Sat Dec 20 22:23:37 2014 +0100
@@ -93,15 +93,15 @@
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac ctxt);
-(*Compiles a term-net for speed*)
-val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl},
- @{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}];
+(*Compile a term-net for speed*)
+val basic_net =
+ Tactic.build_net @{thms TrueI refl reflexive iff_refl ballI allI conjI impI};
(*Instantiates variables in typing conditions.
drawback: does not simplify conjunctions*)
fun type_solver_tac ctxt hyps = SELECT_GOAL
(DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
- ORELSE basic_res_tac 1
+ ORELSE resolve_from_net_tac ctxt basic_net 1
ORELSE (ares_tac hyps 1
APPEND typecheck_step_tac ctxt)));