Theory Dual_Systems

(* Title: Dual_Systems.thy
   Author: Chelsea Edmonds
*)

section ‹ Dual Systems ›
text ‹The concept of a dual incidence system \<^cite>‹"colbournHandbookCombinatorialDesigns2007"›
 is an important property in design theory. It enables us to reason on the existence of several 
different types of design constructs through dual properties \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"››

theory Dual_Systems imports Incidence_Matrices
begin

subsection ‹Dual Blocks ›
text ‹A dual design of $(\mathcal{V}, \mathcal{B})$, is the design where each block in $\mathcal{B}$
represents a point $x$, and a block in a dual design is a set of blocks which $x$ is in from the original design. 
It is important to note that if a block repeats in $\mathcal{B}$, each instance of the block is a distinct point. 
As such the definition below uses each block's list index as its identifier. The list of points would simply be the 
indices $0..<$length $Bs$ ›   

definition dual_blocks :: "'a set ⇒ 'a set list ⇒ nat set multiset" where
"dual_blocks 𝒱 ℬs ≡ {# {y . y < length ℬs ∧ x ∈ ℬs ! y} . x ∈# (mset_set 𝒱)#}"

lemma dual_blocks_wf: "b ∈# dual_blocks V Bs ⟹ b ⊆ {0..<length Bs}"
  by (auto simp add: dual_blocks_def)

context ordered_incidence_system
begin

definition dual_blocks_ordered :: "nat set list" ("ℬs*") where
"dual_blocks_ordered ≡ map (λ x . {y . y < length ℬs ∧ x ∈ ℬs ! y}) 𝒱s"

lemma dual_blocks_ordered_eq: "dual_blocks 𝒱 ℬs= mset (ℬs*)"
  by (auto simp add: distinct dual_blocks_def dual_blocks_ordered_def mset_set_set)

lemma dual_blocks_len: "length ℬs* = length 𝒱s"
  by (simp add: dual_blocks_ordered_def)

text ‹A dual system is an incidence system ›
sublocale dual_sys: finite_incidence_system "{0..<length ℬs}" "dual_blocks 𝒱 ℬs"
  using dual_blocks_wf by(unfold_locales) (auto)

lemma dual_is_ordered_inc_sys: "ordered_incidence_system [0..<length ℬs] ℬs*"
  using inc_sys_orderedI dual_blocks_ordered_eq
  by (metis atLeastLessThan_upt distinct_upt dual_sys.incidence_system_axioms)

interpretation ordered_dual_sys: ordered_incidence_system "[0..<length ℬs]" "ℬs*"
  using dual_is_ordered_inc_sys by simp 

subsection ‹Basic Dual Properties›
lemma ord_dual_blocks_b: "ordered_dual_sys.𝖻 = 𝗏"
  using dual_blocks_len by (simp add: points_list_length) 

lemma dual_blocks_b: "dual_sys.𝖻 = 𝗏"
  using points_list_length
  by (simp add: dual_blocks_len dual_blocks_ordered_eq) 

lemma dual_blocks_v: "dual_sys.𝗏 = 𝖻"
  by fastforce

lemma ord_dual_blocks_v: "ordered_dual_sys.𝗏 = 𝖻"
  by fastforce

lemma dual_point_block: "i < 𝗏 ⟹ ℬs* ! i = {y. y < length ℬs ∧ (𝒱s ! i) ∈ ℬs ! y}"
  by (simp add: dual_blocks_ordered_def points_list_length)

lemma dual_incidence_iff: "i < 𝗏 ⟹ j < 𝖻 ⟹ ℬs ! j = bl ⟹ 𝒱s ! i = x ⟹ (x ∈ bl ⟷ j ∈ ℬs* ! i)"
  using dual_point_block by (intro iffI)(simp_all)

lemma dual_incidence_iff2: "i < 𝗏 ⟹ j < 𝖻 ⟹ (𝒱s ! i ∈ ℬs ! j  ⟷ j ∈ ℬs* ! i)"
  using dual_incidence_iff by simp

lemma dual_blocks_point_exists: "bl ∈# dual_blocks 𝒱 ℬs ⟹ 
    ∃ x. x ∈ 𝒱 ∧ bl = {y . y < length ℬs ∧ x ∈ ℬs ! y}"
  by (auto simp add: dual_blocks_def)

lemma dual_blocks_ne_index_ne:  "j1 < length ℬs* ⟹ j2 < length ℬs* ⟹ ℬs* ! j1 ≠ ℬs* ! j2 ⟹ j1 ≠ j2"
  by auto

lemma dual_blocks_list_index_img: "image_mset (λx . ℬs* ! x) (mset_set {0..<length ℬs*}) = mset ℬs*"
  using lessThan_atLeast0 ordered_dual_sys.blocks_list_length ordered_dual_sys.blocks_mset_image 
  by presburger

lemma dual_blocks_elem_iff:
  assumes "j < 𝗏"
  shows "x ∈ (ℬs* ! j) ⟷ 𝒱s ! j ∈ ℬs ! x ∧ x < 𝖻"
