author wenzelm Thu, 20 Mar 2014 23:13:33 +0100 changeset 56235 083b41092afe parent 56226 29fd6bd9228e (current diff) parent 56234 59662ce44f02 (diff) child 56236 713ae0c9e652
merged
```--- a/NEWS	Thu Mar 20 09:21:39 2014 -0700
+++ b/NEWS	Thu Mar 20 23:13:33 2014 +0100
@@ -25,6 +25,15 @@
supports input methods via ` (backquote), or << and >> (double angle
brackets).

+* More static checking of proof methods, which allows the system to
+form a closure over the concrete syntax.  Method arguments should be
+processed in the original proof context as far as possible, before
+operating on the goal state.  In any case, the standard discipline for
+subgoal-addressing needs to be observed: no subgoals or a subgoal
+number that is out of range produces an empty result sequence, not an
+exception.  Potential INCOMPATIBILITY for non-conformant tactical
+proof tools.
+

*** Prover IDE -- Isabelle/Scala/jEdit ***
```
```--- a/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 20 23:13:33 2014 +0100
@@ -18,9 +18,10 @@

lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
proof -
-  have "c + inf a b = inf (c+a) (c+b)"
+  have "c + inf a b = inf (c + a) (c + b)"
+  then show ?thesis
qed

end
@@ -37,10 +38,12 @@
done

-lemma add_sup_distrib_right: "sup a b + c = sup (a+c) (b+c)"
+lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
proof -
-  have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
+  have "c + sup a b = sup (c+a) (c+b)"
+  then show ?thesis
qed

end
@@ -54,10 +57,10 @@

-lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
+lemma inf_eq_neg_sup: "inf a b = - sup (- a) (- b)"
proof (rule inf_unique)
fix a b c :: 'a
-  show "- sup (-a) (-b) \<le> a"
+  show "- sup (- a) (- b) \<le> a"
by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
show "- sup (-a) (-b) \<le> b"
@@ -68,26 +71,27 @@
by (subst neg_le_iff_le [symmetric]) (simp add: le_supI)
qed

-lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)"
+lemma sup_eq_neg_inf: "sup a b = - inf (- a) (- b)"
proof (rule sup_unique)
fix a b c :: 'a
-  show "a \<le> - inf (-a) (-b)"
+  show "a \<le> - inf (- a) (- b)"
by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
-  show "b \<le> - inf (-a) (-b)"
+  show "b \<le> - inf (- a) (- b)"
by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
assume "a \<le> c" "b \<le> c"
-  then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
+  then show "- inf (- a) (- b) \<le> c"
+    by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
qed

-lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
+lemma neg_inf_eq_sup: "- inf a b = sup (- a) (- b)"

lemma diff_inf_eq_sup: "a - inf b c = a + sup (- b) (- c)"
using neg_inf_eq_sup [of b c, symmetric] by simp

-lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
+lemma neg_sup_eq_inf: "- sup a b = inf (- a) (- b)"

lemma diff_sup_eq_inf: "a - sup b c = a + inf (- b) (- c)"
@@ -95,13 +99,14 @@

lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
proof -
-  have "0 = - inf 0 (a-b) + inf (a-b) 0"
+  have "0 = - inf 0 (a - b) + inf (a - b) 0"
-  hence "0 = sup 0 (b-a) + inf (a-b) 0"
+  then have "0 = sup 0 (b - a) + inf (a - b) 0"
-  hence "0 = (-a + sup a b) + (inf a b + (-b))"
+  then have "0 = (- a + sup a b) + (inf a b + (- b))"
-  then show ?thesis by (simp add: algebra_simps)
+  then show ?thesis
qed

@@ -115,10 +120,13 @@

lemma pprt_neg: "pprt (- x) = - nprt x"
proof -
-  have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero ..
-  also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup ..
+  have "sup (- x) 0 = sup (- x) (- 0)"
+    unfolding minus_zero ..
+  also have "\<dots> = - inf x 0"
+    unfolding neg_inf_eq_sup ..
finally have "sup (- x) 0 = - inf x 0" .
-  then show ?thesis unfolding pprt_def nprt_def .
+  then show ?thesis
+    unfolding pprt_def nprt_def .
qed

lemma nprt_neg: "nprt (- x) = - pprt x"
@@ -172,20 +180,26 @@
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
proof -
{
-    fix a::'a
-    assume hyp: "sup a (-a) = 0"
-    hence "sup a (-a) + a = a" by (simp)
-    hence "sup (a+a) 0 <= a" by (simp)
-    hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
+    fix a :: 'a
+    assume hyp: "sup a (- a) = 0"
+    then have "sup a (- a) + a = a"
+      by simp
+    then have "sup (a + a) 0 = a"
+    then have "sup (a + a) 0 \<le> a"
+      by simp
+    then have "0 \<le> a"
+      by (blast intro: order_trans inf_sup_ord)
}
note p = this
assume hyp:"sup a (-a) = 0"
-  hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
-  from p[OF hyp] p[OF hyp2] show "a = 0" by simp
+  then have hyp2:"sup (-a) (-(-a)) = 0"
+  from p[OF hyp] p[OF hyp2] show "a = 0"
+    by simp
qed

-lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0"
+lemma inf_0_imp_0: "inf a (- a) = 0 \<Longrightarrow> a = 0"
apply (erule sup_0_imp_0)
@@ -206,24 +220,32 @@
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
proof
-  assume "0 <= a + a"
-  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
-  have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
+  assume "0 \<le> a + a"
+  then have a: "inf (a + a) 0 = 0"
+    by (simp add: inf_commute inf_absorb1)
+  have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
-  hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
-  hence "inf a 0 = 0" by (simp only: add_right_cancel)
-  then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
+  then have "?l = 0 + inf a 0"
+  then have "inf a 0 = 0"
+  then show "0 \<le> a"
+    unfolding le_iff_inf by (simp add: inf_commute)
next
-  assume a: "0 <= a"
-  show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
+  assume a: "0 \<le> a"
+  show "0 \<le> a + a"
qed

lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
proof
assume assm: "a + a = 0"
-  then have "a + a + - a = - a" by simp
-  then have "a + (a + - a) = - a" by (simp only: add_assoc)
-  then have a: "- a = a" by simp
+  then have "a + a + - a = - a"
+    by simp
+  then have "a + (a + - a) = - a"
+  then have a: "- a = a"
+    by simp
show "a = 0"
apply (rule antisym)
apply (unfold neg_le_iff_le [symmetric, of a])
@@ -236,7 +258,8 @@
done
next
assume "a = 0"
-  then show "a + a = 0" by simp
+  then show "a + a = 0"
+    by simp
qed

lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
@@ -261,19 +284,23 @@
"a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
proof -
-  have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
+  have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)"
+    by (subst le_minus_iff, simp)
moreover have "\<dots> \<longleftrightarrow> a \<le> 0"
-  ultimately show ?thesis by blast
+  ultimately show ?thesis
+    by blast
qed

"a + a < 0 \<longleftrightarrow> a < 0"
proof -
-  have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
+  have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)"
+    by (subst less_minus_iff) simp
moreover have "\<dots> \<longleftrightarrow> a < 0"
-  ultimately show ?thesis by blast
+  ultimately show ?thesis
+    by blast
qed

declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp]
@@ -281,17 +308,19 @@
lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
proof -
from add_le_cancel_left [of "uminus a" "plus a a" zero]
-  have "(a <= -a) = (a+a <= 0)"
+  have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
-  thus ?thesis by simp
+  then show ?thesis
+    by simp
qed

lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
proof -
from add_le_cancel_left [of "uminus a" zero "plus a a"]
-  have "(-a <= a) = (0 <= a+a)"
+  have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
-  thus ?thesis by simp
+  then show ?thesis
+    by simp
qed

lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
@@ -314,7 +343,8 @@

end

@@ -325,11 +355,15 @@
proof -
have "0 \<le> \<bar>a\<bar>"
proof -
-    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
-    show ?thesis by (rule add_mono [OF a b, simplified])
+    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>"
+      by (auto simp add: abs_lattice)
+    show ?thesis
+      by (rule add_mono [OF a b, simplified])
qed
-  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
-  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
+  then have "0 \<le> sup a (- a)"
+    unfolding abs_lattice .
+  then have "sup (sup a (- a)) 0 = sup a (- a)"
+    by (rule sup_absorb1)
then show ?thesis
qed
@@ -347,7 +381,8 @@
have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
fix a b
-  show "0 \<le> \<bar>a\<bar>" by simp
+  show "0 \<le> \<bar>a\<bar>"
+    by simp
show "a \<le> \<bar>a\<bar>"
show "\<bar>-a\<bar> = \<bar>a\<bar>"
@@ -359,14 +394,20 @@
}
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
proof -
-    have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
+    have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
+      (is "_=sup ?m ?n")
-    have a: "a + b <= sup ?m ?n" by simp
-    have b: "- a - b <= ?n" by simp
-    have c: "?n <= sup ?m ?n" by simp
-    from b c have d: "-a-b <= sup ?m ?n" by (rule order_trans)
-    have e:"-a-b = -(a+b)" by simp
-    from a d e have "abs(a+b) <= sup ?m ?n"
+    have a: "a + b \<le> sup ?m ?n"
+      by simp
+    have b: "- a - b \<le> ?n"
+      by simp
+    have c: "?n \<le> sup ?m ?n"
+      by simp
+    from b c have d: "- a - b \<le> sup ?m ?n"
+      by (rule order_trans)
+    have e: "- a - b = - (a + b)"
+      by simp
+    from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
apply -
apply (drule abs_leI)
apply (simp_all only: algebra_simps ac_simps minus_add)
@@ -379,7 +420,7 @@
end

