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