Theory Concrete_Examples

(* Author: Andreas Lochbihler, ETH Zurich
   Author: Joshua Schneider, ETH Zurich *)

section ‹Concrete \BNFCC{}s›

theory Concrete_Examples imports
  Preliminaries
  "HOL-Library.Rewrite"
  "HOL-Library.Cardinality"
begin

context includes lifting_syntax
begin

subsection ‹Function space›

lemma rel_fun_mono: "(A ===> B) ≤ (A' ===> B')" if "A' ≤ A" "B ≤ B'"
  using that by(auto simp add: rel_fun_def)

lemma rel_fun_eq: "((=) ===> (=)) = (=)" by(fact fun.rel_eq)

lemma rel_fun_conversep: "(A¯¯ ===> B¯¯) = (A ===> B)¯¯" by(auto simp add: rel_fun_def)

lemma map_fun_id0: "(id ---> id) = id" by(fact map_fun.id)

lemma map_fun_comp: "(f ---> g) ∘ (f' ---> g') = ((f' ∘ f) ---> (g ∘ g'))" by(fact map_fun.comp)

lemma map_fun_parametric: "((A ===> A') ===> (B ===> B') ===> (A' ===> B) ===> (A ===> B')) (--->) (--->)"
  by(fact map_fun_parametric)

definition rel_fun_pos_distr_cond :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒
    ('b × 'b' × 'b'') itself ⇒ bool" where
  "rel_fun_pos_distr_cond A A' _ ⟷ (∀(B :: 'b ⇒ 'b' ⇒ bool) (B' :: 'b' ⇒ 'b'' ⇒ bool).
    (A ===> B) OO (A' ===> B') ≤ (A OO A') ===> (B OO B'))"

definition rel_fun_neg_distr_cond :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒
    ('b × 'b' × 'b'') itself ⇒ bool" where
  "rel_fun_neg_distr_cond A A' _ ⟷ (∀(B :: 'b ⇒ 'b' ⇒ bool) (B' :: 'b' ⇒ 'b'' ⇒ bool).
    (A OO A') ===> (B OO B') ≤ (A ===> B) OO (A' ===> B'))"

lemmas
  rel_fun_pos_distr = rel_fun_pos_distr_cond_def[THEN iffD1, rule_format] and
  rel_fun_neg_distr = rel_fun_neg_distr_cond_def[THEN iffD1, rule_format]

lemma rel_fun_pos_distr_iff [simp]: "rel_fun_pos_distr_cond A A' tytok = True"
  unfolding rel_fun_pos_distr_cond_def by (blast intro!: pos_fun_distr)

lemma rel_fun_neg_distr_imp: "⟦ left_unique A; right_total A; right_unique A'; left_total A' ⟧ ⟹
  rel_fun_neg_distr_cond A A' tytok"
  unfolding rel_fun_neg_distr_cond_def by (fast elim!: neg_fun_distr1[THEN predicate2D])

lemma rel_fun_pos_distr_cond_eq: "rel_fun_pos_distr_cond (=) (=) tytok"
  by simp

lemma rel_fun_neg_distr_cond_eq: "rel_fun_neg_distr_cond (=) (=) tytok"
  by (blast intro: rel_fun_neg_distr_imp left_unique_eq right_unique_eq right_total_eq left_total_eq)

thm fun.set_map fun.map_cong0 fun.rel_mono_strong


subsection ‹Covariant powerset›

lemma rel_set_mono: "A ≤ A' ⟹ rel_set A ≤ rel_set A'" by(fact rel_set_mono)

lemma rel_set_eq: "rel_set (=) = (=)" by(fact rel_set_eq)

lemma rel_set_conversep: "rel_set A¯¯ = (rel_set A)¯¯" by(fact rel_set_conversep)

lemma map_set_id0: "image id = id" by(fact image_id)

lemma map_set_comp: "image f ∘ image g = image (f ∘ g)" by(simp add: fun_eq_iff image_image o_def)

lemma map_set_parametric: includes lifting_syntax shows
  "((A ===> B) ===> rel_set A ===> rel_set B) image image"
  by(fact image_transfer)

