--- 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)"
by (simp add: add_inf_distrib_left)
- thus ?thesis by (simp add: add_commute)
+ then show ?thesis
+ by (simp add: add_commute)
qed
end
@@ -37,10 +38,12 @@
apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
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)
- thus ?thesis by (simp add: add_commute)
+ have "c + sup a b = sup (c+a) (c+b)"
+ by (simp add: add_sup_distrib_left)
+ then show ?thesis
+ by (simp add: add_commute)
qed
end
@@ -54,10 +57,10 @@
lemmas add_sup_inf_distribs =
add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
-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)"])
(simp, simp add: add_sup_distrib_left)
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)"])
(simp, simp add: add_inf_distrib_left)
- 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)"])
(simp, simp add: add_inf_distrib_left)
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)"
by (simp add: inf_eq_neg_sup)
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)"
by (simp add: sup_eq_neg_inf)
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"
by (simp add: inf_commute)
- hence "0 = sup 0 (b-a) + inf (a-b) 0"
+ then have "0 = sup 0 (b - a) + inf (a - b) 0"
by (simp add: inf_eq_neg_sup)
- hence "0 = (-a + sup a b) + (inf a b + (-b))"
+ then have "0 = (- a + sup a b) + (inf a b + (- b))"
by (simp only: add_sup_distrib_left add_inf_distrib_right) simp
- then show ?thesis by (simp add: algebra_simps)
+ then show ?thesis
+ by (simp add: algebra_simps)
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 add: add_sup_distrib_right)
- 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"
+ by (simp add: add_sup_distrib_right)
+ 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"
+ by (simp add: sup_commute)
+ 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 (simp add: inf_eq_neg_sup)
apply (simp add: sup_commute)
apply (erule sup_0_imp_0)
@@ -206,24 +220,32 @@
lemma zero_le_double_add_iff_zero_le_single_add [simp]:
"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=_")
by (simp add: add_sup_inf_distribs inf_aci)
- 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"
+ by (simp add: a, simp add: inf_commute)
+ then have "inf a 0 = 0"
+ by (simp only: add_right_cancel)
+ 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"
+ by (simp add: add_mono[OF a a, simplified])
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"
+ by (simp only: add_assoc)
+ 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 @@
lemma double_add_le_zero_iff_single_add_le_zero [simp]:
"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"
by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
- ultimately show ?thesis by blast
+ ultimately show ?thesis
+ by blast
qed
lemma double_add_less_zero_iff_single_less_zero [simp]:
"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"
by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp
- 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"
by (simp add: add_assoc[symmetric])
- 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"
by (simp add: add_assoc[symmetric])
- 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
-lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
+lemmas add_sup_inf_distribs =
+ add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
class lattice_ab_group_add_abs = lattice_ab_group_add + abs +
@@ -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
by (simp add: add_sup_inf_distribs ac_simps pprt_def nprt_def abs_lattice)
qed
@@ -347,7 +381,8 @@
have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
by (simp add: abs_lattice le_supI)
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>"
by (auto simp add: abs_lattice)
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")
by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
- 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)"
+ by (simp add: algebra_simps)
+ have "- b \<le> \<bar>b\<bar>"
+ 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)
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
- apply (metis (full_types) add_increasing add_uminus_conv_diff lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
+ apply (metis (full_types) add_increasing add_uminus_conv_diff
+ lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg
+ mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
done
- have yx: "?y <= ?x"
+ have yx: "?y \<le> ?x"
apply simp
- apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
+ apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff
+ lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos
+ 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)
apply (simp add: i1)
@@ -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)"
by (simp add: prts[symmetric])
show ?thesis
- proof cases
- assume "0 <= a * b"
+ proof (cases "0 \<le> a * b")
+ case True
then show ?thesis
apply (simp_all add: mulprts abs_prts)
- apply (insert a)
+ using a
apply (auto simp add:
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 (simp_all add: mulprts abs_prts)
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"
by (simp add: algebra_simps)
- moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
+ moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2"
by (simp_all add: assms mult_mono)
- 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"
by (simp add: mult_left_mono assms)
- moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
+ moreover have "pprt a * nprt b2 \<le> pprt a1 * nprt b2"
by (simp add: mult_right_mono_neg assms)
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"
by (simp add: mult_right_mono assms)
- moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
+ moreover have "nprt a2 * pprt b \<le> nprt a2 * pprt b1"
by (simp add: mult_left_mono_neg assms)
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"
by (simp add: mult_left_mono_neg assms)
- moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
+ moreover have "nprt a * nprt b1 \<le> nprt a1 * nprt b1"
by (simp add: mult_right_mono_neg assms)
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
+ by (simp add: algebra_simps)
qed
instance int :: lattice_ring
proof
fix k :: int
- show "abs k = sup k (- k)"
+ show "\<bar>k\<bar> = sup k (- k)"
by (auto simp add: sup_int_def)
qed
instance real :: lattice_ring
proof
fix a :: real
- show "abs a = sup a (- a)"
+ show "\<bar>a\<bar> = sup a (- a)"
by (auto simp add: sup_real_def)
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 =
ctxt addsimps (fresh_prod :: abs_fresh)
addsimps fresh_perm_app;
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
|> fold Simplifier.add_cong strong_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
- NO_CASES (HEADGOAL (
+ HEADGOAL (
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 @@
text {* advanced examples *}
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
+ #> Sign.add_consts_i
+ [(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
- #> Sign.add_consts_i
- [(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 frees = fold (Term.add_frees o Thm.prop_of) adefs [];
- 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 frees = fold (Term.add_frees o Thm.prop_of) adefs [];
+ 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;