src/HOL/List.thy
changeset 46147 2c4d8de91c4c
parent 46143 c932c80d3eae
child 46149 54ca5b2775a8
     1.1 --- a/src/HOL/List.thy	Fri Jan 06 21:48:45 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Jan 06 22:16:01 2012 +0100
     1.3 @@ -2470,6 +2470,23 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma union_set_fold:
     1.8 +  "set xs \<union> A = fold Set.insert xs A"
     1.9 +proof -
    1.10 +  interpret comp_fun_idem Set.insert
    1.11 +    by (fact comp_fun_idem_insert)
    1.12 +  show ?thesis by (simp add: union_fold_insert fold_set_fold)
    1.13 +qed
    1.14 +
    1.15 +lemma minus_set_fold:
    1.16 +  "A - set xs = fold Set.remove xs A"
    1.17 +proof -
    1.18 +  interpret comp_fun_idem Set.remove
    1.19 +    by (fact comp_fun_idem_remove)
    1.20 +  show ?thesis
    1.21 +    by (simp add: minus_fold_remove [of _ A] fold_set_fold)
    1.22 +qed
    1.23 +
    1.24  lemma (in lattice) Inf_fin_set_fold:
    1.25    "Inf_fin (set (x # xs)) = fold inf xs x"
    1.26  proof -
    1.27 @@ -2588,6 +2605,22 @@
    1.28    "concat xss = foldr append xss []"
    1.29    by (simp add: fold_append_concat_rev foldr_def)
    1.30  
    1.31 +lemma union_set_foldr:
    1.32 +  "set xs \<union> A = foldr Set.insert xs A"
    1.33 +proof -
    1.34 +  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
    1.35 +    by auto
    1.36 +  then show ?thesis by (simp add: union_set_fold foldr_fold)
    1.37 +qed
    1.38 +
    1.39 +lemma minus_set_foldr:
    1.40 +  "A - set xs = foldr Set.remove xs A"
    1.41 +proof -
    1.42 +  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
    1.43 +    by (auto simp add: remove_def)
    1.44 +  then show ?thesis by (simp add: minus_set_fold foldr_fold)
    1.45 +qed
    1.46 +
    1.47  lemma (in lattice) Inf_fin_set_foldr [code]:
    1.48    "Inf_fin (set (x # xs)) = foldr inf xs x"
    1.49    by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
    1.50 @@ -5166,7 +5199,7 @@
    1.51  subsubsection {* Counterparts for set-related operations *}
    1.52  
    1.53  definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    1.54 -  [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
    1.55 +  "member xs x \<longleftrightarrow> x \<in> set xs"
    1.56  
    1.57  text {*
    1.58    Use @{text member} only for generating executable code.  Otherwise use
    1.59 @@ -5182,16 +5215,11 @@
    1.60    "x \<in> set xs \<longleftrightarrow> member xs x"
    1.61    by (simp add: member_def)
    1.62  
    1.63 -declare INF_def [code_unfold]
    1.64 -declare SUP_def [code_unfold]
    1.65 -
    1.66 -declare set_map [symmetric, code_unfold]
    1.67 -
    1.68  definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.69 -  list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    1.70 +  list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    1.71  
    1.72  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.73 -  list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    1.74 +  list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    1.75  
    1.76  definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.77    list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
    1.78 @@ -5497,4 +5525,75 @@
    1.79  code_const list_ex
    1.80    (Haskell "any")
    1.81  
    1.82 +
    1.83 +subsubsection {* Implementation of sets by lists *}
    1.84 +
    1.85 +text {* Basic operations *}
    1.86 +
    1.87 +lemma is_empty_set [code]:
    1.88 +  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
    1.89 +  by (simp add: Set.is_empty_def null_def)
    1.90 +
    1.91 +lemma empty_set [code]:
    1.92 +  "{} = set []"
    1.93 +  by simp
    1.94 +
    1.95 +lemma [code]:
    1.96 +  "x \<in> set xs \<longleftrightarrow> List.member xs x"
    1.97 +  "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
    1.98 +  by (simp_all add: member_def)
    1.99 +
   1.100 +lemma UNIV_coset [code]:
   1.101 +  "UNIV = List.coset []"
   1.102 +  by simp
   1.103 +
   1.104 +lemma insert_code [code]:
   1.105 +  "insert x (set xs) = set (List.insert x xs)"
   1.106 +  "insert x (List.coset xs) = List.coset (removeAll x xs)"
   1.107 +  by simp_all
   1.108 +
   1.109 +lemma remove_code [code]:
   1.110 +  "Set.remove x (set xs) = set (removeAll x xs)"
   1.111 +  "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
   1.112 +  by (simp_all add: remove_def Compl_insert)
   1.113 +
   1.114 +lemma Ball_set [code]:
   1.115 +  "Ball (set xs) P \<longleftrightarrow> list_all P xs"
   1.116 +  by (simp add: list_all_iff)
   1.117 +
   1.118 +lemma Bex_set [code]:
   1.119 +  "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
   1.120 +  by (simp add: list_ex_iff)
   1.121 +
   1.122 +lemma card_set [code]:
   1.123 +  "card (set xs) = length (remdups xs)"
   1.124 +proof -
   1.125 +  have "card (set (remdups xs)) = length (remdups xs)"
   1.126 +    by (rule distinct_card) simp
   1.127 +  then show ?thesis by simp
   1.128 +qed
   1.129 +
   1.130 +
   1.131 +text {* Operations on relations *}
   1.132 +
   1.133 +lemma product_code [code]:
   1.134 +  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
   1.135 +  by (auto simp add: Product_Type.product_def)
   1.136 +
   1.137 +lemma Id_on_set [code]:
   1.138 +  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
   1.139 +  by (auto simp add: Id_on_def)
   1.140 +
   1.141 +lemma trancl_set_ntrancl [code]:
   1.142 +  "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
   1.143 +  by (simp add: finite_trancl_ntranl)
   1.144 +
   1.145 +lemma set_rel_comp [code]:
   1.146 +  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
   1.147 +  by (auto simp add: Bex_def)
   1.148 +
   1.149 +lemma wf_set [code]:
   1.150 +  "wf (set xs) = acyclic (set xs)"
   1.151 +  by (simp add: wf_iff_acyclic_if_finite)
   1.152 +
   1.153  end