src/HOL/Library/Cset.thy
changeset 46884 154dc6ec0041
parent 46146 6baea4fca6bd
child 47232 e2f0176149d0
     1.1 --- a/src/HOL/Library/Cset.thy	Mon Mar 12 15:12:22 2012 +0100
     1.2 +++ b/src/HOL/Library/Cset.thy	Mon Mar 12 21:41:11 2012 +0100
     1.3 @@ -175,10 +175,10 @@
     1.4  subsection {* Simplified simprules *}
     1.5  
     1.6  lemma empty_simp [simp]: "member Cset.empty = bot"
     1.7 -  by (simp add: fun_eq_iff bot_apply)
     1.8 +  by (simp add: fun_eq_iff)
     1.9  
    1.10  lemma UNIV_simp [simp]: "member Cset.UNIV = top"
    1.11 -  by (simp add: fun_eq_iff top_apply)
    1.12 +  by (simp add: fun_eq_iff)
    1.13  
    1.14  lemma is_empty_simp [simp]:
    1.15    "is_empty A \<longleftrightarrow> set_of A = {}"
    1.16 @@ -222,7 +222,7 @@
    1.17  
    1.18  lemma member_SUP [simp]:
    1.19    "member (SUPR A f) = SUPR A (member \<circ> f)"
    1.20 -  by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto)
    1.21 +  by (auto simp add: fun_eq_iff member_def, unfold SUP_def, auto)
    1.22  
    1.23  lemma member_bind [simp]:
    1.24    "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
    1.25 @@ -247,14 +247,14 @@
    1.26   
    1.27  lemma bind_single [simp]:
    1.28    "A \<guillemotright>= single = A"
    1.29 -  by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def)
    1.30 +  by (simp add: Cset.set_eq_iff fun_eq_iff single_def member_def)
    1.31  
    1.32  lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
    1.33    by (auto simp add: Cset.set_eq_iff fun_eq_iff)
    1.34  
    1.35  lemma empty_bind [simp]:
    1.36    "Cset.empty \<guillemotright>= f = Cset.empty"
    1.37 -  by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply)
    1.38 +  by (simp add: Cset.set_eq_iff fun_eq_iff )
    1.39  
    1.40  lemma member_of_pred [simp]:
    1.41    "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
    1.42 @@ -360,7 +360,7 @@
    1.43       Predicate.Empty \<Rightarrow> Cset.empty
    1.44     | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
    1.45     | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
    1.46 -  by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric])
    1.47 +  by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff eval_member [symmetric] member_def [symmetric])
    1.48  
    1.49  lemma of_seq_code [code]:
    1.50    "of_seq Predicate.Empty = Cset.empty"