diff -r 135ac0fb2686 -r d7269488c4b5 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sun Oct 17 13:35:52 2010 +0100
+++ b/Nominal/FSet.thy	Sun Oct 17 15:28:05 2010 +0100
@@ -450,12 +450,13 @@
   by simp
 
 lemma insert_fset_rsp [quot_preserve]:
-  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = insert_fset"
+  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) Cons = insert_fset"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id insert_fset_def)
 
 lemma union_fset_rsp [quot_preserve]:
-  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = union_fset"
+  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) 
+  append = union_fset"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
@@ -519,69 +520,6 @@
 
 section {* Lifted theorems *}
 
-
-subsection {* in_fset *}
-
-lemma notin_empty_fset: 
-  shows "x |\<notin>| {||}"
-  by (descending) (simp add: memb_def)
-
-lemma in_fset: 
-  shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
-  by (descending) (simp add: memb_def)
-
-lemma notin_fset: 
-  shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
-  by (descending) (simp add: memb_def)
-
-lemma fset_eq_iff:
-  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
-  by (descending) (auto simp add: memb_def)
-
-lemma none_in_empty_fset:
-  shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
-  by (descending) (simp add: memb_def)
-
-
-subsection {* insert_fset *}
-
-lemma in_insert_fset_iff[simp]:
-  shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
-  by (descending) (simp add: memb_def)
-
-lemma
-  shows insert_fsetI1: "x |\<in>| insert_fset x S"
-  and   insert_fsetI2: "x |\<in>| S \<Longrightarrow> x |\<in>| insert_fset y S"
-  by (descending, simp add: memb_def)+
-
-lemma insert_absorb_fset[simp]:
-  shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S"
-  by (descending) (auto simp add: memb_def)
-
-lemma empty_not_insert_fset[simp]:
-  shows "{||} \<noteq> insert_fset x S"
-  and   "insert_fset x S \<noteq> {||}"
-  by (descending, simp)+
-
-lemma insert_fset_left_comm:
-  shows "insert_fset x (insert_fset y S) = insert_fset y (insert_fset x S)"
-  by (descending) (auto)
-
-lemma insert_fset_left_idem:
-  shows "insert_fset x (insert_fset x S) = insert_fset x S"
-  by (descending) (auto)
-
-lemma singleton_fset_eq[simp]:
-  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
-  by (descending) (auto)
-
-
-(* FIXME: is this in any case a useful lemma *)
-lemma in_fset_mdef:
-  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
-  by (descending) (auto simp add: memb_def diff_list_def)
-
-
 subsection {* fset *}
 
 lemma fset_simps [simp]:
@@ -618,6 +556,68 @@
   by (descending) (auto simp add: diff_list_def)
 
 
+subsection {* in_fset *}
+
+lemma in_fset: 
+  shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
+  by (descending) (simp add: memb_def)
+
+lemma notin_fset: 
+  shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
+  by (simp add: in_fset)
+
+lemma notin_empty_fset: 
+  shows "x |\<notin>| {||}"
+  by (simp add: in_fset)
+
+lemma fset_eq_iff:
+  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
+  by (descending) (auto simp add: memb_def)
+
+lemma none_in_empty_fset:
+  shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
+  by (descending) (simp add: memb_def)
+
+
+subsection {* insert_fset *}
+
+lemma in_insert_fset_iff [simp]:
+  shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
+  by (descending) (simp add: memb_def)
+
+lemma
+  shows insert_fsetI1: "x |\<in>| insert_fset x S"
+  and   insert_fsetI2: "x |\<in>| S \<Longrightarrow> x |\<in>| insert_fset y S"
+  by simp_all
+
+lemma insert_absorb_fset [simp]:
+  shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S"
+  by (descending) (auto simp add: memb_def)
+
+lemma empty_not_insert_fset[simp]:
+  shows "{||} \<noteq> insert_fset x S"
+  and   "insert_fset x S \<noteq> {||}"
+  by (descending, simp)+
+
+lemma insert_fset_left_comm:
+  shows "insert_fset x (insert_fset y S) = insert_fset y (insert_fset x S)"
+  by (descending) (auto)
+
+lemma insert_fset_left_idem:
+  shows "insert_fset x (insert_fset x S) = insert_fset x S"
+  by (descending) (auto)
+
+lemma singleton_fset_eq[simp]:
+  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
+  by (descending) (auto)
+
+
+(* FIXME: is this a useful lemma ? *)
+lemma in_fset_mdef:
+  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
+  by (descending) (auto simp add: memb_def diff_list_def)
+
+
 subsection {* union_fset *}
 
 lemmas [simp] =
