--- a/Nominal/FSet.thy	Wed Apr 14 07:34:03 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 07:57:55 2010 +0200
@@ -131,13 +131,11 @@
 
 lemma fcard_raw_not_memb:
   fixes x :: "'a"
-  fixes xs :: "'a list"
   shows "\<not>(memb x xs) \<longleftrightarrow> (fcard_raw (x # xs) = Suc (fcard_raw xs))"
   by auto
 
 lemma fcard_raw_suc:
   fixes xs :: "'a list"
-  fixes n :: "nat"
   assumes c: "fcard_raw xs = Suc n"
   shows "\<exists>x ys. \<not>(memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
   unfolding memb_def
@@ -230,18 +228,9 @@
 
 text {* raw section *}
 
-lemma map_rsp_aux:
-  assumes a: "a \<approx> b"
-  shows "map f a \<approx> map f b"
-  using a
-  apply(induct a arbitrary: b)
-  apply(auto)
-  apply(metis rev_image_eqI)
-  done
-
 lemma map_rsp[quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) map map"
-  by (auto simp add: map_rsp_aux)
+  by auto
 
 lemma cons_left_comm:
   "x # y # xs \<approx> y # x # xs"
@@ -256,14 +245,14 @@
   by simp
 
 lemma fset_raw_strong_cases:
-  "(xs = []) \<or> (\<exists>x ys. ((x \<notin> set ys) \<and> (xs \<approx> x # ys)))"
+  "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
   apply (induct xs)
   apply (simp)
   apply (rule disjI2)
   apply (erule disjE)
   apply (rule_tac x="a" in exI)
   apply (rule_tac x="[]" in exI)
-  apply (simp)
+  apply (simp add: memb_def)
   apply (erule exE)+
   apply (case_tac "x = a")
   apply (rule_tac x="a" in exI)
@@ -271,7 +260,7 @@
   apply (simp)
   apply (rule_tac x="x" in exI)
   apply (rule_tac x="a # ys" in exI)
-  apply (auto)
+  apply (auto simp add: memb_def)
   done
 
 fun
@@ -386,8 +375,8 @@
   by (induct l) (simp_all add: not_memb_nil)
 
 lemma memb_finter_raw:
-  "memb e (finter_raw l r) = (memb e l \<and> memb e r)"
-  apply (induct l)
+  "memb x (finter_raw xs ys) = (memb x xs \<and> memb x ys)"
+  apply (induct xs)
   apply (simp add: not_memb_nil)
   apply (simp add: finter_raw.simps)
   apply (simp add: memb_cons_iff)
@@ -419,12 +408,12 @@
 is "finter_raw"
 
 lemma funion_sym_pre:
-  "a @ b \<approx> b @ a"
+  "xs @ ys \<approx> ys @ xs"
   by auto
 
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  by (auto)
+  by auto
 
 lemma set_cong: 
   shows "(set x = set y) = (x \<approx> y)"
@@ -467,11 +456,11 @@
   by (lifting nil_not_cons)
 
 lemma finsert_left_comm:
-  "finsert a (finsert b S) = finsert b (finsert a S)"
+  "finsert x (finsert y S) = finsert y (finsert x S)"
   by (lifting cons_left_comm)
 
 lemma finsert_left_idem:
-  "finsert a (finsert a S) = finsert a S"
+  "finsert x (finsert x S) = finsert x S"
   by (lifting cons_left_idem)
 
 lemma fsingleton_eq[simp]:
@@ -485,16 +474,18 @@
   "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
   by (lifting set.simps)
 
+thm memb_def[symmetric, THEN meta_eq_to_obj_eq]
+
 lemma in_fset_to_set:
-  "x \<in> fset_to_set xs \<equiv> x |\<in>| xs"
+  "x \<in> fset_to_set S \<equiv> x |\<in>| S"
   by (lifting memb_def[symmetric])
 
 lemma none_fin_fempty:
-  "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"
+  "(\<forall>x. x \<notin> fset_to_set S) = (S = {||})"
   by (lifting none_mem_nil)
 
 lemma fset_cong:
-  "(fset_to_set x = fset_to_set y) = (x = y)"
+  "(fset_to_set S = fset_to_set T) = (S = T)"
   by (lifting set_cong)
 
 text {* fcard *}
@@ -507,46 +498,46 @@
   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
   by (lifting fcard_raw_cons)
 
-lemma fcard_0: "(fcard a = 0) = (a = {||})"
+lemma fcard_0: "(fcard S = 0) = (S = {||})"
   by (lifting fcard_raw_0)
 
 lemma fcard_1:
