Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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:
isabelle