proof (intro iffI conjI)
  show "x ∈ ℬs* ! j ⟹ 𝒱s ! j ∈ ℬs ! x"
    using assms ordered_incidence_system.dual_point_block ordered_incidence_system_axioms 
    by fastforce
  show "x ∈ ℬs* ! j ⟹ x < 𝖻"
    using assms dual_blocks_ordered_def dual_point_block by fastforce
  show "𝒱s ! j ∈ ℬs ! x ∧ x < 𝖻 ⟹ x ∈ ℬs* ! j"
    by (metis (full_types) assms blocks_list_length dual_incidence_iff)
qed

text ‹The incidence matrix of the dual of a design is just the transpose ›
lemma dual_incidence_mat_eq_trans: "ordered_dual_sys.N = N⇧T"
proof (intro eq_matI)
  show dimr: "dim_row ordered_dual_sys.N = dim_row N⇧T" using dual_blocks_v by (simp) 
  show dimc: "dim_col ordered_dual_sys.N = dim_col N⇧T" using ord_dual_blocks_b by (simp)
  show "⋀i j. i < dim_row N⇧T ⟹ j < dim_col N⇧T ⟹ ordered_dual_sys.N $$ (i, j) = N⇧T $$ (i, j)" 
  proof -
    fix i j assume ilt: "i < dim_row N⇧T" assume jlt: "j < dim_col N⇧T"
    then have ilt2: "i < length ℬs"using dimr
      using blocks_list_length ord_dual_blocks_v ilt ordered_dual_sys.dim_row_is_v by linarith
    then have ilt3: "i < 𝖻" by simp
    have jlt2: "j < 𝗏" using jlt
      using dim_row_is_v by fastforce 
    have "ordered_dual_sys.N $$ (i, j) =  (if ([0..<length ℬs] ! i) ∈ (ℬs* ! j) then 1 else 0)"
      using dimr dual_blocks_len ilt jlt inc_matrix_elems_one_zero
      by (metis  inc_mat_dim_row inc_matrix_point_in_block_iff index_transpose_mat(3) )
    then have "ordered_dual_sys.N $$ (i, j) = (if 𝒱s ! j ∈ ℬs ! i then 1 else 0)" 
      using ilt3 jlt2 dual_incidence_iff2 by simp 
    thus "ordered_dual_sys.N $$ (i, j) = N⇧T $$ (i, j)" 
      using ilt3 jlt2 dim_row_is_v dim_col_is_b N_trans_index_val by simp
  qed
qed

lemma dual_incidence_mat_eq_trans_rev: "(ordered_dual_sys.N)⇧T = N"
  using dual_incidence_mat_eq_trans by simp 

subsection ‹Incidence System Dual Properties›
text ‹Many common design properties have a dual in the dual design which enables extensive reasoning
Using incidence matrices and the transpose property these are easy to prove. We leave examples of 
counting proofs (commented out), to demonstrate how incidence matrices can significantly simplify 
reasoning ›

lemma dual_blocks_nempty:
  assumes "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x > 0)"
  assumes "bl ∈# dual_blocks 𝒱 ℬs"
  shows "bl ≠ {}"
proof -
  have "bl ∈# {# {y . y < length ℬs ∧ x ∈ ℬs ! y} . x ∈# (mset_set 𝒱)#}" 
    using assms dual_blocks_def by metis 
  then obtain x where "x ∈# (mset_set 𝒱)" and blval: "bl = {y . y < length ℬs ∧ x ∈ ℬs ! y}"
    by blast 
  then obtain bl' where "bl' ∈# ℬ" and xin: "x ∈ bl'" using assms(1)
    using point_in_block_rep_min_iff by auto 
  then obtain y where "y < length ℬs" and "ℬs ! y = bl'"
    using valid_blocks_index_cons by auto 
  then have "y ∈ bl"
    by (simp add: xin blval) 
  thus ?thesis by blast
qed

lemma dual_blocks_size_is_rep: "j < length ℬs* ⟹ card (ℬs* ! j) = ℬ rep (𝒱s ! j)"
  using dual_incidence_mat_eq_trans trans_mat_rep_block_size_sym(2)
  by (metis dual_blocks_len dual_is_ordered_inc_sys inc_mat_dim_row mat_rep_num_N_row 
      ordered_incidence_system.mat_block_size_N_col points_list_length size_mset) 

(* Old Counting proof 
proof -
  have 1: "card (ℬs* ! j) = card {y . y < length ℬs ∧ (𝒱s ! j) ∈ ℬs ! y}"
    using assms dual_blocks_len dual_point_block points_list_length by force
  also have 2: "... = card {y ∈ {0..<length ℬs} . (𝒱s ! j) ∈ ℬs ! y}" by simp
  also have "... = size (mset_set {y ∈ {0..<length ℬs} . (𝒱s ! j) ∈ ℬs ! y})" by simp
  also have "... = size {# y ∈# mset_set {0..< length ℬs} . (𝒱s ! j) ∈ ℬs ! y #}" 
    using filter_mset_mset_set by simp 
  finally have "card (ℬs* ! j) = size {# bl ∈# ℬ . (𝒱s ! j) ∈ bl #}"
    by (metis 1 2 filter_size_blocks_eq_card_indexes lessThan_atLeast0 size_mset) 
  thus ?thesis by (simp add: point_replication_number_def)
qed
*)

