Theory Regular_Tree_Relations.FSet_Utils

```theory FSet_Utils
imports "HOL-Library.FSet"
"HOL-Library.List_Lexorder"
Ground_Terms
begin

context
includes fset.lifting
begin

lift_definition fCollect :: "('a ⇒ bool) ⇒ 'a fset" is "λ P. if finite (Collect P) then Collect P else {}"
by auto

lift_definition fSigma :: "'a fset ⇒ ('a ⇒ 'b fset) ⇒ ('a × 'b) fset" is Sigma
by auto

lift_definition is_fempty :: "'a fset ⇒ bool" is Set.is_empty .
lift_definition fremove :: "'a ⇒ 'a fset ⇒ 'a fset" is Set.remove

lift_definition finj_on :: "('a ⇒ 'b) ⇒ 'a fset ⇒ bool" is inj_on .
lift_definition the_finv_into  :: "'a fset ⇒ ('a ⇒ 'b) ⇒ 'b ⇒ 'a" is the_inv_into .

lemma fCollect_memberI [intro!]:
"finite (Collect P) ⟹ P x ⟹ x |∈| fCollect P"
by transfer auto

lemma fCollect_member [iff]:
"x |∈| fCollect P ⟷ finite (Collect P) ∧ P x"
by transfer (auto split: if_splits)

lemma fCollect_cong: "(⋀x. P x = Q x) ⟹ fCollect P = fCollect Q"
by presburger
end

syntax
"_fColl" :: "pttrn ⇒ bool ⇒ 'a set"    ("(1{|_./ _|})")
translations
"{|x. P|}" ⇌ "CONST fCollect (λx. P)"

syntax (ASCII)
"_fCollect" :: "pttrn ⇒ 'a set ⇒ bool ⇒ 'a set"  ("(1{(_/|:| _)./ _})")
syntax
"_fCollect" :: "pttrn ⇒ 'a set ⇒ bool ⇒ 'a set"  ("(1{(_/ |∈| _)./ _})")
translations
"{p|:|A. P}" ⇀ "CONST fCollect (λp. p |∈| A ∧ P)"

syntax (ASCII)
"_fBall"       :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool"      ("(3ALL (_/|:|_)./ _)" [0, 0, 10] 10)
"_fBex"        :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool"      ("(3EX (_/|:|_)./ _)" [0, 0, 10] 10)

syntax (input)
"_fBall"       :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool"      ("(3! (_/|:|_)./ _)" [0, 0, 10] 10)
"_fBex"        :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool"      ("(3? (_/|:|_)./ _)" [0, 0, 10] 10)

syntax
"_fBall"       :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool"      ("(3∀(_/|∈|_)./ _)" [0, 0, 10] 10)
"_fBex"        :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool"      ("(3∃(_/|∈|_)./ _)" [0, 0, 10] 10)

translations
"∀x|∈|A. P" ⇌ "CONST fBall A (λx. P)"
"∃x|∈|A. P" ⇌ "CONST fBex A (λx. P)"

syntax (ASCII output)
"_setlessfAll" :: "[idt, 'a, bool] ⇒ bool"  ("(3ALL _|<|_./ _)"  [0, 0, 10] 10)
"_setlessfEx"  :: "[idt, 'a, bool] ⇒ bool"  ("(3EX _|<|_./ _)"  [0, 0, 10] 10)
"_setlefAll"   :: "[idt, 'a, bool] ⇒ bool"  ("(3ALL _|<=|_./ _)" [0, 0, 10] 10)
"_setlefEx"    :: "[idt, 'a, bool] ⇒ bool"  ("(3EX _|<=|_./ _)" [0, 0, 10] 10)

syntax
"_setlessfAll" :: "[idt, 'a, bool] ⇒ bool"   ("(3∀_|⊂|_./ _)"  [0, 0, 10] 10)
"_setlessfEx"  :: "[idt, 'a, bool] ⇒ bool"   ("(3∃_|⊂|_./ _)"  [0, 0, 10] 10)
"_setlefAll"   :: "[idt, 'a, bool] ⇒ bool"   ("(3∀_|⊆|_./ _)" [0, 0, 10] 10)
"_setlefEx"    :: "[idt, 'a, bool] ⇒ bool"   ("(3∃_|⊆|_./ _)" [0, 0, 10] 10)

translations
"∀A|⊂|B. P" ⇀ "∀A. A |⊂| B ⟶ P"
"∃A|⊂|B. P" ⇀ "∃A. A |⊂| B ∧ P"
"∀A|⊆|B. P" ⇀ "∀A. A |⊆| B ⟶ P"
"∃A|⊆|B. P" ⇀ "∃A. A |⊆| B ∧ P"

syntax
"_fSetcompr" :: "'a ⇒ idts ⇒ bool ⇒ 'a fset"    ("(1{|_ |/_./ _|})")

parse_translation ‹
let
val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", \<^const_syntax>‹Ex›));

fun nvars (Const (\<^syntax_const>‹_idts›, _) \$ _ \$ idts) = nvars idts + 1
| nvars _ = 1;

fun setcompr_tr ctxt [e, idts, b] =
let
val eq = Syntax.const \<^const_syntax>‹HOL.eq› \$ Bound (nvars idts) \$ e;
val P = Syntax.const \<^const_syntax>‹HOL.conj› \$ eq \$ b;
val exP = ex_tr ctxt [idts, P];
in Syntax.const \<^const_syntax>‹fCollect› \$ absdummy dummyT exP end;

in [(\<^syntax_const>‹_fSetcompr›, setcompr_tr)] end
›

print_translation ‹
[Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>‹fBall› \<^syntax_const>‹_fBall›,
Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>‹fBex› \<^syntax_const>‹_fBex›]
› ― ‹to avoid eta-contraction of body›

print_translation ‹
let
val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (\<^const_syntax>‹Ex›, "DUMMY"));

fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
let
fun check (Const (\<^const_syntax>‹Ex›, _) \$ Abs (_, _, P), n) = check (P, n + 1)
| check (Const (\<^const_syntax>‹HOL.conj›, _) \$
(Const (\<^const_syntax>‹HOL.eq›, _) \$ Bound m \$ e) \$ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (=) (0 upto (n - 1), add_loose_bnos (e, 0, []))
| check _ = false;

fun tr' (_ \$ abs) =
let val _ \$ idts \$ (_ \$ (_ \$ _ \$ e) \$ Q) = ex_tr' ctxt [abs]
in Syntax.const \<^syntax_const>‹_fSetcompr› \$ e \$ idts \$ Q end;
in
if check (P, 0) then tr' P
else
let
val (x as _ \$ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
val M = Syntax.const \<^syntax_const>‹_fColl› \$ x \$ t;
in
case t of
Const (\<^const_syntax>‹HOL.conj›, _) \$
(Const (\<^const_syntax>‹fmember›, _) \$
(Const (\<^syntax_const>‹_bound›, _) \$ Free (yN, _)) \$ A) \$ P =>
if xN = yN then Syntax.const \<^syntax_const>‹_fCollect› \$ x \$ A \$ P else M
| _ => M
end
end;
in [(\<^const_syntax>‹fCollect›, setcompr_tr')] end
›

syntax
"_fSigma" :: "pttrn ⇒ 'a fset ⇒ 'b fset ⇒ ('a × 'b) set"  ("(3fSIGMA _|:|_./ _)" [0, 0, 10] 10)
translations
"fSIGMA x|:|A. B" ⇌ "CONST fSigma A (λx. B)"

notation
ffUnion ("|⋃|")

context
includes fset.lifting
begin

lemma right_total_cr_fset [transfer_rule]:
"right_total cr_fset"
by (auto simp: cr_fset_def right_total_def)

lemma bi_unique_cr_fset [transfer_rule]:
"bi_unique cr_fset"
by (auto simp: bi_unique_def cr_fset_def fset_inject)

lemma right_total_pcr_fset_eq [transfer_rule]:
"right_total (pcr_fset (=))"

lemma bi_unique_pcr_fset [transfer_rule]:
"bi_unique (pcr_fset (=))"

lemma set_fset_of_list_transfer [transfer_rule]:
"rel_fun (list_all2 A) (pcr_fset A) set fset_of_list"
unfolding pcr_fset_def rel_set_def rel_fun_def
by (force simp: list_all2_conv_all_nth in_set_conv_nth cr_fset_def fset_of_list.rep_eq relcompp_apply)

lemma fCollectD: "a |∈| {|x . P x|} ⟹ P a"
by transfer (auto split: if_splits)

lemma fCollectI: "P a ⟹ finite (Collect P) ⟹ a |∈| {| x. P x|}"
by (auto intro: fCollect_memberI)

lemma fCollect_fempty_eq [simp]: "fCollect P = {||} ⟷ (∀x. ¬ P x) ∨ infinite (Collect P)"
by auto

lemma fempty_fCollect_eq [simp]: "{||} = fCollect P ⟷ (∀x. ¬ P x) ∨ infinite (Collect P)"
by auto

lemma fset_image_conv:
"{f x | x. x |∈| T} = fset (f |`| T)"
by transfer auto