lemma sup_eq_if:
-  fixes a :: "'a\<Colon>{lattice_ab_group_add, linorder}"
+  fixes a :: "'a::{lattice_ab_group_add, linorder}"
shows "sup a (- a) = (if a < 0 then - a else a)"
proof -
note add_le_cancel_right [of a a "- a", symmetric, simplified]
@@ -388,18 +429,23 @@
qed

lemma abs_if_lattice:
-  fixes a :: "'a\<Colon>{lattice_ab_group_add_abs, linorder}"
+  fixes a :: "'a::{lattice_ab_group_add_abs, linorder}"
shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
by auto

lemma estimate_by_abs:
-  "a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b"
+  fixes a b c :: "'a::lattice_ab_group_add_abs"
+  shows "a + b \<le> c \<Longrightarrow> a \<le> c + \<bar>b\<bar>"
proof -
-  assume "a+b <= c"
-  then have "a <= c+(-b)" by (simp add: algebra_simps)
-  have "(-b) <= abs b" by (rule abs_ge_minus_self)
-  then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
-  with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
+  assume "a + b \<le> c"
+  then have "a \<le> c + (- b)"
+  have "- b \<le> \<bar>b\<bar>"
+    by (rule abs_ge_minus_self)
+  then have "c + (- b) \<le> c + \<bar>b\<bar>"
+  with `a \<le> c + (- b)` show ?thesis
+    by (rule order_trans)
qed

class lattice_ring = ordered_ring + lattice_ab_group_add_abs
@@ -410,15 +456,17 @@

end

-lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lattice_ring))"
+lemma abs_le_mult:
+  fixes a b :: "'a::lattice_ring"
+  shows "\<bar>a * b\<bar> \<le> \<bar>a\<bar> * \<bar>b\<bar>"
proof -
let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
-  have a: "(abs a) * (abs b) = ?x"
+  have a: "\<bar>a\<bar> * \<bar>b\<bar> = ?x"
by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
{
fix u v :: 'a
-    have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>
+    have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
u * v = pprt a * pprt b + pprt a * nprt b +
nprt a * pprt b + nprt a * nprt b"
apply (subst prts[of u], subst prts[of v])
@@ -426,16 +474,22 @@
done
}
note b = this[OF refl[of a] refl[of b]]
-  have xy: "- ?x <= ?y"
+  have xy: "- ?x \<le> ?y"
apply simp
+      mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
done
-  have yx: "?y <= ?x"
+  have yx: "?y \<le> ?x"
apply simp
+      mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
done
-  have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
-  have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
+  have i1: "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>"
+    by (simp only: a b yx)
+  have i2: "- (\<bar>a\<bar> * \<bar>b\<bar>) \<le> a * b"
+    by (simp only: a b xy)
show ?thesis
apply (rule abs_leI)
@@ -445,37 +499,38 @@

instance lattice_ring \<subseteq> ordered_ring_abs
proof
-  fix a b :: "'a\<Colon> lattice_ring"
+  fix a b :: "'a::lattice_ring"
assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
-  show "abs (a*b) = abs a * abs b"
+  show "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
proof -
-    have s: "(0 <= a*b) | (a*b <= 0)"
-      apply (auto)
+    have s: "(0 \<le> a * b) \<or> (a * b \<le> 0)"
+      apply auto
apply (rule_tac split_mult_pos_le)
-      apply (rule_tac contrapos_np[of "a*b <= 0"])
-      apply (simp)
+      apply (rule_tac contrapos_np[of "a * b \<le> 0"])
+      apply simp
apply (rule_tac split_mult_neg_le)
-      apply (insert a)
-      apply (blast)
+      using a
+      apply blast
done
have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
show ?thesis
-    proof cases
-      assume "0 <= a * b"
+    proof (cases "0 \<le> a * b")
+      case True
then show ?thesis
-        apply (insert a)
+        using a
algebra_simps
iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
-          apply(drule (1) mult_nonneg_nonpos[of a b], simp)
-          apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
+        apply(drule (1) mult_nonneg_nonpos[of a b], simp)
+        apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
done
next
-      assume "~(0 <= a*b)"
-      with s have "a*b <= 0" by simp
+      case False
+      with s have "a * b \<le> 0"
+        by simp
then show ?thesis
apply (insert a)
@@ -488,11 +543,12 @@
qed