lemma dual_blocks_size_is_rep_obtain: 
  assumes "bl ∈# dual_blocks 𝒱 ℬs"
  obtains x where "x ∈ 𝒱" and "card bl = ℬ rep x"
proof -
  obtain j where jlt1: "j < length ℬs*" and bleq: "ℬs* ! j = bl"
    by (metis assms dual_blocks_ordered_eq in_mset_conv_nth) 
  then have jlt: "j < 𝗏"
    by (simp add: dual_blocks_len points_list_length) 
  let ?x = "𝒱s ! j"
  have xin: "?x ∈ 𝒱" using jlt
    by (simp add: valid_points_index) 
  have "card bl = ℬ rep ?x" using dual_blocks_size_is_rep jlt1 bleq by auto
  thus ?thesis using xin that by auto 
qed

lemma dual_blocks_rep_is_size:
  assumes "i < length ℬs"
  shows "(mset ℬs*) rep i = card (ℬs ! i)"
proof -
  have "[0..<length ℬs] ! i = i" using assms by simp
  then have "(mset ℬs*) rep i = mat_rep_num ordered_dual_sys.N i" 
    using ordered_dual_sys.mat_rep_num_N_row assms length_upt minus_nat.diff_0 
      ordered_dual_sys.points_list_length by presburger 
  also have "... = mat_block_size (ordered_dual_sys.N)⇧T i" using dual_incidence_mat_eq_trans 
    trans_mat_rep_block_size_sym(2) by (metis assms inc_mat_dim_col index_transpose_mat(2))
  finally show ?thesis using dual_incidence_mat_eq_trans_rev
    by (metis assms blocks_list_length mat_block_size_N_col)
qed

(* Counting Proof
proof -
  have "(mset ℬs* ) rep i = size {# bl ∈# (mset ℬs* ) . i ∈ bl #}" 
    by (simp add: point_replication_number_def)
  also have 1: "... = size {# bl ∈# {# {y . y < length ℬs ∧ x ∈ ℬs ! y} . x ∈# (mset_set 𝒱)#} . i ∈ bl #}" 
    using dual_blocks_ordered_eq dual_blocks_def by metis 
  also have "... = size (filter_mset (λ bl . i ∈ bl) 
      (image_mset (λ x . {y . y < length ℬs ∧ x ∈ ℬs ! y}) (mset_set 𝒱)))" by simp
  finally have "(mset ℬs* ) rep i = size (image_mset (λ x . {y . y < length ℬs ∧ x ∈ ℬs ! y}) 
      (filter_mset (λ bl . i ∈ {y . y < length ℬs ∧ bl ∈ ℬs ! y}) (mset_set 𝒱)))"
    using filter_mset_image_mset by (metis 1 ordered_dual_sys.point_rep_number_alt_def) 
  then have "(mset ℬs* ) rep i = size (filter_mset (λ bl . i ∈ {y . y < length ℬs ∧ bl ∈ ℬs ! y}) 
      (mset_set 𝒱))"
    by fastforce
  then have "(mset ℬs* ) rep i = size (filter_mset (λ bl . bl ∈ ℬs ! i) (mset_set 𝒱))" 
    using assms by simp
  then have "(mset ℬs* ) rep i =  card {x ∈ 𝒱 . x ∈ (ℬs ! i)}" by simp
  thus ?thesis using assms block_size_alt by auto
qed
*)

lemma dual_blocks_inter_index: 
  assumes "j1 < length ℬs*" "j2 < length ℬs*"
  shows "(ℬs* ! j1) |∩| (ℬs* ! j2) = points_index ℬ {𝒱s ! j1, 𝒱s ! j2}"
proof -
  have assms2: "j1 < 𝗏" "j2 < 𝗏" using assms
    by (simp_all add: dual_blocks_len points_list_length) 
  have "(ℬs* ! j1) |∩| (ℬs* ! j2) = mat_inter_num (ordered_dual_sys.N) j1 j2"
    by (simp add: assms(1) assms(2) ordered_dual_sys.mat_inter_num_conv)
  also have "... = mat_point_index N {j1, j2}" using dual_incidence_mat_eq_trans_rev trans_mat_point_index_inter_sym(2)
    by (metis assms inc_mat_dim_col)
  finally show ?thesis using assms2 incidence_mat_two_index
    by presburger
