Theory PiE_Rel_Extras

(* Theory: PiE_Rel_Extras
   Author: Chelsea Edmonds *)

section‹Extensional function extras›
text‹Counting lemmas (i.e. reasoning on cardinality) of sets on the extensional function relation ›

theory PiE_Rel_Extras imports Card_Partitions.Card_Partitions
begin

subsection ‹Relations and Extensional Function sets ›
text ‹A number of lemmas to convert between relations and functions for counting purposes. 
Note, ultimately not needed in this formalisation, but may be of use in the future ›

lemma Range_unfold: "Range r = {y. ∃x. (x, y) ∈ r}"
  by blast

definition fun_to_rel:: " 'a set ⇒ 'b set  ⇒ ('a ⇒ 'b) ⇒('a × 'b) set" where
"fun_to_rel A B f ≡ {(a, b) | a b . a ∈ A ∧ b ∈ B ∧ f a = b}"

definition rel_to_fun:: "('a × 'b) set ⇒ ('a ⇒ 'b)" where
"rel_to_fun R ≡ λ a . (if a ∈ Domain R then (THE b . (a, b) ∈ R) else undefined)"

lemma fun_to_relI: "a ∈ A ⟹ b ∈ B ⟹ f a = b ⟹ (a, b) ∈ fun_to_rel A B f"
  unfolding fun_to_rel_def by auto

lemma fun_to_rel_alt: "fun_to_rel A B f ≡ {(a, f a) | a b . a ∈ A ∧ f a ∈ B}"
  unfolding fun_to_rel_def by simp 

lemma fun_to_relI2: "a ∈ A ⟹ f a ∈ B  ⟹ (a, f a) ∈ fun_to_rel A B f"
  using fun_to_rel_alt by fast

lemma rel_to_fun_in[simp]: "a ∈ Domain R ⟹ (rel_to_fun R) a = (THE b . (a, b) ∈ R)"
  unfolding rel_to_fun_def by simp

lemma rel_to_fun_undefined[simp]: "a ∉ Domain R ⟹ (rel_to_fun R) a = undefined"
  unfolding rel_to_fun_def by simp

lemma single_valued_unique_Dom_iff: "single_valued R ⟷ (∀ x ∈ Domain R. ∃! y . (x, y) ∈ R)"
  using single_valued_def by fastforce 

