adapted to changes in Cset.thy
authorhaftmann
Fri Aug 26 23:02:00 2011 +0200 (2011-08-26)
changeset 44556c0fd385a41f4
parent 44555 da75ffe3d988
child 44557 9ab8c88449a4
adapted to changes in Cset.thy
src/HOL/Library/List_Cset.thy
     1.1 --- a/src/HOL/Library/List_Cset.thy	Fri Aug 26 21:11:23 2011 +0200
     1.2 +++ b/src/HOL/Library/List_Cset.thy	Fri Aug 26 23:02:00 2011 +0200
     1.3 @@ -14,9 +14,13 @@
     1.4    "coset xs = Set (- set xs)"
     1.5  hide_const (open) coset
     1.6  
     1.7 +lemma set_of_coset [simp]:
     1.8 +  "set_of (List_Cset.coset xs) = - set xs"
     1.9 +  by (simp add: coset_def)
    1.10 +
    1.11  lemma member_coset [simp]:
    1.12 -  "member (List_Cset.coset xs) = - set xs"
    1.13 -  by (simp add: coset_def)
    1.14 +  "member (List_Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
    1.15 +  by (simp add: coset_def fun_eq_iff)
    1.16  hide_fact (open) member_coset
    1.17  
    1.18  code_datatype Cset.set List_Cset.coset
    1.19 @@ -24,18 +28,7 @@
    1.20  lemma member_code [code]:
    1.21    "member (Cset.set xs) = List.member xs"
    1.22    "member (List_Cset.coset xs) = Not \<circ> List.member xs"
    1.23 -  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    1.24 -
    1.25 -lemma member_image_UNIV [simp]:
    1.26 -  "member ` UNIV = UNIV"
    1.27 -proof -
    1.28 -  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
    1.29 -  proof
    1.30 -    fix A :: "'a set"
    1.31 -    show "A = member (Set A)" by simp
    1.32 -  qed
    1.33 -  then show ?thesis by (simp add: image_def)
    1.34 -qed
    1.35 +  by (simp_all add: fun_eq_iff member_def fun_Compl_def member_set)
    1.36  
    1.37  definition (in term_syntax)
    1.38    setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    1.39 @@ -124,12 +117,12 @@
    1.40  lemma Infimum_inf [code]:
    1.41    "Infimum (Cset.set As) = foldr inf As top"
    1.42    "Infimum (List_Cset.coset []) = bot"
    1.43 -  by (simp_all add: Inf_set_foldr Inf_UNIV)
    1.44 +  by (simp_all add: Inf_set_foldr)
    1.45  
    1.46  lemma Supremum_sup [code]:
    1.47    "Supremum (Cset.set As) = foldr sup As bot"
    1.48    "Supremum (List_Cset.coset []) = top"
    1.49 -  by (simp_all add: Sup_set_foldr Sup_UNIV)
    1.50 +  by (simp_all add: Sup_set_foldr)
    1.51  
    1.52  end
    1.53  
    1.54 @@ -140,29 +133,26 @@
    1.55  hide_fact (open) single_set
    1.56  
    1.57  lemma bind_set [code]:
    1.58 -  "Cset.bind (Cset.set xs) f = foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs"
    1.59 -proof(rule sym)
    1.60 -  show "foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f"
    1.61 -    by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def)
    1.62 -qed
    1.63 -hide_fact (open) bind_set
    1.64 +  "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
    1.65 +  by (simp add: Cset.bind_def SUPR_set_fold)
    1.66  
    1.67  lemma pred_of_cset_set [code]:
    1.68    "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
    1.69  proof -
    1.70    have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
    1.71 -    by(auto simp add: Cset.pred_of_cset_def mem_def)
    1.72 +    by (simp add: Cset.pred_of_cset_def member_code member_set)
    1.73    moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
    1.74 -    by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
    1.75 -  ultimately show ?thesis by(simp)
    1.76 +    by (induct xs) (auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
    1.77 +  ultimately show ?thesis by simp
    1.78  qed
    1.79  hide_fact (open) pred_of_cset_set
    1.80  
    1.81 +
    1.82  subsection {* Derived operations *}
    1.83  
    1.84  lemma subset_eq_forall [code]:
    1.85    "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
    1.86 -  by (simp add: subset_eq)
    1.87 +  by (simp add: subset_eq member_def)
    1.88  
    1.89  lemma subset_subset_eq [code]:
    1.90    "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
    1.91 @@ -175,7 +165,7 @@
    1.92    "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
    1.93  
    1.94  instance proof
    1.95 -qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
    1.96 +qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff fun_eq_iff member_def)
    1.97  
    1.98  end
    1.99  
   1.100 @@ -186,14 +176,18 @@
   1.101  
   1.102  subsection {* Functorial operations *}
   1.103  
   1.104 +lemma member_cset_of:
   1.105 +  "member = set_of"
   1.106 +  by (rule ext)+ (simp add: member_def)
   1.107 +
   1.108  lemma inter_project [code]:
   1.109    "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
   1.110    "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
   1.111  proof -
   1.112    show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   1.113 -    by (simp add: inter project_def Cset.set_def)
   1.114 +    by (simp add: inter project_def Cset.set_def member_cset_of)
   1.115    have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   1.116 -    by (simp add: fun_eq_iff More_Set.remove_def)
   1.117 +    by (simp add: fun_eq_iff More_Set.remove_def member_cset_of)
   1.118    have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   1.119      fold More_Set.remove xs \<circ> member"
   1.120      by (rule fold_commute) (simp add: fun_eq_iff)
   1.121 @@ -201,9 +195,9 @@
   1.122      member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
   1.123      by (simp add: fun_eq_iff)
   1.124    then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
   1.125 -    by (simp add: Diff_eq [symmetric] minus_set *)
   1.126 +    by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
   1.127    moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
   1.128 -    by (auto simp add: More_Set.remove_def * intro: ext)
   1.129 +    by (auto simp add: More_Set.remove_def * member_cset_of intro: ext)
   1.130    ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
   1.131      by (simp add: foldr_fold)
   1.132  qed
   1.133 @@ -218,7 +212,7 @@
   1.134    "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.135  proof -
   1.136    have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   1.137 -    by (simp add: fun_eq_iff)
   1.138 +    by (simp add: fun_eq_iff member_cset_of)
   1.139    have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
   1.140      fold Set.insert xs \<circ> member"
   1.141      by (rule fold_commute) (simp add: fun_eq_iff)
   1.142 @@ -226,15 +220,15 @@
   1.143      member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   1.144      by (simp add: fun_eq_iff)
   1.145    then have "sup (Cset.set xs) A = fold Cset.insert xs A"
   1.146 -    by (simp add: union_set *)
   1.147 +    by (simp add: union_set * member_cset_of)
   1.148    moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   1.149 -    by (auto simp add: * intro: ext)
   1.150 +    by (auto simp add: * member_cset_of intro: ext)
   1.151    ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
   1.152      by (simp add: foldr_fold)
   1.153    show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.154 -    by (auto simp add: coset_def)
   1.155 +    by (auto simp add: coset_def member_cset_of)
   1.156  qed
   1.157  
   1.158  declare mem_def[simp del]
   1.159  
   1.160 -end
   1.161 \ No newline at end of file
   1.162 +end