lemma mult_le_prts:
-  assumes "a1 <= (a::'a::lattice_ring)"
-    and "a <= a2"
-    and "b1 <= b"
-    and "b <= b2"
-  shows "a * b <=
+  fixes a b :: "'a::lattice_ring"
+  assumes "a1 \<le> a"
+    and "a \<le> a2"
+    and "b1 \<le> b"
+    and "b \<le> b2"
+  shows "a * b \<le>
pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
proof -
have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
@@ -501,31 +557,31 @@
done
then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
-  moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
+  moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2"
-  moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
+  moreover have "pprt a * nprt b \<le> pprt a1 * nprt b2"
proof -
-    have "pprt a * nprt b <= pprt a * nprt b2"
+    have "pprt a * nprt b \<le> pprt a * nprt b2"
-    moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
+    moreover have "pprt a * nprt b2 \<le> pprt a1 * nprt b2"
ultimately show ?thesis
by simp
qed
-  moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
+  moreover have "nprt a * pprt b \<le> nprt a2 * pprt b1"
proof -
-    have "nprt a * pprt b <= nprt a2 * pprt b"
+    have "nprt a * pprt b \<le> nprt a2 * pprt b"
-    moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
+    moreover have "nprt a2 * pprt b \<le> nprt a2 * pprt b1"
ultimately show ?thesis
by simp
qed
-  moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
+  moreover have "nprt a * nprt b \<le> nprt a1 * nprt b1"
proof -
-    have "nprt a * nprt b <= nprt a * nprt b1"
+    have "nprt a * nprt b \<le> nprt a * nprt b1"
-    moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
+    moreover have "nprt a * nprt b1 \<le> nprt a1 * nprt b1"
ultimately show ?thesis
by simp
@@ -537,36 +593,41 @@
qed

lemma mult_ge_prts:
-  assumes "a1 <= (a::'a::lattice_ring)"
-    and "a <= a2"
-    and "b1 <= b"
-    and "b <= b2"
-  shows "a * b >=
+  fixes a b :: "'a::lattice_ring"
+  assumes "a1 \<le> a"
+    and "a \<le> a2"
+    and "b1 \<le> b"
+    and "b \<le> b2"
+  shows "a * b \<ge>
nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
proof -
-  from assms have a1:"- a2 <= -a"
+  from assms have a1: "- a2 \<le> -a"
by auto
-  from assms have a2: "-a <= -a1"
+  from assms have a2: "- a \<le> -a1"
by auto
-  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
-  have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1"
+  from mult_le_prts[of "- a2" "- a" "- a1" "b1" b "b2",
+    OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
+  have le: "- (a * b) \<le> - nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
+    - pprt a1 * pprt b1 + - pprt a2 * nprt b1"
by simp
-  then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
+  then have "- (- nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
+      - pprt a1 * pprt b1 + - pprt a2 * nprt b1) \<le> a * b"
by (simp only: minus_le_iff)
-  then show ?thesis by (simp add: algebra_simps)
+  then show ?thesis
qed

instance int :: lattice_ring
proof
fix k :: int
-  show "abs k = sup k (- k)"
+  show "\<bar>k\<bar> = sup k (- k)"
qed

instance real :: lattice_ring
proof
fix a :: real
-  show "abs a = sup a (- a)"
+  show "\<bar>a\<bar> = sup a (- a)"
qed
```
```--- a/src/HOL/Nominal/Nominal.thy	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 20 23:13:33 2014 +0100
@@ -3638,13 +3638,15 @@
(* tactics for generating fresh names and simplifying fresh_funs *)
ML_file "nominal_fresh_fun.ML"

-method_setup generate_fresh =
-  {* setup_generate_fresh *}
-  {* tactic to generate a name fresh for all the variables in the goal *}
-
-method_setup fresh_fun_simp =
-  {* setup_fresh_fun_simp *}
-  {* tactic to delete one inner occurence of fresh_fun *}
+method_setup generate_fresh = {*
+  Args.type_name {proper = true, strict = true} >>
+    (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s))
+*} "generate a name fresh for all the variables in the goal"
+
+method_setup fresh_fun_simp = {*
+  Scan.lift (Args.parens (Args.\$\$\$ "no_asm") >> K true || Scan.succeed false) >>
+    (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))
+*} "delete one inner occurence of fresh_fun"

(************************************************)```
```--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -5,7 +5,7 @@
a tactic to analyse instances of the fresh_fun.
*)

-(* FIXME proper ML structure *)
+(* FIXME proper ML structure! *)

(* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)

@@ -52,12 +52,11 @@
(* A tactic to generate a name fresh for  all the free *)
(* variables and parameters of the goal                *)

