theory ML_Utils
imports
  "HOL-Library.FSet"
  "Dict_Construction.Dict_Construction"
begin

ML_file "utils.ML"

ML‹
fun econtr_tac neg_thms ctxt =
  let
    val neg_thms = map (fn thm => @{thm notE} OF [thm]) neg_thms
  in SOLVED' (eresolve_tac ctxt neg_thms) end

(* from HOL.thy *)
fun eval_tac ctxt =
  let val conv = Code_Runtime.dynamic_holds_conv ctxt
  in
    CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
    resolve_tac ctxt [TrueI]
  end
›

lemma norm_all_conjunction:
  "⋀P Q. ((⋀x. PROP P x) &&& PROP Q) ≡ (⋀x. PROP P x &&& PROP Q)"
  "⋀P Q. (PROP P &&& (⋀x. PROP Q x)) ≡ (⋀x. PROP P &&& PROP Q x)"
proof -
  show "((⋀x. PROP P x) &&& PROP Q) ≡ (⋀x. PROP P x &&& PROP Q)" for P Q
    proof
      fix x
      assume "(⋀x. PROP P x) &&& PROP Q"
      note Pure.conjunctionD1[OF this, rule_format] Pure.conjunctionD2[OF this]
      thus "PROP P x &&& PROP Q" .
    next
      assume "(⋀x. PROP P x &&& PROP Q)"
      note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this]
      thus "(⋀x. PROP P x) &&& PROP Q" .
    qed
next
  show "(PROP P &&& (⋀x. PROP Q x)) ≡ (⋀x. PROP P &&& PROP Q x)" for P Q
    proof
      fix x
      assume "PROP P &&& (⋀x. PROP Q x)"
      note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this, rule_format]
      thus "PROP P &&& PROP Q x" .
    next
      assume "(⋀x. PROP P &&& PROP Q x)"
      note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this]
      thus "PROP P &&& (⋀x. PROP Q x)" .
    qed
qed

ML‹
fun norm_all_conjunction_tac ctxt =
  CONVERSION (repeat1_conv (Dict_Construction_Util.changed_conv (Conv.top_sweep_conv
    (K (Conv.rewrs_conv @{thms norm_all_conjunction})) ctxt)))
›

end

fun repeat1_conv cv = cv then_conv Conv.repeat_conv cv

fun init [] = error "empty list"
  | init [_] = []
  | init (x :: xs) = x :: init xs

fun last [] = error "empty list"
  | last [x] = x
  | last (_ :: xs) = last xs

val unvarify_typ =
  let
    fun aux (TVar ((name, idx), sort)) = TFree (name ^ Value.print_int idx, sort)
      | aux t = t
  in map_atyps aux end

fun all_consts (Const (name, typ)) = [(name, typ)]
  | all_consts (t $ u) = union (op =) (all_consts t) (all_consts u)
  | all_consts (Abs (_, _, t)) = all_consts t
  | all_consts _ = []

