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 (* synonym *) 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 (* synonym *) 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 (* synonym *) 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⇙ ∀𝔵⇘