--- 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))"