Theory Design_Isomorphisms

(* Title: Design_Isomorphisms
   Author: Chelsea Edmonds 
*)

section ‹Design Isomorphisms›

theory Design_Isomorphisms imports Design_Basics Sub_Designs
begin

subsection ‹Images of Set Systems›

text ‹We loosely define the concept of taking the "image" of a set system, as done in isomorphisms. 
Note that this is not based off mathematical theory, but is for ease of notation›
definition blocks_image :: "'a set multiset  ('a  'b)  'b set multiset" where
"blocks_image B f  image_mset ((`) f) B"

lemma image_block_set_constant_size: "size (B) = size (blocks_image B f)"
  by (simp add: blocks_image_def)

lemma (in incidence_system) image_set_system_wellformed: 
  "incidence_system (f ` 𝒱) (blocks_image  f)"
  by (unfold_locales, auto simp add: blocks_image_def) (meson image_eqI wf_invalid_point)

lemma (in finite_incidence_system) image_set_system_finite: 
  "finite_incidence_system (f ` 𝒱) (blocks_image  f)"
  using image_set_system_wellformed finite_sets 
  by (intro_locales) (simp_all add: blocks_image_def finite_incidence_system_axioms.intro)

subsection ‹Incidence System Isomorphisms›

text ‹Isomorphism's are defined by the Handbook of Combinatorial Designs 
cite"colbournHandbookCombinatorialDesigns2007"

locale incidence_system_isomorphism = source: incidence_system 𝒱  + target: incidence_system 𝒱' ℬ'
  for "𝒱" and "" and "𝒱'" and "ℬ'" + fixes bij_map ("π")
  assumes bij: "bij_betw π 𝒱 𝒱'"
  assumes block_img: "image_mset ((`) π)  = ℬ'"
begin

lemma iso_eq_order: "card 𝒱 = card 𝒱'"
  using bij bij_betw_same_card by auto

lemma iso_eq_block_num: "size  = size ℬ'"
  using block_img by (metis size_image_mset) 

lemma iso_block_img_alt_rep: "{# π ` bl . bl ∈# #} = ℬ'"
  using block_img by simp

lemma inv_iso_block_img: "image_mset ((`) (inv_into 𝒱 π)) ℬ' = "
proof - 
  have " x. x  𝒱  ((inv_into 𝒱 π)  π) x = x"
    using bij bij_betw_inv_into_left comp_apply by fastforce  
  then have " bl x . bl ∈#   x  bl   ((inv_into 𝒱 π)  π) x = x" 
    using source.wellformed by blast
  then have img: " bl . bl ∈#   image ((inv_into 𝒱 π)  π) bl = bl"
    by simp 
  have "image_mset ((`) (inv_into 𝒱 π)) ℬ' = image_mset ((`) (inv_into 𝒱 π)) (image_mset ((`) π) )" 
    using block_img by simp
  then have "image_mset ((`) (inv_into 𝒱 π)) ℬ' = image_mset ((`) ((inv_into 𝒱 π)  π)) " 
    by (metis (no_types, opaque_lifting) block_img comp_apply image_comp multiset.map_comp multiset.map_cong0)
  thus ?thesis using img by simp
qed

lemma inverse_incidence_sys_iso: "incidence_system_isomorphism 𝒱' ℬ' 𝒱  (inv_into 𝒱 π)"
  using bij bij_betw_inv_into inv_iso_block_img by (unfold_locales) simp

lemma iso_points_map: "π ` 𝒱 = 𝒱'"
  using bij by (simp add: bij_betw_imp_surj_on)

lemma iso_points_inv_map: "(inv_into 𝒱 π) `  𝒱' = 𝒱"
  using incidence_system_isomorphism.iso_points_map inverse_incidence_sys_iso by blast

lemma iso_points_ss_card: 
  assumes "ps  𝒱"
  shows "card ps = card (π ` ps)"
  using assms bij bij_betw_same_card bij_betw_subset by blast

lemma iso_block_in: "bl ∈#   (π ` bl) ∈# ℬ'"
  using iso_block_img_alt_rep
  by (metis image_eqI in_image_mset)

lemma iso_inv_block_in: "x ∈# ℬ'  x  (`) π ` set_mset "
  by (metis block_img in_image_mset)

