--- a/Nominal/FSet.thy Wed Apr 14 08:16:54 2010 +0200
+++ b/Nominal/FSet.thy Wed Apr 14 08:35:31 2010 +0200
@@ -245,9 +245,9 @@
"x # x # xs \<approx> x # xs"
by auto
-lemma none_mem_nil:
- "(\<forall>x. x \<notin> set xs) = (xs \<approx> [])"
- by simp
+lemma none_memb_nil:
+ "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+ by (simp add: memb_def)
lemma fset_raw_strong_cases:
"(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
@@ -339,7 +339,7 @@
lemma ffold_raw_rsp_pre:
"\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
apply (induct a arbitrary: b)
- apply (simp add: hd_in_set memb_absorb memb_def none_mem_nil)
+ apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
apply (simp add: ffold_raw.simps)
apply (rule conjI)
apply (rule_tac [!] impI)
@@ -486,8 +486,8 @@
by (lifting memb_def[symmetric])
lemma none_fin_fempty:
- "(\<forall>x. x \<notin> fset_to_set S) = (S = {||})"
- by (lifting none_mem_nil)
+ "(\<forall>x. x |\<notin>| S) = (S = {||})"
+ by (lifting none_memb_nil)
lemma fset_cong:
"(fset_to_set S = fset_to_set T) = (S = T)"