# HG changeset patch # User wenzelm # Date 1419110617 -3600 # Node ID ff40c53d1af99f25eb2687f86e6403ad7f595a4a # Parent 857a600f0c94555a01beb41314780bd54ed3b0be proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application; diff -r 857a600f0c94 -r ff40c53d1af9 src/CTT/CTT.thy --- 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! diff -r 857a600f0c94 -r ff40c53d1af9 src/HOL/Tools/Meson/meson.ML --- 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) diff -r 857a600f0c94 -r ff40c53d1af9 src/HOL/Tools/record.ML --- 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))])); diff -r 857a600f0c94 -r ff40c53d1af9 src/Provers/classical.ML --- 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 diff -r 857a600f0c94 -r ff40c53d1af9 src/Provers/typedsimp.ML --- 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; - diff -r 857a600f0c94 -r ff40c53d1af9 src/Pure/tactic.ML --- 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 ***) diff -r 857a600f0c94 -r ff40c53d1af9 src/Sequents/modal.ML --- 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 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; diff -r 857a600f0c94 -r ff40c53d1af9 src/Tools/intuitionistic.ML --- 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 diff -r 857a600f0c94 -r ff40c53d1af9 src/ZF/Tools/typechk.ML --- 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)));