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
  by (simp add: remove_def)

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_syntaxEx));

    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_syntaxHOL.eq $ Bound (nvars idts) $ e;
        val P = Syntax.const const_syntaxHOL.conj $ eq $ b;
        val exP = ex_tr ctxt [idts, P];
      in Syntax.const const_syntaxfCollect $ absdummy dummyT exP end;

  in [(syntax_const‹_fSetcompr›, setcompr_tr)] end

print_translation [Syntax_Trans.preserve_binder_abs2_tr' const_syntaxfBall syntax_const‹_fBall›,
  Syntax_Trans.preserve_binder_abs2_tr' const_syntaxfBex syntax_const‹_fBex›] ― ‹to avoid eta-contraction of body›

print_translation let
  val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (const_syntaxEx, "DUMMY"));

  fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
    let
      fun check (Const (const_syntaxEx, _) $ Abs (_, _, P), n) = check (P, n + 1)
        | check (Const (const_syntaxHOL.conj, _) $
              (Const (const_syntaxHOL.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_syntaxHOL.conj, _) $
              (Const (const_syntaxfmember, _) $
                (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_syntaxfCollect, 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 (=))"
  by (simp add: right_total_cr_fset fset.pcr_cr_eq)

lemma bi_unique_pcr_fset [transfer_rule]:
  "bi_unique (pcr_fset (=))"
  by (simp add: fset.pcr_cr_eq bi_unique_cr_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 fSigmaD1 = SigmaD1[Transfer.transferred]
lemmas fSigmaD2 = SigmaD2[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]
  by (simp add: inf_absorb1)
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
  by (simp add: finite_funas_term)
lift_definition ffunas_gterm :: "'f gterm  ('f × nat) fset" is funas_gterm
  by (simp add: finite_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