fun induct_of_bnf_const ctxt const =
  let
    open Dict_Construction_Util

    val (name, _) = dest_Const const

    fun cmp {T, ...} (Const (name', _)) = if name = name' then SOME T else NONE
      | cmp _ _ = NONE

    fun is_disc_or_sel (sugar as {discs, selss, ...}) =
      maps (map (cmp sugar)) selss @ map (cmp sugar) discs

    val Ts =
      Ctr_Sugar.ctr_sugars_of ctxt
      |> maps is_disc_or_sel
      |> cat_options
  in
    case Ts of
      (Type (typ_name, _) :: _) =>
        BNF_FP_Def_Sugar.fp_sugar_of ctxt typ_name
        |> Option.mapPartial #fp_co_induct_sugar
        |> Option.map #co_inducts
    | _ => NONE
  end

theory Compiler_Utils
imports
  "HOL-Library.Monad_Syntax"
  "HOL-Library.FSet"
  "HOL-Library.Finite_Map"
begin

section ‹Miscellaneous›

notation undefined ("❖")

lemma distinct_sorted_list_of_fset[simp, intro]: "distinct (sorted_list_of_fset S)"
including fset.lifting
by transfer (rule distinct_sorted_list_of_set)

lemma sum_nat_le_single:
  fixes x :: nat
  assumes y: "y ∈ S" and x: "x ≤ f y" and finite: "finite S"
  shows "x ≤ sum f S"
proof -
  have "sum f S = sum f (insert y S)"
    using y by (metis insert_absorb)
  with finite have "sum f S = f y + sum f (S - {y})"
    by (metis sum.insert_remove)
  with x show ?thesis
    by linarith
qed

lemma sum_nat_less_single:
  fixes x :: nat
  assumes y: "y ∈ S" and x: "x < f y" and finite: "finite S"
  shows "x < sum f S"
proof -
  have "sum f S = sum f (insert y S)"
    using y by (metis insert_absorb)
  with finite have "sum f S = f y + sum f (S - {y})"
    by (metis sum.insert_remove)
  with x show ?thesis
    by linarith
qed

lemma prod_BallI: "(⋀a b. (a, b) ∈ M ⟹ P a b) ⟹ Ball M (λ(a, b). P a b)"
by auto

lemma fset_map_snd_id:
  assumes "⋀a b e. (a, b) ∈ fset cs ⟹ f a b = b"
  shows "(λ(a, b). (a, f a b)) |`| cs = cs"
proof -
  have "(λ(a, b). (a, f a b)) |`| cs = id |`| cs"
    proof (rule fset.map_cong0, safe)
      fix a b
      assume "(a, b) ∈ fset cs"
      hence "f a b = b"
        using assms by auto
      thus "(a, f a b) = id (a, b)"
        by simp
    qed
  thus ?thesis
    by simp
qed

lemmas disj_cases = disjE[case_names 1 2, consumes 1]

lemma case_prod_twice: "case_prod f (case_prod (λa b. (g a b, h a b)) x) = case_prod (λa b. f (g a b) (h a b)) x"
by (simp add: split_beta)

lemma map_of_map_keyed:
  "map_of (map (λ(k, v). (k, f k v)) xs) = (λk. map_option (f k) (map_of xs k))"
  by (induction xs) (auto simp: fun_eq_iff)

locale rekey =
  fixes f :: "'a ⇒ 'b"
  assumes bij: "bij f"
begin

lemma map_of_rekey:
  "map_of (map (λ(k, v). (f k, g k v)) xs) k = map_option (g (inv f k)) (map_of xs (inv f k))"
using bij
by (induction xs) (auto simp: bij_def surj_f_inv_f)

lemma map_of_rekey': "map_of (map (map_prod f g) xs) k = map_option g (map_of xs (inv f k))"
unfolding map_prod_def
by (rule map_of_rekey)

lemma fst_distinct: "distinct (map fst xs) ⟹ distinct (map (λ(k, _). f k) xs)"
proof (induction xs)
  case Cons
  thus ?case
    apply (auto split: prod.splits)
    using bij unfolding bij_def
    by (metis fst_conv injD rev_image_eqI)
qed auto

lemma inv: "rekey (inv f)"
apply standard
using bij
by (simp add: bij_imp_bij_inv)

end

section ‹Finite sets›

lemma fset_eq_empty_iff: "M = {||} ⟷ (∀x. x |∉| M)"
by auto

context
  includes fset.lifting
begin

lemma fbind_subset_eqI: "fBall S (λs. f s |⊆| T) ⟹ fbind S f |⊆| T"
by transfer' fastforce

lemma prod_fBallI: "(⋀a b. (a, b) |∈| M ⟹ P a b) ⟹ fBall M (λ(a, b). P a b)"
by transfer (rule prod_BallI)

lemma ffUnion_subset_elem: "x |∈| X ⟹ x |⊆| ffUnion X"
including fset.lifting
by transfer auto

lemma fbindE:
  assumes "x |∈| fbind S f"
  obtains s where "x |∈| f s" "s |∈| S"
using assms by transfer' auto

lemma ffUnion_least_rev: "ffUnion A |⊆| C ⟹ fBall A (λX. X |⊆| C)"
by transfer blast

lemma inj_on_fimage_set_diff:
  assumes "inj_on f (fset C)" "A |⊆| C" "B |⊆| C"
  shows "f |`| (A - B) = f |`| A - f |`| B"
using assms
by transfer (meson Diff_subset inj_on_image_set_diff order_trans)

lemma list_all_iff_fset: "list_all P xs ⟷ fBall (fset_of_list xs) P"
by transfer (rule list_all_iff)

lemma fbind_fun_funion: "fbind M (λx. f x |∪| g x) = fbind M f |∪| fbind M g"
by transfer' auto

end

lemma funion_strictE:
  assumes "c |∈| A |∪| B"
  obtains (A) "c |∈| A" | (B) "c |∉| A" "c |∈| B"
using assms by auto

lemma max_decr:
  fixes X :: "nat set"
  assumes "∃x ∈ X. x ≥ k" "finite X"
  shows "Max ((λx. x - k) ` X) = Max X - k"
proof (rule mono_Max_commute[symmetric])
  show "mono (λx. x - k)"
    by (rule monoI) linarith
  show "finite X"
    by fact
  show "X ≠ {}"
    using assms by auto
qed

lemma max_ex_gr: "∃x ∈ X. k < x ⟹ finite X ⟹ X ≠ {} ⟹ k < Max X"
by (simp add: Max_gr_iff)

context includes fset.lifting begin

lemma fmax_decr:
  fixes X :: "nat fset"
  assumes "fBex X (λx. x ≥ k)"
  shows "fMax ((λx. x - k) |`| X) = fMax X - k"
using assms by transfer (rule max_decr)

lemma fmax_ex_gr: "fBex X (λx. k < x) ⟹ X ≠ {||} ⟹ k < fMax X"
by transfer (rule max_ex_gr)

lemma fMax_le: "fBall M (λx. x ≤ k) ⟹ M ≠ {||} ⟹ fMax M ≤ k"
by transfer auto

end

section ‹Sets›

subsection ‹Code setup trickery›

definition compress :: "'a set ⇒ 'a set" where
"compress = id"

lemma [code]: "compress (set xs) = set (remdups xs)"
unfolding compress_def id_apply by simp

definition the_elem' :: "'a::linorder set ⇒ 'a" where
"the_elem' S = the_elem (set (sorted_list_of_set S))"

lemma the_elem_id: "finite S ⟹ the_elem' S = the_elem S"
unfolding the_elem'_def
by auto

context
  includes fset.lifting
begin

lift_definition fcompress :: "'a fset ⇒ 'a fset" is compress
unfolding compress_def by simp

lemma fcompress_eq[simp]: "fcompress M = M"
by transfer' (auto simp: compress_def)

lift_definition fthe_elem' :: "'a::linorder fset ⇒ 'a" is the_elem' .

lemma fthe_elem'_eq: "fthe_elem' = fthe_elem"
proof
  fix S :: "'a fset"
  show "fthe_elem' S = fthe_elem S"
    by transfer (fastforce intro: the_elem_id)
qed

end


subsection ‹@{type set}s as maps›

definition is_map :: "('a × 'b) set ⇒ bool" where
"is_map M = Ball M (λ(a⇩1, b⇩1). Ball M (λ(a⇩2, b⇩2). a⇩1 = a⇩2 ⟶ b⇩1 = b⇩2))"

lemma is_mapI[intro]:
  assumes "⋀a b⇩1 b⇩2. (a, b⇩1) ∈ M ⟹ (a, b⇩2) ∈ M ⟹ b⇩1 = b⇩2"
  shows "is_map M"
using assms unfolding is_map_def by auto

lemma distinct_is_map:
  assumes "distinct (map fst m)"
  shows "is_map (set m)"
using assms
by (metis Some_eq_map_of_iff is_mapI option.inject)

lemma is_map_image:
  assumes "is_map M"
  shows "is_map ((λ(a, b). (a, f a b)) ` M)"
using assms unfolding is_map_def by auto

lemma is_mapD:
  assumes "is_map M" "(a, b⇩1) ∈ M" "(a, b⇩2) ∈ M"
  shows "b⇩1 = b⇩2"
using assms unfolding is_map_def by auto

lemma is_map_subset: "is_map N ⟹ M ⊆ N ⟹ is_map M"
unfolding is_map_def by blast

lemma map_of_is_map: "(k, v) ∈ set m ⟹ is_map (set m) ⟹ map_of m k = Some v"
by (metis is_mapD map_of_SomeD weak_map_of_SomeI)

definition get_map :: "('a × 'b) set ⇒ 'a ⇒ ('a × 'b)" where
"get_map M k = the_elem (Set.filter (λ(k', _). k = k') M)"

lemma get_map_elem:
  assumes "is_map M"
  assumes "(k, v) ∈ M"
  shows "get_map M k = (k, v)"
proof -
  from assms have "Set.filter (λ(k', _). k = k') M = {(k, v)}"
    unfolding is_map_def by fastforce
  thus ?thesis
    unfolding get_map_def by simp
qed

lemma get_map_map:
  assumes "is_map S" "k ∈ fst ` S"
  shows "get_map ((λ(a, b). (a, f a b)) ` S) k = (case get_map S k of (a, b) ⇒ (a, f a b))"
proof -
  from assms obtain v where "(k, v) ∈ S"
    by force
  hence "get_map S k = (k, v)"
    using assms by (simp add: get_map_elem)

  have "(k, f k v) ∈ (λ(a, b). (a, f a b)) ` S"
    using ‹(k, v) ∈ S› by auto
  hence "get_map ((λ(a, b). (a, f a b)) ` S) k = (k, f k v)"
    using assms by (metis get_map_elem is_map_image) (* takes long *)

  show ?thesis
    unfolding ‹get_map S k = _› ‹get_map (_ ` S) k = _›
    by simp
qed

lemma is_map_fst_inj: "is_map S ⟹ inj_on fst S"
by (fastforce intro: inj_onI dest: is_mapD)

context
  includes fset.lifting
begin

lemma is_map_transfer:
  fixes A :: "'a ⇒ 'b ⇒ bool"
  assumes [transfer_rule]: "bi_unique A"
  shows "rel_fun (rel_set (rel_prod (=) A)) (=) is_map is_map"
unfolding is_map_def[abs_def]
by transfer_prover

lift_definition is_fmap :: "('a × 'b) fset ⇒ bool" is is_map parametric is_map_transfer .

lemma is_fmapI[intro]:
  assumes "⋀a b⇩1 b⇩2. (a, b⇩1) |∈| M ⟹ (a, b⇩2) |∈| M ⟹ b⇩1 = b⇩2"
  shows "is_fmap M"
using assms by transfer' auto

lemma is_fmap_image: "is_fmap M ⟹ is_fmap ((λ(a, b). (a, f a b)) |`| M)"
by transfer' (rule is_map_image)

lemma is_fmapD:
  assumes "is_fmap M" "(a, b⇩1) |∈| M" "(a, b⇩2) |∈| M"
  shows "b⇩1 = b⇩2"
using assms by transfer' (rule is_mapD)

lemma is_fmap_subset: "is_fmap N ⟹ M |⊆| N ⟹ is_fmap M"
by transfer' (rule is_map_subset)

end


subsection ‹Conversion into sorted lists›

definition ordered_map :: "('a::linorder × 'b) set ⇒ ('a × 'b) list" where
"ordered_map S = map (get_map S) (sorted_list_of_set (fst ` S))"

lemma ordered_map_set_eq:
  assumes "finite S" "is_map S"
  shows "set (ordered_map S) = S"
proof -
  have "set (ordered_map S) = get_map S ` set (sorted_list_of_set (fst ` S))"
    unfolding ordered_map_def by simp
  also have "… = get_map S ` (fst ` S)"
    using assms by (auto simp: sorted_list_of_set)
  also have "… = (get_map S ∘ fst) ` S"
    unfolding o_def by auto
  also have "… = id ` S"
    using assms
    by (force simp: get_map_elem)
  finally show ?thesis
    by simp
qed

lemma ordered_map_image:
  assumes "finite S" "is_map S"
  shows "map (λ(a, b). (a, f a b)) (ordered_map S) = ordered_map ((λ(a, b). (a, f a b)) ` S)"
using assms
unfolding ordered_map_def list.map_comp image_comp
by (auto simp: fst_def[abs_def] comp_def case_prod_twice get_map_map)

lemma ordered_map_distinct:
  assumes "finite S" "is_map S"
  shows "distinct (map fst (ordered_map S))"
proof -
  have "inj_on (fst ∘ get_map S) (set (sorted_list_of_set (fst ` S)))"
    apply rule
    using sorted_list_of_set assms(1)
    apply simp
    apply (erule imageE)
    apply (erule imageE)
    subgoal for x y x' y'
      apply (cases x', cases y')
      apply simp
      apply (subst (asm) get_map_elem)
        apply (rule assms)
       apply assumption
      apply (subst (asm) get_map_elem)
        apply (rule assms)
       apply assumption
      apply simp
      done
    done
  then show ?thesis
    unfolding ordered_map_def
    by (auto intro: distinct_sorted_list_of_set simp: distinct_map)
qed

lemma ordered_map_keys:
  assumes "finite S" "is_map S"
  shows "map fst (ordered_map S) = sorted_list_of_set (fst ` S)"
proof -
  have "fst (get_map S z) = z" if "z ∈ fst ` S" for z
    using assms that by (fastforce simp: get_map_elem)
  moreover have "set (sorted_list_of_set (fst ` S)) = fst ` S"
    using assms by (force simp: sorted_list_of_set)
  ultimately show ?thesis
    unfolding ordered_map_def
    by (metis (no_types, lifting) map_idI map_map o_apply)
qed

corollary ordered_map_sound:
  assumes "is_map S" "finite S" "(a, b) ∈ set (ordered_map S)"
  shows "(a, b) ∈ S"
using assms by (metis ordered_map_set_eq)

lemma ordered_map_nonempty:
  assumes "is_map S" "ordered_map S ≠ []" "finite S"
  shows "S ≠ {}"
using assms unfolding ordered_map_def by auto

lemma ordered_map_remove:
  assumes "is_map S" "finite S" "x ∈ S"
  shows "ordered_map (S - {x}) = remove1 x (ordered_map S)"
proof -
  have distinct: "distinct (sorted_list_of_set (fst ` S))"
    using assms
    by (fastforce simp: sorted_list_of_set)

  have "inj_on (get_map S) (fst ` S)"
    using assms
    by (fastforce simp: get_map_elem intro: inj_onI)

  hence inj: "inj_on (get_map S) (set (sorted_list_of_set (fst ` S)))"
    using assms
    by (simp add: sorted_list_of_set)

  have "ordered_map (S - {x}) = map (get_map (S - {x})) (sorted_list_of_set (fst ` (S - {x})))"
    unfolding ordered_map_def by simp
  also have "… = map (get_map (S - {x})) (sorted_list_of_set (fst ` S - {fst x}))"
    proof (subst inj_on_image_set_diff)
      show "inj_on fst S"
        by (rule is_map_fst_inj) fact
    next
      show "{x} ⊆ S"
        using assms by simp
    qed auto
  also have "… = map (get_map (S - {x})) (remove1 (fst x) (sorted_list_of_set (fst ` S)))"
    proof (subst sorted_list_of_set_remove)
      show "finite (fst ` S)"
        using assms by simp
    qed simp
  also have "… = map (get_map S) (remove1 (fst x) (sorted_list_of_set (fst ` S)))"
    proof (rule list.map_cong0)
      fix z
      assume "z ∈ set (remove1 (fst x) (sorted_list_of_set (fst ` S)))"
      with distinct have "z ≠ fst x"
        by simp
      thus "get_map (S - {x}) z = get_map S z"
        unfolding get_map_def Set.filter_def
        by (metis (full_types, lifting) case_prodE fst_conv member_remove remove_def)
    qed
  also have "… = map (get_map S) (removeAll (fst x) (sorted_list_of_set (fst ` S)))"
    using distinct
    by (auto simp: distinct_remove1_removeAll)
  also have "… = removeAll (get_map S (fst x)) (map (get_map S) (sorted_list_of_set (fst ` S)))"
    proof (subst map_removeAll_inj_on)
      have "fst x ∈ set (sorted_list_of_set (fst ` S))"
        using assms by (fastforce simp: sorted_list_of_set)
      hence "insert (fst x) (set (sorted_list_of_set (fst ` S))) = set (sorted_list_of_set (fst ` S))"
        by auto
      with inj show "inj_on (get_map S) (insert (fst x) (set (sorted_list_of_set (fst ` S))))"
        by auto
    qed simp
  also have "… = removeAll x (map (get_map S) (sorted_list_of_set (fst ` S)))"
    using assms by (auto simp: get_map_elem[where v = "snd x"])
  also have "… = remove1 x (map (get_map S) (sorted_list_of_set (fst ` S)))"
    using distinct inj
    by (simp add: distinct_remove1_removeAll distinct_map)
  finally show ?thesis
    unfolding ordered_map_def .
qed

lemma ordered_map_list_all:
  assumes "finite S" "is_map S"
  shows "list_all P (ordered_map S) = Ball S P"
unfolding list_all_iff
using assms by (simp add: ordered_map_set_eq)

lemma ordered_map_singleton[simp]: "ordered_map {(x, y)} = [(x, y)]"
unfolding ordered_map_def get_map_def Set.filter_def the_elem_def
by auto

context
  includes fset.lifting
begin

lift_definition ordered_fmap :: "('a::linorder × 'b) fset ⇒ ('a × 'b) list" is ordered_map .

lemma ordered_fmap_set_eq: "is_fmap S ⟹ fset_of_list (ordered_fmap S) = S"
by transfer (rule ordered_map_set_eq)

lemma ordered_fmap_image:
  assumes "is_fmap S"
  shows "map (λ(a, b). (a, f a b)) (ordered_fmap S) = ordered_fmap ((λ(a, b). (a, f a b)) |`| S)"
using assms by transfer (rule ordered_map_image)

lemma ordered_fmap_distinct:
  assumes "is_fmap S"
  shows "distinct (map fst (ordered_fmap S))"
using assms
by transfer (rule ordered_map_distinct)

lemma ordered_fmap_keys:
  assumes "is_fmap S"
  shows "map fst (ordered_fmap S) = sorted_list_of_fset (fst |`| S)"
using assms
by transfer (rule ordered_map_keys)

lemma ordered_fmap_sound:
  assumes "is_fmap S" "(a, b) ∈ set (ordered_fmap S)"
  shows "(a, b) |∈| S"
using assms by transfer (rule ordered_map_sound)

lemma ordered_fmap_nonempty:
  assumes "is_fmap S" "ordered_fmap S ≠ []"
  shows "S ≠ {||}"
using assms by transfer (rule ordered_map_nonempty)

lemma ordered_fmap_remove:
  assumes "is_fmap S" "x |∈| S"
  shows "ordered_fmap (S - {| x |}) = remove1 x (ordered_fmap S)"
using assms by transfer (rule ordered_map_remove)

lemma ordered_fmap_list_all:
  assumes "is_fmap S"
  shows "list_all P (ordered_fmap S) = fBall S P"
unfolding list_all_iff
using assms by transfer (simp add: ordered_map_set_eq)

lemma ordered_fmap_singleton[simp]: "ordered_fmap {| (x, y) |} = [(x, y)]"
by transfer' simp

end


subsection ‹Grouping into sets›

definition group_by :: "('a ⇒ ('b × 'c)) ⇒ 'a set ⇒ ('b × 'c set) set" where
"group_by f s = {(fst (f a), {snd (f a')| a'. a' ∈ s ∧ fst (f a) = fst (f a') }) |a. a ∈ s}"

lemma group_by_nonempty: "M ≠ {} ⟹ group_by f M ≠ {}"
unfolding group_by_def by blast

lemma group_by_nonempty_inner:
  assumes "(b, cs) ∈ group_by f as"
  obtains c where "c ∈ cs"
using assms unfolding group_by_def by blast

lemma group_by_sound: "c ∈ cs ⟹ (b, cs) ∈ group_by f as ⟹ ∃a ∈ as. f a = (b, c)"
unfolding group_by_def by force

lemma group_byD: "(b, cs) ∈ group_by f as ⟹ f a = (b, c) ⟹ a ∈ as ⟹ c ∈ cs"
unfolding group_by_def by force

lemma group_byE[elim]:
  assumes "c ∈ cs" "(b, cs) ∈ group_by f as"
  obtains a where "a ∈ as" "f a = (b, c)"
using assms by (metis group_by_sound)

lemma group_byE2:
  assumes "(b, cs) ∈ group_by f as"
  obtains a where "a ∈ as" "fst (f a) = b"
using assms
by (metis group_byE group_by_nonempty_inner prod.sel(1))

lemma group_by_complete:
  assumes "a ∈ as"
  obtains cs where "(fst (f a), cs) ∈ group_by f as" "snd (f a) ∈ cs"
using assms unfolding group_by_def by auto

lemma group_by_single: "(a, x) ∈ group_by f s ⟹ (a, y) ∈ group_by f s ⟹ x = y"
unfolding group_by_def
by force

definition group_by' :: "('a ⇒ ('b × 'c)) ⇒ 'a set ⇒ ('b × 'c set) set" where
"group_by' f s = (λa. let (fa, _) = f a in (fa, (snd ∘ f) ` Set.filter (λa'. fa = fst (f a')) s)) ` s"

lemma group_by'_eq[code, code_unfold]: "group_by = group_by'"
apply (rule ext)+
unfolding group_by_def group_by'_def Set.filter_def
by (auto simp: Let_def split_beta)

lemma is_map_group_by[intro]: "is_map (group_by f M)"
unfolding group_by_def by force

lemma group_by_keys[simp]: "fst ` group_by f M = fst ` f ` M"
unfolding group_by_def by force

context
  includes fset.lifting
begin

lift_definition fgroup_by :: "('a ⇒ ('b × 'c)) ⇒ 'a fset ⇒ ('b × 'c fset) fset" is group_by
unfolding inf_apply inf_bool_def group_by_def by auto

lemma fgroup_by_nonempty: "M ≠ {||} ⟹ fgroup_by f M ≠ {||}"
by transfer' (rule group_by_nonempty)

lemma fgroup_by_nonempty_inner:
  assumes "(b, cs) |∈| fgroup_by f as"
  obtains c where "c |∈| cs"
using assms by transfer' (rule group_by_nonempty_inner)

lemma fgroup_by_sound: "c |∈| cs ⟹ (b, cs) |∈| fgroup_by f as ⟹ fBex as (λa. f a = (b, c))"
by transfer (metis group_by_sound)

lemma fgroup_byD: "(b, cs) |∈| fgroup_by f as ⟹ f a = (b, c) ⟹ a |∈| as ⟹ c |∈| cs"
by transfer' (metis group_byD)

lemma fgroup_byE[elim]:
  assumes "c |∈| cs" "(b, cs) |∈| fgroup_by f as"
  obtains a where "a |∈| as" "f a = (b, c)"
using assms by transfer' auto

lemma fgroup_byE2:
  assumes "(b, cs) |∈| fgroup_by f as"
  obtains a where "a |∈| as" "fst (f a) = b"
using assms by transfer' (rule group_byE2)

lemma fgroup_by_complete:
  assumes "a |∈| as"
  obtains cs where "(fst (f a), cs) |∈| fgroup_by f as" "snd (f a) |∈| cs"
using assms proof (transfer)
  fix a :: 'a and as :: "'a set"
  fix f :: "'a ⇒ ('c × 'b)"
  fix thesis

  assume as: "finite as"
  assume "a ∈ as"
  then obtain cs where cs: "(fst (f a), cs) ∈ group_by f as" "snd (f a) ∈ cs"
    by (metis group_by_complete)
  hence "finite cs"
    unfolding group_by_def using as by force

  assume thesis: "⋀cs. finite cs ⟹ (fst (f a), cs) ∈ group_by f as ⟹ snd (f a) ∈ cs ⟹ thesis"
  show thesis
    by (rule thesis) fact+
qed

lemma fgroup_by_single: "(a, x) |∈| fgroup_by f s ⟹ (a, y) |∈| fgroup_by f s ⟹ x = y"
by transfer (metis group_by_single)

definition fgroup_by' :: "('a ⇒ ('b × 'c)) ⇒ 'a fset ⇒ ('b × 'c fset) fset" where
"fgroup_by' f s = fcompress ((λa. let (fa, _) = f a in (fa, (snd ∘ f) |`| ffilter (λa'. fa = fst (f a')) s)) |`| s)"

