equal
deleted
inserted
replaced
5675 by (simp_all add: Pow_insert Let_def) |
5675 by (simp_all add: Pow_insert Let_def) |
5676 |
5676 |
5677 text {* Further operations on sets *} |
5677 text {* Further operations on sets *} |
5678 |
5678 |
5679 (* Minimal refinement of equality on sets *) |
5679 (* Minimal refinement of equality on sets *) |
5680 lemma [code]: |
5680 declare subset_eq[code del] |
5681 "HOL.equal (set []) (List.coset []) = False" |
5681 lemma subset_code [code]: |
5682 by (metis UNIV_coset UNIV_not_empty empty_set equal_eq) |
5682 "set xs <= B \<longleftrightarrow> (ALL x : set xs. x : B)" |
|
5683 "List.coset xs <= List.coset ys \<longleftrightarrow> set ys <= set xs" |
|
5684 "List.coset [] <= set [] \<longleftrightarrow> False" |
|
5685 by auto |
5683 |
5686 |
5684 lemma setsum_code [code]: |
5687 lemma setsum_code [code]: |
5685 "setsum f (set xs) = listsum (map f (remdups xs))" |
5688 "setsum f (set xs) = listsum (map f (remdups xs))" |
5686 by (simp add: listsum_distinct_conv_setsum_set) |
5689 by (simp add: listsum_distinct_conv_setsum_set) |
5687 |
5690 |