src/HOL/Library/Cset.thy
changeset 43971 892030194015
parent 43241 93b1183e43e5
child 44555 da75ffe3d988
     1.1 --- a/src/HOL/Library/Cset.thy	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Library/Cset.thy	Mon Jul 25 16:55:48 2011 +0200
     1.3 @@ -86,6 +86,12 @@
     1.4  
     1.5  subsection {* Basic operations *}
     1.6  
     1.7 +abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
     1.8 +hide_const (open) empty
     1.9 +
    1.10 +abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
    1.11 +hide_const (open) UNIV
    1.12 +
    1.13  definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
    1.14    [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
    1.15  
    1.16 @@ -124,9 +130,42 @@
    1.17  
    1.18  end
    1.19  
    1.20 +subsection {* More operations *}
    1.21 +
    1.22 +text {* conversion from @{typ "'a list"} *}
    1.23 +
    1.24 +definition set :: "'a list \<Rightarrow> 'a Cset.set" where
    1.25 +  "set xs = Set (List.set xs)"
    1.26 +hide_const (open) set
    1.27 +
    1.28 +text {* conversion from @{typ "'a Predicate.pred"} *}
    1.29 +
    1.30 +definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred"
    1.31 +where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
    1.32 +
    1.33 +definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
    1.34 +where "of_pred = Cset.Set \<circ> Predicate.eval"
    1.35 +
    1.36 +definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
    1.37 +where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
    1.38 +
    1.39 +text {* monad operations *}
    1.40 +
    1.41 +definition single :: "'a \<Rightarrow> 'a Cset.set" where
    1.42 +  "single a = Set {a}"
    1.43 +
    1.44 +definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
    1.45 +                (infixl "\<guillemotright>=" 70)
    1.46 +  where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
    1.47  
    1.48  subsection {* Simplified simprules *}
    1.49  
    1.50 +lemma empty_simp [simp]: "member Cset.empty = {}"
    1.51 +  by(simp)
    1.52 +
    1.53 +lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV"
    1.54 +  by simp
    1.55 +
    1.56  lemma is_empty_simp [simp]:
    1.57    "is_empty A \<longleftrightarrow> member A = {}"
    1.58    by (simp add: More_Set.is_empty_def)
    1.59 @@ -142,10 +181,103 @@
    1.60    by (simp add: More_Set.project_def)
    1.61  declare filter_def [simp del]
    1.62  
    1.63 +lemma member_set [simp]:
    1.64 +  "member (Cset.set xs) = set xs"
    1.65 +  by (simp add: set_def)
    1.66 +hide_fact (open) member_set set_def
    1.67 +
    1.68 +lemma set_simps [simp]:
    1.69 +  "Cset.set [] = Cset.empty"
    1.70 +  "Cset.set (x # xs) = insert x (Cset.set xs)"
    1.71 +by(simp_all add: Cset.set_def)
    1.72 +
    1.73 +lemma member_SUPR [simp]:
    1.74 +  "member (SUPR A f) = SUPR A (member \<circ> f)"
    1.75 +unfolding SUPR_def by simp
    1.76 +
    1.77 +lemma member_bind [simp]:
    1.78 +  "member (P \<guillemotright>= f) = member (SUPR (member P) f)"
    1.79 +by (simp add: bind_def Cset.set_eq_iff)
    1.80 +
    1.81 +lemma member_single [simp]:
    1.82 +  "member (single a) = {a}"
    1.83 +by(simp add: single_def)
    1.84 +
    1.85 +lemma single_sup_simps [simp]:
    1.86 +  shows single_sup: "sup (single a) A = insert a A"
    1.87 +  and sup_single: "sup A (single a) = insert a A"
    1.88 +by(auto simp add: Cset.set_eq_iff)
    1.89 +
    1.90 +lemma single_bind [simp]:
    1.91 +  "single a \<guillemotright>= B = B a"
    1.92 +by(simp add: bind_def single_def)
    1.93 +
    1.94 +lemma bind_bind:
    1.95 +  "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
    1.96 +by(simp add: bind_def)
    1.97 +
    1.98 +lemma bind_single [simp]:
    1.99 +  "A \<guillemotright>= single = A"
   1.100 +by(simp add: bind_def single_def)
   1.101 +
   1.102 +lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
   1.103 +by(auto simp add: Cset.set_eq_iff)
   1.104 +
   1.105 +lemma empty_bind [simp]:
   1.106 +  "Cset.empty \<guillemotright>= f = Cset.empty"
   1.107 +by(simp add: Cset.set_eq_iff)
   1.108 +
   1.109 +lemma member_of_pred [simp]:
   1.110 +  "member (of_pred P) = {x. Predicate.eval P x}"
   1.111 +by(simp add: of_pred_def Collect_def)
   1.112 +
   1.113 +lemma member_of_seq [simp]:
   1.114 +  "member (of_seq xq) = {x. Predicate.member xq x}"
   1.115 +by(simp add: of_seq_def eval_member)
   1.116 +
   1.117 +lemma eval_pred_of_cset [simp]: 
   1.118 +  "Predicate.eval (pred_of_cset A) = Cset.member A"
   1.119 +by(simp add: pred_of_cset_def)
   1.120 +
   1.121 +subsection {* Default implementations *}
   1.122 +
   1.123 +lemma set_code [code]:
   1.124 +  "Cset.set = foldl (\<lambda>A x. insert x A) Cset.empty"
   1.125 +proof(rule ext, rule Cset.set_eqI)
   1.126 +  fix xs
   1.127 +  show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
   1.128 +    by(induct xs rule: rev_induct)(simp_all)
   1.129 +qed
   1.130 +
   1.131 +lemma single_code [code]:
   1.132 +  "single a = insert a Cset.empty"
   1.133 +by(simp add: Cset.single_def)
   1.134 +
   1.135 +lemma of_pred_code [code]:
   1.136 +  "of_pred (Predicate.Seq f) = (case f () of
   1.137 +     Predicate.Empty \<Rightarrow> Cset.empty
   1.138 +   | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
   1.139 +   | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
   1.140 +by(auto split: seq.split 
   1.141 +        simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff)
   1.142 +
   1.143 +lemma of_seq_code [code]:
   1.144 +  "of_seq Predicate.Empty = Cset.empty"
   1.145 +  "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
   1.146 +  "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
   1.147 +by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
   1.148 +
   1.149  declare mem_def [simp del]
   1.150  
   1.151 +no_notation bind (infixl "\<guillemotright>=" 70)
   1.152  
   1.153  hide_const (open) is_empty insert remove map filter forall exists card
   1.154 -  Inter Union
   1.155 +  Inter Union bind single of_pred of_seq
   1.156 +
   1.157 +hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def 
   1.158 +  bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind 
   1.159 +  member_single single_sup_simps single_sup sup_single single_bind
   1.160 +  bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
   1.161 +  eval_pred_of_cset set_code single_code of_pred_code of_seq_code
   1.162  
   1.163  end