src/HOL/Library/Cset.thy
changeset 45970 b6d0cff57d96
parent 44563 01b2732cf4ad
child 45986 c9e50153e5ae
     1.1 --- a/src/HOL/Library/Cset.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Library/Cset.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -24,10 +24,6 @@
     1.4  definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
     1.5    "member A x \<longleftrightarrow> x \<in> set_of A"
     1.6  
     1.7 -lemma member_set_of:
     1.8 -  "set_of = member"
     1.9 -  by (rule ext)+ (simp add: member_def mem_def)
    1.10 -
    1.11  lemma member_Set [simp]:
    1.12    "member (Set A) x \<longleftrightarrow> x \<in> A"
    1.13    by (simp add: member_def)
    1.14 @@ -38,7 +34,7 @@
    1.15  
    1.16  lemma set_eq_iff:
    1.17    "A = B \<longleftrightarrow> member A = member B"
    1.18 -  by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def mem_def)
    1.19 +  by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def)
    1.20  hide_fact (open) set_eq_iff
    1.21  
    1.22  lemma set_eqI:
    1.23 @@ -76,7 +72,7 @@
    1.24    [simp]: "A - B = Set (set_of A - set_of B)"
    1.25  
    1.26  instance proof
    1.27 -qed (auto intro!: Cset.set_eqI simp add: member_def mem_def)
    1.28 +qed (auto intro!: Cset.set_eqI simp add: member_def)
    1.29  
    1.30  end
    1.31  
    1.32 @@ -364,19 +360,13 @@
    1.33       Predicate.Empty \<Rightarrow> Cset.empty
    1.34     | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
    1.35     | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
    1.36 -  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.37 -  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
    1.38 -  apply simp_all
    1.39 -  done
    1.40 +  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.41  
    1.42  lemma of_seq_code [code]:
    1.43    "of_seq Predicate.Empty = Cset.empty"
    1.44    "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
    1.45    "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
    1.46 -  apply (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff mem_def Collect_def)
    1.47 -  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
    1.48 -  apply simp_all
    1.49 -  done
    1.50 +  by (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
    1.51  
    1.52  lemma bind_set:
    1.53    "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
    1.54 @@ -387,9 +377,9 @@
    1.55    "pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot"
    1.56  proof -
    1.57    have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
    1.58 -    by (simp add: Cset.pred_of_cset_def member_set)
    1.59 +    by (simp add: Cset.pred_of_cset_def)
    1.60    moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
    1.61 -    by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI, simp add: mem_def)
    1.62 +    by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI)
    1.63    ultimately show ?thesis by simp
    1.64  qed
    1.65  hide_fact (open) pred_of_cset_set