Theory Elementary_Logic
section ‹Elementary Logic›
theory Elementary_Logic
imports
Proof_System
Propositional_Wff
begin
no_notation funcset (infixr "→" 60)
notation funcset (infixr "⇸" 60)
subsection ‹Proposition 5200›
proposition prop_5200:
assumes "A ∈ wffs⇘α⇙"
shows "⊢ A =⇘α⇙ A"
using assms and equality_reflexivity and dv_thm by simp
corollary hyp_prop_5200:
assumes "is_hyps ℋ" and "A ∈ wffs⇘α⇙"
shows "ℋ ⊢ A =⇘α⇙ A"
using derivability_implies_hyp_derivability[OF prop_5200[OF assms(2)] assms(1)] .
subsection ‹Proposition 5201 (Equality Rules)›
proposition prop_5201_1:
assumes "ℋ ⊢ A" and "ℋ ⊢ A ≡⇧𝒬 B"
shows "ℋ ⊢ B"
proof -
from assms(2) have "ℋ ⊢ A =⇘o⇙ B"
unfolding equivalence_def .
with assms(1) show ?thesis
by (rule rule_R'[where p = "[]"]) auto
qed
proposition prop_5201_2:
assumes "ℋ ⊢ A =⇘α⇙ B"
shows "ℋ ⊢ B =⇘α⇙ A"
proof -
have "ℋ ⊢ A =⇘α⇙ A"
proof (rule hyp_prop_5200)
from assms show "is_hyps ℋ"
by (blast elim: is_derivable_from_hyps.cases)
show "A ∈ wffs⇘α⇙"
by (fact hyp_derivable_form_is_wffso[OF assms, THEN wffs_from_equality(1)])
qed
from this and assms show ?thesis
by (rule rule_R'[where p = "[«,»]"]) (force+, fastforce dest: subforms_from_app)
qed
proposition prop_5201_3:
assumes "ℋ ⊢ A =⇘α⇙ B" and "ℋ ⊢ B =⇘α⇙ C"
shows "ℋ ⊢ A =⇘α⇙ C"
using assms by (rule rule_R'[where p = "[»]"]) (force+, fastforce dest: subforms_from_app)
proposition prop_5201_4:
assumes "ℋ ⊢ A =⇘α→β⇙ B" and "ℋ ⊢ C =⇘α⇙ D"
shows "ℋ ⊢ A · C =⇘β⇙ B · D"
proof -
have "ℋ ⊢ A · C =⇘β⇙ A · C"
proof (rule hyp_prop_5200)
from assms show "is_hyps ℋ"
by (blast elim: is_derivable_from_hyps.cases)
from assms have "A ∈ wffs⇘α→β⇙" and "C ∈ wffs⇘α⇙"
using hyp_derivable_form_is_wffso and wffs_from_equality by blast+
then show "A · C ∈ wffs⇘β⇙"
by auto
qed
from this and assms(1) have "ℋ ⊢ A · C =⇘β⇙ B · C"
by (rule rule_R'[where p = "[»,«]"]) (force+, fastforce dest: subforms_from_app)
from this and assms(2) show ?thesis
by (rule rule_R'[where p = "[»,»]"]) (force+, fastforce dest: subforms_from_app)
qed
proposition prop_5201_5:
assumes "ℋ ⊢ A =⇘α→β⇙ B" and "C ∈ wffs⇘α⇙"
shows "ℋ ⊢ A · C =⇘β⇙ B · C"
proof -
have "ℋ ⊢ A · C =⇘β⇙ A · C"
proof (rule hyp_prop_5200)
from assms(1) show "is_hyps ℋ"
by (blast elim: is_derivable_from_hyps.cases)
have "A ∈ wffs⇘α→β⇙"
by (fact hyp_derivable_form_is_wffso[OF assms(1), THEN wffs_from_equality(1)])
with assms(2) show "A · C ∈ wffs⇘β⇙"
by auto
qed
from this and assms(1) show ?thesis
by (rule rule_R'[where p = "[»,«]"]) (force+, fastforce dest: subforms_from_app)
qed
proposition prop_5201_6:
assumes "ℋ ⊢ C =⇘α⇙ D" and "A ∈ wffs⇘α→β⇙"
shows "ℋ ⊢ A · C =⇘β⇙ A · D"
proof -
have "ℋ ⊢ A · C =⇘β⇙ A · C"
proof (rule hyp_prop_5200)
from assms(1) show "is_hyps ℋ"
by (blast elim: is_derivable_from_hyps.cases)
have "C ∈ wffs⇘α⇙"
by (fact hyp_derivable_form_is_wffso[OF assms(1), THEN wffs_from_equality(1)])
with assms(2) show "A · C ∈ wffs⇘β⇙"
by auto
qed
from this and assms(1) show ?thesis
by (rule rule_R'[where p = "[»,»]"]) (force+, fastforce dest: subforms_from_app)
qed
lemmas Equality_Rules = prop_5201_1 prop_5201_2 prop_5201_3 prop_5201_4 prop_5201_5 prop_5201_6
subsection ‹Proposition 5202 (Rule RR)›
proposition prop_5202:
assumes "⊢ A =⇘α⇙ B ∨ ⊢ B =⇘α⇙ A"
and "p ∈ positions C" and "A ≼⇘p⇙ C" and "C⦉p ← B⦊ ⊳ D"
and "ℋ ⊢ C"
shows "ℋ ⊢ D"
proof -
from assms(5) have "⊢ C =⇘o⇙ C"
using prop_5200 and hyp_derivable_form_is_wffso by blast
moreover from assms(1) consider (a) "⊢ A =⇘α⇙ B" | (b) "⊢ B =⇘α⇙ A"
by blast
then have "⊢ A =⇘α⇙ B"
by cases (assumption, fact Equality_Rules(2))
ultimately have "⊢ C =⇘o⇙ D"
by (rule rule_R[where p = "» # p"]) (use assms(2-4) in auto)
then have "ℋ ⊢ C =⇘o⇙ D"
proof -
from assms(5) have "is_hyps ℋ"
by (blast elim: is_derivable_from_hyps.cases)
with ‹⊢ C =⇘o⇙ D› show ?thesis
by (fact derivability_implies_hyp_derivability)
qed
with assms(5) show ?thesis
by (rule Equality_Rules(1)[unfolded equivalence_def])
qed
lemmas rule_RR = prop_5202
subsection ‹Proposition 5203›
proposition prop_5203:
assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘β⇙"
and "∀v ∈ vars A. ¬ is_bound v B"
shows "⊢ (λx⇘α⇙. B) · A =⇘β⇙ ❙S {(x, α) ↣ A} B"
using assms(2,1,3) proof induction
case (var_is_wff β y)
then show ?case
proof (cases "y⇘β⇙ = x⇘α⇙")
case True
then have "α = β"
by simp
moreover from assms(1) have "⊢ (λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A"
using axiom_4_2 by (intro axiom_is_derivable_from_no_hyps)
moreover have "❙S {(x, α) ↣ A} (x⇘α⇙) = A"
by force
ultimately show ?thesis
using True by (simp only:)
next
case False
with assms(1) have "⊢ (λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙"
using axiom_4_1_var by (intro axiom_is_derivable_from_no_hyps)
moreover from False have "❙S {(x, α) ↣ A} (y⇘β⇙) = y⇘β⇙"
by auto
ultimately show ?thesis
by (simp only:)
qed
next
case (con_is_wff β c)
from assms(1) have "⊢ (λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙"
using axiom_4_1_con by (intro axiom_is_derivable_from_no_hyps)
moreover have "❙S {(x, α) ↣ A} (⦃c⦄⇘β⇙) = ⦃c⦄⇘β⇙"
by auto
ultimately show ?case
by (simp only:)
next
case (app_is_wff γ β D C)
from app_is_wff.prems(2) have not_bound_subforms: "∀v ∈ vars A. ¬ is_bound v D ∧ ¬ is_bound v C"
using is_bound_in_app_homomorphism by fast
from ‹D ∈ wffs⇘γ→β⇙› have "⊢ (λx⇘α⇙. D) · A =⇘γ→β⇙ ❙S {(x, α) ↣ A} D"
using app_is_wff.IH(1)[OF assms(1)] and not_bound_subforms by simp
moreover from ‹C ∈ wffs⇘γ⇙› have "⊢ (λx⇘α⇙. C) · A =⇘γ⇙ ❙S {(x, α) ↣ A} C"
using app_is_wff.IH(2)[OF assms(1)] and not_bound_subforms by simp
moreover have "⊢ (λx⇘α⇙. D · C) · A =⇘β⇙ ((λx⇘α⇙. D) · A) · ((λx⇘α⇙. C) · A)"
using axiom_is_derivable_from_no_hyps[OF axiom_4_3[OF assms(1) ‹D ∈ wffs⇘γ→β⇙› ‹C ∈ wffs⇘γ⇙›]] .
ultimately show ?case
using Equality_Rules(3,4) and substitute.simps(3) by presburger
next
case (abs_is_wff β D γ y)
then show ?case
proof (cases "y⇘γ⇙ = x⇘α⇙")
case True
then have "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→β⇙ λy⇘γ⇙. D"
using axiom_is_derivable_from_no_hyps[OF axiom_4_5[OF assms(1) abs_is_wff.hyps(1)]] by fast
moreover from True have "❙S {(x, α) ↣ A} (λy⇘γ⇙. D) = λy⇘γ⇙. D"
using empty_substitution_neutrality
by (simp add: singleton_substitution_simps(4) fmdrop_fmupd_same)
ultimately show ?thesis
by (simp only:)
next
case False
have "binders_at (λy⇘γ⇙. D) [«] = {(y, γ)}"
by simp
then have "is_bound (y, γ) (λy⇘γ⇙. D)"
by fastforce
with abs_is_wff.prems(2) have "(y, γ) ∉ vars A"
by blast
with ‹y⇘γ⇙ ≠ x⇘α⇙› have "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→β⇙ λy⇘γ⇙. (λx⇘α⇙. D) · A"
using axiom_4_4[OF assms(1) abs_is_wff.hyps(1)] and axiom_is_derivable_from_no_hyps by blast
moreover have "⊢ (λx⇘α⇙. D) · A =⇘β⇙ ❙S {(x, α) ↣ A} D"
proof -
have "∀p. y⇘γ⇙ ≼⇘« # p⇙ λy⇘γ⇙. D ⟶ y⇘γ⇙ ≼⇘p⇙ D"
using subforms_from_abs by fastforce
from abs_is_wff.prems(2) have "∀v ∈ vars A. ¬ is_bound v D"
using is_bound_in_abs_body by fast
then show ?thesis
by (fact abs_is_wff.IH[OF assms(1)])
qed
ultimately have "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→β⇙ λy⇘γ⇙. ❙S {(x, α) ↣ A} D"
by (rule rule_R[where p = "[»,«]"]) force+
with False show ?thesis
by simp
qed
qed
subsection ‹Proposition 5204›
proposition prop_5204:
assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘β⇙" and "C ∈ wffs⇘β⇙"
and "⊢ B =⇘β⇙ C"
and "∀v ∈ vars A. ¬ is_bound v B ∧ ¬ is_bound v C"
shows "⊢ ❙S {(x, α) ↣ A} (B =⇘β⇙ C)"
proof -
have "⊢ (λx⇘α⇙. B) · A =⇘β⇙ (λx⇘α⇙. B) · A"
proof -
have "(λx⇘α⇙. B) · A ∈ wffs⇘β⇙"
using assms(1,2) by auto
then show ?thesis
by (fact prop_5200)
qed
from this and assms(4) have "⊢ (λx⇘α⇙. B) · A =⇘β⇙ (λx⇘α⇙. C) · A"
by (rule rule_R[where p = "[»,«,«]"]) force+
moreover from assms(1,2,5) have "⊢ (λx⇘α⇙. B) · A =⇘β⇙ ❙S {(x, α) ↣ A} B"
using prop_5203 by auto
moreover from assms(1,3,5) have "⊢ (λx⇘α⇙. C) · A =⇘β⇙ ❙S {(x, α) ↣ A} C"
using prop_5203 by auto
ultimately have "⊢ (❙S {(x, α) ↣ A} B) =⇘β⇙ (❙S {(x, α) ↣ A} C)"
using Equality_Rules(2,3) by blast
then show ?thesis
by simp
qed
subsection ‹Proposition 5205 ($\eta$-conversion)›
proposition prop_5205:
shows "⊢ 𝔣⇘α→β⇙ =⇘α→β⇙ (λy⇘α⇙. 𝔣⇘α→β⇙ · y⇘α⇙)"
proof -
{
fix y
assume "y⇘α⇙ ≠ 𝔵⇘α⇙"
let ?A = "λy⇘α⇙. 𝔣⇘α→β⇙ · y⇘α⇙"
have "⊢ (𝔣⇘α→β⇙ =⇘α→β⇙ ?A) =⇘o⇙ ∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ ?A · 𝔵⇘α⇙)"
proof -
have "⊢ (𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) =⇘o⇙ ∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙)" (is "⊢ ?B =⇘o⇙ ?C")
using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
have "⊢ ❙S {(𝔤, α→β) ↣ ?A} (?B =⇘o⇙ ?C)"
proof -
have "?A ∈ wffs⇘α→β⇙" and "?B ∈ wffs⇘o⇙" and "?C ∈ wffs⇘o⇙"
by auto
moreover have "∀v ∈ vars ?A. ¬ is_bound v ?B ∧ ¬ is_bound v ?C"
proof
fix v
assume "v ∈ vars ?A"
have "vars ?B = {(𝔣, α→β), (𝔤, α→β)}" and "vars ?C = {(𝔣, α→β), (𝔵, α), (𝔤, α→β)}"
by force+
with ‹y⇘α⇙ ≠ 𝔵⇘α⇙› have "(y, α) ∉ vars ?B" and "(y, α) ∉ vars ?C"
by force+
then have "¬ is_bound (y, α) ?B" and "¬ is_bound (y, α) ?C"
using absent_var_is_not_bound by blast+
moreover have "¬ is_bound (𝔣, α→β) ?B" and "¬ is_bound (𝔣, α→β) ?C"
by code_simp+
moreover from ‹v ∈ vars ?A› have "v ∈ {(y, α), (𝔣, α→β)}"
by auto
ultimately show "¬ is_bound v ?B ∧ ¬ is_bound v ?C"
by fast
qed
ultimately show ?thesis
using ‹⊢ ?B =⇘o⇙ ?C› and prop_5204 by presburger
qed
then show ?thesis
by simp
qed
moreover have "⊢ ?A · 𝔵⇘α⇙ =⇘β⇙ 𝔣⇘α→β⇙ · 𝔵⇘α⇙"
proof -
have "𝔵⇘α⇙ ∈ wffs⇘α⇙" and "𝔣⇘α→β⇙ · y⇘α⇙ ∈ wffs⇘β⇙"
by auto
moreover have "∀v ∈ vars (𝔵⇘α⇙). ¬ is_bound v (𝔣⇘α→β⇙ · y⇘α⇙)"
using ‹y⇘α⇙ ≠ 𝔵⇘α⇙› by auto
moreover have "❙S {(y, α) ↣ 𝔵⇘α⇙} (𝔣⇘α→β⇙ · y⇘α⇙) = 𝔣⇘α→β⇙ · 𝔵⇘α⇙"
by simp
ultimately show ?thesis
using prop_5203 by metis
qed
ultimately have "⊢ (𝔣⇘α→β⇙ =⇘α→β⇙ ?A) =⇘o⇙ ∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔣⇘α→β⇙ · 𝔵⇘α⇙)"
by (rule rule_R[where p = "[»,»,«,»]"]) force+
moreover have "⊢ (𝔣⇘α→β⇙ =⇘α→β⇙ 𝔣⇘α→β⇙) =⇘o⇙ ∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔣⇘α→β⇙ · 𝔵⇘α⇙)"
proof -
let ?A = "𝔣⇘α→β⇙"
have "⊢ (𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) =⇘o⇙ ∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙)" (is "⊢ ?B =⇘o⇙ ?C")
using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
have "⊢ ❙S {(𝔤, α→β) ↣ ?A} (?B =⇘o⇙ ?C)"
proof -
have "?A ∈ wffs⇘α→β⇙" and "?B ∈ wffs⇘o⇙" and "?C ∈ wffs⇘o⇙"
by auto
moreover have "∀v ∈ vars ?A. ¬ is_bound v ?B ∧ ¬ is_bound v ?C"
proof
fix v
assume "v ∈ vars ?A"
have "vars ?B = {(𝔣, α→β), (𝔤, α→β)}" and "vars ?C = {(𝔣, α→β), (𝔵, α), (𝔤, α→β)}"
by force+
with ‹y⇘α⇙ ≠ 𝔵⇘α⇙› have "(y, α) ∉ vars ?B" and "(y, α) ∉ vars ?C"
by force+
then have "¬ is_bound (y, α) ?B" and "¬ is_bound (y, α) ?C"
using absent_var_is_not_bound by blast+
moreover have "¬ is_bound (𝔣, α→β) ?B" and "¬ is_bound (𝔣, α→β) ?C"
by code_simp+
moreover from ‹v ∈ vars ?A ›have "v ∈ {(y, α), (𝔣, α→β)}"
by auto
ultimately show "¬ is_bound v ?B ∧ ¬ is_bound v ?C"
by fast
qed
ultimately show ?thesis
using ‹⊢ ?B =⇘o⇙ ?C› and prop_5204 by presburger
qed
then show ?thesis
by simp
qed
ultimately have "⊢ 𝔣⇘α→β⇙ =⇘α→β⇙ (λy⇘α⇙. 𝔣⇘α→β⇙ · y⇘α⇙)"
using Equality_Rules(1)[unfolded equivalence_def] and Equality_Rules(2) and prop_5200
by (metis wffs_of_type_intros(1))
}
note x_neq_y = this
then have "§6": "⊢ 𝔣⇘α→β⇙ =⇘α→β⇙ λ𝔶⇘α⇙. 𝔣⇘α→β⇙ · 𝔶⇘α⇙" (is "⊢ ?B =⇘_⇙ ?C")
by simp
then have "§7": "⊢ (λ𝔵⇘α⇙. 𝔣⇘α→β⇙ · 𝔵⇘α⇙) =⇘α→β⇙ (λ𝔶⇘α⇙. (λ𝔵⇘α⇙. 𝔣⇘α→β⇙ · 𝔵⇘α⇙) · 𝔶⇘α⇙)"
proof -
let ?A = "λ𝔵⇘α⇙. 𝔣⇘α→β⇙ · 𝔵⇘α⇙"
have "?A ∈ wffs⇘α→β⇙" and "?B ∈ wffs⇘α→β⇙" and "?C ∈ wffs⇘α→β⇙"
by auto
moreover have "∀v ∈ vars ?A. ¬ is_bound v ?B ∧ ¬ is_bound v ?C"
proof
fix v
assume "v ∈ vars ?A"
have "¬ is_bound (𝔵, α) ?B" and "¬ is_bound (𝔵, α) ?C"
by code_simp+
moreover have "¬ is_bound (𝔣, α→β) ?B" and "¬ is_bound (𝔣, α→β) ?C"
by code_simp+
moreover from ‹v ∈ vars ?A ›have "v ∈ {(𝔵, α), (𝔣, α→β)}"
by auto
ultimately show "¬ is_bound v ?B ∧ ¬ is_bound v ?C"
by fast
qed
ultimately have "⊢ ❙S {(𝔣, α→β) ↣ ?A} (?B =⇘α→β⇙ ?C)"
using "§6" and prop_5204 by presburger
then show ?thesis
by simp
qed
have "⊢ (λ𝔵⇘α⇙. 𝔣⇘α→β⇙ · 𝔵⇘α⇙) =⇘α→β⇙ (λ𝔶⇘α⇙. 𝔣⇘α→β⇙ · 𝔶⇘α⇙)"
proof -
have "⊢ (λ𝔵⇘α⇙. 𝔣⇘α→β⇙ · 𝔵⇘α⇙) · 𝔶⇘α⇙ =⇘β⇙ 𝔣⇘α→β⇙ · 𝔶⇘α⇙"
proof -
have "𝔶⇘α⇙ ∈ wffs⇘α⇙" and "𝔣⇘α→β⇙ · 𝔵⇘α⇙ ∈ wffs⇘β⇙"
by auto
moreover have "∀v ∈ vars (𝔶⇘α⇙). ¬ is_bound v (𝔣⇘α→β⇙ · 𝔵⇘α⇙)"
by simp
moreover have "❙S {(𝔵, α) ↣ 𝔶⇘α⇙} (𝔣⇘α→β⇙ · 𝔵⇘α⇙) = 𝔣⇘α→β⇙ · 𝔶⇘α⇙"
by simp
ultimately show ?thesis
using prop_5203 by metis
qed
from "§7" and this show ?thesis
by (rule rule_R [where p = "[»,«]"]) force+
qed
with "§6" and x_neq_y[of y] show ?thesis
using Equality_Rules(2,3) by blast
qed
subsection ‹Proposition 5206 ($\alpha$-conversion)›
proposition prop_5206:
assumes "A ∈ wffs⇘α⇙"
and "(z, β) ∉ free_vars A"
and "is_free_for (z⇘β⇙) (x, β) A"
shows "⊢ (λx⇘β⇙. A) =⇘β→α⇙ (λz⇘β⇙. ❙S {(x, β) ↣ z⇘β⇙} A)"
proof -
have "is_substitution {(x, β) ↣ z⇘β⇙}"
by auto
from this and assms(1) have "❙S {(x, β) ↣ z⇘β⇙} A ∈ wffs⇘α⇙"
by (fact substitution_preserves_typing)
obtain y where "(y, β) ∉ {(x, β), (z, β)} ∪ vars A"
proof -
have "finite ({(x, β), (z, β)} ∪ vars A)"
using vars_form_finiteness by blast
with that show ?thesis
using fresh_var_existence by metis
qed
then have "(y, β) ≠ (x, β)" and "(y, β) ≠ (z, β)" and "(y, β) ∉ vars A" and "(y, β) ∉ free_vars A"
using free_vars_in_all_vars by auto
have "§1": "⊢ (λx⇘β⇙. A) =⇘β→α⇙ (λy⇘β⇙. (λx⇘β⇙. A) · y⇘β⇙)"
proof -
let ?A = "λx⇘β⇙. A"
have *: "⊢ 𝔣⇘β→α⇙ =⇘β→α⇙ (λy⇘β⇙. 𝔣⇘β→α⇙ · y⇘β⇙)" (is "⊢ ?B =⇘_⇙ ?C")
by (fact prop_5205)
moreover have "⊢ ❙S {(𝔣, β→α) ↣ ?A} (?B =⇘β→α⇙ ?C)"
proof -
from assms(1) have "?A ∈ wffs⇘β→α⇙" and "?B ∈ wffs⇘β→α⇙" and "?C ∈ wffs⇘β→α⇙"
by auto
moreover have "∀v ∈ vars ?A. ¬ is_bound v ?B ∧ ¬ is_bound v ?C"
proof
fix v
assume "v ∈ vars ?A"
then consider (a) "v = (x, β)" | (b) "v ∈ vars A"
by fastforce
then show "¬ is_bound v ?B ∧ ¬ is_bound v ?C"
proof cases
case a
then show ?thesis
using ‹(y, β) ≠ (x, β)› by force
next
case b
then have "¬ is_bound v ?B"
by simp
moreover have "¬ is_bound v ?C"
using b and ‹(y, β) ∉ vars A› by code_simp force
ultimately show ?thesis
by blast
qed
qed
ultimately show ?thesis
using prop_5204 and * by presburger
qed
ultimately show ?thesis
by simp
qed
then have "§2": "⊢ (λx⇘β⇙. A) =⇘β→α⇙ (λy⇘β⇙. ❙S {(x, β) ↣ y⇘β⇙} A)"
proof -
have "⊢ (λx⇘β⇙. A) · y⇘β⇙ =⇘α⇙ ❙S {(x, β) ↣ y⇘β⇙} A" (is "⊢ (λx⇘β⇙. ?B) · ?A =⇘_⇙ _")
proof -
have "?A ∈ wffs⇘β⇙" and "?B ∈ wffs⇘α⇙"
by blast fact
moreover have "∀v ∈ vars ?A. ¬ is_bound v ?B"
using ‹(y, β) ∉ vars A› and absent_var_is_not_bound by auto
ultimately show ?thesis
by (fact prop_5203)
qed
with "§1" show ?thesis
by (rule rule_R [where p = "[»,«]"]) force+
qed
moreover
have "§3": "⊢ (λz⇘β⇙. ❙S {(x, β) ↣ z⇘β⇙} A) =⇘β→α⇙ (λy⇘β⇙. (λz⇘β⇙. ❙S {(x, β) ↣ z⇘β⇙} A) · y⇘β⇙)"
proof -
let ?A = "λz⇘β⇙. ❙S {(x, β) ↣ z⇘β⇙} A"
have *: "⊢ 𝔣⇘β→α⇙ =⇘β→α⇙ (λy⇘β⇙. 𝔣⇘β→α⇙ · y⇘β⇙)" (is "⊢ ?B =⇘_⇙ ?C")
by (fact prop_5205)
moreover have "⊢ ❙S {(𝔣, β→α) ↣ ?A} (?B =⇘β→α⇙ ?C)"
proof -
have "?A ∈ wffs⇘β→α⇙" and "?B ∈ wffs⇘β→α⇙" and "?C ∈ wffs⇘β→α⇙"
using ‹❙S {(x, β) ↣ z⇘β⇙} A ∈ wffs⇘α⇙› by auto
moreover have "∀v ∈ vars ?A. ¬ is_bound v ?B ∧ ¬ is_bound v ?C"
proof
fix v
assume "v ∈ vars ?A"
then consider (a) "v = (z, β)" | (b) "v ∈ vars (❙S {(x, β) ↣ z⇘β⇙} A)"
by fastforce
then show "¬ is_bound v ?B ∧ ¬ is_bound v ?C"
proof cases
case a
then show ?thesis
using ‹(y, β) ≠ (z, β)› by auto
next
case b
then have "¬ is_bound v ?B"
by simp
moreover from b and ‹(y, β) ∉ vars A› and ‹(y, β) ≠ (z, β)› have "v ≠ (y, β)"
using renaming_substitution_minimal_change by blast
then have "¬ is_bound v ?C"
by code_simp simp
ultimately show ?thesis
by blast
qed
qed
ultimately show ?thesis
using prop_5204 and * by presburger
qed
ultimately show ?thesis
by simp
qed
then have "§4": "⊢ (λz⇘β⇙. ❙S {(x, β) ↣ z⇘β⇙} A) =⇘β→α⇙ (λy⇘β⇙. ❙S {(x, β) ↣ y⇘β⇙} A)"
proof -
have "⊢ (λz⇘β⇙. ❙S {(x, β) ↣ z⇘β⇙} A) · y⇘β⇙ =⇘α⇙ ❙S {(x, β) ↣ y⇘β⇙} A" (is "⊢ (λz⇘β⇙. ?B) · ?A =⇘_⇙ _")
proof -
have "?A ∈ wffs⇘β⇙" and "?B ∈ wffs⇘α⇙"
by blast fact
moreover from ‹(y, β) ∉ vars A› and ‹(y, β) ≠ (z, β)› have "∀v ∈ vars ?A. ¬ is_bound v ?B"
using absent_var_is_not_bound and renaming_substitution_minimal_change by auto
ultimately have "⊢ (λz⇘β⇙. ❙S {(x, β) ↣ z⇘β⇙} A) · y⇘β⇙ =⇘α⇙ ❙S {(z, β) ↣ y⇘β⇙} ❙S {(x, β) ↣ z⇘β⇙} A"
using prop_5203 by fast
moreover have "❙S {(z, β) ↣ y⇘β⇙} ❙S {(x, β) ↣ z⇘β⇙} A = ❙S {(x, β) ↣ y⇘β⇙} A"
by (fact renaming_substitution_composability[OF assms(2,3)])
ultimately show ?thesis
by (simp only:)
qed
with "§3" show ?thesis
by (rule rule_R [where p = "[»,«]"]) auto
qed
ultimately show ?thesis
using Equality_Rules(2,3) by blast
qed
lemmas "α" = prop_5206
subsection ‹Proposition 5207 ($\beta$-conversion)›
context
begin
private lemma bound_var_renaming_equality:
assumes "A ∈ wffs⇘α⇙"
and "z⇘γ⇙ ≠ y⇘γ⇙"
and "(z, γ) ∉ vars A"
shows "⊢ A =⇘α⇙ rename_bound_var (y, γ) z A"
using assms proof induction
case (var_is_wff α x)
then show ?case
using prop_5200 by force
next
case (con_is_wff α c)
then show ?case
using prop_5200 by force
next
case (app_is_wff α β A B)
then show ?case
using Equality_Rules(4) by auto
next
case (abs_is_wff β A α x)
then show ?case
proof (cases "(y, γ) = (x, α)")
case True
have "⊢ λy⇘γ⇙. A =⇘γ→β⇙ λy⇘γ⇙. A"
by (fact abs_is_wff.hyps[THEN prop_5200[OF wffs_of_type_intros(4)]])
moreover have "⊢ A =⇘β⇙ rename_bound_var (y, γ) z A"
using abs_is_wff.IH[OF assms(2)] and abs_is_wff.prems(2) by fastforce
ultimately have "⊢ λy⇘γ⇙. A =⇘γ→β⇙ λy⇘γ⇙. rename_bound_var (y, γ) z A"
by (rule rule_R[where p = "[»,«]"]) force+
moreover
have "
⊢ λy⇘γ⇙. rename_bound_var (y, γ) z A
=⇘γ→β⇙
λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A)"
proof -
have "rename_bound_var (y, γ) z A ∈ wffs⇘β⇙"
using hyp_derivable_form_is_wffso[OF ‹⊢ A =⇘β⇙ rename_bound_var (y, γ) z A›]
by (blast dest: wffs_from_equality)
moreover from abs_is_wff.prems(2) have "(z, γ) ∉ free_vars (rename_bound_var (y, γ) z A)"
using rename_bound_var_free_vars[OF abs_is_wff.hyps assms(2)] by simp
moreover from abs_is_wff.prems(2) have "is_free_for (z⇘γ⇙) (y, γ) (rename_bound_var (y, γ) z A)"
using is_free_for_in_rename_bound_var[OF abs_is_wff.hyps assms(2)] by simp
ultimately show ?thesis
using "α" by fast
qed
ultimately have "⊢ λy⇘γ⇙. A =⇘γ→β⇙ λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} (rename_bound_var (y, γ) z A)"
by (rule Equality_Rules(3))
then show ?thesis
using True by auto
next
case False
have "⊢ λx⇘α⇙. A =⇘α→β⇙ λx⇘α⇙. A"
by (fact abs_is_wff.hyps[THEN prop_5200[OF wffs_of_type_intros(4)]])
moreover have "⊢ A =⇘β⇙ rename_bound_var (y, γ) z A"
using abs_is_wff.IH[OF assms(2)] and abs_is_wff.prems(2) by fastforce
ultimately have "⊢ λx⇘α⇙. A =⇘α→β⇙ λx⇘α⇙. rename_bound_var (y, γ) z A"
by (rule rule_R[where p = "[»,«]"]) force+
then show ?thesis
using False by auto
qed
qed
proposition prop_5207:
assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘β⇙"
and "is_free_for A (x, α) B"
shows "⊢ (λx⇘α⇙. B) · A =⇘β⇙ ❙S {(x, α) ↣ A} B"
using assms proof (induction "form_size B" arbitrary: B β rule: less_induct)
case less
from less(3,1,2,4) show ?case
proof (cases B rule: wffs_of_type_cases)
case (var_is_wff y)
then show ?thesis
proof (cases "y⇘β⇙ = x⇘α⇙")
case True
then have "α = β"
by simp
moreover from assms(1) have "⊢ (λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A"
using axiom_4_2 by (intro axiom_is_derivable_from_no_hyps)
moreover have "❙S {(x, α) ↣ A} (x⇘α⇙) = A"
by force
ultimately show ?thesis
unfolding True and var_is_wff by simp
next
case False
with assms(1) have "⊢ (λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙"
using axiom_4_1_var by (intro axiom_is_derivable_from_no_hyps)
moreover from False have "❙S {(x, α) ↣ A} (y⇘β⇙) = y⇘β⇙"
by auto
ultimately show ?thesis
unfolding False and var_is_wff by simp
qed
next
case (con_is_wff c)
from assms(1) have "⊢ (λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙"
using axiom_4_1_con by (intro axiom_is_derivable_from_no_hyps)
moreover have "❙S {(x, α) ↣ A} (⦃c⦄⇘β⇙) = ⦃c⦄⇘β⇙"
by auto
ultimately show ?thesis
by (simp only: con_is_wff)
next
case (app_is_wff γ D C)
have "form_size D < form_size B" and "form_size C < form_size B"
unfolding app_is_wff(1) by simp_all
from less(4)[unfolded app_is_wff(1)] have "is_free_for A (x, α) D" and "is_free_for A (x, α) C"
using is_free_for_from_app by iprover+
from ‹is_free_for A (x, α) D› have "⊢ (λx⇘α⇙. D) · A =⇘γ→β⇙ ❙S {(x, α) ↣ A} D"
by (fact less(1)[OF ‹form_size D < form_size B› assms(1) app_is_wff(2)])
moreover from ‹is_free_for A (x, α) C› have "⊢ (λx⇘α⇙. C) · A =⇘γ⇙ ❙S {(x, α) ↣ A} C"
by (fact less(1)[OF ‹form_size C < form_size B› assms(1) app_is_wff(3)])
moreover have "⊢ (λx⇘α⇙. D · C) · A =⇘β⇙ ((λx⇘α⇙. D) · A) · ((λx⇘α⇙. C) · A)"
by (fact axiom_4_3[OF assms(1) app_is_wff(2,3), THEN axiom_is_derivable_from_no_hyps])
ultimately show ?thesis
unfolding app_is_wff(1) using Equality_Rules(3,4) and substitute.simps(3) by presburger
next
case (abs_is_wff δ D γ y)
then show ?thesis
proof (cases "y⇘γ⇙ = x⇘α⇙")
case True
with abs_is_wff(1) have "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘β⇙ λy⇘γ⇙. D"
using axiom_4_5[OF assms(1) abs_is_wff(3)] by (simp add: axiom_is_derivable_from_no_hyps)
moreover have "❙S {(x, α) ↣ A} (λy⇘γ⇙. D) = λy⇘γ⇙. D"
using True by (simp add: empty_substitution_neutrality fmdrop_fmupd_same)
ultimately show ?thesis
unfolding abs_is_wff(2) by (simp only:)
next
case False
have "form_size D < form_size B"
unfolding abs_is_wff(2) by simp
have "is_free_for A (x, α) D"
using is_free_for_from_abs[OF less(4)[unfolded abs_is_wff(2)]] and ‹y⇘γ⇙ ≠ x⇘α⇙› by blast
have "⊢ (λx⇘α⇙. (λy⇘γ⇙. D)) · A =⇘β⇙ λy⇘γ⇙. ❙S {(x, α) ↣ A} D"
proof (cases "(y, γ) ∉ vars A")
case True
with ‹y⇘γ⇙ ≠ x⇘α⇙› have "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→δ⇙ λy⇘γ⇙. (λx⇘α⇙. D) · A"
using axiom_4_4[OF assms(1) abs_is_wff(3)] and axiom_is_derivable_from_no_hyps by auto
moreover have "⊢ (λx⇘α⇙. D) · A =⇘δ⇙ ❙S {(x, α) ↣ A} D"
by
(
fact less(1)
[OF ‹form_size D < form_size B› assms(1) ‹D ∈ wffs⇘δ⇙› ‹is_free_for A (x, α) D›]
)
ultimately show ?thesis
unfolding abs_is_wff(1) by (rule rule_R[where p = "[»,«]"]) force+
next
case False
have "finite (vars {A, D})"
using vars_form_finiteness and vars_form_set_finiteness by simp
then obtain z where "(z, γ) ∉ ({(x, α), (y, γ)} ∪ vars {A, D})"
using fresh_var_existence by (metis Un_insert_left finite.simps insert_is_Un)
then have "z⇘γ⇙ ≠ x⇘α⇙" and "z⇘γ⇙ ≠ y⇘γ⇙" and "(z, γ) ∉ vars {A, D}"
by simp_all
then show ?thesis
proof (cases "(x, α) ∉ free_vars D")
case True
define D' where "D' = ❙S {(y, γ) ↣ z⇘γ⇙} D"
have "is_substitution {(y, γ) ↣ z⇘γ⇙}"
by auto
with ‹D ∈ wffs⇘δ⇙› and D'_def have "D' ∈ wffs⇘δ⇙"
using substitution_preserves_typing by blast
then have "⊢ (λx⇘α⇙. λz⇘γ⇙. D') · A =⇘γ→δ⇙ λz⇘γ⇙. (λx⇘α⇙. D') · A"
using ‹z⇘γ⇙ ≠ x⇘α⇙› and ‹(z, γ) ∉ vars {A, D}› and axiom_4_4[OF assms(1)]
and axiom_is_derivable_from_no_hyps
by auto
moreover have "§2": "⊢ (λx⇘α⇙. D') · A =⇘δ⇙ D'"
proof -
have "form_size D' = form_size D"
unfolding D'_def by (fact renaming_substitution_preserves_form_size)
then have "form_size D' < form_size B"
using ‹form_size D < form_size B› by simp
moreover from ‹z⇘γ⇙ ≠ x⇘α⇙› have "is_free_for A (x, α) D'"
unfolding D'_def and is_free_for_def
using substitution_preserves_freeness[OF True] and is_free_at_in_free_vars
by fast
ultimately have "⊢ (λx⇘α⇙. D') · A =⇘δ⇙ ❙S {(x, α) ↣ A} D'"
using less(1) and assms(1) and ‹D' ∈ wffs⇘δ⇙› by simp
moreover from ‹z⇘γ⇙ ≠ x⇘α⇙› have "(x, α) ∉ free_vars D'"
unfolding D'_def using substitution_preserves_freeness[OF True] by fast
then have "❙S {(x, α) ↣ A} D' = D'"
by (fact free_var_singleton_substitution_neutrality)
ultimately show ?thesis
by (simp only:)
qed
ultimately have "§3": "⊢ (λx⇘α⇙. λz⇘γ⇙. D') · A =⇘γ→δ⇙ λz⇘γ⇙. D'" (is ‹⊢ ?A3›)
by (rule rule_R[where p = "[»,«]"]) force+
moreover have "§4": "⊢ (λy⇘γ⇙. D) =⇘γ→δ⇙ λz⇘γ⇙. D'"
proof -
have "(z, γ) ∉ free_vars D"
using ‹(z, γ) ∉ vars {A, D}› and free_vars_in_all_vars_set by auto
moreover have "is_free_for (z⇘γ⇙) (y, γ) D"
using ‹(z, γ) ∉ vars {A, D}› and absent_var_is_free_for by force
ultimately have "⊢ λy⇘γ⇙. D =⇘γ→δ⇙ λz⇘γ⇙. ❙S {(y, γ) ↣ z⇘γ⇙} D"
using "α"[OF ‹D ∈ wffs⇘δ⇙›] by fast
then show ?thesis
using D'_def by blast
qed
ultimately have "§5": "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→δ⇙ λy⇘γ⇙. D"
proof -
note rule_RR' = rule_RR[OF disjI2]
have "§5⇩1": "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→δ⇙ λz⇘γ⇙. D'" (is ‹⊢ ?A5⇩1›)
by (rule rule_RR'[OF "§4", where p = "[«,»,«,«]" and C = "?A3"]) (use "§3" in ‹force+›)
show ?thesis
by (rule rule_RR'[OF "§4", where p = "[»]" and C = "?A5⇩1"]) (use "§5⇩1" in ‹force+›)
qed
then show ?thesis
using free_var_singleton_substitution_neutrality[OF ‹(x, α) ∉ free_vars D›]
by (simp only: ‹β = γ→δ›)
next
case False
have "(y, γ) ∉ free_vars A"
proof (rule ccontr)
assume "¬ (y, γ) ∉ free_vars A"
moreover from ‹¬ (x, α) ∉ free_vars D› obtain p
where "p ∈ positions D" and "is_free_at (x, α) p D"
using free_vars_in_is_free_at by blast
then have "« # p ∈ positions (λy⇘γ⇙. D)" and "is_free_at (x, α) (« # p) (λy⇘γ⇙. D)"
using is_free_at_to_abs[OF ‹is_free_at (x, α) p D›] and ‹y⇘γ⇙ ≠ x⇘α⇙› by (simp, fast)
moreover have "in_scope_of_abs (y, γ) (« # p) (λy⇘γ⇙. D)"
by force
ultimately have "¬ is_free_for A (x, α) (λy⇘γ⇙. D)"
by blast
with ‹is_free_for A (x, α) B›[unfolded abs_is_wff(2)] show False
by contradiction
qed
define A' where "A' = rename_bound_var (y, γ) z A"
have "A' ∈ wffs⇘α⇙"
unfolding A'_def by (fact rename_bound_var_preserves_typing[OF assms(1)])
from ‹(z, γ) ∉ vars {A, D}› have "(y, γ) ∉ vars A'"
using
old_var_not_free_not_occurring_after_rename
[
OF assms(1) ‹z⇘γ⇙ ≠ y⇘γ⇙› ‹(y, γ) ∉ free_vars A›
]
unfolding A'_def by simp
from A'_def have "§6": "⊢ A =⇘α⇙ A'"
using bound_var_renaming_equality[OF assms(1) ‹z⇘γ⇙ ≠ y⇘γ⇙›] and ‹(z, γ) ∉ vars {A, D}›
by simp
moreover have "§7": "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A' =⇘γ→δ⇙ λy⇘γ⇙. (λx⇘α⇙. D) · A'" (is ‹⊢ ?A7›)
using axiom_4_4[OF ‹A' ∈ wffs⇘α⇙› ‹D ∈ wffs⇘δ⇙›]
and ‹(y, γ) ∉ vars A'› and ‹y⇘γ⇙ ≠ x⇘α⇙› and axiom_is_derivable_from_no_hyps
by auto
ultimately have "§8": "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→δ⇙ λy⇘γ⇙. (λx⇘α⇙. D) · A"
proof -
note rule_RR' = rule_RR[OF disjI2]
have "§8⇩1": "⊢ (λx⇘α⇙. λy⇘γ⇙. D) · A =⇘γ→δ⇙ λy⇘γ⇙. (λx⇘α⇙. D) · A'" (is ‹⊢ ?A8⇩1›)
by (rule rule_RR'[OF "§6", where p = "[«,»,»]" and C = "?A7"]) (use "§7" in ‹force+›)
show ?thesis
by (rule rule_RR'[OF "§6", where p = "[»,«,»]" and C = "?A8⇩1"]) (use "§8⇩1" in ‹force+›)
qed
moreover have "form_size D < form_size B"
unfolding abs_is_wff(2) by (simp only: form_size.simps(4) lessI)
with assms(1) have "§9": "⊢ (λx⇘α⇙. D) · A =⇘δ⇙ ❙S {(x, α) ↣ A} D"
using less(1) and ‹D ∈ wffs⇘δ⇙› and ‹is_free_for A (x, α) D› by (simp only:)
ultimately show ?thesis
unfolding ‹β = γ→δ› by (rule rule_R[where p = "[»,«]"]) force+
qed
qed
then show ?thesis
unfolding abs_is_wff(2) using False and singleton_substitution_simps(4) by simp
qed
qed
qed
end
subsection ‹Proposition 5208›
proposition prop_5208:
assumes "vs ≠ []" and "B ∈ wffs⇘β⇙"
shows "⊢ ·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ vs B) (map FVar vs) =⇘β⇙ B"
using assms(1) proof (induction vs rule: list_nonempty_induct)
case (single v)
obtain x and α where "v = (x, α)"
by fastforce
then have "·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ [v] B) (map FVar [v]) = (λx⇘α⇙. B) · x⇘α⇙"
by simp
moreover have "⊢ (λx⇘α⇙. B) · x⇘α⇙ =⇘β⇙ B"
proof -
have "is_free_for (x⇘α⇙) (x, α) B"
by fastforce
then have "⊢ (λx⇘α⇙. B) · x⇘α⇙ =⇘β⇙ ❙S {(x, α) ↣ x⇘α⇙} B"
by (rule prop_5207 [OF wffs_of_type_intros(1) assms(2)])
then show ?thesis
using identity_singleton_substitution_neutrality by (simp only:)
qed
ultimately show ?case
by (simp only:)
next
case (cons v vs)
obtain x and α where "v = (x, α)"
by fastforce
have "⊢ ·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ (v # vs) B) (map FVar (v # vs)) =⇘β⇙ ·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ vs B) (map FVar vs)"
proof -
have "·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ (v # vs) B) (map FVar (v # vs)) ∈ wffs⇘β⇙"
proof -
have "λ⇧𝒬⇩⋆ (v # vs) B ∈ wffs⇘foldr (→) (map snd (v # vs)) β⇙"
using generalized_abs_wff [OF assms(2)] by blast
moreover
have "∀k < length (map FVar (v # vs)). map FVar (v # vs) ! k ∈ wffs⇘map snd (v # vs) ! k⇙"
proof safe
fix k
assume *: "k < length (map FVar (v # vs))"
moreover obtain x and α where "(v # vs) ! k = (x, α)"
by fastforce
with * have "map FVar (v # vs) ! k = x⇘α⇙" and "map snd (v # vs) ! k = α"
by (metis length_map nth_map snd_conv)+
ultimately show "map FVar (v # vs) ! k ∈ wffs⇘map snd (v # vs) ! k⇙"
by fastforce
qed
ultimately show ?thesis
using generalized_app_wff[where As = "map FVar (v # vs)" and ts = "map snd (v # vs)"] by simp
qed
then have "
⊢ ·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ (v # vs) B) (map FVar (v # vs)) =⇘β⇙ ·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ (v # vs) B) (map FVar (v # vs))"
by (fact prop_5200)
then have "
⊢ ·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ (v # vs) B) (map FVar (v # vs)) =⇘β⇙ ·⇧𝒬⇩⋆ ((λ⇧𝒬⇩⋆ (v # vs) B) · FVar v) (map FVar vs)"
by simp
moreover have "⊢ (λ⇧𝒬⇩⋆ (v # vs) B) · FVar v =⇘foldr (→) (map snd vs) β⇙ (λ⇧𝒬⇩⋆ vs B)"
proof -
have "⊢ (λ⇧𝒬⇩⋆ (v # vs) B) · FVar v =⇘foldr (→) (map snd vs) β⇙ ❙S {v ↣ FVar v} (λ⇧𝒬⇩⋆ vs B)"
proof -
from ‹v = (x, α)› have "λ⇧𝒬⇩⋆ (v # vs) B = λx⇘α⇙. λ⇧𝒬⇩⋆ vs B"
by simp
have "λ⇧𝒬⇩⋆ vs B ∈ wffs⇘foldr (→) (map snd vs) β⇙"
using generalized_abs_wff[OF assms(2)] by blast
moreover have "is_free_for (x⇘α⇙) (x, α) (λ⇧𝒬⇩⋆ vs B)"
by fastforce
ultimately
have "⊢ (λx⇘α⇙. λ⇧𝒬⇩⋆ vs B) · x⇘α⇙ =⇘foldr (→) (map snd vs) β⇙ ❙S {(x, α) ↣ x⇘α⇙} λ⇧𝒬⇩⋆ vs B"
by (rule prop_5207 [OF wffs_of_type_intros(1)])
with ‹v = (x, α)› show ?thesis
by simp
qed
then show ?thesis
using identity_singleton_substitution_neutrality by (simp only:)
qed
ultimately show ?thesis
proof (induction rule: rule_R [where p = "[»] @ replicate (length vs) «"])
case occ_subform
then show ?case
unfolding equality_of_type_def using leftmost_subform_in_generalized_app
by (metis append_Cons append_Nil is_subform_at.simps(3) length_map)
next
case replacement
then show ?case
unfolding equality_of_type_def using leftmost_subform_in_generalized_app_replacement
and is_subform_implies_in_positions and leftmost_subform_in_generalized_app
by (metis append_Cons append_Nil length_map replace_right_app)
qed
qed
moreover have "⊢ ·⇧𝒬⇩⋆ (λ⇧𝒬⇩⋆ vs B) (map FVar vs) =⇘β⇙ B"
by (fact cons.IH)
ultimately show ?case
by (rule rule_R [where p = "[»]"]) auto
qed
subsection ‹Proposition 5209›
proposition prop_5209:
assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘β⇙" and "C ∈ wffs⇘β⇙"
and "⊢ B =⇘β⇙ C"
and "is_free_for A (x, α) (B =⇘β⇙ C)"
shows "⊢ ❙S {(x, α) ↣ A} (B =⇘β⇙ C)"
proof -
have "⊢ (λx⇘α⇙. B) · A =⇘β⇙ (λx⇘α⇙. B) · A"
proof -
have "(λx⇘α⇙. B) · A ∈ wffs⇘β⇙"
using assms(1,2) by blast
then show ?thesis
by (fact prop_5200)
qed
from this and assms(4) have "⊢ (λx⇘α⇙. B) · A =⇘β⇙ (λx⇘α⇙. C) · A"
by (rule rule_R [where p = "[»,«,«]"]) force+
moreover have "⊢ (λx⇘α⇙. B) · A =⇘β⇙ ❙S {(x, α) ↣ A} B"
proof -
from assms(5)[unfolded equality_of_type_def] have "is_free_for A (x, α) (Q⇘β⇙ · B)"
by (rule is_free_for_from_app)
then have "is_free_for A (x, α) B"
by (rule is_free_for_from_app)
with assms(1,2) show ?thesis
by (rule prop_5207)
qed
moreover have "⊢ (λx⇘α⇙. C) · A =⇘β⇙ ❙S {(x, α) ↣ A} C"
proof -
from assms(5)[unfolded equality_of_type_def] have "is_free_for A (x, α) C"
by (rule is_free_for_from_app)
with assms(1,3) show ?thesis
by (rule prop_5207)
qed
ultimately have "⊢ (❙S {(x, α) ↣ A} B) =⇘β⇙ (❙S {(x, α) ↣ A} C)"
using Equality_Rules(2,3) by blast
then show ?thesis
by simp
qed
subsection ‹Proposition 5210›
proposition prop_5210:
assumes "B ∈ wffs⇘β⇙"
shows "⊢ T⇘o⇙ =⇘o⇙ (B =⇘β⇙ B)"
proof -
have "§1": "
⊢
((λ𝔶⇘β⇙. 𝔶⇘β⇙) =⇘β→β⇙ (λ𝔶⇘β⇙. 𝔶⇘β⇙))
=⇘o⇙
∀𝔵⇘β⇙. ((λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙ =⇘β⇙ (λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙)"
proof -
have "⊢ (𝔣⇘β→β⇙ =⇘β→β⇙ 𝔤⇘β→β⇙) =⇘o⇙ ∀𝔵⇘β⇙. (𝔣⇘β→β⇙ · 𝔵⇘β⇙ =⇘β⇙ 𝔤⇘β→β⇙ · 𝔵⇘β⇙)" (is "⊢ ?B =⇘o⇙ ?C")
using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
moreover have "(λ𝔶⇘β⇙. 𝔶⇘β⇙) ∈ wffs⇘β→β⇙" and "?B ∈ wffs⇘o⇙" and "?C ∈ wffs⇘o⇙"
by auto
moreover have "is_free_for (λ𝔶⇘β⇙. 𝔶⇘β⇙) (𝔣, β→β) (?B =⇘o⇙ ?C)"
by simp
ultimately have "⊢ ❙S {(𝔣, β→β) ↣ (λ𝔶⇘β⇙. 𝔶⇘β⇙)} (?B =⇘o⇙ ?C)" (is "⊢ ?S")
using prop_5209 by presburger
moreover have "?S =
(
(λ𝔶⇘β⇙. 𝔶⇘β⇙) =⇘β→β⇙ 𝔤⇘β→β⇙) =⇘o⇙ ∀𝔵⇘β⇙. ((λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙ =⇘β⇙ 𝔤⇘β→β⇙ · 𝔵⇘β⇙
)" (is "_ = ?B' =⇘o⇙ ?C'")
by simp
ultimately have "⊢ ?B' =⇘o⇙ ?C'"
by (simp only:)
moreover from ‹(λ𝔶⇘β⇙. 𝔶⇘β⇙) ∈ wffs⇘β→β⇙› have "?B' ∈ wffs⇘o⇙" and "?C' ∈ wffs⇘o⇙"
by auto
moreover have "is_free_for (λ𝔶⇘β⇙. 𝔶⇘β⇙) (𝔤, β→β) (?B' =⇘o⇙ ?C')"
by simp
ultimately have "⊢ ❙S {(𝔤, β→β) ↣ (λ𝔶⇘β⇙. 𝔶⇘β⇙)} (?B' =⇘o⇙ ?C')" (is "⊢ ?S'")
using prop_5209[OF ‹(λ𝔶⇘β⇙. 𝔶⇘β⇙) ∈ wffs⇘β→β⇙›] by blast
then show ?thesis
by simp
qed
then have "⊢ (λ𝔵⇘β⇙. T⇘o⇙) =⇘β→o⇙ (λ𝔵⇘β⇙. (𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙))"
proof -
have "λ𝔶⇘β⇙. 𝔶⇘β⇙ ∈ wffs⇘β→β⇙"
by blast
then have "⊢ λ𝔶⇘β⇙. 𝔶⇘β⇙ =⇘β→β⇙ λ𝔶⇘β⇙. 𝔶⇘β⇙"
by (fact prop_5200)
with "§1" have "⊢ ∀𝔵⇘β⇙. ((λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙ =⇘β⇙ (λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙)"
using rule_R and is_subform_at.simps(1) by blast
moreover have "⊢ (λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙"
using axiom_4_2[OF wffs_of_type_intros(1)] by (rule axiom_is_derivable_from_no_hyps)
ultimately have "⊢ ∀𝔵⇘β⇙. (𝔵⇘β⇙ =⇘β⇙ (λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙)"
by (rule rule_R[where p = "[»,«,«,»]"]) auto
from this and ‹⊢ (λ𝔶⇘β⇙. 𝔶⇘β⇙) · 𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙› have "⊢ ∀𝔵⇘β⇙. (𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙)"
by (rule rule_R[where p = "[»,«,»]"]) auto
then show ?thesis
unfolding forall_def and PI_def by (fold equality_of_type_def)
qed
from this and assms have 3: "⊢ (λ𝔵⇘β⇙. T⇘o⇙) · B =⇘o⇙ (λ𝔵⇘β⇙. (𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙)) · B"
by (rule Equality_Rules(5))
then show ?thesis
proof -
have "⊢ (λ𝔵⇘β⇙. T⇘o⇙) · B =⇘o⇙ T⇘o⇙"
using prop_5207[OF assms true_wff] by fastforce
from 3 and this have "⊢ T⇘o⇙ =⇘o⇙ (λ𝔵⇘β⇙. (𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙)) · B"
by (rule rule_R[where p = "[«,»]"]) auto
moreover have "⊢ (λ𝔵⇘β⇙. (𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙)) · B =⇘o⇙ (B =⇘β⇙ B)"
proof -
have "𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙ ∈ wffs⇘o⇙" and "is_free_for B (𝔵, β) (𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙)"
by (blast, intro is_free_for_in_equality is_free_for_in_var)
moreover have "❙S {(𝔵, β) ↣ B} (𝔵⇘β⇙ =⇘β⇙ 𝔵⇘β⇙) = (B =⇘β⇙ B)"
by simp
ultimately show ?thesis
using prop_5207[OF assms] by metis
qed
ultimately show ?thesis
by (rule rule_R [where p = "[»]"]) auto
qed
qed
subsection ‹Proposition 5211›
proposition prop_5211:
shows "⊢ (T⇘o⇙ ∧⇧𝒬 T⇘o⇙) =⇘o⇙ T⇘o⇙"
proof -
have const_T_wff: "(λx⇘o⇙. T⇘o⇙) ∈ wffs⇘o→o⇙" for x
by blast
have "§1": "⊢ (λ𝔶⇘o⇙. T⇘o⇙) · T⇘o⇙ ∧⇧𝒬 (λ𝔶⇘o⇙. T⇘o⇙) · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. (λ𝔶⇘o⇙. T⇘o⇙) · 𝔵⇘o⇙"
proof -
have "⊢ 𝔤⇘o→o⇙ · T⇘o⇙ ∧⇧𝒬 𝔤⇘o→o⇙ · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙" (is "⊢ ?B =⇘o⇙ ?C")
using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
moreover have "?B ∈ wffs⇘o⇙" and "?C ∈ wffs⇘o⇙"
by auto
moreover have "is_free_for (λ𝔶⇘o⇙. T⇘o⇙) (𝔤, o→o) (?B =⇘o⇙ ?C)"
by simp
ultimately have "⊢ ❙S {(𝔤, o→o) ↣ (λ𝔶⇘o⇙. T⇘o⇙)} (?B =⇘o⇙ ?C)"
using const_T_wff and prop_5209 by presburger
then show ?thesis
by simp
qed
then have "⊢ T⇘o⇙ ∧⇧𝒬 T⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. T⇘o⇙"
proof -
have T_β_redex: "⊢ (λ𝔶⇘o⇙. T⇘o⇙) · A =⇘o⇙ T⇘o⇙" if "A ∈ wffs⇘o⇙" for A
using that and prop_5207[OF that true_wff] by fastforce
from "§1" and T_β_redex[OF true_wff]
have "⊢ T⇘o⇙ ∧⇧𝒬 (λ𝔶⇘o⇙. T⇘o⇙) · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. (λ𝔶⇘o⇙. T⇘o⇙) · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,«,»]"]) force+
from this and T_β_redex[OF false_wff] have "⊢ T⇘o⇙ ∧⇧𝒬 T⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. (λ𝔶⇘o⇙. T⇘o⇙) · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,»]"]) force+
from this and T_β_redex[OF wffs_of_type_intros(1)] show ?thesis
by (rule rule_R[where p = "[»,»,«]"]) force+
qed
moreover have "⊢ T⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. T⇘o⇙"
using prop_5210[OF const_T_wff] by simp
ultimately show ?thesis
using Equality_Rules(2,3) by blast
qed
lemma true_is_derivable:
shows "⊢ T⇘o⇙"
unfolding true_def using Q_wff by (rule prop_5200)
subsection ‹Proposition 5212›
proposition prop_5212:
shows "⊢ T⇘o⇙ ∧⇧𝒬 T⇘o⇙"
proof -
have "⊢ T⇘o⇙"
by (fact true_is_derivable)
moreover have "⊢ (T⇘o⇙ ∧⇧𝒬 T⇘o⇙) =⇘o⇙ T⇘o⇙"
by (fact prop_5211)
then have "⊢ T⇘o⇙ ≡⇧𝒬 (T⇘o⇙ ∧⇧𝒬 T⇘o⇙)"
unfolding equivalence_def by (fact Equality_Rules(2))
ultimately show ?thesis
by (rule Equality_Rules(1))
qed
subsection ‹Proposition 5213›
proposition prop_5213:
assumes "⊢ A =⇘α⇙ B" and "⊢ C =⇘β⇙ D"
shows "⊢ (A =⇘α⇙ B) ∧⇧𝒬 (C =⇘β⇙ D)"
proof -
from assms have "A ∈ wffs⇘α⇙" and "C ∈ wffs⇘β⇙"
using hyp_derivable_form_is_wffso and wffs_from_equality by blast+
have "⊢ T⇘o⇙ =⇘o⇙ (A =⇘α⇙ A)"
by (fact prop_5210[OF ‹A ∈ wffs⇘α⇙›])
moreover have "⊢ A =⇘α⇙ B"
by fact
ultimately have "⊢ T⇘o⇙ =⇘o⇙ (A =⇘α⇙ B)"
by (rule rule_R[where p = "[»,»]"]) force+
have "⊢ T⇘o⇙ =⇘o⇙ (C =⇘β⇙ C)"
by (fact prop_5210[OF ‹C ∈ wffs⇘β⇙›])
moreover have "⊢ C =⇘β⇙ D"
by fact
ultimately have "⊢ T⇘o⇙ =⇘o⇙ (C =⇘β⇙ D)"
by (rule rule_R[where p = "[»,»]"]) force+
then show ?thesis
proof -
have "⊢ T⇘o⇙ ∧⇧𝒬 T⇘o⇙"
by (fact prop_5212)
from this and ‹⊢ T⇘o⇙ =⇘o⇙ (A =⇘α⇙ B)› have "⊢ (A =⇘α⇙ B) ∧⇧𝒬 T⇘o⇙"
by (rule rule_R[where p = "[«,»]"]) force+
from this and ‹⊢ T⇘o⇙ =⇘o⇙ (C =⇘β⇙ D)› show ?thesis
by (rule rule_R[where p = "[»]"]) force+
qed
qed
subsection ‹Proposition 5214›
proposition prop_5214:
shows "⊢ T⇘o⇙ ∧⇧𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙"
proof -
have id_on_o_is_wff: "(λ𝔵⇘o⇙. 𝔵⇘o⇙) ∈ wffs⇘o→o⇙"
by blast
have "§1": "⊢ (λ𝔵⇘o⇙. 𝔵⇘o⇙) · T⇘o⇙ ∧⇧𝒬 (λ𝔵⇘o⇙. 𝔵⇘o⇙) · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. (λ𝔵⇘o⇙. 𝔵⇘o⇙) · 𝔵⇘o⇙"
proof -
have "⊢ 𝔤⇘o→o⇙ · T⇘o⇙ ∧⇧𝒬 𝔤⇘o→o⇙ · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙" (is "⊢ ?B =⇘o⇙ ?C")
using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
moreover have "?B ∈ wffs⇘o⇙" and "?C ∈ wffs⇘o⇙" and "is_free_for (λ𝔵⇘o⇙. 𝔵⇘o⇙) (𝔤, o→o) (?B =⇘o⇙ ?C)"
by auto
ultimately have "⊢ ❙S {(𝔤, o→o) ↣ (λ𝔵⇘o⇙. 𝔵⇘o⇙)} (?B =⇘o⇙ ?C)"
using id_on_o_is_wff and prop_5209 by presburger
then show ?thesis
by simp
qed
then have "⊢ T⇘o⇙ ∧⇧𝒬 F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. 𝔵⇘o⇙"
proof -
have id_β_redex: "⊢ (λ𝔵⇘o⇙. 𝔵⇘o⇙) · A =⇘o⇙ A" if "A ∈ wffs⇘o⇙" for A
by (fact axiom_is_derivable_from_no_hyps[OF axiom_4_2[OF that]])
from "§1" and id_β_redex[OF true_wff]
have "⊢ T⇘o⇙ ∧⇧𝒬 (λ𝔵⇘o⇙. 𝔵⇘o⇙) · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. (λ𝔵⇘o⇙. 𝔵⇘o⇙) · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,«,»]"]) force+
from this and id_β_redex[OF false_wff] have "⊢ T⇘o⇙ ∧⇧𝒬 F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. (λ𝔵⇘o⇙. 𝔵⇘o⇙) · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,»]"]) force+
from this and id_β_redex[OF wffs_of_type_intros(1)] show ?thesis
by (rule rule_R[where p = "[»,»,«]"]) force+
qed
then show ?thesis
by simp
qed
subsection ‹Proposition 5215 (Universal Instantiation)›
proposition prop_5215:
assumes "ℋ ⊢ ∀x⇘α⇙. B" and "A ∈ wffs⇘α⇙"
and "is_free_for A (x, α) B"
shows "ℋ ⊢ ❙S {(x, α) ↣ A} B"
proof -
from assms(1) have "is_hyps ℋ"
by (blast elim: is_derivable_from_hyps.cases)
from assms(1) have "ℋ ⊢ (λ𝔵⇘α⇙. T⇘o⇙) =⇘α→o⇙ (λx⇘α⇙. B)"
by simp
with assms(2) have "ℋ ⊢ (λ𝔵⇘α⇙. T⇘o⇙) · A =⇘o⇙ (λx⇘α⇙. B) · A"
by (intro Equality_Rules(5))
then have "ℋ ⊢ T⇘o⇙ =⇘o⇙ ❙S {(x, α) ↣ A} B"
proof -
have "ℋ ⊢ (λ𝔵⇘α⇙. T⇘o⇙) · A =⇘o⇙ T⇘o⇙"
proof -
have "⊢ (λ𝔵⇘α⇙. T⇘o⇙) · A =⇘o⇙ T⇘o⇙"
using prop_5207[OF assms(2) true_wff is_free_for_in_true] and derived_substitution_simps(1)
by (simp only:)
from this and ‹is_hyps ℋ› show ?thesis
by (rule derivability_implies_hyp_derivability)
qed
moreover have "ℋ ⊢ (λx⇘α⇙. B) · A =⇘o⇙ ❙S {(x, α) ↣ A} B"
proof -
have "B ∈ wffs⇘o⇙"
using hyp_derivable_form_is_wffso[OF assms(1)] by (fastforce elim: wffs_from_forall)
with assms(2,3) have "⊢ (λx⇘α⇙. B) · A =⇘o⇙ ❙S {(x, α) ↣ A} B"
using prop_5207 by (simp only:)
from this and ‹is_hyps ℋ› show ?thesis
by (rule derivability_implies_hyp_derivability)
qed
ultimately show ?thesis
using ‹ℋ ⊢ (λ𝔵⇘α⇙. T⇘o⇙) · A =⇘o⇙ (λx⇘α⇙. B) · A› and Equality_Rules(2,3) by meson
qed
then show ?thesis
proof -
have "ℋ ⊢ T⇘o⇙"
by (fact derivability_implies_hyp_derivability[OF true_is_derivable ‹is_hyps ℋ›])
from this and ‹ℋ ⊢ T⇘o⇙ =⇘o⇙ ❙S {(x, α) ↣ A} B› show ?thesis
by (rule Equality_Rules(1)[unfolded equivalence_def])
qed
qed
lemmas "∀I" = prop_5215
subsection ‹Proposition 5216›
proposition prop_5216:
assumes "A ∈ wffs⇘o⇙"
shows "⊢ (T⇘o⇙ ∧⇧𝒬 A) =⇘o⇙ A"
proof -
let ?B = "λ𝔵⇘o⇙. (T⇘o⇙ ∧⇧𝒬 𝔵⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)"
have B_is_wff: "?B ∈ wffs⇘o→o⇙"
by auto
have "§1": "⊢ ?B · T⇘o⇙ ∧⇧𝒬 ?B · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. ?B · 𝔵⇘o⇙"
proof -
have "⊢ 𝔤⇘o→o⇙ · T⇘o⇙ ∧⇧𝒬 𝔤⇘o→o⇙ · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙" (is "⊢ ?C =⇘o⇙ ?D")
using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
moreover have "?C ∈ wffs⇘o⇙" and "?D ∈ wffs⇘o⇙" and "is_free_for ?B (𝔤, o→o) (?C =⇘o⇙ ?D)"
by auto
ultimately have "⊢ ❙S {(𝔤, o→o) ↣ ?B} (?C =⇘o⇙ ?D)"
using B_is_wff and prop_5209 by presburger
then show ?thesis
by simp
qed
have *: "is_free_for A (𝔵, o) (T⇘o⇙ ∧⇧𝒬 𝔵⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)" for A
by (intro is_free_for_in_conj is_free_for_in_equality is_free_for_in_true is_free_for_in_var)
have "⊢ (T⇘o⇙ ∧⇧𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) ∧⇧𝒬 (T⇘o⇙ ∧⇧𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙)"
by (fact prop_5213[OF prop_5211 prop_5214])
moreover
have "⊢ (T⇘o⇙ ∧⇧𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) ∧⇧𝒬 (T⇘o⇙ ∧⇧𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ ∀𝔵⇘o⇙. (T⇘o⇙ ∧⇧𝒬 𝔵⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)"
proof -
have B_β_redex: "⊢ ?B · A =⇘o⇙ (T⇘o⇙ ∧⇧𝒬 A =⇘o⇙ A)" if "A ∈ wffs⇘o⇙" for A
proof -
have "T⇘o⇙ ∧⇧𝒬 𝔵⇘o⇙ =⇘o⇙ 𝔵⇘o⇙ ∈ wffs⇘o⇙"
by blast
moreover have "❙S {(𝔵, o) ↣ A} (T⇘o⇙ ∧⇧𝒬 𝔵⇘o⇙ =⇘o⇙ 𝔵⇘o⇙) = (T⇘o⇙ ∧⇧𝒬 A =⇘o⇙ A)"
by simp
ultimately show ?thesis
using * and prop_5207[OF that] by metis
qed
from "§1" and B_β_redex[OF true_wff]
have "⊢ (T⇘o⇙ ∧⇧𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) ∧⇧𝒬 ?B · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. ?B · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,«,»]"]) force+
from this and B_β_redex[OF false_wff]
have "⊢ (T⇘o⇙ ∧⇧𝒬 T⇘o⇙ =⇘o⇙ T⇘o⇙) ∧⇧𝒬 (T⇘o⇙ ∧⇧𝒬 F⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ ∀𝔵⇘o⇙. ?B · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,»]"]) force+
from this and B_β_redex[OF wffs_of_type_intros(1)] show ?thesis
by (rule rule_R[where p = "[»,»,«]"]) force+
qed
ultimately have "⊢ ∀𝔵⇘o⇙. (T⇘o⇙ ∧⇧𝒬 𝔵⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)"
by (rule rule_R[where p = "[]"]) fastforce+
show ?thesis
using "∀I"[OF ‹⊢ ∀𝔵⇘o⇙. (T⇘o⇙ ∧⇧𝒬 𝔵⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)› assms *] by simp
qed
subsection ‹Proposition 5217›
proposition prop_5217:
shows "⊢ (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ F⇘o⇙"
proof -
let ?B = "λ𝔵⇘o⇙. (T⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)"
have B_is_wff: "?B ∈ wffs⇘o→o⇙"
by auto
have *: "is_free_for A (𝔵, o) (T⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)" for A
by (intro is_free_for_in_equality is_free_for_in_true is_free_for_in_var)
have "§1": "⊢ ?B · T⇘o⇙ ∧⇧𝒬 ?B · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. ?B · 𝔵⇘o⇙"
proof -
have "⊢ 𝔤⇘o→o⇙ · T⇘o⇙ ∧⇧𝒬 𝔤⇘o→o⇙ · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙" (is "⊢ ?C =⇘o⇙ ?D")
using axiom_1[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
moreover have "?C ∈ wffs⇘o⇙" and "?D ∈ wffs⇘o⇙" and "is_free_for ?B (𝔤, o→o) (?C =⇘o⇙ ?D)"
by auto
ultimately have "⊢ ❙S {(𝔤, o→o) ↣ ?B} (?C =⇘o⇙ ?D)"
using B_is_wff and prop_5209 by presburger
then show ?thesis
by simp
qed
then have "⊢ (T⇘o⇙ =⇘o⇙ T⇘o⇙) ∧⇧𝒬 (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ ∀𝔵⇘o⇙. (T⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)" (is "⊢ ?A")
proof -
have B_β_redex: "⊢ ?B · A =⇘o⇙ (T⇘o⇙ =⇘o⇙ A)" if "A ∈ wffs⇘o⇙" for A
proof -
have "T⇘o⇙ =⇘o⇙ 𝔵⇘o⇙ ∈ wffs⇘o⇙"
by auto
moreover have "❙S {(𝔵, o) ↣ A} (T⇘o⇙ =⇘o⇙ 𝔵⇘o⇙) = (T⇘o⇙ =⇘o⇙ A)"
by simp
ultimately show ?thesis
using * and prop_5207[OF that] by metis
qed
from "§1" and B_β_redex[OF true_wff] have "⊢ (T⇘o⇙ =⇘o⇙ T⇘o⇙) ∧⇧𝒬 ?B · F⇘o⇙ =⇘o⇙ ∀𝔵⇘o⇙. ?B · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,«,»]"]) force+
from this and B_β_redex[OF false_wff]
have "⊢ (T⇘o⇙ =⇘o⇙ T⇘o⇙) ∧⇧𝒬 (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ ∀𝔵⇘o⇙. ?B · 𝔵⇘o⇙"
by (rule rule_R[where p = "[«,»,»]"]) force+
from this and B_β_redex[OF wffs_of_type_intros(1)] show ?thesis
by (rule rule_R[where p = "[»,»,«]"]) force+
qed
from prop_5210[OF true_wff] have "⊢ T⇘o⇙ ∧⇧𝒬 (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ ∀𝔵⇘o⇙. (T⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)"
by (rule rule_RR[OF disjI2, where p = "[«,»,«,»]" and C = ?A]) (force+, fact)
from this and prop_5216[where A = "T⇘o⇙ =⇘o⇙ F⇘o⇙"]
have "⊢ (T⇘o⇙ =⇘o⇙ F⇘o⇙) =⇘o⇙ ∀𝔵⇘o⇙. (T⇘o⇙ =⇘o⇙ 𝔵⇘o⇙)"
by (rule rule_R [where p = "[«,»]"]) force+
moreover have "§5": "
⊢ ((λ𝔵⇘o⇙. T⇘o⇙) =⇘o→o⇙ (λ𝔵⇘o⇙. 𝔵⇘o⇙)) =⇘o⇙ ∀𝔵⇘o⇙. ((λ𝔵⇘o⇙. T⇘o⇙) · 𝔵⇘o⇙ =⇘o⇙ (λ𝔵⇘o⇙. 𝔵⇘o⇙) · 𝔵⇘o⇙)"
proof -
have "⊢ (𝔣⇘o→o⇙ =⇘o→o⇙ 𝔤⇘o→o⇙) =⇘o⇙ ∀𝔵⇘o⇙. (𝔣⇘o→o⇙ · 𝔵⇘o⇙ =⇘o⇙ 𝔤⇘o→o⇙ · 𝔵⇘o⇙)" (is "⊢ ?C =⇘o⇙ ?D")
using axiom_3[unfolded equivalence_def] by (rule axiom_is_derivable_from_no_hyps)
moreover have "is_free_for ((λ𝔵⇘o⇙. T⇘o⇙)) (𝔣, o→o) (?C =⇘o⇙ ?D)"
by fastforce
moreover have "(λ𝔵⇘o⇙. T⇘o⇙) ∈ wffs⇘o→o⇙" and "?C ∈ wffs⇘o⇙" and "?D ∈ wffs⇘o⇙"
by auto
ultimately have "⊢ ❙S {(𝔣, o→o) ↣ (λ𝔵⇘o⇙. T⇘o⇙)} (?C =⇘o⇙ ?D)"
using prop_5209 by presburger
then have "⊢ ((λ𝔵⇘o⇙. T⇘o⇙) =⇘o→o⇙ 𝔤⇘o→o⇙) =⇘o⇙ ∀𝔵⇘o⇙. ((λ𝔵⇘o⇙. T⇘o⇙) · 𝔵⇘o⇙ =⇘o⇙ 𝔤⇘o→o⇙ · 𝔵⇘o⇙)"
(is "⊢ ?C' =⇘o⇙ ?D'")
by simp
moreover have "is_free_for ((λ𝔵⇘o⇙. 𝔵⇘o⇙)) (𝔤, o→o) (?C' =⇘o⇙ ?D')"
by fastforce
moreover have "(λ𝔵⇘o⇙. 𝔵⇘o⇙) ∈ wffs⇘o→o⇙" and "?C' ∈ wffs⇘o⇙" and "?D' ∈ wffs⇘o⇙"
using ‹(λ𝔵⇘o⇙. T⇘o⇙) ∈ wffs⇘o→o⇙› by auto
ultimately have "⊢ ❙S {(𝔤, o→o) ↣ (λ𝔵⇘o⇙. 𝔵⇘o⇙)} (?C' =⇘o⇙ ?D')"
using prop_5209 by presburger
then show ?thesis
by simp
qed
then have "⊢ F⇘o⇙ =⇘o⇙ ∀𝔵⇘