Theory Binary_operations

theory Binary_operations
 imports Bij_betw_simplicial_complex_bool_func
begin

section‹Binary operations over Boolean functions and simplicial complexes›

text‹In this theory some results on binary operations over Boolean functions and
  their relationship to operations over the induced simplicial complexes are
  presented. We follow the presentation by Chastain and Scoville~\<^cite>‹‹Sect. 1.1› in "CHSC"›.›

definition bool_fun_or :: "nat ⇒ (bool vec ⇒ bool) ⇒ (bool vec ⇒ bool) ⇒ (bool vec ⇒ bool)"
  where "(bool_fun_or n f g) ≡ (λx. f x ∨ g x)"

definition bool_fun_and :: "nat ⇒ (bool vec ⇒ bool) ⇒ (bool vec ⇒ bool) ⇒ (bool vec ⇒ bool)"
  where "(bool_fun_and n f g) ≡ (λx. f x ∧ g x)"

lemma eq_union_or:
  "simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
  = simplicial_complex_induced_by_monotone_boolean_function n f
    ∪ simplicial_complex_induced_by_monotone_boolean_function n g"
  (is "?sc n (?bf_or n f g) = ?sc n f ∪ ?sc n g")
proof
  show "?sc n f ∪ ?sc n g ⊆ ?sc n (?bf_or n f g)"
  proof
    fix σ :: "nat set"
    assume "σ ∈ (?sc n f ∪ ?sc n g)"
    hence sigma: "σ ∈ ?sc n f ∨ σ ∈ ?sc n g" by auto
    have "f (simplicial_complex.bool_vec_from_simplice n σ)
           ∨ g (simplicial_complex.bool_vec_from_simplice n σ)"
    proof (cases "σ ∈ ?sc n f")
      case True
      from simplicial_complex.simplicial_complex_implies_true [OF True]
      show "f (simplicial_complex.bool_vec_from_simplice n σ)
           ∨ g (simplicial_complex.bool_vec_from_simplice n σ)" by fast
    next
      case False
      hence sigmain: "σ ∈ ?sc n g" using sigma by fast
      from simplicial_complex.simplicial_complex_implies_true [OF sigmain]
      show "f (simplicial_complex.bool_vec_from_simplice n σ)
           ∨ g (simplicial_complex.bool_vec_from_simplice n σ)" by fast
    qed
    thus "σ ∈ ?sc n (?bf_or n f g)"
      using simplicial_complex_induced_by_monotone_boolean_function_def
      using bool_fun_or_def sigma by auto
  qed
next
  show "?sc n (?bf_or n f g) ⊆ ?sc n f ∪ ?sc n g"
  proof
    fix σ::"nat set"
    assume sigma: "σ ∈ ?sc n (?bf_or n f g)"
    hence "bool_fun_or n f g (simplicial_complex.bool_vec_from_simplice n σ)"
      unfolding simplicial_complex.bool_vec_from_simplice_def
      unfolding simplicial_complex_induced_by_monotone_boolean_function_def
      unfolding ceros_of_boolean_input_def
      by auto (smt (verit) dim_vec eq_vecI index_vec)+
    hence "(f (simplicial_complex.bool_vec_from_simplice n σ))
            ∨ (g (simplicial_complex.bool_vec_from_simplice n σ))"
      unfolding bool_fun_or_def
      by auto
    hence "σ ∈ ?sc n f ∨ σ ∈ ?sc n g"
      by (smt (z3) sigma bool_fun_or_def mem_Collect_eq
            simplicial_complex_induced_by_monotone_boolean_function_def)
    thus "σ ∈ simplicial_complex_induced_by_monotone_boolean_function n f
          ∪ simplicial_complex_induced_by_monotone_boolean_function n g"
      by auto
  qed
qed

lemma eq_inter_and:
  "simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
  = simplicial_complex_induced_by_monotone_boolean_function n f
    ∩ simplicial_complex_induced_by_monotone_boolean_function n g"
  (is "?sc n (?bf_and n f g) = ?sc n f ∩ ?sc n g")
