tuned proofs;
authorwenzelm
Thu Feb 16 22:53:24 2012 +0100 (2012-02-16)
changeset 465071b24c24017dd
parent 46506 c7faa011bfa7
child 46508 ec9630fe9ca7
tuned proofs;
src/HOL/Library/AList.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/DAList.thy
     1.1 --- a/src/HOL/Library/AList.thy	Thu Feb 16 22:18:28 2012 +0100
     1.2 +++ b/src/HOL/Library/AList.thy	Thu Feb 16 22:53:24 2012 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  lemma updates_twist [simp]:
     1.5   "k \<notin> set ks \<Longrightarrow> 
     1.6    map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
     1.7 -  by (simp add: updates_conv' update_conv' map_upds_twist)
     1.8 +  by (simp add: updates_conv' update_conv')
     1.9  
    1.10  lemma updates_apply_notin[simp]:
    1.11   "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
     2.1 --- a/src/HOL/Library/Binomial.thy	Thu Feb 16 22:18:28 2012 +0100
     2.2 +++ b/src/HOL/Library/Binomial.thy	Thu Feb 16 22:53:24 2012 +0100
     2.3 @@ -68,8 +68,7 @@
     2.4    need to reason about division.*}
     2.5  lemma binomial_Suc_Suc_eq_times:
     2.6      "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
     2.7 -  by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
     2.8 -    del: mult_Suc mult_Suc_right)
     2.9 +  by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)
    2.10  
    2.11  text{*Another version, with -1 instead of Suc.*}
    2.12  lemma times_binomial_minus1_eq:
    2.13 @@ -255,7 +254,7 @@
    2.14  proof-
    2.15    from kn obtain h where h: "k = Suc h" by (cases k, auto)
    2.16    {assume n0: "n=0" then have ?thesis using kn 
    2.17 -      by (cases k, simp_all add: pochhammer_rec del: pochhammer_Suc)}
    2.18 +      by (cases k) (simp_all add: pochhammer_rec)}
    2.19    moreover
    2.20    {assume n0: "n \<noteq> 0"
    2.21      then have ?thesis apply (simp add: h pochhammer_Suc_setprod)
    2.22 @@ -311,7 +310,7 @@
    2.23        using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
    2.24        by auto
    2.25      have ?thesis
    2.26 -      unfolding h h pochhammer_Suc_setprod eq setprod_timesf[symmetric]
    2.27 +      unfolding h pochhammer_Suc_setprod eq setprod_timesf[symmetric]
    2.28        apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
    2.29        apply (auto simp add: inj_on_def image_def h )
    2.30        apply (rule_tac x="h - x" in bexI)
     3.1 --- a/src/HOL/Library/DAList.thy	Thu Feb 16 22:18:28 2012 +0100
     3.2 +++ b/src/HOL/Library/DAList.thy	Thu Feb 16 22:53:24 2012 +0100
     3.3 @@ -12,8 +12,10 @@
     3.4  subsection {* Type @{text "('key, 'value) alist" } *}
     3.5  
     3.6  typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
     3.7 -morphisms impl_of Alist
     3.8 -by(rule exI[where x="[]"]) simp
     3.9 +  morphisms impl_of Alist
    3.10 +proof
    3.11 +  show "[] \<in> {xs. distinct (map fst xs)}" by simp
    3.12 +qed
    3.13  
    3.14  lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
    3.15  by(simp add: impl_of_inject)