nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:9568f9f31822
+:72b777cc5479
-(*  Title:      Quotient.thy
+(*  Title:      HOL/Quotient_Examples/FSet.thy
-Author:     Cezary Kaliszyk
+Author:     Cezary Kaliszyk, TU Munich
-Author:     Christian Urban
+Author:     Christian Urban, TU Munich
-provides a reasoning infrastructure for the type of finite sets
+A reasoning infrastructure for the type of finite sets.
 *)
 theory FSet
-imports Quotient Quotient_List List
+imports Quotient_List
 begin
 text {* Definiton of List relation and the quotient type *}
 fun
 where
 "finter_raw [] l = []"
 | "finter_raw (h # t) l =
 (if memb h l then h # (finter_raw t l) else finter_raw t l)"
-fun
+primrec
 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 where
 "delete_raw [] x = []"
-| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
+| "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))"
+primrec
+fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+"fminus_raw l [] = l"
+| "fminus_raw l (h # t) = fminus_raw (delete_raw l h) t"
 definition
 rsp_fold
 where
 "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 primrec
 ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 where
 "ffold_raw f z [] = z"
-| "ffold_raw f z (a # A) =
+| "ffold_raw f z (a # xs) =
 (if (rsp_fold f) then
-if memb a A then ffold_raw f z A
+if memb a xs then ffold_raw f z xs
-else f a (ffold_raw f z A)
+else f a (ffold_raw f z xs)
 else z)"
 text {* Composition Quotient *}
 lemma list_rel_refl:
 by (rule list_rel_refl) (metis equivp_def fset_equivp)
 lemma compose_list_refl:
 shows "(list_rel op \<approx> OOO op \<approx>) r r"
 proof
-show c: "list_rel op \<approx> r r" by (rule list_rel_refl)
+have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
-have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+show "list_rel op \<approx> r r" by (rule list_rel_refl)
-show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
+with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
 qed
 lemma Quotient_fset_list:
 shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
 by (fact list_quotient[OF Quotient_fset])
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
+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 set_in_eq)
 proof (intro iffI conjI)
 show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
 show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
 next
 assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
-then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
+then have b: "map abs_fset r \<approx> map abs_fset s"
+proof (elim pred_compE)
 fix b ba
 assume c: "list_rel op \<approx> r b"
 assume d: "b \<approx> ba"
 assume e: "list_rel op \<approx> ba s"
 have f: "map abs_fset r = map abs_fset b"
 lemma [quot_respect]:
 "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
 by (simp add: memb_def[symmetric] memb_delete_raw)
+lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \<and> \<not> memb x ys)"
+by (induct ys arbitrary: xs)
+(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+lemma [quot_respect]:
+"(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+by (simp add: memb_def[symmetric] fminus_raw_memb)
 lemma fcard_raw_gt_0:
 assumes a: "x \<in> set xs"
 shows "0 < fcard_raw xs"
 using a by (induct xs) (auto simp add: memb_def)
 lemma fcard_raw_rsp_aux:
 assumes a: "xs \<approx> ys"
 shows "fcard_raw xs = fcard_raw ys"
 using a
-apply (induct xs arbitrary: ys)
+proof (induct xs arbitrary: ys)
-apply (auto simp add: memb_def)
+case Nil
-apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
+show ?case using Nil.prems by simp
-apply (auto)
+next
-apply (drule_tac x="x" in spec)
+case (Cons a xs)
-apply (blast)
+have a: "a # xs \<approx> ys" by fact
-apply (drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
+have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact
-apply (simp add: fcard_raw_delete_one memb_def)
+show ?case proof (cases "a \<in> set xs")
-apply (case_tac "a \<in> set ys")
+assume c: "a \<in> set xs"
-apply (simp only: if_True)
+have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)"
-apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
+proof (intro allI iffI)
-apply (drule Suc_pred'[OF fcard_raw_gt_0])
+fix x
-apply (auto)
+assume "x \<in> set xs"
-done
+then show "x \<in> set ys" using a by auto
+next
+fix x
+assume d: "x \<in> set ys"
+have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp
+show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast
+qed
+then show ?thesis using b c by (simp add: memb_def)
+next
+assume c: "a \<notin> set xs"
+have d: "xs \<approx> [x\<leftarrow>ys . x \<noteq> a] \<Longrightarrow> fcard_raw xs = fcard_raw [x\<leftarrow>ys . x \<noteq> a]" using b by simp
+have "Suc (fcard_raw xs) = fcard_raw ys"
+proof (cases "a \<in> set ys")
+assume e: "a \<in> set ys"
+have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c
+by (auto simp add: fcard_raw_delete_one)
+have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e)
+then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def)
+next
+case False then show ?thesis using a c d by auto
+qed
+then show ?thesis using a c d by (simp add: memb_def)
+qed
+qed
 lemma fcard_raw_rsp[quot_respect]:
 shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
 by (simp add: fcard_raw_rsp_aux)
 shows "\<exists>x\<in>set y. xa \<in> set x"
 proof -
 obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
 have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
 then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
