summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/List_Set.thy

changeset 32880 | b8bee63c7202 |

parent 31851 | c04f8c51d0ab |

child 33939 | fcb50b497763 |

--- a/src/HOL/Library/List_Set.thy Mon Oct 05 17:28:59 2009 +0100 +++ b/src/HOL/Library/List_Set.thy Tue Oct 06 15:59:12 2009 +0200 @@ -65,10 +65,18 @@ "Set.insert x (set xs) = set (insert x xs)" by (auto simp add: insert_def) +lemma insert_set_compl: + "Set.insert x (- set xs) = - set (List_Set.remove_all x xs)" + by (auto simp del: mem_def simp add: remove_all_def) + lemma remove_set: "remove x (set xs) = set (remove_all x xs)" by (auto simp add: remove_def remove_all_def) +lemma remove_set_compl: + "List_Set.remove x (- set xs) = - set (List_Set.insert x xs)" + by (auto simp del: mem_def simp add: remove_def List_Set.insert_def) + lemma image_set: "image f (set xs) = set (map f xs)" by simp @@ -98,14 +106,12 @@ qed lemma Inter_set: - "Inter (set (A # As)) = foldl (op \<inter>) A As" + "Inter (set As) = foldl (op \<inter>) UNIV As" proof - - have "finite (set (A # As))" by simp - moreover have "fold (op \<inter>) UNIV (set (A # As)) = foldl (\<lambda>y x. x \<inter> y) UNIV (A # As)" + have "fold (op \<inter>) UNIV (set As) = foldl (\<lambda>y x. x \<inter> y) UNIV As" by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - ultimately have "Inter (set (A # As)) = foldl (op \<inter>) UNIV (A # As)" - by (simp only: Inter_fold_inter Int_commute) - then show ?thesis by simp + then show ?thesis + by (simp only: Inter_fold_inter finite_set Int_commute) qed lemma Union_set: @@ -118,14 +124,12 @@ qed lemma INTER_set: - "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) (f A) As" + "INTER (set As) f = foldl (\<lambda>B A. f A \<inter> B) UNIV As" proof - - have "finite (set (A # As))" by simp - moreover have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set (A # As)) = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)" + have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set As) = foldl (\<lambda>B A. f A \<inter> B) UNIV As" by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - ultimately have "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)" - by (simp only: INTER_fold_inter) - then show ?thesis by simp + then show ?thesis + by (simp only: INTER_fold_inter finite_set) qed lemma UNION_set: