1.1 --- a/doc-src/IsarRef/Thy/Generic.thy Mon Jun 16 17:56:08 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Mon Jun 16 22:13:39 2008 +0200
1.3 @@ -308,7 +308,7 @@
1.4
1.5 \item [@{method rule_tac} etc.] do resolution of rules with explicit
1.6 instantiation. This works the same way as the ML tactics @{ML
1.7 - Tactic.res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
1.8 + res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
1.9
1.10 Multiple rules may be only given if there is no instantiation; then
1.11 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
1.12 @@ -323,12 +323,12 @@
1.13
1.14 \item [@{method thin_tac}~@{text \<phi>}] deletes the specified
1.15 assumption from a subgoal; note that @{text \<phi>} may contain schematic
1.16 - variables. See also @{ML Tactic.thin_tac} in
1.17 + variables. See also @{ML thin_tac} in
1.18 \cite[\S3]{isabelle-ref}.
1.19
1.20 \item [@{method subgoal_tac}~@{text \<phi>}] adds @{text \<phi>} as an
1.21 - assumption to a subgoal. See also @{ML Tactic.subgoal_tac} and @{ML
1.22 - Tactic.subgoals_tac} in \cite[\S3]{isabelle-ref}.
1.23 + assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
1.24 + subgoals_tac} in \cite[\S3]{isabelle-ref}.
1.25
1.26 \item [@{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"}] renames
1.27 parameters of a goal according to the list @{text "x\<^sub>1, \<dots>,
2.1 --- a/doc-src/IsarRef/Thy/ML_Tactic.thy Mon Jun 16 17:56:08 2008 +0200
2.2 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Mon Jun 16 22:13:39 2008 +0200
2.3 @@ -41,7 +41,7 @@
2.4 @{ML forward_tac}).
2.5
2.6 \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
2.7 - @{ML RuleInsts.res_inst_tac}).
2.8 + @{ML res_inst_tac}).
2.9
2.10 \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
2.11 vs.\ @{ML rtac}).
2.12 @@ -66,11 +66,11 @@
2.13 \begin{tabular}{lll}
2.14 @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
2.15 @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
2.16 - @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
2.17 + @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
2.18 @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
2.19 @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
2.20 @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
2.21 - @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
2.22 + @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
2.23 @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
2.24 \end{tabular}
2.25 \medskip
3.1 --- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 17:56:08 2008 +0200
3.2 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 22:13:39 2008 +0200
3.3 @@ -864,7 +864,7 @@
3.4 (EVERY
3.5 [ (*push in occurrences of X...*)
3.6 (REPEAT o CHANGED)
3.7 - (RuleInsts.res_inst_tac (Simplifier.the_context ss)
3.8 + (res_inst_tac (Simplifier.the_context ss)
3.9 [(("x", 1), "X")] (insert_commute RS ssubst) 1),
3.10 (*...allowing further simplifications*)
3.11 simp_tac ss 1,
4.1 --- a/src/CCL/CCL.thy Mon Jun 16 17:56:08 2008 +0200
4.2 +++ b/src/CCL/CCL.thy Mon Jun 16 22:13:39 2008 +0200
4.3 @@ -415,7 +415,7 @@
4.4
4.5 ML {*
4.6 fun po_coinduct_tac ctxt s i =
4.7 - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
4.8 + res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
4.9 *}
4.10
4.11
4.12 @@ -460,11 +460,8 @@
4.13 done
4.14
4.15 ML {*
4.16 - fun eq_coinduct_tac ctxt s i =
4.17 - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
4.18 -
4.19 - fun eq_coinduct3_tac ctxt s i =
4.20 - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
4.21 + fun eq_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
4.22 + fun eq_coinduct3_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
4.23 *}
4.24
4.25
5.1 --- a/src/CCL/Hered.thy Mon Jun 16 17:56:08 2008 +0200
5.2 +++ b/src/CCL/Hered.thy Mon Jun 16 22:13:39 2008 +0200
5.3 @@ -97,8 +97,7 @@
5.4 done
5.5
5.6 ML {*
5.7 - fun HTT_coinduct_tac ctxt s i =
5.8 - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
5.9 + fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
5.10 *}
5.11
5.12 lemma HTT_coinduct3:
5.13 @@ -111,7 +110,7 @@
5.14 val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
5.15
5.16 fun HTT_coinduct3_tac ctxt s i =
5.17 - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
5.18 + res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
5.19
5.20 val HTTgenIs =
5.21 map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
6.1 --- a/src/CCL/Wfd.thy Mon Jun 16 17:56:08 2008 +0200
6.2 +++ b/src/CCL/Wfd.thy Mon Jun 16 22:13:39 2008 +0200
6.3 @@ -55,7 +55,7 @@
6.4
6.5 ML {*
6.6 fun wfd_strengthen_tac ctxt s i =
6.7 - RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
6.8 + res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
6.9 *}
6.10
6.11 lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P"
6.12 @@ -456,7 +456,7 @@
6.13 in
6.14
6.15 fun rcall_tac ctxt i =
6.16 - let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i
6.17 + let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i
6.18 in IHinst tac @{thms rcallTs} i end
6.19 THEN eresolve_tac @{thms rcall_lemmas} i
6.20
6.21 @@ -478,7 +478,7 @@
6.22 hyp_subst_tac)
6.23
6.24 fun clean_ccs_tac ctxt =
6.25 - let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in
6.26 + let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
6.27 TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
6.28 eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
6.29 hyp_subst_tac))
7.1 --- a/src/CTT/CTT.thy Mon Jun 16 17:56:08 2008 +0200
7.2 +++ b/src/CTT/CTT.thy Mon Jun 16 22:13:39 2008 +0200
7.3 @@ -417,13 +417,13 @@
7.4 The (rtac EqE i) lets them apply to equality judgements. **)
7.5
7.6 fun NE_tac ctxt sp i =
7.7 - TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
7.8 + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
7.9
7.10 fun SumE_tac ctxt sp i =
7.11 - TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
7.12 + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
7.13
7.14 fun PlusE_tac ctxt sp i =
7.15 - TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
7.16 + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
7.17
7.18 (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
7.19
8.1 --- a/src/FOL/FOL.thy Mon Jun 16 17:56:08 2008 +0200
8.2 +++ b/src/FOL/FOL.thy Mon Jun 16 22:13:39 2008 +0200
8.3 @@ -70,8 +70,7 @@
8.4 done
8.5
8.6 ML {*
8.7 - fun case_tac ctxt a =
8.8 - RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
8.9 + fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
8.10 *}
8.11
8.12 method_setup case_tac =
9.1 --- a/src/HOL/Auth/Message.thy Mon Jun 16 17:56:08 2008 +0200
9.2 +++ b/src/HOL/Auth/Message.thy Mon Jun 16 22:13:39 2008 +0200
9.3 @@ -884,8 +884,7 @@
9.4 (EVERY
9.5 [ (*push in occurrences of X...*)
9.6 (REPEAT o CHANGED)
9.7 - (RuleInsts.res_inst_tac (Simplifier.the_context ss)
9.8 - [(("x", 1), "X")] (insert_commute RS ssubst) 1),
9.9 + (res_inst_tac (Simplifier.the_context ss) [(("x", 1), "X")] (insert_commute RS ssubst) 1),
9.10 (*...allowing further simplifications*)
9.11 simp_tac ss 1,
9.12 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
10.1 --- a/src/HOL/Bali/Basis.thy Mon Jun 16 17:56:08 2008 +0200
10.2 +++ b/src/HOL/Bali/Basis.thy Mon Jun 16 22:13:39 2008 +0200
10.3 @@ -230,7 +230,7 @@
10.4 ML {*
10.5 fun sum3_instantiate ctxt thm = map (fn s =>
10.6 simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
10.7 - (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
10.8 + (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
10.9 *}
10.10 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
10.11
11.1 --- a/src/HOL/Bali/WellType.thy Mon Jun 16 17:56:08 2008 +0200
11.2 +++ b/src/HOL/Bali/WellType.thy Mon Jun 16 22:13:39 2008 +0200
11.3 @@ -653,10 +653,11 @@
11.4 apply (safe del: disjE)
11.5 (* 17 subgoals *)
11.6 apply (tactic {* ALLGOALS (fn i =>
11.7 - if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
11.8 - RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
11.9 - RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
11.10 - else RuleInsts.thin_tac @{context} "All ?P" i) *})
11.11 + if i = 11 then EVERY'
11.12 + [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
11.13 + thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
11.14 + thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
11.15 + else thin_tac @{context} "All ?P" i) *})
11.16 (*apply (safe del: disjE elim!: wt_elim_cases)*)
11.17 apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
11.18 apply (simp_all (no_asm_use) split del: split_if_asm)
12.1 --- a/src/HOL/Hyperreal/MacLaurin.thy Mon Jun 16 17:56:08 2008 +0200
12.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy Mon Jun 16 22:13:39 2008 +0200
12.3 @@ -50,7 +50,7 @@
12.4
12.5 fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
12.6 resolve_tac @{thms deriv_rulesI} i ORELSE
12.7 - ((rtac (RuleInsts.read_instantiate ctxt [(("f", 0), get_fun_name prem)]
12.8 + ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
12.9 @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
12.10
12.11 fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
13.1 --- a/src/HOL/IMPP/Hoare.thy Mon Jun 16 17:56:08 2008 +0200
13.2 +++ b/src/HOL/IMPP/Hoare.thy Mon Jun 16 22:13:39 2008 +0200
13.3 @@ -283,7 +283,7 @@
13.4 apply (blast) (* cut *)
13.5 apply (blast) (* weaken *)
13.6 apply (tactic {* ALLGOALS (EVERY'
13.7 - [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y",
13.8 + [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
13.9 simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
13.10 apply (simp_all (no_asm_use) add: triple_valid_def2)
13.11 apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
14.1 --- a/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 17:56:08 2008 +0200
14.2 +++ b/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 22:13:39 2008 +0200
14.3 @@ -108,8 +108,8 @@
14.4 apply (rule hoare_ehoare.induct)
14.5 (*18*)
14.6 apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
14.7 -apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *})
14.8 -apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *})
14.9 +apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *})
14.10 +apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *})
14.11 apply (simp_all only: cnvalid1_eq cenvalid_def2)
14.12 apply fast
14.13 apply fast
15.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Jun 16 17:56:08 2008 +0200
15.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Jun 16 22:13:39 2008 +0200
15.3 @@ -54,7 +54,7 @@
15.4 gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
15.5
15.6 fun cut_inst_tac_term' tinst th =
15.7 - res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
15.8 + res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
15.9
15.10 fun get_dyn_thm thy name atom_name =
15.11 PureThy.get_thm thy name handle ERROR _ =>
16.1 --- a/src/HOL/Prolog/prolog.ML Mon Jun 16 17:56:08 2008 +0200
16.2 +++ b/src/HOL/Prolog/prolog.ML Mon Jun 16 22:13:39 2008 +0200
16.3 @@ -53,7 +53,7 @@
16.4 fun atomizeD ctxt thm = let
16.5 fun at thm = case concl_of thm of
16.6 _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
16.7 - (RuleInsts.read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
16.8 + (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
16.9 | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
16.10 | _$(Const("op -->",_)$_$_) => at(thm RS mp)
16.11 | _ => [thm]
17.1 --- a/src/HOL/Real/rat_arith.ML Mon Jun 16 17:56:08 2008 +0200
17.2 +++ b/src/HOL/Real/rat_arith.ML Mon Jun 16 22:13:39 2008 +0200
17.3 @@ -14,7 +14,7 @@
17.4
17.5 val simps =
17.6 [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
17.7 - RuleInsts.read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
17.8 + read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
17.9 @{thm divide_1}, @{thm divide_zero_left},
17.10 @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
17.11 @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
18.1 --- a/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 17:56:08 2008 +0200
18.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 22:13:39 2008 +0200
18.3 @@ -880,7 +880,7 @@
18.4 (EVERY
18.5 [ (*push in occurrences of X...*)
18.6 (REPEAT o CHANGED)
18.7 - (RuleInsts.res_inst_tac (Simplifier.the_context ss)
18.8 + (res_inst_tac (Simplifier.the_context ss)
18.9 [(("x", 1), "X")] (insert_commute RS ssubst) 1),
18.10 (*...allowing further simplifications*)
18.11 simp_tac ss 1,
19.1 --- a/src/HOL/TLA/TLA.thy Mon Jun 16 17:56:08 2008 +0200
19.2 +++ b/src/HOL/TLA/TLA.thy Mon Jun 16 22:13:39 2008 +0200
19.3 @@ -307,15 +307,15 @@
19.4
19.5 fun merge_temp_box_tac ctxt i =
19.6 REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
19.7 - RuleInsts.eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
19.8 + eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
19.9
19.10 fun merge_stp_box_tac ctxt i =
19.11 REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
19.12 - RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
19.13 + eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
19.14
19.15 fun merge_act_box_tac ctxt i =
19.16 REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
19.17 - RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
19.18 + eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
19.19 *}
19.20
19.21 (* rewrite rule to push universal quantification through box:
20.1 --- a/src/HOL/Tools/TFL/post.ML Mon Jun 16 17:56:08 2008 +0200
20.2 +++ b/src/HOL/Tools/TFL/post.ML Mon Jun 16 22:13:39 2008 +0200
20.3 @@ -152,7 +152,7 @@
20.4 rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
20.5
20.6 (*Strip off the outer !P*)
20.7 -val spec'= RuleInsts.read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
20.8 +val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
20.9
20.10 fun tracing true _ = ()
20.11 | tracing false msg = writeln msg;
21.1 --- a/src/HOL/Tools/induct_tacs.ML Mon Jun 16 17:56:08 2008 +0200
21.2 +++ b/src/HOL/Tools/induct_tacs.ML Mon Jun 16 22:13:39 2008 +0200
21.3 @@ -44,7 +44,7 @@
21.4 (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
21.5 Var (xi, _) :: _ => xi
21.6 | _ => raise THM ("Malformed cases rule", 0, [rule]));
21.7 - in RuleInsts.res_inst_tac ctxt [(xi, s)] rule i st end
21.8 + in res_inst_tac ctxt [(xi, s)] rule i st end
21.9 handle THM _ => Seq.empty;
21.10
21.11 fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
21.12 @@ -100,7 +100,7 @@
21.13 val concls = HOLogic.dest_concls (Thm.concl_of rule);
21.14 val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
21.15 error "Induction rule has different numbers of variables";
21.16 - in RuleInsts.res_inst_tac ctxt insts rule i st end
21.17 + in res_inst_tac ctxt insts rule i st end
21.18 handle THM _ => Seq.empty;
21.19
21.20 end;
22.1 --- a/src/HOL/Tools/meson.ML Mon Jun 16 17:56:08 2008 +0200
22.2 +++ b/src/HOL/Tools/meson.ML Mon Jun 16 22:13:39 2008 +0200
22.3 @@ -646,7 +646,7 @@
22.4 (*Rules to convert the head literal into a negated assumption. If the head
22.5 literal is already negated, then using notEfalse instead of notEfalse'
22.6 prevents a double negation.*)
22.7 -val notEfalse = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE;
22.8 +val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
22.9 val notEfalse' = rotate_prems 1 notEfalse;
22.10
22.11 fun negated_asm_of_head th =
23.1 --- a/src/HOL/Tools/metis_tools.ML Mon Jun 16 17:56:08 2008 +0200
23.2 +++ b/src/HOL/Tools/metis_tools.ML Mon Jun 16 22:13:39 2008 +0200
23.3 @@ -24,10 +24,10 @@
23.4 (* ------------------------------------------------------------------------- *)
23.5 (* Useful Theorems *)
23.6 (* ------------------------------------------------------------------------- *)
23.7 - val EXCLUDED_MIDDLE = rotate_prems 1 (RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE);
23.8 + val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
23.9 val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*)
23.10 val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
23.11 - val ssubst_em = RuleInsts.read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
23.12 + val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
23.13
23.14 (* ------------------------------------------------------------------------- *)
23.15 (* Useful Functions *)
24.1 --- a/src/HOL/Tools/record_package.ML Mon Jun 16 17:56:08 2008 +0200
24.2 +++ b/src/HOL/Tools/record_package.ML Mon Jun 16 22:13:39 2008 +0200
24.3 @@ -2155,8 +2155,8 @@
24.4
24.5 fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} =>
24.6 fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
24.7 - st |> (RuleInsts.res_inst_tac context [((rN, 0), s)] cases_scheme 1
24.8 - THEN RuleInsts.res_inst_tac context [((rN, 0), s')] cases_scheme 1
24.9 + st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
24.10 + THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
24.11 THEN (METAHYPS equality_tac 1))
24.12 (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
24.13 end);
25.1 --- a/src/HOL/Tools/split_rule.ML Mon Jun 16 17:56:08 2008 +0200
25.2 +++ b/src/HOL/Tools/split_rule.ML Mon Jun 16 22:13:39 2008 +0200
25.3 @@ -124,7 +124,7 @@
25.4
25.5
25.6 fun pair_tac ctxt s =
25.7 - RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
25.8 + res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
25.9 THEN' hyp_subst_tac
25.10 THEN' K prune_params_tac;
25.11
26.1 --- a/src/HOL/UNITY/UNITY_tactics.ML Mon Jun 16 17:56:08 2008 +0200
26.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Jun 16 22:13:39 2008 +0200
26.3 @@ -41,9 +41,9 @@
26.4 @{thm EnsuresI}, @{thm ensuresI}] 1),
26.5 (*now there are two subgoals: co & transient*)
26.6 simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
26.7 - RuleInsts.res_inst_tac (Simplifier.the_context ss)
26.8 + res_inst_tac (Simplifier.the_context ss)
26.9 [(("act", 0), sact)] @{thm totalize_transientI} 2
26.10 - ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
26.11 + ORELSE res_inst_tac (Simplifier.the_context ss)
26.12 [(("act", 0), sact)] @{thm transientI} 2,
26.13 (*simplify the command's domain*)
26.14 simp_tac (ss addsimps [@{thm Domain_def}]) 3,
27.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Jun 16 17:56:08 2008 +0200
27.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Jun 16 22:13:39 2008 +0200
27.3 @@ -1089,7 +1089,7 @@
27.4 ML {*
27.5
27.6 fun Seq_case_tac ctxt s i =
27.7 - RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
27.8 + res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
27.9 THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
27.10
27.11 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
27.12 @@ -1104,7 +1104,7 @@
27.13 (* rws are definitions to be unfolded for admissibility check *)
27.14 fun Seq_induct_tac ctxt s rws i =
27.15 let val ss = Simplifier.local_simpset_of ctxt in
27.16 - RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
27.17 + res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
27.18 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
27.19 THEN simp_tac (ss addsimps rws) i
27.20 end;
27.21 @@ -1114,13 +1114,13 @@
27.22 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
27.23
27.24 fun pair_tac ctxt s =
27.25 - RuleInsts.res_inst_tac ctxt [(("p", 0), s)] PairE
27.26 + res_inst_tac ctxt [(("p", 0), s)] PairE
27.27 THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
27.28
27.29 (* induction on a sequence of pairs with pairsplitting and simplification *)
27.30 fun pair_induct_tac ctxt s rws i =
27.31 let val ss = Simplifier.local_simpset_of ctxt in
27.32 - RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
27.33 + res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
27.34 THEN pair_tac ctxt "a" (i+3)
27.35 THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
27.36 THEN simp_tac (ss addsimps rws) i
28.1 --- a/src/HOLCF/Tools/domain/domain_library.ML Mon Jun 16 17:56:08 2008 +0200
28.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML Mon Jun 16 22:13:39 2008 +0200
28.3 @@ -24,7 +24,7 @@
28.4 fun upd_second f (x,y,z) = ( x, f y, z);
28.5 fun upd_third f (x,y,z) = ( x, y, f z);
28.6
28.7 -fun atomize ctxt thm = let val r_inst = RuleInsts.read_instantiate ctxt;
28.8 +fun atomize ctxt thm = let val r_inst = read_instantiate ctxt;
28.9 fun at thm = case concl_of thm of
28.10 _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
28.11 | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
29.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 17:56:08 2008 +0200
29.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 22:13:39 2008 +0200
29.3 @@ -376,7 +376,7 @@
29.4 val goal = lift_defined %: (nonlazy args, concl);
29.5 fun tacs ctxt = [
29.6 rtac @{thm rev_contrapos} 1,
29.7 - RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
29.8 + eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
29.9 asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
29.10 in pg [] goal tacs end;
29.11 in
29.12 @@ -477,7 +477,7 @@
29.13 mk_trp (con_app con1 args1 ~<< con_app con2 args2));
29.14 fun tacs ctxt = [
29.15 rtac @{thm rev_contrapos} 1,
29.16 - RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
29.17 + eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
29.18 @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
29.19 @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
29.20 in pg [] goal tacs end;
29.21 @@ -709,7 +709,7 @@
29.22 mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
29.23 val take_ss = HOL_ss addsimps take_rews;
29.24 fun quant_tac ctxt i = EVERY
29.25 - (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
29.26 + (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
29.27
29.28 fun ind_prems_tac prems = EVERY
29.29 (maps (fn cons =>
29.30 @@ -766,7 +766,7 @@
29.31 map (K (atac 1)) (nonlazy args) @
29.32 map (K (etac spec 1)) (List.filter is_rec args);
29.33 fun cases_tacs (cons, cases) =
29.34 - RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 ::
29.35 + res_inst_tac context [(("x", 0), "x")] cases 1 ::
29.36 asm_simp_tac (take_ss addsimps prems) 1 ::
29.37 maps con_tacs cons;
29.38 in
29.39 @@ -783,8 +783,8 @@
29.40 val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
29.41 val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
29.42 fun tacf {prems, context} = [
29.43 - RuleInsts.res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
29.44 - RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
29.45 + res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
29.46 + res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
29.47 stac fix_def2 1,
29.48 REPEAT (CHANGED
29.49 (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
29.50 @@ -833,7 +833,7 @@
29.51 val goal =
29.52 mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
29.53 fun arg_tacs ctxt vn = [
29.54 - RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
29.55 + eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
29.56 etac disjE 1,
29.57 asm_simp_tac (HOL_ss addsimps con_rews) 1,
29.58 asm_simp_tac take_ss 1];
29.59 @@ -843,7 +843,7 @@
29.60 fun foo_tacs ctxt n (cons, cases) =
29.61 simp_tac take_ss 1 ::
29.62 rtac allI 1 ::
29.63 - RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
29.64 + res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
29.65 asm_simp_tac take_ss 1 ::
29.66 maps (con_tacs ctxt) cons;
29.67 fun tacs ctxt =
29.68 @@ -887,8 +887,7 @@
29.69 else (* infinite case *)
29.70 let
29.71 fun one_finite n dn =
29.72 - RuleInsts.read_instantiate global_ctxt
29.73 - [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
29.74 + read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
29.75 val finites = mapn one_finite 1 dnames;
29.76
29.77 val goal =
29.78 @@ -936,7 +935,7 @@
29.79 fun x_tacs ctxt n x = [
29.80 rotate_tac (n+1) 1,
29.81 etac all2E 1,
29.82 - RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
29.83 + eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
29.84 TRY (safe_tac HOL_cs),
29.85 REPEAT (CHANGED (asm_simp_tac take_ss 1))];
29.86 fun tacs ctxt = [
30.1 --- a/src/LCF/LCF.thy Mon Jun 16 17:56:08 2008 +0200
30.2 +++ b/src/LCF/LCF.thy Mon Jun 16 22:13:39 2008 +0200
30.3 @@ -317,7 +317,7 @@
30.4
30.5 ML {*
30.6 fun induct_tac ctxt v i =
30.7 - RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
30.8 + res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
30.9 REPEAT (resolve_tac @{thms adm_lemmas} i)
30.10 *}
30.11
30.12 @@ -376,7 +376,7 @@
30.13
30.14 ML {*
30.15 fun induct2_tac ctxt (f, g) i =
30.16 - RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
30.17 + res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
30.18 REPEAT(resolve_tac @{thms adm_lemmas} i)
30.19 *}
30.20
31.1 --- a/src/Sequents/LK0.thy Mon Jun 16 17:56:08 2008 +0200
31.2 +++ b/src/Sequents/LK0.thy Mon Jun 16 22:13:39 2008 +0200
31.3 @@ -157,11 +157,11 @@
31.4 ML {*
31.5 (*Cut and thin, replacing the right-side formula*)
31.6 fun cutR_tac ctxt s i =
31.7 - RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
31.8 + res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
31.9
31.10 (*Cut and thin, replacing the left-side formula*)
31.11 fun cutL_tac ctxt s i =
31.12 - RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
31.13 + res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
31.14 *}
31.15
31.16
32.1 --- a/src/ZF/Tools/induct_tacs.ML Mon Jun 16 17:56:08 2008 +0200
32.2 +++ b/src/ZF/Tools/induct_tacs.ML Mon Jun 16 22:13:39 2008 +0200
32.3 @@ -102,7 +102,7 @@
32.4 [] => error "induction is not available for this datatype"
32.5 | major::_ => FOLogic.dest_Trueprop major)
32.6 in
32.7 - RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state
32.8 + eres_inst_tac ctxt [(ixn, var)] rule i state
32.9 end
32.10 handle Find_tname msg =>
32.11 if exh then (*try boolean case analysis instead*)
33.1 --- a/src/ZF/UNITY/SubstAx.thy Mon Jun 16 17:56:08 2008 +0200
33.2 +++ b/src/ZF/UNITY/SubstAx.thy Mon Jun 16 22:13:39 2008 +0200
33.3 @@ -360,7 +360,7 @@
33.4 @{thm EnsuresI}, @{thm ensuresI}] 1),
33.5 (*now there are two subgoals: co & transient*)
33.6 simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
33.7 - RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
33.8 + res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
33.9 (*simplify the command's domain*)
33.10 simp_tac (ss addsimps [@{thm domain_def}]) 3,
33.11 (* proving the domain part *)
34.1 --- a/src/ZF/ind_syntax.ML Mon Jun 16 17:56:08 2008 +0200
34.2 +++ b/src/ZF/ind_syntax.ML Mon Jun 16 22:13:39 2008 +0200
34.3 @@ -51,7 +51,7 @@
34.4 (*For deriving cases rules. CollectD2 discards the domain, which is redundant;
34.5 read_instantiate replaces a propositional variable by a formula variable*)
34.6 val equals_CollectD =
34.7 - RuleInsts.read_instantiate @{context} [(("W", 0), "?Q")]
34.8 + read_instantiate @{context} [(("W", 0), "?Q")]
34.9 (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
34.10
34.11