(* Title: Quotient.thy+ −
Author: Cezary Kaliszyk + −
Author: Christian Urban+ −
+ −
provides a reasoning infrastructure for the type of finite sets+ −
*)+ −
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 + −
unfolding 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+ −
"x |\<notin>| S \<equiv> \<not> (x |\<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)"+ −
and "\<not> (x # xs \<approx> [])"+ −
by auto+ −
+ −
lemma not_memb_nil:+ −
shows "\<not> memb x []"+ −
by (simp add: memb_def)+ −
+ −
lemma no_memb_nil:+ −
"(\<forall>x. \<not> memb x xs) = (xs = [])"+ −
by (simp add: memb_def)+ −
+ −
lemma none_memb_nil:+ −
"(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"+ −
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 {* Unions *}+ −
+ −
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:+ −
shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"+ −
by (induct xs) (auto simp add: memb_def)+ −
+ −
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:+ −
shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"+ −
by auto+ −
+ −
lemma fcard_raw_suc:+ −
assumes a: "fcard_raw xs = Suc n"+ −
shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"+ −
using a+ −
by (induct xs) (auto simp add: memb_def split: if_splits)+ −
+ −
lemma singleton_fcard_1: + −
shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"+ −
by (induct xs) (auto simp add: memb_def subset_insert)+ −
+ −
lemma fcard_raw_1:+ −
shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"+ −
apply (auto dest!: fcard_raw_suc)+ −
apply (simp add: fcard_raw_0)+ −
apply (rule_tac x="x" in exI)+ −
apply simp+ −
apply (subgoal_tac "set xs = {x}")+ −
apply (drule singleton_fcard_1)+ −
apply auto+ −
done+ −
+ −
lemma fcard_raw_delete_one:+ −
shows "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_suc_memb:+ −
assumes a: "fcard_raw A = Suc n"+ −
shows "\<exists>a. memb a A"+ −
using a+ −
apply (induct A)+ −
apply simp+ −
apply (rule_tac x="a" in exI)+ −
apply (simp add: memb_def)+ −
done+ −
+ −
lemma memb_card_not_0:+ −
assumes a: "memb a A"+ −
shows "\<not>(fcard_raw A = 0)"+ −
proof -+ −
have "\<not>(\<forall>x. \<not> memb x A)" using a by auto+ −
then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp+ −
then show ?thesis using fcard_raw_0[of A] by simp+ −
qed+ −
+ −
lemma fcard_raw_rsp_aux:+ −
assumes a: "xs \<approx> ys"+ −
shows "fcard_raw xs = fcard_raw ys"+ −
using a+ −
apply(induct xs arbitrary: ys)+ −
apply(auto simp add: memb_def)+ −
apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")+ −
apply simp+ −
apply auto+ −
apply (drule_tac x="x" in spec)+ −
apply blast+ −
apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)+ −
apply(simp add: fcard_raw_delete_one memb_def)+ −
apply(metis Suc_pred'[OF fcard_raw_gt_0])+ −
done+ −
+ −
lemma fcard_raw_rsp[quot_respect]:+ −
shows "(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 (xs @ ys) \<approx> (map f xs) @ (map f ys)"+ −
by simp+ −
+ −
lemma memb_append:+ −
"memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"+ −
by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)+ −
+ −
text {* raw section *}+ −
+ −
lemma map_rsp[quot_respect]:+ −
shows "(op = ===> op \<approx> ===> op \<approx>) map map"+ −
by auto+ −
+ −
lemma cons_left_comm:+ −
"x # y # xs \<approx> y # x # xs"+ −
by auto+ −
+ −
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)))"+ −
apply (induct xs)+ −
apply (simp)+ −
apply (rule disjI2)+ −
apply (erule disjE)+ −
apply (rule_tac x="a" in exI)+ −
apply (rule_tac x="[]" in exI)+ −
apply (simp add: memb_def)+ −
apply (erule exE)++ −
apply (case_tac "x = a")+ −
apply (rule_tac x="a" in exI)+ −
apply (rule_tac x="ys" in exI)+ −
apply (simp)+ −
apply (rule_tac x="x" in exI)+ −
apply (rule_tac x="a # ys" in exI)+ −
apply (auto simp add: memb_def)+ −
done+ −
+ −
section {* deletion *}+ −
+ −
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 xs y) = (memb x xs \<and> x \<noteq> y)"+ −
by (induct xs arbitrary: x y) (auto simp add: memb_def)+ −
+ −
lemma delete_raw_rsp:+ −
"xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"+ −
by (simp add: memb_def[symmetric] memb_delete_raw)+ −
+ −
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:+ −
shows "\<not> memb x (delete_raw xs x)"+ −
by (induct xs) (auto simp add: memb_def)+ −
+ −
lemma not_memb_delete_raw_ident:+ −
shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"+ −
by (induct xs) (auto simp add: memb_def)+ −
+ −
lemma fset_raw_delete_raw_cases:+ −
"xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"+ −
by (induct xs) (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+ −
+ −
lemma ffold_raw_rsp_pre:+ −
"\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"+ −
apply (induct a arbitrary: b)+ −
apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)+ −
apply (simp add: ffold_raw.simps)+ −
apply (rule conjI)+ −
apply (rule_tac [!] impI)+ −
apply (rule_tac [!] conjI)+ −
apply (rule_tac [!] impI)+ −
apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")+ −
apply (simp)+ −
apply (simp add: memb_cons_iff memb_def)+ −
apply auto+ −
apply (drule_tac x="e" in spec)+ −
apply blast+ −
apply (simp add: memb_cons_iff)+ −
apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)+ −
length_Suc_conv memb_absorb nil_not_cons(2))+ −
apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")+ −
apply (simp only:)+ −
apply (rule_tac f="f a1" in arg_cong)+ −
apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")+ −
apply simp+ −
apply (simp add: memb_delete_raw)+ −
apply (auto simp add: memb_cons_iff)[1]+ −
apply (erule memb_commute_ffold_raw)+ −
apply (drule_tac x="a1" in spec)+ −
apply (simp add: memb_cons_iff)+ −
apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)+ −
length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))+ −
done+ −
+ −
lemma [quot_respect]:+ −
"(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"+ −
by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)+ −
+ −
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 x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"+ −
apply (induct xs)+ −
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:+ −
"xs @ ys \<approx> ys @ xs"+ −
by auto+ −
+ −
lemma append_rsp[quot_respect]:+ −
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"+ −
by auto+ −
+ −
lemma set_cong: + −
shows "(set x = set y) = (x \<approx> 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)+ −
+ −
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 x (finsert y S) = finsert y (finsert x S)"+ −
by (lifting cons_left_comm)+ −
+ −
lemma finsert_left_idem:+ −
"finsert x (finsert x S) = finsert x 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 S \<equiv> x |\<in>| S"+ −
by (lifting memb_def[symmetric])+ −
+ −
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)"+ −
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 S = 0) = (S = {||})"+ −
by (lifting fcard_raw_0)+ −
+ −
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 fcard_delete:+ −
"fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"+ −
by (lifting fcard_raw_delete)+ −
+ −
lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"+ −
by (lifting fcard_raw_suc_memb)+ −
+ −
lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"+ −
by (lifting mem_card_not_0)+ −
+ −
text {* funion *}+ −
+ −
lemma funion_simps[simp]:+ −
shows "{||} |\<union>| S = S"+ −
and "finsert x S |\<union>| T = finsert x (S |\<union>| T)"+ −
by (lifting append.simps)+ −
+ −
lemma funion_sym:+ −
shows "S |\<union>| T = T |\<union>| S"+ −
by (lifting funion_sym_pre)+ −
+ −
lemma funion_assoc:+ −
shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"+ −
by (lifting append_assoc)+ −
+ −
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)"+ −
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 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)+ −
+ −
lemma inj_fmap_eq_iff:+ −
"inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"+ −
by (lifting inj_map_eq_iff)+ −
+ −
lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"+ −
by (lifting map_append)+ −
+ −
lemma fin_funion:+ −
"x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"+ −
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: + −
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 fset_raw_delete_raw_cases)+ −
+ −
text {* inter *}+ −
+ −
lemma finter_empty_l: "({||} |\<inter>| S) = {||}"+ −
by (lifting finter_raw.simps(1))+ −
+ −
lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"+ −
by (lifting finter_raw_empty)+ −
+ −
lemma finter_finsert:+ −
"finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"+ −
by (lifting finter_raw.simps(2))+ −
+ −
lemma fin_finter:+ −
"x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"+ −
by (lifting memb_finter_raw)+ −
+ −
lemma expand_fset_eq:+ −
"(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"+ −
by (lifting list_eq.simps[simplified memb_def[symmetric]])+ −
+ −
+ −
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+ −