src/HOL/Library/Multiset.thy
changeset 60752 b48830b670a1
parent 60678 17ba2df56dee
child 60804 080a979a985b
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Jul 18 20:37:16 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Jul 18 20:47:08 2015 +0200
     1.3 @@ -1898,23 +1898,25 @@
     1.4              Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
     1.5                    mk_mset T [x] $ mk_mset T xs
     1.6  
     1.7 -    fun mset_member_tac m i =
     1.8 +    fun mset_member_tac ctxt m i =
     1.9        if m <= 0 then
    1.10 -        rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i
    1.11 +        resolve_tac ctxt @{thms multi_member_this} i ORELSE
    1.12 +        resolve_tac ctxt @{thms multi_member_last} i
    1.13        else
    1.14 -        rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i
    1.15 -
    1.16 -    val mset_nonempty_tac =
    1.17 -      rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
    1.18 +        resolve_tac ctxt @{thms multi_member_skip} i THEN mset_member_tac ctxt (m - 1) i
    1.19 +
    1.20 +    fun mset_nonempty_tac ctxt =
    1.21 +      resolve_tac ctxt @{thms nonempty_plus} ORELSE'
    1.22 +      resolve_tac ctxt @{thms nonempty_single}
    1.23  
    1.24      fun regroup_munion_conv ctxt =
    1.25        Function_Lib.regroup_conv ctxt @{const_abbrev Mempty} @{const_name plus}
    1.26          (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
    1.27  
    1.28 -    fun unfold_pwleq_tac i =
    1.29 -      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
    1.30 -        ORELSE (rtac @{thm pw_leq_lstep} i)
    1.31 -        ORELSE (rtac @{thm pw_leq_empty} i)
    1.32 +    fun unfold_pwleq_tac ctxt i =
    1.33 +      (resolve_tac ctxt @{thms pw_leq_step} i THEN (fn st => unfold_pwleq_tac ctxt (i + 1) st))
    1.34 +        ORELSE (resolve_tac ctxt @{thms pw_leq_lstep} i)
    1.35 +        ORELSE (resolve_tac ctxt @{thms pw_leq_empty} i)
    1.36  
    1.37      val set_mset_simps = [@{thm set_mset_empty}, @{thm set_mset_single}, @{thm set_mset_union},
    1.38                          @{thm Un_insert_left}, @{thm Un_empty_left}]
    1.39 @@ -1925,7 +1927,7 @@
    1.40        mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
    1.41        mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_mset_simps,
    1.42        smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
    1.43 -      reduction_pair= @{thm ms_reduction_pair}
    1.44 +      reduction_pair = @{thm ms_reduction_pair}
    1.45      })
    1.46    end
    1.47  \<close>