lemma fgroup_by'_eq[code, code_unfold]: "fgroup_by = fgroup_by'"
unfolding fgroup_by'_def[abs_def] fcompress_eq
by transfer' (metis group_by'_def group_by'_eq)

lemma is_fmap_group_by[intro]: "is_fmap (fgroup_by f M)"
by transfer' (rule is_map_group_by)

lemma fgroup_by_keys[simp]: "fst |`| fgroup_by f M = fst |`| f |`| M"
by transfer' (rule group_by_keys)

end


subsection ‹Singletons›

lemma singleton_set_holds:
  assumes "∀x ∈ M. ∀y ∈ M. f x = f y" "m ∈ M"
  shows "f m = the_elem (f ` M)"
proof -
  let ?n = "the_elem (f ` M)"
  have "f ` M = {f m}"
    using assms(1) assms(2) by blast
  hence "?n = (THE n. {f m} = {n})"
    unfolding the_elem_def by simp
  thus ?thesis by auto
qed

lemma singleton_set_is:
  assumes "∀x ∈ M. x = y" "M ≠ {}"
  shows "M = {y}"
using assms by auto

context
  includes fset.lifting
begin

lemma singleton_fset_holds:
  assumes "fBall M (λx. fBall M (λy. f x = f y))" "m |∈| M"
  shows "f m = fthe_elem (f |`| M)"
