(* Title: HOL/Library/FSet.thy Author: Ondrej Kuncar, TU Muenchen Author: Cezary Kaliszyk and Christian Urban Author: Andrei Popescu, TU Muenchen Author: Martin Desharnais, MPI-INF Saarbruecken
*)
section \<open>Type of finite sets defined as a subtype of sets\<close>
theory FSet imports Main Countable begin
subsection \<open>Definition of the type\<close>
typedef'a fset = "{A :: 'a set. finite A}" morphisms fset Abs_fset by auto
setup_lifting type_definition_fset
subsection \<open>Basic operations and type class instantiations\<close>
(* FIXME transfer and right_total vs. bi_total *) instantiation fset :: (finite) finite begin instanceby (standard; transfer; simp) end
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" begin
lift_definition bot_fset :: "'a fset"is"{}" parametric empty_transfer by simp
lift_definition less_eq_fset :: "'a fset \ 'a fset \ bool" is subset_eq parametric subset_transfer
.
lemma less_fset_transfer[transfer_rule]: includes lifting_syntax assumes [transfer_rule]: "bi_unique A" shows"((pcr_fset A) ===> (pcr_fset A) ===> (=)) (\) (<)" unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover
lift_definition sup_fset :: "'a fset \ 'a fset \ 'a fset" is union parametric union_transfer by simp
lift_definition inf_fset :: "'a fset \ 'a fset \ 'a fset" is inter parametric inter_transfer by simp
lift_definition minus_fset :: "'a fset \ 'a fset \ 'a fset" is minus parametric Diff_transfer by simp
instance by (standard; transfer; auto)+
end
abbreviation fempty :: "'a fset" (\<open>{||}\<close>) where "{||} \<equiv> bot" abbreviation fsubset_eq :: "'a fset \ 'a fset \ bool" (infix \|\|\ 50) where "xs |\| ys \ xs \ ys" abbreviation fsubset :: "'a fset \ 'a fset \ bool" (infix \|\|\ 50) where "xs |\| ys \ xs < ys" abbreviation funion :: "'a fset \ 'a fset \ 'a fset" (infixl \|\|\ 65) where "xs |\| ys \ sup xs ys" abbreviation finter :: "'a fset \ 'a fset \ 'a fset" (infixl \|\|\ 65) where "xs |\| ys \ inf xs ys" abbreviation fminus :: "'a fset \ 'a fset \ 'a fset" (infixl \|-|\ 65) where "xs |-| ys \ minus xs ys"
instantiation fset :: (equal) equal begin definition"HOL.equal A B \ A |\| B \ B |\| A" instanceby intro_classes (auto simp add: equal_fset_def) end
instantiation fset :: (type) conditionally_complete_lattice begin
contextincludes lifting_syntax begin
lemma right_total_Inf_fset_transfer: assumes [transfer_rule]: "bi_unique A"and [transfer_rule]: "right_total A" shows"(rel_set (rel_set A) ===> rel_set A)
(\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {})
(\<lambda>S. if finite (Inf S) then Inf S else {})" by transfer_prover
lemma Inf_fset_transfer: assumes [transfer_rule]: "bi_unique A"and [transfer_rule]: "bi_total A" shows"(rel_set (rel_set A) ===> rel_set A) (\A. if finite (Inf A) then Inf A else {})
(\<lambda>A. if finite (Inf A) then Inf A else {})" by transfer_prover
lift_definition Inf_fset :: "'a fset set \ 'a fset" is "\A. if finite (Inf A) then Inf A else {}"
parametric right_total_Inf_fset_transfer Inf_fset_transfer by simp
lemma Sup_fset_transfer: assumes [transfer_rule]: "bi_unique A" shows"(rel_set (rel_set A) ===> rel_set A) (\A. if finite (Sup A) then Sup A else {})
(\<lambda>A. if finite (Sup A) then Sup A else {})" by transfer_prover
lift_definition Sup_fset :: "'a fset set \ 'a fset" is "\A. if finite (Sup A) then Sup A else {}"
parametric Sup_fset_transfer by simp
lemma finite_Sup: "\z. finite z \ (\a. a \ X \ a \ z) \ finite (Sup X)" by (auto intro: finite_subset)
lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset (=)) ===> (=)) bdd_below bdd_below" by auto
end
instance proof fix x z :: "'a fset" fix X :: "'a fset set"
{ assume"x \ X" "bdd_below X" thenshow"Inf X |\| x" by transfer auto next assume"X \ {}" "(\x. x \ X \ z |\| x)" thenshow"z |\| Inf X" by transfer (clarsimp, blast) next assume"x \ X" "bdd_above X" thenobtain z where"x \ X" "(\x. x \ X \ x |\| z)" by (auto simp: bdd_above_def) thenshow"x |\| Sup X" by transfer (auto intro!: finite_Sup) next assume"X \ {}" "(\x. x \ X \ x |\| z)" thenshow"Sup X |\| z" by transfer (clarsimp, blast)
} qed end
instantiation fset :: (finite) complete_lattice begin
lemma fsingleton_inject[dest!]: "{|a|} = {|b|} \ a = b" by (rule singleton_inject[Transfer.transferred])
lemma fsingleton_finsert_inj_eq[iff,no_atp]: "({|b|} = finsert a A) = (a = b \ A |\| {|b|})" by (rule singleton_insert_inj_eq[Transfer.transferred])
lemma fsingleton_finsert_inj_eq'[iff,no_atp]: "(finsert a A = {|b|}) = (a = b \ A |\| {|b|})" by (rule singleton_insert_inj_eq'[Transfer.transferred])
lemma fsubset_fsingletonD: "A |\| {|x|} \ A = {||} \ A = {|x|}" by (rule subset_singletonD[Transfer.transferred])
lemma fminus_single_finsert: "A |-| {|x|} |\| B \ A |\| finsert x B" by (rule Diff_single_insert[Transfer.transferred])
lemma fdoubleton_eq_iff: "({|a, b|} = {|c, d|}) = (a = c \ b = d \ a = d \ b = c)" by (rule doubleton_eq_iff[Transfer.transferred])
lemma funion_fsingleton_iff: "(A |\| B = {|x|}) = (A = {||} \ B = {|x|} \ A = {|x|} \ B = {||} \ A = {|x|} \B = {|x|})" by (rule Un_singleton_iff[Transfer.transferred])
lemma fsingleton_funion_iff: "({|x|} = A |\| B) = (A = {||} \ B = {|x|} \ A = {|x|} \ B = {||} \ A = {|x|} \B = {|x|})" by (rule singleton_Un_iff[Transfer.transferred])
lemma fimage_eqI[simp, intro]: "b = f x \ x |\| A \ b |\| f |`| A" by (rule image_eqI[Transfer.transferred])
lemma fimageI: "x |\| A \ f x |\| f |`| A" by (rule imageI[Transfer.transferred])
lemma rev_fimage_eqI: "x |\| A \ b = f x \ b |\| f |`| A" by (rule rev_image_eqI[Transfer.transferred])
lemma fimageE[elim!]: "b |\| f |`| A \ (\x. b = f x \ x |\| A \ thesis) \ thesis" by (rule imageE[Transfer.transferred])
lemma Compr_fimage_eq: "{x. x |\| f |`| A \ P x} = f ` {x. x |\| A \ P (f x)}" by (rule Compr_image_eq[Transfer.transferred])
lemma fimage_funion: "f |`| (A |\| B) = f |`| A |\| f |`| B" by (rule image_Un[Transfer.transferred])
lemma fimage_iff: "(z |\| f |`| A) = fBex A (\x. z = f x)" by (rule image_iff[Transfer.transferred])
lemma fimage_fsubset_iff[no_atp]: "(f |`| A |\| B) = fBall A (\x. f x |\| B)" by (rule image_subset_iff[Transfer.transferred])
lemma fimage_fsubsetI: "(\x. x |\| A \ f x |\| B) \ f |`| A |\| B" by (rule image_subsetI[Transfer.transferred])
lemma fimage_ident[simp]: "(\x. x) |`| Y = Y" by (rule image_ident[Transfer.transferred])
lemma if_split_fmem1: "((if Q then x else y) |\| b) = ((Q \ x |\| b) \ (\ Q \ y |\| b))" by (rule if_split_mem1[Transfer.transferred])
lemma if_split_fmem2: "(a |\| (if Q then x else y)) = ((Q \ a |\| x) \ (\ Q \ a |\| y))" by (rule if_split_mem2[Transfer.transferred])
lemma pfsubsetI[intro!,no_atp]: "A |\| B \ A \ B \ A |\| B" by (rule psubsetI[Transfer.transferred])
lemma pfsubsetE[elim!,no_atp]: "A |\| B \ (A |\| B \ \ B |\| A \ R) \ R" by (rule psubsetE[Transfer.transferred])
lemma pfsubset_finsert_iff: "(A |\| finsert x B) =
(if x |\<in>| B then A |\<subset>| B else if x |\<in>| A then A |-| {|x|} |\<subset>| B else A |\<subseteq>| B)" by (rule psubset_insert_iff[Transfer.transferred])
lemma pfsubset_eq: "(A |\| B) = (A |\| B \ A \ B)" by (rule psubset_eq[Transfer.transferred])
lemma pfsubset_imp_fsubset: "A |\| B \ A |\| B" by (rule psubset_imp_subset[Transfer.transferred])
lemma pfsubset_trans: "A |\| B \ B |\| C \ A |\| C" by (rule psubset_trans[Transfer.transferred])
lemma pfsubsetD: "A |\| B \ c |\| A \ c |\| B" by (rule psubsetD[Transfer.transferred])
lemma pfsubset_fsubset_trans: "A |\| B \ B |\| C \ A |\| C" by (rule psubset_subset_trans[Transfer.transferred])
lemma fsubset_pfsubset_trans: "A |\| B \ B |\| C \ A |\| C" by (rule subset_psubset_trans[Transfer.transferred])
lemma pfsubset_imp_ex_fmem: "A |\| B \ \b. b |\| B |-| A" by (rule psubset_imp_ex_mem[Transfer.transferred])
lemma fimage_fPow_mono: "f |`| A |\| B \ (|`|) f |`| fPow A |\| fPow B" by (rule image_Pow_mono[Transfer.transferred])
lemma fimage_fPow_surj: "f |`| A = B \ (|`|) f |`| fPow A = fPow B" by (rule image_Pow_surj[Transfer.transferred])
lemma fsubset_finsertI: "B |\| finsert a B" by (rule subset_insertI[Transfer.transferred])
lemma fsubset_finsertI2: "A |\| B \ A |\| finsert b B" by (rule subset_insertI2[Transfer.transferred])
lemma fsubset_finsert: "x |\| A \ (A |\| finsert x B) = (A |\| B)" by (rule subset_insert[Transfer.transferred])
lemma funion_upper1: "A |\| A |\| B" by (rule Un_upper1[Transfer.transferred])
lemma funion_upper2: "B |\| A |\| B" by (rule Un_upper2[Transfer.transferred])
lemma funion_least: "A |\| C \ B |\| C \ A |\| B |\| C" by (rule Un_least[Transfer.transferred])
lemma finter_lower1: "A |\| B |\| A" by (rule Int_lower1[Transfer.transferred])
lemma finter_lower2: "A |\| B |\| B" by (rule Int_lower2[Transfer.transferred])
lemma finter_greatest: "C |\| A \ C |\| B \ C |\| A |\| B" by (rule Int_greatest[Transfer.transferred])
lemma fminus_fsubset: "A |-| B |\| A" by (rule Diff_subset[Transfer.transferred])
lemma fminus_fsubset_conv: "(A |-| B |\| C) = (A |\| B |\| C)" by (rule Diff_subset_conv[Transfer.transferred])
lemma fsubset_fempty[simp]: "(A |\| {||}) = (A = {||})" by (rule subset_empty[Transfer.transferred])
lemma not_pfsubset_fempty[iff]: "\ A |\| {||}" by (rule not_psubset_empty[Transfer.transferred])
lemma finsert_is_funion: "finsert a A = {|a|} |\| A" by (rule insert_is_Un[Transfer.transferred])
lemma finsert_not_fempty[simp]: "finsert a A \ {||}" by (rule insert_not_empty[Transfer.transferred])
lemma fempty_not_finsert: "{||} \ finsert a A" by (rule empty_not_insert[Transfer.transferred])
lemma finsert_absorb: "a |\| A \ finsert a A = A" by (rule insert_absorb[Transfer.transferred])
lemma finsert_absorb2[simp]: "finsert x (finsert x A) = finsert x A" by (rule insert_absorb2[Transfer.transferred])
lemma finsert_commute: "finsert x (finsert y A) = finsert y (finsert x A)" by (rule insert_commute[Transfer.transferred])
lemma finsert_fsubset[simp]: "(finsert x A |\| B) = (x |\| B \ A |\| B)" by (rule insert_subset[Transfer.transferred])
lemma finsert_inter_finsert[simp]: "finsert a A |\| finsert a B = finsert a (A |\| B)" by (rule insert_inter_insert[Transfer.transferred])
lemma finsert_disjoint[simp,no_atp]: "(finsert a A |\| B = {||}) = (a |\| B \ A |\| B = {||})" "({||} = finsert a A |\| B) = (a |\| B \ {||} = A |\| B)" by (rule insert_disjoint[Transfer.transferred])+
lemma disjoint_finsert[simp,no_atp]: "(B |\| finsert a A = {||}) = (a |\| B \ B |\| A = {||})" "({||} = A |\| finsert b B) = (b |\| A \ {||} = A |\| B)" by (rule disjoint_insert[Transfer.transferred])+
lemma fimage_fempty[simp]: "f |`| {||} = {||}" by (rule image_empty[Transfer.transferred])
lemma fimage_finsert[simp]: "f |`| finsert a B = finsert (f a) (f |`| B)" by (rule image_insert[Transfer.transferred])
lemma fimage_constant: "x |\| A \ (\x. c) |`| A = {|c|}" by (rule image_constant[Transfer.transferred])
lemma fimage_constant_conv: "(\x. c) |`| A = (if A = {||} then {||} else {|c|})" by (rule image_constant_conv[Transfer.transferred])
lemma fimage_fimage: "f |`| g |`| A = (\x. f (g x)) |`| A" by (rule image_image[Transfer.transferred])
lemma finsert_fimage[simp]: "x |\| A \ finsert (f x) (f |`| A) = f |`| A" by (rule insert_image[Transfer.transferred])
lemma fimage_is_fempty[iff]: "(f |`| A = {||}) = (A = {||})" by (rule image_is_empty[Transfer.transferred])
lemma fempty_is_fimage[iff]: "({||} = f |`| A) = (A = {||})" by (rule empty_is_image[Transfer.transferred])
lemma fimage_cong: "M = N \ (\x. x |\| N \ f x = g x) \ f |`| M = g |`| N" by (rule image_cong[Transfer.transferred])
lemma fimage_finter_fsubset: "f |`| (A |\| B) |\| f |`| A |\| f |`| B" by (rule image_Int_subset[Transfer.transferred])
lemma fimage_fminus_fsubset: "f |`| A |-| f |`| B |\| f |`| (A |-| B)" by (rule image_diff_subset[Transfer.transferred])
lemma finter_absorb: "A |\| A = A" by (rule Int_absorb[Transfer.transferred])
lemma finter_left_absorb: "A |\| (A |\| B) = A |\| B" by (rule Int_left_absorb[Transfer.transferred])
lemma finter_commute: "A |\| B = B |\| A" by (rule Int_commute[Transfer.transferred])
lemma finter_left_commute: "A |\| (B |\| C) = B |\| (A |\| C)" by (rule Int_left_commute[Transfer.transferred])
lemma finter_assoc: "A |\| B |\| C = A |\| (B |\| C)" by (rule Int_assoc[Transfer.transferred])
lemma finter_ac: "A |\| B |\| C = A |\| (B |\| C)" "A |\| (A |\| B) = A |\| B" "A |\| B = B |\| A" "A |\| (B |\| C) = B |\| (A |\| C)" by (rule Int_ac[Transfer.transferred])+
lemma finter_absorb1: "B |\| A \ A |\| B = B" by (rule Int_absorb1[Transfer.transferred])
lemma finter_absorb2: "A |\| B \ A |\| B = A" by (rule Int_absorb2[Transfer.transferred])
lemma finter_fempty_left: "{||} |\| B = {||}" by (rule Int_empty_left[Transfer.transferred])
lemma finter_fempty_right: "A |\| {||} = {||}" by (rule Int_empty_right[Transfer.transferred])
lemma disjoint_iff_fnot_equal: "(A |\| B = {||}) = fBall A (\x. fBall B ((\) x))" by (rule disjoint_iff_not_equal[Transfer.transferred])
lemma finter_funion_distrib: "A |\| (B |\| C) = A |\| B |\| (A |\| C)" by (rule Int_Un_distrib[Transfer.transferred])
lemma finter_funion_distrib2: "B |\| C |\| A = B |\| A |\| (C |\| A)" by (rule Int_Un_distrib2[Transfer.transferred])
lemma finter_fsubset_iff[no_atp, simp]: "(C |\| A |\| B) = (C |\| A \ C |\| B)" by (rule Int_subset_iff[Transfer.transferred])
lemma funion_absorb: "A |\| A = A" by (rule Un_absorb[Transfer.transferred])
lemma funion_left_absorb: "A |\| (A |\| B) = A |\| B" by (rule Un_left_absorb[Transfer.transferred])
lemma funion_commute: "A |\| B = B |\| A" by (rule Un_commute[Transfer.transferred])
lemma funion_left_commute: "A |\| (B |\| C) = B |\| (A |\| C)" by (rule Un_left_commute[Transfer.transferred])
lemma funion_assoc: "A |\| B |\| C = A |\| (B |\| C)" by (rule Un_assoc[Transfer.transferred])
lemma funion_ac: "A |\| B |\| C = A |\| (B |\| C)" "A |\| (A |\| B) = A |\| B" "A |\| B = B |\| A" "A |\| (B |\| C) = B |\| (A |\| C)" by (rule Un_ac[Transfer.transferred])+
lemma funion_absorb1: "A |\| B \ A |\| B = B" by (rule Un_absorb1[Transfer.transferred])
lemma funion_absorb2: "B |\| A \ A |\| B = A" by (rule Un_absorb2[Transfer.transferred])
lemma funion_fempty_left: "{||} |\| B = B" by (rule Un_empty_left[Transfer.transferred])
lemma funion_fempty_right: "A |\| {||} = A" by (rule Un_empty_right[Transfer.transferred])
lemma funion_finsert_left[simp]: "finsert a B |\| C = finsert a (B |\| C)" by (rule Un_insert_left[Transfer.transferred])
lemma funion_finsert_right[simp]: "A |\| finsert a B = finsert a (A |\| B)" by (rule Un_insert_right[Transfer.transferred])
lemma finter_finsert_left: "finsert a B |\| C = (if a |\| C then finsert a (B |\| C) else B |\| C)" by (rule Int_insert_left[Transfer.transferred])
lemma finter_finsert_left_ifffempty[simp]: "a |\| C \ finsert a B |\| C = B |\| C" by (rule Int_insert_left_if0[Transfer.transferred])
lemma finter_finsert_left_if1[simp]: "a |\| C \ finsert a B |\| C = finsert a (B |\| C)" by (rule Int_insert_left_if1[Transfer.transferred])
lemma finter_finsert_right: "A |\| finsert a B = (if a |\| A then finsert a (A |\| B) else A |\| B)" by (rule Int_insert_right[Transfer.transferred])
lemma finter_finsert_right_ifffempty[simp]: "a |\| A \ A |\| finsert a B = A |\| B" by (rule Int_insert_right_if0[Transfer.transferred])
lemma finter_finsert_right_if1[simp]: "a |\| A \ A |\| finsert a B = finsert a (A |\| B)" by (rule Int_insert_right_if1[Transfer.transferred])
lemma funion_finter_distrib: "A |\| (B |\| C) = A |\| B |\| (A |\| C)" by (rule Un_Int_distrib[Transfer.transferred])
lemma funion_finter_distrib2: "B |\| C |\| A = B |\| A |\| (C |\| A)" by (rule Un_Int_distrib2[Transfer.transferred])
lemma funion_finter_crazy: "A |\| B |\| (B |\| C) |\| (C |\| A) = A |\| B |\| (B |\| C) |\| (C |\| A)" by (rule Un_Int_crazy[Transfer.transferred])
lemma fsubset_funion_eq: "(A |\| B) = (A |\| B = B)" by (rule subset_Un_eq[Transfer.transferred])
lemma funion_fempty[iff]: "(A |\| B = {||}) = (A = {||} \ B = {||})" by (rule Un_empty[Transfer.transferred])
lemma funion_fsubset_iff[no_atp, simp]: "(A |\| B |\| C) = (A |\| C \ B |\| C)" by (rule Un_subset_iff[Transfer.transferred])
lemma funion_fminus_finter: "A |-| B |\| (A |\| B) = A" by (rule Un_Diff_Int[Transfer.transferred])
lemma ffunion_empty[simp]: "ffUnion {||} = {||}" by (rule Union_empty[Transfer.transferred])
lemma ffunion_mono: "A |\| B \ ffUnion A |\| ffUnion B" by (rule Union_mono[Transfer.transferred])
lemma ffunion_insert[simp]: "ffUnion (finsert a B) = a |\| ffUnion B" by (rule Union_insert[Transfer.transferred])
lemma fminus_finter2: "A |\| C |-| (B |\| C) = A |\| C |-| B" by (rule Diff_Int2[Transfer.transferred])
lemma funion_finter_assoc_eq: "(A |\| B |\| C = A |\| (B |\| C)) = (C |\| A)" by (rule Un_Int_assoc_eq[Transfer.transferred])
lemma fBall_funion: "fBall (A |\| B) P = (fBall A P \ fBall B P)" by (rule ball_Un[Transfer.transferred])
lemma fBex_funion: "fBex (A |\| B) P = (fBex A P \ fBex B P)" by (rule bex_Un[Transfer.transferred])
lemma fminus_eq_fempty_iff[simp,no_atp]: "(A |-| B = {||}) = (A |\| B)" by (rule Diff_eq_empty_iff[Transfer.transferred])
lemma fminus_cancel[simp]: "A |-| A = {||}" by (rule Diff_cancel[Transfer.transferred])
lemma fminus_idemp[simp]: "A |-| B |-| B = A |-| B" by (rule Diff_idemp[Transfer.transferred])
lemma fminus_triv: "A |\| B = {||} \ A |-| B = A" by (rule Diff_triv[Transfer.transferred])
lemma fempty_fminus[simp]: "{||} |-| A = {||}" by (rule empty_Diff[Transfer.transferred])
lemma fminus_fempty[simp]: "A |-| {||} = A" by (rule Diff_empty[Transfer.transferred])
lemma fminus_finsertffempty[simp,no_atp]: "x |\| A \ A |-| finsert x B = A |-| B" by (rule Diff_insert0[Transfer.transferred])
lemma fminus_finsert: "A |-| finsert a B = A |-| B |-| {|a|}" by (rule Diff_insert[Transfer.transferred])
lemma fminus_finsert2: "A |-| finsert a B = A |-| {|a|} |-| B" by (rule Diff_insert2[Transfer.transferred])
lemma finsert_fminus_if: "finsert x A |-| B = (if x |\| B then A |-| B else finsert x (A |-| B))" by (rule insert_Diff_if[Transfer.transferred])
lemma finsert_fminus1[simp]: "x |\| B \ finsert x A |-| B = A |-| B" by (rule insert_Diff1[Transfer.transferred])
lemma finsert_fminus_single[simp]: "finsert a (A |-| {|a|}) = finsert a A" by (rule insert_Diff_single[Transfer.transferred])
lemma finsert_fminus: "a |\| A \ finsert a (A |-| {|a|}) = A" by (rule insert_Diff[Transfer.transferred])
lemma fminus_finsert_absorb: "x |\| A \ finsert x A |-| {|x|} = A" by (rule Diff_insert_absorb[Transfer.transferred])
lemma fminus_disjoint[simp]: "A |\| (B |-| A) = {||}" by (rule Diff_disjoint[Transfer.transferred])
lemma fminus_partition: "A |\| B \ A |\| (B |-| A) = B" by (rule Diff_partition[Transfer.transferred])
lemma double_fminus: "A |\| B \ B |\| C \ B |-| (C |-| A) = A" by (rule double_diff[Transfer.transferred])
lemma funion_fminus_cancel[simp]: "A |\| (B |-| A) = A |\| B" by (rule Un_Diff_cancel[Transfer.transferred])
lemma funion_fminus_cancel2[simp]: "B |-| A |\| A = B |\| A" by (rule Un_Diff_cancel2[Transfer.transferred])
lemma fminus_funion: "A |-| (B |\| C) = A |-| B |\| (A |-| C)" by (rule Diff_Un[Transfer.transferred])
lemma fminus_finter: "A |-| (B |\| C) = A |-| B |\| (A |-| C)" by (rule Diff_Int[Transfer.transferred])
lemma funion_fminus: "A |\| B |-| C = A |-| C |\| (B |-| C)" by (rule Un_Diff[Transfer.transferred])
lemma finter_fminus: "A |\| B |-| C = A |\| (B |-| C)" by (rule Int_Diff[Transfer.transferred])
lemma fminus_finter_distrib: "C |\| (A |-| B) = C |\| A |-| (C |\| B)" by (rule Diff_Int_distrib[Transfer.transferred])
lemma fminus_finter_distrib2: "A |-| B |\| C = A |\| C |-| (B |\| C)" by (rule Diff_Int_distrib2[Transfer.transferred])
lemma fUNIV_bool[no_atp]: "fUNIV = {|False, True|}" by (rule UNIV_bool[Transfer.transferred])
lemma fPow_fempty[simp]: "fPow {||} = {|{||}|}" by (rule Pow_empty[Transfer.transferred])
lemma fPow_finsert: "fPow (finsert a A) = fPow A |\| finsert a |`| fPow A" by (rule Pow_insert[Transfer.transferred])
lemma funion_fPow_fsubset: "fPow A |\| fPow B |\| fPow (A |\| B)" by (rule Un_Pow_subset[Transfer.transferred])
lemma fPow_finter_eq[simp]: "fPow (A |\| B) = fPow A |\| fPow B" by (rule Pow_Int_eq[Transfer.transferred])
lemma fset_eq_fsubset: "(A = B) = (A |\| B \ B |\| A)" by (rule set_eq_subset[Transfer.transferred])
lemma fsubset_iff[no_atp]: "(A |\| B) = (\t. t |\| A \ t |\| B)" by (rule subset_iff[Transfer.transferred])
lemma fsubset_iff_pfsubset_eq: "(A |\| B) = (A |\| B \ A = B)" by (rule subset_iff_psubset_eq[Transfer.transferred])
lemma all_not_fin_conv[simp]: "(\x. x |\| A) = (A = {||})" by (rule all_not_in_conv[Transfer.transferred])
lemma ex_fin_conv: "(\x. x |\| A) = (A \ {||})" by (rule ex_in_conv[Transfer.transferred])
lemma fimage_mono: "A |\| B \ f |`| A |\| f |`| B" by (rule image_mono[Transfer.transferred])
lemma fPow_mono: "A |\| B \ fPow A |\| fPow B" by (rule Pow_mono[Transfer.transferred])
lemma finsert_mono: "C |\| D \ finsert a C |\| finsert a D" by (rule insert_mono[Transfer.transferred])
lemma funion_mono: "A |\| C \ B |\| D \ A |\| B |\| C |\| D" by (rule Un_mono[Transfer.transferred])
lemma finter_mono: "A |\| C \ B |\| D \ A |\| B |\| C |\| D" by (rule Int_mono[Transfer.transferred])
lemma fminus_mono: "A |\| C \ D |\| B \ A |-| B |\| C |-| D" by (rule Diff_mono[Transfer.transferred])
lemma fin_mono: "A |\| B \ x |\| A \ x |\| B" by (rule in_mono[Transfer.transferred])
lemma fthe_felem_eq[simp]: "fthe_elem {|x|} = x" by (rule the_elem_eq[Transfer.transferred])
lemma fLeast_mono: "mono f \ fBex S (\x. fBall S ((\) x)) \ (LEAST y. y |\| f |`| S) = f (LEAST x. x |\| S)" by (rule Least_mono[Transfer.transferred])
lemma fbind_fbind: "fbind (fbind A B) C = fbind A (\x. fbind (B x) C)" by (rule Set.bind_bind[Transfer.transferred])
lemma fempty_fbind[simp]: "fbind {||} f = {||}" by (rule empty_bind[Transfer.transferred])
lemma nonfempty_fbind_const: "A \ {||} \ fbind A (\_. B) = B" by (rule nonempty_bind_const[Transfer.transferred])
lemma fbind_const: "fbind A (\_. B) = (if A = {||} then {||} else B)" by (rule bind_const[Transfer.transferred])
lemma ffmember_filter[simp]: "(x |\| ffilter P A) = (x |\| A \ P x)" by transfer simp
lemma fequalityI: "A |\| B \ B |\| A \ A = B" by (rule equalityI[Transfer.transferred])
lemma subset_ffilter: "ffilter P A |\| ffilter Q A = (\ x. x |\| A \ P x \ Q x)" by transfer auto
lemma eq_ffilter: "(ffilter P A = ffilter Q A) = (\x. x |\| A \ P x = Q x)" by transfer auto
lemma pfsubset_ffilter: "(\x. x |\| A \ P x \ Q x) \ (x |\| A \ \ P x \ Q x) \
ffilter P A |\<subset>| ffilter Q A" unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
(* FIXME, transferred doesn't work here *) lemma set_finsert: assumes"x |\| A" obtains B where"A = finsert x B"and"x |\| B" using assms by transfer (metis Set.set_insert finite_insert)
lemma mk_disjoint_finsert: "a |\| A \ \B. A = finsert a B \ a |\| B" by (rule exI [where x = "A |-| {|a|}"]) blast
lemma finsert_eq_iff: assumes"a |\| A" and "b |\| B" shows"(finsert a A = finsert b B) =
(if a = b then A = B else \<exists>C. A = finsert b C \<and> b |\<notin>| C \<and> B = finsert a C \<and> a |\<notin>| C)" using assms by transfer (force simp: insert_eq_iff)
lemma subset_fimage_iff: "(B |\| f|`|A) = (\ AA. AA |\| A \ B = f|`|AA)" by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
lemma fimage_strict_mono: assumes"inj_on f (fset B)"and"A |\| B" shows"f |`| A |\| f |`| B" \<comment> \<open>TODO: Configure transfer framework to lift @{thm Fun.image_strict_mono}.\<close> proof (rule pfsubsetI) from\<open>A |\<subset>| B\<close> have "A |\<subseteq>| B" by (rule pfsubset_imp_fsubset) thus"f |`| A |\| f |`| B" by (rule fimage_mono) next from\<open>A |\<subset>| B\<close> have "A |\<subseteq>| B" and "A \<noteq> B" by (simp_all add: pfsubset_eq)
have"fset A \ fset B" using\<open>A \<noteq> B\<close> by (simp add: fset_cong) hence"f ` fset A \ f ` fset B" using\<open>A |\<subseteq>| B\<close> by (simp add: inj_on_image_eq_iff[OF \<open>inj_on f (fset B)\<close>] less_eq_fset.rep_eq) hence"fset (f |`| A) \ fset (f |`| B)" by (simp add: fimage.rep_eq) thus"f |`| A \ f |`| B" by (simp add: fset_cong) qed
lemma bex_simps [simp, no_atp]: "\A P Q. fBex A (\x. P x \ Q) = (fBex A P \ Q)" "\A P Q. fBex A (\x. P \ Q x) = (P \ fBex A Q)" "\P. fBex {||} P = False" "\a B P. fBex (finsert a B) P = (P a \ fBex B P)" "\A P f. fBex (f |`| A) P = fBex A (\x. P (f x))" "\A P. (\ fBex A P) = fBall A (\x. \ P x)" by auto
lemma ball_simps [simp, no_atp]: "\A P Q. fBall A (\x. P x \ Q) = (fBall A P \ Q)" "\A P Q. fBall A (\x. P \ Q x) = (P \ fBall A Q)" "\A P Q. fBall A (\x. P \ Q x) = (P \ fBall A Q)" "\A P Q. fBall A (\x. P x \ Q) = (fBex A P \ Q)" "\P. fBall {||} P = True" "\a B P. fBall (finsert a B) P = (P a \ fBall B P)" "\A P f. fBall (f |`| A) P = fBall A (\x. P (f x))" "\A P. (\ fBall A P) = fBex A (\x. \ P x)" by auto
lemma atomize_fBall: "(\x. x |\| A ==> P x) == Trueprop (fBall A (\x. P x))" by (simp add: Set.atomize_ball)
lemma fBall_mono[mono]: "P \ Q \ fBall S P \ fBall S Q" by auto
lemma fBex_mono[mono]: "P \ Q \ fBex S P \ fBex S Q" by auto
end
subsubsection \<open>\<open>fcard\<close>\<close>
(* FIXME: improve transferred to handle bounded meta quantification *)
lemma fcard_fempty: "fcard {||} = 0" by transfer (rule card.empty)
lemma fcard_finsert_disjoint: "x |\| A \ fcard (finsert x A) = Suc (fcard A)" by transfer (rule card_insert_disjoint)
lemma fcard_finsert_if: "fcard (finsert x A) = (if x |\| A then fcard A else Suc (fcard A))" by transfer (rule card_insert_if)
lemma fcard_0_eq [simp, no_atp]: "fcard A = 0 \ A = {||}" by transfer (rule card_0_eq)
lemma fcard_Suc_fminus1: "x |\| A \ Suc (fcard (A |-| {|x|})) = fcard A" by transfer (rule card_Suc_Diff1)
lemma fcard_fminus_fsingleton: "x |\| A \ fcard (A |-| {|x|}) = fcard A - 1" by transfer (rule card_Diff_singleton)
lemma fcard_fminus_fsingleton_if: "fcard (A |-| {|x|}) = (if x |\| A then fcard A - 1 else fcard A)" by transfer (rule card_Diff_singleton_if)
lemma fcard_fminus_finsert[simp]: assumes"a |\| A" and "a |\| B" shows"fcard (A |-| finsert a B) = fcard (A |-| B) - 1" using assms by transfer (rule card_Diff_insert)
lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A |-| {|x|}))" by transfer (rule card.insert_remove)
lemma fcard_finsert_le: "fcard A \ fcard (finsert x A)" by transfer (rule card_insert_le)
lemma fcard_mono: "A |\| B \ fcard A \ fcard B" by transfer (rule card_mono)
lemma fcard_seteq: "A |\| B \ fcard B \ fcard A \ A = B" by transfer (rule card_seteq)
lemma pfsubset_fcard_mono: "A |\| B \ fcard A < fcard B" by transfer (rule psubset_card_mono)
lemma fcard_funion_finter: "fcard A + fcard B = fcard (A |\| B) + fcard (A |\| B)" by transfer (rule card_Un_Int)
lemma fcard_funion_disjoint: "A |\| B = {||} \ fcard (A |\| B) = fcard A + fcard B" by transfer (rule card_Un_disjoint)
lemma fcard_funion_fsubset: "B |\| A \ fcard (A |-| B) = fcard A - fcard B" by transfer (rule card_Diff_subset)
lemma diff_fcard_le_fcard_fminus: "fcard A - fcard B \ fcard(A |-| B)" by transfer (rule diff_card_le_card_Diff)
lemma fcard_fminus1_less: "x |\| A \ fcard (A |-| {|x|}) < fcard A" by transfer (rule card_Diff1_less)
lemma fcard_fminus2_less: "x |\| A \ y |\| A \ fcard (A |-| {|x|} |-| {|y|}) < fcard A" by transfer (rule card_Diff2_less)
lemma fcard_fminus1_le: "fcard (A |-| {|x|}) \ fcard A" by transfer (rule card_Diff1_le)
lemma fcard_pfsubset: "A |\| B \ fcard A < fcard B \ A < B" by transfer (rule card_psubset)
(* FIXME: improve transferred to handle bounded meta quantification *)
context comp_fun_commute begin lemma ffold_empty[simp]: "ffold f z {||} = z" by (rule fold_empty[Transfer.transferred])
lemma ffold_finsert [simp]: assumes"x |\| A" shows"ffold f z (finsert x A) = f x (ffold f z A)" using assms by (transfer fixing: f) (rule fold_insert)
lemma ffold_fun_left_comm: "f x (ffold f z A) = ffold f (f x z) A" by (transfer fixing: f) (rule fold_fun_left_comm)
lemma ffold_finsert2: "x |\| A \ ffold f z (finsert x A) = ffold f (f x z) A" by (transfer fixing: f) (rule fold_insert2)
lemma ffold_rec: assumes"x |\| A" shows"ffold f z A = f x (ffold f z (A |-| {|x|}))" using assms by (transfer fixing: f) (rule fold_rec)
lemma ffold_finsert_fremove: "ffold f z (finsert x A) = f x (ffold f z (A |-| {|x|}))" by (transfer fixing: f) (rule fold_insert_remove) end
lemma ffold_fimage: assumes"inj_on g (fset A)" shows"ffold f z (g |`| A) = ffold (f \ g) z A" using assms by transfer' (rule fold_image)
lemma ffold_cong: assumes"comp_fun_commute f""comp_fun_commute g" "\x. x |\| A \ f x = g x" and"s = t"and"A = B" shows"ffold f s A = ffold g t B" using assms[unfolded comp_fun_commute_def'] by transfer (meson Finite_Set.fold_cong subset_UNIV)
context comp_fun_idem begin
lemma ffold_finsert_idem: "ffold f z (finsert x A) = f x (ffold f z A)" by (transfer fixing: f) (rule fold_insert_idem)
lemma eq_fold: "F (finsert x A) = ffold f x A" by transfer (rule set.eq_fold)
lemma singleton [simp]: "F {|x|} = x" by transfer (rule set.singleton)
lemma insert_not_elem: "x |\| A \ A \ {||} \ F (finsert x A) = x \<^bold>* F A" by transfer (rule set.insert_not_elem)
lemma in_idem: "x |\| A \ x \<^bold>* F A = F A" by transfer (rule set.in_idem)
lemma insert [simp]: "A \ {||} \ F (finsert x A) = x \<^bold>* F A" by transfer (rule set.insert)
end
locale semilattice_order_fset = binary?: semilattice_order + semilattice_fset begin
end
context linorder begin
sublocale fMin: semilattice_order_fset min less_eq less
rewrites "semilattice_set.F min = Min" defines fMin = fMin.F proof - show"semilattice_order_fset min (\) (<)" by standard
show"semilattice_set.F min = Min"unfolding Min_def .. qed
sublocale fMax: semilattice_order_fset max greater_eq greater
rewrites "semilattice_set.F max = Max" defines fMax = fMax.F proof - show"semilattice_order_fset max (\) (>)" by standard
show"semilattice_set.F max = Max" unfolding Max_def .. qed
end
lemma mono_fMax_commute: "mono f \ A \ {||} \ f (fMax A) = fMax (f |`| A)" by transfer (rule mono_Max_commute)
lemma mono_fMin_commute: "mono f \ A \ {||} \ f (fMin A) = fMin (f |`| A)" by transfer (rule mono_Min_commute)
lemma fMax_in[simp]: "A \ {||} \ fMax A |\| A" by transfer (rule Max_in)
lemma fMin_in[simp]: "A \ {||} \ fMin A |\| A" by transfer (rule Min_in)
lemma fMax_ge[simp]: "x |\| A \ x \ fMax A" by transfer (rule Max_ge)
lemma fMin_le[simp]: "x |\| A \ fMin A \ x" by transfer (rule Min_le)
lemma fMax_eqI: "(\y. y |\| A \ y \ x) \ x |\| A \ fMax A = x" by transfer (rule Max_eqI)
lemma fMin_eqI: "(\y. y |\| A \ x \ y) \ x |\| A \ fMin A = x" by transfer (rule Min_eqI)
lemma fMax_finsert[simp]: "fMax (finsert x A) = (if A = {||} then x else max x (fMax A))" by transfer simp
lemma fMin_finsert[simp]: "fMin (finsert x A) = (if A = {||} then x else min x (fMin A))" by transfer simp
context linorder begin
lemma fset_linorder_max_induct[case_names fempty finsert]: assumes"P {||}" and"\x S. \\y. y |\| S \ y < x; P S\ \ P (finsert x S)" shows"P S" proof - (* FIXME transfer and right_total vs. bi_total *) note Domainp_forall_transfer[transfer_rule] show ?thesis using assms by (transfer fixing: less) (auto intro: finite_linorder_max_induct) qed
lemma fset_linorder_min_induct[case_names fempty finsert]: assumes"P {||}" and"\x S. \\y. y |\| S \ y > x; P S\ \ P (finsert x S)" shows"P S" proof - (* FIXME transfer and right_total vs. bi_total *) note Domainp_forall_transfer[transfer_rule] show ?thesis using assms by (transfer fixing: less) (auto intro: finite_linorder_min_induct) qed
end
subsection \<open>Choice in fsets\<close>
lemma fset_choice: assumes"\x. x |\| A \ (\y. P x y)" shows"\f. \x. x |\| A \ P x (f x)" using assms by transfer metis
subsection \<open>Induction and Cases rules for fsets\<close>
lemma fset_exhaust [case_names empty insert, cases type: fset]: assumes fempty_case: "S = {||} \ P" and finsert_case: "\x S'. S = finsert x S' \ P" shows"P" using assms by transfer blast
lemma fset_induct [case_names empty insert]: assumes fempty_case: "P {||}" and finsert_case: "\x S. P S \ P (finsert x S)" shows"P S" proof - (* FIXME transfer and right_total vs. bi_total *) note Domainp_forall_transfer[transfer_rule] show ?thesis using assms by transfer (auto intro: finite_induct) qed
lemma fset_induct_stronger [case_names empty insert, induct type: fset]: assumes empty_fset_case: "P {||}" and insert_fset_case: "\x S. \x |\| S; P S\ \ P (finsert x S)" shows"P S" proof - (* FIXME transfer and right_total vs. bi_total *) note Domainp_forall_transfer[transfer_rule] show ?thesis using assms by transfer (auto intro: finite_induct) qed
lemma fset_card_induct: assumes empty_fset_case: "P {||}" and card_fset_Suc_case: "\S T. Suc (fcard S) = (fcard T) \ P S \ P T" shows"P S" proof (induct S) case empty show"P {||}"by (rule empty_fset_case) next case (insert x S) have h: "P S"by fact have"x |\| S" by fact thenhave"Suc (fcard S) = fcard (finsert x S)" by transfer auto thenshow"P (finsert x S)" using h card_fset_Suc_case by simp qed
lemma fset_strong_cases: obtains"xs = {||}"
| ys x where"x |\| ys" and "xs = finsert x ys" by auto
lemma fset_induct2: "P {||} {||} \
(\<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" by (induct xsa arbitrary: ysa; metis fset_induct_stronger)
subsection \<open>Lemmas depending on induction\<close>
lemma ffUnion_fsubset_iff: "ffUnion A |\| B \ fBall A (\x. x |\| B)" by (induction A) simp_all
subsection \<open>Setup for Lifting/Transfer\<close>
subsubsection \<open>Relator and predicator properties\<close>
lemma rel_fset_alt_def: "rel_fset R = (\A B. (\x.\y. x|\|A \ y|\|B \ R x y) \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))" by transfer' (metis (no_types, opaque_lifting) rel_set_def)
lemma finite_rel_set: assumes fin: "finite X""finite Z" assumes R_S: "rel_set (R OO S) X Z" shows"\Y. finite Y \ rel_set R X Y \ rel_set S Y Z" proof - obtain f g where f: "\x\X. R x (f x) \ (\z\Z. S (f x) z)" and g: "\z\Z. S (g z) z \ (\x\X. R x (g z))"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