lemma iso_img_block_orig_exists: "x ∈# ℬ'   bl . bl ∈#   x = π ` bl"
  using iso_inv_block_in by blast

lemma iso_blocks_map_inj: "x ∈#   y ∈#   π ` x = π ` y  x = y"
  using image_inv_into_cancel incidence_system.wellformed iso_points_inv_map iso_points_map
  by (metis (no_types, lifting) source.incidence_system_axioms subset_image_iff)

lemma iso_bij_betwn_block_sets: "bij_betw ((`) π) (set_mset ) (set_mset ℬ')"
  apply ( simp add: bij_betw_def inj_on_def)
  using iso_block_in iso_inv_block_in iso_blocks_map_inj by auto 

lemma iso_bij_betwn_block_sets_inv: "bij_betw ((`) (inv_into 𝒱 π)) (set_mset ℬ') (set_mset )"
  using incidence_system_isomorphism.iso_bij_betwn_block_sets inverse_incidence_sys_iso by blast 

lemma iso_bij_betw_individual_blocks: "bl ∈#   bij_betw π bl (π ` bl)"
  using bij bij_betw_subset source.wellformed by blast 

lemma iso_bij_betw_individual_blocks_inv: "bl ∈#   bij_betw (inv_into 𝒱 π) (π ` bl) bl"
  using bij bij_betw_subset source.wellformed bij_betw_inv_into_subset by fastforce 

lemma iso_bij_betw_individual_blocks_inv_alt: 
    "bl ∈# ℬ'  bij_betw (inv_into 𝒱 π) bl ((inv_into 𝒱 π) ` bl)"
  using incidence_system_isomorphism.iso_bij_betw_individual_blocks inverse_incidence_sys_iso
  by blast 
  
lemma iso_inv_block_in_alt:  "(π ` bl) ∈# ℬ'  bl  𝒱  bl ∈# "
  using image_eqI image_inv_into_cancel inv_iso_block_img iso_points_inv_map
  by (metis (no_types, lifting) iso_points_map multiset.set_map subset_image_iff)

lemma iso_img_block_not_in: 
  assumes "x ∉# "
  assumes "x  𝒱"
  shows "(π ` x) ∉# ℬ'"
proof (rule ccontr)
  assume a: "¬ π ` x ∉# ℬ'"
  then have a: "π ` x ∈# ℬ'" by simp
  then have " y . y  (π ` x)  (inv_into 𝒱 π) y  𝒱"
    using target.wf_invalid_point iso_points_inv_map by auto 
  then have "((`) (inv_into 𝒱 π)) (π ` x) ∈# " 
    using iso_bij_betwn_block_sets_inv by (meson a bij_betw_apply) 
  thus False
    using a assms(1) assms(2) iso_inv_block_in_alt by blast 
qed

lemma iso_block_multiplicity:
  assumes  "bl  𝒱" 
  shows "source.multiplicity bl = target.multiplicity (π ` bl)"
proof (cases "bl ∈# ")
  case True
  have "inj_on ((`) π) (set_mset )"
    using bij_betw_imp_inj_on iso_bij_betwn_block_sets by auto 
  then have "count  bl = count ℬ' (π ` bl)" 
    using count_image_mset_le_count_inj_on count_image_mset_ge_count True block_img inv_into_f_f 
      less_le_not_le order.not_eq_order_implies_strict by metis  
  thus ?thesis by simp
next
  case False
  have s_mult: "source.multiplicity bl = 0"
    by (simp add: False count_eq_zero_iff) 
  then have "target.multiplicity (π ` bl) = 0"
    using False count_inI iso_inv_block_in_alt
    by (metis assms) 
  thus ?thesis
    using s_mult by simp
qed

lemma iso_point_in_block_img_iff: "p  𝒱  bl ∈#   p  bl  (π p)  (π ` bl)"
  by (metis bij bij_betw_imp_surj_on iso_bij_betw_individual_blocks_inv bij_betw_inv_into_left imageI)

lemma iso_point_subset_block_iff: "p  𝒱  bl ∈#   p  bl  (π ` p)  (π ` bl)"
  apply auto
  using image_subset_iff iso_point_in_block_img_iff subset_iff by metis

lemma iso_is_image_block: "ℬ' = blocks_image  π"
  unfolding blocks_image_def by (simp add: block_img iso_points_map)