qed
(* Counting Proof 
  have fin: "finite {0..<length ℬs}"
    by auto 
  have j1lt: "j1 < 𝗏" using assms
    using dual_blocks_len points_list_length by auto 
  have j2lt: "j2 < 𝗏" using assms dual_blocks_len points_list_length by auto
  have iff: "⋀ x. (x ∈(ℬs* ! j1) ∧ x ∈ (ℬs* ! j2)) ⟷ (𝒱s ! j1 ∈ ℬs ! x ∧ x < 𝖻 ∧ 𝒱s ! j2 ∈ ℬs ! x)" 
    by (auto simp add: dual_blocks_elem_iff j1lt j2lt)
  have pi: "points_index ℬ {𝒱s ! j1, 𝒱s ! j2} = size {# bl ∈# ℬ . 𝒱s !j1 ∈ bl ∧ 𝒱s ! j2 ∈ bl#}" 
    by (auto simp add: points_index_def)
  have "(ℬs* ! j1) |∩| (ℬs* ! j2) = card ({x . x <length ℬs ∧ x ∈ (ℬs* ! j1) ∧ x ∈ (ℬs* ! j2)})"
    apply (auto simp add: intersection_number_def)
    by (smt (verit) Collect_cong Int_Collect blocks_list_length dual_blocks_elem_iff inf.idem inf_set_def j2lt mem_Collect_eq)
  then have "(ℬs* ! j1) |∩| (ℬs* ! j2) = card ({x . x <length ℬs ∧ 𝒱s ! j1 ∈ ℬs ! x ∧ 𝒱s ! j2 ∈ ℬs ! x})" using iff
    size_mset by (smt (verit, best) Collect_cong) 
  then have "(ℬs* ! j1) |∩| (ℬs* ! j2) = size (mset_set {x ∈ {0..<length ℬs}. 𝒱s ! j1 ∈ ℬs ! x ∧ 𝒱s ! j2 ∈ ℬs ! x})" by simp
  then have "(ℬs* ! j1) |∩| (ℬs* ! j2) = size ({#x ∈# mset_set {0..<length ℬs}. 𝒱s ! j1 ∈ ℬs ! x ∧ 𝒱s ! j2 ∈ ℬs ! x#})" using fin by simp
  then have "(ℬs* ! j1) |∩| (ℬs* ! j2) = size (filter_mset (λ x . 𝒱s ! j1 ∈ ℬs ! x ∧ 𝒱s ! j2 ∈ ℬs ! x) (mset_set {0..<length ℬs}))" by simp
  then have "(ℬs* ! j1) |∩| (ℬs* ! j2) = size (image_mset (λ i. ℬs ! i) (filter_mset (λ x . 𝒱s ! j1 ∈ ℬs ! x ∧ 𝒱s ! j2 ∈ ℬs ! x) (mset_set {0..<length ℬs})))"
    by simp
  then have "(ℬs* ! j1) |∩| (ℬs* ! j2) = size (filter_mset (λ x . 𝒱s ! j1 ∈ x ∧ 𝒱s ! j2 ∈ x) (image_mset (λ i. ℬs ! i) (mset_set {0..<length ℬs})))"
    by (simp add: filter_mset_image_mset)
  then have "(ℬs* ! j1) |∩| (ℬs* ! j2) = size {# bl ∈# ℬ . 𝒱s !j1 ∈ bl ∧ 𝒱s ! j2 ∈ bl#}"
    by (metis blocks_list_length blocks_mset_image lessThan_atLeast0) 
  thus ?thesis using pi by simp
qed
*)

lemma dual_blocks_points_index_inter: 
  assumes "i1 < 𝖻" "i2 < 𝖻"
  shows "(mset ℬs*) index {i1, i2} = (ℬs ! i1) |∩| (ℬs ! i2)"
proof -
  have "(mset ℬs*) index {i1, i2} = mat_point_index (ordered_dual_sys.N) {i1, i2}"
    using assms(1) assms(2) blocks_list_length ord_dual_blocks_v ordered_dual_sys.dim_row_is_v 
      ordered_dual_sys.incidence_mat_two_index ordered_dual_sys.mat_ord_inc_sys_point by presburger 
  also have "... = mat_inter_num N i1 i2" using dual_incidence_mat_eq_trans trans_mat_point_index_inter_sym(1)
    by (metis assms(1) assms(2) dual_incidence_mat_eq_trans_rev ord_dual_blocks_v ordered_dual_sys.dim_row_is_v) 
  finally show ?thesis using mat_inter_num_conv
    using assms(1) assms(2) by auto 
qed