lemma rel_to_fun_range:
  assumes "single_valued R"
  assumes "a ∈ Domain R"
  shows "(THE b . (a, b) ∈ R) ∈ Range R"
  using single_valued_unique_Dom_iff
  by (metis Range_iff assms(1) assms(2) theI') 

lemma rel_to_fun_extensional: "single_valued R ⟹ rel_to_fun R ∈ (Domain R →⇩E Range R)"
  by (intro PiE_I) (simp_all add: rel_to_fun_range)

lemma single_value_fun_to_rel:  "single_valued (fun_to_rel A B f)"
  unfolding single_valued_def fun_to_rel_def
  by simp

lemma fun_to_rel_domain: 
  assumes "f ∈ A →⇩E B"
  shows "Domain (fun_to_rel A B f) = A"
  unfolding fun_to_rel_def using assms by (auto simp add: subset_antisym subsetI Domain_unfold)

lemma fun_to_rel_range: 
  assumes "f ∈ A →⇩E B"
  shows "Range (fun_to_rel A B f) ⊆ B"
  unfolding fun_to_rel_def using assms by (auto simp add: subsetI Range_unfold)

lemma rel_to_fun_to_rel: 
  assumes "f ∈ A →⇩E B"
  shows "rel_to_fun (fun_to_rel A B f) = f"
proof (intro ext allI)
  fix x
  show "rel_to_fun (fun_to_rel A B f) x = f x"
  proof (cases "x ∈ A")
    case True
    then have ind: "x ∈ Domain (fun_to_rel A B f)" using fun_to_rel_domain assms 
      by blast
    have "(x, f x) ∈ fun_to_rel A B f" using fun_to_rel_alt True single_value_fun_to_rel
      using assms by fastforce 
    moreover have "rel_to_fun (fun_to_rel A B f) x = (THE b. (x, b) ∈ (fun_to_rel A B f))" by (simp add: ind)
    ultimately show ?thesis using single_value_fun_to_rel single_valuedD the_equality
      by (metis (no_types, lifting)) 
  next
    case False
    then have "x ∉ Domain (fun_to_rel A B f)" unfolding fun_to_rel_def
      by blast 
    then show ?thesis
      using False assms by auto 
  qed
qed

lemma fun_to_rel_to_fun: 
  assumes "single_valued R"
  shows "fun_to_rel (Domain R) (Range R) (rel_to_fun R) = R"
proof (intro subset_antisym subsetI)
  fix x assume "x ∈ fun_to_rel (Domain R) (Range R) (rel_to_fun R)"
  then obtain a b where "x = (a, b)" and "a ∈ Domain R" and "b ∈ Range R" and "(rel_to_fun R a) = b"
    using fun_to_rel_def by (smt (verit) mem_Collect_eq) 
  then have "b = (THE b'. (a, b') ∈ R)" using rel_to_fun_in
    by simp 
  then show "x ∈ R"
    by (metis (no_types, lifting) ‹a ∈ Domain R› ‹x = (a, b)› assms single_valued_unique_Dom_iff the1_equality)
next
  fix x assume "x ∈ R"
  then obtain a b where "x = (a, b)" and "(a, b) ∈ R" and "∀ c . (a, c) ∈ R ⟶ b = c"
    using assms
    by (metis prod.collapse single_valued_def)
  then have "a ∈ Domain R" "b ∈ Range R" by blast+
  then have "b = (THE b' . (a, b') ∈ R)"
    by (metis ‹∀c. (a, c) ∈ R ⟶ b = c› ‹x = (a, b)› ‹x ∈ R› the_equality) 
  then have "(a, b) ∈ fun_to_rel (Domain R) (Range R) (rel_to_fun R)"
    using ‹a ∈ Domain R› ‹b ∈ Range R› by (intro fun_to_relI) (simp_all)
  then show "x ∈ fun_to_rel (Domain R) (Range R) (rel_to_fun R)" using ‹x = (a, b)› by simp
qed

lemma bij_betw_fun_to_rel: 
  assumes "f ∈ A →⇩E B"
  shows "bij_betw (λ a . (a, f a)) A (fun_to_rel A B f)"
proof (intro bij_betw_imageI inj_onI)
  show "⋀x y. x ∈ A ⟹ y ∈ A ⟹ (x, f x) = (y, f y) ⟹ x = y" by simp
next
  show "(λa. (a, f a)) ` A = fun_to_rel A B f"
  proof (intro subset_antisym subsetI)
    fix x assume "x ∈ (λa. (a, f a)) ` A"
    then obtain a where "a ∈ A" and "x = (a, f a)" by blast
    then show "x ∈ fun_to_rel A B f" using fun_to_rel_alt assms
      by fastforce 
  next
    fix x assume "x ∈ fun_to_rel A B f"
    then show "x ∈ (λa. (a, f a)) ` A" using fun_to_rel_alt
      using image_iff by fastforce 
  qed
qed

lemma fun_to_rel_indiv_card: 
  assumes "f ∈ A →⇩E B"
  shows "card (fun_to_rel A B f) = card A"
  using bij_betw_fun_to_rel assms bij_betw_same_card[of "(λ a . (a, f a))" A "(fun_to_rel A B f)"]
  by (metis)

lemma fun_to_rel_inj: 
  assumes "C ⊆ A →⇩E B"
  shows "inj_on (fun_to_rel A B) C"
proof (intro inj_onI ext allI)
  fix f g x  assume fin: "f ∈ C" and gin: "g ∈ C" and eq: "fun_to_rel A B f = fun_to_rel A B g"
  then show "f x = g x"
  proof (cases "x ∈ A")
    case True
    then have "(x, f x) ∈ fun_to_rel A B f" using fun_to_rel_alt
      by (smt (verit) PiE_mem assms fin fun_to_rel_def mem_Collect_eq subset_eq)
    moreover have "(x, g x) ∈ fun_to_rel A B g" using fun_to_rel_alt True
      by (smt (verit) PiE_mem assms fun_to_rel_def gin mem_Collect_eq subset_eq)
    ultimately show ?thesis  using eq single_value_fun_to_rel single_valued_def
      by metis 
  next
    case False
    then have "f x = undefined" "g x = undefined" using fin gin assms by auto 
    then show ?thesis by simp
  qed
qed

lemma fun_to_rel_ss: "fun_to_rel A B f ⊆ A × B"
  unfolding fun_to_rel_def by auto

lemma card_fun_to_rel: "C ⊆ A →⇩E B ⟹ card C = card ((λ f . fun_to_rel A B f ) ` C)"
  using card_image fun_to_rel_inj by metis 

subsection ‹Cardinality Lemmas ›
text ‹Lemmas to count variations of filtered sets over the extensional function set relation ›

lemma card_PiE_filter_range_set:
  assumes "⋀ a. a ∈ A' ⟹ X a ∈ C"
  assumes "A' ⊆ A"
  assumes "finite A"
  shows "card {f ∈ A →⇩E C . ∀ a ∈ A' . f a = X a} = (card C)^(card A - card A')"
proof -
  have finA: "finite A'" using assms(3) finite_subset assms(2) by auto 
  have c1: "card (A - A') = card A - card A'" using assms(2)
  using card_Diff_subset finA by blast 
  define g :: "('a  ⇒ 'b) ⇒ ('a  ⇒ 'b)" where "g ≡ λ f. (λ a' . if a' ∈ A' then undefined else f a')"
  have "bij_betw g {f ∈ A →⇩E C . ∀ a ∈ A' . f a = X a} ((A - A') →⇩E C)"
  proof (intro bij_betw_imageI inj_onI)
    fix h h' assume h1in: "h ∈ {f ∈ A →⇩E C. ∀ a ∈ A' . f a = X a}" and h2in: "h' ∈ {f ∈ A →⇩E C. ∀ a ∈ A' . f a = X a}" "g h = g h'"
    then have eq: "(λ a' . if a' ∈ A' then undefined  else h a') = (λ a' .  if a' ∈ A' then undefined else h' a')"
      using g_def by simp
    show "h = h'"
    proof (intro ext allI)
      fix x
      show "h x = h' x" using h1in h2in eq by (cases "x ∈ A'", simp, meson)
    qed
  next
    show "g ` {f ∈ A →⇩E C. ∀ a ∈ A' . f a = X a} = A - A' →⇩E C"
    proof (intro subset_antisym subsetI)
      fix g' assume "g' ∈ g ` {f ∈ A →⇩E C. ∀ a ∈ A' . f a = X a}"
      then obtain f' where geq: "g' = g f'" and fin: "f' ∈ A →⇩E C" and "∀ a ∈ A' . f' a = X a"
        by blast
      show "g' ∈ A - A' →⇩E C"
        using g_def fin geq by (intro PiE_I)(auto)
    next
      fix g' assume gin: "g' ∈ A - A' →⇩E C"
      define f' where "f' = (λ a' . (if a' ∈ A' then X a' else g' a'))" 
      then have eqc: "∀ a' ∈ A' . f' a' = X a'" by auto
      have fin: "f' ∈ A →⇩E C"
      proof (intro PiE_I)
        fix x assume "x ∈ A"
        have "x ∉ A' ⟹ f' x = g' x" using f'_def by auto
        moreover have "x ∈ A' ⟹ f' x = X x" using f'_def by (simp add: ‹x ∈ A›) 
        ultimately show "f' x ∈ C"
          using gin  PiE_E ‹x ∈ A› assms(1)[of x] by (metis Diff_iff) 
      next
        fix x assume "x ∉ A"
        then show "f' x = undefined"
          using f'_def gin assms(2) by auto 
      qed
      have "g' = g f'" unfolding f'_def g_def 
        by (auto simp add: fun_eq_iff) (metis DiffE PiE_arb gin) 
      then show "g' ∈ g ` {f ∈ A →⇩E C. ∀ a ∈ A' . f a = X a}" using fin eqc by blast
    qed
  qed
  then have "card {f ∈ A →⇩E C . ∀ a ∈ A' . f a = X a} = card ((A - A') →⇩E C)"
    using bij_betw_same_card by blast
  also have "... = (card C)^card (A - A')" 
    using card_funcsetE assms(3) by (metis finite_Diff) 
  finally show ?thesis using c1 by auto
qed

lemma card_PiE_filter_range_indiv: "X a' ∈ C ⟹ a' ∈ A ⟹ finite A ⟹
    card {f ∈ A →⇩E C . f a' = X a'} = (card C)^(card A - 1)"
  using card_PiE_filter_range_set[of "{a'}" X C A ] by auto

lemma card_PiE_filter_range_set_const: "c ∈ C ⟹ A' ⊆ A ⟹ finite A ⟹ 
    card {f ∈ A →⇩E C . ∀ a ∈ A' . f a = c} = (card C)^(card A - card A')"
  using card_PiE_filter_range_set[of A' "λ a . c"] by auto

lemma card_PiE_filter_range_set_nat: "c ∈ {0..<n} ⟹ A' ⊆ A ⟹ finite A ⟹
    card {f ∈ A →⇩E {0..<n} . ∀ a ∈ A' . f a = c} = n^(card A - card A')"
  using card_PiE_filter_range_set_const[of c "{0..<n}" A' A] by auto

end