using assms
by transfer (rule singleton_set_holds)

lemma singleton_fset_is:
  assumes "fBall M (λx. x = y)" "M ≠ {||}"
  shows "M = {| y |}"
using assms by transfer' (rule singleton_set_is)

end


subsection ‹Pairwise relations›

definition pairwise :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"pairwise P M ⟷ (∀m ∈ M. ∀n ∈ M. P m n)"

lemma pairwiseI[intro!]:
  assumes "⋀m n. m ∈ M ⟹ n ∈ M ⟹ P m n"
  shows "pairwise P M"
using assms unfolding pairwise_def by simp

lemma pairwiseD[dest]:
  assumes "pairwise P M" "m ∈ M" "n ∈ M"
  shows "P m n"
using assms unfolding pairwise_def by simp

lemma pairwise_subset: "pairwise P M ⟹ N ⊆ M ⟹ pairwise P N"
unfolding pairwise_def by blast

lemma pairwise_weaken: "pairwise P M ⟹ (⋀x y. x ∈ M ⟹ y ∈ M ⟹ P x y ⟹ Q x y) ⟹ pairwise Q M"
by auto

lemma pairwise_image[simp]: "pairwise P (f ` M) = pairwise (λx y. P (f x) (f y)) M"
by auto

context
  includes fset.lifting