-fun generate_fresh_tac atom_name i thm =
+fun generate_fresh_tac ctxt atom_name = SUBGOAL (fn (goal, _) =>
let
-   val thy = theory_of_thm thm;
+   val thy = Proof_Context.theory_of ctxt;
(* the parsing function returns a qualified name, we get back the base name *)
val atom_basename = Long_Name.base_name atom_name;
-   val goal = nth (prems_of thm) (i - 1);
val ps = Logic.strip_params goal;
val Ts = rev (map snd ps);
fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
@@ -76,11 +75,12 @@
(* find the variable we want to instantiate *)
val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
in
+   fn st =>
(cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
rtac fs_name_thm 1 THEN
-   etac exE 1) thm
-  handle List.Empty  => all_tac thm (* if we collected no variables then we do nothing *)
-  end;
+   etac exE 1) st
+  handle List.Empty  => all_tac st (* if we collected no variables then we do nothing *)
+ end) 1;

fun get_inner_fresh_fun (Bound j) = NONE
| get_inner_fresh_fun (v as Free _) = NONE
@@ -97,15 +97,14 @@
(* This tactic generates a fresh name of the atom type *)
(* given by the innermost fresh_fun                    *)

-fun generate_fresh_fun_tac i thm =
+fun generate_fresh_fun_tac ctxt = SUBGOAL (fn (goal, _) =>
let
-    val goal = nth (prems_of thm) (i - 1);
val atom_name_opt = get_inner_fresh_fun goal;
in
case atom_name_opt of
-    NONE => all_tac thm
-  | SOME atom_name  => generate_fresh_tac atom_name i thm
-  end
+    NONE => all_tac
+  | SOME atom_name  => generate_fresh_tac ctxt atom_name
+  end) 1;

(* Two substitution tactics which looks for the innermost occurence in
one assumption or in the conclusion *)
@@ -123,24 +122,23 @@
curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux
(1 upto Thm.nprems_of th)))))) ctxt th;

-fun fresh_fun_tac ctxt no_asm i thm =
+fun fresh_fun_tac ctxt no_asm = SUBGOAL (fn (goal, i) =>
(* Find the variable we instantiate *)
let
-    val thy = theory_of_thm thm;
+    val thy = Proof_Context.theory_of ctxt;
val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
val simp_ctxt =
val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
-    val goal = nth (prems_of thm) (i-1);
val atom_name_opt = get_inner_fresh_fun goal;
val n = length (Logic.strip_params goal);
(* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
(* is the last one in the list, the inner one *)
in
case atom_name_opt of
-    NONE => all_tac thm
+    NONE => all_tac
| SOME atom_name =>
let
val atom_basename = Long_Name.base_name atom_name;
@@ -173,21 +171,7 @@
(subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i)))
ORELSE
(subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st
-  end)) thm
-
+  end))
end
-  end
+  end)

-(* syntax for options, given "(no_asm)" will give back true, without
-   gives back false *)
-val options_syntax =
-    (Args.parens (Args.\$\$\$ "no_asm") >> (K true)) ||
-     (Scan.succeed false);
-
-fun setup_generate_fresh x =
-  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
-    (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
-
-fun setup_fresh_fun_simp x =
-  (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x;
-```
```--- a/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -142,7 +142,7 @@
(* stac contains the simplifiation tactic that is *)
(* applied (see (no_asm) options below            *)
fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i =
-    ("general simplification of permutations", fn st =>
+    ("general simplification of permutations", fn st => SUBGOAL (fn _ =>
let
val ctxt' = ctxt
addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
@@ -150,8 +150,8 @@
|> fold Simplifier.del_cong weak_congs
in
-      stac ctxt' i st
-    end);
+      stac ctxt' i
+    end) i st);

(* general simplification of permutations and permutation that arose from eqvt-problems *)
fun perm_simp stac ctxt = ```
```--- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -174,7 +174,7 @@

(** The Main Function **)

-fun lex_order_tac quiet ctxt solve_tac (st: thm) =
+fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
val ((_ \$ (_ \$ rel)) :: tl) = prems_of st
@@ -187,26 +187,27 @@
val table = (* 2: create table *)
map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
in
-    case search_table table of
-      NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
-    | SOME order =>
-      let
-        val clean_table = map (fn x => map (nth x) order) table
-        val relation = mk_measures domT (map (nth measure_funs) order)
-        val _ =
-          if not quiet then
-            Pretty.writeln (Pretty.block
-              [Pretty.str "Found termination order:", Pretty.brk 1,
-                Pretty.quote (Syntax.pretty_term ctxt relation)])
-          else ()
-
-      in (* 4: proof reconstruction *)
-        st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
-        THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
-        THEN (rtac @{thm "wf_empty"} 1)
-        THEN EVERY (map prove_row clean_table))
-      end
-  end
+    fn st =>
+      case search_table table of
+        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
+      | SOME order =>
+        let
+          val clean_table = map (fn x => map (nth x) order) table
+          val relation = mk_measures domT (map (nth measure_funs) order)
+          val _ =
+            if not quiet then
+              Pretty.writeln (Pretty.block
+                [Pretty.str "Found termination order:", Pretty.brk 1,
+                  Pretty.quote (Syntax.pretty_term ctxt relation)])
+            else ()
+
+        in (* 4: proof reconstruction *)
+          st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
+          THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+          THEN (rtac @{thm "wf_empty"} 1)
+          THEN EVERY (map prove_row clean_table))
+        end
+  end) 1 st;