(* Counting Proof 
proof - 
  have "⋀ j . j ∈# mset_set {0..<length ℬs*} ⟹ j < 𝗏"
    by (metis atLeastLessThan_iff atLeastLessThan_upt dual_blocks_len mset_upt points_list_length set_mset_mset) 
  then have iff: "⋀ j i. j ∈# mset_set {0..<length ℬs*} ⟹ i < 𝖻 ⟹ i ∈ (ℬs* ! j) ⟷ (𝒱s ! j) ∈ (ℬs ! i)" 
    using assms dual_incidence_iff2 by simp 
  then have iff2: "⋀ j . j ∈# mset_set {0..<length ℬs*} ⟹ i1 ∈ (ℬs* ! j) ∧ i2 ∈ (ℬs* ! j) ⟷ (𝒱s ! j) ∈ (ℬs ! i1) ∧ (𝒱s ! j) ∈ (ℬs ! i2)"
    using assms by auto
  have ss2: "(ℬs ! i2) ⊆ 𝒱" using wellformed assms by auto
  then have ss: "{x . x ∈ (ℬs ! i1) ∧ x ∈ (ℬs ! i2)} ⊆ 𝒱"
    by auto 
  then have inter:  "(ℬs ! i1) |∩| (ℬs ! i2) = card {x ∈ 𝒱. x ∈ (ℬs ! i1) ∧ x ∈ (ℬs ! i2)}"
    using intersection_number_def by (metis Collect_conj_eq Collect_mem_eq Int_absorb1)
  have inj: "inj_on (λ j. 𝒱s ! j) {j ∈ {0..<length 𝒱s} . (𝒱s ! j) ∈ (ℬs ! i1) ∧ (𝒱s ! j) ∈ (ℬs ! i2)}"
    by (simp add: inj_on_nth distinct) 
  have init: "(mset ℬs* ) index {i1, i2} = size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#}"
    by (simp add: points_index_def)
  then have "size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#} = size {#j ∈# mset_set {0..<length ℬs*} . i1 ∈ (ℬs* ! j) ∧ i2 ∈ (ℬs* ! j)#}"
  proof - 
    have "size {#j ∈# mset_set {0..<length ℬs*} . i1 ∈ (ℬs* ! j) ∧ i2 ∈ (ℬs* ! j)#} 
      = size (filter_mset (λ j. i1 ∈ (ℬs* ! j) ∧ i2 ∈ (ℬs* ! j)) (mset_set {0..<length ℬs*})) " by simp
    also have s1: "... = size (image_mset (λx . ℬs* ! x) (filter_mset (λ j. i1 ∈ (ℬs* ! j) ∧ i2 ∈ (ℬs* ! j)) (mset_set {0..<length ℬs*})))" by fastforce
    also have s2: "... = size (filter_mset (λ j. i1 ∈ j ∧ i2 ∈ j) (image_mset (λx . ℬs* ! x) (mset_set {0..<length ℬs*})))"
      by (simp add: filter_mset_image_mset) 
    finally have "size {#j ∈# mset_set {0..<length ℬs*} . i1 ∈ (ℬs* ! j) ∧ i2 ∈ (ℬs* ! j)#} = size (filter_mset (λ j. i1 ∈ j ∧ i2 ∈ j) (mset ℬs* ))"
      using dual_blocks_list_index_img s2 s1 by presburger 
    thus ?thesis by simp
  qed
  then have "size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#} = size {#j ∈# mset_set {0..<length ℬs*} . (𝒱s ! j) ∈ (ℬs ! i1) ∧ (𝒱s ! j) ∈ (ℬs ! i2)#}" using iff2
    by (smt (verit, ccfv_SIG) filter_mset_cong) 
  then have "size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#} = 
    card ({j ∈ {0..<length ℬs*} . (𝒱s ! j) ∈ (ℬs ! i1) ∧ (𝒱s ! j) ∈ (ℬs ! i2)})" by simp
  then have "size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#} = 
    card ({j ∈ {0..<length 𝒱s} . (𝒱s ! j) ∈ (ℬs ! i1) ∧ (𝒱s ! j) ∈ (ℬs ! i2)})" using dual_blocks_len by presburger 
  then have "size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#} = 
    card (image (λ j. 𝒱s ! j) {j ∈ {0..<length 𝒱s} . (𝒱s ! j) ∈ (ℬs ! i1) ∧ (𝒱s ! j) ∈ (ℬs ! i2)})"  
    using inj card_image[of "(λ j. 𝒱s ! j)" "{j ∈ {0..<length 𝒱s} . (𝒱s ! j) ∈ (ℬs ! i1) ∧ (𝒱s ! j) ∈ (ℬs ! i2)}"] by simp
  then have "size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#} = 
    card {j ∈ image (λ j. 𝒱s ! j) {0..<length 𝒱s}. j ∈ (ℬs ! i1) ∧ j ∈ (ℬs ! i2)}" 
    using Compr_image_eq[of "(λ j. 𝒱s ! j)" "{0..<length 𝒱s}" "(λ j . j ∈ (ℬs ! i1) ∧ j ∈ (ℬs ! i2))"] by simp
  then have "size {#bl ∈# (mset ℬs* ) . i1 ∈ bl ∧ i2 ∈ bl#} = 
    card {j ∈ 𝒱. j ∈ (ℬs ! i1) ∧ j ∈ (ℬs ! i2)}"
    using lessThan_atLeast0 points_list_length points_set_index_img by presburger 
  thus ?thesis using init inter by simp
qed*)
end 