end

subsection ‹Design Isomorphisms›
text ‹Apply the concept of isomorphisms to designs only›

locale design_isomorphism = incidence_system_isomorphism 𝒱  𝒱' ℬ' π + source: design 𝒱  + 
  target: design 𝒱' ℬ' for 𝒱 and  and 𝒱' and ℬ' and bij_map ("π")
  
context design_isomorphism
begin

lemma inverse_design_isomorphism: "design_isomorphism 𝒱' ℬ' 𝒱  (inv_into 𝒱 π)"
  using inverse_incidence_sys_iso source.wf_design target.wf_design
  by (simp add: design_isomorphism.intro) 

end

subsubsection ‹Isomorphism Operation›
text ‹Define the concept of isomorphic designs outside the scope of locale›

definition isomorphic_designs (infixl "D" 50) where
"𝒟 D 𝒟'  ( π . design_isomorphism (fst 𝒟) (snd 𝒟) (fst 𝒟') (snd 𝒟') π)"

lemma isomorphic_designs_symmetric: "(𝒱, ) D (𝒱', ℬ')  (𝒱', ℬ') D (𝒱, )"
  using isomorphic_designs_def design_isomorphism.inverse_design_isomorphism
  by metis

lemma isomorphic_designs_implies_bij: "(𝒱, ) D (𝒱', ℬ')   π . bij_betw π 𝒱 𝒱'"
  using incidence_system_isomorphism.bij isomorphic_designs_def
  by (metis design_isomorphism.axioms(1) fst_conv)

lemma isomorphic_designs_implies_block_map: "(𝒱, ) D (𝒱', ℬ')   π . image_mset ((`) π)  = ℬ'"
  using incidence_system_isomorphism.block_img isomorphic_designs_def
  using design_isomorphism.axioms(1) by fastforce

context design
begin 

lemma isomorphic_designsI [intro]: "design 𝒱' ℬ'  bij_betw π 𝒱 𝒱'  image_mset ((`) π)  = ℬ' 
     (𝒱, ) D (𝒱', ℬ')"
  using design_isomorphism.intro isomorphic_designs_def wf_design image_set_system_wellformed
  by (metis bij_betw_imp_surj_on blocks_image_def fst_conv incidence_system_axioms 
      incidence_system_isomorphism.intro incidence_system_isomorphism_axioms_def snd_conv)

lemma eq_designs_isomorphic: 
  assumes "𝒱 = 𝒱'"
  assumes " = ℬ'"
  shows "(𝒱, ) D (𝒱', ℬ')" 
proof -
  interpret d1: design 𝒱  using assms
    using wf_design by auto 
  interpret d2: design 𝒱' ℬ' using assms
    using wf_design by blast 
  have "design_isomorphism 𝒱  𝒱' ℬ' id" using assms by (unfold_locales) simp_all
  thus ?thesis unfolding isomorphic_designs_def by auto
qed

end

context design_isomorphism
begin

subsubsection ‹Design Properties/Operations under Isomorphism›

lemma design_iso_point_rep_num_eq: 
  assumes "p  𝒱"
  shows " rep p = ℬ' rep (π p)"
proof -
  have "{#b ∈#  . p  b#} = {#b ∈#  . π p  π ` b#}" 
    using assms filter_mset_cong iso_point_in_block_img_iff assms by force
  then have "{#b ∈# ℬ' . π p  b#} = image_mset ((`) π) {#b ∈#  . p  b#}"
    by (simp add: image_mset_filter_swap block_img)
  thus ?thesis
    by (simp add: point_replication_number_def) 
qed

lemma design_iso_rep_numbers_eq: "source.replication_numbers = target.replication_numbers"
  apply (simp add: source.replication_numbers_def target.replication_numbers_def)
  using  design_iso_point_rep_num_eq design_isomorphism.design_iso_point_rep_num_eq iso_points_map
  by (metis (no_types, lifting) inverse_design_isomorphism iso_points_inv_map rev_image_eqI)

lemma design_iso_block_size_eq: "bl ∈#   card bl = card (π ` bl)"
  using card_image_le finite_subset_image image_inv_into_cancel
  by (metis iso_points_inv_map iso_points_map le_antisym source.finite_blocks source.wellformed)
  