-have j: "ya \<in> set y'" using b h by simp
+have "ya \<in> set y'" using b h by simp
-have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c])
+then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element)
 then show ?thesis using f i by auto
 qed
 lemma [quot_respect]:
 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 qed
 qed
 then show "concat a \<approx> concat b" by simp
 qed
+lemma [quot_respect]:
+"((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+by auto
 text {* Distributive lattice with bot *}
 lemma sub_list_not_eq:
 "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
 by (auto simp add: sub_list_def)
 lemma append_inter_distrib:
 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
 apply (induct x)
 apply (simp_all add: memb_def)
 apply (simp add: memb_def[symmetric] memb_finter_raw)
-by (auto simp add: memb_def)
+apply (auto simp add: memb_def)
+done
-instantiation fset :: (type) "{bot,distrib_lattice}"
+instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
 begin
 quotient_definition
 "bot :: 'a fset" is "[] :: 'a list"
 "sup  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
 is
 "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 abbreviation
-funion  (infixl "|\<union>|" 65)
+funion (infixl "|\<union>|" 65)
 where
 "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
 quotient_definition
-"inf  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+"inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
 is
 "finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 abbreviation
 finter (infixl "|\<inter>|" 65)
 where
 "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
+quotient_definition
+"minus \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+is
+"fminus_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 instance
 proof
 fix x y z :: "'a fset"
 show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
 abbreviation
 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
 where
 "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 section {* Other constants on the Quotient Type *}
 quotient_definition
 "fcard :: 'a fset \<Rightarrow> nat"
 is
 "fcard_raw"
 quotient_definition
 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 is
 "map"
 quotient_definition
 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
 is "delete_raw"
 quotient_definition
 "fset_to_set :: 'a fset \<Rightarrow> 'a set"
 is "set"
 quotient_definition
 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
 is "ffold_raw"
 quotient_definition
 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
 is
 "concat"
+quotient_definition
+"ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+"filter"
 text {* Compositional Respectfullness and Preservation *}
 lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
 by (fact compose_list_refl)
 lemma sub_list_cons:
 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
 by (auto simp add: memb_def sub_list_def)
+lemma fminus_raw_red: "fminus_raw (x # xs) ys = (if memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
+by (induct ys arbitrary: xs x)
+(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
 text {* Cardinality of finite sets *}
 lemma fcard_raw_0:
 shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
 by (induct xs) (auto simp add: memb_def)
 lemma cons_left_idem:
 "x # x # xs \<approx> x # xs"
 by auto
 lemma fset_raw_strong_cases:
-"(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
+obtains "xs = []"
-apply (induct xs)
+| x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
-apply (simp)
+proof (induct xs arbitrary: x ys)
-apply (rule disjI2)
+case Nil
-apply (erule disjE)
+then show thesis by simp
-apply (rule_tac x="a" in exI)
+next
-apply (rule_tac x="[]" in exI)
+case (Cons a xs)
-apply (simp add: memb_def)
+have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
-apply (erule exE)+
+have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
-apply (case_tac "x = a")
+have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
-apply (rule_tac x="a" in exI)
+have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
-apply (rule_tac x="ys" in exI)
+proof -
-apply (simp)
+fix x :: 'a
-apply (rule_tac x="x" in exI)
+fix ys :: "'a list"
-apply (rule_tac x="a # ys" in exI)
+assume d:"\<not> memb x ys"
-apply (auto simp add: memb_def)
+assume e:"xs \<approx> x # ys"
-done
+show thesis
+proof (cases "x = a")
+assume h: "x = a"
+then have f: "\<not> memb a ys" using d by simp
+have g: "a # xs \<approx> a # ys" using e h by auto
+show thesis using b f g by simp
+next
+assume h: "x \<noteq> a"
+then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+have g: "a # xs \<approx> x # (a # ys)" using e h by auto
+show thesis using b f g by simp
+qed
+qed
+then show thesis using a c by blast
+qed
 section {* deletion *}
 lemma memb_delete_raw_ident:
 shows "\<not> memb x (delete_raw xs x)"
 lemma finter_raw_empty:
 "finter_raw l [] = []"
 by (induct l) (simp_all add: not_memb_nil)
 lemma set_cong:
-shows "(set x = set y) = (x \<approx> y)"
+shows "(x \<approx> y) = (set x = set y)"
 by auto
 lemma inj_map_eq_iff:
 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
 then show ?case using z list_eq2_refl by simp
 next
 case (Suc m)
 have b: "l \<approx> r" by fact
 have d: "fcard_raw l = Suc m" by fact
-have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb)
 then obtain a where e: "memb a l" by auto
 then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
 have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
 have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