definition rel_set_pos_distr_cond :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒ bool" where
  "rel_set_pos_distr_cond A A' ⟷ rel_set A OO rel_set A' ≤ rel_set (A OO A')"

definition rel_set_neg_distr_cond :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒ bool" where
  "rel_set_neg_distr_cond A A' ⟷ rel_set (A OO A') ≤ rel_set A OO rel_set A'"

lemmas
  rel_set_pos_distr = rel_set_pos_distr_cond_def[THEN iffD1, rule_format] and
  rel_set_neg_distr = rel_set_neg_distr_cond_def[THEN iffD1, rule_format]

lemma rel_set_pos_distr_iff [simp]: "rel_set_pos_distr_cond A A' = True"
  unfolding rel_set_pos_distr_cond_def by(simp add: rel_set_OO)

lemma rel_set_neg_distr_iff [simp]: "rel_set_neg_distr_cond A A' = True"
  unfolding rel_set_neg_distr_cond_def by(simp add: rel_set_OO)

lemma rel_set_pos_distr_eq: "rel_set_pos_distr_cond (=) (=)"
  by simp

lemma rel_set_neg_distr_eq: "rel_set_neg_distr_cond (=) (=)"
  by simp


subsection ‹Bounded sets›

text ‹
  We define bounded sets as a subtype, with an additional fixed parameter which controls the bound.
  Using the \BNFCC{} structure on the covariant powerset functor, it suffices to show the
  preconditions for the closedness of \BNFCC{} under subtypes.
›

typedef ('a, 'k) bset = "{A :: 'a set. finite A ∧ card A ≤ CARD('k)}"
proof
  show "{} ∈ ?bset" by simp
qed

setup_lifting type_definition_bset

lemma bset_map_closed:
  fixes f A
  defines "B ≡ image f A"
  assumes "finite A ∧ card A ≤ CARD('k)"
  shows "finite B ∧ card B ≤ CARD('k)"
  using assms by(auto intro: card_image_le[THEN order_trans])

lift_definition map_bset :: "('a ⇒ 'b) ⇒ ('a, 'k) bset ⇒ ('b, 'k) bset" is image
  by(fact bset_map_closed)

lift_definition rel_bset :: "('a ⇒ 'b ⇒ bool) ⇒ ('a, 'k) bset ⇒ ('b, 'k) bset ⇒ bool" is rel_set .

definition neg_distr_cond_bset :: "('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ 'c ⇒ bool) ⇒ 'k itself ⇒ bool" where
  "neg_distr_cond_bset C C' _ ⟷ rel_bset (C OO C') ≤ rel_bset C OO (rel_bset C' :: (_, 'k) bset ⇒ _)"

lemma right_unique_rel_set_lemma:
  assumes "right_unique R" and "rel_set R X Y"
  obtains f where "Y = image f X" and "∀x∈X. R x (f x)"
proof
  define f where "f x = (THE y. R x y)" for x
  { fix x assume "x ∈ X"
    with ‹rel_set R X Y› ‹right_unique R› have "R x (f x)"
      by (simp add: right_unique_def rel_set_def f_def) (metis theI)
    with assms ‹x ∈ X› have  "R x (f x)" "f x ∈ Y"
      by (fastforce simp add: right_unique_def rel_set_def)+ }
  moreover
  have "∃x∈X. y = f x" if "y ∈ Y" for y using ‹rel_set R X Y› that
    by(auto simp add: f_def dest!: rel_setD2 dest: right_uniqueD[OF ‹right_unique R›]
        intro: the_equality[symmetric])
  ultimately show "∀x∈X. R x (f x)" "Y = image f X"
    by (auto simp: inj_on_def image_iff)
qed

lemma left_unique_rel_set_lemma:
  assumes "left_unique R" and "rel_set R Y X"
  obtains f where "Y = image f X" and "∀x∈X. R (f x) x"
