equal
deleted
inserted
replaced
2165 fixes M::"('a::fs multiset)" |
2165 fixes M::"('a::fs multiset)" |
2166 shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" |
2166 shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" |
2167 proof - |
2167 proof - |
2168 have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp |
2168 have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp |
2169 also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto |
2169 also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto |
2170 also have "... = supp (set_of M)" by (simp add: supp_of_finite_sets) |
2170 also have "... = supp (set_of M)" |
|
2171 by (simp add: supp_of_finite_sets) |
2171 also have " ... \<subseteq> supp M" by (rule supp_set_of) |
2172 also have " ... \<subseteq> supp M" by (rule supp_set_of) |
2172 finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" . |
2173 finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" . |
2173 qed |
2174 qed |
2174 |
2175 |
2175 lemma supp_of_multisets: |
2176 lemma supp_of_multisets: |
2951 |
2952 |
2952 |
2953 |
2953 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2954 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2954 case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) => |
2955 case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) => |
2955 let |
2956 let |
2956 |
|
2957 fun first_is_neg lhs rhs [] = NONE |
2957 fun first_is_neg lhs rhs [] = NONE |
2958 | first_is_neg lhs rhs (thm::thms) = |
2958 | first_is_neg lhs rhs (thm::thms) = |
2959 (case Thm.prop_of thm of |
2959 (case Thm.prop_of thm of |
2960 _ $ (@{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ l $ r)) => |
2960 _ $ (@{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ l $ r)) => |
2961 (if l = lhs andalso r = rhs then SOME(thm) |
2961 (if l = lhs andalso r = rhs then SOME(thm) |
2974 end) |
2974 end) |
2975 | _ => false) |
2975 | _ => false) |
2976 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |
2976 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |
2977 |> map HOLogic.conj_elims |
2977 |> map HOLogic.conj_elims |
2978 |> flat |
2978 |> flat |
2979 |
|
2980 |
|
2981 in |
2979 in |
2982 case first_is_neg lhs rhs prems of |
2980 case first_is_neg lhs rhs prems of |
2983 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
2981 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
2984 | NONE => NONE |
2982 | NONE => NONE |
2985 end |
2983 end |