--- a/src/HOL/IMP/Sec_TypingT.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/IMP/Sec_TypingT.thy Fri Jul 22 08:02:37 2016 +0200
@@ -107,9 +107,9 @@
have "s = s' (\<le> l)" by auto
moreover
from termi_if_non0[OF 1 0, of t] obtain t' where
- "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
+ t': "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
moreover
- from confinement[OF this 1] `\<not> sec b \<le> l`
+ from confinement[OF t' 1] `\<not> sec b \<le> l`
have "t = t' (\<le> l)" by auto
ultimately
show ?case using `s = t (\<le> l)` by auto
@@ -134,9 +134,9 @@
have "s = s' (\<le> l)" by auto
moreover
from termi_if_non0[OF 1 0, of t] obtain t' where
- "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
+ t': "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
moreover
- from confinement[OF this 1] `\<not> sec b \<le> l`
+ from confinement[OF t' 1] `\<not> sec b \<le> l`
have "t = t' (\<le> l)" by auto
ultimately
show ?case using `s = t (\<le> l)` by auto
--- a/src/HOL/Int.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Int.thy Fri Jul 22 08:02:37 2016 +0200
@@ -633,13 +633,13 @@
case equal with assms(1) show P by simp
next
case greater
- then have "nat k > 0" by simp
- moreover from this have "k = int (nat k)" by auto
+ then have *: "nat k > 0" by simp
+ moreover from * have "k = int (nat k)" by auto
ultimately show P using assms(2) by blast
next
case less
- then have "nat (- k) > 0" by simp
- moreover from this have "k = - int (nat (- k))" by auto
+ then have *: "nat (- k) > 0" by simp
+ moreover from * have "k = - int (nat (- k))" by auto
ultimately show P using assms(3) by blast
qed
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jul 22 08:02:37 2016 +0200
@@ -1217,8 +1217,8 @@
using zero_neq_one by (intro exI)
show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y"
proof transfer
- fix x y :: ereal assume "0 \<le> x" "x < y"
- moreover from dense[OF this(2)] guess z ..
+ fix x y :: ereal assume "0 \<le> x" and *: "x < y"
+ moreover from dense[OF *] guess z ..
ultimately show "\<exists>z\<in>Collect (op \<le> 0). x < z \<and> z < y"
by (intro bexI[of _ z]) auto
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Jul 22 08:02:37 2016 +0200
@@ -1512,7 +1512,7 @@
assume "Lcm A \<noteq> 0"
from unbounded obtain f where f: "f \<in> A" "subdegree (Lcm A) < subdegree f"
unfolding bdd_above_def by (auto simp: not_le)
- moreover from this and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
+ moreover from f and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
by (intro dvd_imp_subdegree_le dvd_Lcm) simp_all
ultimately show False by simp
qed
--- a/src/HOL/Library/Multiset.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Jul 22 08:02:37 2016 +0200
@@ -2493,9 +2493,9 @@
obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K"
"a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
proof -
- from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K"
- "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
- moreover from this(3) [of a] have "a \<notin># K" by auto
+ from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K" and
+ *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
+ moreover from * [of a] have "a \<notin># K" by auto
ultimately show thesis by (auto intro: that)
qed
--- a/src/HOL/Library/Perm.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Library/Perm.thy Fri Jul 22 08:02:37 2016 +0200
@@ -593,9 +593,9 @@
define m where "m = order f a - n mod order f a - 1"
moreover have "order f a - n mod order f a > 0"
by simp
- ultimately have "order f a - n mod order f a = Suc m"
+ ultimately have *: "order f a - n mod order f a = Suc m"
by arith
- moreover from this have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)"
+ moreover from * have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)"
by (auto simp add: mod_Suc)
ultimately show ?case
using Suc
--- a/src/HOL/Library/Permutations.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Library/Permutations.thy Fri Jul 22 08:02:37 2016 +0200
@@ -1269,9 +1269,9 @@
where x'y': "map_of xs x = Some x'" "map_of xs y = Some y'"
by (cases "map_of xs x"; cases "map_of xs y")
(simp_all add: map_of_eq_None_iff)
- moreover from this x'y' have "(x,x') \<in> set xs" "(y,y') \<in> set xs"
+ moreover from x'y' have *: "(x,x') \<in> set xs" "(y,y') \<in> set xs"
by (force dest: map_of_SomeD)+
- moreover from this eq x'y' have "x' = y'" by simp
+ moreover from * eq x'y' have "x' = y'" by simp
ultimately show "x = y" using assms
by (force simp: distinct_map dest: inj_onD[of _ _ "(x,x')" "(y,y')"])
qed
--- a/src/HOL/Library/Polynomial_FPS.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Fri Jul 22 08:02:37 2016 +0200
@@ -125,10 +125,10 @@
from assms have "\<not>monom 1 (Suc n) dvd p"
by (auto simp: monom_1_dvd_iff simp del: power_Suc)
- then obtain k where "k \<le> n" "fps_of_poly p $ k \<noteq> 0"
+ then obtain k where k: "k \<le> n" "fps_of_poly p $ k \<noteq> 0"
by (auto simp: monom_1_dvd_iff' less_Suc_eq_le)
- moreover from this and zero[of k] have "k = n" by linarith
- ultimately show "fps_of_poly p $ n \<noteq> 0" by simp
+ with zero[of k] have "k = n" by linarith
+ with k show "fps_of_poly p $ n \<noteq> 0" by simp
qed
lemma fps_of_poly_dvd:
--- a/src/HOL/Multivariate_Analysis/Gamma.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Fri Jul 22 08:02:37 2016 +0200
@@ -1470,10 +1470,10 @@
finally show "(rGamma x) = 0 \<longleftrightarrow> (\<exists>n. x = - real_of_nat n)" by simp
next
fix x :: real assume "\<And>n. x \<noteq> - of_nat n"
- hence "complex_of_real x \<notin> \<int>\<^sub>\<le>\<^sub>0"
+ hence x: "complex_of_real x \<notin> \<int>\<^sub>\<le>\<^sub>0"
by (subst of_real_in_nonpos_Ints_iff) (auto elim!: nonpos_Ints_cases')
- moreover from this have "x \<noteq> 0" by auto
- ultimately have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)"
+ then have "x \<noteq> 0" by auto
+ with x have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)"
by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
simp: Polygamma_of_real rGamma_real_def [abs_def])
thus "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (x + of_nat k))
@@ -2248,8 +2248,8 @@
hence "(g has_field_derivative 0) (at z)" for z using g_g'[of z] by simp
hence "\<exists>c'. \<forall>z\<in>UNIV. g z = c'" by (intro has_field_derivative_zero_constant) simp_all
then obtain c' where c: "\<And>z. g z = c'" by (force simp: dist_0_norm)
- moreover from this[of 0] have "c' = pi" unfolding g_def by simp
- ultimately have "g z = pi" by simp
+ from this[of 0] have "c' = pi" unfolding g_def by simp
+ with c have "g z = pi" by simp
show ?thesis
proof (cases "z \<in> \<int>")
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Fri Jul 22 08:02:37 2016 +0200
@@ -582,9 +582,9 @@
from prime_factorization_exists'[OF assms(1)] guess A . note A = this
moreover from A and assms have "A \<noteq> {#}" by auto
then obtain x where "x \<in># A" by blast
- with A(1) have "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
- moreover from this A have "x dvd a" by simp
- ultimately show ?thesis by blast
+ with A(1) have *: "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
+ with A have "x dvd a" by simp
+ with * show ?thesis by blast
qed
lemma prime_divisors_induct [case_names zero unit factor]:
--- a/src/HOL/Number_Theory/Polynomial_Factorial.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Number_Theory/Polynomial_Factorial.thy Fri Jul 22 08:02:37 2016 +0200
@@ -1207,7 +1207,7 @@
shows "irreducible [:a,b:]"
proof (rule irreducibleI)
fix p q assume pq: "[:a,b:] = p * q"
- also from this assms have "degree \<dots> = degree p + degree q"
+ also from pq assms have "degree \<dots> = degree p + degree q"
by (intro degree_mult_eq) auto
finally have "degree p = 0 \<or> degree q = 0" using assms by auto
with assms pq show "is_unit p \<or> is_unit q"
--- a/src/HOL/Probability/Embed_Measure.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy Fri Jul 22 08:02:37 2016 +0200
@@ -33,10 +33,10 @@
finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .
next
fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"
- then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
+ then obtain A' where A': "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
by (auto simp: subset_eq choice_iff)
- moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
- ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}"
+ then have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
+ with A' show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}"
by simp blast
qed (auto dest: sets.sets_into_space)
@@ -81,7 +81,7 @@
proof-
{
fix A assume A: "A \<in> sets M"
- also from this have "A = A \<inter> space M" by auto
+ also from A have "A = A \<inter> space M" by auto
also have "... = f -` f ` A \<inter> space M" using A assms
by (auto dest: inj_onD sets.sets_into_space)
finally have "f -` f ` A \<inter> space M \<in> sets M" .
--- a/src/HOL/Probability/PMF_Impl.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy Fri Jul 22 08:02:37 2016 +0200
@@ -402,9 +402,9 @@
(\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
proof -
from assms have wf: "pmf_of_list_wf xs" by (intro pmf_of_list_wfI) force
- moreover from this assms have "set_pmf (pmf_of_list xs) = fst ` set xs"
+ with assms have "set_pmf (pmf_of_list xs) = fst ` set xs"
by (intro set_pmf_of_list_eq) auto
- ultimately show ?thesis
+ with wf show ?thesis
by (intro mapping_of_pmfI) (auto simp: lookup_tabulate pmf_pmf_of_list)
qed
--- a/src/HOL/Probability/Random_Permutations.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy Fri Jul 22 08:02:37 2016 +0200
@@ -52,9 +52,9 @@
by (force, simp_all)
termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)")
fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a
- assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
- moreover from this have "card A > 0" by (simp add: card_gt_0_iff)
- ultimately show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)"
+ assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
+ then have "card A > 0" by (simp add: card_gt_0_iff)
+ with A show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)"
by simp
qed simp_all
@@ -128,9 +128,9 @@
termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)")
fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b
and y :: 'a and g :: "'b \<Rightarrow> 'c pmf"
- assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
- moreover from this have "card A > 0" by (simp add: card_gt_0_iff)
- ultimately show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)"
+ assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
+ then have "card A > 0" by (simp add: card_gt_0_iff)
+ with A show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)"
by simp
qed simp_all