lemma fimage_def:
"f |`| A = {| y. ∃x|∈|A. y = f x |}"
by transfer auto

lemma ffilter_simp: "ffilter P A = {a |∈| A. P a}"
by transfer auto

lemmas fset_list_fsubset_eq_nth_conv = set_list_subset_eq_nth_conv[Transfer.transferred]
lemmas mem_idx_fset_sound = mem_idx_sound[Transfer.transferred]
― ‹Dealing with fset products›

abbreviation fTimes :: "'a fset ⇒ 'b fset ⇒ ('a × 'b) fset"  (infixr "|×|" 80)
where "A |×| B ≡ fSigma A (λ_. B)"

lemma fSigma_repeq:
"fset (A |×| B) = fset A × fset B"
by (transfer) auto

lemmas fSigmaI [intro!] = SigmaI[Transfer.transferred]
lemmas fSigmaE [elim!] = SigmaE[Transfer.transferred]
lemmas fSigmaE2 = SigmaE2[Transfer.transferred]
lemmas fSigma_cong = Sigma_cong[Transfer.transferred]
lemmas fSigma_mono = Sigma_mono[Transfer.transferred]
lemmas fSigma_empty1 [simp] = Sigma_empty1[Transfer.transferred]
lemmas fSigma_empty2 [simp] = Sigma_empty2[Transfer.transferred]
lemmas fmem_Sigma_iff [iff] = mem_Sigma_iff[Transfer.transferred]
lemmas fmem_Times_iff = mem_Times_iff[Transfer.transferred]
lemmas fSigma_empty_iff = Sigma_empty_iff[Transfer.transferred]
lemmas fTimes_subset_cancel2 = Times_subset_cancel2[Transfer.transferred]
lemmas fTimes_eq_cancel2 = Times_eq_cancel2[Transfer.transferred]
lemmas fUN_Times_distrib = UN_Times_distrib[Transfer.transferred]
lemmas fsplit_paired_Ball_Sigma [simp, no_atp] = split_paired_Ball_Sigma[Transfer.transferred]
lemmas fsplit_paired_Bex_Sigma [simp, no_atp] = split_paired_Bex_Sigma[Transfer.transferred]
lemmas fSigma_Un_distrib1 = Sigma_Un_distrib1[Transfer.transferred]
lemmas fSigma_Un_distrib2 = Sigma_Un_distrib2[Transfer.transferred]
lemmas fSigma_Int_distrib1 = Sigma_Int_distrib1[Transfer.transferred]
lemmas fSigma_Int_distrib2 = Sigma_Int_distrib2[Transfer.transferred]
lemmas fSigma_Diff_distrib1 = Sigma_Diff_distrib1[Transfer.transferred]
lemmas fSigma_Diff_distrib2 = Sigma_Diff_distrib2[Transfer.transferred]
lemmas fSigma_Union = Sigma_Union[Transfer.transferred]
lemmas fTimes_Un_distrib1 = Times_Un_distrib1[Transfer.transferred]
lemmas fTimes_Int_distrib1 = Times_Int_distrib1[Transfer.transferred]
lemmas fTimes_Diff_distrib1 = Times_Diff_distrib1[Transfer.transferred]
lemmas fTimes_empty [simp] = Times_empty[Transfer.transferred]
lemmas ftimes_subset_iff = times_subset_iff[Transfer.transferred]
lemmas ftimes_eq_iff = times_eq_iff[Transfer.transferred]
lemmas ffst_image_times [simp] = fst_image_times[Transfer.transferred]
lemmas fsnd_image_times [simp] = snd_image_times[Transfer.transferred]
lemmas fsnd_image_Sigma = snd_image_Sigma[Transfer.transferred]
lemmas finsert_Times_insert = insert_Times_insert[Transfer.transferred]
lemmas fTimes_Int_Times = Times_Int_Times[Transfer.transferred]
lemmas fimage_paired_Times = image_paired_Times[Transfer.transferred]
lemmas fproduct_swap = product_swap[Transfer.transferred]
lemmas fswap_product = swap_product[Transfer.transferred]
lemmas fsubset_fst_snd = subset_fst_snd[Transfer.transferred]
lemmas map_prod_ftimes = map_prod_times[Transfer.transferred]