-  fixes xs::"'b fset"
-  shows "(fcard xs = 1) = (\<exists>x. xs = {|x|})"
+  fixes S::"'b fset"
+  shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
   by (lifting fcard_raw_1)
 
-lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"
+lemma fcard_gt_0: "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
   by (lifting fcard_raw_gt_0)
 
-lemma fcard_not_fin: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"
+lemma fcard_not_fin: "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
   by (lifting fcard_raw_not_memb)
 
-lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys \<and> fcard ys = n"
+lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
   by (lifting fcard_raw_suc)
 
 lemma fcard_delete:
-  "fcard (fdelete xs y) = (if y |\<in>| xs then fcard xs - 1 else fcard xs)"
+  "fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"
   by (lifting fcard_raw_delete)
 
 text {* funion *}
 
 lemma funion_simps[simp]:
-  "{||} |\<union>| ys = ys"
-  "finsert x xs |\<union>| ys = finsert x (xs |\<union>| ys)"
+  "{||} |\<union>| S = S"
+  "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
   by (lifting append.simps)
 
 lemma funion_sym:
-  "a |\<union>| b = b |\<union>| a"
+  "S |\<union>| T = T |\<union>| S"
   by (lifting funion_sym_pre)
 
 lemma funion_assoc:
- "x |\<union>| xa |\<union>| xb = x |\<union>| (xa |\<union>| xb)"
+ "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
   by (lifting append_assoc)
 
 section {* Induction and Cases rules for finite sets *}
 
 lemma fset_strong_cases:
-  "X = {||} \<or> (\<exists>a Y. a \<notin> fset_to_set Y \<and> X = finsert a Y)"
+  "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
   by (lifting fset_raw_strong_cases)
 
 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
@@ -596,24 +587,22 @@
 
 lemma fmap_simps[simp]:
   "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
-  "fmap f (finsert x xs) = finsert (f x) (fmap f xs)"
+  "fmap f (finsert x S) = finsert (f x) (fmap f S)"
   by (lifting map.simps)
 
 lemma fmap_set_image:
-  "fset_to_set (fmap f fs) = f ` (fset_to_set fs)"
-  apply (induct fs)
-  apply (simp_all)
-done
+  "fset_to_set (fmap f S) = f ` (fset_to_set S)"
+  by (induct S) (simp_all)
 
 lemma inj_fmap_eq_iff:
-  "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
+  "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
   by (lifting inj_map_eq_iff)
 
-lemma fmap_funion: "fmap f (a |\<union>| b) = fmap f a |\<union>| fmap f b"
+lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
   by (lifting map_append)
 
 lemma fin_funion:
-  "(e |\<in>| l |\<union>| r) = (e |\<in>| l \<or> e |\<in>| r)"
+  "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
   by (lifting memb_append)
 
 text {* ffold *}
@@ -631,37 +620,40 @@
 
 text {* fdelete *}
 
-lemma fin_fdelete: "(x |\<in>| fdelete A a) = (x |\<in>| A \<and> x \<noteq> a)"
+lemma fin_fdelete: 
+  shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
   by (lifting memb_delete_raw)
 
-lemma fin_fdelete_ident: "a |\<notin>| fdelete A a"
+lemma fin_fdelete_ident: 
+  shows "x |\<notin>| fdelete S x"
   by (lifting memb_delete_raw_ident)
 
-lemma not_memb_fdelete_ident: "b |\<notin>| A \<Longrightarrow> fdelete A b = A"
+lemma not_memb_fdelete_ident: 
+  shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
   by (lifting not_memb_delete_raw_ident)
 
 lemma fset_fdelete_cases:
-  "X = {||} \<or> (\<exists>a. a |\<in>| X \<and> X = finsert a (fdelete X a))"
+  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
   by (lifting fset_raw_delete_raw_cases)
 
 text {* inter *}
 
-lemma finter_empty_l: "({||} |\<inter>| r) = {||}"
+lemma finter_empty_l: "({||} |\<inter>| S) = {||}"
   by (lifting finter_raw.simps(1))
 
-lemma finter_empty_r: "(l |\<inter>| {||}) = {||}"
+lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"
   by (lifting finter_raw_empty)
 
 lemma finter_finsert:
-  "(finsert h t |\<inter>| l) = (if h |\<in>| l then finsert h (t |\<inter>| l) else t |\<inter>| l)"
+  "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
   by (lifting finter_raw.simps(2))
 
 lemma fin_finter:
-  "(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)"
+  "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
   by (lifting memb_finter_raw)
 
 lemma expand_fset_eq:
-  "(xs = ys) = (\<forall>x. (x |\<in>| xs) = (x |\<in>| ys))"
+  "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])