subsection ‹Dual Properties for Design sub types ›
context ordered_design
begin

lemma dual_is_design: 
  assumes "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x > 0)" ― ‹ Required to ensure no blocks are empty ›
  shows "design {0..<length ℬs} (dual_blocks 𝒱 ℬs)"
  using dual_blocks_nempty assms by (unfold_locales) (simp) 
end

context ordered_proper_design
begin

lemma dual_sys_b_non_zero: "dual_sys.𝖻 ≠ 0"
  using v_non_zero dual_blocks_b by auto

lemma dual_is_proper_design: 
  assumes "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x > 0)"  ― ‹ Required to ensure no blocks are empty ›
  shows "proper_design {0..<length ℬs} (dual_blocks 𝒱 ℬs)"
  using dual_blocks_nempty dual_sys_b_non_zero assms by (unfold_locales) (simp_all)

end

context ordered_block_design 
begin

lemma dual_blocks_const_rep: "i ∈ {0..<length ℬs} ⟹ (mset ℬs*) rep i = 𝗄"
  using dual_blocks_rep_is_size uniform by (metis atLeastLessThan_iff nth_mem_mset) 

lemma dual_blocks_constant_rep_design:
  assumes "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x > 0)"
  shows "constant_rep_design {0..<length ℬs} (dual_blocks 𝒱 ℬs) 𝗄"
proof -
  interpret des: proper_design "{0..<length ℬs}" "(dual_blocks 𝒱 ℬs)"
    using dual_is_proper_design assms by simp
  show ?thesis using dual_blocks_const_rep dual_blocks_ordered_eq by (unfold_locales) (simp)
qed


end

context ordered_constant_rep
begin

lemma dual_blocks_const_size:  "j < length ℬs* ⟹ card (ℬs* ! j) = 𝗋"
  using dual_blocks_rep_is_size dual_blocks_len dual_blocks_size_is_rep by fastforce 

lemma dual_is_block_design: "block_design {0..<length ℬs} (dual_blocks 𝒱 ℬs) 𝗋"
proof -
  have "𝗋 > 0" by (simp add: r_gzero)
  then have "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x > 0)" using rep_number by simp
  then interpret pdes: proper_design "{0..<length ℬs}" "(dual_blocks 𝒱 ℬs)" 
    using dual_is_proper_design by simp
  have "⋀ bl. bl ∈# dual_blocks 𝒱 ℬs ⟹ card bl = 𝗋" 
    using dual_blocks_const_size 
    by (metis dual_blocks_ordered_eq in_set_conv_nth set_mset_mset)
  thus ?thesis by (unfold_locales) (simp)
qed

end

context ordered_pairwise_balance 
begin

lemma dual_blocks_const_intersect: 
  assumes "j1 < length ℬs*" "j2 < length ℬs*"
  assumes "j1 ≠ j2"
  shows "(ℬs* ! j1) |∩| (ℬs* ! j2) = Λ"
proof -
  have "𝒱s ! j1 ≠ 𝒱s ! j2" using assms(3)
    using assms(1) assms(2) distinct dual_blocks_len nth_eq_iff_index_eq by auto 
  then have c: "card {𝒱s ! j1, 𝒱s ! j2} = 2"
    using card_2_iff by blast 
  have ss: "{𝒱s ! j1, 𝒱s ! j2} ⊆ 𝒱" using assms points_list_length
    using dual_blocks_len by auto 
  have "(ℬs* ! j1) |∩| (ℬs* ! j2) = points_index ℬ {𝒱s ! j1, 𝒱s ! j2}"
    using dual_blocks_inter_index assms by simp
  thus ?thesis using ss c balanced
    by blast 
qed

lemma dual_is_const_intersect_des: 
  assumes "Λ > 0"
  shows "const_intersect_design {0..<(length ℬs)} (dual_blocks 𝒱 ℬs) Λ"
proof -
  have "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x ≥ Λ)" using const_index_lt_rep by simp
  then have "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x > 0)" using assms
    by (metis gr_zeroI le_zero_eq) 
  then interpret pd: proper_design "{0..<(length ℬs)}" "(dual_blocks 𝒱 ℬs)" 
    using dual_is_proper_design by (simp) 
  show ?thesis proof (unfold_locales)
    fix b1 b2
    assume b1in: "b1 ∈# dual_blocks 𝒱 ℬs"
    assume b2in:  "b2 ∈# remove1_mset b1 (dual_blocks 𝒱 ℬs)"
    obtain j1 where b1eq: "b1 = ℬs* ! j1" and j1lt: "j1 < length ℬs*" using b1in
      by (metis dual_blocks_ordered_eq in_set_conv_nth set_mset_mset) 
    obtain j2 where b2eq: "b2 = ℬs* ! j2" and j2lt: "j2 < length ℬs*" and "j1 ≠ j2" 
      using b2in index_remove1_mset_ne
      by (metis (mono_tags) b1eq dual_blocks_ordered_eq j1lt nth_mem set_mset_mset) 
    then show "b1 |∩| b2 = Λ" 
      using dual_blocks_const_intersect b1eq b2eq j1lt j2lt by simp 
  qed