fun lexicographic_order_tac quiet ctxt =
TRY (Function_Common.apply_termination_rule ctxt 1) THEN```
```--- a/src/HOL/Tools/Function/termination.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Tools/Function/termination.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -272,10 +272,10 @@

in

-fun wf_union_tac ctxt st =
+fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
-    val cert = cterm_of (theory_of_thm st)
+    val cert = cterm_of thy
val ((_ \$ (_ \$ rel)) :: ineqs) = prems_of st

fun mk_compr ineq =
@@ -304,8 +304,8 @@
in
(PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
-     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
-  end
+     THEN rewrite_goal_tac ctxt Un_aci_simps 1)  (* eliminate duplicates *)
+  end) 1 st

end
```
```--- a/src/HOL/Tools/coinduction.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Tools/coinduction.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -40,19 +40,20 @@
(THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
end;

-fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
+fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
let
val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
fun find_coinduct t =
Induct.find_coinductP ctxt t @
(try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
-    val raw_thm = case opt_raw_thm
-      of SOME raw_thm => raw_thm
-       | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
+    val raw_thm =
+      (case opt_raw_thm of
+        SOME raw_thm => raw_thm
+      | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
val cases = Rule_Cases.get raw_thm |> fst
in
Object_Logic.rulify_tac ctxt THEN'
Method.insert_tac prems THEN'
Object_Logic.atomize_prems_tac ctxt THEN'
@@ -110,10 +111,10 @@
unfold_thms_tac ctxt eqs
end)) ctxt)))])
end) ctxt) THEN'
-      K (prune_params_tac ctxt))) st
-    |> Seq.maps (fn (_, st) =>
+      K (prune_params_tac ctxt))
+    #> Seq.maps (fn st =>
CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
-  end;
+  end));

local
```
```--- a/src/HOL/Topological_Spaces.thy	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Topological_Spaces.thy	Thu Mar 20 23:13:33 2014 +0100
@@ -373,7 +373,7 @@
qed

ML {*
-  fun eventually_elim_tac ctxt thms thm =
+  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
let
val thy = Proof_Context.theory_of ctxt
val mp_thms = thms RL [@{thm eventually_rev_mp}]
@@ -381,11 +381,11 @@
(@{thm allI} RS @{thm always_eventually})
|> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
|> fold (fn _ => fn thm => @{thm impI} RS thm) thms
-      val cases_prop = prop_of (raw_elim_thm RS thm)
+      val cases_prop = prop_of (raw_elim_thm RS st)
val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
in
-      CASES cases (rtac raw_elim_thm 1) thm
-    end
+      CASES cases (rtac raw_elim_thm 1)
+    end) 1
*}

method_setup eventually_elim = {*```
```--- a/src/HOL/ex/Antiquote.thy	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/ex/Antiquote.thy	Thu Mar 20 23:13:33 2014 +0100
@@ -13,14 +13,14 @@
syntax.
*}

-definition var :: "'a => ('a => nat) => nat"  ("VAR _" [1000] 999)
+definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"  ("VAR _" [1000] 999)
where "var x env = env x"

-definition Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
+definition Expr :: "(('a \<Rightarrow> nat) \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
where "Expr exp env = exp env"

syntax
-  "_Expr" :: "'a => 'a"  ("EXPR _" [1000] 999)
+  "_Expr" :: "'a \<Rightarrow> 'a"  ("EXPR _" [1000] 999)

