src/HOL/Library/Multiset.thy
changeset 57492 74bf65a1910a
parent 57418 6ab1c7cb0b8d
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Jul 02 17:34:45 2014 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 11 14:24:23 2014 +1000
     1.3 @@ -1653,7 +1653,7 @@
     1.4   apply (simp (no_asm))
     1.5   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
     1.6   apply (simp (no_asm_simp) add: add_assoc [symmetric])
     1.7 - apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
     1.8 + apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
     1.9   apply (simp add: diff_union_single_conv)
    1.10   apply (simp (no_asm_use) add: trans_def)
    1.11   apply blast
    1.12 @@ -1664,7 +1664,7 @@
    1.13   apply (rule conjI)
    1.14    apply (simp add: multiset_eq_iff split: nat_diff_split)
    1.15   apply (rule conjI)
    1.16 -  apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
    1.17 +  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
    1.18    apply (simp add: multiset_eq_iff split: nat_diff_split)
    1.19   apply (simp (no_asm_use) add: trans_def)
    1.20   apply blast
    1.21 @@ -2760,7 +2760,9 @@
    1.22            using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
    1.23          also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
    1.24            apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
    1.25 -          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
    1.26 +          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1]
    1.27 +            [[hypsubst_thin = true]]
    1.28 +          by fastforce
    1.29          finally show ?thesis .
    1.30        qed
    1.31        thus "count (mmap p1 M) b1 = count N1 b1" by transfer
    1.32 @@ -2796,7 +2798,9 @@
    1.33          also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
    1.34          also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
    1.35            apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
    1.36 -          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
    1.37 +          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def
    1.38 +            [[hypsubst_thin = true]]
    1.39 +          by fastforce
    1.40          finally show ?thesis .
    1.41        qed
    1.42        thus "count (mmap p2 M) b2 = count N2 b2" by transfer