summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 22 Jul 2016 08:02:37 +0200 | |

changeset 63539 | 70d4d9e5707b |

parent 63533 | 42b6186fc0e4 |

child 63540 | f8652d0534fa |

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

--- 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