tuned proofs -- avoid improper use of "this";
authorwenzelm
Fri Jul 22 08:02:37 2016 +0200 (2016-07-22)
changeset 6353970d4d9e5707b
parent 63533 42b6186fc0e4
child 63540 f8652d0534fa
tuned proofs -- avoid improper use of "this";
src/HOL/IMP/Sec_TypingT.thy
src/HOL/Int.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Perm.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Polynomial_FPS.thy
src/HOL/Multivariate_Analysis/Gamma.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Polynomial_Factorial.thy
src/HOL/Probability/Embed_Measure.thy
src/HOL/Probability/PMF_Impl.thy
src/HOL/Probability/Random_Permutations.thy
     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