lemma fCollect_case_prod [simp]:
"{|(a, b). P a ∧ Q b|} = fCollect P |×| fCollect Q"
by transfer (auto dest: finite_cartesian_productD1 finite_cartesian_productD2)
lemma fCollect_case_prodD:
"x |∈| {|(x, y). A x y|} ⟹ A (fst x) (snd x)"
by auto

(*FIX *)
lemmas fCollect_case_prod_Sigma = Collect_case_prod_Sigma[Transfer.transferred]
lemmas ffst_image_Sigma = fst_image_Sigma[Transfer.transferred]
lemmas fimage_split_eq_Sigma = image_split_eq_Sigma[Transfer.transferred]

― ‹Dealing with transitive closure›

lift_definition ftrancl :: "('a × 'a) fset ⇒ ('a × 'a) fset"  ("(_|⇧+|)" [1000] 999) is trancl
by auto

lemmas fr_into_trancl [intro, Pure.intro] = r_into_trancl[Transfer.transferred]
lemmas ftrancl_into_trancl [Pure.intro] = trancl_into_trancl[Transfer.transferred]
lemmas ftrancl_induct[consumes 1, case_names Base Step] = trancl.induct[Transfer.transferred]
lemmas ftrancl_mono = trancl_mono[Transfer.transferred]
lemmas ftrancl_trans[trans] = trancl_trans[Transfer.transferred]
lemmas ftrancl_empty [simp] = trancl_empty [Transfer.transferred]
lemmas ftranclE[cases set: ftrancl] = tranclE[Transfer.transferred]
lemmas converse_ftrancl_induct[consumes 1, case_names Base Step] = converse_trancl_induct[Transfer.transferred]
lemmas converse_ftranclE = converse_tranclE[Transfer.transferred]
lemma in_ftrancl_UnI:
"x |∈| R|⇧+| ∨ x |∈| S|⇧+| ⟹ x |∈| (R |∪| S)|⇧+|"
by transfer (auto simp add: trancl_mono)

