# HG changeset patch
# User wenzelm
# Date 1469167357 -7200
# Node ID 70d4d9e5707b23d4d20c91aa63ff153e6e0deda8
# Parent  42b6186fc0e41a247fbece5b9359a13ca4994c29
tuned proofs -- avoid improper use of "this";

diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/IMP/Sec_TypingT.thy
--- 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
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Int.thy
--- 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
 
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Library/Extended_Nonnegative_Real.thy
--- 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
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Library/Formal_Power_Series.thy
--- 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
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Library/Multiset.thy
--- 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
 
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Library/Perm.thy
--- 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
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Library/Permutations.thy
--- 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
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Library/Polynomial_FPS.thy
--- 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:
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Multivariate_Analysis/Gamma.thy
--- 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>")
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Number_Theory/Factorial_Ring.thy
--- 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]:
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Number_Theory/Polynomial_Factorial.thy
--- 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"
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Probability/Embed_Measure.thy
--- 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" .
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Probability/PMF_Impl.thy
--- 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
 
diff -r 42b6186fc0e4 -r 70d4d9e5707b src/HOL/Probability/Random_Permutations.thy
--- 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