src/HOL/Library/Cset.thy
changeset 44555 da75ffe3d988
parent 43971 892030194015
child 44558 cc878a312673
     1.1 --- a/src/HOL/Library/Cset.thy	Fri Aug 26 18:24:22 2011 +0200
     1.2 +++ b/src/HOL/Library/Cset.thy	Fri Aug 26 21:11:23 2011 +0200
     1.3 @@ -10,16 +10,27 @@
     1.4  subsection {* Lifting *}
     1.5  
     1.6  typedef (open) 'a set = "UNIV :: 'a set set"
     1.7 -  morphisms member Set by rule+
     1.8 +  morphisms set_of Set by rule+
     1.9  hide_type (open) set
    1.10  
    1.11 +lemma set_of_Set [simp]:
    1.12 +  "set_of (Set A) = A"
    1.13 +  by (rule Set_inverse) rule
    1.14 +
    1.15 +lemma Set_set_of [simp]:
    1.16 +  "Set (set_of A) = A"
    1.17 +  by (fact set_of_inverse)
    1.18 +
    1.19 +definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
    1.20 +  "member A x \<longleftrightarrow> x \<in> set_of A"
    1.21 +
    1.22 +lemma member_set_of:
    1.23 +  "set_of = member"
    1.24 +  by (rule ext)+ (simp add: member_def mem_def)
    1.25 +
    1.26  lemma member_Set [simp]:
    1.27 -  "member (Set A) = A"
    1.28 -  by (rule Set_inverse) rule
    1.29 -
    1.30 -lemma Set_member [simp]:
    1.31 -  "Set (member A) = A"
    1.32 -  by (fact member_inverse)
    1.33 +  "member (Set A) x \<longleftrightarrow> x \<in> A"
    1.34 +  by (simp add: member_def)
    1.35  
    1.36  lemma Set_inject [simp]:
    1.37    "Set A = Set B \<longleftrightarrow> A = B"
    1.38 @@ -27,7 +38,7 @@
    1.39  
    1.40  lemma set_eq_iff:
    1.41    "A = B \<longleftrightarrow> member A = member B"
    1.42 -  by (simp add: member_inject)
    1.43 +  by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def mem_def)
    1.44  hide_fact (open) set_eq_iff
    1.45  
    1.46  lemma set_eqI:
    1.47 @@ -41,16 +52,16 @@
    1.48  begin
    1.49  
    1.50  definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
    1.51 -  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
    1.52 +  [simp]: "A \<le> B \<longleftrightarrow> set_of A \<subseteq> set_of B"
    1.53  
    1.54  definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
    1.55 -  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
    1.56 +  [simp]: "A < B \<longleftrightarrow> set_of A \<subset> set_of B"
    1.57  
    1.58  definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.59 -  [simp]: "inf A B = Set (member A \<inter> member B)"
    1.60 +  [simp]: "inf A B = Set (set_of A \<inter> set_of B)"
    1.61  
    1.62  definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.63 -  [simp]: "sup A B = Set (member A \<union> member B)"
    1.64 +  [simp]: "sup A B = Set (set_of A \<union> set_of B)"
    1.65  
    1.66  definition bot_set :: "'a Cset.set" where
    1.67    [simp]: "bot = Set {}"
    1.68 @@ -59,13 +70,13 @@
    1.69    [simp]: "top = Set UNIV"
    1.70  
    1.71  definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.72 -  [simp]: "- A = Set (- (member A))"
    1.73 +  [simp]: "- A = Set (- (set_of A))"
    1.74  
    1.75  definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.76 -  [simp]: "A - B = Set (member A - member B)"
    1.77 +  [simp]: "A - B = Set (set_of A - set_of B)"
    1.78  
    1.79  instance proof
    1.80 -qed (auto intro: Cset.set_eqI)
    1.81 +qed (auto intro!: Cset.set_eqI simp add: member_def mem_def)
    1.82  
    1.83  end
    1.84  
    1.85 @@ -73,16 +84,19 @@
    1.86  begin
    1.87  
    1.88  definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
    1.89 -  [simp]: "Inf_set As = Set (Inf (image member As))"
    1.90 +  [simp]: "Inf_set As = Set (Inf (image set_of As))"
    1.91  
    1.92  definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
    1.93 -  [simp]: "Sup_set As = Set (Sup (image member As))"
    1.94 +  [simp]: "Sup_set As = Set (Sup (image set_of As))"
    1.95  
    1.96  instance proof
    1.97 -qed (auto simp add: le_fun_def le_bool_def)
    1.98 +qed (auto simp add: le_fun_def)
    1.99  
   1.100  end
   1.101  
   1.102 +instance Cset.set :: (type) complete_boolean_algebra proof
   1.103 +qed (unfold INF_def SUP_def, auto)
   1.104 +
   1.105  
   1.106  subsection {* Basic operations *}
   1.107  
   1.108 @@ -93,40 +107,40 @@
   1.109  hide_const (open) UNIV
   1.110  
   1.111  definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
   1.112 -  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
   1.113 +  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (set_of A)"
   1.114  
   1.115  definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.116 -  [simp]: "insert x A = Set (Set.insert x (member A))"
   1.117 +  [simp]: "insert x A = Set (Set.insert x (set_of A))"
   1.118  
   1.119  definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.120 -  [simp]: "remove x A = Set (More_Set.remove x (member A))"
   1.121 +  [simp]: "remove x A = Set (More_Set.remove x (set_of A))"
   1.122  
   1.123  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
   1.124 -  [simp]: "map f A = Set (image f (member A))"
   1.125 +  [simp]: "map f A = Set (image f (set_of A))"
   1.126  
   1.127  enriched_type map: map
   1.128    by (simp_all add: fun_eq_iff image_compose)
   1.129  
   1.130  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.131 -  [simp]: "filter P A = Set (More_Set.project P (member A))"
   1.132 +  [simp]: "filter P A = Set (More_Set.project P (set_of A))"
   1.133  
   1.134  definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.135 -  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
   1.136 +  [simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P"
   1.137  
   1.138  definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.139 -  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
   1.140 +  [simp]: "exists P A \<longleftrightarrow> Bex (set_of A) P"
   1.141  
   1.142  definition card :: "'a Cset.set \<Rightarrow> nat" where
   1.143 -  [simp]: "card A = Finite_Set.card (member A)"
   1.144 +  [simp]: "card A = Finite_Set.card (set_of A)"
   1.145    
   1.146  context complete_lattice
   1.147  begin
   1.148  
   1.149  definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
   1.150 -  [simp]: "Infimum A = Inf (member A)"
   1.151 +  [simp]: "Infimum A = Inf (set_of A)"
   1.152  
   1.153  definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
   1.154 -  [simp]: "Supremum A = Sup (member A)"
   1.155 +  [simp]: "Supremum A = Sup (set_of A)"
   1.156  
   1.157  end
   1.158  
   1.159 @@ -140,134 +154,138 @@
   1.160  
   1.161  text {* conversion from @{typ "'a Predicate.pred"} *}
   1.162  
   1.163 -definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred"
   1.164 -where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
   1.165 +definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where
   1.166 +  [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
   1.167  
   1.168 -definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
   1.169 -where "of_pred = Cset.Set \<circ> Predicate.eval"
   1.170 +definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set" where
   1.171 +  "of_pred = Cset.Set \<circ> Collect \<circ> Predicate.eval"
   1.172  
   1.173 -definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
   1.174 -where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
   1.175 +definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set" where 
   1.176 +  "of_seq = of_pred \<circ> Predicate.pred_of_seq"
   1.177  
   1.178  text {* monad operations *}
   1.179  
   1.180  definition single :: "'a \<Rightarrow> 'a Cset.set" where
   1.181    "single a = Set {a}"
   1.182  
   1.183 -definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
   1.184 -                (infixl "\<guillemotright>=" 70)
   1.185 -  where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
   1.186 +definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" (infixl "\<guillemotright>=" 70) where
   1.187 +  "A \<guillemotright>= f = (SUP x : set_of A. f x)"
   1.188 +
   1.189  
   1.190  subsection {* Simplified simprules *}
   1.191  
   1.192 -lemma empty_simp [simp]: "member Cset.empty = {}"
   1.193 -  by(simp)
   1.194 +lemma empty_simp [simp]: "member Cset.empty = bot"
   1.195 +  by (simp add: fun_eq_iff bot_apply)
   1.196  
   1.197 -lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV"
   1.198 -  by simp
   1.199 +lemma UNIV_simp [simp]: "member Cset.UNIV = top"
   1.200 +  by (simp add: fun_eq_iff top_apply)
   1.201  
   1.202  lemma is_empty_simp [simp]:
   1.203 -  "is_empty A \<longleftrightarrow> member A = {}"
   1.204 +  "is_empty A \<longleftrightarrow> set_of A = {}"
   1.205    by (simp add: More_Set.is_empty_def)
   1.206  declare is_empty_def [simp del]
   1.207  
   1.208  lemma remove_simp [simp]:
   1.209 -  "remove x A = Set (member A - {x})"
   1.210 +  "remove x A = Set (set_of A - {x})"
   1.211    by (simp add: More_Set.remove_def)
   1.212  declare remove_def [simp del]
   1.213  
   1.214  lemma filter_simp [simp]:
   1.215 -  "filter P A = Set {x \<in> member A. P x}"
   1.216 +  "filter P A = Set {x \<in> set_of A. P x}"
   1.217    by (simp add: More_Set.project_def)
   1.218  declare filter_def [simp del]
   1.219  
   1.220 -lemma member_set [simp]:
   1.221 -  "member (Cset.set xs) = set xs"
   1.222 +lemma set_of_set [simp]:
   1.223 +  "set_of (Cset.set xs) = set xs"
   1.224    by (simp add: set_def)
   1.225 -hide_fact (open) member_set set_def
   1.226 +hide_fact (open) set_def
   1.227  
   1.228  lemma set_simps [simp]:
   1.229    "Cset.set [] = Cset.empty"
   1.230    "Cset.set (x # xs) = insert x (Cset.set xs)"
   1.231  by(simp_all add: Cset.set_def)
   1.232  
   1.233 -lemma member_SUPR [simp]:
   1.234 +lemma member_SUP [simp]:
   1.235    "member (SUPR A f) = SUPR A (member \<circ> f)"
   1.236 -unfolding SUPR_def by simp
   1.237 +  by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto)
   1.238  
   1.239  lemma member_bind [simp]:
   1.240 -  "member (P \<guillemotright>= f) = member (SUPR (member P) f)"
   1.241 -by (simp add: bind_def Cset.set_eq_iff)
   1.242 +  "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
   1.243 +  by (simp add: bind_def Cset.set_eq_iff)
   1.244  
   1.245  lemma member_single [simp]:
   1.246 -  "member (single a) = {a}"
   1.247 -by(simp add: single_def)
   1.248 +  "member (single a) = (\<lambda>x. x \<in> {a})"
   1.249 +  by (simp add: single_def fun_eq_iff)
   1.250  
   1.251  lemma single_sup_simps [simp]:
   1.252    shows single_sup: "sup (single a) A = insert a A"
   1.253    and sup_single: "sup A (single a) = insert a A"
   1.254 -by(auto simp add: Cset.set_eq_iff)
   1.255 +  by (auto simp add: Cset.set_eq_iff single_def)
   1.256  
   1.257  lemma single_bind [simp]:
   1.258    "single a \<guillemotright>= B = B a"
   1.259 -by(simp add: bind_def single_def)
   1.260 +  by (simp add: Cset.set_eq_iff SUP_insert single_def)
   1.261  
   1.262  lemma bind_bind:
   1.263    "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
   1.264 -by(simp add: bind_def)
   1.265 -
   1.266 +  by (simp add: bind_def, simp only: SUP_def image_image, simp)
   1.267 + 
   1.268  lemma bind_single [simp]:
   1.269    "A \<guillemotright>= single = A"
   1.270 -by(simp add: bind_def single_def)
   1.271 +  by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def)
   1.272  
   1.273  lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
   1.274 -by(auto simp add: Cset.set_eq_iff)
   1.275 +  by (auto simp add: Cset.set_eq_iff fun_eq_iff)
   1.276  
   1.277  lemma empty_bind [simp]:
   1.278    "Cset.empty \<guillemotright>= f = Cset.empty"
   1.279 -by(simp add: Cset.set_eq_iff)
   1.280 +  by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply)
   1.281  
   1.282  lemma member_of_pred [simp]:
   1.283 -  "member (of_pred P) = {x. Predicate.eval P x}"
   1.284 -by(simp add: of_pred_def Collect_def)
   1.285 +  "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
   1.286 +  by (simp add: of_pred_def fun_eq_iff)
   1.287  
   1.288  lemma member_of_seq [simp]:
   1.289 -  "member (of_seq xq) = {x. Predicate.member xq x}"
   1.290 -by(simp add: of_seq_def eval_member)
   1.291 +  "member (of_seq xq) = (\<lambda>x. x \<in> {x. Predicate.member xq x})"
   1.292 +  by (simp add: of_seq_def eval_member)
   1.293  
   1.294  lemma eval_pred_of_cset [simp]: 
   1.295    "Predicate.eval (pred_of_cset A) = Cset.member A"
   1.296 -by(simp add: pred_of_cset_def)
   1.297 +  by (simp add: pred_of_cset_def)
   1.298  
   1.299  subsection {* Default implementations *}
   1.300  
   1.301  lemma set_code [code]:
   1.302 -  "Cset.set = foldl (\<lambda>A x. insert x A) Cset.empty"
   1.303 -proof(rule ext, rule Cset.set_eqI)
   1.304 -  fix xs
   1.305 -  show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
   1.306 -    by(induct xs rule: rev_induct)(simp_all)
   1.307 +  "Cset.set = (\<lambda>xs. fold insert xs Cset.empty)"
   1.308 +proof (rule ext, rule Cset.set_eqI)
   1.309 +  fix xs :: "'a list"
   1.310 +  show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
   1.311 +    by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
   1.312 +      fun_eq_iff Cset.set_def union_set [symmetric])
   1.313  qed
   1.314  
   1.315  lemma single_code [code]:
   1.316    "single a = insert a Cset.empty"
   1.317 -by(simp add: Cset.single_def)
   1.318 +  by (simp add: Cset.single_def)
   1.319  
   1.320  lemma of_pred_code [code]:
   1.321    "of_pred (Predicate.Seq f) = (case f () of
   1.322       Predicate.Empty \<Rightarrow> Cset.empty
   1.323     | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
   1.324     | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
   1.325 -by(auto split: seq.split 
   1.326 -        simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff)
   1.327 +  apply (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric] Collect_def mem_def member_set_of)
   1.328 +  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
   1.329 +  apply simp_all
   1.330 +  done
   1.331  
   1.332  lemma of_seq_code [code]:
   1.333    "of_seq Predicate.Empty = Cset.empty"
   1.334    "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
   1.335    "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
   1.336 -by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
   1.337 -
   1.338 -declare mem_def [simp del]
   1.339 +  apply (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff mem_def Collect_def)
   1.340 +  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
   1.341 +  apply simp_all
   1.342 +  done
   1.343  
   1.344  no_notation bind (infixl "\<guillemotright>=" 70)
   1.345  
   1.346 @@ -275,7 +293,7 @@
   1.347    Inter Union bind single of_pred of_seq
   1.348  
   1.349  hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def 
   1.350 -  bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind 
   1.351 +  bind_def empty_simp UNIV_simp set_simps member_bind 
   1.352    member_single single_sup_simps single_sup sup_single single_bind
   1.353    bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
   1.354    eval_pred_of_cset set_code single_code of_pred_code of_seq_code