lemma ftranclD:
"(x, y) |∈| R|⇧+| ⟹ ∃z. (x, z) |∈| R ∧ (z = y ∨ (z, y) |∈| R|⇧+|)"
by (induct rule: ftrancl_induct) (auto, meson ftrancl_into_trancl)

lemma ftranclD2:
"(x, y) |∈| R|⇧+| ⟹ ∃z. (x = z ∨ (x, z) |∈| R|⇧+|) ∧ (z, y) |∈| R"
by (induct rule: ftrancl_induct) auto

lemma not_ftrancl_into:
"(x, z) |∉| r|⇧+| ⟹ (y, z) |∈| r ⟹ (x, y) |∉| r|⇧+|"
by transfer (auto simp add: trancl.trancl_into_trancl)
lemmas ftrancl_map_both_fRestr = trancl_map_both_Restr[Transfer.transferred]
lemma ftrancl_map_both_fsubset:
"finj_on f X ⟹ R |⊆| X |×| X ⟹ (map_both f |`| R)|⇧+| = map_both f |`| R|⇧+|"
using ftrancl_map_both_fRestr[of f X R]
lemmas ftrancl_map_prod_mono = trancl_map_prod_mono[Transfer.transferred]
lemmas ftrancl_map = trancl_map[Transfer.transferred]