begin

lift_definition fpairwise :: "('a ⇒ 'a ⇒ bool) ⇒ 'a fset ⇒ bool" is pairwise .

lemma fpairwise_alt_def[code]: "fpairwise P M ⟷ fBall M (λm. fBall M (λn. P m n))"
by transfer' auto

lemma fpairwiseI[intro!]:
  assumes "⋀m n. m |∈| M ⟹ n |∈| M ⟹ P m n"
  shows "fpairwise P M"
using assms unfolding fpairwise_alt_def by blast

lemma fpairwiseD:
  assumes "fpairwise P M" "m |∈| M" "n |∈| M"
  shows "P m n"
  using assms unfolding fpairwise_alt_def by auto

lemma fpairwise_image[simp]: "fpairwise P (f |`| M) = fpairwise (λx y. P (f x) (f y)) M"
by (auto dest: fpairwiseD)

end

lemma fpairwise_subset: "fpairwise P M ⟹ N |⊆| M ⟹ fpairwise P N"
unfolding fpairwise_alt_def by auto

lemma fpairwise_weaken: "fpairwise P M ⟹ (⋀x y. x |∈| M ⟹ y |∈| M ⟹ P x y ⟹ Q x y) ⟹ fpairwise Q M"
unfolding fpairwise_alt_def by auto


