moved lemmas about List.set and set operations to List theory
authorhaftmann
Fri Jan 06 22:16:01 2012 +0100 (2012-01-06)
changeset 461472c4d8de91c4c
parent 46146 6baea4fca6bd
child 46148 04a8da7dcffc
moved lemmas about List.set and set operations to List theory
src/HOL/Library/List_Cset.thy
src/HOL/List.thy
src/HOL/More_Set.thy
     1.1 --- a/src/HOL/Library/List_Cset.thy	Fri Jan 06 21:48:45 2012 +0100
     1.2 +++ b/src/HOL/Library/List_Cset.thy	Fri Jan 06 22:16:01 2012 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    
     1.5  lemma filter_set [code]:
     1.6    "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
     1.7 -  by (simp add: Cset.set_def project_set)
     1.8 +  by (simp add: Cset.set_def)
     1.9  
    1.10  lemma forall_set [code]:
    1.11    "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
     2.1 --- a/src/HOL/List.thy	Fri Jan 06 21:48:45 2012 +0100
     2.2 +++ b/src/HOL/List.thy	Fri Jan 06 22:16:01 2012 +0100
     2.3 @@ -2470,6 +2470,23 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +lemma union_set_fold:
     2.8 +  "set xs \<union> A = fold Set.insert xs A"
     2.9 +proof -
    2.10 +  interpret comp_fun_idem Set.insert
    2.11 +    by (fact comp_fun_idem_insert)
    2.12 +  show ?thesis by (simp add: union_fold_insert fold_set_fold)
    2.13 +qed
    2.14 +
    2.15 +lemma minus_set_fold:
    2.16 +  "A - set xs = fold Set.remove xs A"
    2.17 +proof -
    2.18 +  interpret comp_fun_idem Set.remove
    2.19 +    by (fact comp_fun_idem_remove)
    2.20 +  show ?thesis
    2.21 +    by (simp add: minus_fold_remove [of _ A] fold_set_fold)
    2.22 +qed
    2.23 +
    2.24  lemma (in lattice) Inf_fin_set_fold:
    2.25    "Inf_fin (set (x # xs)) = fold inf xs x"
    2.26  proof -
    2.27 @@ -2588,6 +2605,22 @@
    2.28    "concat xss = foldr append xss []"
    2.29    by (simp add: fold_append_concat_rev foldr_def)
    2.30  
    2.31 +lemma union_set_foldr:
    2.32 +  "set xs \<union> A = foldr Set.insert xs A"
    2.33 +proof -
    2.34 +  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
    2.35 +    by auto
    2.36 +  then show ?thesis by (simp add: union_set_fold foldr_fold)
    2.37 +qed
    2.38 +
    2.39 +lemma minus_set_foldr:
    2.40 +  "A - set xs = foldr Set.remove xs A"
    2.41 +proof -
    2.42 +  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
    2.43 +    by (auto simp add: remove_def)
    2.44 +  then show ?thesis by (simp add: minus_set_fold foldr_fold)
    2.45 +qed
    2.46 +
    2.47  lemma (in lattice) Inf_fin_set_foldr [code]:
    2.48    "Inf_fin (set (x # xs)) = foldr inf xs x"
    2.49    by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
    2.50 @@ -5166,7 +5199,7 @@
    2.51  subsubsection {* Counterparts for set-related operations *}
    2.52  
    2.53  definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    2.54 -  [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
    2.55 +  "member xs x \<longleftrightarrow> x \<in> set xs"
    2.56  
    2.57  text {*
    2.58    Use @{text member} only for generating executable code.  Otherwise use
    2.59 @@ -5182,16 +5215,11 @@
    2.60    "x \<in> set xs \<longleftrightarrow> member xs x"
    2.61    by (simp add: member_def)
    2.62  
    2.63 -declare INF_def [code_unfold]
    2.64 -declare SUP_def [code_unfold]
    2.65 -
    2.66 -declare set_map [symmetric, code_unfold]
    2.67 -
    2.68  definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    2.69 -  list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    2.70 +  list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    2.71  
    2.72  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    2.73 -  list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    2.74 +  list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    2.75  
    2.76  definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    2.77    list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
    2.78 @@ -5497,4 +5525,75 @@
    2.79  code_const list_ex
    2.80    (Haskell "any")
    2.81  
    2.82 +
    2.83 +subsubsection {* Implementation of sets by lists *}
    2.84 +
    2.85 +text {* Basic operations *}
    2.86 +
    2.87 +lemma is_empty_set [code]:
    2.88 +  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
    2.89 +  by (simp add: Set.is_empty_def null_def)
    2.90 +
    2.91 +lemma empty_set [code]:
    2.92 +  "{} = set []"
    2.93 +  by simp
    2.94 +
    2.95 +lemma [code]:
    2.96 +  "x \<in> set xs \<longleftrightarrow> List.member xs x"
    2.97 +  "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
    2.98 +  by (simp_all add: member_def)
    2.99 +
   2.100 +lemma UNIV_coset [code]:
   2.101 +  "UNIV = List.coset []"
   2.102 +  by simp
   2.103 +
   2.104 +lemma insert_code [code]:
   2.105 +  "insert x (set xs) = set (List.insert x xs)"
   2.106 +  "insert x (List.coset xs) = List.coset (removeAll x xs)"
   2.107 +  by simp_all
   2.108 +
   2.109 +lemma remove_code [code]:
   2.110 +  "Set.remove x (set xs) = set (removeAll x xs)"
   2.111 +  "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
   2.112 +  by (simp_all add: remove_def Compl_insert)
   2.113 +
   2.114 +lemma Ball_set [code]:
   2.115 +  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
   2.116 +  by (simp add: list_all_iff)
   2.117 +
   2.118 +lemma Bex_set [code]:
   2.119 +  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
   2.120 +  by (simp add: list_ex_iff)
   2.121 +
   2.122 +lemma card_set [code]:
   2.123 +  "card (set xs) = length (remdups xs)"
   2.124 +proof -
   2.125 +  have "card (set (remdups xs)) = length (remdups xs)"
   2.126 +    by (rule distinct_card) simp
   2.127 +  then show ?thesis by simp
   2.128 +qed
   2.129 +
   2.130 +
   2.131 +text {* Operations on relations *}
   2.132 +
   2.133 +lemma product_code [code]:
   2.134 +  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
   2.135 +  by (auto simp add: Product_Type.product_def)
   2.136 +
   2.137 +lemma Id_on_set [code]:
   2.138 +  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
   2.139 +  by (auto simp add: Id_on_def)
   2.140 +
   2.141 +lemma trancl_set_ntrancl [code]:
   2.142 +  "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
   2.143 +  by (simp add: finite_trancl_ntranl)
   2.144 +
   2.145 +lemma set_rel_comp [code]:
   2.146 +  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
   2.147 +  by (auto simp add: Bex_def)
   2.148 +
   2.149 +lemma wf_set [code]:
   2.150 +  "wf (set xs) = acyclic (set xs)"
   2.151 +  by (simp add: wf_iff_acyclic_if_finite)
   2.152 +
   2.153  end
     3.1 --- a/src/HOL/More_Set.thy	Fri Jan 06 21:48:45 2012 +0100
     3.2 +++ b/src/HOL/More_Set.thy	Fri Jan 06 22:16:01 2012 +0100
     3.3 @@ -7,91 +7,6 @@
     3.4  imports List
     3.5  begin
     3.6  
     3.7 -subsection {* Basic set operations *}
     3.8 -
     3.9 -lemma is_empty_set [code]:
    3.10 -  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
    3.11 -  by (simp add: Set.is_empty_def null_def)
    3.12 -
    3.13 -lemma empty_set [code]:
    3.14 -  "{} = set []"
    3.15 -  by simp
    3.16 -
    3.17 -
    3.18 -subsection {* Functorial set operations *}
    3.19 -
    3.20 -lemma union_set_fold:
    3.21 -  "set xs \<union> A = fold Set.insert xs A"
    3.22 -proof -
    3.23 -  interpret comp_fun_idem Set.insert
    3.24 -    by (fact comp_fun_idem_insert)
    3.25 -  show ?thesis by (simp add: union_fold_insert fold_set_fold)
    3.26 -qed
    3.27 -
    3.28 -lemma union_set_foldr:
    3.29 -  "set xs \<union> A = foldr Set.insert xs A"
    3.30 -proof -
    3.31 -  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
    3.32 -    by auto
    3.33 -  then show ?thesis by (simp add: union_set_fold foldr_fold)
    3.34 -qed
    3.35 -
    3.36 -lemma minus_set_fold:
    3.37 -  "A - set xs = fold Set.remove xs A"
    3.38 -proof -
    3.39 -  interpret comp_fun_idem Set.remove
    3.40 -    by (fact comp_fun_idem_remove)
    3.41 -  show ?thesis
    3.42 -    by (simp add: minus_fold_remove [of _ A] fold_set_fold)
    3.43 -qed
    3.44 -
    3.45 -lemma minus_set_foldr:
    3.46 -  "A - set xs = foldr Set.remove xs A"
    3.47 -proof -
    3.48 -  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
    3.49 -    by (auto simp add: remove_def)
    3.50 -  then show ?thesis by (simp add: minus_set_fold foldr_fold)
    3.51 -qed
    3.52 -
    3.53 -
    3.54 -subsection {* Basic operations *}
    3.55 -
    3.56 -lemma [code]:
    3.57 -  "x \<in> set xs \<longleftrightarrow> List.member xs x"
    3.58 -  "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
    3.59 -  by (simp_all add: member_def)
    3.60 -
    3.61 -lemma UNIV_coset [code]:
    3.62 -  "UNIV = List.coset []"
    3.63 -  by simp
    3.64 -
    3.65 -lemma insert_code [code]:
    3.66 -  "insert x (set xs) = set (List.insert x xs)"
    3.67 -  "insert x (List.coset xs) = List.coset (removeAll x xs)"
    3.68 -  by simp_all
    3.69 -
    3.70 -lemma remove_code [code]:
    3.71 -  "Set.remove x (set xs) = set (removeAll x xs)"
    3.72 -  "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
    3.73 -  by (simp_all add: remove_def Compl_insert)
    3.74 -
    3.75 -lemma Ball_set [code]:
    3.76 -  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
    3.77 -  by (simp add: list_all_iff)
    3.78 -
    3.79 -lemma Bex_set [code]:
    3.80 -  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
    3.81 -  by (simp add: list_ex_iff)
    3.82 -
    3.83 -lemma card_set [code]:
    3.84 -  "card (set xs) = length (remdups xs)"
    3.85 -proof -
    3.86 -  have "card (set (remdups xs)) = length (remdups xs)"
    3.87 -    by (rule distinct_card) simp
    3.88 -  then show ?thesis by simp
    3.89 -qed
    3.90 -
    3.91 -
    3.92  subsection {* Functorial operations *}
    3.93  
    3.94  lemma inter_code [code]:
    3.95 @@ -152,28 +67,5 @@
    3.96    "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
    3.97    by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
    3.98  
    3.99 -
   3.100 -subsection {* Operations on relations *}
   3.101 -
   3.102 -lemma product_code [code]:
   3.103 -  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
   3.104 -  by (auto simp add: Product_Type.product_def)
   3.105 -
   3.106 -lemma Id_on_set [code]:
   3.107 -  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
   3.108 -  by (auto simp add: Id_on_def)
   3.109 -
   3.110 -lemma trancl_set_ntrancl [code]:
   3.111 -  "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
   3.112 -  by (simp add: finite_trancl_ntranl)
   3.113 -
   3.114 -lemma set_rel_comp [code]:
   3.115 -  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
   3.116 -  by (auto simp add: Bex_def)
   3.117 -
   3.118 -lemma wf_set [code]:
   3.119 -  "wf (set xs) = acyclic (set xs)"
   3.120 -  by (simp add: wf_iff_acyclic_if_finite)
   3.121 -
   3.122  end
   3.123