lemmas ffUnion_iff [simp] = Union_iff[Transfer.transferred]
lemmas ffUnionI [intro] = UnionI[Transfer.transferred]
lemmas fUn_simps [simp] = UN_simps[Transfer.transferred]

(* TODO Diff *)
lemmas fINT_simps [simp] = INT_simps[Transfer.transferred]

lemmas fUN_ball_bex_simps [simp] = UN_ball_bex_simps[Transfer.transferred]

(* List *)
lemmas in_fset_conv_nth = in_set_conv_nth[Transfer.transferred]
lemmas fnth_mem [simp] = nth_mem[Transfer.transferred]
lemmas distinct_sorted_list_of_fset = distinct_sorted_list_of_set [Transfer.transferred]
lemmas fcard_fset = card_set[Transfer.transferred]
lemma upt_fset:
"fset_of_list [i..<j] = fCollect (λ n. i ≤ n ∧ n < j)"
by (induct j arbitrary: i) auto

(* Restr *)
abbreviation fRestr :: "('a × 'a) fset ⇒ 'a fset ⇒ ('a × 'a) fset" where
"fRestr r A ≡ r |∩| (A |×| A)"

(* Identity on set*)

lift_definition fId_on :: "'a fset ⇒ ('a × 'a) fset" is Id_on
using Id_on_subset_Times finite_subset by fastforce

lemmas fId_on_empty [simp] = Id_on_empty [Transfer.transferred]
lemmas fId_on_eqI = Id_on_eqI [Transfer.transferred]
lemmas fId_onI [intro!] = Id_onI [Transfer.transferred]
lemmas fId_onE [elim!] = Id_onE [Transfer.transferred]
lemmas fId_on_iff = Id_on_iff [Transfer.transferred]
lemmas fId_on_fsubset_fTimes = Id_on_subset_Times [Transfer.transferred]

(* Converse*)
lift_definition fconverse :: "('a × 'b) fset ⇒ ('b × 'a) fset"  ("(_|¯|)" [1000] 999) is converse by auto

lemmas fconverseI [sym] = converseI [Transfer.transferred]
lemmas fconverseD [sym] = converseD [Transfer.transferred]
lemmas fconverseE [elim!] = converseE [Transfer.transferred]
lemmas fconverse_iff [iff] = converse_iff[Transfer.transferred]
lemmas fconverse_fconverse [simp] = converse_converse[Transfer.transferred]
lemmas fconverse_empty[simp] = converse_empty[Transfer.transferred]

(* injectivity *)

lemmas finj_on_def' = inj_on_def[Transfer.transferred]
lemmas fsubset_finj_on = subset_inj_on[Transfer.transferred]
lemmas the_finv_into_f_f = the_inv_into_f_f[Transfer.transferred]
lemmas f_the_finv_into_f = f_the_inv_into_f[Transfer.transferred]
lemmas the_finv_into_into = the_inv_into_into[Transfer.transferred]
lemmas the_finv_into_onto [simp] = the_inv_into_onto[Transfer.transferred]
lemmas the_finv_into_f_eq = the_inv_into_f_eq[Transfer.transferred]
lemmas the_finv_into_comp = the_inv_into_comp[Transfer.transferred]
lemmas finj_on_the_finv_into = inj_on_the_inv_into [Transfer.transferred]
lemmas finj_on_fUn = inj_on_Un[Transfer.transferred]

lemma finj_Inl_Inr:
"finj_on Inl A" "finj_on Inr A"
by (transfer, auto)+
lemma finj_CInl_CInr:
"finj_on CInl A" "finj_on CInr A"
using finj_Inl_Inr by force+

lemma finj_Some:
"finj_on Some A"
by (transfer, auto)

(* Image *)

lift_definition fImage :: "('a × 'b) fset ⇒ 'a fset ⇒ 'b fset" (infixr "|``|" 90) is Image
using finite_Image by force