-have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
-have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5))
 have i: "list_eq2 l (a # delete_raw l a)"
 by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
 have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
 then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
 qed
 }
 then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
 qed
+text {* Set *}
+lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
+by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
+by (auto simp add: sub_list_set)
+lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
+by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+lemma memb_set: "memb x xs = (x \<in> set xs)"
+by (simp only: memb_def)
+lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
+by (induct xs, simp)
+(metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
+lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
+by (induct xs) auto
+lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
+by (induct xs) (simp_all add: memb_def)
+lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
+by (induct ys arbitrary: xs)
+(simp_all add: fminus_raw.simps delete_raw_set, blast)
+text {* Raw theorems of ffilter *}
+lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+unfolding sub_list_def memb_def by auto
+lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+unfolding memb_def by auto
 text {* Lifted theorems *}
 lemma not_fin_fnil: "x |\<notin>| {||}"
 by (lifting not_memb_nil)
 lemma none_fin_fempty:
 "(\<forall>x. x |\<notin>| S) = (S = {||})"
 by (lifting none_memb_nil)
 lemma fset_cong:
-"(fset_to_set S = fset_to_set T) = (S = T)"
+"(S = T) = (fset_to_set S = fset_to_set T)"
 by (lifting set_cong)
 text {* fcard *}
 lemma fcard_fempty [simp]:
 lemma fcard_1:
 shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
 by (lifting fcard_raw_1)
 lemma fcard_gt_0:
 shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
 by (lifting fcard_raw_gt_0)
 lemma fcard_not_fin:
 shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
 by (lifting fcard_raw_not_memb)
 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 fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
 by (lifting memb_card_not_0)
 text {* funion *}
-lemma funion_simps[simp]:
+lemmas [simp] =
-shows "{||} |\<union>| S = S"
+sup_bot_left[where 'a="'a fset", standard]
-and   "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+sup_bot_right[where 'a="'a fset", standard]
-by (lifting append.simps)
+lemma funion_finsert[simp]:
-lemma funion_empty[simp]:
+shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
-shows "S |\<union>| {||} = S"
+by (lifting append.simps(2))
-by (lifting append_Nil2)
 lemma singleton_union_left:
 "{|a|} |\<union>| S = finsert a S"
 by simp
 by (subst sup.commute) simp
 section {* Induction and Cases rules for finite sets *}
 lemma fset_strong_cases:
-"S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
+obtains "xs = {||}"
+| x ys where "x |\<notin>| ys" and "xs = finsert x ys"
 by (lifting fset_raw_strong_cases)
 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
 shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (lifting list.exhaust)
 lemma fset_induct_weak[case_names fempty finsert]:
 shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
 by (lifting list.induct)
 lemma fset_induct[case_names fempty finsert, induct type: fset]:
 assumes prem1: "P {||}"
 and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
 shows "P S"
 proof(induct S rule: fset_induct_weak)
 case fempty
 show "P {||}" by (rule prem1)
 apply simp_all
 apply (induct_tac xa rule: fset_induct)
 apply simp_all
 done
+lemma fset_fcard_induct:
+assumes a: "P {||}"
+and     b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
+shows "P zs"
+proof (induct zs)
+show "P {||}" by (rule a)
+next
+fix x :: 'a and zs :: "'a fset"
+assume h: "P zs"
+assume "x |\<notin>| zs"
+then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
+then show "P (finsert x zs)" using b h by simp
+qed
 text {* fmap *}
 lemma fmap_simps[simp]:
 "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
 "fmap f (finsert x S) = finsert (f x) (fmap f S)"
 by (lifting map.simps)
 lemma fmap_set_image:
 "fset_to_set (fmap f S) = f ` (fset_to_set S)"
-by (induct S) (simp_all)
+by (induct S) simp_all
 lemma inj_fmap_eq_iff:
 "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
 by (lifting inj_map_eq_iff)
 lemma fin_funion:
 "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
 by (lifting memb_append)
+text {* to_set *}
+lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+by (lifting memb_set)
+lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+by (simp add: fin_set)
+lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+by (lifting fcard_raw_set)
+lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+by (lifting sub_list_set)
+lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+unfolding less_fset by (lifting sub_list_neq_set)
+lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+by (lifting filter_set)
+lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+by (lifting delete_raw_set)
+lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+by (lifting inter_raw_set)
+lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+by (lifting set_append)
+lemma fminus_set: "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
+by (lifting fminus_raw_set)
+lemmas fset_to_set_trans =
+fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
+inter_set union_set ffilter_set fset_to_set_simps
+fset_cong fdelete_set fmap_set_image fminus_set
 text {* ffold *}
 lemma ffold_nil: "ffold f z {||} = z"
 by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
 "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete b h))"
 by (lifting memb_commute_ffold_raw)
 text {* fdelete *}
 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:
 shows "x |\<notin>| fdelete S x"
 by (lifting memb_delete_raw_ident)
 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:
 shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
 by (lifting sub_list_def[simplified memb_def[symmetric]])
 lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
 by (rule meta_eq_to_obj_eq)
 (lifting sub_list_def[simplified memb_def[symmetric]])
+lemma fminus_fin: "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+by (lifting fminus_raw_memb)
+lemma fminus_red: "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+by (lifting fminus_raw_red)
+lemma fminus_red_fin[simp]: "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+by (simp add: fminus_red)
+lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+by (simp add: fminus_red)
 lemma expand_fset_eq:
 "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
 by (lifting list_eq.simps[simplified memb_def[symmetric]])
 by (lifting concat.simps(2))
 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
 by (lifting concat_append)
+text {* ffilter *}
+lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+by (lifting sub_list_filter)
+lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+by (lifting list_eq_filter)
+lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+section {* lemmas transferred from Finite_Set theory *}
+text {* finiteness for finite sets holds *}
+lemma finite_fset: "finite (fset_to_set S)"
+by (induct S) auto
+lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+unfolding fset_to_set_trans
+by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
+lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+unfolding fset_to_set_trans
+by (rule subset_empty)
+lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+unfolding fset_to_set_trans
+by (rule not_psubset_empty)
+lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+unfolding fset_to_set_trans
+by (rule card_mono[OF finite_fset])
+lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+unfolding fset_to_set_trans
+by (rule card_seteq[OF finite_fset])
+lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+unfolding fset_to_set_trans
+by (rule psubset_card_mono[OF finite_fset])
+lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+unfolding fset_to_set_trans
+by (rule card_Un_Int[OF finite_fset finite_fset])
+lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+unfolding fset_to_set_trans
+by (rule card_Un_disjoint[OF finite_fset finite_fset])
+lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+unfolding fset_to_set_trans
+by (rule card_Diff1_less[OF finite_fset])
+lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+unfolding fset_to_set_trans
+by (rule card_Diff2_less[OF finite_fset])
+lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+unfolding fset_to_set_trans
+by (rule card_Diff1_le[OF finite_fset])
+lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+unfolding fset_to_set_trans
+by (rule card_psubset[OF finite_fset])
+lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+unfolding fset_to_set_trans
+by (rule card_image_le[OF finite_fset])
+lemma fin_fminus_fnotin: "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+unfolding fset_to_set_trans
+by blast
+lemma fin_fnotin_fminus: "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+unfolding fset_to_set_trans
+by blast
+lemma fin_mdef: "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+unfolding fset_to_set_trans
+by blast
+lemma fcard_fminus_finsert[simp]:
+assumes "a |\<in>| A" and "a |\<notin>| B"
+shows "fcard(A - finsert a B) = fcard(A - B) - 1"
+using assms unfolding fset_to_set_trans
+by (rule card_Diff_insert[OF finite_fset])
+lemma fcard_fminus_fsubset:
+assumes "B |\<subseteq>| A"
+shows "fcard (A - B) = fcard A - fcard B"
+using assms unfolding fset_to_set_trans
+by (rule card_Diff_subset[OF finite_fset])
+lemma fcard_fminus_subset_finter:
+"fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
+unfolding fset_to_set_trans
+by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
 ML {*
-fun dest_fsetT (Type ("FSet.fset", [T])) = T
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 *}
 no_notation
 list_eq (infix "\<approx>" 50)

changeset 2084	72b777cc5479
parent 1952	27cdc0a3a763
child 2187	f9cc69b432ff