proof
  show "?sc n f ∩ ?sc n g ⊆ ?sc n (?bf_and n f g)"
  proof
    fix σ :: "nat set"
    assume "σ ∈ (?sc n f ∩ ?sc n g)"
    hence sigma: "σ ∈ ?sc n f ∧ σ ∈ ?sc n g" by auto
    have "f (simplicial_complex.bool_vec_from_simplice n σ)
           ∧ g (simplicial_complex.bool_vec_from_simplice n σ)"
    proof -
      from sigma have sigmaf: "σ ∈ ?sc n f" and sigmag: "σ ∈ ?sc n g"
        by auto
      have "f (simplicial_complex.bool_vec_from_simplice n σ)"
        using simplicial_complex.simplicial_complex_implies_true [OF sigmaf] .
      moreover have "g (simplicial_complex.bool_vec_from_simplice n σ)"
        using simplicial_complex.simplicial_complex_implies_true [OF sigmag] .
      ultimately show ?thesis by fast
    qed
    thus "σ ∈ ?sc n (?bf_and n f g)"
      unfolding simplicial_complex_induced_by_monotone_boolean_function_def
      unfolding bool_fun_and_def
      using sigma apply auto
      by (smt (z3) Collect_cong ceros_of_boolean_input_def dim_vec index_vec mem_Collect_eq
          simplicial_complex.bool_vec_from_simplice_def
          simplicial_complex_induced_by_monotone_boolean_function_def)
  qed
next
  show "?sc n (?bf_and n f g) ⊆ ?sc n f ∩ ?sc n g"
  proof
    fix σ :: "nat set"
    assume sigma: "σ ∈ ?sc n (?bf_and n f g)"
    hence "bool_fun_and n f g (simplicial_complex.bool_vec_from_simplice n σ)"
      unfolding simplicial_complex.bool_vec_from_simplice_def
      unfolding simplicial_complex_induced_by_monotone_boolean_function_def
      unfolding ceros_of_boolean_input_def
      by auto (smt (verit) dim_vec eq_vecI index_vec)+
    hence "(f (simplicial_complex.bool_vec_from_simplice n σ))
          ∧ (g (simplicial_complex.bool_vec_from_simplice n σ))"
      unfolding bool_fun_and_def
      by auto
    hence "σ ∈ ?sc n f ∧ σ ∈ ?sc n g"
      using bool_fun_and_def sigma simplicial_complex_induced_by_monotone_boolean_function_def by auto
    thus "σ ∈ simplicial_complex_induced_by_monotone_boolean_function n f
          ∩ simplicial_complex_induced_by_monotone_boolean_function n g"
      by auto
  qed
qed

definition bool_fun_ast :: "(nat × nat) ⇒ (bool vec ⇒ bool) × (bool vec ⇒ bool)
    ⇒ (bool vec × bool vec ⇒ bool)"
  where "(bool_fun_ast n f) ≡ (λ (x,y). (fst f x) ∧ (snd f y))"

definition
  simplicial_complex_induced_by_monotone_boolean_function_ast
    :: "(nat × nat) ⇒ ((bool vec × bool vec ⇒ bool)) ⇒ (nat set * nat set) set"
  where "simplicial_complex_induced_by_monotone_boolean_function_ast n f =
        {z. ∃x y. dim_vec x = fst n ∧ dim_vec y = snd n ∧ f (x, y)
          ∧ ((ceros_of_boolean_input x), (ceros_of_boolean_input y)) = z}"

lemma fst_es_simplice:
  "a ∈ simplicial_complex_induced_by_monotone_boolean_function_ast n f
    ⟹ (∃x y. f (x, y) ∧ (ceros_of_boolean_input x) = fst(a))"
  by (smt (verit) fst_conv mem_Collect_eq
        simplicial_complex_induced_by_monotone_boolean_function_ast_def)

lemma snd_es_simplice:
  "a ∈ simplicial_complex_induced_by_monotone_boolean_function_ast n f
    ⟹ (∃x y. f (x, y) ∧ (ceros_of_boolean_input y) = snd(a))"
  by (smt (verit) snd_conv mem_Collect_eq
      simplicial_complex_induced_by_monotone_boolean_function_ast_def)

definition set_ast :: "(nat set) set ⇒ (nat set) set ⇒ ((nat set*nat set) set)"
  where "set_ast A B ≡ {c. ∃a∈A. ∃b∈B. c = (a,b)}"

definition set_fst :: "(nat*nat) set ⇒ nat set"
  where "set_fst AB = {a. ∃ab∈AB. a = fst ab}"

lemma set_fst_simp [simp]:
  assumes "y ≠ {}"
  shows "set_fst (x × y) = x"
proof
  show "set_fst (x × y) ⊆ x"
    by (smt (verit) SigmaE mem_Collect_eq prod.sel(1) set_fst_def subsetI)
  show "x ⊆ set_fst (x × y)"
  proof
    fix a::"nat"
    assume "a ∈ x"
    then obtain b where "b ∈ y" and "(a,b) ∈ (x×y)"
      using assms by blast
    then show "a ∈ set_fst (x × y)"
      using set_fst_def by fastforce
  qed
qed

definition set_snd :: "(nat*nat) set ⇒ nat set"
  where "set_snd AB = {b. ∃ab∈AB. b = snd(ab)}"

