author | wenzelm |

Fri Jul 22 08:02:37 2016 +0200 (2016-07-22) | |

changeset 63539 | 70d4d9e5707b |

parent 63533 | 42b6186fc0e4 |

child 63540 | f8652d0534fa |

tuned proofs -- avoid improper use of "this";

1.1 --- a/src/HOL/IMP/Sec_TypingT.thy Thu Jul 21 10:52:27 2016 +0200 1.2 +++ b/src/HOL/IMP/Sec_TypingT.thy Fri Jul 22 08:02:37 2016 +0200 1.3 @@ -107,9 +107,9 @@ 1.4 have "s = s' (\<le> l)" by auto 1.5 moreover 1.6 from termi_if_non0[OF 1 0, of t] obtain t' where 1.7 - "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. 1.8 + t': "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. 1.9 moreover 1.10 - from confinement[OF this 1] `\<not> sec b \<le> l` 1.11 + from confinement[OF t' 1] `\<not> sec b \<le> l` 1.12 have "t = t' (\<le> l)" by auto 1.13 ultimately 1.14 show ?case using `s = t (\<le> l)` by auto 1.15 @@ -134,9 +134,9 @@ 1.16 have "s = s' (\<le> l)" by auto 1.17 moreover 1.18 from termi_if_non0[OF 1 0, of t] obtain t' where 1.19 - "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. 1.20 + t': "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. 1.21 moreover 1.22 - from confinement[OF this 1] `\<not> sec b \<le> l` 1.23 + from confinement[OF t' 1] `\<not> sec b \<le> l` 1.24 have "t = t' (\<le> l)" by auto 1.25 ultimately 1.26 show ?case using `s = t (\<le> l)` by auto

2.1 --- a/src/HOL/Int.thy Thu Jul 21 10:52:27 2016 +0200 2.2 +++ b/src/HOL/Int.thy Fri Jul 22 08:02:37 2016 +0200 2.3 @@ -633,13 +633,13 @@ 2.4 case equal with assms(1) show P by simp 2.5 next 2.6 case greater 2.7 - then have "nat k > 0" by simp 2.8 - moreover from this have "k = int (nat k)" by auto 2.9 + then have *: "nat k > 0" by simp 2.10 + moreover from * have "k = int (nat k)" by auto 2.11 ultimately show P using assms(2) by blast 2.12 next 2.13 case less 2.14 - then have "nat (- k) > 0" by simp 2.15 - moreover from this have "k = - int (nat (- k))" by auto 2.16 + then have *: "nat (- k) > 0" by simp 2.17 + moreover from * have "k = - int (nat (- k))" by auto 2.18 ultimately show P using assms(3) by blast 2.19 qed 2.20

3.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 21 10:52:27 2016 +0200 3.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jul 22 08:02:37 2016 +0200 3.3 @@ -1217,8 +1217,8 @@ 3.4 using zero_neq_one by (intro exI) 3.5 show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y" 3.6 proof transfer 3.7 - fix x y :: ereal assume "0 \<le> x" "x < y" 3.8 - moreover from dense[OF this(2)] guess z .. 3.9 + fix x y :: ereal assume "0 \<le> x" and *: "x < y" 3.10 + moreover from dense[OF *] guess z .. 3.11 ultimately show "\<exists>z\<in>Collect (op \<le> 0). x < z \<and> z < y" 3.12 by (intro bexI[of _ z]) auto 3.13 qed

4.1 --- a/src/HOL/Library/Formal_Power_Series.thy Thu Jul 21 10:52:27 2016 +0200 4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri Jul 22 08:02:37 2016 +0200 4.3 @@ -1512,7 +1512,7 @@ 4.4 assume "Lcm A \<noteq> 0" 4.5 from unbounded obtain f where f: "f \<in> A" "subdegree (Lcm A) < subdegree f" 4.6 unfolding bdd_above_def by (auto simp: not_le) 4.7 - moreover from this and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)" 4.8 + moreover from f and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)" 4.9 by (intro dvd_imp_subdegree_le dvd_Lcm) simp_all 4.10 ultimately show False by simp 4.11 qed

5.1 --- a/src/HOL/Library/Multiset.thy Thu Jul 21 10:52:27 2016 +0200 5.2 +++ b/src/HOL/Library/Multiset.thy Fri Jul 22 08:02:37 2016 +0200 5.3 @@ -2493,9 +2493,9 @@ 5.4 obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K" 5.5 "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a" 5.6 proof - 5.7 - from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K" 5.8 - "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E) 5.9 - moreover from this(3) [of a] have "a \<notin># K" by auto 5.10 + from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K" and 5.11 + *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E) 5.12 + moreover from * [of a] have "a \<notin># K" by auto 5.13 ultimately show thesis by (auto intro: that) 5.14 qed 5.15

