src/HOL/List.thy
changeset 46156 f58b7f9d3920
parent 46151 913ea585efdc
child 46176 1898e61e89c4
     1.1 --- a/src/HOL/List.thy	Sat Jan 07 20:18:56 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Jan 07 20:44:23 2012 +0100
     1.3 @@ -2605,7 +2605,19 @@
     1.4    "concat xss = foldr append xss []"
     1.5    by (simp add: fold_append_concat_rev foldr_def)
     1.6  
     1.7 -lemma union_set_foldr:
     1.8 +lemma minus_set_foldr [code]:
     1.9 +  "A - set xs = foldr Set.remove xs A"
    1.10 +proof -
    1.11 +  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
    1.12 +    by (auto simp add: remove_def)
    1.13 +  then show ?thesis by (simp add: minus_set_fold foldr_fold)
    1.14 +qed
    1.15 +
    1.16 +lemma subtract_coset_filter [code]:
    1.17 +  "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
    1.18 +  by auto
    1.19 +
    1.20 +lemma union_set_foldr [code]:
    1.21    "set xs \<union> A = foldr Set.insert xs A"
    1.22  proof -
    1.23    have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
    1.24 @@ -2613,13 +2625,17 @@
    1.25    then show ?thesis by (simp add: union_set_fold foldr_fold)
    1.26  qed
    1.27  
    1.28 -lemma minus_set_foldr:
    1.29 -  "A - set xs = foldr Set.remove xs A"
    1.30 -proof -
    1.31 -  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
    1.32 -    by (auto simp add: remove_def)
    1.33 -  then show ?thesis by (simp add: minus_set_fold foldr_fold)
    1.34 -qed
    1.35 +lemma union_coset_foldr [code]:
    1.36 +  "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
    1.37 +  by auto
    1.38 +
    1.39 +lemma inter_set_filer [code]:
    1.40 +  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
    1.41 +  by auto
    1.42 +
    1.43 +lemma inter_coset_foldr [code]:
    1.44 +  "A \<inter> List.coset xs = foldr Set.remove xs A"
    1.45 +  by (simp add: Diff_eq [symmetric] minus_set_foldr)
    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 @@ -2645,6 +2661,9 @@
    1.50    "Sup (set xs) = foldr sup xs bot"
    1.51    by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
    1.52  
    1.53 +declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
    1.54 +declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
    1.55 +
    1.56  lemma (in complete_lattice) INF_set_foldr [code]:
    1.57    "INFI (set xs) f = foldr (inf \<circ> f) xs top"
    1.58    by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
    1.59 @@ -2653,6 +2672,29 @@
    1.60    "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
    1.61    by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
    1.62  
    1.63 +(* FIXME: better implement conversion by bisection *)
    1.64 +
    1.65 +lemma pred_of_set_fold_sup:
    1.66 +  assumes "finite A"
    1.67 +  shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
    1.68 +proof (rule sym)
    1.69 +  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
    1.70 +    by (fact comp_fun_idem_sup)
    1.71 +  from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
    1.72 +qed
    1.73 +
    1.74 +lemma pred_of_set_set_fold_sup:
    1.75 +  "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
    1.76 +proof -
    1.77 +  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
    1.78 +    by (fact comp_fun_idem_sup)
    1.79 +  show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
    1.80 +qed
    1.81 +
    1.82 +lemma pred_of_set_set_foldr_sup [code]:
    1.83 +  "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
    1.84 +  by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
    1.85 +
    1.86  
    1.87  subsubsection {* @{text upt} *}
    1.88  
    1.89 @@ -5538,15 +5580,23 @@
    1.90    "{} = set []"
    1.91    by simp
    1.92  
    1.93 +lemma UNIV_coset [code]:
    1.94 +  "UNIV = List.coset []"
    1.95 +  by simp
    1.96 +
    1.97 +lemma compl_set [code]:
    1.98 +  "- set xs = List.coset xs"
    1.99 +  by simp
   1.100 +
   1.101 +lemma compl_coset [code]:
   1.102 +  "- List.coset xs = set xs"
   1.103 +  by simp
   1.104 +
   1.105  lemma [code]:
   1.106    "x \<in> set xs \<longleftrightarrow> List.member xs x"
   1.107    "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
   1.108    by (simp_all add: member_def)
   1.109  
   1.110 -lemma UNIV_coset [code]:
   1.111 -  "UNIV = List.coset []"
   1.112 -  by simp
   1.113 -
   1.114  lemma insert_code [code]:
   1.115    "insert x (set xs) = set (List.insert x xs)"
   1.116    "insert x (List.coset xs) = List.coset (removeAll x xs)"
   1.117 @@ -5557,6 +5607,14 @@
   1.118    "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
   1.119    by (simp_all add: remove_def Compl_insert)
   1.120  
   1.121 +lemma project_set [code]:
   1.122 +  "Set.project P (set xs) = set (filter P xs)"
   1.123 +  by auto
   1.124 +
   1.125 +lemma image_set [code]:
   1.126 +  "image f (set xs) = set (map f xs)"
   1.127 +  by simp
   1.128 +
   1.129  lemma Ball_set [code]:
   1.130    "Ball (set xs) P \<longleftrightarrow> list_all P xs"
   1.131    by (simp add: list_all_iff)
   1.132 @@ -5573,6 +5631,15 @@
   1.133    then show ?thesis by simp
   1.134  qed
   1.135  
   1.136 +lemma the_elem_set [code]:
   1.137 +  "the_elem (set [x]) = x"
   1.138 +  by simp
   1.139 +
   1.140 +lemma Pow_set [code]:
   1.141 +  "Pow (set []) = {{}}"
   1.142 +  "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
   1.143 +  by (simp_all add: Pow_insert Let_def)
   1.144 +
   1.145  
   1.146  text {* Operations on relations *}
   1.147