lemma design_iso_block_sizes_eq: "source.sys_block_sizes = target.sys_block_sizes"
  apply (simp add: source.sys_block_sizes_def target.sys_block_sizes_def)
  by (metis (no_types, lifting) design_iso_block_size_eq iso_block_in iso_img_block_orig_exists)

lemma design_iso_points_index_eq: 
  assumes "ps  𝒱" 
  shows " index ps = ℬ' index (π ` ps)"
proof - 
  have " b . b ∈#   ((ps  b) = ((π ` ps)  π ` b))" 
    using iso_point_subset_block_iff assms by blast
  then have "{#b ∈#  . ps  b#} = {#b ∈#  . (π ` ps)  (π ` b)#}" 
    using assms filter_mset_cong by force  
  then have "{#b ∈# ℬ' . π ` ps  b#} = image_mset ((`) π) {#b ∈#  . ps  b#}"
    by (simp add: image_mset_filter_swap block_img)
  thus ?thesis
    by (simp add: points_index_def)
qed

lemma design_iso_points_indices_imp: 
  assumes "x  source.point_indices t"
  shows "x  target.point_indices t"
proof - 
  obtain ps where t: "card ps = t" and ss: "ps  𝒱" and x: " index ps = x" using assms
    by (auto simp add: source.point_indices_def)
  then have x_val: "x = ℬ' index (π ` ps)" using design_iso_points_index_eq by auto
  have x_img: " (π ` ps)  𝒱'" 
    using ss bij iso_points_map by fastforce 
  then have "card (π ` ps) = t" using t ss iso_points_ss_card by auto
  then show ?thesis using target.point_indices_elem_in x_img x_val by blast 
qed

lemma design_iso_points_indices_eq: "source.point_indices t = target.point_indices t"
  using inverse_design_isomorphism design_isomorphism.design_iso_points_indices_imp
    design_iso_points_indices_imp by blast 

lemma design_iso_block_intersect_num_eq: 
  assumes "b1 ∈# "
  assumes "b2 ∈# "
  shows "b1 |∩| b2 = (π ` b1) |∩| (π ` b2)"
proof -
  have split: "π ` (b1  b2) = (π ` b1)  (π ` b2)" using assms bij bij_betw_inter_subsets
    by (metis source.wellformed) 
  thus ?thesis using source.wellformed
    by (simp add: intersection_number_def iso_points_ss_card split assms(2) inf.coboundedI2) 
qed

lemma design_iso_inter_numbers_imp: 
  assumes "x  source.intersection_numbers" 
  shows "x  target.intersection_numbers"
proof - 
  obtain b1 b2 where 1: "b1 ∈# " and 2: "b2 ∈# (remove1_mset b1 )" and xval: "x = b1 |∩| b2" 
    using assms by (auto simp add: source.intersection_numbers_def)
  then have pi1: "π ` b1 ∈# ℬ'" by (simp add: iso_block_in)
  have pi2: "π ` b2 ∈# (remove1_mset (π ` b1) ℬ')" using iso_block_in 2
    by (metis (no_types, lifting) "1" block_img image_mset_remove1_mset_if in_remove1_mset_neq 
        iso_blocks_map_inj more_than_one_mset_mset_diff multiset.set_map)
  have "x = (π ` b1) |∩| (π ` b2)" using 1 2 design_iso_block_intersect_num_eq
    by (metis in_diffD xval)
  then have "x  {b1 |∩| b2 | b1 b2 . b1 ∈# ℬ'  b2 ∈# (ℬ' - {#b1#})}" 
    using pi1 pi2 by blast
  then show ?thesis by (simp add: target.intersection_numbers_def) 
qed

lemma design_iso_intersection_numbers: "source.intersection_numbers = target.intersection_numbers"
  using inverse_design_isomorphism design_isomorphism.design_iso_inter_numbers_imp 
      design_iso_inter_numbers_imp by blast

lemma design_iso_n_intersect_num: 
  assumes "b1 ∈# " 
  assumes "b2 ∈# " 
  shows "b1 |∩|⇩n b2 = ((π ` b1) |∩|⇩n (π ` b2))"