subsection ‹Relators›

lemma rel_set_eq_eq: "rel_set (=) A B ⟹ A = B"
unfolding rel_set_def by fast

lemma rel_set_image:
  assumes "rel_set P A B"
  assumes "⋀a b. a ∈ A ⟹ b ∈ B ⟹ P a b ⟹ Q (f a) (g b)"
  shows "rel_set Q (f ` A) (g ` B)"
using assms
by (force intro!: rel_setI dest: rel_setD1 rel_setD2)

corollary rel_set_image_eq:
  assumes "rel_set P A B"
  assumes "⋀a b. a ∈ A ⟹ b ∈ B ⟹ P a b ⟹ f a = g b"
  shows "f ` A = g ` B"
proof -
  have "rel_set (=) (f ` A) (g ` B)"
    by (rule rel_set_image) fact+
  thus ?thesis
    by (rule rel_set_eq_eq)
qed

lemma rel_set_refl_strong[intro]:
  assumes "⋀x. x ∈ S ⟹ P x x"
  shows "rel_set P S S"
proof (rule rel_setI)
  fix x
  assume "x ∈ S"
  thus "∃y ∈ S. P x y"
    using assms by blast
next
  fix y
  assume "y ∈ S"
  thus "∃x ∈ S. P x y"
    using assms by blast
