Theory FSet_Util (Isabelle2020: April 2020)

theory FSet_Util
  imports "HOL-Library.FSet" ― ‹Replace later with FSet from HOL.Library›
    Basic_Utils
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 fremove [code_abbrev]: "fremove x A = A |-| {|x|}"
  by transfer auto

lemma fminus [code]:
  "A |-| B = ffilter (λ x. x |∉| B) A"
  by transfer auto

lemma is_fempty [code_abbrev]: "is_fempty S ⟷ S = {||}"
  by transfer (auto simp: Set.is_empty_def)

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)"


text ‹
  Simproc for pulling ‹x = t› in ‹{x. … ∧ x = t ∧ …}›
  to the front (and similarly for ‹t = x›):
›

simproc_setup defined_fCollect ("{|x. P x ∧ Q x|}") = ‹
  fn _ => Quantifier1.rearrange_Collect
    (fn ctxt =>
      resolve_tac ctxt @{thms fCollect_cong} 1 THEN
      resolve_tac ctxt @{thms iffI} 1 THEN
      ALLGOALS
        (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
          DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
›

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"

print_translation ‹
  let
    val All_binder = Mixfix.binder_name \<^const_syntax>‹All›;
    val Ex_binder = Mixfix.binder_name \<^const_syntax>‹Ex›;
    val impl = \<^const_syntax>‹HOL.implies›;
    val conj = \<^const_syntax>‹HOL.conj›;
    val sbset = \<^const_syntax>‹subset›;
    val sbset_eq = \<^const_syntax>‹subset_eq›;

    val trans =
     [((All_binder, impl, sbset), \<^syntax_const>‹_setlessfAll›),
      ((All_binder, impl, sbset_eq), \<^syntax_const>‹_setlefAll›),
      ((Ex_binder, conj, sbset), \<^syntax_const>‹_setlessfEx›),
      ((Ex_binder, conj, sbset_eq), \<^syntax_const>‹_setlefEx›)];

    fun mk v (v', T) c n P =
      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
      then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P
      else raise Match;

    fun tr' q = (q, fn _ =>
      (fn [Const (\<^syntax_const>‹_bound›, _) $ Free (v, Type (\<^type_name>‹fset›, _)),
          Const (c, _) $
            (Const (d, _) $ (Const (\<^syntax_const>‹_bound›, _) $ Free (v', T)) $ n) $ P] =>
          (case AList.lookup (=) trans (q, c, d) of
            NONE => raise Match
          | SOME l => mk v (v', T) l n P)
        | _ => raise Match));
  in
    [tr' All_binder, tr' Ex_binder]
  end
›

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 (=))"
  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 (auto simp: list_all2_conv_all_nth cr_fset_def fset_of_list.rep_eq relcompp_apply dest!: in_set_idx)
     (metis nth_mem)


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

― ‹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 ftrancl_singelton [simp] = trancl_singelton[Transfer.transferred]
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_set = trancl_mono_set[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 = inj_on_trancl_map_both[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 in_fset_idx = in_set_idx[Transfer.transferred]
lemmas fsubseteq_fset_conv_nth[simp] = subseteq_set_conv_nth[Transfer.transferred]
lemmas mem_idx_fset_sound = mem_idx_sound[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

end

code_datatype fset_of_list



context
includes fset.lifting
begin

subsubsection ‹Implementation of fsets by lists›

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]
lemmas ftrancl_Un2_separatorE = trancl_Un2_separatorE[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)

lift_definition fmap_project :: "('a ⇒ 'b option) ⇒ 'a fset ⇒ 'b fset" is List.map_project
proof -
  fix f :: "'a ⇒ 'b option" and S :: "'a set"
  assume "finite S"
  then show "finite (List.map_project f S)"
    using finite.simps
    by induct (fastforce simp: List.map_project_def)+
qed

lemmas nftrancl_Zero [simp, code] = ntrancl_Zero[Transfer.transferred]
lemmas nftrancl_Suc [simp] = ntrancl_Suc'[Transfer.transferred]
lemma [code]: "nftrancl (Suc n) r = (let r' = nftrancl n r in r' |∪| r' |O| r)"
  by (auto simp: Let_def)

lemmas funion_fset_fold [code] = union_set_fold [Transfer.transferred]
lemmas ftrancl_fset_of_list_ntrancl [code] = trancl_set_ntrancl[Transfer.transferred]
lemmas fset_of_list_frelcomp [code] = set_relcomp[Transfer.transferred]
lemmas frelcomp_empty_ftrancl_simp = rel_comp_empty_trancl_simp[Transfer.transferred]


lemma fmap_project [code]:
  "fmap_project f (fset_of_list xs) = fset_of_list (List.map_filter f xs)"
  by transfer (auto simp add: map_project_def map_filter_def image_def)

lemma fImage_list [code]:
  "R |``| S = fmap_project (λ(x, y). if x |∈| S then Some y else None) R"
  by transfer (auto simp: List.map_project_def split: prod.split if_split_asm)


lemmas is_fempty_fset_of_list [code_unfold] = is_empty_set[Transfer.transferred]
lemmas fempty_fset [code_unfold] = empty_set[Transfer.transferred]
lemma [code_unfold]:
  "x |∈| fset_of_list xs ⟷ List.member xs x"
  by (simp_all add: member_def fset_of_list_elem)

lemmas finsert_code [code] = insert_code(1)[Transfer.transferred]
lemmas fremove_code [code] = remove_code(1)[Transfer.transferred]
lemmas ffilter_fset [code] = filter_set[Transfer.transferred]
lemmas fimage_fset [code] = image_set[Transfer.transferred]
lemmas finter_fset_filter[code] = inter_set_filter[Transfer.transferred]
text ‹A frequent case -- avoid intermediate sets›
lemma [code_unfold]:
  "fset_of_list xs |⊆| fset_of_list ys ⟷ list_all (λx. x |∈| fset_of_list ys) xs"
  by (auto simp: list_all_iff fset_of_list_elem)
lemmas fBall_fset[code_unfold] = Ball_set[Transfer.transferred]
lemmas fBex_fset [code_unfold] = Bex_set[Transfer.transferred]
lemmas card_fset [code_unfold] = card_set[Transfer.transferred]
lemmas fthe_elem_fset[code_unfold] = the_elem_set[Transfer.transferred]
lemmas fPow_fset [code_unfold] = Pow_set[Transfer.transferred]

lemma ffUnion [code]:
  "|⋃| (fset_of_list xs) = (fold (|∪|) xs {||})"
  by transfer  (auto simp: transfer_bforall_def Sup_set_fold)

lemma fSigma_code [code]:
  "fSigma A f = |⋃| ((λ x. (λ y. Pair x y) |`| f x) |`| A)"
  by auto

lemma fId_on_code[code]:
  "fId_on Q = (λ p. (p, p)) |`| Q"
  by auto

end

hide_const (open) fmap_project
declare fset_of_list.rep_eq[code]


(* 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)

definition less_eq_linorder_fset :: "('a :: linorder) fset ⇒ ('a :: linorder) fset ⇒ bool" where
  "less_eq_linorder_fset A B ⟷ (sorted_list_of_fset A) ≤ (sorted_list_of_fset B)"
definition less_linorder_fset :: "('a :: linorder) fset ⇒ ('a :: linorder) fset ⇒ bool" where
  "less_linorder_fset A B ⟷ (sorted_list_of_fset A) < (sorted_list_of_fset B)"

lemma fset_linorder: "class.linorder less_eq_linorder_fset less_linorder_fset"
proof
  fix x :: "'a fset" and y assume "less_eq_linorder_fset x y" "less_eq_linorder_fset y x"
  then show "x = y" using sorted_list_of_fset_simps
    by (auto simp: less_linorder_fset_def less_eq_linorder_fset_def dest: sorted_list_of_fset_id)
qed (auto simp: less_linorder_fset_def less_eq_linorder_fset_def)

end