Theory Quant_Logic

section ‹Quantifiers›

theory Quant_Logic
  imports Pred_Logic Exponential_Objects
begin

subsection ‹Universal Quantification›

definition FORALL :: "cset ⇒ cfunc" where
  "FORALL X = (THE χ. is_pullback 𝟭 𝟭 (Ω⇗X⇖) Ω (β⇘𝟭⇙) 𝗍 ((𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯) χ)"

lemma FORALL_is_pullback:
  "is_pullback 𝟭 𝟭 (Ω⇗X⇖) Ω (β⇘𝟭⇙) 𝗍 ((𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯) (FORALL X)"
  unfolding FORALL_def
  using characteristic_function_exists element_monomorphism
  by (typecheck_cfuncs, simp add: the1I2)

lemma FORALL_type[type_rule]:
  "FORALL X : Ω⇗X⇖ → Ω"
  using FORALL_is_pullback unfolding is_pullback_def  by auto

lemma all_true_implies_FORALL_true:
  assumes p_type[type_rule]: "p : X → Ω" and all_p_true: "⋀ x. x ∈⇩c X ⟹ p ∘⇩c x = 𝗍"
  shows "FORALL X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
proof -
  have "p ∘⇩c left_cart_proj X 𝟭 = 𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙"
  proof (etcs_rule one_separator)
    fix x
    assume x_type: "x ∈⇩c X ×⇩c 𝟭"

    have "(p ∘⇩c left_cart_proj X 𝟭) ∘⇩c x = p ∘⇩c (left_cart_proj X 𝟭 ∘⇩c x)"
      using x_type p_type comp_associative2 by (typecheck_cfuncs, auto)
    also have "... = 𝗍"
      using x_type all_p_true by (typecheck_cfuncs, auto)
    also have "... = 𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙ ∘⇩c x "
      using x_type by (typecheck_cfuncs, metis id_right_unit2 id_type one_unique_element)
    also have "... = (𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙) ∘⇩c x"
      using x_type comp_associative2 by (typecheck_cfuncs, auto)    
    finally show "(p ∘⇩c left_cart_proj X 𝟭) ∘⇩c x = (𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙) ∘⇩c x".
  qed
  then have "(p ∘⇩c left_cart_proj X 𝟭)⇧♯ = (𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯"
    by simp
  then have "FORALL X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍 ∘⇩c β⇘𝟭⇙"
    using FORALL_is_pullback unfolding is_pullback_def  by auto
  then show "FORALL X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
    using NOT_false_is_true NOT_is_pullback is_pullback_def  by auto
qed

lemma all_true_implies_FORALL_true2:
  assumes p_type[type_rule]: "p : X ×⇩c Y → Ω" and all_p_true: "⋀ xy. xy ∈⇩c X ×⇩c Y ⟹ p ∘⇩c xy = 𝗍"
  shows "FORALL X ∘⇩c p⇧♯ = 𝗍 ∘⇩c β⇘Y⇙"
proof -
  have "p = 𝗍 ∘⇩c β⇘X ×⇩c Y⇙"
  proof (etcs_rule one_separator)
    fix xy
    assume xy_type[type_rule]: "xy ∈⇩c X ×⇩c Y"
    then have "p ∘⇩c xy = 𝗍"
      using all_p_true by blast
    then have "p ∘⇩c xy = 𝗍 ∘⇩c (β⇘X ×⇩c Y⇙ ∘⇩c xy)"
      by (typecheck_cfuncs, metis id_right_unit2 id_type one_unique_element)
    then show "p ∘⇩c xy = (𝗍 ∘⇩c β⇘X ×⇩c Y⇙) ∘⇩c xy"
      by (typecheck_cfuncs, smt comp_associative2)
  qed
  then have "p⇧♯ = (𝗍 ∘⇩c β⇘X ×⇩c Y⇙)⇧♯"
    by blast
  then have "p⇧♯ = (𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙ ∘⇩c (id X ×⇩f β⇘Y⇙))⇧♯"
    by (typecheck_cfuncs, metis terminal_func_unique)
  then have "p⇧♯ = ((𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙) ∘⇩c (id X ×⇩f β⇘Y⇙))⇧♯"
    by (typecheck_cfuncs, smt comp_associative2)
  then have "p⇧♯ = (𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯ ∘⇩c β⇘Y⇙"
    by (typecheck_cfuncs, simp add: sharp_comp)
  then have "FORALL X ∘⇩c p⇧♯ = (FORALL X ∘⇩c (𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯) ∘⇩c β⇘Y⇙"
    by (typecheck_cfuncs, smt comp_associative2)
  then have "FORALL X ∘⇩c p⇧♯ = (𝗍 ∘⇩c β⇘𝟭⇙) ∘⇩c β⇘Y⇙"
    using FORALL_is_pullback unfolding is_pullback_def  by auto
  then show "FORALL X ∘⇩c p⇧♯ = 𝗍 ∘⇩c β⇘Y⇙"
    by (metis id_right_unit2 id_type terminal_func_unique true_func_type)
