# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1287050992 -3600
# Node ID c848f93807b9572d724c93b49fdf1bf3f1ec2ca6
# Parent  693562f03eeed1778fb69375dc18fde0f36b7095
deleted some unused lemmas

diff -r 693562f03eee -r c848f93807b9 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Thu Oct 14 04:14:22 2010 +0100
+++ b/Nominal/FSet.thy	Thu Oct 14 11:09:52 2010 +0100
@@ -91,11 +91,6 @@
   shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
   by (fact list_quotient[OF Quotient_fset])
 
-(*
-lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys"
-  by (rule eq_reflection) auto
-*)
-
 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
   unfolding list_eq.simps
   by (simp only: set_map)
@@ -155,19 +150,23 @@
   qed
 qed
 
+
+lemma set_finter_raw[simp]:
+  "set (finter_raw xs ys) = set xs \<inter> set ys"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma set_fminus_raw[simp]: 
+  "set (fminus_raw xs ys) = (set xs - set ys)"
+  by (induct ys arbitrary: xs) (auto)
+
+
 text {* Respectfullness *}
 
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
   by (simp)
 
-(*
-lemma append_rsp_unfolded:
-  "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"
-  by auto
-*)
-
-lemma [quot_respect]:
+lemma sub_list_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
   by (auto simp add: sub_list_def)
 
@@ -176,7 +175,7 @@
   by (auto simp add: memb_def)
 
 lemma nil_rsp[quot_respect]:
-  shows "[] \<approx> []"
+  shows "(op \<approx>) Nil Nil"
   by simp
 
 lemma cons_rsp[quot_respect]:
@@ -195,6 +194,24 @@
   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
   by auto
 
+lemma finter_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+  by simp
+
+lemma removeAll_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
+  by simp
+
+lemma fminus_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+  by simp
+
+lemma fcard_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
+  by (simp add: fcard_raw_def)
+
+
+
 lemma not_memb_nil:
   shows "\<not> memb x []"
   by (simp add: memb_def)
@@ -203,36 +220,6 @@
   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
   by (induct xs) (auto simp add: memb_def)
 
-lemma set_finter_raw[simp]:
-  "set (finter_raw xs ys) = set xs \<inter> set ys"
-  by (induct xs) (auto simp add: memb_def)
-
-lemma [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
-  by (simp)
-
-(*
-lemma memb_removeAll:
-  "memb x (removeAll y xs) \<longleftrightarrow> memb x xs \<and> x \<noteq> y"
-  by (induct xs arbitrary: x y) (auto simp add: memb_def)
-*)
-
-lemma [quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
-  by (simp)
-
-lemma set_fminus_raw[simp]: 
-  "set (fminus_raw xs ys) = (set xs - set ys)"
-  by (induct ys arbitrary: xs) (auto)
-
-lemma [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
-  by simp
-
-lemma fcard_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
-  by (simp add: fcard_raw_def)
-
 lemma memb_absorb:
   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
   by (induct xs) (auto simp add: memb_def)
@@ -241,9 +228,6 @@
   "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
   by (simp add: memb_def)
 
-lemma not_memb_removeAll_ident:
-  shows "\<not> memb x xs \<Longrightarrow> removeAll x xs = xs"
-  by (induct xs) (auto simp add: memb_def)
 
 lemma memb_commute_ffold_raw:
   "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
@@ -269,7 +253,7 @@
   apply(blast)
   by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
 
-lemma [quot_respect]:
+lemma ffold_raw_rsp[quot_respect]:
   shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
   unfolding fun_rel_def
   apply(auto intro: ffold_raw_rsp_pre)
@@ -737,9 +721,6 @@
 
 section {* deletion *}
 
-lemma memb_removeAll_ident:
-  shows "\<not> memb x (removeAll x xs)"
-  by (induct xs) (auto simp add: memb_def)
 
 lemma fset_raw_removeAll_cases:
   "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # removeAll x xs)"
@@ -790,7 +771,7 @@
   apply (auto simp add: memb_def)[2]
   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
-  apply (auto simp add: list_eq2_refl not_memb_removeAll_ident)
+  apply (auto simp add: list_eq2_refl memb_def)
   done
 
 lemma memb_delete_list_eq2:
@@ -799,10 +780,6 @@
   using a cons_delete_list_eq2[of e r]
   by simp
 
-lemma removeAll_rsp:
-  "xs \<approx> ys \<Longrightarrow> removeAll x xs \<approx> removeAll x ys"
-  by (simp add: memb_def[symmetric])
-
 lemma list_eq2_equiv:
   "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
 proof
@@ -833,7 +810,7 @@
       then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
 	unfolding memb_def by auto
       have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
-      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp[OF b] by simp
+      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
       have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
       then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
       have i: "list_eq2 l (a # removeAll a l)"
@@ -1123,13 +1100,13 @@
   shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
   by (descending) (simp add: memb_def)
 
-lemma fin_fdelete_ident:
+lemma fnotin_fdelete:
   shows "x |\<notin>| fdelete x S"
-  by (lifting memb_removeAll_ident)
+  by (descending) (simp add: memb_def)
 
-lemma not_memb_fdelete_ident:
+lemma fnotin_fdelete_ident:
   shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
-  by (lifting not_memb_removeAll_ident)
+  by (descending) (simp add: memb_def)
 
 lemma fset_fdelete_cases:
   shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"