@@ -659,12 +659,12 @@
   shows "x |\<notin>| ys \<Longrightarrow> insert_fset x xs - ys = insert_fset x (xs - ys)"
   by (simp add: minus_insert_fset)
 
-lemma in_fset_minus_fset_notin_fset: 
+lemma in_minus_fset: 
   shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
   unfolding in_fset minus_fset
   by blast
 
-lemma in_fset_notin_fset_minus_fset: 
+lemma notin_minus_fset: 
   shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
   unfolding in_fset minus_fset
   by blast
@@ -731,7 +731,7 @@
   shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
   by (descending) (simp add: sub_list_def)
 
-lemma not_psubset_fset_fnil: 
+lemma not_psubset_empty_fset: 
   shows "\<not> xs |\<subset>| {||}"
   by (metis fset_simps(1) psubset_fset not_psubset_empty)
 
@@ -747,7 +747,7 @@
   shows "fset (map_fset f S) = f ` (fset S)"
   by (descending) (simp)
 
-lemma inj_map_fset_eq_iff:
+lemma nj_map_fset_cong:
   shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T"
   by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
 
@@ -762,7 +762,7 @@
   shows "card_fset xs = card (fset xs)"
   by (lifting card_list_def)
 
-lemma card_insert_fset_if [simp]:
+lemma card_insert_fset_iff [simp]:
   shows "card_fset (insert_fset x S) = (if x |\<in>| S then card_fset S else Suc (card_fset S))"
   by (descending) (auto simp add: card_list_def memb_def insert_absorb)
 
@@ -772,7 +772,7 @@
 
 lemma card_empty_fset[simp]:
   shows "card_fset {||} = 0"
-  by (simp add: card_fset_0)
+  by (simp add: card_fset)
 
 lemma card_fset_1:
   shows "card_fset S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
@@ -784,7 +784,7 @@
   
 lemma card_notin_fset:
   shows "(x |\<notin>| S) = (card_fset (insert_fset x S) = Suc (card_fset S))"
-  by (descending) (auto simp add: memb_def card_list_def insert_absorb)
+  by simp
 
 lemma card_fset_Suc: 
   shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n"
@@ -792,19 +792,15 @@
   apply(auto simp add: card_list_def memb_def dest!: card_eq_SucD)
   by (metis Diff_insert_absorb set_removeAll)
 
-lemma card_rsemove_fset:
+lemma card_remove_fset_iff [simp]:
   shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)"
   by (descending) (simp add: card_list_def memb_def)
 
-lemma card_Suc_in_fset: 
-  shows "card_fset A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
-  apply(descending)
-  apply(simp add: card_list_def memb_def)
-  apply(drule card_eq_SucD)
-  apply(auto)
-  done
+lemma card_Suc_exists_in_fset: 
+  shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
+  by (drule card_fset_Suc) (auto)
 
-lemma in_fset_card_fset_not_0: 
+lemma in_card_fset_not_0: 
   shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
   by (descending) (auto simp add: card_list_def memb_def)
 
@@ -839,12 +835,12 @@
   unfolding card_fset in_fset remove_fset 
   by (rule card_Diff1_less[OF finite_fset])
 
-lemma card_rsemove_fset_less2: 
+lemma card_remove_fset_less2: 
   shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> card_fset (remove_fset y (remove_fset x xs)) < card_fset xs"
   unfolding card_fset remove_fset in_fset
   by (rule card_Diff2_less[OF finite_fset])
 
-lemma card_rsemove_fset_le1: 
+lemma card_remove_fset_le1: 
   shows "card_fset (remove_fset x xs) \<le> card_fset xs"
   unfolding remove_fset card_fset
   by (rule card_Diff1_le[OF finite_fset])
@@ -873,7 +869,7 @@
   unfolding subset_fset card_fset minus_fset
   by (rule card_Diff_subset[OF finite_fset])
 
-lemma card_minus_subset_inter_fset:
+lemma card_minus_fset:
   shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)"
   unfolding inter_fset card_fset minus_fset
   by (rule card_Diff_subset_Int) (simp)
@@ -881,15 +877,15 @@
 
 subsection {* concat_fset *}
 
-lemma concat_empty_fset:
+lemma concat_empty_fset [simp]:
   shows "concat_fset {||} = {||}"
   by (lifting concat.simps(1))
 
-lemma concat_insert_fset:
+lemma concat_insert_fset [simp]:
   shows "concat_fset (insert_fset x S) = x |\<union>| concat_fset S"
   by (lifting concat.simps(2))
 
-lemma concat_inter_fset:
+lemma concat_inter_fset [simp]:
   shows "concat_fset (xs |\<union>| ys) = concat_fset xs |\<union>| concat_fset ys"
   by (lifting concat_append)