lemma
  simplicial_complex_ast_implies_fst_true:
  assumes "γ ∈ simplicial_complex_induced_by_monotone_boolean_function_ast nn
     (bool_fun_ast nn f)"
  shows "fst f (simplicial_complex.bool_vec_from_simplice (fst nn) (fst γ))"
  using assms
  unfolding simplicial_complex.bool_vec_from_simplice_def
  unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
  unfolding bool_fun_ast_def
  unfolding ceros_of_boolean_input_def
  apply auto
  by (smt (verit, ccfv_threshold) bool_fun_ast_def case_prod_conv dim_vec index_vec vec_eq_iff)

lemma
  simplicial_complex_ast_implies_snd_true:
  assumes "γ ∈ simplicial_complex_induced_by_monotone_boolean_function_ast nn
     (bool_fun_ast nn f)"
  shows "snd f (simplicial_complex.bool_vec_from_simplice (snd nn) (snd γ))"
  using assms
  unfolding simplicial_complex.bool_vec_from_simplice_def
  unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
  unfolding bool_fun_ast_def
  unfolding ceros_of_boolean_input_def
  by auto (smt (verit, ccfv_threshold) bool_fun_ast_def
        case_prod_conv dim_vec index_vec vec_eq_iff)

lemma eq_ast:
"simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
= set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
          (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
proof
  show "set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
     (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
    ⊆ simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
        (bool_fun_ast (n, m) f)"
  proof
    fix γ::"nat set*nat set"
    assume pert: "γ ∈ set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
     (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
    hence f: "(fst γ) ∈ simplicial_complex_induced_by_monotone_boolean_function n (fst f)"
      unfolding set_ast_def
      by auto
    have sigma: "fst f (simplicial_complex.bool_vec_from_simplice n (fst γ))"
      using simplicial_complex.simplicial_complex_implies_true [OF f] .
    from pert have g: "(snd γ) ∈ simplicial_complex_induced_by_monotone_boolean_function m (snd f)"
      unfolding set_ast_def by auto
    have tau: "(snd f) (simplicial_complex.bool_vec_from_simplice m (snd γ))"
      using simplicial_complex.simplicial_complex_implies_true [OF g] .
    from sigma and tau have sigtau: "bool_fun_ast (n, m) f
        ((simplicial_complex.bool_vec_from_simplice n (fst γ)),
         (simplicial_complex.bool_vec_from_simplice m (snd γ)))"
      unfolding bool_fun_ast_def
      by auto
    from sigtau
    show "γ ∈ simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
              (bool_fun_ast (n, m) f)"
      unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
      unfolding bool_fun_ast_def
      using sigma apply auto
      using f g simplicial_complex_induced_by_monotone_boolean_function_def by fastforce
  qed
next
  show "simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
     (bool_fun_ast (n, m) f)
    ⊆ set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
        (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
    proof
    fix γ :: "nat set*nat set"
    assume pert: "γ ∈ simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
     (bool_fun_ast (n, m) f)"
    have sigma: "(fst γ) ∈ simplicial_complex_induced_by_monotone_boolean_function n (fst f)"
      unfolding bool_fun_ast_def
      unfolding simplicial_complex_induced_by_monotone_boolean_function_def
      unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
      apply auto
      apply (rule exI [of _ "simplicial_complex.bool_vec_from_simplice n (fst γ)"], safe)
      using simplicial_complex.bool_vec_from_simplice_def apply auto[1]
        apply (metis fst_conv pert simplicial_complex_ast_implies_fst_true)
      using ceros_of_boolean_input_def simplicial_complex.bool_vec_from_simplice_def
        apply fastforce
      using ceros_of_boolean_input_def pert
          simplicial_complex.bool_vec_from_simplice_def
          simplicial_complex_induced_by_monotone_boolean_function_ast_def by force
   have tau: "(snd γ) ∈ simplicial_complex_induced_by_monotone_boolean_function m (snd f)"
      unfolding bool_fun_ast_def
      unfolding simplicial_complex_induced_by_monotone_boolean_function_def
      unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
      apply auto
      apply (rule exI [of _ "simplicial_complex.bool_vec_from_simplice m (snd γ)"], safe)
      using simplicial_complex.bool_vec_from_simplice_def apply auto[1]
        apply (metis snd_conv pert simplicial_complex_ast_implies_snd_true)
      using ceros_of_boolean_input_def simplicial_complex.bool_vec_from_simplice_def
       apply fastforce
      using ceros_of_boolean_input_def pert
        simplicial_complex.bool_vec_from_simplice_def
        simplicial_complex_induced_by_monotone_boolean_function_ast_def by force
    from sigma and tau
    show "γ ∈ set_ast
        (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
        (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
      using set_ast_def
      by force
  qed
qed

end