qed


lemma dual_is_simp_const_inter_des: 
  assumes "Λ > 0"
  assumes "⋀ bl. bl ∈# ℬ ⟹ incomplete_block bl"  
  shows "simple_const_intersect_design {0..<(length ℬs)} (dual_blocks 𝒱 ℬs) Λ"
proof -
  interpret d: const_intersect_design "{0..<(length ℬs)}" "(dual_blocks 𝒱 ℬs)"  "Λ"
    using assms dual_is_const_intersect_des by simp
  ― ‹ Show that m < block size for all blocks ›
  have "⋀ x. x ∈ 𝒱 ⟹ Λ < ℬ rep x" using assms incomplete_index_strict_lt_rep
    by blast 
  then have "⋀ bl. bl ∈# (dual_blocks 𝒱 ℬs) ⟹ Λ < card bl"
    by (metis dual_blocks_size_is_rep_obtain) 
  then interpret s: simple_design "{0..<(length ℬs)}" "(dual_blocks 𝒱 ℬs)" 
    using d.simple_const_inter_block_size by simp
  show ?thesis by (unfold_locales)
qed
end

context ordered_const_intersect_design
begin

lemma dual_is_balanced: 
  assumes "ps ⊆ {0..<length ℬs}"
  assumes "card ps = 2"
  shows "(dual_blocks 𝒱 ℬs) index ps = 𝗆"
proof -
  obtain i1 i2 where psin: "ps = {i1, i2}" and neq: "i1 ≠ i2" using assms
    by (meson card_2_iff) 
  then have lt: "i1 < 𝖻" using assms 
    by (metis atLeastLessThan_iff blocks_list_length insert_subset) 
  have lt2: "i2 < 𝖻" using assms psin
    by (metis atLeastLessThan_iff blocks_list_length insert_subset) 
  then have inter: "(dual_blocks 𝒱 ℬs) index ps = (ℬs ! i1) |∩| (ℬs ! i2)" using dual_blocks_points_index_inter neq lt
    using dual_blocks_ordered_eq psin by presburger
  have inb1: "(ℬs ! i1) ∈# ℬ"
    using lt by auto 
  have inb2: "(ℬs ! i2) ∈# (ℬ - {#(ℬs ! i1)#})" using lt2 neq blocks_index_ne_belong
    by (metis blocks_list_length lt) 
  thus ?thesis using const_intersect inb1 inb2 inter by blast 
qed

lemma dual_is_pbd: 
  assumes "(⋀ x . x ∈ 𝒱 ⟹ ℬ rep x > 0)"
  assumes "𝖻 ≥ 2"
  shows "pairwise_balance {0..<(length ℬs)} (dual_blocks 𝒱 ℬs) 𝗆"
proof -
  interpret pd: proper_design "{0..<(length ℬs)}" "(dual_blocks 𝒱 ℬs)" 
    using dual_is_proper_design
    by (simp add: assms) 
  show ?thesis proof (unfold_locales)
    show "(1 ::nat) ≤ 2" by simp
    then show "2 ≤ dual_sys.𝗏" using  assms(2)
      by fastforce 
    show "⋀ps. ps ⊆ {0..<length ℬs} ⟹ card ps = 2 ⟹ dual_blocks 𝒱 ℬs index ps = 𝗆"
      using dual_is_balanced by simp
  qed
qed

end

context ordered_sym_bibd
begin

lemma dual_is_balanced: 
  assumes "ps ⊆ {0..<length ℬs}"
  assumes "card ps = 2"
  shows "(dual_blocks 𝒱 ℬs) index ps = Λ"
proof -
  obtain i1 i2 where psin: "ps = {i1, i2}" and neq: "i1 ≠ i2" 
    using assms by (meson card_2_iff) 
  then have lt: "i1 < 𝖻" using assms 
    by (metis atLeastLessThan_iff blocks_list_length insert_subset) 
  have lt2: "i2 < 𝖻" using assms psin
    by (metis atLeastLessThan_iff blocks_list_length insert_subset) 
  then have inter: "(dual_blocks 𝒱 ℬs) index ps = (ℬs ! i1) |∩| (ℬs ! i2)" 
    using dual_blocks_points_index_inter neq lt dual_blocks_ordered_eq psin by presburger
  have inb1: "(ℬs ! i1) ∈# ℬ"
    using lt by auto 
  have inb2: "(ℬs ! i2) ∈# (ℬ - {#(ℬs ! i1)#})" using lt2 neq blocks_index_simp_unique
    by (metis blocks_list_length in_remove1_mset_neq lt valid_blocks_index) 
  thus ?thesis using sym_block_intersections_index inb1 inter by blast
qed

