--- a/src/Doc/IsarRef/Proof.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Doc/IsarRef/Proof.thy Tue Sep 03 22:30:52 2013 +0200
@@ -1195,7 +1195,7 @@
later.
@{rail "
- @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')')
+ @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')')
;
caseref: nameref attributes?
;
--- a/src/Doc/ROOT Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Doc/ROOT Tue Sep 03 22:30:52 2013 +0200
@@ -284,6 +284,8 @@
session Tutorial (doc) in "Tutorial" = HOL +
options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
+ theories [threads = 1]
+ "ToyList/ToyList_Test"
theories [thy_output_indent = 5]
"ToyList/ToyList"
"Ifexpr/Ifexpr"
--- a/src/Doc/Tutorial/ToyList/ToyList.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Tue Sep 03 22:30:52 2013 +0200
@@ -2,18 +2,6 @@
imports Datatype
begin
-(*<*)
-ML {* (* FIXME somewhat non-standard, fragile *)
- let
- val texts =
- map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
- ["ToyList1", "ToyList2"];
- val trs = Outer_Syntax.parse Position.start (implode texts);
- val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
- in @{assert} (Toplevel.is_toplevel end_state) end;
-*}
-(*>*)
-
text{*\noindent
HOL already has a predefined theory of lists called @{text List} ---
@{text ToyList} is merely a small fragment of it chosen as an example. In
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Tue Sep 03 22:30:52 2013 +0200
@@ -0,0 +1,16 @@
+theory ToyList_Test
+imports Datatype
+begin
+
+ML {* (* FIXME somewhat non-standard, fragile *)
+ let
+ val texts =
+ map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
+ ["ToyList1", "ToyList2"];
+ val trs = Outer_Syntax.parse Position.start (implode texts);
+ val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
+ in @{assert} (Toplevel.is_toplevel end_state) end;
+*}
+
+end
+
--- a/src/HOL/Algebra/Divisibility.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Tue Sep 03 22:30:52 2013 +0200
@@ -3637,11 +3637,11 @@
assume cunit:"c \<in> Units G"
have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c" by (simp add: b)
- also with ccarr acarr cunit
+ also from ccarr acarr cunit
have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
- also with ccarr cunit
+ also from ccarr cunit
have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
- also with acarr
+ also from acarr
have "\<dots> = a" by simp
finally have "a = b \<otimes> inv c" by simp
with ccarr cunit
--- a/src/HOL/BNF/Examples/Stream.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy Tue Sep 03 22:30:52 2013 +0200
@@ -423,9 +423,9 @@
case False
hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth)
moreover
- { from less(2) have "length (shd s) > 0" by (cases s) simp_all
- moreover with False have "y > 0" by (cases y) simp_all
- ultimately have "y - length (shd s) < y" by simp
+ { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all
+ with False have "y > 0" by (cases y) simp_all
+ with * have "y - length (shd s) < y" by simp
}
moreover have "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto
ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
--- a/src/HOL/BNF/More_BNFs.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Tue Sep 03 22:30:52 2013 +0200
@@ -898,11 +898,10 @@
proof (intro multiset_eqI, transfer fixing: f)
fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
assume "M1 \<in> multiset" "M2 \<in> multiset"
- moreover
hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
"setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
- ultimately show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
+ then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
setsum M1 {a. f a = x \<and> 0 < M1 a} +
setsum M2 {a. f a = x \<and> 0 < M2 a}"
by (auto simp: setsum.distrib[symmetric])
--- a/src/HOL/Big_Operators.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Big_Operators.thy Tue Sep 03 22:30:52 2013 +0200
@@ -46,7 +46,7 @@
proof -
from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
by (auto dest: mk_disjoint_insert)
- moreover from `finite A` this have "finite B" by simp
+ moreover from `finite A` A have "finite B" by simp
ultimately show ?thesis by simp
qed
--- a/src/HOL/Complete_Lattices.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy Tue Sep 03 22:30:52 2013 +0200
@@ -250,7 +250,7 @@
shows "\<Sqinter>A \<sqsubseteq> u"
proof -
from `A \<noteq> {}` obtain v where "v \<in> A" by blast
- moreover with assms have "v \<sqsubseteq> u" by blast
+ moreover from `v \<in> A` assms(1) have "v \<sqsubseteq> u" by blast
ultimately show ?thesis by (rule Inf_lower2)
qed
@@ -260,7 +260,7 @@
shows "u \<sqsubseteq> \<Squnion>A"
proof -
from `A \<noteq> {}` obtain v where "v \<in> A" by blast
- moreover with assms have "u \<sqsubseteq> v" by blast
+ moreover from `v \<in> A` assms(1) have "u \<sqsubseteq> v" by blast
ultimately show ?thesis by (rule Sup_upper2)
qed
--- a/src/HOL/Complex.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Complex.thy Tue Sep 03 22:30:52 2013 +0200
@@ -707,11 +707,11 @@
unfolding d_def by simp
moreover from a assms have "cos a = cos x" and "sin a = sin x"
by (simp_all add: complex_eq_iff)
- hence "cos d = 1" unfolding d_def cos_diff by simp
- moreover hence "sin d = 0" by (rule cos_one_sin_zero)
+ hence cos: "cos d = 1" unfolding d_def cos_diff by simp
+ moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
ultimately have "d = 0"
unfolding sin_zero_iff even_mult_two_ex
- by (safe, auto simp add: numeral_2_eq_2 less_Suc_eq)
+ by (auto simp add: numeral_2_eq_2 less_Suc_eq)
thus "a = x" unfolding d_def by simp
qed (simp add: assms del: Re_sgn Im_sgn)
with `z \<noteq> 0` show "arg z = x"
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Tue Sep 03 22:30:52 2013 +0200
@@ -138,7 +138,6 @@
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
note 6 Y0
- moreover
ultimately have ?case by (simp add: mkPinj_cn) }
moreover
{ assume "x>y" hence "EX d. x = d + y" by arith
@@ -286,7 +285,6 @@
from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
moreover
note 6
- moreover
ultimately have ?case by (simp add: mkPinj_cn) }
moreover
{ assume "x > y" hence "EX d. x = d + y" by arith
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 22:30:52 2013 +0200
@@ -2168,7 +2168,6 @@
by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
moreover
- moreover
{assume c: "?c = 0" and d: "?d>0"
from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
from d have d': "2*?d \<noteq> 0" by simp
@@ -2314,7 +2313,6 @@
by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
moreover
- moreover
{assume c: "?c = 0" and d: "?d>0"
from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
from d have d': "2*?d \<noteq> 0" by simp
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 03 22:30:52 2013 +0200
@@ -1314,7 +1314,7 @@
head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
have ?case by simp}
moreover
- {moreover assume nz: "n = 0"
+ { assume nz: "n = 0"
from polymul_degreen[OF norm(5,4), where m="0"]
polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
norm(5,6) degree_npolyhCN[OF norm(6)]
--- a/src/HOL/Deriv.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Deriv.thy Tue Sep 03 22:30:52 2013 +0200
@@ -416,10 +416,10 @@
proof
fix h show "F h = 0"
proof (rule ccontr)
- assume "F h \<noteq> 0"
- moreover from this have h: "h \<noteq> 0"
+ assume **: "F h \<noteq> 0"
+ then have h: "h \<noteq> 0"
by (clarsimp simp add: F.zero)
- ultimately have "0 < ?r h"
+ with ** have "0 < ?r h"
by (simp add: divide_pos_pos)
from LIM_D [OF * this] obtain s where s: "0 < s"
and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
@@ -528,11 +528,11 @@
lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
proof safe
assume "f differentiable x in s"
- then obtain f' where "FDERIV f x : s :> f'"
+ then obtain f' where *: "FDERIV f x : s :> f'"
unfolding isDiff_def by auto
- moreover then obtain c where "f' = (\<lambda>x. x * c)"
+ then obtain c where "f' = (\<lambda>x. x * c)"
by (metis real_bounded_linear FDERIV_bounded_linear)
- ultimately show "\<exists>D. DERIV f x : s :> D"
+ with * show "\<exists>D. DERIV f x : s :> D"
unfolding deriv_fderiv by auto
qed (auto simp: isDiff_def deriv_fderiv)
@@ -730,8 +730,8 @@
DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
unfolding DERIV_iff2
proof (rule filterlim_cong)
- assume "eventually (\<lambda>x. f x = g x) (nhds x)"
- moreover then have "f x = g x" by (auto simp: eventually_nhds)
+ assume *: "eventually (\<lambda>x. f x = g x) (nhds x)"
+ moreover from * have "f x = g x" by (auto simp: eventually_nhds)
moreover assume "x = y" "u = v"
ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
by (auto simp: eventually_at_filter elim: eventually_elim1)
@@ -1319,7 +1319,8 @@
and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
- shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
+ shows "\<exists>g'c f'c c.
+ DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
proof -
let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
from assms have "a < b" by simp
@@ -1348,7 +1349,7 @@
{
from cdef have "?h b - ?h a = (b - a) * l" by auto
- also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
+ also from leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
}
moreover
@@ -1458,14 +1459,15 @@
using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less)
ultimately have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
using f g `x < a` by (intro GMVT') auto
- then guess c ..
+ then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c"
+ by blast
moreover
- with g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c"
+ from * g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c"
by (simp add: field_simps)
ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
qed
- then guess \<zeta> ..
+ then obtain \<zeta> where "\<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" ..
then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)"
unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
moreover
@@ -1581,9 +1583,10 @@
have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y"
using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+
- then guess y ..
- from this
- have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
+ then obtain y where [arith]: "t < y" "y < a"
+ and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y"
+ by blast
+ from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps)
have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t"
--- a/src/HOL/Divides.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Divides.thy Tue Sep 03 22:30:52 2013 +0200
@@ -742,11 +742,11 @@
apply (subst less_iff_Suc_add)
apply (auto simp add: add_mult_distrib)
done
- from `n \<noteq> 0` assms have "fst qr = fst qr'"
+ from `n \<noteq> 0` assms have *: "fst qr = fst qr'"
by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
- moreover from this assms have "snd qr = snd qr'"
+ with assms have "snd qr = snd qr'"
by (simp add: divmod_nat_rel_def)
- ultimately show ?thesis by (cases qr, cases qr') simp
+ with * show ?thesis by (cases qr, cases qr') simp
qed
text {*
--- a/src/HOL/Fields.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Fields.thy Tue Sep 03 22:30:52 2013 +0200
@@ -919,8 +919,8 @@
assume notless: "~ (0 < x)"
have "~ (1 < inverse x)"
proof
- assume "1 < inverse x"
- also with notless have "... \<le> 0" by simp
+ assume *: "1 < inverse x"
+ also from notless and * have "... \<le> 0" by simp
also have "... < 1" by (rule zero_less_one)
finally show False by auto
qed
--- a/src/HOL/Finite_Set.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Finite_Set.thy Tue Sep 03 22:30:52 2013 +0200
@@ -1103,7 +1103,7 @@
proof -
from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
by (auto dest: mk_disjoint_insert)
- moreover from `finite A` this have "finite B" by simp
+ moreover from `finite A` A have "finite B" by simp
ultimately show ?thesis by simp
qed
--- a/src/HOL/Imperative_HOL/Legacy_Mrec.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Imperative_HOL/Legacy_Mrec.thy Tue Sep 03 22:30:52 2013 +0200
@@ -118,7 +118,7 @@
proof (cases "mrec b h1")
case (Some result)
then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce
- moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
+ moreover from mrec_rec have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
apply (intro 1(2))
apply (auto simp add: Inr Inl')
done
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Sep 03 22:30:52 2013 +0200
@@ -469,12 +469,12 @@
assume pivot: "l \<le> p \<and> p \<le> r"
assume i_outer: "i < l \<or> r < i"
from partition_outer_remains [OF part True] i_outer
- have "Array.get h a !i = Array.get h1 a ! i" by fastforce
+ have 2: "Array.get h a !i = Array.get h1 a ! i" by fastforce
moreover
- with 1(1) [OF True pivot qs1] pivot i_outer
- have "Array.get h1 a ! i = Array.get h2 a ! i" by auto
+ from 1(1) [OF True pivot qs1] pivot i_outer 2
+ have 3: "Array.get h1 a ! i = Array.get h2 a ! i" by auto
moreover
- with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
+ from qs2 1(2) [of p h2 h' ret2] True pivot i_outer 3
have "Array.get h2 a ! i = Array.get h' a ! i" by auto
ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp
}
@@ -604,9 +604,9 @@
shows "success (f \<guillemotright>= g) h"
using assms(1) proof (rule success_effectE)
fix h' r
- assume "effect f h h' r"
- moreover with assms(2) have "success (g r) h'" .
- ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
+ assume *: "effect f h h' r"
+ with assms(2) have "success (g r) h'" .
+ with * show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
qed
lemma success_partitionI:
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 03 22:30:52 2013 +0200
@@ -490,7 +490,6 @@
moreover
from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
- moreover
ultimately show ?thesis by (simp add: multiset_of_append)
qed
--- a/src/HOL/Induct/Common_Patterns.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy Tue Sep 03 22:30:52 2013 +0200
@@ -388,19 +388,18 @@
refl: "star r x x"
| step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-text{* Underscores are replaced by the default name hyps: *}
+text {* Underscores are replaced by the default name hyps: *}
-lemmas star_induct = star.induct[case_names base step[r _ IH]]
+lemmas star_induct = star.induct [case_names base step[r _ IH]]
lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-proof(induct rule: star_induct)
-print_cases
- case base thus ?case .
+proof (induct rule: star_induct) print_cases
+ case base
+ then show ?case .
next
- case (step a b c)
- from step.prems have "star r b z" by(rule step.IH)
- from step.r this show ?case by(rule star.step)
+ case (step a b c) print_facts
+ from step.prems have "star r b z" by (rule step.IH)
+ with step.r show ?case by (rule star.step)
qed
-
end
\ No newline at end of file
--- a/src/HOL/Library/ContNotDenum.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Tue Sep 03 22:30:52 2013 +0200
@@ -323,64 +323,46 @@
lemma closed_subset_ex:
fixes c::real
- assumes alb: "a < b"
- shows
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
-proof -
- {
- assume clb: "c < b"
- {
- assume cla: "c < a"
- from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
- with alb have
- "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
- by auto
- hence
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by auto
- }
- moreover
- {
- assume ncla: "\<not>(c < a)"
- with clb have cdef: "a \<le> c \<and> c < b" by simp
- obtain ka where kadef: "ka = (c + b)/2" by blast
+ assumes "a < b"
+ shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
+proof (cases "c < b")
+ case True
+ show ?thesis
+ proof (cases "c < a")
+ case True
+ with `a < b` `c < b` have "c \<notin> closed_int a b"
+ unfolding closed_int_def by auto
+ with `a < b` show ?thesis by auto
+ next
+ case False
+ then have "a \<le> c" by simp
+ def ka \<equiv> "(c + b)/2"
- from kadef clb have kalb: "ka < b" by auto
- moreover from kadef cdef have kagc: "ka > c" by simp
- ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
- moreover from cdef kagc have "ka \<ge> a" by simp
- hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
- ultimately have
- "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
- using kalb by auto
- hence
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by auto
-
- }
+ from ka_def `c < b` have kalb: "ka < b" by auto
+ moreover from ka_def `c < b` have kagc: "ka > c" by simp
+ ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
+ moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
+ hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
ultimately have
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by (rule case_split)
- }
- moreover
- {
- assume "\<not> (c < b)"
- hence cgeb: "c \<ge> b" by simp
+ "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
+ using kalb by auto
+ then show ?thesis
+ by auto
+ qed
+next
+ case False
+ then have "c \<ge> b" by simp
- obtain kb where kbdef: "kb = (a + b)/2" by blast
- with alb have kblb: "kb < b" by auto
- with kbdef cgeb have "a < kb \<and> kb < c" by auto
- moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
- moreover from kblb have
- "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
- ultimately have
- "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
- by simp
- hence
- "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
- by auto
- }
- ultimately show ?thesis by (rule case_split)
+ def kb \<equiv> "(a + b)/2"
+ with `a < b` have "kb < b" by auto
+ with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
+ from `kb < c` have c: "c \<notin> closed_int a kb"
+ unfolding closed_int_def by auto
+ with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
+ unfolding closed_int_def by auto
+ with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
+ by simp
+ then show ?thesis by auto
qed
subsection {* newInt: Interval generation *}
--- a/src/HOL/Library/Countable_Set.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Countable_Set.thy Tue Sep 03 22:30:52 2013 +0200
@@ -55,7 +55,8 @@
assumes "countable S" "infinite S"
obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
proof -
- from `countable S`[THEN countableE] guess f .
+ obtain f :: "'a \<Rightarrow> nat" where "inj_on f S"
+ using `countable S` by (rule countableE)
then have "bij_betw f S (f`S)"
unfolding bij_betw_def by simp
moreover
@@ -169,9 +170,12 @@
"countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
-lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"
+lemma countable_image[intro, simp]:
+ assumes "countable A"
+ shows "countable (f`A)"
proof -
- from A guess g by (rule countableE)
+ obtain g :: "'a \<Rightarrow> nat" where "inj_on g A"
+ using assms by (rule countableE)
moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
by (auto intro: inj_on_inv_into inv_into_into)
ultimately show ?thesis
--- a/src/HOL/Library/Extended_Real.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue Sep 03 22:30:52 2013 +0200
@@ -146,11 +146,11 @@
"-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
proof -
case (goal1 P x)
- moreover then obtain a b where "x = (a, b)" by (cases x) auto
- ultimately show P
+ then obtain a b where "x = (a, b)" by (cases x) auto
+ with goal1 show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
-termination proof qed (rule wf_empty)
+termination by default (rule wf_empty)
lemma Infty_neq_0[simp]:
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -234,8 +234,8 @@
| " -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
proof -
case (goal1 P x)
- moreover then obtain a b where "x = (a,b)" by (cases x) auto
- ultimately show P by (cases rule: ereal2_cases[of a b]) auto
+ then obtain a b where "x = (a,b)" by (cases x) auto
+ with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
qed simp_all
termination by (relation "{}") simp
@@ -496,8 +496,8 @@
"-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
proof -
case (goal1 P x)
- moreover then obtain a b where "x = (a, b)" by (cases x) auto
- ultimately show P by (cases rule: ereal2_cases[of a b]) auto
+ then obtain a b where "x = (a, b)" by (cases x) auto
+ with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
qed simp_all
termination by (relation "{}") simp
@@ -1338,9 +1338,9 @@
next
{ assume "c = \<infinity>" have ?thesis
proof cases
- assume "\<forall>i. f i = 0"
- moreover then have "range f = {0}" by auto
- ultimately show "c * SUPR UNIV f \<le> y" using *
+ assume **: "\<forall>i. f i = 0"
+ then have "range f = {0}" by auto
+ with ** show "c * SUPR UNIV f \<le> y" using *
by (auto simp: SUP_def min_max.sup_absorb1)
next
assume "\<not> (\<forall>i. f i = 0)"
@@ -1368,7 +1368,8 @@
next
case (real r)
with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" by auto
- moreover from assms[of n] guess i ..
+ moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
+ using assms ..
ultimately show ?thesis
by (auto intro!: bexI[of _ i])
qed
@@ -1383,11 +1384,12 @@
proof
fix n ::nat have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
- then guess x ..
+ then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
qed
- from choice[OF this] guess f .. note f = this
+ from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
+ where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
have "SUPR UNIV f = Sup A"
proof (rule SUP_eqI)
fix i show "f i \<le> Sup A" using f
@@ -1417,9 +1419,9 @@
from `A \<noteq> {}` obtain x where "x \<in> A" by auto
show ?thesis
proof cases
- assume "\<infinity> \<in> A"
- moreover then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
- ultimately show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
+ assume *: "\<infinity> \<in> A"
+ then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
+ with * show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
next
assume "\<infinity> \<notin> A"
have "\<exists>x\<in>A. 0 \<le> x"
@@ -1433,10 +1435,12 @@
then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
by(cases x) auto
qed
- from choice[OF this] guess f .. note f = this
+ from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
+ where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
have "SUPR UNIV f = \<infinity>"
proof (rule SUP_PInfty)
- fix n :: nat show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
+ fix n :: nat
+ show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
using f[THEN spec, of n] `0 \<le> x`
by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
qed
@@ -1489,10 +1493,13 @@
fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
proof -
- { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto }
- moreover then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
+ {
+ fix x
+ have "-a - -x = -(a - x)" using assms by (cases x) auto
+ } note * = this
+ then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
by (auto simp: image_image)
- ultimately show ?thesis
+ with * show ?thesis
using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
qed
@@ -1606,9 +1613,9 @@
unfolding open_ereal_generated
proof (induct rule: generate_topology.induct)
case (Int A B)
- moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
- by auto
- ultimately show ?case
+ then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
+ by auto
+ with Int show ?case
by (intro exI[of _ "max x z"]) fastforce
next
{ fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
@@ -1621,9 +1628,9 @@
unfolding open_ereal_generated
proof (induct rule: generate_topology.induct)
case (Int A B)
- moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
- by auto
- ultimately show ?case
+ then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
+ by auto
+ with Int show ?case
by (intro exI[of _ "min x z"]) fastforce
next
{ fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
@@ -1711,8 +1718,9 @@
fixes S :: "ereal set"
assumes "open S" "x \<in> S" and x: "\<bar>x\<bar> \<noteq> \<infinity>"
obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
-proof-
- guess e using ereal_open_cont_interval[OF assms] .
+proof -
+ obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
+ using assms by (rule ereal_open_cont_interval)
with that[of "x-e" "x+e"] ereal_between[OF x, of e]
show thesis by auto
qed
@@ -1759,8 +1767,9 @@
lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
unfolding tendsto_def
proof safe
- fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
- from open_MInfty[OF this] guess B .. note B = this
+ fix S :: "ereal set"
+ assume "open S" "-\<infinity> \<in> S"
+ from open_MInfty[OF this] obtain B where "{..<ereal B} \<subseteq> S" ..
moreover
assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
@@ -1775,7 +1784,7 @@
unfolding tendsto_PInfty eventually_sequentially
proof safe
fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
- from this[rule_format, of "r+1"] guess N ..
+ then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n" by blast
moreover have "ereal r < ereal (r + 1)" by auto
ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
by (blast intro: less_le_trans)
@@ -1785,7 +1794,7 @@
unfolding tendsto_MInfty eventually_sequentially
proof safe
fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
- from this[rule_format, of "r - 1"] guess N ..
+ then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)" by blast
moreover have "ereal (r - 1) < ereal r" by auto
ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
by (blast intro: le_less_trans)
--- a/src/HOL/Library/FinFun.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/FinFun.thy Tue Sep 03 22:30:52 2013 +0200
@@ -960,7 +960,7 @@
{ fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
proof -
obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
- moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
+ moreover from g' have "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
qed }
--- a/src/HOL/Library/Float.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Float.thy Tue Sep 03 22:30:52 2013 +0200
@@ -44,7 +44,7 @@
lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
-lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
+lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
@@ -175,7 +175,7 @@
lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
by (induct n) simp_all
-lemma fixes x y::float
+lemma fixes x y::float
shows real_of_float_min: "real (min x y) = min (real x) (real y)"
and real_of_float_max: "real (max x y) = max (real x) (real y)"
by (simp_all add: min_def max_def)
@@ -197,7 +197,7 @@
then show "\<exists>c. a < c \<and> c < b"
apply (intro exI[of _ "(a + b) * Float 1 -1"])
apply transfer
- apply (simp add: powr_neg_numeral)
+ apply (simp add: powr_neg_numeral)
done
qed
@@ -222,14 +222,14 @@
plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
done
-lemma transfer_numeral [transfer_rule]:
+lemma transfer_numeral [transfer_rule]:
"fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
by (simp add: minus_numeral[symmetric] del: minus_numeral)
-lemma transfer_neg_numeral [transfer_rule]:
+lemma transfer_neg_numeral [transfer_rule]:
"fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
@@ -321,7 +321,7 @@
"exponent f = snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
\<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))"
-lemma
+lemma
shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
proof -
@@ -351,7 +351,7 @@
lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
using mantissa_not_dvd[of f] by auto
-lemma
+lemma
fixes m e :: int
defines "f \<equiv> float_of (m * 2 powr e)"
assumes dvd: "\<not> 2 dvd m"
@@ -740,19 +740,23 @@
qed
lemma bitlen_Float:
-fixes m e
-defines "f \<equiv> Float m e"
-shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
-proof cases
- assume "m \<noteq> 0"
+ fixes m e
+ defines "f \<equiv> Float m e"
+ shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
+proof (cases "m = 0")
+ case True
+ then show ?thesis by (simp add: f_def bitlen_def Float_def)
+next
+ case False
hence "f \<noteq> float_of 0"
unfolding real_of_float_eq by (simp add: f_def)
hence "mantissa f \<noteq> 0"
by (simp add: mantissa_noteq_0)
moreover
- from f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`] guess i .
+ obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
+ by (rule f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`])
ultimately show ?thesis by (simp add: abs_mult)
-qed (simp add: f_def bitlen_def Float_def)
+qed
lemma compute_bitlen[code]:
shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
@@ -865,9 +869,9 @@
is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
lemma compute_lapprox_posrat[code]:
- fixes prec x y
- shows "lapprox_posrat prec x y =
- (let
+ fixes prec x y
+ shows "lapprox_posrat prec x y =
+ (let
l = rat_precision prec x y;
d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
in normfloat (Float d (- l)))"
@@ -948,7 +952,7 @@
assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
shows "real (rapprox_posrat n x y) < 1"
proof -
- have powr1: "2 powr real (rat_precision n (int x) (int y)) =
+ have powr1: "2 powr real (rat_precision n (int x) (int y)) =
2 ^ nat (rat_precision n (int x) (int y))" using rat_precision_pos[of x y n] assms
by (simp add: powr_realpow[symmetric])
have "x * 2 powr real (rat_precision n (int x) (int y)) / y = (x / y) *
@@ -978,7 +982,7 @@
(if y = 0 then 0
else if 0 \<le> x then
(if 0 < y then lapprox_posrat prec (nat x) (nat y)
- else - (rapprox_posrat prec (nat x) (nat (-y))))
+ else - (rapprox_posrat prec (nat x) (nat (-y))))
else (if 0 < y
then - (rapprox_posrat prec (nat (-x)) (nat y))
else lapprox_posrat prec (nat (-x)) (nat (-y))))"
@@ -993,7 +997,7 @@
(if y = 0 then 0
else if 0 \<le> x then
(if 0 < y then rapprox_posrat prec (nat x) (nat y)
- else - (lapprox_posrat prec (nat x) (nat (-y))))
+ else - (lapprox_posrat prec (nat x) (nat (-y))))
else (if 0 < y
then - (lapprox_posrat prec (nat (-x)) (nat y))
else rapprox_posrat prec (nat (-x)) (nat (-y))))"
@@ -1017,7 +1021,7 @@
by (simp add: field_simps powr_divide2[symmetric])
show ?thesis
- using not_0
+ using not_0
by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
qed (transfer, auto)
hide_fact (open) compute_float_divl
@@ -1037,7 +1041,7 @@
by (simp add: field_simps powr_divide2[symmetric])
show ?thesis
- using not_0
+ using not_0
by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
qed (transfer, auto)
hide_fact (open) compute_float_divr
@@ -1104,7 +1108,7 @@
(simp add: powr_minus inverse_eq_divide)
qed
-lemma rapprox_rat_nonneg_neg:
+lemma rapprox_rat_nonneg_neg:
"0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
unfolding rapprox_rat_def round_up_def
by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)
@@ -1157,7 +1161,7 @@
"0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
proof transfer
fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
- def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
+ def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
proof cases
assume nonneg: "0 \<le> p"
@@ -1279,12 +1283,16 @@
lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
-proof cases
- assume nzero: "floor_fl x \<noteq> float_of 0"
- have "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
- from denormalize_shift[OF this[THEN eq_reflection] nzero] guess i . note i = this
- thus ?thesis by simp
-qed (simp add: floor_fl_def)
+proof (cases "floor_fl x = float_of 0")
+ case True
+ then show ?thesis by (simp add: floor_fl_def)
+next
+ case False
+ have eq: "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
+ obtain i where "\<lfloor>real x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
+ by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
+ then show ?thesis by simp
+qed
end
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Sep 03 22:30:52 2013 +0200
@@ -3804,8 +3804,8 @@
by (simp add: split_if_asm dist_fps_def)
moreover
from fps_eq_least_unique[OF `f \<noteq> g`]
- obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
- moreover hence "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
+ obtain n where n: "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
+ moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
by (auto simp add: leastP_def setge_def)
ultimately show ?thesis using `j \<le> i` by simp
next
--- a/src/HOL/Library/Fraction_Field.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Tue Sep 03 22:30:52 2013 +0200
@@ -209,7 +209,7 @@
next
case False
then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto
- moreover with False have "0 \<noteq> Fract a b" by simp
+ with False have "0 \<noteq> Fract a b" by simp
with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_fract_def eq_fract)
with Fract `q = Fract a b` `b \<noteq> 0` show thesis by auto
qed
--- a/src/HOL/Library/FuncSet.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue Sep 03 22:30:52 2013 +0200
@@ -375,7 +375,8 @@
proof (rule ccontr)
assume "\<not> ?thesis"
then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
- from choice[OF this] guess f ..
+ from choice[OF this]
+ obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" ..
then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
with `Pi\<^sub>E I F = {}` show False by auto
qed
@@ -437,8 +438,10 @@
shows "F i \<subseteq> F' i"
proof
fix x assume "x \<in> F i"
- with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
- from choice[OF this] guess f .. note f = this
+ with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))"
+ by auto
+ from choice[OF this] obtain f
+ where f: " \<forall>j. (j \<in> I \<longrightarrow> f j \<in> F j \<and> (i = j \<longrightarrow> x = f j)) \<and> (j \<notin> I \<longrightarrow> f j = undefined)" ..
then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
then have "f \<in> Pi\<^sub>E I F'" using assms by simp
then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
--- a/src/HOL/Library/Liminf_Limsup.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Tue Sep 03 22:30:52 2013 +0200
@@ -169,15 +169,15 @@
moreover
{ fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
- proof cases
- assume "\<exists>z. y < z \<and> z < C"
- then guess z ..
- moreover then have "z \<le> INFI {x. z < X x} X"
+ proof (cases "\<exists>z. y < z \<and> z < C")
+ case True
+ then obtain z where z: "y < z \<and> z < C" ..
+ moreover from z have "z \<le> INFI {x. z < X x} X"
by (auto intro!: INF_greatest)
ultimately show ?thesis
using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
next
- assume "\<not> (\<exists>z. y < z \<and> z < C)"
+ case False
then have "C \<le> INFI {x. y < X x} X"
by (intro INF_greatest) auto
with `y < C` show ?thesis
@@ -203,7 +203,7 @@
show "f0 \<le> y"
proof cases
assume "\<exists>z. y < z \<and> z < f0"
- then guess z ..
+ then obtain z where "y < z \<and> z < f0" ..
moreover have "z \<le> INFI {x. z < f x} f"
by (rule INF_greatest) simp
ultimately show ?thesis
@@ -240,22 +240,22 @@
next
fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
show "y \<le> f0"
- proof cases
- assume "\<exists>z. f0 < z \<and> z < y"
- then guess z ..
+ proof (cases "\<exists>z. f0 < z \<and> z < y")
+ case True
+ then obtain z where "f0 < z \<and> z < y" ..
moreover have "SUPR {x. f x < z} f \<le> z"
by (rule SUP_least) simp
ultimately show ?thesis
using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
next
- assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+ case False
show ?thesis
proof (rule classical)
assume "\<not> y \<le> f0"
then have "eventually (\<lambda>x. f x < y) F"
using lim[THEN topological_tendstoD, of "{..< y}"] by auto
then have "eventually (\<lambda>x. f x \<le> f0) F"
- using discrete by (auto elim!: eventually_elim1 simp: not_less)
+ using False by (auto elim!: eventually_elim1 simp: not_less)
then have "y \<le> SUPR {x. f x \<le> f0} f"
by (rule lower)
moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
--- a/src/HOL/Library/Permutations.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Permutations.thy Tue Sep 03 22:30:52 2013 +0200
@@ -166,8 +166,8 @@
have xfgpF': "?xF = ?g ` ?pF'" .
have Fs: "card F = n - 1" using `x \<notin> F` H0 `finite F` by auto
from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto
- moreover hence "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
- ultimately have pF'f: "finite ?pF'" using H0 `finite F`
+ then have "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
+ then have pF'f: "finite ?pF'" using H0 `finite F`
apply (simp only: Collect_split Collect_mem_eq)
apply (rule finite_cartesian_product)
apply simp_all
@@ -195,7 +195,7 @@
thus ?thesis unfolding inj_on_def by blast
qed
from `x \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
- hence "\<exists>m. n = Suc m" by arith
+ hence "\<exists>m. n = Suc m" by presburger
then obtain m where n[simp]: "n = Suc m" by blast
from pFs H0 have xFc: "card ?xF = fact n"
unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF`
--- a/src/HOL/Library/RBT_Impl.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Tue Sep 03 22:30:52 2013 +0200
@@ -146,8 +146,7 @@
= Set.insert k (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
proof -
assume "rbt_sorted (Branch c t1 k v t2)"
- moreover from this have "rbt_sorted t1" "rbt_sorted t2" by simp_all
- ultimately show ?thesis by (simp add: rbt_lookup_keys)
+ then show ?thesis by (simp add: rbt_lookup_keys)
qed
lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))"
@@ -1405,14 +1404,14 @@
proof(cases "n mod 2 = 0")
case True note ge0
moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
- moreover with True have "P (n div 2) kvs" by(rule IH)
+ moreover from True n2 have "P (n div 2) kvs" by(rule IH)
moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs'
where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
by(cases "snd (rbtreeify_f (n div 2) kvs)")
(auto simp add: snd_def split: prod.split_asm)
moreover from "1.prems" length_rbtreeify_f[OF n2] ge0
- have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
- moreover with True kvs'[symmetric] refl refl
+ have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
+ moreover from True kvs'[symmetric] refl refl n2'
have "Q (n div 2) kvs'" by(rule IH)
moreover note feven[unfolded feven_def]
(* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
@@ -1421,14 +1420,14 @@
next
case False note ge0
moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
- moreover with False have "P (n div 2) kvs" by(rule IH)
+ moreover from False n2 have "P (n div 2) kvs" by(rule IH)
moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs'
where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
by(cases "snd (rbtreeify_f (n div 2) kvs)")
(auto simp add: snd_def split: prod.split_asm)
moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 False
- have "n div 2 \<le> length kvs'" by(simp add: kvs') arith
- moreover with False kvs'[symmetric] refl refl have "P (n div 2) kvs'" by(rule IH)
+ have n2': "n div 2 \<le> length kvs'" by(simp add: kvs') arith
+ moreover from False kvs'[symmetric] refl refl n2' have "P (n div 2) kvs'" by(rule IH)
moreover note fodd[unfolded fodd_def]
ultimately have "P (Suc (2 * (n div 2))) kvs" by -
thus ?thesis using False
@@ -1451,14 +1450,14 @@
proof(cases "n mod 2 = 0")
case True note ge0
moreover from "2.prems" have n2: "n div 2 \<le> Suc (length kvs)" by simp
- moreover with True have "Q (n div 2) kvs" by(rule IH)
+ moreover from True n2 have "Q (n div 2) kvs" by(rule IH)
moreover from length_rbtreeify_g[OF ge0 n2] ge0 "2.prems" obtain t k v kvs'
where kvs': "rbtreeify_g (n div 2) kvs = (t, (k, v) # kvs')"
by(cases "snd (rbtreeify_g (n div 2) kvs)")
(auto simp add: snd_def split: prod.split_asm)
moreover from "2.prems" length_rbtreeify_g[OF ge0 n2] ge0
- have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
- moreover with True kvs'[symmetric] refl refl
+ have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
+ moreover from True kvs'[symmetric] refl refl n2'
have "Q (n div 2) kvs'" by(rule IH)
moreover note geven[unfolded geven_def]
ultimately have "Q (2 * (n div 2)) kvs" by -
@@ -1467,14 +1466,14 @@
next
case False note ge0
moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp
- moreover with False have "P (n div 2) kvs" by(rule IH)
+ moreover from False n2 have "P (n div 2) kvs" by(rule IH)
moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs'
where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
by(cases "snd (rbtreeify_f (n div 2) kvs)")
(auto simp add: snd_def split: prod.split_asm, arith)
moreover from "2.prems" length_rbtreeify_f[OF n2] ge0 False
- have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
- moreover with False kvs'[symmetric] refl refl
+ have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
+ moreover from False kvs'[symmetric] refl refl n2'
have "Q (n div 2) kvs'" by(rule IH)
moreover note godd[unfolded godd_def]
ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
--- a/src/HOL/Library/Ramsey.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Ramsey.thy Tue Sep 03 22:30:52 2013 +0200
@@ -326,11 +326,11 @@
have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
obtain Y t
- where "Y \<subseteq> Z" "infinite Y" "t < s"
+ where *: "Y \<subseteq> Z" "infinite Y" "t < s"
"(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
by (insert Ramsey [OF infZ part2]) auto
- moreover from this have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
- ultimately show ?thesis by iprover
+ then have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
+ with * show ?thesis by iprover
qed
--- a/src/HOL/Library/While_Combinator.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy Tue Sep 03 22:30:52 2013 +0200
@@ -93,8 +93,9 @@
next
case (Suc k)
hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
- then guess k by (rule exE[OF Suc.IH[of "c s"]])
- with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
+ from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" ..
+ with assms show ?case
+ by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
qed
next
fix k assume "\<not> b' ((c' ^^ k) (f s))"
@@ -107,8 +108,8 @@
show ?case
proof (cases "b s")
case True
- with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
- then guess k by (rule exE[OF Suc.IH[of "c s"]])
+ with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
+ from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" ..
thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
qed (auto intro: exI[of _ "0"])
qed
--- a/src/HOL/Library/Zorn.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Library/Zorn.thy Tue Sep 03 22:30:52 2013 +0200
@@ -119,9 +119,9 @@
lemma chain_sucD:
assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)"
proof -
- from `chain X` have "chain (suc X)" by (rule chain_suc)
- moreover then have "suc X \<subseteq> A" unfolding chain_def by blast
- ultimately show ?thesis by blast
+ from `chain X` have *: "chain (suc X)" by (rule chain_suc)
+ then have "suc X \<subseteq> A" unfolding chain_def by blast
+ with * show ?thesis by blast
qed
lemma suc_Union_closed_total':
@@ -348,8 +348,8 @@
moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto
ultimately have "subset.chain A ?C"
using subset.chain_extend [of A C X] and `X \<in> A` by auto
- moreover assume "\<Union>C \<noteq> X"
- moreover then have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
+ moreover assume **: "\<Union>C \<noteq> X"
+ moreover from ** have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
ultimately show False using * by blast
qed
@@ -578,11 +578,11 @@
case 0 show ?case by fact
next
case (Suc i)
- moreover obtain s where "s \<in> R" and "(f (Suc (Suc i)), f(Suc i)) \<in> s"
+ then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
using 1 by auto
- moreover hence "s initial_segment_of r \<or> r initial_segment_of s"
+ then have "s initial_segment_of r \<or> r initial_segment_of s"
using assms(1) `r \<in> R` by (simp add: Chains_def)
- ultimately show ?case by (simp add: init_seg_of_def) blast
+ with Suc s show ?case by (simp add: init_seg_of_def) blast
qed
}
thus False using assms(2) and `r \<in> R`
@@ -682,15 +682,14 @@
qed
ultimately have "Well_order ?m" by (simp add: order_on_defs)
--{*We show that the extension is above m*}
- moreover hence "(m, ?m) \<in> I" using `Well_order m` and `x \<notin> Field m`
+ moreover have "(m, ?m) \<in> I" using `Well_order ?m` and `Well_order m` and `x \<notin> Field m`
by (fastforce simp: I_def init_seg_of_def Field_def)
ultimately
--{*This contradicts maximality of m:*}
have False using max and `x \<notin> Field m` unfolding Field_def by blast
}
hence "Field m = UNIV" by auto
- moreover with `Well_order m` have "Well_order m" by simp
- ultimately show ?thesis by blast
+ with `Well_order m` show ?thesis by blast
qed
corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
--- a/src/HOL/Limits.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Limits.thy Tue Sep 03 22:30:52 2013 +0200
@@ -33,16 +33,17 @@
"(at_infinity \<Colon> real filter) = sup at_top at_bot"
unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
proof (intro arg_cong[where f=Abs_filter] ext iffI)
- fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
- then guess r ..
+ fix P :: "real \<Rightarrow> bool"
+ assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
+ then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
next
- fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
+ fix P :: "real \<Rightarrow> bool"
+ assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
- by (intro exI[of _ "max p (-q)"])
- (auto simp: abs_real_def)
+ by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
qed
lemma at_top_le_at_infinity:
--- a/src/HOL/List.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/List.thy Tue Sep 03 22:30:52 2013 +0200
@@ -722,12 +722,18 @@
using `xs \<noteq> []` proof (induct xs)
case Nil then show ?case by simp
next
- case (Cons x xs) show ?case proof (cases xs)
- case Nil with single show ?thesis by simp
+ case (Cons x xs)
+ show ?case
+ proof (cases xs)
+ case Nil
+ with single show ?thesis by simp
next
- case Cons then have "xs \<noteq> []" by simp
- moreover with Cons.hyps have "P xs" .
- ultimately show ?thesis by (rule cons)
+ case Cons
+ show ?thesis
+ proof (rule cons)
+ from Cons show "xs \<noteq> []" by simp
+ with Cons.hyps show "P xs" .
+ qed
qed
qed
@@ -1061,12 +1067,13 @@
lemma map_eq_imp_length_eq:
assumes "map f xs = map g ys"
shows "length xs = length ys"
-using assms proof (induct ys arbitrary: xs)
+ using assms
+proof (induct ys arbitrary: xs)
case Nil then show ?case by simp
next
case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
from Cons xs have "map f zs = map g ys" by simp
- moreover with Cons have "length zs = length ys" by blast
+ with Cons have "length zs = length ys" by blast
with xs show ?case by simp
qed
@@ -1669,10 +1676,10 @@
hence n: "n < Suc (length xs)" by simp
moreover
{ assume "n < length xs"
- with n obtain n' where "length xs - n = Suc n'"
+ with n obtain n' where n': "length xs - n = Suc n'"
by (cases "length xs - n", auto)
moreover
- then have "length xs - Suc n = n'" by simp
+ from n' have "length xs - Suc n = n'" by simp
ultimately
have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
}
@@ -3801,14 +3808,12 @@
then have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws"
using False and `xs' \<noteq> []` and `ys' = xs' @ ws` and len
by (intro less.hyps) auto
- then obtain m n zs where "concat (replicate m zs) = xs'"
+ then obtain m n zs where *: "concat (replicate m zs) = xs'"
and "concat (replicate n zs) = ws" by blast
- moreover
then have "concat (replicate (m + n) zs) = ys'"
using `ys' = xs' @ ws`
by (simp add: replicate_add)
- ultimately
- show ?thesis by blast
+ with * show ?thesis by blast
qed
then show ?case
using xs'_def ys'_def by metis
@@ -4074,8 +4079,8 @@
case Nil thus ?case by simp
next
case (Cons a xs)
- moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
- ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
+ then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
+ with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
qed
@@ -4195,8 +4200,8 @@
hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
proof (induct xss)
case (Cons x xs)
- moreover hence "x = []" by (cases x) auto
- ultimately show ?case by auto
+ then have "x = []" by (cases x) auto
+ with Cons show ?case by auto
qed simp
thus ?thesis using True by simp
next
@@ -4585,7 +4590,7 @@
proof -
from assms have "map f xs = map f ys"
by (simp add: sorted_distinct_set_unique)
- moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
+ with `inj_on f (set xs \<union> set ys)` show "xs = ys"
by (blast intro: map_inj_on)
qed
@@ -4620,11 +4625,12 @@
lemma foldr_max_sorted:
assumes "sorted (rev xs)"
shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
-using assms proof (induct xs)
+ using assms
+proof (induct xs)
case (Cons x xs)
- moreover hence "sorted (rev xs)" using sorted_append by auto
- ultimately show ?case
- by (cases xs, auto simp add: sorted_append max_def)
+ then have "sorted (rev xs)" using sorted_append by auto
+ with Cons show ?case
+ by (cases xs) (auto simp add: sorted_append max_def)
qed simp
lemma filter_equals_takeWhile_sorted_rev:
--- a/src/HOL/Map.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Map.thy Tue Sep 03 22:30:52 2013 +0200
@@ -715,18 +715,19 @@
by (rule set_map_of_compr)
ultimately show ?rhs by simp
next
- assume ?rhs show ?lhs proof
+ assume ?rhs show ?lhs
+ proof
fix k
show "map_of xs k = map_of ys k" proof (cases "map_of xs k")
case None
- moreover with `?rhs` have "map_of ys k = None"
+ with `?rhs` have "map_of ys k = None"
by (simp add: map_of_eq_None_iff)
- ultimately show ?thesis by simp
+ with None show ?thesis by simp
next
case (Some v)
- moreover with distinct `?rhs` have "map_of ys k = Some v"
+ with distinct `?rhs` have "map_of ys k = Some v"
by simp
- ultimately show ?thesis by simp
+ with Some show ?thesis by simp
qed
qed
qed
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Sep 03 22:30:52 2013 +0200
@@ -144,8 +144,8 @@
where "class": "class G C = Some (D', fs', ms')"
unfolding class_def by(auto dest!: weak_map_of_SomeI)
hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
- hence "(C, D') \<in> (subcls1 G)^+" ..
- also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
+ hence *: "(C, D') \<in> (subcls1 G)^+" ..
+ also from * acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
finally show False using acyc by(auto simp add: acyclic_def)
qed
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Sep 03 22:30:52 2013 +0200
@@ -2743,10 +2743,10 @@
using subspace_substandard[of "\<lambda>i. i \<notin> d"] .
ultimately have "span d \<subseteq> ?B"
using span_mono[of d "?B"] span_eq[of "?B"] by blast
- moreover have "card d \<le> dim (span d)"
+ moreover have *: "card d \<le> dim (span d)"
using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_inc[of d]
by auto
- moreover then have "dim ?B \<le> dim (span d)"
+ moreover from * have "dim ?B \<le> dim (span d)"
using dim_substandard[OF assms] by auto
ultimately show ?thesis
using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto
@@ -8604,7 +8604,7 @@
{ fix i assume "i:I"
{ assume "e i = 0"
have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg)
- moreover hence "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp
+ moreover from ge have "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp
ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto
hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
using `e i = 0` by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 03 22:30:52 2013 +0200
@@ -1441,14 +1441,14 @@
have *:"(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
apply(rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
using assms(3-)[unfolded has_vector_derivative_def] using assms(1-2)
- by (auto simp: Basis_real_def)
+ by auto
show ?thesis
proof(rule ccontr)
- assume "f' \<noteq> f''"
- moreover
- hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
- using * by (auto simp: fun_eq_iff)
- ultimately show False unfolding o_def by auto
+ assume **: "f' \<noteq> f''"
+ with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
+ by (auto simp: fun_eq_iff)
+ with ** show False
+ unfolding o_def by auto
qed
qed
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Sep 03 22:30:52 2013 +0200
@@ -63,10 +63,10 @@
assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S"
proof -
from compact_eq_closed[of S] compact_attains_sup[of S] assms
- obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
- moreover then have "Sup S = s"
+ obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
+ then have "Sup S = s"
by (auto intro!: Sup_eqI)
- ultimately show ?thesis
+ with S show ?thesis
by simp
qed
@@ -75,10 +75,10 @@
assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S"
proof -
from compact_eq_closed[of S] compact_attains_inf[of S] assms
- obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
- moreover then have "Inf S = s"
+ obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
+ then have "Inf S = s"
by (auto intro!: Inf_eqI)
- ultimately show ?thesis
+ with S show ?thesis
by simp
qed
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Sep 03 22:30:52 2013 +0200
@@ -905,12 +905,11 @@
then show "\<exists>a b. k = {a..b}" by auto
have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
proof (simp add: k interval_eq_empty subset_interval not_less, safe)
- fix i :: 'a assume i: "i \<in> Basis"
- moreover
+ fix i :: 'a
+ assume i: "i \<in> Basis"
with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
by (auto simp: PiE_iff)
- moreover note ord[of i]
- ultimately
+ with i ord[of i]
show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
by (auto simp: subset_iff eucl_le[where 'a='a])
qed
@@ -952,7 +951,7 @@
by auto
qed
then guess f unfolding bchoice_iff .. note f = this
- moreover then have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
+ moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
by auto
moreover from f have "x \<in> ?B (restrict f Basis)"
by (auto simp: mem_interval eucl_le[where 'a='a])
@@ -3874,7 +3873,7 @@
setprod_timesf setprod_constant inner_diff_left)
next
case False
- moreover with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \<noteq> {}"
+ with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \<noteq> {}"
unfolding interval_ne_empty
apply (intro ballI)
apply (erule_tac x=i in ballE)
@@ -3882,7 +3881,7 @@
done
moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b - a) \<bullet> i"
by (simp add: inner_simps field_simps)
- ultimately show ?thesis
+ ultimately show ?thesis using False
by (simp add: image_affinity_interval content_closed_interval'
setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left)
qed
@@ -3918,17 +3917,20 @@
unfolding interval_ne_empty by auto
show "(\<exists>xa. x \<bullet> i = m i * xa \<and> a \<bullet> i \<le> xa \<and> xa \<le> b \<bullet> i) \<longleftrightarrow>
min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) \<le> x \<bullet> i \<and> x \<bullet> i \<le> max (m i * (a \<bullet> i)) (m i * (b \<bullet> i))"
- proof cases
- assume "m i \<noteq> 0"
- moreover then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
+ proof (cases "m i = 0")
+ case True
+ with a_le_b show ?thesis by auto
+ next
+ case False
+ then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
by (auto simp add: field_simps)
- moreover have
+ from False have
"min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (a \<bullet> i) else m i * (b \<bullet> i))"
"max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (b \<bullet> i) else m i * (a \<bullet> i))"
using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
- ultimately show ?thesis using a_le_b
+ with False show ?thesis using a_le_b
unfolding * by (auto simp add: le_divide_eq divide_le_eq ac_simps)
- qed (insert a_le_b, auto)
+ qed
qed
qed simp
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 03 22:30:52 2013 +0200
@@ -288,8 +288,8 @@
next
fix S
assume "open S" "x \<in> S"
- from open_prod_elim[OF this] guess a' b' .
- moreover with A(4)[of a'] B(4)[of b']
+ from open_prod_elim[OF this] guess a' b' . note a'b' = this
+ moreover from a'b' A(4)[of a'] B(4)[of b']
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
@@ -3264,12 +3264,12 @@
unfolding C_def by auto
qed
then have "U \<subseteq> \<Union>C" using `U \<subseteq> \<Union>A` by auto
- ultimately obtain T where "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
+ ultimately obtain T where T: "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
using * by metis
- moreover then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
+ then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
by (auto simp: C_def)
then guess f unfolding bchoice_iff Bex_def ..
- ultimately show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
+ with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
unfolding C_def by (intro exI[of _ "f`T"]) fastforce
qed
@@ -3708,10 +3708,9 @@
assume f: "bounded (range f)"
obtain r where r: "subseq r" "monoseq (f \<circ> r)"
unfolding comp_def by (metis seq_monosub)
- moreover
then have "Bseq (f \<circ> r)"
unfolding Bseq_eq_bounded using f by (auto intro: bounded_subset)
- ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
+ with r show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
qed
@@ -5558,9 +5557,9 @@
and c: "\<And>y. y \<in> t \<Longrightarrow> c y \<in> C \<and> open (a y) \<and> open (b y) \<and> x \<in> a y \<and> y \<in> b y \<and> a y \<times> b y \<subseteq> c y"
by metis
then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
- from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
+ from compactE_image[OF `compact t` this] obtain D where D: "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
by auto
- moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
+ moreover from D c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
by (fastforce simp: subset_eq)
ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
@@ -7345,8 +7344,8 @@
shows "\<exists>S\<subseteq>A. card S = n"
proof cases
assume "finite A"
- from ex_bij_betw_nat_finite[OF this] guess f ..
- moreover with `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
+ from ex_bij_betw_nat_finite[OF this] guess f .. note f = this
+ moreover from f `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
by (auto simp: bij_betw_def intro: subset_inj_on)
ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
by (auto simp: bij_betw_def card_image)
--- a/src/HOL/Nat.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Nat.thy Tue Sep 03 22:30:52 2013 +0200
@@ -1888,8 +1888,8 @@
proof -
have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
by (auto elim: dvd_plusE)
- also with assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
- also with assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
+ also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
+ also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
finally show ?thesis .
qed
--- a/src/HOL/Nominal/Examples/Crary.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Tue Sep 03 22:30:52 2013 +0200
@@ -766,9 +766,8 @@
assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>"
shows "\<Gamma>' \<turnstile> s is s over \<Gamma>"
proof -
- have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact
- moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
- ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
+ from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
+ with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
qed
lemma logical_subst_monotonicity :
--- a/src/HOL/Number_Theory/Binomial.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy Tue Sep 03 22:30:52 2013 +0200
@@ -203,7 +203,7 @@
by (subst choose_reduce_nat, auto simp add: field_simps)
also note one
also note two
- also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
+ also from less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
apply (subst fact_plus_one_nat)
apply (subst distrib_right [symmetric])
apply simp
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Tue Sep 03 22:30:52 2013 +0200
@@ -298,7 +298,7 @@
proof -
have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
by (simp add: ring_simprules)
- also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
+ also from `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
by (simp add: ring_simprules)
finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
--- a/src/HOL/Predicate.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Predicate.thy Tue Sep 03 22:30:52 2013 +0200
@@ -225,9 +225,9 @@
"\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
proof -
assume assm: "\<exists>!x. eval A x"
- then obtain x where "eval A x" ..
- moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
- ultimately show ?thesis by simp
+ then obtain x where x: "eval A x" ..
+ with assm have "singleton dfault A = x" by (rule singleton_eqI)
+ with x show ?thesis by simp
qed
lemma single_singleton:
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 03 22:30:52 2013 +0200
@@ -54,7 +54,8 @@
sorted_single [code_pred_intro]
sorted_many [code_pred_intro]
-code_pred sorted proof -
+code_pred sorted
+proof -
assume "sorted xa"
assume 1: "xa = [] \<Longrightarrow> thesis"
assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
@@ -65,9 +66,12 @@
case (Cons x xs) show ?thesis proof (cases xs)
case Nil with Cons 2 show ?thesis by simp
next
- case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
- moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
- ultimately show ?thesis by (rule 3)
+ case (Cons y zs)
+ show ?thesis
+ proof (rule 3)
+ from Cons `xa = x # xs` show "xa = x # y # zs" by simp
+ with `sorted xa` show "x \<le> y" and "sorted (y # zs)" by simp_all
+ qed
qed
qed
qed
--- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Sep 03 22:30:52 2013 +0200
@@ -177,9 +177,9 @@
by (auto intro!: measurable_If simp: space_pair_measure)
next
case (union F)
- moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
+ then have "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
- ultimately show ?case
+ with union show ?case
unfolding sets_pair_measure[symmetric] by simp
qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
@@ -515,9 +515,9 @@
shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
using f proof induct
case (cong u v)
- moreover then have "?I u = ?I v"
+ then have "?I u = ?I v"
by (intro positive_integral_cong) (auto simp: space_pair_measure)
- ultimately show ?case
+ with cong show ?case
by (simp cong: positive_integral_cong)
qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
positive_integral_monotone_convergence_SUP
--- a/src/HOL/Probability/Fin_Map.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Tue Sep 03 22:30:52 2013 +0200
@@ -342,9 +342,9 @@
case (UN K)
show ?case
proof safe
- fix x X assume "x \<in> X" "X \<in> K"
- moreover with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
- ultimately show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
+ fix x X assume "x \<in> X" and X: "X \<in> K"
+ with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
+ with X show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
qed
next
case (Basis s) then obtain a b where s: "s = Pi' a b" and b: "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto
@@ -363,12 +363,10 @@
show "y \<in> s" unfolding s
proof
show "domain y = a" using d s `a \<noteq> {}` by (auto simp: dist_le_1_imp_domain_eq a_dom)
- fix i assume "i \<in> a"
- moreover
+ fix i assume i: "i \<in> a"
hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d
by (auto simp: dist_finmap_def `a \<noteq> {}` intro!: le_less_trans[OF dist_proj])
- ultimately
- show "y i \<in> b i" by (rule in_b)
+ with i show "y i \<in> b i" by (rule in_b)
qed
next
assume "\<not>a \<noteq> {}"
@@ -715,9 +713,9 @@
proof -
have "\<Union>{f s|s. P s} = (\<Union>n::nat. let s = set (from_nat n) in if P s then f s else {})"
proof safe
- fix x X s assume "x \<in> f s" "P s"
- moreover with assms obtain l where "s = set l" using finite_list by blast
- ultimately show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s`
+ fix x X s assume *: "x \<in> f s" "P s"
+ with assms obtain l where "s = set l" using finite_list by blast
+ with * show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s`
by (auto intro!: exI[where x="to_nat l"])
next
fix x n assume "x \<in> (let s = set (from_nat n) in if P s then f s else {})"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Sep 03 22:30:52 2013 +0200
@@ -235,7 +235,7 @@
using sets.sets_into_space by auto
then have "A = (\<Pi>\<^sub>E i\<in>I. if i\<in>J then E i else space (M i))"
using A J by (auto simp: prod_emb_PiE)
- moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
+ moreover have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
using sets.top E by auto
ultimately show ?thesis using that by auto
qed
@@ -792,9 +792,9 @@
proof (intro measure_eqI[symmetric])
interpret I: finite_product_sigma_finite M "{i}" by default simp
fix A assume A: "A \<in> sets (M i)"
- moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
+ then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
using sets.sets_into_space by (auto simp: space_PiM)
- ultimately show "emeasure (M i) A = emeasure ?D A"
+ then show "emeasure (M i) A = emeasure ?D A"
using A I.measure_times[of "\<lambda>_. A"]
by (simp add: emeasure_distr measurable_component_singleton)
qed simp
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Sep 03 22:30:52 2013 +0200
@@ -246,7 +246,7 @@
then show ?case by auto
qed
moreover
- then have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
+ from w have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
moreover
from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
then have "?M (J k) (A k) (w k) \<noteq> {}"
@@ -344,10 +344,10 @@
assume "I = {}" then show ?thesis by (simp add: space_PiM_empty)
next
assume "I \<noteq> {}"
- then obtain i where "i \<in> I" by auto
- moreover then have "emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)) = (space (Pi\<^sub>M I M))"
+ then obtain i where i: "i \<in> I" by auto
+ then have "emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)) = (space (Pi\<^sub>M I M))"
by (auto simp: prod_emb_def space_PiM)
- ultimately show ?thesis
+ with i show ?thesis
using emeasure_PiM_emb_not_empty[of "{i}" "\<lambda>i. space (M i)"]
by (simp add: emeasure_PiM emeasure_space_1)
qed
--- a/src/HOL/Probability/Information.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Information.thy Tue Sep 03 22:30:52 2013 +0200
@@ -381,10 +381,10 @@
shows "absolutely_continuous S (distr (S \<Otimes>\<^sub>M T) S fst)"
proof -
interpret sigma_finite_measure T by fact
- { fix A assume "A \<in> sets S" "emeasure S A = 0"
- moreover then have "fst -` A \<inter> space (S \<Otimes>\<^sub>M T) = A \<times> space T"
+ { fix A assume A: "A \<in> sets S" "emeasure S A = 0"
+ then have "fst -` A \<inter> space (S \<Otimes>\<^sub>M T) = A \<times> space T"
by (auto simp: space_pair_measure dest!: sets.sets_into_space)
- ultimately have "emeasure (S \<Otimes>\<^sub>M T) (fst -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
+ with A have "emeasure (S \<Otimes>\<^sub>M T) (fst -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
by (simp add: emeasure_pair_measure_Times) }
then show ?thesis
unfolding absolutely_continuous_def
@@ -398,10 +398,10 @@
shows "absolutely_continuous T (distr (S \<Otimes>\<^sub>M T) T snd)"
proof -
interpret sigma_finite_measure T by fact
- { fix A assume "A \<in> sets T" "emeasure T A = 0"
- moreover then have "snd -` A \<inter> space (S \<Otimes>\<^sub>M T) = space S \<times> A"
+ { fix A assume A: "A \<in> sets T" "emeasure T A = 0"
+ then have "snd -` A \<inter> space (S \<Otimes>\<^sub>M T) = space S \<times> A"
by (auto simp: space_pair_measure dest!: sets.sets_into_space)
- ultimately have "emeasure (S \<Otimes>\<^sub>M T) (snd -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
+ with A have "emeasure (S \<Otimes>\<^sub>M T) (snd -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
by (simp add: emeasure_pair_measure_Times) }
then show ?thesis
unfolding absolutely_continuous_def
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Sep 03 22:30:52 2013 +0200
@@ -675,12 +675,11 @@
assumes f: "simple_function M f"
shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
(\<Sum>x \<in> f ` space M. x * (emeasure M) (f -` {x} \<inter> space M \<inter> A))"
-proof cases
- assume "A = space M"
- moreover hence "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
+proof (cases "A = space M")
+ case True
+ then have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
by (auto intro!: simple_integral_cong)
- moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
- ultimately show ?thesis by (simp add: simple_integral_def)
+ with True show ?thesis by (simp add: simple_integral_def)
next
assume "A \<noteq> space M"
then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
@@ -1001,10 +1000,10 @@
unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
proof (safe intro!: SUP_least)
fix g assume g: "simple_function M g"
- and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
- moreover then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
+ and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
+ then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
using f by (auto intro!: SUP_upper2)
- ultimately show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
+ with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
by (intro positive_integral_SUP_approx[OF f g _ g'])
(auto simp: le_fun_def max_def)
qed
@@ -1357,7 +1356,7 @@
proof (safe intro!: incseq_SucI)
fix n :: nat and x
assume *: "1 \<le> real n * u x"
- also from gt_1[OF this] have "real n * u x \<le> real (Suc n) * u x"
+ also from gt_1[OF *] have "real n * u x \<le> real (Suc n) * u x"
using `0 \<le> u x` by (auto intro!: ereal_mult_right_mono)
finally show "1 \<le> real (Suc n) * u x" by auto
qed
@@ -2658,10 +2657,9 @@
using f by (simp add: positive_integral_cmult)
next
case (add u v)
- moreover then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
+ then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
by (simp add: ereal_right_distrib)
- moreover note f
- ultimately show ?case
+ with add f show ?case
by (auto simp add: positive_integral_add ereal_zero_le_0_iff intro!: positive_integral_add[symmetric])
next
case (seq U)
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Sep 03 22:30:52 2013 +0200
@@ -983,22 +983,20 @@
shows "integrable lborel f \<longleftrightarrow> integrable (\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel) (\<lambda>x. f (p2e x))"
(is "_ \<longleftrightarrow> integrable ?B ?f")
proof
- assume "integrable lborel f"
- moreover then have f: "f \<in> borel_measurable borel"
+ assume *: "integrable lborel f"
+ then have f: "f \<in> borel_measurable borel"
by auto
- moreover with measurable_p2e
- have "f \<circ> p2e \<in> borel_measurable ?B"
+ with measurable_p2e have "f \<circ> p2e \<in> borel_measurable ?B"
by (rule measurable_comp)
- ultimately show "integrable ?B ?f"
+ with * f show "integrable ?B ?f"
by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
next
- assume "integrable ?B ?f"
- moreover
+ assume *: "integrable ?B ?f"
then have "?f \<circ> e2p \<in> borel_measurable (borel::'a measure)"
by (auto intro!: measurable_e2p)
then have "f \<in> borel_measurable borel"
by (simp cong: measurable_cong)
- ultimately show "integrable lborel f"
+ with * show "integrable lborel f"
by (simp add: borel_fubini_positiv_integral integrable_def)
qed
--- a/src/HOL/Probability/Measure_Space.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Tue Sep 03 22:30:52 2013 +0200
@@ -158,7 +158,8 @@
and A: "A`S \<subseteq> M"
and disj: "disjoint_family_on A S"
shows "(\<Sum>i\<in>S. f (A i)) = f (\<Union>i\<in>S. A i)"
-using `finite S` disj A proof induct
+ using `finite S` disj A
+proof induct
case empty show ?case using f by (simp add: positive_def)
next
case (insert s S)
@@ -168,7 +169,6 @@
have "A s \<in> M" using insert by blast
moreover have "(\<Union>i\<in>S. A i) \<in> M"
using insert `finite S` by auto
- moreover
ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)"
using ad UNION_in_sets A by (auto simp add: additive_def)
with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A]
@@ -781,15 +781,15 @@
using sets.sets_into_space by auto
show "{} \<in> null_sets M"
by auto
- fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
- then have "A \<in> sets M" "B \<in> sets M"
+ fix A B assume null_sets: "A \<in> null_sets M" "B \<in> null_sets M"
+ then have sets: "A \<in> sets M" "B \<in> sets M"
by auto
- moreover then have "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
+ then have *: "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
"emeasure M (A - B) \<le> emeasure M A"
by (auto intro!: emeasure_subadditive emeasure_mono)
- moreover have "emeasure M B = 0" "emeasure M A = 0"
- using sets by auto
- ultimately show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
+ then have "emeasure M B = 0" "emeasure M A = 0"
+ using null_sets by auto
+ with sets * show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
by (auto intro!: antisym)
qed
@@ -1563,9 +1563,9 @@
by (auto intro!: Lim_eventually eventually_sequentiallyI[where c=i])
next
assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
- then obtain f where "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
- moreover then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
- ultimately have *: "\<And>i. F i \<subset> F (f i)" by auto
+ then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
+ then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
+ with f have *: "\<And>i. F i \<subset> F (f i)" by auto
have "incseq (\<lambda>i. ?M (F i))"
using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
--- a/src/HOL/Probability/Projective_Limit.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy Tue Sep 03 22:30:52 2013 +0200
@@ -257,14 +257,13 @@
finally have "fm n x \<in> fm n ` B n" .
thus "x \<in> B n"
proof safe
- fix y assume "y \<in> B n"
- moreover
+ fix y assume y: "y \<in> B n"
hence "y \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
by (auto simp add: proj_space proj_sets)
assume "fm n x = fm n y"
note inj_onD[OF inj_on_fm[OF space_borel],
OF `fm n x = fm n y` `x \<in> space _` `y \<in> space _`]
- ultimately show "x \<in> B n" by simp
+ with y show "x \<in> B n" by simp
qed
qed
{ fix n
@@ -438,10 +437,11 @@
apply (subst (2) tendsto_iff, subst eventually_sequentially)
proof safe
fix e :: real assume "0 < e"
- { fix i x assume "i \<ge> n" "t \<in> domain (fm n x)"
- moreover
+ { fix i x
+ assume i: "i \<ge> n"
+ assume "t \<in> domain (fm n x)"
hence "t \<in> domain (fm i x)" using J_mono[OF `i \<ge> n`] by auto
- ultimately have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
+ with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn])
} note index_shift = this
have I: "\<And>i. i \<ge> n \<Longrightarrow> Suc (diagseq i) \<ge> n"
@@ -487,11 +487,11 @@
also have "finmap_of (Utn ` J n) z = fm n (\<lambda>i. z (Utn i))"
unfolding finmap_eq_iff
proof clarsimp
- fix i assume "i \<in> J n"
- moreover hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
+ fix i assume i: "i \<in> J n"
+ hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
unfolding Utn_def
by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto
- ultimately show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
+ with i show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
by (simp add: finmap_eq_iff fm_def compose_def)
qed
finally have "fm n (\<lambda>i. z (Utn i)) \<in> K' n" .
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Sep 03 22:30:52 2013 +0200
@@ -412,14 +412,14 @@
have ac: "absolutely_continuous M ?M" unfolding absolutely_continuous_def
proof
- fix A assume A: "A \<in> null_sets M"
- with `absolutely_continuous M N` have "A \<in> null_sets N"
+ fix A assume A_M: "A \<in> null_sets M"
+ with `absolutely_continuous M N` have A_N: "A \<in> null_sets N"
unfolding absolutely_continuous_def by auto
- moreover with A have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
+ moreover from A_M A_N have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0"
using positive_integral_positive[of M] by (auto intro!: antisym)
then show "A \<in> null_sets ?M"
- using A by (simp add: emeasure_M null_sets_def sets_eq)
+ using A_M by (simp add: emeasure_M null_sets_def sets_eq)
qed
have upper_bound: "\<forall>A\<in>sets M. ?M A \<le> 0"
proof (rule ccontr)
@@ -431,7 +431,7 @@
using emeasure_space[of ?M A] by (simp add: sets_eq[THEN sets_eq_imp_space_eq])
finally have pos_t: "0 < ?M (space M)" by simp
moreover
- then have "emeasure M (space M) \<noteq> 0"
+ from pos_t have "emeasure M (space M) \<noteq> 0"
using ac unfolding absolutely_continuous_def by (auto simp: null_sets_def)
then have pos_M: "0 < emeasure M (space M)"
using emeasure_nonneg[of M "space M"] by (simp add: le_less)
@@ -594,12 +594,14 @@
proof (rule disjCI, simp)
assume *: "0 < emeasure M A \<longrightarrow> N A \<noteq> \<infinity>"
show "emeasure M A = 0 \<and> N A = 0"
- proof cases
- assume "emeasure M A = 0" moreover with ac A have "N A = 0"
+ proof (cases "emeasure M A = 0")
+ case True
+ with ac A have "N A = 0"
unfolding absolutely_continuous_def by auto
- ultimately show ?thesis by simp
+ with True show ?thesis by simp
next
- assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
+ case False
+ with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
using Q' by (auto intro!: plus_emeasure sets.countable_UN)
also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 03 22:30:52 2013 +0200
@@ -1244,8 +1244,8 @@
interpret N: sigma_algebra \<Omega>' A' using measure_measure by (auto simp: measure_space_def)
have "A = sets M" "A' = sets N"
using measure_measure by (simp_all add: sets_def Abs_measure_inverse)
- with `sets M = sets N` have "A = A'" by simp
- moreover with M.top N.top M.space_closed N.space_closed have "\<Omega> = \<Omega>'" by auto
+ with `sets M = sets N` have AA': "A = A'" by simp
+ moreover from M.top N.top M.space_closed N.space_closed AA' have "\<Omega> = \<Omega>'" by auto
moreover { fix B have "\<mu> B = \<mu>' B"
proof cases
assume "B \<in> A"
@@ -1977,7 +1977,7 @@
moreover have "D \<union> (\<Omega> - E) = (\<Union>i. ?f i)"
by (auto simp: image_iff split: split_if_asm)
moreover
- then have "disjoint_family ?f" unfolding disjoint_family_on_def
+ have "disjoint_family ?f" unfolding disjoint_family_on_def
using `D \<in> M`[THEN sets_into_space] `D \<subseteq> E` by auto
ultimately have "\<Omega> - (D \<union> (\<Omega> - E)) \<in> M"
using sets by auto
@@ -2193,11 +2193,11 @@
proof -
have "E \<subseteq> Pow \<Omega>"
using E sets_into_space by force
- then have "sigma_sets \<Omega> E = dynkin \<Omega> E"
+ then have *: "sigma_sets \<Omega> E = dynkin \<Omega> E"
using `Int_stable E` by (rule sigma_eq_dynkin)
- moreover then have "dynkin \<Omega> E = M"
+ then have "dynkin \<Omega> E = M"
using assms dynkin_subset[OF E(1)] by simp
- ultimately show ?thesis
+ with * show ?thesis
using assms by (auto simp: dynkin_def)
qed
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Sep 03 22:30:52 2013 +0200
@@ -5,7 +5,7 @@
lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
by (unfold inj_on_def) blast
-lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
+lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
by auto
section "Define the state space"
@@ -143,8 +143,8 @@
thus "x ! j = y ! j"
proof (induct j)
case (Suc j)
- moreover hence "j < n" by simp
- ultimately show ?case using *[OF `j < n`]
+ hence "j < n" by simp
+ with Suc show ?case using *[OF `j < n`]
by (cases "y ! j") simp_all
qed simp
qed
@@ -234,7 +234,7 @@
hence zs: "inversion (Some i, zs) = xs"
by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
moreover
- hence Not_zs: "inversion (Some i, (map Not zs)) = xs"
+ from zs have Not_zs: "inversion (Some i, (map Not zs)) = xs"
by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
ultimately
have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
--- a/src/HOL/Quotient_Examples/FSet.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue Sep 03 22:30:52 2013 +0200
@@ -1033,9 +1033,9 @@
case (insert x A)
from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})"
by (auto simp add: in_fset)
- then have "A = B - {|x|}" by (rule insert.hyps(2))
- moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
- ultimately show ?case by (metis in_fset_mdef)
+ then have A: "A = B - {|x|}" by (rule insert.hyps(2))
+ with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
+ with A show ?case by (metis in_fset_mdef)
qed
subsection {* alternate formulation with a different decomposition principle
--- a/src/HOL/Rat.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Rat.thy Tue Sep 03 22:30:52 2013 +0200
@@ -237,7 +237,7 @@
next
case False
then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
- moreover with False have "0 \<noteq> Fract a b" by simp
+ with False have "0 \<noteq> Fract a b" by simp
with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
qed
--- a/src/HOL/Real.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Real.thy Tue Sep 03 22:30:52 2013 +0200
@@ -947,7 +947,7 @@
using complete_real[of X] by blast
then have "Sup X = s"
unfolding Sup_real_def by (best intro: Least_equality)
- also with s z have "... \<le> z"
+ also from s z have "... \<le> z"
by blast
finally show "Sup X \<le> z" . }
note Sup_least = this
--- a/src/HOL/Real_Vector_Spaces.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Sep 03 22:30:52 2013 +0200
@@ -758,10 +758,10 @@
show "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"])
fix S assume "open S" "x \<in> S"
- then obtain e where "0 < e" "{y. dist x y < e} \<subseteq> S"
+ then obtain e where e: "0 < e" and "{y. dist x y < e} \<subseteq> S"
by (auto simp: open_dist subset_eq dist_commute)
moreover
- then obtain i where "inverse (Suc i) < e"
+ from e obtain i where "inverse (Suc i) < e"
by (auto dest!: reals_Archimedean)
then have "{y. dist x y < inverse (Suc i)} \<subseteq> {y. dist x y < e}"
by auto
@@ -833,7 +833,8 @@
show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
proof (rule ext, safe)
fix S :: "real set" assume "open S"
- then guess f unfolding open_real_def bchoice_iff ..
+ then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
+ unfolding open_real_def bchoice_iff ..
then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
by (fastforce simp: dist_real_def)
show "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1525,7 +1526,8 @@
with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
by (auto simp: LIMSEQ_def dist_real_def)
{ fix x :: real
- from ex_le_of_nat[of x] guess n ..
+ obtain n where "x \<le> real_of_nat n"
+ using ex_le_of_nat[of x] ..
note monoD[OF mono this]
also have "f (real_of_nat n) \<le> y"
by (rule LIMSEQ_le_const[OF limseq])
--- a/src/HOL/Set_Interval.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Set_Interval.thy Tue Sep 03 22:30:52 2013 +0200
@@ -269,9 +269,9 @@
"{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
proof
assume "{a..b} = {c}"
- hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
- moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
- ultimately show "a = b \<and> b = c" by auto
+ hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
+ with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
+ with * show "a = b \<and> b = c" by auto
qed simp
lemma Icc_subset_Ici_iff[simp]:
@@ -827,21 +827,23 @@
subset is exactly that interval. *}
lemma subset_card_intvl_is_intvl:
- "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
-proof cases
- assume "finite A"
- thus "PROP ?P"
- proof(induct A rule:finite_linorder_max_induct)
+ assumes "A \<subseteq> {k..<k+card A}"
+ shows "A = {k..<k+card A}"
+proof (cases "finite A")
+ case True
+ from this and assms show ?thesis
+ proof (induct A rule: finite_linorder_max_induct)
case empty thus ?case by auto
next
case (insert b A)
- moreover hence "b ~: A" by auto
- moreover have "A <= {k..<k+card A}" and "b = k+card A"
- using `b ~: A` insert by fastforce+
- ultimately show ?case by auto
+ hence *: "b \<notin> A" by auto
+ with insert have "A <= {k..<k+card A}" and "b = k+card A"
+ by fastforce+
+ with insert * show ?case by auto
qed
next
- assume "~finite A" thus "PROP ?P" by simp
+ case False
+ with assms show ?thesis by simp
qed
@@ -1470,7 +1472,7 @@
case 0 then show ?case by simp
next
case (Suc n)
- moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
+ moreover from Suc `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
ultimately show ?case by (simp add: field_simps divide_inverse)
qed
ultimately show ?thesis by simp
--- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 03 22:30:52 2013 +0200
@@ -572,13 +572,13 @@
shows "delete x (Node l y d r) = Some (Node l' y d r)"
proof -
from delete_Some_x_set_of [OF del_l]
- obtain "x \<in> set_of l"
+ obtain x: "x \<in> set_of l"
by simp
- moreover with dist
+ with dist
have "delete x r = None"
by (cases "delete x r") (auto dest:delete_Some_x_set_of)
- ultimately
+ with x
show ?thesis
using del_l dist
by (auto split: option.splits)
@@ -590,13 +590,13 @@
shows "delete x (Node l y d r) = Some (Node l y d r')"
proof -
from delete_Some_x_set_of [OF del_r]
- obtain "x \<in> set_of r"
+ obtain x: "x \<in> set_of r"
by simp
- moreover with dist
+ with dist
have "delete x l = None"
by (cases "delete x l") (auto dest:delete_Some_x_set_of)
- ultimately
+ with x
show ?thesis
using del_r dist
by (auto split: option.splits)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 03 22:30:52 2013 +0200
@@ -456,11 +456,11 @@
provide a hint to the user. *)
fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
not (null fixes) andalso
- exists (String.isSuffix ".hyps" o fst) assumes andalso
+ exists (String.isSuffix ".hyps" o Name_Space.full_name Name_Space.default_naming o fst) assumes andalso
exists (exists (curry (op =) name o shortest_name o fst)
o datatype_constrs hol_ctxt) deep_dataTs
val likely_in_struct_induct_step =
- exists is_struct_induct_step (Proof_Context.cases_of ctxt)
+ exists is_struct_induct_step (Proof_Context.dest_cases ctxt)
val _ = if standard andalso likely_in_struct_induct_step then
pprint_nt (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 03 22:30:52 2013 +0200
@@ -1574,6 +1574,9 @@
Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
"adding alternative introduction rules for code generation of inductive predicates"
+fun qualified_binding a =
+ Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
+
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
(* FIXME ... this is important to avoid changing the background theory below *)
fun generic_code_pred prep_const options raw_const lthy =
@@ -1593,14 +1596,17 @@
val cases_rules = map mk_cases preds
val cases =
map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
- assumes = ("that", tl (Logic.strip_imp_prems case_rule))
- :: (map_filter (fn (fact_name, fact) => Option.map (rpair [fact]) fact_name)
- ((SOME (Long_Name.base_name pred_name ^ ".prems") :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule)),
+ assumes =
+ (Binding.name "that", tl (Logic.strip_imp_prems case_rule)) ::
+ map_filter (fn (fact_name, fact) =>
+ Option.map (fn a => (qualified_binding a, [fact])) fact_name)
+ ((SOME (Long_Name.base_name pred_name ^ ".prems") :: names_of ctxt' pred_name) ~~
+ Logic.strip_imp_prems case_rule),
binds = [], cases = []}) preds cases_rules
val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
val lthy'' = lthy'
|> fold Variable.auto_fixes cases_rules
- |> Proof_Context.add_cases true case_env
+ |> Proof_Context.update_cases true case_env
fun after_qed thms goal_ctxt =
let
val global_thms = Proof_Context.export goal_ctxt
--- a/src/HOL/Topological_Spaces.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Sep 03 22:30:52 2013 +0200
@@ -215,14 +215,14 @@
lemma (in linorder) less_separate:
assumes "x < y"
shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
-proof cases
- assume "\<exists>z. x < z \<and> z < y"
- then guess z ..
+proof (cases "\<exists>z. x < z \<and> z < y")
+ case True
+ then obtain z where "x < z \<and> z < y" ..
then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
by auto
then show ?thesis by blast
next
- assume "\<not> (\<exists>z. x < z \<and> z < y)"
+ case False
with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
by auto
then show ?thesis by blast
@@ -570,10 +570,11 @@
lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
unfolding eventually_at_top_linorder
proof safe
- fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
+ fix N assume "\<forall>n\<ge>N. P n"
+ then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
next
fix N assume "\<forall>n>N. P n"
- moreover from gt_ex[of N] guess y ..
+ moreover obtain y where "N < y" using gt_ex[of N] ..
ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
qed
@@ -606,7 +607,7 @@
fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
next
fix N assume "\<forall>n<N. P n"
- moreover from lt_ex[of N] guess y ..
+ moreover obtain y where "y < N" using lt_ex[of N] ..
ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
qed
@@ -765,7 +766,7 @@
shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
unfolding eventually_at_topological
proof safe
- from gt_ex[of x] guess y ..
+ obtain y where "x < y" using gt_ex[of x] ..
moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
moreover note gt_ex[of x]
moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
@@ -782,7 +783,7 @@
shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
unfolding eventually_at_topological
proof safe
- from lt_ex[of x] guess y ..
+ obtain y where "y < x" using lt_ex[of x] ..
moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
@@ -1513,10 +1514,16 @@
"\<And>i. open (A i)" "\<And>i. x \<in> A i"
"\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F ----> x"
proof atomize_elim
- from countable_basis_at_decseq[of x] guess A . note A = this
- { fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
+ obtain A :: "nat \<Rightarrow> 'a set" where A:
+ "\<And>i. open (A i)"
+ "\<And>i. x \<in> A i"
+ "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+ by (rule countable_basis_at_decseq) blast
+ {
+ fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
- by (auto elim: eventually_elim1 simp: subset_eq) }
+ by (auto elim: eventually_elim1 simp: subset_eq)
+ }
with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F ----> x)"
by (intro exI[of _ A]) (auto simp: tendsto_def)
qed
@@ -1525,13 +1532,16 @@
assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
shows "eventually P (inf (nhds a) (principal s))"
proof (rule ccontr)
- from countable_basis[of a] guess A . note A = this
- assume "\<not> eventually P (inf (nhds a) (principal s))"
+ obtain A :: "nat \<Rightarrow> 'a set" where A:
+ "\<And>i. open (A i)"
+ "\<And>i. a \<in> A i"
+ "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F ----> a"
+ by (rule countable_basis) blast
+ assume "\<not> ?thesis"
with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
- then guess F ..
- hence F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
- by fast+
+ then obtain F where F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
+ by blast
with A have "F ----> a" by auto
hence "eventually (\<lambda>n. P (F n)) sequentially"
using assms F0 by simp
@@ -1668,7 +1678,8 @@
fix B :: "'b set" assume "continuous_on s f" "open B"
then have "\<forall>x\<in>f -` B \<inter> s. (\<exists>A. open A \<and> x \<in> A \<and> s \<inter> A \<subseteq> f -` B)"
by (auto simp: continuous_on_topological subset_eq Ball_def imp_conjL)
- then guess A unfolding bchoice_iff ..
+ then obtain A where "\<forall>x\<in>f -` B \<inter> s. open (A x) \<and> x \<in> A x \<and> s \<inter> A x \<subseteq> f -` B"
+ unfolding bchoice_iff ..
then show "\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s"
by (intro exI[of _ "\<Union>x\<in>f -` B \<inter> s. A x"]) auto
next
@@ -1883,7 +1894,7 @@
moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
using `compact s` unfolding compact_eq_heine_borel by auto
- then guess D ..
+ then obtain D where "D \<subseteq> C \<union> {- t} \<and> finite D \<and> s \<subseteq> \<Union>D" ..
then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
by (intro exI[of _ "D - {-t}"]) auto
qed
@@ -1925,7 +1936,8 @@
fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
unfolding continuous_on_open_invariant by blast
- then guess A unfolding bchoice_iff .. note A = this
+ then obtain A where A: "\<forall>c\<in>C. open (A c) \<and> A c \<inter> s = f -` c \<inter> s"
+ unfolding bchoice_iff ..
with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
by (fastforce simp add: subset_eq set_eq_iff)+
from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
@@ -2114,7 +2126,8 @@
instance linear_continuum_topology \<subseteq> perfect_space
proof
fix x :: 'a
- from ex_gt_or_lt [of x] guess y ..
+ obtain y where "x < y \<or> y < x"
+ using ex_gt_or_lt [of x] ..
with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y]
show "\<not> open {x}"
by auto
@@ -2145,7 +2158,8 @@
moreover obtain b where "b \<in> B" "x < b" "b < min a y"
using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
by (auto intro: less_imp_le)
- moreover then have "?z \<le> b"
+ moreover have "?z \<le> b"
+ using `b \<in> B` `x < b`
by (intro cInf_lower[where z=x]) auto
moreover have "b \<in> U"
using `x \<le> ?z` `?z \<le> b` `b < min a y`
--- a/src/HOL/ex/Dedekind_Real.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Tue Sep 03 22:30:52 2013 +0200
@@ -8,7 +8,7 @@
*)
theory Dedekind_Real
-imports Rat Lubs
+imports Complex_Main
begin
section {* Positive real numbers *}
@@ -782,7 +782,7 @@
have "r + ?d < r*x"
proof -
have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
- also with ypos have "... = (r/y) * (y + ?d)"
+ also from ypos have "... = (r/y) * (y + ?d)"
by (simp only: algebra_simps divide_inverse, simp)
also have "... = r*x" using ypos
by simp
@@ -1785,10 +1785,10 @@
proof
fix pa
assume "pa \<in> ?pS"
- then obtain a where "a \<in> S" and "a = real_of_preal pa"
+ then obtain a where a: "a \<in> S" "a = real_of_preal pa"
by simp
- moreover hence "a \<le> u" using sup by simp
- ultimately show "pa \<le> pu"
+ then have "a \<le> u" using sup by simp
+ with a show "pa \<le> pu"
using sup and u_is_pu by (simp add: real_of_preal_le_iff)
qed
@@ -1864,9 +1864,9 @@
fix s
assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
hence "\<exists> x \<in> S. s = x + -X + 1" ..
- then obtain x1 where "x1 \<in> S" and "s = x1 + (-X) + 1" ..
- moreover hence "x1 \<le> x" using S_le_x by simp
- ultimately have "s \<le> x + - X + 1" by arith
+ then obtain x1 where x1: "x1 \<in> S" "s = x1 + (-X) + 1" ..
+ then have "x1 \<le> x" using S_le_x by simp
+ with x1 have "s \<le> x + - X + 1" by arith
}
then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
by (auto simp add: isUb_def setle_def)
--- a/src/HOL/ex/HarmonicSeries.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/HOL/ex/HarmonicSeries.thy Tue Sep 03 22:30:52 2013 +0200
@@ -65,7 +65,7 @@
proof -
from xs have
"x \<ge> 2^(m - 1) + 1" by auto
- moreover with mgt0 have
+ moreover from mgt0 have
"2^(m - 1) + 1 \<ge> (1::nat)" by auto
ultimately have
"x \<ge> 1" by (rule xtrans)
--- a/src/Pure/General/binding.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/General/binding.ML Tue Sep 03 22:30:52 2013 +0200
@@ -9,10 +9,11 @@
signature BINDING =
sig
- type binding
+ eqtype binding
val dest: binding -> bool * (string * bool) list * bstring
val make: bstring * Position.T -> binding
val pos_of: binding -> Position.T
+ val set_pos: Position.T -> binding -> binding
val name: bstring -> binding
val name_of: binding -> bstring
val map_name: (bstring -> bstring) -> binding -> binding
@@ -41,13 +42,12 @@
(* datatype *)
-abstype binding = Binding of
+datatype binding = Binding of
{conceal: bool, (*internal -- for foundational purposes only*)
prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
name: bstring, (*base name*)
- pos: Position.T} (*source position*)
-with
+ pos: Position.T}; (*source position*)
fun make_binding (conceal, prefix, qualifier, name, pos) =
Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -65,9 +65,12 @@
(* name and position *)
fun make (name, pos) = make_binding (false, [], [], name, pos);
-fun name name = make (name, Position.none);
fun pos_of (Binding {pos, ...}) = pos;
+fun set_pos pos =
+ map_binding (fn (conceal, prefix, qualifier, name, _) => (conceal, prefix, qualifier, name, pos));
+
+fun name name = make (name, Position.none);
fun name_of (Binding {name, ...}) = name;
fun eq_name (b, b') = name_of b = name_of b';
@@ -140,7 +143,6 @@
else legacy_feature (bad binding);
end;
-end;
type binding = Binding.binding;
--- a/src/Pure/Isar/isar_syn.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Sep 03 22:30:52 2013 +0200
@@ -608,14 +608,13 @@
(opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
>> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
-val case_spec =
- (@{keyword "("} |--
- Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
- Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
-
val _ =
Outer_Syntax.command @{command_spec "case"} "invoke local context"
- (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
+ ((@{keyword "("} |--
+ Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
+ --| @{keyword ")"}) ||
+ Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
+ Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
(* proof structure *)
--- a/src/Pure/Isar/keyword.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Isar/keyword.ML Tue Sep 03 22:30:52 2013 +0200
@@ -36,6 +36,7 @@
val prf_decl: T
val prf_asm: T
val prf_asm_goal: T
+ val prf_asm_goal_script: T
val prf_script: T
val kinds: T list
val tag: string -> T -> T
@@ -115,13 +116,14 @@
val prf_decl = kind "prf_decl";
val prf_asm = kind "prf_asm";
val prf_asm_goal = kind "prf_asm_goal";
+val prf_asm_goal_script = kind "prf_asm_goal_script";
val prf_script = kind "prf_script";
val kinds =
[control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
- prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+ prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
(* tags *)
@@ -242,14 +244,14 @@
val is_proof = command_category
[qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
- prf_asm, prf_asm_goal, prf_script];
+ prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
val is_proof_body = command_category
- [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
- prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+ [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain,
+ prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
val is_theory_goal = command_category [thy_goal];
-val is_proof_goal = command_category [prf_goal, prf_asm_goal];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
val is_qed = command_category [qed, qed_block];
val is_qed_global = command_category [qed_global];
--- a/src/Pure/Isar/keyword.scala Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Isar/keyword.scala Tue Sep 03 22:30:52 2013 +0200
@@ -38,6 +38,7 @@
val PRF_DECL = "prf_decl"
val PRF_ASM = "prf_asm"
val PRF_ASM_GOAL = "prf_asm_goal"
+ val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
val PRF_SCRIPT = "prf_script"
@@ -52,11 +53,11 @@
val theory1 = Set(THY_BEGIN, THY_END)
val theory2 = Set(THY_DECL, THY_GOAL)
val proof =
- Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL,
- PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
+ Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
+ PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
val proof1 =
Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
- val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
+ val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
val improper = Set(THY_SCRIPT, PRF_SCRIPT)
}
--- a/src/Pure/Isar/proof.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Isar/proof.ML Tue Sep 03 22:30:52 2013 +0200
@@ -70,8 +70,10 @@
val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
val unfolding: ((thm list * attribute list) list) list -> state -> state
val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val invoke_case: string * binding option list * attribute list -> state -> state
- val invoke_case_cmd: string * binding option list * Attrib.src list -> state -> state
+ val invoke_case: (string * Position.T) * binding option list * attribute list ->
+ state -> state
+ val invoke_case_cmd: (string * Position.T) * binding option list * Attrib.src list ->
+ state -> state
val begin_block: state -> state
val next_block: state -> state
val end_block: state -> state
@@ -399,8 +401,8 @@
Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
state
|> map_goal
- (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #>
- Proof_Context.add_cases true meth_cases)
+ (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
+ Proof_Context.update_cases true meth_cases)
(K (statement, [], using, goal', before_qed, after_qed)) I)
end;
@@ -741,20 +743,18 @@
local
-fun qualified_binding a =
- Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
-
-fun gen_invoke_case prep_att (name, xs, raw_atts) state =
+fun gen_invoke_case prep_att ((name, pos), xs, raw_atts) state =
let
val atts = map (prep_att (context_of state)) raw_atts;
val (asms, state') = state |> map_context_result (fn ctxt =>
- ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
- val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
+ ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt (name, pos) xs));
+ val assumptions =
+ asms |> map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts));
in
state'
|> assume assumptions
|> bind_terms Auto_Bind.no_facts
- |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
+ |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
end;
in
--- a/src/Pure/Isar/proof_context.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Sep 03 22:30:52 2013 +0200
@@ -31,7 +31,6 @@
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
val facts_of: Proof.context -> Facts.T
- val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
val naming_of: Proof.context -> Name_Space.naming
val restore_naming: Proof.context -> Proof.context -> Proof.context
@@ -132,9 +131,10 @@
val add_assms_i: Assumption.export ->
(Thm.binding * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
- val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
- val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
- val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
+ val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
+ val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
+ val apply_case: Rule_Cases.T -> Proof.context -> (binding * term list) list * Proof.context
+ val check_case: Proof.context -> string * Position.T -> binding option list -> Rule_Cases.T
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -192,6 +192,9 @@
(** Isar proof context information **)
+type cases = ((Rule_Cases.T * bool) * int) Name_Space.table;
+val empty_cases: cases = Name_Space.empty_table Markup.caseN;
+
datatype data =
Data of
{mode: mode, (*inner syntax mode*)
@@ -199,7 +202,7 @@
tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
facts: Facts.T, (*local facts*)
- cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*)
+ cases: cases}; (*named case contexts: case, is_proper, running index*)
fun make_data (mode, syntax, tsig, consts, facts, cases) =
Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
@@ -210,7 +213,7 @@
fun init thy =
make_data (mode_default, Local_Syntax.init thy,
(Sign.tsig_of thy, Sign.tsig_of thy),
- (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
+ (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
);
fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
@@ -1132,28 +1135,23 @@
(** cases **)
+fun dest_cases ctxt =
+ Symtab.fold (fn (a, (c, i)) => cons (i, (a, c))) (#2 (cases_of ctxt)) []
+ |> sort (int_ord o pairself #1) |> map #2;
+
local
-fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name;
-
-fun add_case _ ("", _) cases = cases
- | add_case _ (name, NONE) cases = rem_case name cases
- | add_case is_proper (name, SOME c) cases = (name, (c, is_proper)) :: rem_case name cases;
-
-fun prep_case name fxs c =
- let
- fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
- | replace [] ys = ys
- | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
- val Rule_Cases.Case {fixes, assumes, binds, cases} = c;
- val fixes' = replace fxs fixes;
- val binds' = map drop_schematic binds;
- in
- if null (fold (Term.add_tvarsT o snd) fixes []) andalso
- null (fold (fold Term.add_vars o snd) assumes []) then
- Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
- else error ("Illegal schematic variable(s) in case " ^ quote name)
- end;
+fun update_case _ _ ("", _) res = res
+ | update_case _ _ (name, NONE) ((space, tab), index) =
+ let
+ val tab' = Symtab.delete_safe name tab;
+ in ((space, tab'), index) end
+ | update_case context is_proper (name, SOME c) (cases, index) =
+ let
+ val (_, cases') = cases |> Name_Space.define context false
+ (Binding.make (name, Position.none), ((c, is_proper), index));
+ val index' = index + 1;
+ in (cases', index') end;
fun fix (b, T) ctxt =
let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
@@ -1161,7 +1159,13 @@
in
-fun add_cases is_proper = map_cases o fold (add_case is_proper);
+fun update_cases is_proper args ctxt =
+ let
+ val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming);
+ val cases = cases_of ctxt;
+ val index = Symtab.fold (fn _ => Integer.add 1) (#2 cases) 0;
+ val (cases', _) = fold (update_case context is_proper) args (cases, index);
+ in map_cases (K cases') ctxt end;
fun case_result c ctxt =
let
@@ -1171,16 +1175,29 @@
in
ctxt'
|> bind_terms (map drop_schematic binds)
- |> add_cases true (map (apsnd SOME) cases)
+ |> update_cases true (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;
val apply_case = apfst fst oo case_result;
-fun get_case ctxt name xs =
- (case AList.lookup (op =) (cases_of ctxt) name of
- NONE => error ("Unknown case: " ^ quote name)
- | SOME (c, _) => prep_case name xs c);
+fun check_case ctxt (name, pos) fxs =
+ let
+ val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, _), _)) =
+ Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
+
+ fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
+ | replace [] ys = ys
+ | replace (_ :: _) [] =
+ error ("Too many parameters for case " ^ quote name ^ Position.here pos);
+ val fixes' = replace fxs fixes;
+ val binds' = map drop_schematic binds;
+ in
+ if null (fold (Term.add_tvarsT o snd) fixes []) andalso
+ null (fold (fold Term.add_vars o snd) assumes []) then
+ Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
+ else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos)
+ end;
end;
@@ -1256,8 +1273,9 @@
[Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
Pretty.quote (prt_term t)];
- fun prt_asm (a, ts) = Pretty.block (Pretty.breaks
- ((if a = "" then [] else [Pretty.str (a ^ ":")]) @ map (Pretty.quote o prt_term) ts));
+ fun prt_asm (b, ts) = Pretty.block (Pretty.breaks
+ ((if Binding.is_empty b then []
+ else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts));
fun prt_sect _ _ _ [] = []
| prt_sect s sep prt xs =
@@ -1278,10 +1296,10 @@
fun pretty_cases ctxt =
let
- fun add_case (_, (_, false)) = I
- | add_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
- cons (name, (fixes, case_result c ctxt));
- val cases = fold add_case (cases_of ctxt) [];
+ fun mk_case (_, (_, false)) = NONE
+ | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
+ SOME (name, (fixes, case_result c ctxt));
+ val cases = dest_cases ctxt |> map_filter mk_case;
in
if null cases then []
else [Pretty.big_list "cases:" (map pretty_case cases)]
--- a/src/Pure/Isar/rule_cases.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Isar/rule_cases.ML Tue Sep 03 22:30:52 2013 +0200
@@ -21,7 +21,7 @@
include BASIC_RULE_CASES
datatype T = Case of
{fixes: (binding * typ) list,
- assumes: (string * term list) list,
+ assumes: (binding * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list}
val case_hypsN: string
@@ -62,7 +62,7 @@
datatype T = Case of
{fixes: (binding * typ) list,
- assumes: (string * term list) list,
+ assumes: (binding * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list};
@@ -91,21 +91,22 @@
| extract_fixes (SOME outline) prop =
chop (length (Logic.strip_params outline)) (strip_params prop);
-fun extract_assumes _ _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
- | extract_assumes qual hnames (SOME outline) prop =
+fun extract_assumes _ _ NONE prop = ([(Binding.empty, Logic.strip_assums_hyp prop)], [])
+ | extract_assumes qualifier hyp_names (SOME outline) prop =
let
+ val qual = Binding.qualify true qualifier o Binding.name;
val (hyps, prems) =
chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
- fun extract ((hname,h)::ps) = (qual hname, h :: map snd ps);
- val (hyps1,hyps2) = chop (length hnames) hyps;
- val pairs1 = if hyps1 = [] then [] else hnames ~~ hyps1;
- val pairs = pairs1 @ (map (pair case_hypsN) hyps2);
- val named_hyps = map extract (partition_eq (eq_fst op =) pairs)
+ fun extract ((hyp_name, hyp) :: rest) = (qual hyp_name, hyp :: map snd rest);
+ val (hyps1, hyps2) = chop (length hyp_names) hyps;
+ val pairs1 = if null hyps1 then [] else hyp_names ~~ hyps1;
+ val pairs = pairs1 @ map (pair case_hypsN) hyps2;
+ val named_hyps = map extract (partition_eq (eq_fst op =) pairs);
in (named_hyps, [(qual case_premsN, prems)]) end;
fun bindings args = map (apfst Binding.name) args;
-fun extract_case thy (case_outline, raw_prop) name hnames concls =
+fun extract_case thy (case_outline, raw_prop) name hyp_names concls =
let
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
val len = length props;
@@ -120,7 +121,8 @@
else
fold_rev Term.abs fixes1
(app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
- val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
+ val (assumes1, assumes2) =
+ extract_assumes name hyp_names case_outline prop
|> pairself (map (apsnd (maps Logic.dest_conjunctions)));
val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
@@ -153,11 +155,11 @@
let
val n = length cases;
val nprems = Logic.count_prems prop;
- fun add_case ((name, hnames), concls) (cs, i) =
+ fun add_case ((name, hyp_names), concls) (cs, i) =
((case try (fn () =>
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
NONE => (name, NONE)
- | SOME p => (name, extract_case thy p name hnames concls)) :: cs, i - 1);
+ | SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1);
in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
in
--- a/src/Pure/PIDE/command.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/PIDE/command.ML Tue Sep 03 22:30:52 2013 +0200
@@ -57,7 +57,7 @@
(case expr of
Expr (exec_id, body) =>
uninterruptible (fn restore_attributes => fn () =>
- if Execution.running execution_id exec_id then
+ if Execution.running execution_id exec_id [Future.the_worker_group ()] then
let
val res =
(body
--- a/src/Pure/PIDE/execution.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/PIDE/execution.ML Tue Sep 03 22:30:52 2013 +0200
@@ -11,7 +11,7 @@
val discontinue: unit -> unit
val is_running: Document_ID.execution -> bool
val is_running_exec: Document_ID.exec -> bool
- val running: Document_ID.execution -> Document_ID.exec -> bool
+ val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
val peek: Document_ID.exec -> Future.group list
val cancel: Document_ID.exec -> unit
val terminate: Document_ID.exec -> unit
@@ -33,7 +33,7 @@
fun make_state (execution, execs) = State {execution = execution, execs = execs};
fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
-val init_state = make_state (Document_ID.none, Inttab.empty);
+val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
val state = Synchronized.var "Execution.state" init_state;
fun get_state () = let val State args = Synchronized.value state in args end;
@@ -58,18 +58,18 @@
fun is_running_exec exec_id =
Inttab.defined (#execs (get_state ())) exec_id;
-fun running execution_id exec_id =
- Synchronized.guarded_access state
+fun running execution_id exec_id groups =
+ Synchronized.change_result state
(fn State {execution = execution_id', execs} =>
let
val continue = execution_id = execution_id';
val execs' =
if continue then
- Inttab.update_new (exec_id, [Future.the_worker_group ()]) execs
+ Inttab.update_new (exec_id, groups) execs
handle Inttab.DUP dup =>
- error ("Execution already registered: " ^ Document_ID.print dup)
+ raise Fail ("Execution already registered: " ^ Document_ID.print dup)
else execs;
- in SOME (continue, make_state (execution_id', execs')) end);
+ in (continue, make_state (execution_id', execs')) end);
fun peek exec_id =
Inttab.lookup_list (#execs (get_state ())) exec_id;
@@ -89,7 +89,10 @@
let
val exec_id = the_default 0 (Position.parse_id pos);
val group = Future.worker_subgroup ();
- val _ = change_state (apsnd (Inttab.cons_list (exec_id, group)));
+ val _ = change_state (apsnd (fn execs =>
+ if Inttab.defined execs exec_id
+ then Inttab.cons_list (exec_id, group) execs
+ else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
val future =
(singleton o Future.forks)
@@ -127,7 +130,7 @@
if Inttab.defined execs' exec_id then ()
else groups |> List.app (fn group =>
if Task_Queue.is_canceled group then ()
- else error ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
+ else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
in execs' end);
fun reset () =
--- a/src/Pure/PIDE/markup.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Tue Sep 03 22:30:52 2013 +0200
@@ -46,6 +46,7 @@
val type_nameN: string
val constantN: string
val fixedN: string val fixed: string -> T
+ val caseN: string val case_: string -> T
val dynamic_factN: string val dynamic_fact: string -> T
val tfreeN: string val tfree: T
val tvarN: string val tvar: T
@@ -288,6 +289,7 @@
val constantN = "constant";
val (fixedN, fixed) = markup_string "fixed" nameN;
+val (caseN, case_) = markup_string "case" nameN;
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
--- a/src/Pure/PIDE/markup.scala Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Sep 03 22:30:52 2013 +0200
@@ -105,8 +105,8 @@
val CLASS = "class"
val TYPE_NAME = "type_name"
val FIXED = "fixed"
+ val CASE = "case"
val CONSTANT = "constant"
-
val DYNAMIC_FACT = "dynamic_fact"
--- a/src/Pure/Pure.thy Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Pure.thy Tue Sep 03 22:30:52 2013 +0200
@@ -60,7 +60,8 @@
and "then" "from" "with" :: prf_chain % "proof"
and "note" "using" "unfolding" :: prf_decl % "proof"
and "fix" "assume" "presume" "def" :: prf_asm % "proof"
- and "obtain" "guess" :: prf_asm_goal % "proof"
+ and "obtain" :: prf_asm_goal % "proof"
+ and "guess" :: prf_asm_goal_script % "proof"
and "let" "write" :: prf_decl % "proof"
and "case" :: prf_asm % "proof"
and "{" :: prf_open % "proof"
--- a/src/Pure/Thy/thy_info.ML Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Sep 03 22:30:52 2013 +0200
@@ -165,18 +165,20 @@
(* scheduling loader tasks *)
datatype result =
- Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int};
+ Result of {theory: theory, exec_id: Document_ID.exec,
+ present: unit -> unit, commit: unit -> unit, weight: int};
-fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0};
+fun theory_result theory =
+ Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
fun result_theory (Result {theory, ...}) = theory;
fun result_present (Result {present, ...}) = present;
fun result_commit (Result {commit, ...}) = commit;
fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
-fun join_theory (Result {theory, id, ...}) =
+fun join_theory (Result {theory, exec_id, ...}) =
Exn.capture Thm.join_theory_proofs theory ::
- map Exn.Exn (maps Task_Queue.group_status (Execution.peek id));
+ map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id));
datatype task =
@@ -271,13 +273,19 @@
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
- val id = serial ();
- val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
+ val exec_id = Document_ID.make ();
+ val _ =
+ Execution.running Document_ID.none exec_id [] orelse
+ raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
+
+ val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
val (theory, present, weight) =
Thy_Load.load_thy last_timing update_time dir header text_pos text
(if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
fun commit () = update_thy deps theory;
- in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end;
+ in
+ Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
+ end;
fun check_deps dir name =
(case lookup_deps name of
--- a/src/Pure/Tools/keywords.scala Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Pure/Tools/keywords.scala Tue Sep 03 22:30:52 2013 +0200
@@ -38,6 +38,7 @@
"prf_decl" -> "proof-decl",
"prf_asm" -> "proof-asm",
"prf_asm_goal" -> "proof-asm-goal",
+ "prf_asm_goal_script" -> "proof-asm-goal",
"prf_script" -> "proof-script"
).withDefault((s: String) => s)
--- a/src/Tools/jEdit/src/rendering.scala Tue Sep 03 22:12:48 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Tue Sep 03 22:30:52 2013 +0200
@@ -77,7 +77,8 @@
Keyword.THY_SCRIPT -> LABEL,
Keyword.PRF_SCRIPT -> DIGIT,
Keyword.PRF_ASM -> KEYWORD3,
- Keyword.PRF_ASM_GOAL -> KEYWORD3
+ Keyword.PRF_ASM_GOAL -> KEYWORD3,
+ Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT
).withDefaultValue(KEYWORD1)
}