qed

lemma all_true_implies_FORALL_true3:
  assumes p_type[type_rule]: "p : X ×⇩c 𝟭 → Ω" and all_p_true: "⋀ x. x ∈⇩c X ⟹ p ∘⇩c ⟨x, id 𝟭⟩ = 𝗍"
  shows "FORALL X ∘⇩c p⇧♯ = 𝗍"
proof -
  have "FORALL X ∘⇩c p⇧♯ = 𝗍 ∘⇩c β⇘𝟭⇙"
    by (etcs_rule all_true_implies_FORALL_true2, metis all_p_true cart_prod_decomp id_type one_unique_element)
  then show ?thesis
    by (metis id_right_unit2 id_type terminal_func_unique true_func_type)
qed

lemma FORALL_true_implies_all_true:
  assumes p_type: "p : X → Ω" and FORALL_p_true: "FORALL X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
  shows "⋀ x. x ∈⇩c X ⟹ p ∘⇩c x = 𝗍"
proof (rule ccontr)
  fix x
  assume x_type: "x ∈⇩c X"
  assume "p ∘⇩c x ≠ 𝗍"
  then have "p ∘⇩c x = 𝖿"
    using comp_type p_type true_false_only_truth_values x_type by blast
  then have "p ∘⇩c left_cart_proj X 𝟭 ∘⇩c ⟨x, id 𝟭⟩ = 𝖿"
    using id_type left_cart_proj_cfunc_prod x_type by auto
  then have p_left_proj_false: "p ∘⇩c left_cart_proj X 𝟭 ∘⇩c ⟨x, id 𝟭⟩ = 𝖿 ∘⇩c β⇘X ×⇩c 𝟭⇙ ∘⇩c ⟨x, id 𝟭⟩"
    using x_type by (typecheck_cfuncs, metis id_right_unit2 one_unique_element)

  have "𝗍 ∘⇩c id 𝟭 = FORALL X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯"
    using FORALL_p_true id_right_unit2 true_func_type by auto
  then obtain j where 
      j_type: "j ∈⇩c 𝟭" and 
      j_id: "β⇘𝟭⇙ ∘⇩c j = id 𝟭" and
      t_j_eq_p_left_proj: "(𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯ ∘⇩c j = (p ∘⇩c left_cart_proj X 𝟭)⇧♯"
    using FORALL_is_pullback p_type unfolding is_pullback_def by (typecheck_cfuncs, blast)
  then have "j = id 𝟭"
    using id_type one_unique_element by blast
  then have "(𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯ = (p ∘⇩c left_cart_proj X 𝟭)⇧♯"
    using id_right_unit2 t_j_eq_p_left_proj p_type by (typecheck_cfuncs, auto)
  then have "𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙ = p ∘⇩c left_cart_proj X 𝟭"
    using p_type by (typecheck_cfuncs, metis flat_cancels_sharp)
  then have p_left_proj_true: "𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙ ∘⇩c ⟨x, id 𝟭⟩ = p ∘⇩c left_cart_proj X 𝟭 ∘⇩c ⟨x, id 𝟭⟩"
    using p_type x_type comp_associative2 by (typecheck_cfuncs, auto)

  have "𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙ ∘⇩c ⟨x, id 𝟭⟩ = 𝖿 ∘⇩c β⇘X ×⇩c 𝟭⇙ ∘⇩c ⟨x, id 𝟭⟩"
    using p_left_proj_false p_left_proj_true by auto
  then have "𝗍 ∘⇩c id 𝟭 = 𝖿 ∘⇩c id 𝟭"
    by (metis id_type right_cart_proj_cfunc_prod right_cart_proj_type terminal_func_unique x_type)
  then have "𝗍 = 𝖿"
    using true_func_type false_func_type id_right_unit2 by auto
  then show False
    using true_false_distinct by auto
qed