proof
  define f where "f x = (THE y. R y x)" for x
  { fix x assume "x ∈ X"
    with ‹rel_set R Y X› ‹left_unique R› have "R (f x) x"
      by (simp add: left_unique_def rel_set_def f_def)  (metis theI)
    with assms ‹x ∈ X› have  "R (f x) x" "f x ∈ Y"
      by (fastforce simp add: left_unique_def rel_set_def)+ }
  moreover
  have "∃x∈X. y = f x" if "y ∈ Y" for y using ‹rel_set R Y X› that
    by(auto simp add: f_def dest!: rel_setD1 dest: left_uniqueD[OF ‹left_unique R›]
        intro: the_equality[symmetric])
  ultimately show "∀x∈X. R (f x) x" "Y = image f X"
    by (auto simp: inj_on_def image_iff)
qed

lemma neg_distr_cond_bset_right_unique:
  "right_unique C ⟹ neg_distr_cond_bset C D tytok"
  unfolding neg_distr_cond_bset_def
  apply(rule predicate2I)
  apply transfer
  apply(auto 6 2 intro: card_image_le[THEN order_trans] elim: right_unique_rel_set_lemma
      simp add: rel_set_OO[symmetric])
  done

lemma neg_distr_cond_bset_left_unique:
  "left_unique D ⟹ neg_distr_cond_bset C D tytok"
  unfolding neg_distr_cond_bset_def
  apply(rule predicate2I)
  apply transfer
  apply(auto 6 2 intro: card_image_le[THEN order_trans] elim: left_unique_rel_set_lemma
      simp add: rel_set_OO[symmetric])
  done

lemma neg_distr_cond_bset_eq: "neg_distr_cond_bset (=) (=) tytok"
  by (intro neg_distr_cond_bset_right_unique right_unique_eq)


subsection ‹Contravariant powerset (sets as predicates)›

type_synonym 'a pred = "'a ⇒ bool"

definition map_pred :: "('b ⇒ 'a) ⇒ 'a pred ⇒ 'b pred" where
  "map_pred f = (f ---> id)"

definition rel_pred :: "('a ⇒ 'b ⇒ bool) ⇒ 'a pred ⇒ 'b pred ⇒ bool" where
  "rel_pred R = (R ===> (⟷))"

lemma rel_pred_mono: "A' ≤ A ⟹ rel_pred A ≤ rel_pred A'" unfolding rel_pred_def
  by(auto elim!: rel_fun_mono)

lemma rel_pred_eq: "rel_pred (=) = (=)"
  by(simp add: rel_pred_def rel_fun_eq)

lemma rel_pred_conversep: "rel_pred A¯¯ = (rel_pred A)¯¯"
  using rel_fun_conversep[of _ "(=)"] by (simp add: rel_pred_def)

lemma map_pred_id0: "map_pred id = id"
  by (simp add: map_pred_def map_fun_id)

