nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:135ac0fb2686
+:d7269488c4b5
 lemma map_prs [quot_preserve]:
 shows "(abs_fset \<circ> map f) [] = abs_fset []"
 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)
 lemma list_all2_app_l:
 assumes a: "reflp R"
 section {* Lifted theorems *}
+subsection {* fset *}
+lemma fset_simps [simp]:
+"fset {||} = ({} :: 'a set)"
+"fset (insert_fset (x :: 'a) S) = insert x (fset S)"
+by (lifting set.simps)
+lemma finite_fset [simp]:
+shows "finite (fset S)"
+by (descending) (simp)
+lemma fset_cong:
+shows "fset S = fset T \<longleftrightarrow> S = T"
+by (descending) (simp)
+lemma filter_fset [simp]:
+shows "fset (filter_fset P xs) = P \<inter> fset xs"
+by (descending) (auto simp add: mem_def)
+lemma remove_fset [simp]:
+shows "fset (remove_fset x xs) = fset xs - {x}"
+by (descending) (simp)
+lemma inter_fset [simp]:
+shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
+by (descending) (auto simp add: inter_list_def)
+lemma union_fset [simp]:
+shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
+by (lifting set_append)
+lemma minus_fset [simp]:
+shows "fset (xs - ys) = fset xs - fset ys"
+by (descending) (auto simp add: diff_list_def)
 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)
+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)
 by (descending) (simp add: memb_def)
 subsection {* insert_fset *}
-lemma in_insert_fset_iff[simp]:
+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)+
+by simp_all
-lemma insert_absorb_fset[simp]:
+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"
 lemma singleton_fset_eq[simp]:
 shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
 by (descending) (auto)
-(* FIXME: is this in any case a useful lemma *)
+(* 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 {* fset *}
-lemma fset_simps [simp]:
-"fset {||} = ({} :: 'a set)"
-"fset (insert_fset (x :: 'a) S) = insert x (fset S)"
-by (lifting set.simps)
-lemma finite_fset [simp]:
-shows "finite (fset S)"
-by (descending) (simp)
-lemma fset_cong:
-shows "fset S = fset T \<longleftrightarrow> S = T"
-by (descending) (simp)
-lemma filter_fset [simp]:
-shows "fset (filter_fset P xs) = P \<inter> fset xs"
-by (descending) (auto simp add: mem_def)
-lemma remove_fset [simp]:
-shows "fset (remove_fset x xs) = fset xs - {x}"
-by (descending) (simp)
-lemma inter_fset [simp]:
-shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
-by (descending) (auto simp add: inter_list_def)
-lemma union_fset [simp]:
-shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
-by (lifting set_append)
-lemma minus_fset [simp]:
-shows "fset (xs - ys) = fset xs - fset ys"
-by (descending) (auto simp add: diff_list_def)
 subsection {* union_fset *}
 lemmas [simp] =
 sup_bot_left[where 'a="'a fset", standard]
 sup_bot_right[where 'a="'a fset", standard]
 lemma minus_insert_notin_fset[simp]:
 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
 lemma subset_empty_fset:
 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)
 subsection {* map_fset *}
 lemma map_fset_image [simp]:
 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)
 lemma map_union_fset:
 shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
 lemma card_fset:
 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)
 lemma card_fset_0[simp]:
 shows "card_fset S = 0 \<longleftrightarrow> S = {||}"
 by (descending) (simp add: card_list_def)
 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|})"
 by (descending) (auto simp add: card_list_def card_Suc_eq)
 shows "x \<in> fset S \<Longrightarrow> 0 < card_fset S"
 by (descending) (auto simp add: card_list_def card_gt_0_iff)
 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"
 apply(descending)
 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:
+lemma card_Suc_exists_in_fset:
-shows "card_fset A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
+shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
-apply(descending)
+by (drule card_fset_Suc) (auto)
-apply(simp add: card_list_def memb_def)
-apply(drule card_eq_SucD)
+lemma in_card_fset_not_0:
-apply(auto)
-done
-lemma in_fset_card_fset_not_0:
 shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
 by (descending) (auto simp add: card_list_def memb_def)
 lemma card_fset_mono:
 shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset xs \<le> card_fset ys"
 lemma card_remove_fset_less1:
 shows "x |\<in>| xs \<Longrightarrow> card_fset (remove_fset x xs) < card_fset xs"
 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])
 lemma card_psubset_fset:
 shows "card_fset (A - B) = card_fset A - card_fset B"
 using assms
 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)
 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)
 subsection {* filter_fset *}

changeset 2541	d7269488c4b5
parent 2540	135ac0fb2686
child 2542	1f5c8e85c41f