parse_translation {*
[Syntax_Trans.quote_antiquote_tr```
```--- a/src/HOL/ex/Multiquote.thy	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/ex/Multiquote.thy	Thu Mar 20 23:13:33 2014 +0100
@@ -14,8 +14,8 @@
*}

syntax
-  "_quote" :: "'b => ('a => 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
-  "_antiquote" :: "('a => 'b) => 'b"    ("\<acute>_" [1000] 1000)
+  "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
+  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"    ("\<acute>_" [1000] 1000)

parse_translation {*
let
@@ -43,8 +43,8 @@

term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
-term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>"
-term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>"
-term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>"
+term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f \<circ> \<acute>g)\<guillemotright>\<guillemotright>"

end```
```--- a/src/Pure/Isar/method.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/Pure/Isar/method.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -64,7 +64,6 @@
val finish_text: text option * bool -> text
val print_methods: Proof.context -> unit
val check_name: Proof.context -> xstring * Position.T -> string
-  val check_src: Proof.context -> src -> src
val method: Proof.context -> src -> Proof.context -> method
val method_cmd: Proof.context -> src -> Proof.context -> method
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
@@ -339,7 +338,7 @@
(* check *)

fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-fun check_src ctxt src = #1 (Args.check_src ctxt (get_methods ctxt) src);
+fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;

(* get methods *)
@@ -348,7 +347,14 @@
let val table = get_methods ctxt
in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;

-fun method_cmd ctxt = method ctxt o check_src ctxt;
+fun method_closure ctxt src0 =
+  let
+    val (src1, meth) = check_src ctxt src0;
+    val src2 = Args.init_assignable src1;
+    val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
+  in Args.closure src2 end;
+
+fun method_cmd ctxt = method ctxt o method_closure ctxt;

(* method setup *)```
```--- a/src/Pure/Isar/rule_cases.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/Pure/Isar/rule_cases.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -12,7 +12,7 @@
type cases_tactic
val CASES: cases -> tactic -> cases_tactic
val NO_CASES: tactic -> cases_tactic
-  val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
+  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
end

@@ -190,7 +190,7 @@

fun SUBGOAL_CASES tac i st =
(case try Logic.nth_prem (i, Thm.prop_of st) of
-    SOME goal => tac (goal, i) st
+    SOME goal => tac (goal, i, st) st
| NONE => Seq.empty);

fun (tac1 THEN_ALL_NEW_CASES tac2) i st =```
```--- a/src/Pure/ML/ml_context.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -191,3 +191,7 @@

end;

+fun use s =
+  ML_Context.eval_file true (Path.explode s)
+    handle ERROR msg => (writeln msg; error "ML error");
+```
```--- a/src/Pure/ROOT.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/Pure/ROOT.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -226,7 +226,6 @@
(*ML with context and antiquotations*)
use "ML/ml_context.ML";
use "ML/ml_antiquotation.ML";
-val use = ML_Context.eval_file true o Path.explode;
(*^^^^^ end of ML bootstrap 1 ^^^^^*)

(*basic proof engine*)```
```--- a/src/Pure/pure_thy.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/Pure/pure_thy.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -20,6 +20,8 @@
val tycon = Lexicon.mark_type;
val const = Lexicon.mark_const;

+val qualify = Binding.qualify true Context.PureN;
+

(* application syntax variants *)

@@ -207,11 +209,11 @@
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
+   [(qualify (Binding.name "term"), typ "'a => prop", NoSyn),
+    (qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn),
+    (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
#> Sign.local_path
-   [(Binding.name "term", typ "'a => prop", NoSyn),
-    (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
-    (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
#> (Global_Theory.add_defs false o map Thm.no_attributes)
[(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
(Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
@@ -219,9 +221,6 @@
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
\ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
(Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
-  #> Sign.hide_const false "Pure.term"
-  #> Sign.hide_const false "Pure.sort_constraint"
-  #> Sign.hide_const false "Pure.conjunction"
#> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
#> fold (fn (a, prop) =>
snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);```
```--- a/src/Pure/tactical.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/Pure/tactical.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -334,15 +334,14 @@
(*Returns all states that have changed in subgoal i, counted from the LAST
subgoal.  For stac, for example.*)
fun CHANGED_GOAL tac i st =
-    let val np = Thm.nprems_of st
-        val d = np-i                 (*distance from END*)
-        val t = Thm.term_of (Thm.cprem_of st i)
-        fun diff st' =
-            Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
-            orelse
-             not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
-    in  Seq.filter diff (tac i st)  end
-    handle General.Subscript => Seq.empty  (*no subgoal i*);
+  SUBGOAL (fn (t, _) =>
+    let
+      val np = Thm.nprems_of st;
+      val d = np - i;  (*distance from END*)
+      fun diff st' =
+        Thm.nprems_of st' - d <= 0 orelse  (*the subgoal no longer exists*)
+        not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));
+    in Seq.filter diff o tac i end) i st;

(*Returns all states where some subgoals have been solved.  For
subgoal-based tactics this means subgoal i has been solved```
```--- a/src/Tools/induct.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/Tools/induct.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -741,71 +741,71 @@
type case_data = (((string * string list) * string list) list * int);

fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-
-    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
-
-    fun inst_rule (concls, r) =
-      (if null insts then `Rule_Cases.get r
-       else (align_left "Rule has fewer conclusions than arguments given"
-          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
-        |> maps (prep_inst ctxt align_right (atomize_term thy))
-        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
-      |> mod_cases thy
-      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
-
-    val ruleq =
-      (case opt_rule of
-        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
-      | NONE =>
-          (get_inductP ctxt facts @
-            map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
-          |> map_filter (Rule_Cases.mutual_rule ctxt)
-          |> tap (trace_rules ctxt inductN o map #2)
-          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-
-    fun rule_cases ctxt rule cases =
-      let
-        val rule' = Rule_Cases.internalize_params rule;
-        val rule'' = rule' |> simp ? simplified_rule ctxt;
-        val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
-        val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
-      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
-  in
-    (fn i => fn st =>
-      ruleq
-      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
-      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
-        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
-          (CONJUNCTS (ALLGOALS
-            let
-              val adefs = nth_list atomized_defs (j - 1);
-              val xs = nth_list arbitrary (j - 1);
-              val k = nth concls (j - 1) + more_consumes
-            in
-              Method.insert_tac (more_facts @ adefs) THEN'
-                (if simp then
-                   rotate_tac k (length adefs) THEN'
-                   arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
-                 else
-                   arbitrary_tac defs_ctxt k xs)
-             end)
-          THEN' inner_atomize_tac defs_ctxt) j))
-        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
-            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
-            |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
-            |> Seq.maps (fn rule' =>
-              CASES (rule_cases ctxt rule' cases)
-                (rtac rule' i THEN
-                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
-    THEN_ALL_NEW_CASES
-      ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
-        else K all_tac)
-       THEN_ALL_NEW rulify_tac ctxt)
-  end;
+  SUBGOAL_CASES (fn (_, i, st) =>
+    let
+      val thy = Proof_Context.theory_of ctxt;
+
+      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
+      val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
+
+      fun inst_rule (concls, r) =
+        (if null insts then `Rule_Cases.get r
+         else (align_left "Rule has fewer conclusions than arguments given"
+            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
+          |> maps (prep_inst ctxt align_right (atomize_term thy))
+          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+        |> mod_cases thy
+        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
+
+      val ruleq =
+        (case opt_rule of
+          SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
+        | NONE =>
+            (get_inductP ctxt facts @
+              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
+            |> map_filter (Rule_Cases.mutual_rule ctxt)
+            |> tap (trace_rules ctxt inductN o map #2)
+            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
+
+      fun rule_cases ctxt rule cases =
+        let
+          val rule' = Rule_Cases.internalize_params rule;
+          val rule'' = rule' |> simp ? simplified_rule ctxt;
+          val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
+          val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
+        in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
+    in
+      fn st =>
+        ruleq
+        |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
+        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
+          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
+            (CONJUNCTS (ALLGOALS
+              let
+                val adefs = nth_list atomized_defs (j - 1);
+                val xs = nth_list arbitrary (j - 1);
+                val k = nth concls (j - 1) + more_consumes
+              in
+                Method.insert_tac (more_facts @ adefs) THEN'
+                  (if simp then
+                     rotate_tac k (length adefs) THEN'
+                     arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
+                   else
+                     arbitrary_tac defs_ctxt k xs)
+               end)
+            THEN' inner_atomize_tac defs_ctxt) j))
+          THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
+              guess_instance ctxt (internalize ctxt more_consumes rule) i st'
+              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
+              |> Seq.maps (fn rule' =>
+                CASES (rule_cases ctxt rule' cases)
+                  (rtac rule' i THEN
+                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
+      end)
+      THEN_ALL_NEW_CASES
+        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
+         THEN_ALL_NEW rulify_tac ctxt);

val induct_tac = gen_induct_tac (K I);

@@ -832,7 +832,7 @@

in

-fun coinduct_tac ctxt inst taking opt_rule facts =
+fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
let
val thy = Proof_Context.theory_of ctxt;

@@ -849,7 +849,7 @@
|> tap (trace_rules ctxt coinductN)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
in
-    SUBGOAL_CASES (fn (goal, i) => fn st =>
+    fn st =>
ruleq goal
|> Seq.maps (Rule_Cases.consume ctxt [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
@@ -858,8 +858,8 @@
|> Seq.maps (fn rule' =>
CASES (Rule_Cases.make_common (thy,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            (Method.insert_tac more_facts i THEN rtac rule' i) st)))
-  end;
+            (Method.insert_tac more_facts i THEN rtac rule' i) st))
+  end);

end;
```
```--- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 23:13:33 2014 +0100
@@ -89,7 +89,7 @@
(2) exhaustion works for VARIABLES in the premises, not general terms
**)

-fun exhaust_induct_tac exh ctxt var i state =
+fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
@@ -102,12 +102,12 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
-    eres_inst_tac ctxt [(ixn, var)] rule i state
+    eres_inst_tac ctxt [(ixn, var)] rule i
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
-                case_tac ctxt var i state
-            else error msg;
+                case_tac ctxt var i
+            else error msg) i state;

val exhaust_tac = exhaust_induct_tac true;
val induct_tac = exhaust_induct_tac false;```