6.1 --- a/src/HOL/Library/Perm.thy Thu Jul 21 10:52:27 2016 +0200 6.2 +++ b/src/HOL/Library/Perm.thy Fri Jul 22 08:02:37 2016 +0200 6.3 @@ -593,9 +593,9 @@ 6.4 define m where "m = order f a - n mod order f a - 1" 6.5 moreover have "order f a - n mod order f a > 0" 6.6 by simp 6.7 - ultimately have "order f a - n mod order f a = Suc m" 6.8 + ultimately have *: "order f a - n mod order f a = Suc m" 6.9 by arith 6.10 - moreover from this have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)" 6.11 + moreover from * have m2: "order f a - Suc n mod order f a = (if m = 0 then order f a else m)" 6.12 by (auto simp add: mod_Suc) 6.13 ultimately show ?case 6.14 using Suc

7.1 --- a/src/HOL/Library/Permutations.thy Thu Jul 21 10:52:27 2016 +0200 7.2 +++ b/src/HOL/Library/Permutations.thy Fri Jul 22 08:02:37 2016 +0200 7.3 @@ -1269,9 +1269,9 @@ 7.4 where x'y': "map_of xs x = Some x'" "map_of xs y = Some y'" 7.5 by (cases "map_of xs x"; cases "map_of xs y") 7.6 (simp_all add: map_of_eq_None_iff) 7.7 - moreover from this x'y' have "(x,x') \<in> set xs" "(y,y') \<in> set xs" 7.8 + moreover from x'y' have *: "(x,x') \<in> set xs" "(y,y') \<in> set xs" 7.9 by (force dest: map_of_SomeD)+ 7.10 - moreover from this eq x'y' have "x' = y'" by simp 7.11 + moreover from * eq x'y' have "x' = y'" by simp 7.12 ultimately show "x = y" using assms 7.13 by (force simp: distinct_map dest: inj_onD[of _ _ "(x,x')" "(y,y')"]) 7.14 qed

