theory FSet+ −
imports Quotient Quotient_List List+ −
begin+ −
+ −
fun+ −
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)+ −
where+ −
"list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"+ −
+ −
lemma list_eq_equivp:+ −
shows "equivp list_eq"+ −
unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def+ −
by auto+ −
+ −
quotient_type+ −
'a fset = "'a list" / "list_eq"+ −
by (rule list_eq_equivp)+ −
+ −
section {* empty fset, finsert and membership *}+ −
+ −
quotient_definition+ −
fempty ("{||}")+ −
where+ −
"fempty :: 'a fset"+ −
is "[]::'a list"+ −
+ −
quotient_definition+ −
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" + −
is "op #"+ −
+ −
syntax+ −
"@Finset" :: "args => 'a fset" ("{|(_)|}")+ −
+ −
translations+ −
"{|x, xs|}" == "CONST finsert x {|xs|}"+ −
"{|x|}" == "CONST finsert x {||}"+ −
+ −
definition+ −
memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"+ −
where+ −
"memb x xs \<equiv> x \<in> set xs"+ −
+ −
quotient_definition+ −
fin ("_ |\<in>| _" [50, 51] 50)+ −
where+ −
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"+ −
+ −
abbreviation+ −
fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)+ −
where+ −
"a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"+ −
+ −
lemma memb_rsp[quot_respect]:+ −
shows "(op = ===> op \<approx> ===> op =) memb memb"+ −
by (auto simp add: memb_def)+ −
+ −
lemma nil_rsp[quot_respect]:+ −
shows "[] \<approx> []"+ −
by simp+ −
+ −
lemma cons_rsp[quot_respect]:+ −
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"+ −
by simp+ −
+ −
section {* Augmenting an fset -- @{const finsert} *}+ −
+ −
lemma nil_not_cons:+ −
shows+ −
"\<not>[] \<approx> x # xs"+ −
"\<not>x # xs \<approx> []"+ −
by auto+ −
+ −
lemma not_memb_nil:+ −
"\<not>memb x []"+ −
by (simp add: memb_def)+ −
+ −
lemma memb_cons_iff:+ −
shows "memb x (y # xs) = (x = y \<or> memb x xs)"+ −
by (induct xs) (auto simp add: memb_def)+ −
+ −
lemma memb_consI1:+ −
shows "memb x (x # xs)"+ −
by (simp add: memb_def)+ −
+ −
lemma memb_consI2:+ −
shows "memb x xs \<Longrightarrow> memb x (y # xs)"+ −
by (simp add: memb_def)+ −
+ −
lemma memb_absorb:+ −
shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"+ −
by (induct xs) (auto simp add: memb_def id_simps)+ −
+ −
section {* Singletons *}+ −
+ −
lemma singleton_list_eq:+ −
shows "[x] \<approx> [y] \<longleftrightarrow> x = y"+ −
by (simp add: id_simps) auto+ −
+ −
section {* Union *}+ −
+ −
quotient_definition+ −
funion (infixl "|\<union>|" 65)+ −
where+ −
"funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"+ −
is+ −
"op @"+ −
+ −
section {* Cardinality of finite sets *}+ −
+ −
fun+ −
fcard_raw :: "'a list \<Rightarrow> nat"+ −
where+ −
fcard_raw_nil: "fcard_raw [] = 0"+ −
| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"+ −
+ −
quotient_definition+ −
"fcard :: 'a fset \<Rightarrow> nat" + −
is+ −
"fcard_raw"+ −
+ −
lemma fcard_raw_0:+ −
fixes a :: "'a list"+ −
shows "(fcard_raw a = 0) = (a \<approx> [])"+ −
apply (induct a)+ −
apply auto+ −
apply (drule memb_absorb)+ −
apply (auto simp add: nil_not_cons)+ −
done+ −
+ −
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_not_memb:+ −
fixes x :: "'a"+ −
fixes xs :: "'a list"+ −
shows "(~(memb x xs)) = (fcard_raw (x # xs) = Suc (fcard_raw xs))"+ −
by auto+ −
+ −
lemma fcard_raw_suc:+ −
fixes xs :: "'a list"+ −
fixes n :: "nat"+ −
assumes c: "fcard_raw xs = Suc n"+ −
shows "\<exists>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys) \<and> fcard_raw ys = n"+ −
unfolding memb_def+ −
using c+ −
proof (induct xs)+ −
case Nil+ −
then show ?case by simp+ −
next+ −
case (Cons a xs)+ −
have f1: "fcard_raw xs = Suc n \<Longrightarrow> \<exists>a ys. a \<notin> set ys \<and> xs \<approx> a # ys \<and> fcard_raw ys = n" by fact+ −
have f2: "fcard_raw (a # xs) = Suc n" by fact+ −
then show ?case proof (cases "a \<in> set xs")+ −
case True+ −
then show ?thesis using f1 f2 apply -+ −
apply (simp add: memb_def)+ −
apply clarify+ −
by metis+ −
case False+ −
then have ?thesis using f1 f2 apply -+ −
apply (rule_tac x="a" in exI)+ −
apply (rule_tac x="xs" in exI)+ −
apply (simp add: memb_def)+ −
done+ −
qed+ −
qed+ −
qed+ −
+ −
lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0"+ −
apply (induct a)+ −
apply simp_all+ −
apply auto+ −
apply (subgoal_tac "set a2 = {b}")+ −
apply simp+ −
apply (simp add: memb_def)+ −
apply auto+ −
apply (subgoal_tac "set a2 = {}")+ −
apply simp+ −
by (metis memb_def subset_empty subset_insert)+ −
+ −
lemma fcard_raw_1:+ −
fixes a :: "'a list"+ −
shows "(fcard_raw a = 1) = (\<exists>b. a \<approx> [b])"+ −
apply auto+ −
apply (drule fcard_raw_suc)+ −
apply clarify+ −
apply (simp add: fcard_raw_0)+ −
apply (rule_tac x="aa" in exI)+ −
apply simp+ −
apply (subgoal_tac "set a = {b}")+ −
apply (erule singleton_fcard_1)+ −
apply auto+ −
done+ −
+ −
lemma fcard_raw_delete_one:+ −
"fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"+ −
by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)+ −
+ −
lemma fcard_raw_rsp_aux:+ −
assumes a: "a \<approx> b"+ −
shows "fcard_raw a = fcard_raw b"+ −
using a+ −
apply(induct a arbitrary: b)+ −
apply(auto simp add: memb_def)+ −
apply(metis)+ −
apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)+ −
apply(simp add: fcard_raw_delete_one)+ −
apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def)+ −
done+ −
+ −
lemma fcard_raw_rsp[quot_respect]:+ −
"(op \<approx> ===> op =) fcard_raw fcard_raw"+ −
by (simp add: fcard_raw_rsp_aux)+ −
+ −
+ −
section {* fmap and fset comprehension *}+ −
+ −
quotient_definition+ −
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"+ −
is+ −
"map"+ −
+ −
lemma map_append:+ −
"(map f (a @ b)) \<approx> (map f a) @ (map f b)"+ −
by simp+ −
+ −
lemma memb_append:+ −
"memb e (append l r) = (memb e l \<or> memb e r)"+ −
by (induct l) (simp_all add: not_memb_nil memb_cons_iff)+ −
+ −
text {* raw section *}+ −
+ −
lemma map_rsp_aux:+ −
assumes a: "a \<approx> b"+ −
shows "map f a \<approx> map f b"+ −
using a+ −
apply(induct a arbitrary: b)+ −
apply(auto)+ −
apply(metis rev_image_eqI)+ −
done+ −
+ −
lemma map_rsp[quot_respect]:+ −
shows "(op = ===> op \<approx> ===> op \<approx>) map map"+ −
by (auto simp add: map_rsp_aux)+ −
+ −
lemma cons_left_comm:+ −
"x # y # A \<approx> y # x # A"+ −
by (auto simp add: id_simps)+ −
+ −
lemma cons_left_idem:+ −
"x # x # A \<approx> x # A"+ −
by (auto simp add: id_simps)+ −
+ −
lemma none_mem_nil:+ −
"(\<forall>a. a \<notin> set A) = (A \<approx> [])"+ −
by simp+ −
+ −
lemma fset_raw_strong_cases:+ −
"(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"+ −
apply (induct X)+ −
apply (simp)+ −
apply (rule disjI2)+ −
apply (erule disjE)+ −
apply (rule_tac x="a" in exI)+ −
apply (rule_tac x="[]" in exI)+ −
apply (simp)+ −
apply (erule exE)++ −
apply (case_tac "a = aa")+ −
apply (rule_tac x="a" in exI)+ −
apply (rule_tac x="Y" in exI)+ −
apply (simp)+ −
apply (rule_tac x="aa" in exI)+ −
apply (rule_tac x="a # Y" in exI)+ −
apply (auto)+ −
done+ −
+ −
fun+ −
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))"+ −
+ −
lemma memb_delete_raw:+ −
"memb x (delete_raw A a) = (memb x A \<and> x \<noteq> a)"+ −
by (induct A arbitrary: x a) (auto simp add: memb_def)+ −
+ −
lemma [quot_respect]:+ −
"(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"+ −
by (simp add: memb_def[symmetric] memb_delete_raw)+ −
+ −
lemma memb_delete_raw_ident:+ −
"\<not> memb a (delete_raw A a)"+ −
by (induct A) (auto simp add: memb_def)+ −
+ −
lemma not_memb_delete_raw_ident:+ −
"\<not> memb b A \<Longrightarrow> delete_raw A b = A"+ −
by (induct A) (auto simp add: memb_def)+ −
+ −
lemma fset_raw_delete_raw_cases:+ −
"X = [] \<or> (\<exists>a. memb a X \<and> X \<approx> a # delete_raw X a)"+ −
by (induct X) (auto simp add: memb_def)+ −
+ −
lemma fdelete_raw_filter:+ −
"delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"+ −
by (induct xs) simp_all+ −
+ −
lemma fcard_raw_delete:+ −
"fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"+ −
by (simp add: fdelete_raw_filter fcard_raw_delete_one)+ −
+ −
lemma set_rsp[quot_respect]:+ −
"(op \<approx> ===> op =) set set"+ −
by auto+ −
+ −
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) =+ −
(if (rsp_fold f) then+ −
if memb a A then ffold_raw f z A+ −
else f a (ffold_raw f z A)+ −
else z)"+ −
+ −
lemma memb_commute_ffold_raw:+ −
"rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"+ −
apply (induct b)+ −
apply (simp add: not_memb_nil)+ −
apply (simp add: ffold_raw.simps)+ −
apply (rule conjI)+ −
apply (rule_tac [!] impI)+ −
apply (rule_tac [!] conjI)+ −
apply (rule_tac [!] impI)+ −
apply (simp_all add: memb_delete_raw)+ −
apply (simp add: memb_cons_iff)+ −
apply (simp add: not_memb_delete_raw_ident)+ −
apply (simp add: memb_cons_iff rsp_fold_def)+ −
done+ −
+ −
primrec+ −
finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"+ −
where+ −
"finter_raw [] l = []"+ −
| "finter_raw (h # t) l =+ −
(if memb h l then h # (finter_raw t l) else finter_raw t l)"+ −
+ −
lemma finter_raw_empty:+ −
"finter_raw l [] = []"+ −
by (induct l) (simp_all add: not_memb_nil)+ −
+ −
lemma memb_finter_raw:+ −
"memb e (finter_raw l r) = (memb e l \<and> memb e r)"+ −
apply (induct l)+ −
apply (simp add: not_memb_nil)+ −
apply (simp add: finter_raw.simps)+ −
apply (simp add: memb_cons_iff)+ −
apply auto+ −
done+ −
+ −
lemma [quot_respect]:+ −
"(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"+ −
by (simp add: memb_def[symmetric] memb_finter_raw)+ −
+ −
section {* Constants on the Quotient Type *} + −
+ −
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+ −
finter (infix "|\<inter>|" 50)+ −
where+ −
"finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"+ −
is "finter_raw"+ −
+ −
lemma funion_sym_pre:+ −
"a @ b \<approx> b @ a"+ −
by auto+ −
+ −
lemma append_rsp[quot_respect]:+ −
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"+ −
by (auto)+ −
+ −
lemma set_cong: "(set x = set y) = (x \<approx> y)"+ −
apply rule+ −
apply simp_all+ −
apply (induct x y rule: list_induct2')+ −
apply simp_all+ −
apply auto+ −
done+ −
+ −
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)+ −
+ −
quotient_definition+ −
"fconcat :: ('a fset) fset \<Rightarrow> 'a fset"+ −
is+ −
"concat"+ −
+ −
lemma list_equiv_rsp[quot_respect]:+ −
shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"+ −
by auto+ −
+ −
section {* lifted part *}+ −
+ −
lemma not_fin_fnil: "x |\<notin>| {||}"+ −
by (lifting not_memb_nil)+ −
+ −
lemma fin_finsert_iff[simp]:+ −
"x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"+ −
by (lifting memb_cons_iff)+ −
+ −
lemma+ −
shows finsertI1: "x |\<in>| finsert x S"+ −
and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"+ −
by (lifting memb_consI1, lifting memb_consI2)+ −
+ −
lemma finsert_absorb[simp]:+ −
shows "x |\<in>| S \<Longrightarrow> finsert x S = S"+ −
by (lifting memb_absorb)+ −
+ −
lemma fempty_not_finsert[simp]:+ −
"{||} \<noteq> finsert x S"+ −
"finsert x S \<noteq> {||}"+ −
by (lifting nil_not_cons)+ −
+ −
lemma finsert_left_comm:+ −
"finsert a (finsert b S) = finsert b (finsert a S)"+ −
by (lifting cons_left_comm)+ −
+ −
lemma finsert_left_idem:+ −
"finsert a (finsert a S) = finsert a S"+ −
by (lifting cons_left_idem)+ −
+ −
lemma fsingleton_eq[simp]:+ −
shows "{|x|} = {|y|} \<longleftrightarrow> x = y"+ −
by (lifting singleton_list_eq)+ −
+ −
text {* fset_to_set *}+ −
+ −
lemma fset_to_set_simps[simp]:+ −
"fset_to_set {||} = ({} :: 'a set)"+ −
"fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"+ −
by (lifting set.simps)+ −
+ −
lemma in_fset_to_set:+ −
"x \<in> fset_to_set xs \<equiv> x |\<in>| xs"+ −
by (lifting memb_def[symmetric])+ −
+ −
lemma none_fin_fempty:+ −
"(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"+ −
by (lifting none_mem_nil)+ −
+ −
lemma fset_cong:+ −
"(fset_to_set x = fset_to_set y) = (x = y)"+ −
by (lifting set_cong)+ −
+ −
text {* fcard *}+ −
+ −
lemma fcard_fempty [simp]:+ −
shows "fcard {||} = 0"+ −
by (lifting fcard_raw_nil)+ −
+ −
lemma fcard_finsert_if [simp]:+ −
shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"+ −
by (lifting fcard_raw_cons)+ −
+ −
lemma fcard_0: "(fcard a = 0) = (a = {||})"+ −
by (lifting fcard_raw_0)+ −
+ −
lemma fcard_1: "(fcard a = 1) = (\<exists>b. a = {|b|})"+ −
by (lifting fcard_raw_1)+ −
+ −
lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"+ −
by (lifting fcard_raw_gt_0)+ −
+ −
lemma fcard_not_fin: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"+ −
by (lifting fcard_raw_not_memb)+ −
+ −
lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys \<and> fcard ys = n"+ −
by (lifting fcard_raw_suc)+ −
+ −
lemma fcard_delete:+ −
"fcard (fdelete xs y) = (if y |\<in>| xs then fcard xs - 1 else fcard xs)"+ −
by (lifting fcard_raw_delete)+ −
+ −
text {* funion *}+ −
+ −
lemma funion_simps[simp]:+ −
"{||} |\<union>| ys = ys"+ −
"finsert x xs |\<union>| ys = finsert x (xs |\<union>| ys)"+ −
by (lifting append.simps)+ −
+ −
lemma funion_sym:+ −
"a |\<union>| b = b |\<union>| a"+ −
by (lifting funion_sym_pre)+ −
+ −
lemma funion_assoc:+ −
"x |\<union>| xa |\<union>| xb = x |\<union>| (xa |\<union>| xb)"+ −
by (lifting append_assoc)+ −
+ −
section {* Induction and Cases rules for finite sets *}+ −
+ −
lemma fset_strong_cases:+ −
"X = {||} \<or> (\<exists>a Y. a \<notin> fset_to_set Y \<and> X = finsert a Y)"+ −
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)+ −
next+ −
case (finsert x S)+ −
have asm: "P S" by fact+ −
show "P (finsert x S)"+ −
proof(cases "x |\<in>| S")+ −
case True+ −
have "x |\<in>| S" by fact+ −
then show "P (finsert x S)" using asm by simp+ −
next+ −
case False+ −
have "x |\<notin>| S" by fact+ −
then show "P (finsert x S)" using prem2 asm by simp+ −
qed+ −
qed+ −
+ −
lemma fset_induct2:+ −
"P {||} {||} \<Longrightarrow>+ −
(\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>+ −
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>+ −
(\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>+ −
P xsa ysa"+ −
apply (induct xsa arbitrary: ysa)+ −
apply (induct_tac x rule: fset_induct)+ −
apply simp_all+ −
apply (induct_tac xa rule: fset_induct)+ −
apply simp_all+ −
done+ −
+ −
text {* fmap *}+ −
+ −
lemma fmap_simps[simp]:+ −
"fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"+ −
"fmap f (finsert x xs) = finsert (f x) (fmap f xs)"+ −
by (lifting map.simps)+ −
+ −
lemma fmap_set_image:+ −
"fset_to_set (fmap f fs) = f ` (fset_to_set fs)"+ −
apply (induct fs)+ −
apply (simp_all)+ −
done+ −
+ −
lemma inj_fmap_eq_iff:+ −
"inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"+ −
by (lifting inj_map_eq_iff)+ −
+ −
lemma fmap_funion: "fmap f (a |\<union>| b) = fmap f a |\<union>| fmap f b"+ −
by (lifting map_append)+ −
+ −
lemma fin_funion:+ −
"(e |\<in>| l |\<union>| r) = (e |\<in>| l \<or> e |\<in>| r)"+ −
by (lifting memb_append)+ −
+ −
text {* ffold *}+ −
+ −
lemma ffold_nil: "ffold f z {||} = z"+ −
by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])+ −
+ −
lemma ffold_finsert: "ffold f z (finsert a A) =+ −
(if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"+ −
by (lifting ffold_raw.simps(2)[where 'a="'b" and 'b="'a"])+ −
+ −
lemma fin_commute_ffold:+ −
"\<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: "(x |\<in>| fdelete A a) = (x |\<in>| A \<and> x \<noteq> a)"+ −
by (lifting memb_delete_raw)+ −
+ −
lemma fin_fdelete_ident: "a |\<notin>| fdelete A a"+ −
by (lifting memb_delete_raw_ident)+ −
+ −
lemma not_memb_fdelete_ident: "b |\<notin>| A \<Longrightarrow> fdelete A b = A"+ −
by (lifting not_memb_delete_raw_ident)+ −
+ −
lemma fset_fdelete_cases:+ −
"X = {||} \<or> (\<exists>a. a |\<in>| X \<and> X = finsert a (fdelete X a))"+ −
by (lifting fset_raw_delete_raw_cases)+ −
+ −
text {* inter *}+ −
+ −
lemma finter_empty_l: "({||} |\<inter>| r) = {||}"+ −
by (lifting finter_raw.simps(1))+ −
+ −
lemma finter_empty_r: "(l |\<inter>| {||}) = {||}"+ −
by (lifting finter_raw_empty)+ −
+ −
lemma finter_finsert:+ −
"(finsert h t |\<inter>| l) = (if h |\<in>| l then finsert h (t |\<inter>| l) else t |\<inter>| l)"+ −
by (lifting finter_raw.simps(2))+ −
+ −
lemma fin_finter:+ −
"(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)"+ −
by (lifting memb_finter_raw)+ −
+ −
ML {*+ −
fun dest_fsetT (Type ("FSet.fset", [T])) = T+ −
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);+ −
*}+ −
+ −
no_notation+ −
list_eq (infix "\<approx>" 50)+ −
+ −
end+ −