qed

context
  includes fset.lifting
begin

lemma rel_fsetE1:
  assumes "rel_fset P M N" "x |∈| M"
  obtains y where "y |∈| N" "P x y"
using assms by transfer' (auto dest: rel_setD1)

lemma rel_fsetE2:
  assumes "rel_fset P M N" "y |∈| N"
  obtains x where "x |∈| M" "P x y"
using assms by transfer' (auto dest: rel_setD2)

lemma rel_fsetI:
  assumes "⋀x. x |∈| A ⟹ fBex B (R x)" "⋀y. y |∈| B ⟹ fBex A (λx. R x y)"
  shows "rel_fset R A B"
using assms by transfer' (rule rel_setI)

lemma rel_fset_image:
  assumes "rel_fset P A B"
  assumes "⋀a b. a |∈| A ⟹ b |∈| B ⟹ P a b ⟹ Q (f a) (g b)"
  shows "rel_fset Q (f |`| A) (g |`| B)"
using assms by transfer' (rule rel_set_image)

corollary rel_fset_image_eq:
  assumes "rel_fset P A B"
  assumes "⋀a b. a |∈| A ⟹ b |∈| B ⟹ P a b ⟹ f a = g b"
  shows "f |`| A = g |`| B"
using assms by transfer' (rule rel_set_image_eq)

lemma rel_fset_refl_strong:
  assumes "⋀x. x |∈| S ⟹ P x x"
  shows "rel_fset P S S"
using assms
by transfer' (rule rel_set_refl_strong)

end


subsection ‹Selecting values from keys›

definition select :: "('a ⇒ 'b option) ⇒ 'a set ⇒ 'b set" where
"select f S = {z|z. ∃x ∈ S. f x = Some z}"

lemma select_finite:
  assumes "finite S"
  shows "finite (select f S)"
proof -
  have "finite (f ` S)"
    using assms by simp
  moreover have "Some ` (select f S) ⊆ f ` S"
    unfolding select_def by force
  ultimately have "finite (Some ` select f S)"
    by (rule rev_finite_subset)
  moreover have "⋀S. inj_on Some S"
    by simp
  ultimately show ?thesis
    by (rule finite_imageD)
qed

lemma select_memberI: "x ∈ S ⟹ f x = Some y ⟹ y ∈ select f S"
unfolding select_def by blast

lemma select_memberE:
  assumes "y ∈ select f S"
  obtains x where "x ∈ S" "f x = Some y"
using assms unfolding select_def by blast

context
  includes fset.lifting
begin

lift_definition fselect :: "('a ⇒ 'b option) ⇒ 'a fset ⇒ 'b fset" is select
by (rule select_finite)

lemma fselect_memberI[intro]: "x |∈| S ⟹ f x = Some y ⟹ y |∈| fselect f S"
by transfer' (rule select_memberI)

lemma fselect_memberE[elim]:
  assumes "y |∈| fselect f S"
  obtains x where "x |∈| S" "f x = Some y"
using assms by transfer' (rule select_memberE)

end


subsection ‹Miscellaneous›

lemma set_of_list_singletonE:
  assumes "set xs = {x}" "distinct xs"
  shows "xs = [x]"
using assms
by (metis distinct.simps(2) empty_iff insertI1 insert_ident list.simps(15) neq_Nil_conv set_empty2 singletonD)

lemma fset_of_list_singletonE:
  assumes "fset_of_list xs = {|x|}" "distinct xs"
  shows "xs = [x]"
including fset.lifting
  using assms by transfer (rule set_of_list_singletonE)

section ‹Finite maps›

definition fmlookup_default :: "('a, 'b) fmap ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
"fmlookup_default m f x = (case fmlookup m x of None ⇒ f x | Some b ⇒ b)"

lemma fmpred_foldl[intro]:
  assumes "fmpred P init" "⋀x. x ∈ set xs ⟹ fmpred P x"
  shows "fmpred P (foldl (++⇩f) init xs)"
using assms proof (induction xs arbitrary: init)
  case (Cons x xs)
  have "fmpred P (foldl (++⇩f) (init ++⇩f x) xs)"
    proof (rule Cons)
      show "fmpred P (init ++⇩f x)"
        using Cons by auto
    next
      fix x
      assume "x ∈ set xs"
      thus "fmpred P x"
        using Cons by auto
    qed
  thus ?case
    by simp
qed auto

lemma fmdom_foldl_add: "fmdom (foldl (++⇩f) m ns) = fmdom m |∪| ffUnion (fmdom |`| fset_of_list ns)"
by (induction ns arbitrary: m) auto

lemma fmimage_fmmap[simp]: "fmimage (fmmap f m) S = f |`| fmimage m S"
including fmap.lifting fset.lifting
by transfer' auto

lemma fmmap_total:
  assumes "⋀k v. fmlookup m k = Some v ⟹ (∃v'. f v' = v)"
  obtains m' where "m = fmmap f m'"