lemma dual_bibd: "bibd {0..<(length ℬs)} (dual_blocks 𝒱 ℬs) 𝗋 Λ"
proof -
  interpret block: block_design "{0..<(length ℬs)}" "(dual_blocks 𝒱 ℬs)" 𝗋 
    using dual_is_block_design by simp
  show ?thesis proof (unfold_locales)
    show "𝗋 < dual_sys.𝗏"
      using dual_blocks_v incomplete symmetric_condition_1 symmetric_condition_2 by presburger 
    show "(1 ::nat) ≤ 2" by simp
    have "𝗏 ≥ 2"
      by (simp add: t_lt_order) 
    then have "𝖻 ≥ 2" using local.symmetric by auto 
    then show "2 ≤ dual_sys.𝗏" by simp
    show "⋀ps. ps ⊆ {0..<length ℬs} ⟹ card ps = 2 ⟹ dual_blocks 𝒱 ℬs index ps = Λ"
      using dual_is_balanced by simp
    show "2 ≤ 𝗋" using r_ge_two by blast 
  qed
qed

text ‹The dual of a BIBD must by symmetric ›

lemma dual_bibd_symmetric: "symmetric_bibd {0..<(length ℬs)} (dual_blocks 𝒱 ℬs) 𝗋 Λ"
proof -
  interpret bibd: bibd "{0..<(length ℬs)}" "(dual_blocks 𝒱 ℬs)" 𝗋 Λ
    using dual_bibd by simp
  show ?thesis using dual_blocks_b local.symmetric by (unfold_locales) (simp)
qed

end

subsection ‹Generalise Dual Concept ›
text ‹The above formalisation relies on one translation of a dual design. However, any design 
with an ordering of points and blocks such that the matrix is the transpose of the original is 
a dual. The definition below encapsulates this concept. Additionally, we prove an isomorphism
exists between the generated dual from @{term "dual_blocks"} and any design satisfying the is dual
definition›

context ordered_incidence_system 
begin

definition is_dual:: "'b list ⇒ 'b set list ⇒ bool" where
"is_dual Vs' Bs' ≡ ordered_incidence_system Vs' Bs' ∧ (inc_mat_of Vs' Bs' = N⇧T)"

lemma is_dualI: 
  assumes "ordered_incidence_system Vs' Bs'"
  assumes "(inc_mat_of Vs' Bs' = N⇧T)"
  shows "is_dual Vs' Bs'"
  by (auto simp add: is_dual_def assms)

lemma is_dualD1: 
  assumes "is_dual Vs' Bs'"
  shows  "(inc_mat_of Vs' Bs' = N⇧T)"
  using is_dual_def assms
  by auto 

lemma is_dualD2: 
  assumes "is_dual Vs' Bs'"
  shows  "ordered_incidence_system Vs' Bs'"
  using is_dual_def assms
  by auto 

lemma generated_is_dual: "is_dual [0..<(length ℬs)] ℬs*"
proof -
  interpret osys: ordered_incidence_system "[0..<(length ℬs)]" "ℬs*" using dual_is_ordered_inc_sys by simp 
  show ?thesis using is_dual_def
    by (simp add: is_dual_def dual_incidence_mat_eq_trans osys.ordered_incidence_system_axioms) 
qed

lemma is_dual_isomorphism_generated: 
  assumes "is_dual Vs' Bs'"
  shows "∃ π. incidence_system_isomorphism (set Vs') (mset Bs') ({0..<(length ℬs)}) (dual_blocks 𝒱 ℬs) π"
proof -
  interpret os2: ordered_incidence_system "([0..<(length ℬs)])" "(ℬs*)"
    by (simp add: dual_is_ordered_inc_sys) 
  interpret os1: ordered_incidence_system Vs' Bs' using assms
    by (simp add: is_dualD2) 
  interpret tos: two_ordered_sys Vs' Bs' "([0..<(length ℬs)])" "(ℬs*)" 
     using assms  ordered_incidence_system_axioms two_ordered_sys.intro
     by (simp add: is_dualD2 two_ordered_sys.intro dual_is_ordered_inc_sys)
  have os2V: "os2.𝒱 = {0..<(length ℬs)}"
    by auto 
  have os2B: "os2.ℬ = dual_blocks 𝒱 ℬs"
    by (simp add: dual_blocks_ordered_eq) 
  have "os1.N = inc_mat_of Vs' Bs'" by simp
  then have "os2.N = os1.N"
    using assms is_dualD1 dual_incidence_mat_eq_trans by fastforce 
  thus ?thesis using tos.equal_inc_mat_isomorphism_ex os2V os2B by auto
qed

interpretation ordered_dual_sys: ordered_incidence_system "[0..<length ℬs]" "ℬs*"
  using dual_is_ordered_inc_sys by simp 

text ‹Original system is dual of the dual ›
lemma is_dual_rev: "ordered_dual_sys.is_dual 𝒱s ℬs"
  by (simp add: dual_incidence_mat_eq_trans_rev ordered_dual_sys.is_dualI ordered_incidence_system_axioms)

end

end