massaging of code setup for sets
authorhaftmann
Sat Jan 07 20:44:23 2012 +0100 (2012-01-07)
changeset 46156f58b7f9d3920
parent 46155 f27cf421500a
child 46157 3d518b508bbb
massaging of code setup for sets
src/HOL/List.thy
src/HOL/Set.thy
     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  
     2.1 --- a/src/HOL/Set.thy	Sat Jan 07 20:18:56 2012 +0100
     2.2 +++ b/src/HOL/Set.thy	Sat Jan 07 20:44:23 2012 +0100
     2.3 @@ -431,10 +431,6 @@
     2.4  lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
     2.5    by blast
     2.6  
     2.7 -lemma member_exists [code]:
     2.8 -  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
     2.9 -  by (rule sym) (fact bex_triv_one_point2)
    2.10 -
    2.11  lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
    2.12    by blast
    2.13  
    2.14 @@ -1837,10 +1833,6 @@
    2.15    "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
    2.16    by (simp add: project_def)
    2.17  
    2.18 -lemma inter_project [code]:
    2.19 -  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
    2.20 -  by (auto simp add: project_def)
    2.21 -
    2.22  instantiation set :: (equal) equal
    2.23  begin
    2.24