apply (rule that[of "fmmap (inv f) m"])
unfolding fmap.map_comp
apply (subst fmap.map_id[symmetric])
apply (rule fmap.map_cong)
apply (auto simp: fmran'_def f_inv_into_f dest!: assms)
done

lemma set_of_map_upd: "set_of_map (map_upd k v m) = set_of_map (map_drop k m) ∪ {(k, v)}"
unfolding set_of_map_def map_upd_def map_drop_def map_filter_def
by (auto split: if_splits)

lemma map_drop_delete: "map_drop k (map_of ps) = map_of (AList.delete k ps)"
unfolding AList.delete_eq map_drop_def
apply (subst map_filter_map_of)
apply (rule arg_cong[where f = "map_of"])
apply (rule filter_cong[OF refl])
by auto

lemma set_of_map_map_of: "set_of_map (map_of xs) = set (AList.clearjunk xs)"
proof (induction xs rule: clearjunk.induct)
  case (2 p ps)

  (* honourable mention: int-e on IRC, but it's way to short to understand what's going on *)
  have ?case by (simp add: 2[symmetric] delete_conv) (auto simp: set_of_map_def)

  obtain k v where "p = (k, v)"
    by (cases p) auto
  have "set_of_map (map_of (p # ps)) = set_of_map (map_upd k v (map_of ps))"
    unfolding ‹p = _› map_upd_def by simp
  also have "… = set_of_map (map_drop k (map_of ps)) ∪ {(k, v)}"
    by (rule set_of_map_upd)
  also have "… = set_of_map (map_of (AList.delete k ps)) ∪ {(k, v)}"
    by (simp only: map_drop_delete)
  also have "… =  set (AList.clearjunk (AList.delete k ps)) ∪ {(k, v)}"
    using 2 unfolding ‹p = _› by simp
  also have "… = set (AList.clearjunk (p # ps))"
    unfolding ‹p = _› by simp
  finally show ?case .
qed (simp add: set_of_map_def)

lemma fset_of_fmap_code[code]: "fset_of_fmap (fmap_of_list x) = fset_of_list (AList.clearjunk x)"
including fmap.lifting fset.lifting
  by transfer (rule set_of_map_map_of)

lemma distinct_sorted_list_of_fmap[simp, intro]: "distinct (sorted_list_of_fmap m)"
unfolding sorted_list_of_fmap_def
apply (subst distinct_map)
apply rule
subgoal by simp
subgoal by (rule inj_on_convol_ident)
done

section ‹Lists›

lemma rev_induct2[consumes 1, case_names nil snoc]:
  assumes "length xs = length ys"
  assumes "P [] []"
  assumes "⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs @ [x]) (ys @ [y])"
  shows "P xs ys"
proof -
  have "length (rev xs) = length (rev ys)"
    using assms by simp
  hence "P (rev (rev xs)) (rev (rev ys))"
    using assms by (induct rule: list_induct2) auto
  thus ?thesis
    by simp
qed

lemma list_allI[intro]:
  assumes "⋀x. x ∈ set xs ⟹ P x"
  shows "list_all P xs"
using assms unfolding list_all_iff by auto

lemma list_map_snd_id:
  assumes "⋀a b e. (a, b) ∈ set cs ⟹ f a b = b"
  shows "map (λ(a, b). (a, f a b)) cs = cs"
proof -
  have "map (λ(a, b). (a, f a b)) cs = map id cs"
    proof (rule list.map_cong0, safe)
      fix a b
      assume "(a, b) ∈ set cs"
      hence "f a b = b"
        using assms by auto
      thus "(a, f a b) = id (a, b)"
        by simp
    qed
  thus ?thesis
    by simp
qed

lemma list_all2_leftE:
  assumes "list_all2 P xs ys" "x ∈ set xs"
  obtains y where "y ∈ set ys" "P x y"
using assms by induct auto

lemma list_all2_rightE:
  assumes "list_all2 P xs ys" "y ∈ set ys"
  obtains x where "x ∈ set xs" "P x y"
using assms by induct auto

fun list_all3 where
"list_all3 P (x # xs) (y # ys) (z # zs) ⟷ P x y z ∧ list_all3 P xs ys zs" |
"list_all3 P [] [] [] ⟷ True" |
"list_all3 _ _ _ _ ⟷ False"

lemma list_all3_empty[intro]: "list_all3 P [] [] []"
by simp

lemma list_all3_cons[intro]: "list_all3 P xs ys zs ⟹ P x y z ⟹ list_all3 P (x # xs) (y # ys) (z # zs)"
by simp

lemma list_all3_induct[consumes 1, case_names Nil Cons, induct set: list_all3]:
  assumes P: "list_all3 P xs ys zs"
  assumes Nil: "Q [] [] []"
  assumes Cons: "⋀x xs y ys z zs.
    P x y z ⟹ Q xs ys zs ⟹ list_all3 P xs ys zs ⟹ Q (x # xs) (y # ys) (z # zs)"
  shows "Q xs ys zs"
using P
proof (induction P≡P xs ys zs rule: list_all3.induct, goal_cases cons)
  show "Q [] [] []" by fact
next
  case (cons x xs y ys z zs)
  thus ?case
    using Cons by auto
qed auto

lemma list_all3_from_list_all2s:
  assumes "list_all2 P xs ys" "list_all2 Q xs zs"
  assumes "⋀x y z. x ∈ set xs ⟹ y ∈ set ys ⟹ z ∈ set zs ⟹ P x y ⟹ Q x z ⟹ R x y z"
  shows "list_all3 R xs ys zs"
using assms proof (induction arbitrary: zs)
  case Nil
  hence "zs = []" by blast
  thus ?case by simp
next
  case (Cons x y xs ys zs0)
  then obtain z zs where "zs0 = z # zs" by (cases zs0) auto
  show ?case
    using Cons unfolding ‹zs0 = _›
    by auto
qed

lemma those_someD:
  assumes "those xs = Some ys"
  shows "xs = map Some ys"
using assms by (induction xs arbitrary: ys) (auto split: if_splits option.splits)

end