lemma FORALL_true_implies_all_true2:
  assumes p_type[type_rule]: "p : X ×⇩c Y → Ω" and FORALL_p_true: "FORALL X ∘⇩c p⇧♯ = 𝗍 ∘⇩c β⇘Y⇙"
  shows "⋀ x y. x ∈⇩c X ⟹ y ∈⇩c Y ⟹ p ∘⇩c ⟨x, y⟩ = 𝗍"
proof -
  have "p⇧♯ = (𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙)⇧♯ ∘⇩c β⇘Y⇙"
    using FORALL_is_pullback FORALL_p_true unfolding is_pullback_def 
    by (typecheck_cfuncs, metis terminal_func_unique)
  then have "p⇧♯ = ((𝗍 ∘⇩c β⇘X ×⇩c 𝟭⇙) ∘⇩c (id X ×⇩f β⇘Y⇙))⇧♯"
    by (typecheck_cfuncs, simp add: sharp_comp)
  then have "p⇧♯ = (𝗍 ∘⇩c β⇘X ×⇩c Y⇙)⇧♯"
    by (typecheck_cfuncs_prems, smt (z3) comp_associative2 terminal_func_comp)
  then have "p = 𝗍 ∘⇩c β⇘X ×⇩c Y⇙"
    by (typecheck_cfuncs, metis flat_cancels_sharp)
  then have "⋀ x y. x ∈⇩c X ⟹ y ∈⇩c Y ⟹ p ∘⇩c ⟨x, y⟩ = (𝗍 ∘⇩c β⇘X ×⇩c Y⇙) ∘⇩c ⟨x, y⟩"
    by auto
  then show "⋀ x y. x ∈⇩c X ⟹ y ∈⇩c Y ⟹ p ∘⇩c ⟨x, y⟩ = 𝗍"
  proof -
    fix x y
    assume xy_types[type_rule]: "x ∈⇩c X" "y ∈⇩c Y"
    assume "⋀x y. x ∈⇩c X ⟹ y ∈⇩c Y ⟹ p ∘⇩c ⟨x,y⟩ = (𝗍 ∘⇩c β⇘X ×⇩c Y⇙) ∘⇩c ⟨x,y⟩"
    then have "p ∘⇩c ⟨x,y⟩ = (𝗍 ∘⇩c β⇘X ×⇩c Y⇙) ∘⇩c ⟨x,y⟩"
      using xy_types by auto
    then have "p ∘⇩c ⟨x,y⟩ = 𝗍 ∘⇩c (β⇘X ×⇩c Y⇙ ∘⇩c ⟨x,y⟩)"
      by (typecheck_cfuncs, smt comp_associative2)
    then show "p ∘⇩c ⟨x, y⟩ = 𝗍"
      by (typecheck_cfuncs_prems, metis id_right_unit2 id_type one_unique_element)
  qed
qed

lemma FORALL_true_implies_all_true3:
  assumes p_type[type_rule]: "p : X ×⇩c 𝟭 → Ω" and FORALL_p_true: "FORALL X ∘⇩c p⇧♯ = 𝗍"
  shows "⋀ x. x ∈⇩c X  ⟹ p ∘⇩c ⟨x, id 𝟭⟩ = 𝗍"
  using FORALL_p_true FORALL_true_implies_all_true2 id_right_unit2 terminal_func_unique by (typecheck_cfuncs, auto)

lemma FORALL_elim:
  assumes FORALL_p_true: "FORALL X ∘⇩c p⇧♯ = 𝗍" and p_type[type_rule]: "p : X ×⇩c 𝟭 → Ω"
  assumes x_type[type_rule]: "x ∈⇩c X"
  shows "(p ∘⇩c ⟨x, id 𝟭⟩ = 𝗍 ⟹ P) ⟹ P"
  using FORALL_p_true FORALL_true_implies_all_true3 p_type x_type by blast

lemma FORALL_elim':
  assumes FORALL_p_true: "FORALL X ∘⇩c p⇧♯ = 𝗍" and p_type[type_rule]: "p : X ×⇩c 𝟭 → Ω"
  shows "((⋀x. x ∈⇩c X ⟹ p ∘⇩c ⟨x, id 𝟭⟩ = 𝗍) ⟹ P) ⟹ P"
  using FORALL_p_true FORALL_true_implies_all_true3 p_type by auto

subsection ‹Existential Quantification›

definition EXISTS :: "cset ⇒ cfunc" where
  "EXISTS X = NOT ∘⇩c FORALL X ∘⇩c NOT⇗X⇖⇩f"

lemma EXISTS_type[type_rule]:
  "EXISTS X : Ω⇗X⇖ → Ω"
  unfolding EXISTS_def by typecheck_cfuncs

