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