Theory FAE_Sequence

theory FAE_Sequence
  imports "HOL-Library.Confluent_Quotient"
begin

type_synonym 'a seq = "nat ⇒ 'a"

abbreviation finite_range :: "('a ⇒ 'b) ⇒ bool" where "finite_range f ≡ finite (range f)"

lemma finite_range_pair:
  assumes 1: "finite_range (λx. fst (f x))" and 2: "finite_range (λx. snd (f x))"
  shows "finite_range f"
proof -
  have "range f ⊆ range (λx. fst (f x)) × range (λx. snd (f x))"
    by(auto 4 3 intro: rev_image_eqI dest: sym)
  then show ?thesis by(rule finite_subset)(use assms in simp)
qed

definition seq_at :: "'a seq ⇒ 'a ⇒ nat set" where "seq_at f x = f -` {x}"

typedef 'a fseq = "{f :: 'a seq. finite_range f}" morphisms ap_fseq Abs_fseq
  by(rule exI[where x="λ_. undefined"]) simp

setup_lifting type_definition_fseq

lift_bnf 'a fseq [wits: "λx. (λ_ :: nat. x)"]
  subgoal by(metis finite_imageI fun.set_map mem_Collect_eq)
  subgoal by(auto intro: finite_range_pair)
  subgoal by auto
  subgoal by auto
  done

lemma ap_map_fseq [simp]: "ap_fseq (map_fseq f x) = f ∘ ap_fseq x"
  by transfer simp

lift_definition fseq_eq :: "'a fseq ⇒ 'a fseq ⇒ bool" is "λf g. finite {n. f n ≠ g n}" .

lemma fseq_eq_unfold: "fseq_eq f g ⟷ finite {n. ap_fseq f n ≠ ap_fseq g n}"
  by transfer simp

lemma reflp_fseq_eq [simp]: "reflp fseq_eq"
  by(rule reflpI)(simp add: fseq_eq_unfold)

lemma symp_fseq_eq [simp]: "symp fseq_eq"
  by(rule sympI)(simp add: fseq_eq_unfold eq_commute)

lemma transp_fseq_eq [simp]: "transp fseq_eq"
  apply(rule transpI)
  subgoal for f g h unfolding fseq_eq_unfold
    by(rule finite_subset[where B="{n. ap_fseq f n ≠ ap_fseq g n} ∪ {n. ap_fseq g n ≠ ap_fseq h n}"]) auto
  done

lemma equivp_fseq_eq [simp]: "equivp fseq_eq"
  by(simp add: equivp_reflp_symp_transp)

functor map_fseq
  by(simp_all add: fseq.map_id0 fseq.map_comp fun_eq_iff)

quotient_type 'a fae_seq = "'a fseq" / fseq_eq by simp

lemma map_fseq_eq: "fseq_eq f g ⟹ fseq_eq (map_fseq h f) (map_fseq h g)"
  unfolding fseq_eq_unfold by(auto elim!: finite_subset[rotated])

lemma finite_set_fseq [simp]: "finite (set_fseq x)"
  by transfer

interpretation wide_intersection_fseq: wide_intersection_finite fseq_eq map_fseq set_fseq
  by unfold_locales(simp_all add: map_fseq_eq fseq.map_id[unfolded id_def] fseq.set_map cong: fseq.map_cong)

lemma fseq_subdistributivity:
  assumes "A OO B ≠ bot"
  shows "rel_fseq A OO fseq_eq OO rel_fseq B ≤ fseq_eq OO rel_fseq (A OO B) OO fseq_eq"