proof -
  let ?A = "{x . x  b1  x  b2  card x = n}"
  let ?B = "{y . y  (π ` b1)  y  (π ` b2)  card y = n}"
  have b1v: "b1  𝒱"  by (simp add: assms(1) source.wellformed) 
  have b2v: "b2  𝒱"  by (simp add: assms(2) source.wellformed) 
  then have "x y . x  b1  x  b2  y  b1  y  b2   π ` x = π ` y  x = y"
    using b1v bij by (metis bij_betw_imp_surj_on bij_betw_inv_into_subset dual_order.trans)
  then have inj: "inj_on ((`) π) ?A" by (simp add: inj_on_def)
  have eqcard: "xa. xa  b1  xa  b2  card (π ` xa) = card xa" using b1v b2v bij
    using iso_points_ss_card by auto 
  have surj: "x. x  π ` b1  x  π ` b2   
                x  {(π ` xa) | xa . xa  b1  xa  b2  card xa = card x}"
  proof - 
    fix x
    assume x1: "x  π ` b1" and x2: "x  π ` b2" 
    then obtain xa where eq_x: "π ` xa = x" and ss: "xa  𝒱"
      by (metis b1v dual_order.trans subset_imageE)
    then have f1: "xa  b1" by (simp add: x1 assms(1) iso_point_subset_block_iff) 
    then have f2: "xa  b2" by (simp add: eq_x ss assms(2) iso_point_subset_block_iff x2) 
    then have f3: "card xa = card x" using bij by (simp add: eq_x ss iso_points_ss_card)
    then show "x  {(π ` xa) | xa . xa  b1  xa  b2  card xa = card x}" 
      using f1 f2 f3 π ` xa = x by auto
  qed
  have "bij_betw ( (`) π) ?A ?B"
  proof (auto simp add: bij_betw_def)
    show "inj_on ((`) π) {x. x  b1  x  b2  card x = n}" using inj by simp
    show "xa. xa  b1  xa  b2  n = card xa  card (π ` xa) = card xa" 
      using eqcard by simp
    show "x. x  π ` b1  x  π ` b2  n = card x  
            x  (`) π ` {xa. xa  b1  xa  b2  card xa = card x}" 
      using surj by (simp add: setcompr_eq_image)
  qed
  thus ?thesis
    using bij_betw_same_card by (auto simp add: n_intersect_number_def)
qed

lemma subdesign_iso_implies:
  assumes "sub_set_system V B 𝒱 "
  shows "sub_set_system (π ` V) (blocks_image B π) 𝒱' ℬ'"
proof (unfold_locales)
  show "π ` V  𝒱'" 
    by (metis assms image_mono iso_points_map sub_set_system.points_subset) 
  show "blocks_image B π ⊆# ℬ'"
    by (metis assms block_img blocks_image_def image_mset_subseteq_mono sub_set_system.blocks_subset) 
qed

lemma subdesign_image_is_design: 
  assumes "sub_set_system V B 𝒱 "
  assumes "design V B"
  shows "design (π ` V) (blocks_image B π)"
proof -
  interpret fin: finite_incidence_system "(π ` V)" "(blocks_image B π)" using assms(2)
    by (simp add: design.axioms(1) finite_incidence_system.image_set_system_finite)
  interpret des: sub_design V B 𝒱  using assms design.wf_design_iff
    by (unfold_locales, auto simp add: sub_set_system.points_subset sub_set_system.blocks_subset)
  have bl_img: "blocks_image B π ⊆# ℬ'"
    by (simp add: blocks_image_def des.blocks_subset image_mset_subseteq_mono iso_is_image_block)  
  then show ?thesis 
  proof (unfold_locales, auto)
    show "{} ∈# blocks_image B π  False" 
      using assms subdesign_iso_implies target.blocks_nempty bl_img by auto
  qed
qed

lemma sub_design_isomorphism: 
  assumes "sub_set_system V B 𝒱 "
  assumes "design V B"
  shows "design_isomorphism V B (π ` V) (blocks_image B π) π"
proof -
  interpret design "(π ` V)" "(blocks_image B π)"
    by (simp add: assms(1) assms(2) subdesign_image_is_design)
  interpret des: design V B by fact
  show ?thesis
  proof (unfold_locales)
    show "bij_betw π V (π ` V)" using bij
      by (metis assms(1) bij_betw_subset sub_set_system.points_subset) 
    show "image_mset ((`) π) B = blocks_image B π" by (simp add: blocks_image_def)
  qed
qed

end
end