lemma EXISTS_true_implies_exists_true:
  assumes p_type: "p : X → Ω" and EXISTS_p_true: "EXISTS X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
  shows "∃ x. x ∈⇩c X ∧ p ∘⇩c x = 𝗍"
proof -
  have "NOT ∘⇩c FORALL X ∘⇩c NOT⇗X⇖⇩f ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
    using p_type EXISTS_p_true cfunc_type_def comp_associative comp_type
    unfolding EXISTS_def
    by (typecheck_cfuncs, auto)
  then have "NOT ∘⇩c FORALL X ∘⇩c (NOT ∘⇩c p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
    using p_type transpose_of_comp by (typecheck_cfuncs, auto)
  then have "FORALL X ∘⇩c (NOT ∘⇩c p ∘⇩c left_cart_proj X 𝟭)⇧♯ ≠ 𝗍"
    using NOT_true_is_false true_false_distinct by auto
  then have "FORALL X ∘⇩c ((NOT ∘⇩c p) ∘⇩c left_cart_proj X 𝟭)⇧♯ ≠ 𝗍"
    using p_type comp_associative2 by (typecheck_cfuncs, auto)
  then have "¬ (∀ x. x ∈⇩c X ⟶ (NOT ∘⇩c p) ∘⇩c x = 𝗍)"
    using NOT_type all_true_implies_FORALL_true comp_type p_type by blast
  then have "¬ (∀ x. x ∈⇩c X ⟶ NOT ∘⇩c (p ∘⇩c x) = 𝗍)"
    using p_type comp_associative2 by (typecheck_cfuncs, auto)
  then have "¬ (∀ x. x ∈⇩c X ⟶ p ∘⇩c x ≠ 𝗍)"
    using NOT_false_is_true comp_type p_type true_false_only_truth_values by fastforce
  then show "∃x. x ∈⇩c X ∧ p ∘⇩c x = 𝗍"
    by blast
qed

lemma EXISTS_elim:
  assumes EXISTS_p_true: "EXISTS X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍" and p_type: "p : X → Ω"
  shows "(⋀ x. x ∈⇩c X ⟹ p ∘⇩c x = 𝗍 ⟹ Q) ⟹ Q"
  using EXISTS_p_true EXISTS_true_implies_exists_true p_type by auto

lemma exists_true_implies_EXISTS_true:
  assumes p_type: "p : X → Ω" and exists_p_true: "∃ x. x ∈⇩c X ∧ p ∘⇩c x = 𝗍"
  shows  "EXISTS X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
proof -
 have "¬ (∀ x. x ∈⇩c X ⟶ p ∘⇩c x ≠ 𝗍)"
   using exists_p_true by blast
 then have "¬ (∀ x. x ∈⇩c X ⟶ NOT ∘⇩c (p ∘⇩c x) = 𝗍)"
   using NOT_true_is_false true_false_distinct by auto
 then have "¬ (∀ x. x ∈⇩c X ⟶ (NOT ∘⇩c p) ∘⇩c x = 𝗍)"
   using p_type by (typecheck_cfuncs, metis NOT_true_is_false cfunc_type_def comp_associative exists_p_true true_false_distinct)
 then have "FORALL X ∘⇩c ((NOT ∘⇩c p) ∘⇩c left_cart_proj X 𝟭)⇧♯ ≠ 𝗍"
   using FORALL_true_implies_all_true NOT_type comp_type p_type by blast
 then have "FORALL X ∘⇩c (NOT ∘⇩c p ∘⇩c left_cart_proj X 𝟭)⇧♯ ≠ 𝗍"
   using NOT_type cfunc_type_def comp_associative left_cart_proj_type p_type by auto
 then have "NOT ∘⇩c FORALL X ∘⇩c (NOT ∘⇩c p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
   using assms NOT_is_false_implies_true true_false_only_truth_values by (typecheck_cfuncs, blast)
 then have "NOT ∘⇩c FORALL X ∘⇩c NOT⇗X⇖⇩f ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
   using assms transpose_of_comp by (typecheck_cfuncs, auto)
 then have "(NOT ∘⇩c FORALL X ∘⇩c NOT⇗X⇖⇩f) ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
    using assms cfunc_type_def comp_associative by (typecheck_cfuncs,auto)
 then show "EXISTS X ∘⇩c (p ∘⇩c left_cart_proj X 𝟭)⇧♯ = 𝗍"
  by (simp add: EXISTS_def)
qed

end