proof(rule predicate2I; elim relcomppE; transfer fixing: A B)
  fix f and g g' :: "'c seq" and h
  assume fg: "rel_fun(=) A f g" and gg': "finite {n. g n ≠ g' n}" and g'h: "rel_fun (=) B g' h"
    and f: "finite_range f" and g: "finite_range g" and g': "finite_range g'" and h: "finite_range h"
  from assms obtain a c b where ac: "A a c" and cb: "B c b" by(auto simp add: fun_eq_iff)
  let ?X = "{n. g n ≠ g' n}"
  let ?f = "λn. if n ∈ ?X then a else f n"
  let ?h = "λn. if n ∈ ?X then b else h n"
  have "range ?f ⊆ insert a (range f)" by auto
  then have "finite_range ?f" by(rule finite_subset)(simp add: f)
  moreover have "range ?h ⊆ insert b (range h)" by auto
  then have "finite_range ?h" by(rule finite_subset)(simp add: h)
  moreover have "{n. f n ≠ ?f n} ⊆ ?X" by auto
  then have "finite {n. f n ≠ ?f n}" by(rule finite_subset)(simp add: gg')
  moreover have "{n. ?h n ≠ h n} ⊆ ?X" by auto
  then have "finite {n. ?h n ≠ h n}" by(rule finite_subset)(simp add: gg')
  moreover have "rel_fun (=) (A OO B) ?f ?h" using fg g'h ac cb by(auto simp add: rel_fun_def)
  ultimately
  show "∃ya∈{f. finite_range f}. finite {n. f n ≠ ya n} ∧ (∃yb∈{f. finite_range f}. rel_fun (=) (A OO B) ya yb ∧ finite {n. yb n ≠ h n})"
    unfolding mem_Collect_eq Bex_def by blast
qed

lift_bnf 'a fae_seq
  subgoal by(rule fseq_subdistributivity)
  subgoal by(rule wide_intersection_fseq.wide_intersection)
  done

lift_definition fseq_at :: "'a fseq ⇒ 'a ⇒ nat set" is seq_at .

lemma fae_vimage_singleton: "finite (f -` {x}) ⟷ finite (g -` {x})" if "finite {n. f n ≠ g n}"
proof
  assume *: "finite (g -` {x})"
  have "f -` {x} ⊆ g -` {x} ∪ {n. f n ≠ g n}" by auto
  thus "finite (f -` {x})" by(rule finite_subset)(use that * in auto)
next
  assume *: "finite (f -` {x})"
  have "g -` {x} ⊆ f -` {x} ∪ {n. f n ≠ g n}" by auto
  thus "finite (g -` {x})" by(rule finite_subset)(use that * in auto)
qed

lift_definition set_fae_seq_alt :: "'a fae_seq ⇒ 'a set" is "λf. {a. infinite (fseq_at f a)}"
  by(transfer)(clarsimp simp add: set_eq_iff seq_at_def fae_vimage_singleton)

lemma fseq_at_infinite_Inr:
  "⟦infinite (fseq_at f x); fseq_eq (map_fseq Inr f) g⟧ ⟹ ∃x'∈set_fseq g. x ∈ Basic_BNFs.setr x'"
  apply transfer
  apply (auto simp add: seq_at_def vimage_def)
  apply (smt (verit, ccfv_SIG) finite_subset mem_Collect_eq setr.simps subsetI)
  done

lemma fseq_at_Inr_infinite:
  assumes "⋀g. fseq_eq (map_fseq Inr f) g ⟶ (∃x'∈set_fseq g. x ∈ Basic_BNFs.setr x')"
  shows "infinite (fseq_at f x)"
proof
  assume fin: "finite (fseq_at f x)"
  let ?g = "map_fseq (λy. if x = y then Inl undefined else Inr y) f"
  have "fseq_eq (map_fseq Inr f) ?g" using fin
    by transfer(simp add: seq_at_def vimage_def eq_commute)
  with assms[of "?g"] show False by(auto simp add: fseq.set_map)
qed

lemma set_fae_seq_eq_alt: "set_fae_seq f = set_fae_seq_alt f"
  by transfer(use fseq_at_Inr_infinite in ‹force simp add: fseq_at_infinite_Inr›)

end