--- a/src/CCL/Wfd.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/CCL/Wfd.thy Sat Apr 27 20:50:20 2013 +0200
@@ -473,14 +473,11 @@
(*** Clean up Correctness Condictions ***)
-val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
- hyp_subst_tac)
-
fun clean_ccs_tac ctxt =
let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
- eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
- hyp_subst_tac))
+ eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
+ hyp_subst_tac ctxt))
end
fun gen_ccs_tac ctxt rls i =
--- a/src/Doc/ZF/IFOL_examples.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Doc/ZF/IFOL_examples.thy Sat Apr 27 20:50:20 2013 +0200
@@ -36,7 +36,7 @@
done
lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
-by (tactic {*IntPr.fast_tac 1*})
+by (tactic {*IntPr.fast_tac @{context} 1*})
text{*Example of Dyckhoff's method*}
lemma "~ ~ ((P-->Q) | (Q-->P))"
--- a/src/FOL/FOL.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/FOL.thy Sat Apr 27 20:50:20 2013 +0200
@@ -150,7 +150,7 @@
proof (rule r)
{ fix y y'
assume "P(y)" and "P(y')"
- with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac 1")+
+ with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+
then have "y = y'" by (rule subst)
} note r' = this
show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')
--- a/src/FOL/IFOL.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/IFOL.thy Sat Apr 27 20:50:20 2013 +0200
@@ -635,7 +635,7 @@
and [Pure.elim 2] = allE notE' impE'
and [Pure.intro] = exI disjI2 disjI1
-setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
+setup {* Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) *}
lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
--- a/src/FOL/ex/Intuitionistic.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Intuitionistic.thy Sat Apr 27 20:50:20 2013 +0200
@@ -17,7 +17,7 @@
by (assume_tac 1);
by (IntPr.safe_tac 1);
by (IntPr.mp_tac 1);
-by (IntPr.fast_tac 1);
+by (IntPr.fast_tac @{context} 1);
*)
@@ -37,55 +37,55 @@
is intuitionstically equivalent to $P$. [Andy Pitts] *}
lemma "~~(P&Q) <-> ~~P & ~~Q"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*Double-negation does NOT distribute over disjunction*}
lemma "~~(P-->Q) <-> (~~P --> ~~Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "~~~P <-> ~P"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "~~((P --> Q | R) --> (P-->Q) | (P-->R))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "(P<->Q) <-> (Q<->P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "((P --> (Q | (Q-->R))) --> R) --> R"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
--> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
--> (((F-->A)-->B) --> I) --> E"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*Lemmas for the propositional double-negation translation*}
lemma "P --> ~~P"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "~~(~~P --> P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "~~P & ~~(P --> Q) --> ~~Q"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*The following are classically but not constructively valid.
The attempt to prove them terminates quickly!*}
lemma "((P-->Q) --> P) --> P"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
oops
lemma "(P&Q-->R) --> (P-->R) | (Q-->R)"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
oops
@@ -96,7 +96,7 @@
lemma "((P<->Q) --> P&Q&R) &
((Q<->R) --> P&Q&R) &
((R<->P) --> P&Q&R) --> P&Q&R"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*de Bruijn formula with five predicates*}
@@ -105,7 +105,7 @@
((R<->S) --> P&Q&R&S&T) &
((S<->T) --> P&Q&R&S&T) &
((T<->P) --> P&Q&R&S&T) --> P&Q&R&S&T"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
(*** Problems from of Sahlin, Franzen and Haridi,
@@ -116,11 +116,11 @@
text{*Problem 1.1*}
lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) <->
(ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
-by (tactic{*IntPr.best_dup_tac 1*}) --{*SLOW*}
+by (tactic{*IntPr.best_dup_tac @{context} 1*}) --{*SLOW*}
text{*Problem 3.1*}
lemma "~ (EX x. ALL y. mem(y,x) <-> ~ mem(x,x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*Problem 4.1: hopeless!*}
lemma "(ALL x. p(x) --> p(h(x)) | p(g(x))) & (EX x. p(x)) & (ALL x. ~p(h(x)))
@@ -132,78 +132,78 @@
text{*~~1*}
lemma "~~((P-->Q) <-> (~Q --> ~P))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~2*}
lemma "~~(~~P <-> P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*3*}
lemma "~(P-->Q) --> (Q-->P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~4*}
lemma "~~((~P-->Q) <-> (~Q --> P))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~5*}
lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~6*}
lemma "~~(P | ~P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~7*}
lemma "~~(P | ~~~P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~8. Peirce's law*}
lemma "~~(((P-->Q) --> P) --> P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*9*}
lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*10*}
lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
subsection{*11. Proved in each direction (incorrectly, says Pelletier!!) *}
lemma "P<->P"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~12. Dijkstra's law *}
lemma "~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*13. Distributive law*}
lemma "P | (Q & R) <-> (P | Q) & (P | R)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~14*}
lemma "~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~15*}
lemma "~~((P --> Q) <-> (~P | Q))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~16*}
lemma "~~((P-->Q) | (Q-->P))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~17*}
lemma "~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*Dijkstra's "Golden Rule"*}
lemma "(P&Q) <-> P <-> Q <-> (P|Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
subsection{*****Examples with quantifiers*****}
@@ -212,19 +212,19 @@
subsection{*The converse is classical in the following implications...*}
lemma "(EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "(ALL x. P(x)) | Q --> (ALL x. P(x) | Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
@@ -233,28 +233,28 @@
text{*The attempt to prove them terminates quickly!*}
lemma "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
oops
lemma "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
oops
lemma "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
oops
lemma "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
oops
text{*Classically but not intuitionistically valid. Proved by a bug in 1986!*}
lemma "EX x. Q(x) --> (ALL x. Q(x))"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
oops
@@ -275,7 +275,7 @@
text{*20*}
lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
--> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*21*}
lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"
@@ -283,11 +283,11 @@
text{*22*}
lemma "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~23*}
lemma "~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*24*}
lemma "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
@@ -295,10 +295,10 @@
--> ~~(EX x. P(x)&R(x))"
txt{*Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and
@{text ITER_DEEPEN} all take forever*}
-apply (tactic{* IntPr.safe_tac*})
+apply (tactic{* IntPr.safe_tac @{context}*})
apply (erule impE)
-apply (tactic{*IntPr.fast_tac 1*})
-by (tactic{*IntPr.fast_tac 1*})
+apply (tactic{*IntPr.fast_tac @{context} 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*25*}
lemma "(EX x. P(x)) &
@@ -306,7 +306,7 @@
(ALL x. P(x) --> (M(x) & L(x))) &
((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
--> (EX x. Q(x)&P(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~26*}
lemma "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) &
@@ -320,45 +320,45 @@
(ALL x. M(x) & L(x) --> P(x)) &
((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
--> (ALL x. M(x) --> ~L(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~28. AMENDED*}
lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
(~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
(~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
--> (ALL x. P(x) & L(x) --> M(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*29. Essentially the same as Principia Mathematica *11.71*}
lemma "(EX x. P(x)) & (EX y. Q(y))
--> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <->
(ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~30*}
lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
(ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
--> (ALL x. ~~S(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*31*}
lemma "~(EX x. P(x) & (Q(x) | R(x))) &
(EX x. L(x) & P(x)) &
(ALL x. ~ R(x) --> M(x))
--> (EX x. L(x) & M(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*32*}
lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
(ALL x. S(x) & R(x) --> L(x)) &
(ALL x. M(x) --> R(x))
--> (ALL x. P(x) & M(x) --> L(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*~~33*}
lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c))) <->
(ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))"
-apply (tactic{*IntPr.best_tac 1*})
+apply (tactic{*IntPr.best_tac @{context} 1*})
done
@@ -367,7 +367,7 @@
(ALL x. EX y. G(x,y)) &
(ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
--> (ALL x. EX y. H(x,y))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*37*}
lemma "(ALL z. EX w. ALL x. EX y.
@@ -379,47 +379,47 @@
text{*39*}
lemma "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*40. AMENDED*}
lemma "(EX y. ALL x. F(x,y) <-> F(x,x)) -->
~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*44*}
lemma "(ALL x. f(x) -->
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
(EX x. j(x) & (ALL y. g(y) --> h(x,y)))
--> (EX x. j(x) & ~f(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*48*}
lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*51*}
lemma "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
(EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*52*}
text{*Almost the same as 51. *}
lemma "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
(EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*56*}
lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*57*}
lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
(ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
text{*60*}
lemma "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
end
--- a/src/FOL/ex/Propositional_Cla.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Propositional_Cla.thy Sat Apr 27 20:50:20 2013 +0200
@@ -12,7 +12,7 @@
text {* commutative laws of @{text "&"} and @{text "|"} *}
lemma "P & Q --> Q & P"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "P | Q --> Q | P"
by fast
--- a/src/FOL/ex/Propositional_Int.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Propositional_Int.thy Sat Apr 27 20:50:20 2013 +0200
@@ -12,106 +12,106 @@
text {* commutative laws of @{text "&"} and @{text "|"} *}
lemma "P & Q --> Q & P"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "P | Q --> Q | P"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* associative laws of @{text "&"} and @{text "|"} *}
lemma "(P & Q) & R --> P & (Q & R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(P | Q) | R --> P | (Q | R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* distributive laws of @{text "&"} and @{text "|"} *}
lemma "(P & Q) | R --> (P | R) & (Q | R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(P | R) & (Q | R) --> (P & Q) | R"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(P | Q) & R --> (P & R) | (Q & R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(P & R) | (Q & R) --> (P | Q) & R"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* Laws involving implication *}
lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(P & Q --> R) <-> (P--> (Q-->R))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(P --> Q & R) <-> (P-->Q) & (P-->R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* Propositions-as-types *}
-- {* The combinator K *}
lemma "P --> (Q --> P)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
-- {* The combinator S *}
lemma "(P-->Q-->R) --> (P-->Q) --> (P-->R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
-- {* Converse is classical *}
lemma "(P-->Q) | (P-->R) --> (P --> Q | R)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(P-->Q) --> (~Q --> ~P)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* Schwichtenberg's examples (via T. Nipkow) *}
lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma stab_to_peirce:
"(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
--> ((P --> Q) --> P) --> P"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)
--> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma tatsuta: "(((P7 --> P1) --> P10) --> P4 --> P5)
--> (((P8 --> P2) --> P9) --> P3 --> P10)
--> (P1 --> P8) --> P6 --> P7
--> (((P3 --> P2) --> P9) --> P4)
--> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma tatsuta1: "(((P8 --> P2) --> P9) --> P3 --> P10)
--> (((P3 --> P2) --> P9) --> P4)
--> (((P6 --> P1) --> P2) --> P9)
--> (((P7 --> P1) --> P10) --> P4 --> P5)
--> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
end
--- a/src/FOL/ex/Quantifiers_Int.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Quantifiers_Int.thy Sat Apr 27 20:50:20 2013 +0200
@@ -10,91 +10,91 @@
begin
lemma "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
-- {* Converse is false *}
lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* Some harder ones *}
lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
-- {* Converse is false *}
lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* Basic test of quantifier reasoning *}
-- {* TRUE *}
lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* The following should fail, as they are false! *}
lemma "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
- apply (tactic "IntPr.fast_tac 1")?
+ apply (tactic "IntPr.fast_tac @{context} 1")?
oops
lemma "(EX x. Q(x)) --> (ALL x. Q(x))"
- apply (tactic "IntPr.fast_tac 1")?
+ apply (tactic "IntPr.fast_tac @{context} 1")?
oops
schematic_lemma "P(?a) --> (ALL x. P(x))"
- apply (tactic "IntPr.fast_tac 1")?
+ apply (tactic "IntPr.fast_tac @{context} 1")?
oops
schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
- apply (tactic "IntPr.fast_tac 1")?
+ apply (tactic "IntPr.fast_tac @{context} 1")?
oops
text {* Back to things that are provable \dots *}
lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
-- {* An example of why exI should be delayed as long as possible *}
lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
text {* Some slow ones *}
-- {* Principia Mathematica *11.53 *}
lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
(*Principia Mathematica *11.55 *)
lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
(*Principia Mathematica *11.61 *)
lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
- by (tactic "IntPr.fast_tac 1")
+ by (tactic "IntPr.fast_tac @{context} 1")
end
--- a/src/FOL/intprover.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/intprover.ML Sat Apr 27 20:50:20 2013 +0200
@@ -16,19 +16,19 @@
*)
signature INT_PROVER =
- sig
- val best_tac: int -> tactic
- val best_dup_tac: int -> tactic
- val fast_tac: int -> tactic
+sig
+ val best_tac: Proof.context -> int -> tactic
+ val best_dup_tac: Proof.context -> int -> tactic
+ val fast_tac: Proof.context -> int -> tactic
val inst_step_tac: int -> tactic
- val safe_step_tac: int -> tactic
+ val safe_step_tac: Proof.context -> int -> tactic
val safe_brls: (bool * thm) list
- val safe_tac: tactic
- val step_tac: int -> tactic
- val step_dup_tac: int -> tactic
+ val safe_tac: Proof.context -> tactic
+ val step_tac: Proof.context -> int -> tactic
+ val step_dup_tac: Proof.context -> int -> tactic
val haz_brls: (bool * thm) list
val haz_dup_brls: (bool * thm) list
- end;
+end;
structure IntPr : INT_PROVER =
@@ -62,14 +62,16 @@
List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
(*Attack subgoals using safe inferences -- matching, not resolution*)
-val safe_step_tac = FIRST' [eq_assume_tac,
- eq_mp_tac,
- bimatch_tac safe0_brls,
- hyp_subst_tac,
- bimatch_tac safep_brls] ;
+fun safe_step_tac ctxt =
+ FIRST' [
+ eq_assume_tac,
+ eq_mp_tac,
+ bimatch_tac safe0_brls,
+ hyp_subst_tac ctxt,
+ bimatch_tac safep_brls];
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
+fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
(*These steps could instantiate variables and are therefore unsafe.*)
val inst_step_tac =
@@ -77,20 +79,20 @@
biresolve_tac (safe0_brls @ safep_brls);
(*One safe or unsafe step. *)
-fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
+fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i];
-fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i];
+fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i];
(*Dumb but fast*)
-val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
+fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
(*Slower but smarter than fast_tac*)
-val best_tac =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
+fun best_tac ctxt =
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
(*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*)
-val best_dup_tac =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac 1));
+fun best_dup_tac ctxt =
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1));
end;
--- a/src/HOL/Auth/OtwayReesBella.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy Sat Apr 27 20:50:20 2013 +0200
@@ -258,9 +258,9 @@
method_setup disentangle = {*
Scan.succeed
- (K (SIMPLE_METHOD
+ (fn ctxt => SIMPLE_METHOD
(REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE]
- ORELSE' hyp_subst_tac)))) *}
+ ORELSE' hyp_subst_tac ctxt))) *}
"for eliminating conjunctions, disjunctions and the like"
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Apr 27 20:50:20 2013 +0200
@@ -751,11 +751,11 @@
(*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
(*Base*) (force_tac ctxt) 1
-val analz_prepare_tac =
+fun analz_prepare_tac ctxt =
prepare_tac THEN
dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN
(*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN
- REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
+ REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
end
*}
@@ -769,7 +769,7 @@
"additional facts to reason about parts"
method_setup analz_prepare = {*
- Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.analz_prepare_tac ctxt)) *}
"additional facts to reason about analz"
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sat Apr 27 20:50:20 2013 +0200
@@ -764,7 +764,7 @@
prepare_tac ctxt THEN
dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN
(*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN
- REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
+ REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
end
*}
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Sat Apr 27 20:50:20 2013 +0200
@@ -221,7 +221,7 @@
REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
(TRY o dresolve_tac Gwit_thms THEN'
(etac FalseE ORELSE'
- hyp_subst_tac THEN'
+ hyp_subst_tac ctxt THEN'
dresolve_tac Fwit_thms THEN'
(etac FalseE ORELSE' atac))) 1);
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Sat Apr 27 20:50:20 2013 +0200
@@ -504,7 +504,7 @@
val half_goalss = map mk_goal half_pairss;
val half_thmss =
map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
- fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
+ fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
half_goalss half_pairss (flat disc_thmss');
val other_half_goalss = map (mk_goal o map swap) half_pairss;
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Sat Apr 27 20:50:20 2013 +0200
@@ -15,7 +15,7 @@
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
thm list list list -> thm list list list -> tactic
- val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
+ val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
val mk_nchotomy_tac: int -> thm -> tactic
val mk_other_half_disc_exclude_tac: thm -> tactic
val mk_split_tac: Proof.context ->
@@ -44,13 +44,13 @@
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
- hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
+ hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
rtac distinct, rtac uexhaust] @
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
|> k = 1 ? swap |> op @)) 1;
-fun mk_half_disc_exclude_tac m discD disc' =
- (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1;
+fun mk_half_disc_exclude_tac ctxt m discD disc' =
+ (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN' rtac disc') 1;
fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1;
@@ -64,7 +64,7 @@
(if m = 0 then
atac
else
- REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
+ REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
@@ -100,7 +100,7 @@
fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
(rtac uexhaust THEN'
EVERY' (map3 (fn casex => fn if_discs => fn sels =>
- EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
+ EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
fun mk_case_cong_tac ctxt uexhaust cases =
@@ -112,7 +112,7 @@
(* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
rtac uexhaust 1 THEN
- ALLGOALS (fn k => (hyp_subst_tac THEN'
+ ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
flat (nth distinctsss (k - 1))) ctxt)) k) THEN
ALLGOALS (blast_tac naked_ctxt);
--- a/src/HOL/BNF/Tools/bnf_def.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Sat Apr 27 20:50:20 2013 +0200
@@ -971,7 +971,8 @@
(Logic.list_implies (prems_cong,
mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')));
in
- Goal.prove_sorry lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
+ Goal.prove_sorry lthy [] [] in_cong_goal
+ (K ((TRY o hyp_subst_tac lthy THEN' rtac refl) 1))
|> Thm.close_derivation
end;
@@ -989,7 +990,7 @@
val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
(Logic.list_implies (prem0 :: prems, eq));
in
- Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac (#map_cong0 axioms))
+ Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms))
|> Thm.close_derivation
end;
@@ -1073,7 +1074,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
- (fn _ => (TRY o hyp_subst_tac THEN' rtac refl) 1)
+ (fn _ => (TRY o hyp_subst_tac lthy THEN' rtac refl) 1)
|> Thm.close_derivation
end;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Sat Apr 27 20:50:20 2013 +0200
@@ -11,7 +11,7 @@
val mk_collect_set_map_tac: thm list -> tactic
val mk_map_id': thm -> thm
val mk_map_comp': thm -> thm
- val mk_map_cong_tac: thm -> tactic
+ val mk_map_cong_tac: Proof.context -> thm -> tactic
val mk_in_mono_tac: int -> tactic
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_set_map': thm -> thm
@@ -36,8 +36,8 @@
fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
-fun mk_map_cong_tac cong0 =
- (hyp_subst_tac THEN' rtac cong0 THEN'
+fun mk_map_cong_tac ctxt cong0 =
+ (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
fun mk_set_map' set_map = set_map RS @{thm pointfreeE};
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
@@ -82,21 +82,21 @@
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
rtac (@{thm snd_conv} RS sym)],
rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
stac @{thm fst_conv}, atac]) set_maps,
rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map2 (fn convol => fn map_id =>
EVERY' [rtac CollectI, rtac exI, rtac conjI,
@@ -136,7 +136,7 @@
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
+ REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt, rtac @{thm converseI},
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
@@ -163,7 +163,7 @@
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
@@ -188,7 +188,7 @@
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o eresolve_tac [exE, conjE],
REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps,
etac allE, etac impE, etac conjI, etac conjI, atac,
@@ -206,7 +206,7 @@
in
unfold_thms_tac ctxt (srel_O_Grs @
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
- EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
+ EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sat Apr 27 20:50:20 2013 +0200
@@ -128,19 +128,19 @@
(if is_refl disc then all_tac else rtac disc 1))
(map rtac case_splits' @ [K all_tac]) corec_likes discs);
-val solve_prem_prem_tac =
+fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
- hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
+ hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
(rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs =
EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)),
- solve_prem_prem_tac]) (rev kks)) 1;
+ solve_prem_prem_tac ctxt]) (rev kks)) 1;
fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks =
let val r = length kks in
- EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
+ EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt,
REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
EVERY [REPEAT_DETERM_N r
(rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
@@ -156,7 +156,7 @@
end;
fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
- hyp_subst_tac THEN'
+ hyp_subst_tac ctxt THEN'
CONVERSION (hhf_concl_conv
(Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
@@ -164,17 +164,18 @@
(atac ORELSE' REPEAT o etac conjE THEN'
full_simp_tac
(ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN_MAYBE'
- REPEAT o hyp_subst_tac THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
+ REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
fun mk_coinduct_distinct_ctrs ctxt discs discs' =
- hyp_subst_tac THEN' REPEAT o etac conjE THEN'
+ hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt);
fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
discss selss =
let val ks = 1 upto n in
EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, dtac
- meta_spec, dtac meta_mp, atac, rtac exhaust, K (inst_as_projs_tac ctxt 1), hyp_subst_tac] @
+ meta_spec, dtac meta_mp, atac, rtac exhaust, K (inst_as_projs_tac ctxt 1),
+ hyp_subst_tac ctxt] @
map4 (fn k => fn ctr_def => fn discs => fn sels =>
EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @
map2 (fn k' => fn discs' =>
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sat Apr 27 20:50:20 2013 +0200
@@ -290,7 +290,7 @@
prems concls xFs xFs_copy;
in
map (fn goal => Goal.prove_sorry lthy [] [] goal
- (K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals
+ (K ((hyp_subst_tac lthy THEN' rtac refl) 1)) |> Thm.close_derivation) goals
end;
val timer = time (timer "Derived simple theorems");
@@ -476,7 +476,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
(Logic.list_implies (prems, concl)))
- (K ((hyp_subst_tac THEN' atac) 1))
+ (K ((hyp_subst_tac lthy THEN' atac) 1))
|> Thm.close_derivation
end;
@@ -847,7 +847,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
(Logic.list_implies (prems, concl)))
- (K ((hyp_subst_tac THEN' atac) 1))
+ (K ((hyp_subst_tac lthy THEN' atac) 1))
|> Thm.close_derivation
end;
@@ -866,7 +866,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
(mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
- (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
+ (K (mk_bis_srel_tac lthy m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
|> Thm.close_derivation
end;
@@ -890,7 +890,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
(Logic.list_implies (prems, concl)))
- (K (mk_bis_O_tac m bis_srel_thm srel_congs srel_Os))
+ (K (mk_bis_O_tac lthy m bis_srel_thm srel_congs srel_Os))
|> Thm.close_derivation
end;
@@ -980,7 +980,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss)
(HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
- (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm))
+ (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
|> Thm.close_derivation;
val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
@@ -1299,7 +1299,7 @@
val card_of_carT =
Goal.prove_sorry lthy [] []
(fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs)))
- (K (mk_card_of_carT_tac m isNode_defs sbd_sbd_thm
+ (K (mk_card_of_carT_tac lthy m isNode_defs sbd_sbd_thm
sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds))
|> Thm.close_derivation
in
@@ -1368,7 +1368,7 @@
map5 (fn j => fn goal => fn cts => fn set_incl_hsets => fn set_hset_incl_hsetss =>
singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts
+ (K (mk_strT_hset_tac lthy n m j arg_cong_cTs cTs cts
carT_defs strT_defs isNode_defs
set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss'
coalgT_thm set_map'ss)))
@@ -1572,7 +1572,7 @@
val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss))
+ (K (mk_Lev_sbd_tac lthy cts Lev_0s Lev_Sucs to_sbd_thmss))
|> Thm.close_derivation);
val Lev_sbd' = mk_specN n Lev_sbd;
@@ -1591,7 +1591,7 @@
val length_Lev = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs))
+ (K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs))
|> Thm.close_derivation);
val length_Lev' = mk_specN (n + 1) length_Lev;
@@ -1621,7 +1621,7 @@
val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)))
+ (K (mk_prefCl_Lev_tac lthy cts Lev_0s Lev_Sucs)))
|> Thm.close_derivation;
val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev;
@@ -1670,7 +1670,7 @@
val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] []
(Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
- (K (mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
+ (K (mk_set_rv_Lev_tac lthy m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
coalg_set_thmss from_to_sbd_thmss)))
|> Thm.close_derivation;
@@ -1710,7 +1710,7 @@
val set_Lev = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
+ (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
|> Thm.close_derivation;
val set_Lev' = mk_specN (3 * n + 1) set_Lev;
@@ -1748,7 +1748,7 @@
val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss
+ (K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss
from_to_sbd_thmss to_sbd_inj_thmss)))
|> Thm.close_derivation;
@@ -2289,7 +2289,9 @@
val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl)))
- (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids)))
+ (fn _ =>
+ mk_dtor_srel_strong_coinduct_tac lthy
+ m cTs cts dtor_srel_coinduct srel_monos srel_Ids))
|> Thm.close_derivation;
val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
@@ -2584,7 +2586,7 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
+ (K (mk_mcong_tac lthy m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
set_hset_thmss set_hset_hset_thmsss)))
|> Thm.close_derivation
in
@@ -2696,7 +2698,8 @@
val in_bd_tacs = map7 (fn i => fn isNode_hsets => fn carT_def =>
fn card_of_carT => fn mor_image => fn Rep_inverse => fn mor_hsets =>
- K (mk_in_bd_tac (nth isNode_hsets (i - 1)) isNode_hsets carT_def
+ K (mk_in_bd_tac lthy (* FIXME proper context!? *)
+ (nth isNode_hsets (i - 1)) isNode_hsets carT_def
card_of_carT mor_image Rep_inverse mor_hsets
sbd_Cnotzero sbd_Card_order mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm))
ks isNode_hset_thmss carT_defs card_of_carT_thms
@@ -2944,7 +2947,7 @@
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
+ (K (mk_dtor_srel_tac lthy in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sat Apr 27 20:50:20 2013 +0200
@@ -9,18 +9,21 @@
signature BNF_GFP_TACTICS =
sig
- val mk_Lev_sbd_tac: cterm option list -> thm list -> thm list -> thm list list -> tactic
+ val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
+ thm list list -> tactic
val mk_bd_card_order_tac: thm -> tactic
val mk_bd_cinfinite_tac: thm -> tactic
val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
- val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
+ val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
- val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
+ val mk_bis_srel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
+ thm list list -> tactic
val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
{prems: 'a, context: Proof.context} -> tactic
- val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
+ val mk_card_of_carT_tac: Proof.context -> int -> thm list -> thm -> thm -> thm -> thm -> thm ->
+ thm list -> tactic
val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
@@ -44,25 +47,25 @@
thm -> thm -> tactic
val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
- val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
- thm list -> thm list -> tactic
- val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
- thm list -> thm list -> thm list list -> tactic
+ val mk_dtor_srel_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
+ cterm option list -> thm -> thm list -> thm list -> tactic
+ val mk_dtor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
+ thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
- val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
- thm -> thm -> thm -> tactic
+ val mk_in_bd_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm -> thm -> thm list ->
+ thm -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_incl_lsbis_tac: int -> int -> thm -> tactic
val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_length_Lev'_tac: thm -> tactic
- val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic
+ val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
- val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list ->
- thm list list -> thm list list list -> tactic
+ val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
+ thm list list -> thm list list -> thm list list list -> tactic
val mk_map_id_tac: thm list -> thm -> thm -> tactic
val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
@@ -92,7 +95,7 @@
{prems: 'a, context: Proof.context} -> tactic
val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
thm list -> tactic
- val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
+ val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
@@ -100,22 +103,22 @@
val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
thm list -> thm list -> thm -> thm list -> tactic
val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
- val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
- val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
- thm list list -> tactic
+ val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
+ val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
+ thm list -> thm list list -> tactic
val mk_set_bd_tac: thm -> thm -> thm -> tactic
val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
- val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
- thm list list -> thm list list -> tactic
+ val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
+ thm list -> thm list -> thm list list -> thm list list -> tactic
val mk_set_incl_hin_tac: thm list -> tactic
val mk_set_incl_hset_tac: thm -> thm -> tactic
val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
val mk_set_map_tac: thm -> thm -> tactic
- val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
- thm list list -> thm list list -> tactic
- val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
- cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
- thm list list -> thm list list -> thm -> thm list list -> tactic
+ val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
+ thm list -> thm list -> thm list list -> thm list list -> tactic
+ val mk_strT_hset_tac: Proof.context -> int -> int -> int -> ctyp option list ->
+ ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
+ thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic
val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
val mk_unique_mor_tac: thm list -> thm -> tactic
val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
@@ -256,7 +259,7 @@
EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
atac, atac, rtac (hset_def RS sym)] 1
-fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
+fun mk_bis_srel_tac ctxt m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
let
val n = length srel_O_Grs;
val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
@@ -288,7 +291,7 @@
REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE,
- hyp_subst_tac,
+ hyp_subst_tac ctxt,
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
@@ -327,7 +330,7 @@
REPEAT_DETERM o etac allE,
rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
-fun mk_bis_O_tac m bis_srel srel_congs srel_Os =
+fun mk_bis_O_tac ctxt m bis_srel srel_congs srel_Os =
EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
@@ -339,7 +342,7 @@
rtac srel_O,
etac @{thm relcompE},
REPEAT_DETERM o dtac Pair_eqD,
- etac conjE, hyp_subst_tac,
+ etac conjE, hyp_subst_tac ctxt,
REPEAT_DETERM o etac allE, rtac @{thm relcompI},
etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
@@ -371,13 +374,13 @@
atac]) (ks ~~ in_monos)] 1
end;
-fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong =
+fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
let
val n = length lsbis_defs;
in
EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
- hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
+ hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
end;
fun mk_incl_lsbis_tac n i lsbis_def =
@@ -407,7 +410,7 @@
val ks = 1 upto n;
fun coalg_tac (i, ((passive_sets, active_sets), def)) =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
+ hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
rtac (mk_sum_casesN n i), rtac CollectI,
EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
@@ -449,7 +452,7 @@
CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
end;
-fun mk_card_of_carT_tac m isNode_defs sbd_sbd
+fun mk_card_of_carT_tac ctxt m isNode_defs sbd_sbd
sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
let
val n = length isNode_defs;
@@ -518,11 +521,11 @@
if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
rtac sbd_Cnotzero,
rtac @{thm card_of_mono1}, rtac subsetI,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac ctxt,
rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
- hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
+ hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
[rtac (mk_UnIN n i), dtac (def RS iffD1),
@@ -538,7 +541,7 @@
EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
dtac Pair_eqD,
- etac conjE, hyp_subst_tac,
+ etac conjE, hyp_subst_tac ctxt,
dtac (isNode_def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE],
rtac (equalityD2 RS set_mp),
@@ -548,7 +551,7 @@
rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
etac @{thm prefCl_Succ}, atac] 1;
-fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
+fun mk_strT_hset_tac ctxt n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
let
val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
@@ -564,7 +567,7 @@
else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
dtac conjunct2, dtac Pair_eqD, etac conjE,
- hyp_subst_tac, dtac (isNode_def RS iffD1),
+ hyp_subst_tac ctxt, dtac (isNode_def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE],
rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
(ks ~~ (carT_defs ~~ isNode_defs));
@@ -601,7 +604,7 @@
(strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
end;
-fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss =
+fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
let
val n = length Lev_0s;
val ks = 1 upto n;
@@ -615,7 +618,7 @@
EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (i, to_sbd) => EVERY' [rtac subsetI,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
etac set_rev_mp, REPEAT_DETERM o etac allE,
etac (mk_conjunctN n i)])
@@ -623,7 +626,7 @@
(Lev_Sucs ~~ to_sbdss)] 1
end;
-fun mk_length_Lev_tac cts Lev_0s Lev_Sucs =
+fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
let
val n = length Lev_0s;
val ks = n downto 1;
@@ -637,16 +640,17 @@
CONJ_WRAP' (fn Lev_Suc =>
EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
- (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
- rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
- REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
+ (fn i =>
+ EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
+ rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
+ REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
Lev_Sucs] 1
end;
fun mk_length_Lev'_tac length_Lev =
EVERY' [ftac length_Lev, etac ssubst, atac] 1;
-fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs =
+fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs =
let
val n = length Lev_0s;
val ks = n downto 1;
@@ -655,18 +659,21 @@
REPEAT_DETERM o rtac allI,
CONJ_WRAP' (fn Lev_0 =>
EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
- etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
- hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
+ etac @{thm singletonE}, hyp_subst_tac ctxt,
+ dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
+ hyp_subst_tac ctxt,
+ rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
REPEAT_DETERM o rtac allI,
CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
- (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
- dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
+ (fn i =>
+ EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
+ dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt,
rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
rtac Lev_0, rtac @{thm singletonI},
- REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
+ REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt,
rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
@@ -699,7 +706,7 @@
ks)] 1
end;
-fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
+fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
let
val n = length Lev_0s;
val ks = 1 upto n;
@@ -718,7 +725,7 @@
EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn (i, (from_to_sbd, coalg_set)) =>
- EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
rtac (rv_Cons RS arg_cong RS iffD2),
rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
@@ -728,7 +735,7 @@
((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
end;
-fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
+fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
let
val n = length Lev_0s;
val ks = 1 upto n;
@@ -737,10 +744,10 @@
REPEAT_DETERM o rtac allI,
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
- etac @{thm singletonE}, hyp_subst_tac,
+ etac @{thm singletonE}, hyp_subst_tac ctxt,
CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
(if i = i'
- then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
+ then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac ctxt,
CONJ_WRAP' (fn (i'', Lev_0'') =>
EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
@@ -756,7 +763,7 @@
EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn (i, from_to_sbd) =>
- EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
CONJ_WRAP' (fn i' => rtac impI THEN'
CONJ_WRAP' (fn i'' =>
EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
@@ -774,7 +781,7 @@
((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
end;
-fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
+fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
let
val n = length Lev_0s;
val ks = 1 upto n;
@@ -783,18 +790,18 @@
REPEAT_DETERM o rtac allI,
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
- etac @{thm singletonE}, hyp_subst_tac,
+ etac @{thm singletonE}, hyp_subst_tac ctxt,
CONJ_WRAP' (fn i' => rtac impI THEN'
CONJ_WRAP' (fn i'' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
(if i = i''
then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
- hyp_subst_tac,
+ hyp_subst_tac ctxt,
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
dtac list_inject_iffD1 THEN' etac conjE THEN'
(if k = i'
- then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
+ then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
else etac (mk_InN_not_InM i' k RS notE)))
(rev ks)]
else etac (mk_InN_not_InM i'' i RS notE)))
@@ -806,7 +813,7 @@
EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn (i, (from_to_sbd, to_sbd_inj)) =>
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
CONJ_WRAP' (fn i' => rtac impI THEN'
dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
@@ -816,7 +823,7 @@
(if k = i
then EVERY' [dtac (mk_InN_inject n i),
dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
- atac, atac, hyp_subst_tac] THEN'
+ atac, atac, hyp_subst_tac ctxt] THEN'
CONJ_WRAP' (fn i'' =>
EVERY' [rtac impI, dtac (sym RS trans),
rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
@@ -875,7 +882,7 @@
rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
if n = 1 then rtac refl else atac, atac, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
- rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
+ rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
if n = 1 then rtac refl else atac])
(drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
@@ -901,7 +908,7 @@
REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
REPEAT_DETERM_N 4 o etac thin_rl,
rtac set_image_Lev,
- atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
+ atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
if n = 1 then rtac refl else atac])
(drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
@@ -958,7 +965,7 @@
dtac list_inject_iffD1, etac conjE,
if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
- atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
+ atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
@@ -973,7 +980,7 @@
dtac list_inject_iffD1, etac conjE,
if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
- atac, atac, hyp_subst_tac, atac]
+ atac, atac, hyp_subst_tac ctxt, atac]
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
@@ -1132,11 +1139,11 @@
CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
-fun mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
+fun mk_dtor_srel_strong_coinduct_tac ctxt m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
EVERY' (map2 (fn srel_mono => fn srel_Id =>
EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
- etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
+ etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (srel_mono RS set_mp),
REPEAT_DETERM_N m o rtac @{thm subset_refl},
REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
@@ -1220,7 +1227,7 @@
replicate n (@{thm o_id} RS fun_cong))))
maps map_comps map_cong0s)] 1;
-fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
+fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
set_hset_hsetsss =
let
val n = length map_comp's;
@@ -1230,8 +1237,8 @@
coinduct_tac] @
maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
set_hset_hsetss) =>
- [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
- rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
+ [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
+ rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
@@ -1309,7 +1316,7 @@
@{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
-fun mk_in_bd_tac isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
+fun mk_in_bd_tac ctxt isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg =
let
val n = length isNode_hsets;
@@ -1331,7 +1338,7 @@
rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
rtac @{thm proj_image}, rtac @{thm image_eqI}, atac,
ftac (carT_def RS equalityD1 RS set_mp),
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
@@ -1371,7 +1378,7 @@
CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
- hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
+ hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
pickWP_assms_tac,
SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
@@ -1395,7 +1402,7 @@
CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
- hyp_subst_tac,
+ hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
rtac (map_comp RS trans),
SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
@@ -1412,7 +1419,7 @@
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
CONJ_WRAP' (fn (unfold, map_comp) =>
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
- hyp_subst_tac,
+ hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
rtac refl])
(unfolds ~~ map_comps) 1;
@@ -1431,7 +1438,7 @@
CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
- hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
+ hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
pickWP_assms_tac,
rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -1443,7 +1450,7 @@
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
EVERY' [rtac @{thm UN_least},
SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
- etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
+ etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
(ks ~~ rev (drop m set_maps))])
(rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
@@ -1484,18 +1491,18 @@
(eresolve_tac wit ORELSE'
(dresolve_tac wit THEN'
(etac FalseE ORELSE'
- EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
+ EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
- rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
+ rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
- ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
+ ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
- set_maps dtor_set_incls dtor_set_set_inclss =
+fun mk_dtor_srel_tac ctxt in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject
+ dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
let
val m = length dtor_set_incls;
val n = length dtor_set_set_inclss;
@@ -1536,7 +1543,7 @@
dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
- hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
+ hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
(rev (active_set_maps ~~ in_Jsrels))])
(dtor_sets ~~ passive_set_maps),
rtac conjI,
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sat Apr 27 20:50:20 2013 +0200
@@ -294,7 +294,7 @@
in
map2 (fn goal => fn alg_set =>
Goal.prove_sorry lthy [] []
- goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms))
+ goal (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
|> Thm.close_derivation)
goals alg_set_thms
end;
@@ -420,7 +420,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
(Logic.list_implies (prems, concl)))
- (K ((hyp_subst_tac THEN' atac) 1))
+ (K ((hyp_subst_tac lthy THEN' atac) 1))
|> Thm.close_derivation
end;
@@ -654,7 +654,7 @@
val monos =
map2 (fn goal => fn min_algs =>
- Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
+ Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs))
|> Thm.close_derivation)
(map mk_mono_goal min_algss) min_algs_thms;
@@ -1315,7 +1315,7 @@
in
(Goal.prove_sorry lthy [] []
(fold_rev Logic.all (phis @ Izs) goal)
- (K (mk_ctor_induct_tac m set_map'ss init_induct_thm morE_thms mor_Abs_thm
+ (K (mk_ctor_induct_tac lthy m set_map'ss init_induct_thm morE_thms mor_Abs_thm
Rep_inverses Abs_inverses Reps))
|> Thm.close_derivation,
rev (Term.add_tfrees goal []))
@@ -1677,7 +1677,7 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] [] goal
- (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
+ (K (mk_lfp_map_wpull_tac lthy m (rtac induct) map_wpulls ctor_map_thms
(transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms)))
|> Thm.close_derivation;
in
@@ -1728,13 +1728,14 @@
ctors (0 upto n - 1) witss
end;
- fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
+ fun wit_tac ctxt _ = mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
val (Ibnfs, lthy) =
fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
fn T => fn wits => fn lthy =>
- bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b rel_b
- set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
+ bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac lthy) (SOME deads)
+ map_b rel_b set_bs
+ (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
lthy
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
@@ -1780,7 +1781,7 @@
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
+ (K (mk_ctor_srel_tac lthy in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sat Apr 27 20:50:20 2013 +0200
@@ -10,7 +10,7 @@
sig
val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
thm list -> tactic
- val mk_alg_not_empty_tac: thm -> thm list -> thm list -> tactic
+ val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_alg_set_tac: thm -> tactic
val mk_bd_card_order_tac: thm list -> tactic
@@ -18,13 +18,13 @@
val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic
val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
- val mk_ctor_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list ->
- thm list -> tactic
+ val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
+ thm list -> thm list -> thm list -> tactic
val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
- val mk_ctor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
- thm list -> thm list -> thm list list -> tactic
+ val mk_ctor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
+ thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
@@ -38,8 +38,8 @@
val mk_iso_alt_tac: thm list -> thm -> tactic
val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
val mk_least_min_alg_tac: thm -> thm -> tactic
- val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
- thm list list list -> thm list -> tactic
+ val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
+ thm list list -> thm list list list -> thm list -> tactic
val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
@@ -49,7 +49,7 @@
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
thm -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
- val mk_min_algs_mono_tac: thm -> tactic
+ val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
val mk_min_algs_tac: thm -> thm list -> tactic
val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list ->
@@ -73,7 +73,7 @@
thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
val mk_set_map_tac: thm -> tactic
val mk_set_tac: thm -> tactic
- val mk_wit_tac: int -> thm list -> thm list -> tactic
+ val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
val mk_wpull_tac: thm -> tactic
end;
@@ -95,13 +95,13 @@
EVERY' [etac bspec, rtac CollectI] 1 THEN
REPEAT_DETERM (etac conjI 1) THEN atac 1;
-fun mk_alg_not_empty_tac alg_set alg_sets wits =
- (EVERY' [rtac notI, hyp_subst_tac, ftac alg_set] THEN'
+fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
+ (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
REPEAT_DETERM o FIRST'
[rtac subset_UNIV,
EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
- EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac,
+ EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt,
FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
etac @{thm emptyE}) 1;
@@ -280,10 +280,10 @@
CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
end;
-fun mk_min_algs_mono_tac min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
+fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
rtac impI, rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2},
rtac subsetI, rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac,
- rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac, rtac refl] 1;
+ rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite Asuc_Cnotzero =
@@ -384,7 +384,7 @@
REPEAT_DETERM o etac conjE, atac] 1;
fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
- EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
+ EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
@@ -531,7 +531,7 @@
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
etac fold_unique_mor 1;
-fun mk_ctor_induct_tac m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
+fun mk_ctor_induct_tac ctxt m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
let
val n = length set_map'ss;
val ks = 1 upto n;
@@ -539,7 +539,7 @@
fun mk_IH_tac Rep_inv Abs_inv set_map' =
DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE,
- hyp_subst_tac, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
+ hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
fun mk_closed_tac (k, (morE, set_map's)) =
EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
@@ -680,7 +680,7 @@
(induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1
end;
-fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
+fun mk_lfp_map_wpull_tac ctxt m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
let
val n = length wpulls;
val ks = 1 upto n;
@@ -718,7 +718,7 @@
CONJ_WRAP' (K (rtac subset_refl)) ks,
rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map,
rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
- hyp_subst_tac, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
+ hyp_subst_tac ctxt, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
CONJ_WRAP' mk_subset ctor_sets];
in
(induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1
@@ -763,7 +763,7 @@
EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,
rtac wpull, REPEAT_DETERM o atac] 1;
-fun mk_wit_tac n ctor_set wit =
+fun mk_wit_tac ctxt n ctor_set wit =
REPEAT_DETERM (atac 1 ORELSE
EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM o
@@ -771,10 +771,10 @@
(eresolve_tac wit ORELSE'
(dresolve_tac wit THEN'
(etac FalseE ORELSE'
- EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
+ EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
+fun mk_ctor_srel_tac ctxt in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
let
val m = length ctor_set_incls;
@@ -821,7 +821,7 @@
dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
- hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
+ hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
(rev (active_set_maps ~~ in_Isrels))])
(ctor_sets ~~ passive_set_maps),
rtac conjI,
--- a/src/HOL/Bali/AxSem.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Bali/AxSem.thy Sat Apr 27 20:50:20 2013 +0200
@@ -693,7 +693,7 @@
apply (tactic "ALLGOALS strip_tac")
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
-apply (tactic "TRYALL hyp_subst_tac")
+apply (tactic "TRYALL (hyp_subst_tac @{context})")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)
apply (blast intro: ax_derivs.insert)
--- a/src/HOL/HOL.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/HOL.thy Sat Apr 27 20:50:20 2013 +0200
@@ -849,15 +849,15 @@
let
fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
| non_bool_eq _ = false;
- val hyp_subst_tac' =
+ fun hyp_subst_tac' ctxt =
SUBGOAL (fn (goal, i) =>
if Term.exists_Const non_bool_eq goal
- then Hypsubst.hyp_subst_tac i
+ then Hypsubst.hyp_subst_tac ctxt i
else no_tac);
in
Hypsubst.hypsubst_setup
(*prevent substitution on bool*)
- #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+ #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
end
*}
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Sat Apr 27 20:50:20 2013 +0200
@@ -1082,7 +1082,7 @@
fun Seq_case_tac ctxt s i =
res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
- THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+ THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
fun Seq_case_simp_tac ctxt s i =
@@ -1103,7 +1103,7 @@
fun pair_tac ctxt s =
res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
- THEN' hyp_subst_tac THEN' asm_full_simp_tac ctxt;
+ THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
(* induction on a sequence of pairs with pairsplitting and simplification *)
fun pair_induct_tac ctxt s rws i =
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sat Apr 27 20:50:20 2013 +0200
@@ -201,7 +201,7 @@
apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context}))) *})
-apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
+apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac @{context}])")
-- "Level 7"
-- "15 NewC"
@@ -240,7 +240,7 @@
-- "for FAss"
apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
- THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
+ THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
-- "for if"
apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Apr 27 20:50:20 2013 +0200
@@ -1738,7 +1738,7 @@
rotate_tac ~1 1,
((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
(put_simpset HOL_ss context addsimps flat distinct_thms)) 1] @
- (if null idxs then [] else [hyp_subst_tac 1,
+ (if null idxs then [] else [hyp_subst_tac context 1,
SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
let
val SOME prem = find_first (can (HOLogic.dest_eq o
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Sat Apr 27 20:50:20 2013 +0200
@@ -536,11 +536,11 @@
by (blast intro: analz_mono [THEN [2] rev_subsetD])
method_setup valid_certificate_tac = {*
- Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
+ Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
(fn i =>
EVERY [ftac @{thm Gets_certificate_valid} i,
assume_tac i,
- etac conjE i, REPEAT (hyp_subst_tac i)])))
+ etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
*}
text{*The @{text "(no_asm)"} attribute is essential, since it retains
--- a/src/HOL/SET_Protocol/Purchase.thy Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/SET_Protocol/Purchase.thy Sat Apr 27 20:50:20 2013 +0200
@@ -481,9 +481,9 @@
method_setup valid_certificate_tac = {*
Args.goal_spec >> (fn quant =>
- K (SIMPLE_METHOD'' quant (fn i =>
+ fn ctxt => SIMPLE_METHOD'' quant (fn i =>
EVERY [ftac @{thm Gets_certificate_valid} i,
- assume_tac i, REPEAT (hyp_subst_tac i)])))
+ assume_tac i, REPEAT (hyp_subst_tac ctxt i)]))
*}
--- a/src/HOL/Tools/Datatype/datatype.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Sat Apr 27 20:50:20 2013 +0200
@@ -418,13 +418,13 @@
val inj_thm =
Goal.prove_sorry_global thy5 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
- (fn _ => EVERY
+ (fn {context = ctxt, ...} => EVERY
[(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (EVERY
[rtac allI 1, rtac impI 1,
Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
REPEAT (EVERY
- [hyp_subst_tac 1,
+ [hyp_subst_tac ctxt 1,
rewrite_goals_tac rewrites,
REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
(eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
@@ -480,7 +480,7 @@
if length descr = 1 then []
else
drop (length newTs) (Datatype_Aux.split_conj_thm
- (Goal.prove_sorry_global thy5 [] [] iso_t (fn _ => EVERY
+ (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
[(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
@@ -489,7 +489,7 @@
REPEAT (EVERY
[REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
- TRY (hyp_subst_tac 1),
+ TRY (hyp_subst_tac ctxt 1),
rtac (sym RS range_eqI) 1,
resolve_tac iso_char_thms 1])])));
@@ -556,9 +556,9 @@
Lim_inject, Suml_inject, Sumr_inject])
in
Goal.prove_sorry_global thy5 [] [] t
- (fn _ => EVERY
+ (fn {context = ctxt, ...} => EVERY
[rtac iffI 1,
- REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
+ REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
dresolve_tac rep_congs 1, dtac box_equals 1,
REPEAT (resolve_tac rep_thms 1),
REPEAT (eresolve_tac inj_thms 1),
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Sat Apr 27 20:50:20 2013 +0200
@@ -179,9 +179,9 @@
etac elim 1,
REPEAT_DETERM_N j distinct_tac,
TRY (dresolve_tac inject 1),
- REPEAT (etac conjE 1), hyp_subst_tac 1,
+ REPEAT (etac conjE 1), hyp_subst_tac ctxt 1,
REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
- TRY (hyp_subst_tac 1),
+ TRY (hyp_subst_tac ctxt 1),
rtac refl 1,
REPEAT_DETERM_N (n - j - 1) distinct_tac],
intrs, j + 1)
@@ -403,14 +403,15 @@
fun prove_nchotomy (t, exhaustion) =
let
(* For goal i, select the correct disjunct to attack, then prove it *)
- fun tac i 0 = EVERY [TRY (rtac disjI1 i), hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
- | tac i n = rtac disjI2 i THEN tac i (n - 1);
+ fun tac ctxt i 0 =
+ EVERY [TRY (rtac disjI1 i), hyp_subst_tac ctxt i, REPEAT (rtac exI i), rtac refl i]
+ | tac ctxt i n = rtac disjI2 i THEN tac ctxt i (n - 1);
in
Goal.prove_sorry_global thy [] [] t
- (fn _ =>
+ (fn {context = ctxt, ...} =>
EVERY [rtac allI 1,
Datatype_Aux.exh_tac (K exhaustion) 1,
- ALLGOALS (fn i => tac i (i - 1))])
+ ALLGOALS (fn i => tac ctxt i (i - 1))])
end;
val nchotomys =
--- a/src/HOL/Tools/inductive.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/inductive.ML Sat Apr 27 20:50:20 2013 +0200
@@ -534,7 +534,7 @@
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
fun simp_case_tac ctxt i =
- EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac] i;
+ EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
in
@@ -724,7 +724,7 @@
REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
(*Now break down the individual cases. No disjE here in case
some premise involves disjunction.*)
- REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
+ REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
REPEAT (FIRSTGOAL
(resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Sat Apr 27 20:50:20 2013 +0200
@@ -317,7 +317,7 @@
fun elim_Collect_tac ctxt = dtac @{thm iffD1[OF mem_Collect_eq]}
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
THEN' REPEAT_DETERM o etac @{thm conjE}
- THEN' TRY o hyp_subst_tac' ctxt;
+ THEN' TRY o hyp_subst_tac ctxt;
fun intro_image_tac ctxt = rtac @{thm image_eqI}
THEN' (REPEAT_DETERM1 o
@@ -332,7 +332,7 @@
THEN' REPEAT_DETERM o CHANGED o
(TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
THEN' REPEAT_DETERM o etac @{thm Pair_inject}
- THEN' TRY o hyp_subst_tac' ctxt)
+ THEN' TRY o hyp_subst_tac ctxt)
fun tac1_of_formula ctxt (Int (fm1, fm2)) =
TRY o etac @{thm conjE}
@@ -376,16 +376,16 @@
ORELSE' etac @{thm conjE}
ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]) THEN'
- REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl})
+ REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
ORELSE' (etac @{thm imageE}
THEN' (REPEAT_DETERM o CHANGED o
(TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
THEN' REPEAT_DETERM o etac @{thm Pair_inject}
- THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl})))
+ THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
ORELSE' etac @{thm ComplE}
ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}])
- THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl}))
+ THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
fun tac ctxt fm =
let
@@ -398,7 +398,7 @@
THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
THEN' REPEAT_DETERM o resolve_tac @{thms exI}
THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
- THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac' ctxt) THEN' rtac @{thm refl}))))
+ THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' rtac @{thm refl}))))
THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
in
--- a/src/Provers/classical.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Provers/classical.ML Sat Apr 27 20:50:20 2013 +0200
@@ -25,8 +25,8 @@
val swap: thm (* ~ P ==> (~ R ==> P) ==> R *)
val classical: thm (* (~ P ==> P) ==> P *)
val sizef: thm -> int (* size function for BEST_FIRST, typically size_of_thm *)
- val hyp_subst_tacs: (int -> tactic) list (* optional tactics for substitution in
- the hypotheses; assumed to be safe! *)
+ val hyp_subst_tacs: (Proof.context -> int -> tactic) list (* optional tactics for
+ substitution in the hypotheses; assumed to be safe! *)
end;
signature BASIC_CLASSICAL =
@@ -697,7 +697,7 @@
[eq_assume_tac,
eq_mp_tac,
bimatch_from_nets_tac safe0_netpair,
- FIRST' Data.hyp_subst_tacs,
+ FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
bimatch_from_nets_tac safep_netpair])
end;
@@ -733,7 +733,7 @@
(FIRST'
[eq_assume_contr_tac,
bimatch_from_nets_tac safe0_netpair,
- FIRST' Data.hyp_subst_tacs,
+ FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
n_bimatch_from_nets_tac 1 safep_netpair,
bimatch2_tac safep_netpair])
end;
--- a/src/Provers/hypsubst.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Provers/hypsubst.ML Sat Apr 27 20:50:20 2013 +0200
@@ -46,9 +46,8 @@
signature HYPSUBST =
sig
- val bound_hyp_subst_tac : int -> tactic
- val hyp_subst_tac : int -> tactic
- val hyp_subst_tac' : Proof.context -> int -> tactic
+ val bound_hyp_subst_tac : Proof.context -> int -> tactic
+ val hyp_subst_tac : Proof.context -> int -> tactic
val blast_hyp_subst_tac : bool -> int -> tactic
val stac : thm -> int -> tactic
val hypsubst_setup : theory -> theory
@@ -127,14 +126,10 @@
(*Select a suitable equality assumption; substitute throughout the subgoal
If bnd is true, then it replaces Bound variables only. *)
- fun gen_hyp_subst_tac opt_ctxt bnd =
+ fun gen_hyp_subst_tac ctxt bnd =
let fun tac i st = SUBGOAL (fn (Bi, _) =>
let
val (k, _) = eq_var bnd true Bi
- val ctxt =
- (case opt_ctxt of
- NONE => Proof_Context.init_global (Thm.theory_of_thm st)
- | SOME ctxt => ctxt)
val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
etac thin_rl i, rotate_tac (~k) i]
@@ -198,15 +193,13 @@
handle THM _ => no_tac | EQ_VAR => no_tac);
(*Substitutes for Free or Bound variables*)
-val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
- gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
-
-fun hyp_subst_tac' ctxt = FIRST' [ematch_tac [Data.thin_refl],
- gen_hyp_subst_tac (SOME ctxt) false, vars_gen_hyp_subst_tac false];
+fun hyp_subst_tac ctxt =
+ FIRST' [ematch_tac [Data.thin_refl],
+ gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false];
(*Substitutes for Bound variables only -- this is always safe*)
-val bound_hyp_subst_tac =
- gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
+fun bound_hyp_subst_tac ctxt =
+ gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac true;
(** Version for Blast_tac. Hyps that are affected by the substitution are
@@ -271,7 +264,7 @@
val hypsubst_setup =
Method.setup @{binding hypsubst}
- (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
+ (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
"substitution using an assumption (improper)" #>
Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
"simple substitution";
--- a/src/Pure/Isar/context_rules.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Pure/Isar/context_rules.ML Sat Apr 27 20:50:20 2013 +0200
@@ -14,8 +14,8 @@
val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
val print_rules: Proof.context -> unit
- val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
- val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
+ val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
+ val addWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
val wrap: Proof.context -> (int -> tactic) -> int -> tactic
val intro_bang: int option -> attribute
@@ -68,8 +68,9 @@
{next: int,
rules: (int * ((int * bool) * thm)) list,
netpairs: netpair list,
- wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
- (((int -> tactic) -> int -> tactic) * stamp) list};
+ wrappers:
+ ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
+ ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list};
fun make_rules next rules netpairs wrappers =
Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
@@ -170,7 +171,7 @@
fun gen_wrap which ctxt =
let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt)
- in fold_rev fst (which wrappers) end;
+ in fold_rev (fn (w, _) => w ctxt) (which wrappers) end;
val Swrap = gen_wrap #1;
val wrap = gen_wrap #2;
--- a/src/ZF/Tools/inductive_package.ML Sat Apr 27 11:37:50 2013 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Apr 27 20:50:20 2013 +0200
@@ -231,7 +231,7 @@
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
type_elims)
- ORELSE' hyp_subst_tac)),
+ ORELSE' hyp_subst_tac ctxt1)),
if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
else all_tac,
DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
@@ -254,7 +254,7 @@
(*Breaks down logical connectives in the monotonic function*)
val basic_elim_tac =
REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
- ORELSE' bound_hyp_subst_tac))
+ ORELSE' bound_hyp_subst_tac ctxt1))
THEN prune_params_tac
(*Mutual recursion: collapse references to Part(D,h)*)
THEN (PRIMITIVE (fold_rule part_rec_defs));
@@ -348,7 +348,7 @@
(*Now break down the individual cases. No disjE here in case
some premise involves disjunction.*)
REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
- ORELSE' bound_hyp_subst_tac)),
+ ORELSE' (bound_hyp_subst_tac ctxt1))),
ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
val dummy =