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 Yc 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 Yc 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 NOTXf"

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 NOTXf 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 NOTXf c (p c left_cart_proj X 𝟭) = 𝗍"
   using assms transpose_of_comp by (typecheck_cfuncs, auto)
 then have "(NOT c FORALL X c NOTXf) 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