Theory Lovasz_Local.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