--- a/Nominal/FSet.thy	Fri Oct 15 15:52:40 2010 +0900
+++ b/Nominal/FSet.thy	Fri Oct 15 16:23:26 2010 +0900
@@ -298,59 +298,12 @@
   then show "concat a \<approx> concat b" by auto
 qed
 
-
-
-
 lemma [quot_respect]:
   shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
   by auto
 
 text {* Distributive lattice with bot *}
 
-lemma sub_list_not_eq:
-  "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
-  by (auto simp add: sub_list_def)
-
-lemma sub_list_refl:
-  "sub_list x x"
-  by (simp add: sub_list_def)
-
-lemma sub_list_trans:
-  "sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z"
-  by (simp add: sub_list_def)
-
-lemma sub_list_empty:
-  "sub_list [] x"
-  by (simp add: sub_list_def)
-
-lemma sub_list_append_left:
-  "sub_list x (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_append_right:
-  "sub_list y (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_inter_left:
-  shows "sub_list (finter_raw x y) x"
-  by (simp add: sub_list_def)
-
-lemma sub_list_inter_right:
-  shows "sub_list (finter_raw x y) y"
-  by (simp add: sub_list_def)
-
-lemma sub_list_list_eq:
-  "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
-  unfolding sub_list_def list_eq.simps by blast
-
-lemma sub_list_append:
-  "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
-  unfolding sub_list_def by auto
-
-lemma sub_list_inter:
-  "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
-  by (simp add: sub_list_def)
-
 lemma append_inter_distrib:
   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
   apply (induct x)
@@ -417,7 +370,8 @@
 proof
   fix x y z :: "'a fset"
   show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
-    unfolding less_fset_def by (lifting sub_list_not_eq)
+    unfolding less_fset_def 
+    by (descending) (auto simp add: sub_list_def)
   show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
   show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
   show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
@@ -707,10 +661,6 @@
   "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (auto simp add: fcard_raw_def memb_def)
 
-lemma finter_raw_empty:
-  "finter_raw l [] = []"
-  by (induct l) (simp_all add: not_memb_nil)
-
 lemma inj_map_eq_iff:
   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
   by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
@@ -843,11 +793,11 @@
   by (lifting memb_def[symmetric])
 
 lemma none_fin_fempty:
-  "(\<forall>x. x |\<notin>| S) = (S = {||})"
+  "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
   by (lifting none_memb_nil)
 
 lemma fset_cong:
-  "(S = T) = (fset S = fset T)"
+  "S = T \<longleftrightarrow> fset S = fset T"
   by (lifting list_eq.simps)
 
 
@@ -857,7 +807,7 @@
   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
   by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb)
 
-lemma fcard_0[simp]: 
+lemma fcard_0[simp]:
   shows "fcard S = 0 \<longleftrightarrow> S = {||}"
   by (descending) (simp add: fcard_raw_def)
 
@@ -1090,11 +1040,13 @@
 
 section {* finter *}
 
-lemma finter_empty_l: "({||} |\<inter>| S) = {||}"
-  by (lifting finter_raw.simps(1))
+lemma finter_empty_l:
+  shows "{||} |\<inter>| S = {||}"
+  by simp
 
-lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"
-  by (lifting finter_raw_empty)
+lemma finter_empty_r:
+  shows "S |\<inter>| {||} = {||}"
+  by simp
 
 lemma finter_finsert:
   shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
@@ -1105,7 +1057,7 @@
   by (descending) (simp add: memb_def)
 
 lemma fsubset_finsert:
-  shows "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
+  shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
   by (lifting sub_list_cons)
 
 lemma 
@@ -1117,7 +1069,7 @@
   by (descending) (auto simp add: sub_list_def memb_def)
 
 lemma fminus_fin: 
-  shows "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+  shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
   by (descending) (simp add: memb_def)
 
 lemma fminus_red: 
@@ -1207,8 +1159,8 @@
   apply(simp_all)
   done
 
-lemma fsubseteq_fempty: 
-  shows "xs |\<subseteq>| {||} = (xs = {||})"
+lemma fsubseteq_fempty:
+  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
   by (metis finter_empty_r le_iff_inf)
 
 lemma not_fsubset_fnil: 
@@ -1276,8 +1228,8 @@
   unfolding fin_set fminus_set
   by blast
 
-lemma fin_mdef: 
-  shows "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+lemma fin_mdef:
+  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
   unfolding fin_set fset_simps fset_cong fminus_set
   by blast