lemmas fImage_iff = Image_iff[Transfer.transferred]
lemmas fImage_singleton_iff [iff] = Image_singleton_iff[Transfer.transferred]
lemmas fImageI [intro] = ImageI[Transfer.transferred]
lemmas ImageE [elim!] = ImageE[Transfer.transferred]
lemmas frev_ImageI = rev_ImageI[Transfer.transferred]
lemmas fImage_empty1 [simp] = Image_empty1[Transfer.transferred]
lemmas fImage_empty2 [simp] = Image_empty2[Transfer.transferred]
lemmas fImage_fInt_fsubset = Image_Int_subset[Transfer.transferred]
lemmas fImage_fUn = Image_Un[Transfer.transferred]
lemmas fUn_fImage = Un_Image[Transfer.transferred]
lemmas fImage_fsubset = Image_subset[Transfer.transferred]
lemmas fImage_eq_fUN = Image_eq_UN[Transfer.transferred]
lemmas fImage_mono = Image_mono[Transfer.transferred]
lemmas fImage_fUN = Image_UN[Transfer.transferred]
lemmas fUN_fImage = UN_Image[Transfer.transferred]
lemmas fSigma_fImage = Sigma_Image[Transfer.transferred]

(* fix us *)
lemmas fImage_singleton = Image_singleton[Transfer.transferred]
lemmas fImage_Id_on [simp] = Image_Id_on[Transfer.transferred]
lemmas fImage_Id [simp] = Image_Id[Transfer.transferred]
lemmas fImage_fInt_eq = Image_Int_eq[Transfer.transferred]
lemmas fImage_fsubset_eq = Image_subset_eq[Transfer.transferred]
lemmas fImage_fCollect_case_prod [simp] = Image_Collect_case_prod[Transfer.transferred]
lemmas fImage_fINT_fsubset = Image_INT_subset[Transfer.transferred]
(* Misc *)
lemmas term_fset_induct = term.induct[Transfer.transferred]
lemmas fmap_prod_fimageI = map_prod_imageI[Transfer.transferred]
lemmas finj_on_eq_iff = inj_on_eq_iff[Transfer.transferred]
lemmas prod_fun_fimageE = prod_fun_imageE[Transfer.transferred]

lemma rel_set_cr_fset:
"rel_set cr_fset = (λ A B. A = fset ` B)"
proof -
have "rel_set cr_fset A B ⟷ A = fset ` B" for A B
by (auto simp: image_def rel_set_def cr_fset_def )
then show ?thesis by blast
qed
lemma pcr_fset_cr_fset:
"pcr_fset cr_fset = (λ x y. x = fset (fset |`| y))"
unfolding pcr_fset_def rel_set_cr_fset
unfolding cr_fset_def
by (auto simp: image_def relcompp_apply)

lemma sorted_list_of_fset_id:
"sorted_list_of_fset x = sorted_list_of_fset y ⟹ x = y"
by (metis sorted_list_of_fset_simps(2))

(*end *)

lemmas fBall_def = Ball_def[Transfer.transferred]
lemmas fBex_def = Bex_def[Transfer.transferred]
lemmas fCollectE = fCollectD [elim_format]
lemma fCollect_conj_eq:
"finite (Collect P) ⟹ finite (Collect Q) ⟹ {|x. P x ∧ Q x|} = fCollect P |∩| fCollect Q"
by auto

lemma finite_ntrancl:
"finite R ⟹ finite (ntrancl n R)"
by (induct n) auto

lift_definition nftrancl :: "nat ⇒ ('a × 'a) fset ⇒ ('a × 'a) fset" is ntrancl
by (intro finite_ntrancl) simp

lift_definition frelcomp :: "('a × 'b) fset ⇒ ('b × 'c) fset ⇒ ('a × 'c) fset" (infixr "|O|" 75) is relcomp
by (intro finite_relcomp) simp

lemmas frelcompE[elim!] = relcompE[Transfer.transferred]
lemmas frelcompI[intro] = relcompI[Transfer.transferred]
lemma fId_on_frelcomp_id:
"fst |`| R |⊆| S ⟹ fId_on S |O| R = R"
by (auto intro!: frelcompI)
lemma fId_on_frelcomp_id2:
"snd |`| R |⊆| S ⟹ R |O| fId_on S = R"
by (auto intro!: frelcompI)

lemmas fimage_fset = image_set[Transfer.transferred]
lemmas ftrancl_Un2_separatorE = trancl_Un2_separatorE[Transfer.transferred]

(* finite vars of term finite function symbols of terms *)