lemma map_pred_comp: "map_pred f ∘ map_pred g = map_pred (g ∘ f)"
  using map_fun_comp[where g=id and g'=id] by (simp add: map_pred_def)

lemma map_pred_parametric: "((A' ===> A) ===> rel_pred A ===> rel_pred A') map_pred map_pred"
  by (simp add: rel_fun_def rel_pred_def map_pred_def)

definition rel_pred_pos_distr_cond :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒ bool" where
  "rel_pred_pos_distr_cond A B ⟷ rel_pred A OO rel_pred B ≤ rel_pred (A OO B)"

definition rel_pred_neg_distr_cond :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒ bool" where
  "rel_pred_neg_distr_cond A B ⟷  rel_pred (A OO B) ≤ rel_pred A OO rel_pred B"

lemmas
  rel_pred_pos_distr = rel_pred_pos_distr_cond_def[THEN iffD1, rule_format] and
  rel_pred_neg_distr = rel_pred_neg_distr_cond_def[THEN iffD1, rule_format]

lemma rel_pred_pos_distr_iff [simp]: "rel_pred_pos_distr_cond A B = True"
  unfolding rel_pred_pos_distr_cond_def by (auto simp add: rel_pred_def rel_fun_def)

lemma rel_pred_pos_distr_cond_eq: "rel_pred_pos_distr_cond (=) (=)"
  by simp

lemma neg_fun_distr3:
  assumes 1: "left_unique R" "right_total R"
    and 2: "right_unique S" "left_total S"
  shows "rel_fun (R OO R') (S OO S') ≤ rel_fun R S OO rel_fun R' S'"
  using functional_converse_relation[OF 1] functional_relation[OF 2]
  unfolding rel_fun_def OO_def
  apply clarify
  apply (subst all_comm)
  apply (subst all_conj_distrib[symmetric])
  apply (intro choice)
  by metis

text ‹
  As there are no live variables, we can get a weaker condition than if we derived it
  from @{const rel_fun}'s condition!
›

lemma rel_pred_neg_distr_imp:
  "right_unique B ∧ left_total B ∨ left_unique A ∧ right_total A ⟹ rel_pred_neg_distr_cond A B"
  unfolding rel_pred_neg_distr_cond_def rel_pred_def
  apply(clarsimp simp add: vimage2p_def rel_pred_neg_distr_cond_def)
  apply(rewrite in "rel_fun _ ⌑" in asm eq_OO[symmetric])
  apply(elim disjE)
   apply(drule neg_fun_distr2[THEN predicate2D, rotated -1];
      (simp add: left_unique_eq right_unique_eq left_total_eq right_total_eq)?)
  apply(drule neg_fun_distr3[THEN predicate2D, rotated -1];
      (simp add: left_unique_eq right_unique_eq left_total_eq right_total_eq)?)
  done

lemma rel_pred_neg_distr_cond_eq: "rel_pred_neg_distr_cond (=) (=)"
  by(blast intro: rel_pred_neg_distr_imp left_unique_eq right_total_eq)


lemma left_unique_rel_pred: "left_total A ⟹ left_unique (rel_pred A)"
  unfolding rel_pred_def by (erule left_unique_fun) (rule left_unique_eq)

lemma right_unique_rel_pred: "right_total A ⟹ right_unique (rel_pred A)"
  unfolding rel_pred_def by (erule right_unique_fun) (rule right_unique_eq)

lemma left_total_rel_pred: "left_unique A ⟹ left_total (rel_pred A)"
  unfolding rel_pred_def by (erule left_total_fun) (rule left_total_eq)

lemma right_total_rel_pred: "right_unique A ⟹ right_total (rel_pred A)"
  unfolding rel_pred_def by (erule right_total_fun) (rule right_total_eq)

end (* context includes lifting_syntax *)


subsection ‹Filter›

text ‹
  Similarly to bounded sets, we exploit the definition of filters as a subtype in order to
  lift the \BNFCC{} operations. Here we use that the @{const is_filter} predicate is closed under
  zippings.
›

lemma map_filter_closed:
  includes lifting_syntax
  assumes "is_filter F"
  shows "is_filter (((f ---> id) ---> id) F)"
proof -
  define F' where "F' = Abs_filter F"
  have "is_filter (((f ---> id) ---> id) (λP. eventually P F'))"
    by (rule is_filter.intro)(auto elim!: eventually_rev_mp simp add: map_fun_def o_def)
  then show ?thesis using assms by(simp add: F'_def eventually_Abs_filter)
qed

definition rel_pred2_neg_distr_cond :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒ bool" where
  "rel_pred2_neg_distr_cond A B ⟷
  rel_pred (rel_pred (A OO B)) ≤ rel_pred (rel_pred A) OO rel_pred (rel_pred B)"

consts rel_pred2_witness :: "('a ⇒ 'a' ⇒ bool) ⇒ ('a' ⇒ 'a'' ⇒ bool) ⇒
  (('a ⇒ bool) ⇒ bool) × (('a'' ⇒ bool) ⇒ bool) ⇒ ('a' ⇒ bool) ⇒ bool"

specification (rel_pred2_witness)
  rel_pred2_witness1: "⋀K K' x y. ⟦ rel_pred2_neg_distr_cond K K'; rel_pred (rel_pred (K OO K')) x y ⟧ ⟹
    rel_pred (rel_pred K) x (rel_pred2_witness K K' (x, y))"
  rel_pred2_witness2: "⋀K K' x y. ⟦ rel_pred2_neg_distr_cond K K'; rel_pred (rel_pred (K OO K')) x y ⟧ ⟹
    rel_pred (rel_pred K') (rel_pred2_witness K K' (x, y)) y"
  apply (rule exI[of _ "λK K' (x, y). SOME z. rel_pred (rel_pred K) x z ∧ rel_pred (rel_pred K') z y"])
  apply (fold all_conj_distrib)
  apply (intro allI)
  apply (fold imp_conjR)
  apply (clarify)
  apply (rule relcomppE[of "rel_pred (rel_pred _)" "rel_pred (rel_pred _)", rotated])
   apply (rule someI[where P="λz. rel_pred (rel_pred _) _ z ∧ rel_pred (rel_pred _) z _"])
   apply (erule (1) conjI)
  apply (auto simp add: rel_pred2_neg_distr_cond_def)
  done

lemmas rel_pred2_witness = rel_pred2_witness1 rel_pred2_witness2

context includes lifting_syntax
begin

definition rel_filter_neg_distr_cond' :: "('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ 'c ⇒ bool) ⇒ bool" where
  "rel_filter_neg_distr_cond' C C' ⟷ left_total C ∧ right_unique C ∨ right_total C' ∧ left_unique C'"

lemma rel_filter_neg_distr_cond'_stronger:
  assumes "rel_filter_neg_distr_cond' C C'"
  shows "rel_pred2_neg_distr_cond C C'"
  unfolding rel_pred2_neg_distr_cond_def
proof -
  have "rel_pred (rel_pred (C OO C')) ≤ rel_pred (rel_pred C OO rel_pred C')"
    by (auto intro!: rel_pred_mono rel_pred_pos_distr)
  also have "... ≤ rel_pred (rel_pred C) OO rel_pred (rel_pred C')"
    apply (rule rel_pred_neg_distr)
    apply (rule rel_pred_neg_distr_imp)
    apply (insert assms[unfolded rel_filter_neg_distr_cond'_def])
    by (blast dest: left_unique_rel_pred right_total_rel_pred right_unique_rel_pred left_total_rel_pred)
  finally show "rel_pred (rel_pred (C OO C')) ≤ ..." .
qed

lemma rel_filter_neg_distr_cond'_eq: "rel_filter_neg_distr_cond' (=) (=)"
  unfolding rel_filter_neg_distr_cond'_def by (simp add: left_total_eq right_unique_eq)

lemma is_filter_rel_witness:
  assumes F: "is_filter F" and G: "is_filter G"
    and FG: "rel_pred (rel_pred (C OO C')) F G"
    and cond: "rel_filter_neg_distr_cond' C C'"
  shows "is_filter (rel_pred2_witness C C' (F, G))"
proof
  let ?C = "rel_pred (rel_pred C)" and ?C' = "rel_pred (rel_pred C')"
  let ?wit = "rel_pred2_witness C C' (F, G)"
  have "rel_pred2_neg_distr_cond C C'"
    using cond by (rule rel_filter_neg_distr_cond'_stronger)
  with FG have wit1: "?C F ?wit" and wit2: "?C' ?wit G"
    by (rule rel_pred2_witness[rotated])+
  from wit1[unfolded rel_pred_def, THEN rel_funD, of "λ_. True" "λ_. True"] F
  show "?wit (λ_. True)" by (auto simp add: is_filter.True)

  fix P Q
  have *: "(?wit P ⟶ ?wit Q ⟶ ?wit (λx. P x ∧ Q x)) ∧ (?wit P ⟶ (∀x. P x ⟶ Q x) ⟶ ?wit Q)"
    using cond unfolding rel_filter_neg_distr_cond'_def
  proof(elim disjE conjE; use nothing in ‹intro conjI strip›)
    assume "left_total C" "right_unique C"
    hence "left_unique (C ===> (=))" "right_total (C ===> (=))"
      by(blast intro: left_unique_fun left_unique_eq right_total_fun right_total_eq)+
    from functional_converse_relation[OF this] obtain P' Q'
      where P' [transfer_rule]: "(C ===> (=)) P' P" and Q' [transfer_rule]: "(C ===> (=)) Q' Q"
      by fastforce
    have PQ: "(C ===> (=)) (λx. P' x ∧ Q' x) (λx. P x ∧ Q x)" by transfer_prover

    with wit1 P' Q' have P: "?wit P ⟷ F P'" and Q: "?wit Q ⟷ F Q'"
      and PQ: "?wit (λx. P x ∧ Q x) ⟷ F (λx. P' x ∧ Q' x)"
      by(auto dest: rel_funD simp add: rel_pred_def)

    show "?wit (λx. P x ∧ Q x)" if "?wit P" "?wit Q" using that P Q PQ
      by(auto intro: is_filter.conj[OF F])

    assume "∀x. P x ⟶ Q x"
    with P' Q' ‹left_total C› have "∀x. P' x ⟶ Q' x" by(metis (full_types) apply_rsp' left_total_def)
    then show "?wit Q" if "?wit P" using P Q that by(simp add: is_filter.mono[OF F])
  next
    assume "right_total C'" "left_unique C'"
    hence "right_unique (C' ===> (=))" "left_total (C' ===> (=))"
      by(blast intro: right_unique_fun right_unique_eq left_total_fun left_total_eq)+
    from functional_relation[OF this] obtain P' Q'
      where P' [transfer_rule]: "(C' ===> (=)) P P'" and Q' [transfer_rule]: "(C' ===> (=)) Q Q'"
      by fastforce
    have PQ: "(C' ===> (=)) (λx. P x ∧ Q x) (λx. P' x ∧ Q' x)" by transfer_prover

    with wit2 P' Q' have P: "?wit P ⟷ G P'" and Q: "?wit Q ⟷ G Q'"
      and PQ: "?wit (λx. P x ∧ Q x) ⟷ G (λx. P' x ∧ Q' x)"
      by(auto dest: rel_funD simp add: rel_pred_def)
    show "?wit (λx. P x ∧ Q x)" if "?wit P" "?wit Q" using that P Q PQ
      by(auto intro: is_filter.conj[OF G])

    assume "∀x. P x ⟶ Q x"
    with P' Q' ‹right_total C'› have "∀x. P' x ⟶ Q' x" by(metis (full_types) apply_rsp' right_total_def)
    then show "?wit Q" if "?wit P" using P Q that by(simp add: is_filter.mono[OF G])
  qed
  show "?wit (λx. P x ∧ Q x)" if P: "?wit P" and Q: "?wit Q" using * that by simp
  show "?wit Q" if P: "?wit P" and imp: "∀x. P x ⟶ Q x" using * that by simp
qed

end (* context includes lifting_syntax *)


text ‹The following example shows that filters do not satisfy @{command lift_bnf}'s condition.›

experiment begin
unbundle lifting_syntax

definition "raw_filtermap f = ((f ---> id) ---> id)"

lemma raw_filtermap_apply: "raw_filtermap f F = (λP. F (λx. P (f x)))"
  unfolding raw_filtermap_def
  by (simp add: map_fun_def comp_def)

lemma "filtermap f = Abs_filter ∘ raw_filtermap f ∘ Rep_filter"
  unfolding filtermap_def eventually_def
  by (simp add: fun_eq_iff raw_filtermap_apply)

definition Z where
  "Z = {{(False, False), (False, True)}, {(False, False), (True, False)},
    {(False, False), (False, True), (True, False), (True, True)}}"

abbreviation "Z' ≡ (λP. Collect P ∈ Z)"

lemma "is_filter (raw_filtermap fst Z')"
  unfolding Z_def raw_filtermap_apply
  apply (rule is_filter.intro)
    apply (simp add: set_eq_iff; smt)+
  done

lemma "is_filter (raw_filtermap snd Z')"
  unfolding Z_def raw_filtermap_apply
  apply (rule is_filter.intro)
    apply (simp add: set_eq_iff; smt)+
  done

lemma "¬ is_filter Z'"
  apply (rule)
  apply (drule is_filter.mono[of _ "λx. x ∈ {(False, False), (False, True)}"
        "λx. x ∈ {(False, False), (False, True), (True, False)}"])
    apply (auto 3 0 simp add: Z_def)
  done

end (* experiment *)


subsection ‹Almost-everywhere equal sequences›

inductive aeseq_eq :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ bool" for f g where
  "aeseq_eq f g" if "finite {n. f n ≠ g n}"

lemma equivp_aeseq_eq: "equivp aeseq_eq"
proof(rule equivpI)
  show "reflp aeseq_eq" by(simp add: reflp_def aeseq_eq.simps)
  show "symp aeseq_eq" by(simp add: symp_def aeseq_eq.simps eq_commute)
  have "finite {n. f n ≠ h n}" if "finite {n. f n ≠ g n}" "finite {n. g n ≠ h n}"
    for f g h :: "nat ⇒ 'b"
    using finite_subset[of "{n. f n ≠ h n}" "{n. f n ≠ g n} ∪ {n. g n ≠ h n}"] that
    by(fastforce intro: finite_subset)
  then show "transp aeseq_eq" by(auto simp add: transp_def aeseq_eq.simps)
qed

quotient_type 'a aeseq = "nat ⇒ 'a" / aeseq_eq by(rule equivp_aeseq_eq)

lift_definition map_aeseq :: "('a ⇒ 'b) ⇒ 'a aeseq ⇒ 'b aeseq" is "(∘)"
  by(auto simp add: aeseq_eq.simps elim: finite_subset[rotated])

lemma map_aeseq_id: "map_aeseq id x = x"
  by transfer(simp add: equivp_reflp[OF equivp_aeseq_eq])

lemma map_aeseq_comp: "map_aeseq f (map_aeseq g x) = map_aeseq (f ∘ g) x"
  by transfer(simp add: o_assoc equivp_reflp[OF equivp_aeseq_eq])

lift_definition rel_aeseq :: "('a ⇒ 'b ⇒ bool) ⇒ 'a aeseq ⇒ 'b aeseq ⇒ bool" is
  "λR f g. finite {n. ¬ R (f n) (g n)}"
proof(unfold aeseq_eq.simps)
  show "finite {n. ¬ R (f n) (g n)} ⟷ finite {n. ¬ R (f' n) (g' n)}"
    if ff': "finite {n. f n ≠ f' n}" and gg': "finite {n. g n ≠ g' n}"
    for R and f f' :: "nat ⇒ 'a" and g g' :: "nat ⇒ 'b"
  proof(rule iffI)
    assume "finite {n. ¬ R (f n) (g n)}"
    with ff' gg' have "finite ({n. ¬ R (f n) (g n)} ∪ {n. f n ≠ f' n} ∪ {n. g n ≠ g' n})" by simp
    then show "finite {n. ¬ R (f' n) (g' n)}" by(rule finite_subset[rotated]) auto
  next
    assume "finite {n. ¬ R (f' n) (g' n)}"
    with ff' gg' have "finite ({n. ¬ R (f' n) (g' n)} ∪ {n. f n ≠ f' n} ∪ {n. g n ≠ g' n})" by simp
    then show "finite {n. ¬ R (f n) (g n)}" by(rule finite_subset[rotated]) auto
  qed
qed

lemma rel_aeseq_mono: "R ≤ S ⟹ rel_aeseq R ≤ rel_aeseq S"
  by(rule predicate2I; transfer; auto intro: finite_subset[rotated])

lemma rel_aeseq_eq: "rel_aeseq (=) = (=)"
  by(intro ext; transfer; simp add: aeseq_eq.simps)

lemma rel_aeseq_conversep: "rel_aeseq R¯¯ = (rel_aeseq R)¯¯"
  by(simp add: fun_eq_iff; transfer; simp)

lemma map_aeseq_parametric: includes lifting_syntax shows
  "((A ===> B) ===> rel_aeseq A ===> rel_aeseq B) map_aeseq map_aeseq"
  by(intro rel_funI; transfer; auto elim: finite_subset[rotated] dest: rel_funD)

lemma rel_aeseq_distr: "rel_aeseq (R OO S) = rel_aeseq R OO rel_aeseq S"
  apply(intro ext)
  apply(transfer fixing: R S)
  apply(safe)
  subgoal for f h
    apply(rule relcomppI[where b="λn. SOME z. R (f n) z ∧ S z (h n)"])
    apply(auto elim!: finite_subset[rotated] intro: someI2)
    done
  subgoal for f h g
    apply(rule finite_subset[where B="{n. ¬ R (f n) (g n)} ∪ {n. ¬ S (g n) (h n)}"])
    apply auto
    done
  done

end