8.1 --- a/src/HOL/Library/Polynomial_FPS.thy Thu Jul 21 10:52:27 2016 +0200 8.2 +++ b/src/HOL/Library/Polynomial_FPS.thy Fri Jul 22 08:02:37 2016 +0200 8.3 @@ -125,10 +125,10 @@ 8.4 8.5 from assms have "\<not>monom 1 (Suc n) dvd p" 8.6 by (auto simp: monom_1_dvd_iff simp del: power_Suc) 8.7 - then obtain k where "k \<le> n" "fps_of_poly p $ k \<noteq> 0" 8.8 + then obtain k where k: "k \<le> n" "fps_of_poly p $ k \<noteq> 0" 8.9 by (auto simp: monom_1_dvd_iff' less_Suc_eq_le) 8.10 - moreover from this and zero[of k] have "k = n" by linarith 8.11 - ultimately show "fps_of_poly p $ n \<noteq> 0" by simp 8.12 + with zero[of k] have "k = n" by linarith 8.13 + with k show "fps_of_poly p $ n \<noteq> 0" by simp 8.14 qed 8.15 8.16 lemma fps_of_poly_dvd:

9.1 --- a/src/HOL/Multivariate_Analysis/Gamma.thy Thu Jul 21 10:52:27 2016 +0200 9.2 +++ b/src/HOL/Multivariate_Analysis/Gamma.thy Fri Jul 22 08:02:37 2016 +0200 9.3 @@ -1470,10 +1470,10 @@ 9.4 finally show "(rGamma x) = 0 \<longleftrightarrow> (\<exists>n. x = - real_of_nat n)" by simp 9.5 next 9.6 fix x :: real assume "\<And>n. x \<noteq> - of_nat n" 9.7 - hence "complex_of_real x \<notin> \<int>\<^sub>\<le>\<^sub>0" 9.8 + hence x: "complex_of_real x \<notin> \<int>\<^sub>\<le>\<^sub>0" 9.9 by (subst of_real_in_nonpos_Ints_iff) (auto elim!: nonpos_Ints_cases') 9.10 - moreover from this have "x \<noteq> 0" by auto 9.11 - ultimately have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)" 9.12 + then have "x \<noteq> 0" by auto 9.13 + with x have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)" 9.14 by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex 9.15 simp: Polygamma_of_real rGamma_real_def [abs_def]) 9.16 thus "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (x + of_nat k)) 9.17 @@ -2248,8 +2248,8 @@ 9.18 hence "(g has_field_derivative 0) (at z)" for z using g_g'[of z] by simp 9.19 hence "\<exists>c'. \<forall>z\<in>UNIV. g z = c'" by (intro has_field_derivative_zero_constant) simp_all 9.20 then obtain c' where c: "\<And>z. g z = c'" by (force simp: dist_0_norm) 9.21 - moreover from this[of 0] have "c' = pi" unfolding g_def by simp 9.22 - ultimately have "g z = pi" by simp 9.23 + from this[of 0] have "c' = pi" unfolding g_def by simp 9.24 + with c have "g z = pi" by simp 9.25 9.26 show ?thesis 9.27 proof (cases "z \<in> \<int>")

10.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy Thu Jul 21 10:52:27 2016 +0200 10.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy Fri Jul 22 08:02:37 2016 +0200 10.3 @@ -582,9 +582,9 @@ 10.4 from prime_factorization_exists'[OF assms(1)] guess A . note A = this 10.5 moreover from A and assms have "A \<noteq> {#}" by auto 10.6 then obtain x where "x \<in># A" by blast 10.7 - with A(1) have "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod) 10.8 - moreover from this A have "x dvd a" by simp 10.9 - ultimately show ?thesis by blast 10.10 + with A(1) have *: "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod) 10.11 + with A have "x dvd a" by simp 10.12 + with * show ?thesis by blast 10.13 qed 10.14 10.15 lemma prime_divisors_induct [case_names zero unit factor]:

11.1 --- a/src/HOL/Number_Theory/Polynomial_Factorial.thy Thu Jul 21 10:52:27 2016 +0200 11.2 +++ b/src/HOL/Number_Theory/Polynomial_Factorial.thy Fri Jul 22 08:02:37 2016 +0200 11.3 @@ -1207,7 +1207,7 @@ 11.4 shows "irreducible [:a,b:]" 11.5 proof (rule irreducibleI) 11.6 fix p q assume pq: "[:a,b:] = p * q" 11.7 - also from this assms have "degree \<dots> = degree p + degree q" 11.8 + also from pq assms have "degree \<dots> = degree p + degree q" 11.9 by (intro degree_mult_eq) auto 11.10 finally have "degree p = 0 \<or> degree q = 0" using assms by auto 11.11 with assms pq show "is_unit p \<or> is_unit q"

12.1 --- a/src/HOL/Probability/Embed_Measure.thy Thu Jul 21 10:52:27 2016 +0200 12.2 +++ b/src/HOL/Probability/Embed_Measure.thy Fri Jul 22 08:02:37 2016 +0200 12.3 @@ -33,10 +33,10 @@ 12.4 finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" . 12.5 next 12.6 fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}" 12.7 - then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M" 12.8 + then obtain A' where A': "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M" 12.9 by (auto simp: subset_eq choice_iff) 12.10 - moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast 12.11 - ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" 12.12 + then have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast 12.13 + with A' show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" 12.14 by simp blast 12.15 qed (auto dest: sets.sets_into_space) 12.16 12.17 @@ -81,7 +81,7 @@ 12.18 proof- 12.19 { 12.20 fix A assume A: "A \<in> sets M" 12.21 - also from this have "A = A \<inter> space M" by auto 12.22 + also from A have "A = A \<inter> space M" by auto 12.23 also have "... = f -` f ` A \<inter> space M" using A assms 12.24 by (auto dest: inj_onD sets.sets_into_space) 12.25 finally have "f -` f ` A \<inter> space M \<in> sets M" .

13.1 --- a/src/HOL/Probability/PMF_Impl.thy Thu Jul 21 10:52:27 2016 +0200 13.2 +++ b/src/HOL/Probability/PMF_Impl.thy Fri Jul 22 08:02:37 2016 +0200 13.3 @@ -402,9 +402,9 @@ 13.4 (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))" 13.5 proof - 13.6 from assms have wf: "pmf_of_list_wf xs" by (intro pmf_of_list_wfI) force 13.7 - moreover from this assms have "set_pmf (pmf_of_list xs) = fst ` set xs" 13.8 + with assms have "set_pmf (pmf_of_list xs) = fst ` set xs" 13.9 by (intro set_pmf_of_list_eq) auto 13.10 - ultimately show ?thesis 13.11 + with wf show ?thesis 13.12 by (intro mapping_of_pmfI) (auto simp: lookup_tabulate pmf_pmf_of_list) 13.13 qed 13.14

14.1 --- a/src/HOL/Probability/Random_Permutations.thy Thu Jul 21 10:52:27 2016 +0200 14.2 +++ b/src/HOL/Probability/Random_Permutations.thy Fri Jul 22 08:02:37 2016 +0200 14.3 @@ -52,9 +52,9 @@ 14.4 by (force, simp_all) 14.5 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)") 14.6 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a 14.7 - assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" 14.8 - moreover from this have "card A > 0" by (simp add: card_gt_0_iff) 14.9 - ultimately show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" 14.10 + assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" 14.11 + then have "card A > 0" by (simp add: card_gt_0_iff) 14.12 + with A show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)" 14.13 by simp 14.14 qed simp_all 14.15 14.16 @@ -128,9 +128,9 @@ 14.17 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)") 14.18 fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b 14.19 and y :: 'a and g :: "'b \<Rightarrow> 'c pmf" 14.20 - assume "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" 14.21 - moreover from this have "card A > 0" by (simp add: card_gt_0_iff) 14.22 - ultimately show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)" 14.23 + assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)" 14.24 + then have "card A > 0" by (simp add: card_gt_0_iff) 14.25 + with A show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)" 14.26 by simp 14.27 qed simp_all 14.28