tuned proofs;
authorwenzelm
Sun Sep 11 00:14:44 2016 +0200 (2016-09-11)
changeset 638346a757f36997e
parent 63833 4aaeb9427c96
child 63835 4f8c6e63bc41
tuned proofs;
src/HOL/BNF_Def.thy
src/HOL/Divides.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/BNF_Def.thy	Sun Sep 11 00:14:37 2016 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Sun Sep 11 00:14:44 2016 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4    by (simp add: the_inv_f_f)
     1.5  
     1.6  lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
     1.7 -  unfolding vimage2p_def by -
     1.8 +  unfolding vimage2p_def .
     1.9  
    1.10  lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
    1.11    unfolding rel_fun_def vimage2p_def by auto
     2.1 --- a/src/HOL/Divides.thy	Sun Sep 11 00:14:37 2016 +0200
     2.2 +++ b/src/HOL/Divides.thy	Sun Sep 11 00:14:44 2016 +0200
     2.3 @@ -1793,13 +1793,14 @@
     2.4      by (rule div_int_unique)
     2.5  next
     2.6    fix a b c :: int
     2.7 -  assume "c \<noteq> 0"
     2.8 -  hence "\<And>q r. divmod_int_rel a b (q, r)
     2.9 +  assume c: "c \<noteq> 0"
    2.10 +  have "\<And>q r. divmod_int_rel a b (q, r)
    2.11      \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
    2.12      unfolding divmod_int_rel_def
    2.13 -    by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
    2.14 +    by (rule linorder_cases [of 0 b])
    2.15 +      (use c in \<open>auto simp: algebra_simps
    2.16        mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
    2.17 -      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
    2.18 +      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
    2.19    hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
    2.20      using divmod_int_rel [of a b] .
    2.21    thus "(c * a) div (c * b) = a div b"
     3.1 --- a/src/HOL/List.thy	Sun Sep 11 00:14:37 2016 +0200
     3.2 +++ b/src/HOL/List.thy	Sun Sep 11 00:14:44 2016 +0200
     3.3 @@ -4661,8 +4661,7 @@
     3.4    from Suc have "k < card A" by simp
     3.5    moreover have "finite A" using assms by (simp add: card_ge_0_finite)
     3.6    moreover have "finite {xs. ?k_list k xs}"
     3.7 -    using finite_lists_length_eq[OF \<open>finite A\<close>, of k]
     3.8 -    by - (rule finite_subset, auto)
     3.9 +    by (rule finite_subset) (use finite_lists_length_eq[OF \<open>finite A\<close>, of k] in auto)
    3.10    moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
    3.11      by auto
    3.12    moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
     4.1 --- a/src/HOL/Map.thy	Sun Sep 11 00:14:37 2016 +0200
     4.2 +++ b/src/HOL/Map.thy	Sun Sep 11 00:14:44 2016 +0200
     4.3 @@ -695,17 +695,23 @@
     4.4  by (metis map_add_subsumed1 map_le_iff_map_add_commute)
     4.5  
     4.6  lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
     4.7 -proof(rule iffI)
     4.8 -  assume "\<exists>v. f = [x \<mapsto> v]"
     4.9 -  thus "dom f = {x}" by(auto split: if_split_asm)
    4.10 +  (is "?lhs \<longleftrightarrow> ?rhs")
    4.11 +proof
    4.12 +  assume ?rhs
    4.13 +  then show ?lhs by (auto split: if_split_asm)
    4.14  next
    4.15 -  assume "dom f = {x}"
    4.16 -  then obtain v where "f x = Some v" by auto
    4.17 -  hence "[x \<mapsto> v] \<subseteq>\<^sub>m f" by(auto simp add: map_le_def)
    4.18 -  moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using \<open>dom f = {x}\<close> \<open>f x = Some v\<close>
    4.19 -    by(auto simp add: map_le_def)
    4.20 -  ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym)
    4.21 -  thus "\<exists>v. f = [x \<mapsto> v]" by blast
    4.22 +  assume ?lhs
    4.23 +  then obtain v where v: "f x = Some v" by auto
    4.24 +  show ?rhs
    4.25 +  proof
    4.26 +    show "f = [x \<mapsto> v]"
    4.27 +    proof (rule map_le_antisym)
    4.28 +      show "[x \<mapsto> v] \<subseteq>\<^sub>m f"
    4.29 +        using v by (auto simp add: map_le_def)
    4.30 +      show "f \<subseteq>\<^sub>m [x \<mapsto> v]"
    4.31 +        using \<open>dom f = {x}\<close> \<open>f x = Some v\<close> by (auto simp add: map_le_def)
    4.32 +    qed
    4.33 +  qed
    4.34  qed
    4.35  
    4.36  
     5.1 --- a/src/HOL/Transcendental.thy	Sun Sep 11 00:14:37 2016 +0200
     5.2 +++ b/src/HOL/Transcendental.thy	Sun Sep 11 00:14:44 2016 +0200
     5.3 @@ -205,7 +205,7 @@
     5.4    also have "card {0<..<2*n} \<le> 2*n - 1" by (cases n) simp_all
     5.5    also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)"
     5.6      using assms by (simp add: algebra_simps)
     5.7 -  finally have "4 ^ n \<le> (2 * n choose n) * (2 * n)" by - simp_all
     5.8 +  finally have "4 ^ n \<le> (2 * n choose n) * (2 * n)" by simp_all
     5.9    hence "real (4 ^ n) \<le> real ((2 * n choose n) * (2 * n))"
    5.10      by (subst of_nat_le_iff)
    5.11    with assms show ?thesis by (simp add: field_simps)