lemma finite_funs_term: "finite (funs_term t)" by (induct t) auto
lemma finite_funas_term: "finite (funas_term t)" by (induct t) auto
lemma finite_vars_ctxt: "finite (vars_ctxt C)" by (induct C) auto

lift_definition ffuns_term :: "('f, 'v) term ⇒ 'f fset" is funs_term using finite_funs_term
by blast
lift_definition fvars_term :: "('f, 'v) term ⇒ 'v fset" is vars_term by simp
lift_definition fvars_ctxt :: "('f, 'v) ctxt ⇒ 'v fset" is vars_ctxt by (simp add: finite_vars_ctxt)

lemmas fvars_term_ctxt_apply [simp] = vars_term_ctxt_apply[Transfer.transferred]
lemmas fvars_term_of_gterm [simp] = vars_term_of_gterm[Transfer.transferred]
lemmas ground_fvars_term_empty [simp] = ground_vars_term_empty[Transfer.transferred]

lemma ffuns_term_Var [simp]: "ffuns_term (Var x) = {||}"
by transfer auto
lemma fffuns_term_Fun [simp]: "ffuns_term (Fun f ts) = |⋃| (ffuns_term |`| fset_of_list ts) |∪| {|f|}"
by transfer auto

lemma fvars_term_Var [simp]: "fvars_term (Var x) = {|x|}"
by transfer auto
lemma fvars_term_Fun [simp]: "fvars_term (Fun f ts) = |⋃| (fvars_term |`| fset_of_list ts)"
by transfer auto

lift_definition ffunas_term :: "('f, 'v) term ⇒ ('f × nat) fset" is funas_term
lift_definition ffunas_gterm :: "'f gterm ⇒ ('f × nat) fset" is funas_gterm

lemmas ffunas_term_simps [simp] = funas_term.simps[Transfer.transferred]
lemmas ffunas_gterm_simps [simp] = funas_gterm.simps[Transfer.transferred]
lemmas ffunas_term_of_gterm_conv = funas_term_of_gterm_conv[Transfer.transferred]
lemmas ffunas_gterm_gterm_of_term = funas_gterm_gterm_of_term[Transfer.transferred]

lemma sorted_list_of_fset_fimage_dist:
"sorted_list_of_fset (f |`| A) = sort (remdups (map f (sorted_list_of_fset A)))"
by (auto simp: sorted_list_of_fset.rep_eq simp flip: sorted_list_of_set_sort_remdups)

end

(* Move me *)
lemma finite_snd [intro]:
"finite S ⟹ finite {x. (y, x) ∈ S}"
by (induct S rule: finite.induct) auto

lemma finite_Collect_less_eq:
"Q ≤ P ⟹ finite (Collect P) ⟹ finite (Collect Q)"
by (metis (full_types) Ball_Collect infinite_iff_countable_subset rev_predicate1D)

datatype 'a FSet_Lex_Wrapper = Wrapp (ex: "'a fset")

lemma inj_FSet_Lex_Wrapper: "inj Wrapp"
unfolding inj_def by auto

lemmas ftrancl_map_both = inj_on_trancl_map_both[Transfer.transferred]

instantiation FSet_Lex_Wrapper :: (linorder) linorder
begin

definition less_eq_FSet_Lex_Wrapper :: "('a :: linorder) FSet_Lex_Wrapper ⇒ 'a FSet_Lex_Wrapper ⇒ bool"
where "less_eq_FSet_Lex_Wrapper S T =
(let S' = sorted_list_of_fset (ex S) in
let T' = sorted_list_of_fset (ex T) in
S' ≤ T')"

definition less_FSet_Lex_Wrapper :: "'a FSet_Lex_Wrapper ⇒ 'a FSet_Lex_Wrapper ⇒ bool"
where "less_FSet_Lex_Wrapper S T =
(let S' = sorted_list_of_fset (ex S) in
let T' = sorted_list_of_fset (ex T) in
S' < T')"

instance by (intro_classes)
(auto simp: less_eq_FSet_Lex_Wrapper_def less_FSet_Lex_Wrapper_def ex_def FSet_Lex_Wrapper.expand dest: sorted_list_of_fset_id)
end

end```