section ‹Proof System› theory Proof_System imports Syntax begin subsection ‹Axioms› inductive_set axioms :: "form set" where axiom_1: "𝔤⇘o→o⇙ · T⇘_{o}⇙ ∧⇧^{𝒬}𝔤⇘o→o⇙ · F⇘_{o}⇙ ≡⇧^{𝒬}∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙ ∈ axioms" | axiom_2: "(𝔵⇘α⇙ =⇘α⇙ 𝔶⇘α⇙) ⊃⇧^{𝒬}(𝔥⇘α→o⇙ · 𝔵⇘α⇙ ≡⇧^{𝒬}𝔥⇘α→o⇙ · 𝔶⇘α⇙) ∈ axioms" | axiom_3: "(𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) ≡⇧^{𝒬}∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙) ∈ axioms" | axiom_4_1_con: "(λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙ ∈ axioms" if "A ∈ wffs⇘α⇙" | axiom_4_1_var: "(λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙ ∈ axioms" if "A ∈ wffs⇘α⇙" and "y⇘β⇙ ≠ x⇘α⇙" | axiom_4_2: "(λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A ∈ axioms" if "A ∈ wffs⇘α⇙" | axiom_4_3: "(λx⇘α⇙. B · C) · A =⇘β⇙ ((λx⇘α⇙. B) · A) · ((λx⇘α⇙. C) · A) ∈ axioms" if "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘γ→β⇙" and "C ∈ wffs⇘γ⇙" | axiom_4_4: "(λx⇘α⇙. λy⇘γ⇙. B) · A =⇘γ→δ⇙ (λy⇘γ⇙. (λx⇘α⇙. B) · A) ∈ axioms" if "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘δ⇙" and "(y, γ) ∉ {(x, α)} ∪ vars A" | axiom_4_5: "(λx⇘α⇙. λx⇘α⇙. B) · A =⇘α→δ⇙ (λx⇘α⇙. B) ∈ axioms" if "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘δ⇙" | axiom_5: "ι · (Q⇘i⇙ · 𝔶⇘i⇙) =⇘i⇙ 𝔶⇘i⇙ ∈ axioms" lemma axioms_are_wffs_of_type_o: shows "axioms ⊆ wffs⇘o⇙" by (intro subsetI, cases rule: axioms.cases) auto subsection ‹Inference rule R› definition is_rule_R_app :: "position ⇒ form ⇒ form ⇒ form ⇒ bool" where [iff]: "is_rule_R_app p D C E ⟷ ( ∃α A B. E = A =⇘α⇙ B ∧ A ∈ wffs⇘α⇙ ∧ B ∈ wffs⇘α⇙ ∧ ― ‹\<^term>‹E› is a well-formed equality› A ≼⇘p⇙ C ∧ D ∈ wffs⇘o⇙ ∧ C⦉p ← B⦊ ⊳ D )" lemma rule_R_original_form_is_wffo: assumes "is_rule_R_app p D C E" shows "C ∈ wffs⇘o⇙" using assms and replacement_preserves_typing by fastforce subsection ‹Proof and derivability› inductive is_derivable :: "form ⇒ bool" where dv_axiom: "is_derivable A" if "A ∈ axioms" | dv_rule_R: "is_derivable D" if "is_derivable C" and "is_derivable E" and "is_rule_R_app p D C E" lemma derivable_form_is_wffso: assumes "is_derivable A" shows "A ∈ wffs⇘o⇙" using assms and axioms_are_wffs_of_type_o by (fastforce elim: is_derivable.cases) definition is_proof_step :: "form list ⇒ nat ⇒ bool" where [iff]: "is_proof_step 𝒮 i' ⟷ 𝒮 ! i' ∈ axioms ∨ (∃p j k. {j, k} ⊆ {0..<i'} ∧ is_rule_R_app p (𝒮 ! i') (𝒮 ! j) (𝒮 ! k))" definition is_proof :: "form list ⇒ bool" where [iff]: "is_proof 𝒮 ⟷ (∀i' < length 𝒮. is_proof_step 𝒮 i')" lemma common_prefix_is_subproof: assumes "is_proof (𝒮 @ 𝒮⇩_{1})" and "i' < length 𝒮" shows "is_proof_step (𝒮 @ 𝒮⇩_{2}) i'" proof - from assms(2) have *: "(𝒮 @ 𝒮⇩_{1}) ! i' = (𝒮 @ 𝒮⇩_{2}) ! i'" by (simp add: nth_append) moreover from assms(2) have "i' < length (𝒮 @ 𝒮⇩_{1})" by simp ultimately obtain p and j and k where **: "(𝒮 @ 𝒮⇩_{1}) ! i' ∈ axioms ∨ {j, k} ⊆ {0..<i'} ∧ is_rule_R_app p ((𝒮 @ 𝒮⇩_{1}) ! i') ((𝒮 @ 𝒮⇩_{1}) ! j) ((𝒮 @ 𝒮⇩_{1}) ! k)" using assms(1) by fastforce then consider (axiom) "(𝒮 @ 𝒮⇩_{1}) ! i' ∈ axioms" | (rule_R) "{j, k} ⊆ {0..<i'} ∧ is_rule_R_app p ((𝒮 @ 𝒮⇩_{1}) ! i') ((𝒮 @ 𝒮⇩_{1}) ! j) ((𝒮 @ 𝒮⇩_{1}) ! k)" by blast then have " (𝒮 @ 𝒮⇩_{2}) ! i' ∈ axioms ∨ ({j, k} ⊆ {0..<i'} ∧ is_rule_R_app p ((𝒮 @ 𝒮⇩_{2}) ! i') ((𝒮 @ 𝒮⇩_{2}) ! j) ((𝒮 @ 𝒮⇩_{2}) ! k))" proof cases case axiom with * have "(𝒮 @ 𝒮⇩_{2}) ! i' ∈ axioms" by (simp only:) then show ?thesis .. next case rule_R with assms(2) have "(𝒮 @ 𝒮⇩_{1}) ! j = (𝒮 @ 𝒮⇩_{2}) ! j" and "(𝒮 @ 𝒮⇩_{1}) ! k = (𝒮 @ 𝒮⇩_{2}) ! k" by (simp_all add: nth_append) then have "{j, k} ⊆ {0..<i'} ∧ is_rule_R_app p ((𝒮 @ 𝒮⇩_{2}) ! i') ((𝒮 @ 𝒮⇩_{2}) ! j) ((𝒮 @ 𝒮⇩_{2}) ! k)" using * and rule_R by simp then show ?thesis .. qed with ** show ?thesis by fastforce qed lemma added_suffix_proof_preservation: assumes "is_proof 𝒮" and "i' < length (𝒮 @ 𝒮') - length 𝒮'" shows "is_proof_step (𝒮 @ 𝒮') i'" using assms and common_prefix_is_subproof[where 𝒮⇩_{1}= "[]"] by simp lemma append_proof_step_is_proof: assumes "is_proof 𝒮" and "is_proof_step (𝒮 @ [A]) (length (𝒮 @ [A]) - 1)" shows "is_proof (𝒮 @ [A])" using assms and added_suffix_proof_preservation by (simp add: All_less_Suc) lemma added_prefix_proof_preservation: assumes "is_proof 𝒮'" and "i' ∈ {length 𝒮..<length (𝒮 @ 𝒮')}" shows "is_proof_step (𝒮 @ 𝒮') i'" proof - let ?𝒮 = "𝒮 @ 𝒮'" let ?i = "i' - length 𝒮" from assms(2) have "?𝒮 ! i' = 𝒮' ! ?i" and "?i < length 𝒮'" by (simp_all add: nth_append less_diff_conv2) then have "is_proof_step ?𝒮 i' = is_proof_step 𝒮' ?i" proof - from assms(1) and ‹?i < length 𝒮'› obtain j and k and p where *: "𝒮' ! ?i ∈ axioms ∨ ({j, k} ⊆ {0..<?i} ∧ is_rule_R_app p (𝒮' ! ?i) (𝒮' ! j) (𝒮' ! k))" by fastforce then consider (axiom) "𝒮' ! ?i ∈ axioms" | (rule_R) "{j, k} ⊆ {0..<?i} ∧ is_rule_R_app p (𝒮' ! ?i) (𝒮' ! j) (𝒮' ! k)" by blast then have " ?𝒮 ! i' ∈ axioms ∨ ( {j + length 𝒮, k + length 𝒮} ⊆ {0..<i'} ∧ is_rule_R_app p (?𝒮 ! i') (?𝒮 ! (j + length 𝒮)) (?𝒮 ! (k + length 𝒮)) )" proof cases case axiom with ‹?𝒮 ! i' = 𝒮' ! ?i› have "?𝒮 ! i' ∈ axioms" by (simp only:) then show ?thesis .. next case rule_R with assms(2) have "?𝒮 ! (j + length 𝒮) = 𝒮' ! j" and "?𝒮 ! (k + length 𝒮) = 𝒮' ! k" by (simp_all add: nth_append) with ‹?𝒮 ! i' = 𝒮' ! ?i› and rule_R have " {j + length 𝒮, k + length 𝒮} ⊆ {0..<i'} ∧ is_rule_R_app p (?𝒮 ! i') (?𝒮 ! (j + length 𝒮)) (?𝒮 ! (k + length 𝒮))" by auto then show ?thesis .. qed with * show ?thesis by fastforce qed with assms(1) and ‹?i < length 𝒮'› show ?thesis by simp qed lemma proof_but_last_is_proof: assumes "is_proof (𝒮 @ [A])" shows "is_proof 𝒮" using assms and common_prefix_is_subproof[where 𝒮⇩_{1}= "[A]" and 𝒮⇩_{2}= "[]"] by simp lemma proof_prefix_is_proof: assumes "is_proof (𝒮⇩_{1}@ 𝒮⇩_{2})" shows "is_proof 𝒮⇩_{1}" using assms and proof_but_last_is_proof by (induction 𝒮⇩_{2}arbitrary: 𝒮⇩_{1}rule: rev_induct) (simp, metis append.assoc) lemma single_axiom_is_proof: assumes "A ∈ axioms" shows "is_proof [A]" using assms by fastforce lemma proofs_concatenation_is_proof: assumes "is_proof 𝒮⇩_{1}" and "is_proof 𝒮⇩_{2}" shows "is_proof (𝒮⇩_{1}@ 𝒮⇩_{2})" proof - from assms(1) have "∀i' < length 𝒮⇩_{1}. is_proof_step (𝒮⇩_{1}@ 𝒮⇩_{2}) i'" using added_suffix_proof_preservation by auto moreover from assms(2) have "∀i' ∈ {length 𝒮⇩_{1}..<length (𝒮⇩_{1}@ 𝒮⇩_{2})}. is_proof_step (𝒮⇩_{1}@ 𝒮⇩_{2}) i'" using added_prefix_proof_preservation by auto ultimately show ?thesis unfolding is_proof_def by (meson atLeastLessThan_iff linorder_not_le) qed lemma elem_of_proof_is_wffo: assumes "is_proof 𝒮" and "A ∈ lset 𝒮" shows "A ∈ wffs⇘o⇙" using assms and axioms_are_wffs_of_type_o unfolding is_rule_R_app_def and is_proof_step_def and is_proof_def by (induction 𝒮) (simp, metis (full_types) in_mono in_set_conv_nth) lemma axiom_prepended_to_proof_is_proof: assumes "is_proof 𝒮" and "A ∈ axioms" shows "is_proof ([A] @ 𝒮)" using proofs_concatenation_is_proof[OF single_axiom_is_proof[OF assms(2)] assms(1)] . lemma axiom_appended_to_proof_is_proof: assumes "is_proof 𝒮" and "A ∈ axioms" shows "is_proof (𝒮 @ [A])" using proofs_concatenation_is_proof[OF assms(1) single_axiom_is_proof[OF assms(2)]] . lemma rule_R_app_appended_to_proof_is_proof: assumes "is_proof 𝒮" and "i⇩_{C}< length 𝒮" and "𝒮 ! i⇩_{C}= C" and "i⇩_{E}< length 𝒮" and "𝒮 ! i⇩_{E}= E" and "is_rule_R_app p D C E" shows "is_proof (𝒮 @ [D])" proof - let ?𝒮 = "𝒮 @ [D]" let ?i⇩_{D}= "length 𝒮" from assms(2,4) have "i⇩_{C}< ?i⇩_{D}" and "i⇩_{E}< ?i⇩_{D}" by fastforce+ with assms(3,5,6) have "is_rule_R_app p (?𝒮 ! ?i⇩_{D}) (?𝒮 ! i⇩_{C}) (?𝒮 ! i⇩_{E})" by (simp add: nth_append) with assms(2,4) have "∃p j k. {j, k} ⊆ {0..<?i⇩_{D}} ∧ is_rule_R_app p (?𝒮 ! ?i⇩_{D}) (?𝒮 ! j) (?𝒮 ! k)" by fastforce then have "is_proof_step ?𝒮 (length ?𝒮 - 1)" by simp moreover from assms(1) have "∀i' < length ?𝒮 - 1. is_proof_step ?𝒮 i'" using added_suffix_proof_preservation by auto ultimately show ?thesis using less_Suc_eq by auto qed definition is_proof_of :: "form list ⇒ form ⇒ bool" where [iff]: "is_proof_of 𝒮 A ⟷ 𝒮 ≠ [] ∧ is_proof 𝒮 ∧ last 𝒮 = A" lemma proof_prefix_is_proof_of_last: assumes "is_proof (𝒮 @ 𝒮')" and "𝒮 ≠ []" shows "is_proof_of 𝒮 (last 𝒮)" proof - from assms(1) have "is_proof 𝒮" by (fact proof_prefix_is_proof) with assms(2) show ?thesis by fastforce qed definition is_theorem :: "form ⇒ bool" where [iff]: "is_theorem A ⟷ (∃𝒮. is_proof_of 𝒮 A)" lemma proof_form_is_wffo: assumes "is_proof_of 𝒮 A" and "B ∈ lset 𝒮" shows "B ∈ wffs⇘o⇙" using assms and elem_of_proof_is_wffo by blast lemma proof_form_is_theorem: assumes "is_proof 𝒮" and "𝒮 ≠ []" and "i' < length 𝒮" shows "is_theorem (𝒮 ! i')" proof - let ?𝒮⇩_{1}= "take (Suc i') 𝒮" from assms(1) obtain 𝒮⇩_{2}where "is_proof (?𝒮⇩_{1}@ 𝒮⇩_{2})" by (metis append_take_drop_id) then have "is_proof ?𝒮⇩_{1}" by (fact proof_prefix_is_proof) moreover from assms(3) have "last ?𝒮⇩_{1}= 𝒮 ! i'" by (simp add: take_Suc_conv_app_nth) ultimately show ?thesis using assms(2) unfolding is_proof_of_def and is_theorem_def by (metis Zero_neq_Suc take_eq_Nil2) qed theorem derivable_form_is_theorem: assumes "is_derivable A" shows "is_theorem A" using assms proof (induction rule: is_derivable.induct) case (dv_axiom A) then have "is_proof [A]" by (fact single_axiom_is_proof) moreover have "last [A] = A" by simp ultimately show ?case by blast next case (dv_rule_R C E p D) obtain 𝒮⇩_{C}and 𝒮⇩_{E}where "is_proof 𝒮⇩_{C}" and "𝒮⇩_{C}≠ []" and "last 𝒮⇩_{C}= C" and "is_proof 𝒮⇩_{E}" and "𝒮⇩_{E}≠ []" and "last 𝒮⇩_{E}= E" using dv_rule_R.IH by fastforce let ?i⇩_{C}= "length 𝒮⇩_{C}- 1" and ?i⇩_{E}= "length 𝒮⇩_{C}+ length 𝒮⇩_{E}- 1" and ?i⇩_{D}= "length 𝒮⇩_{C}+ length 𝒮⇩_{E}" let ?𝒮 = "𝒮⇩_{C}@ 𝒮⇩_{E}@ [D]" from ‹𝒮⇩_{C}≠ []› have "?i⇩_{C}< length (𝒮⇩_{C}@ 𝒮⇩_{E})" and "?i⇩_{E}< length (𝒮⇩_{C}@ 𝒮⇩_{E})" using linorder_not_le by fastforce+ moreover have "(𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{C}= C" and "(𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{E}= E" using ‹𝒮⇩_{C}≠ []› and ‹last 𝒮⇩_{C}= C› by ( simp add: last_conv_nth nth_append, metis ‹last 𝒮⇩_{E}= E› ‹𝒮⇩_{E}≠ []› append_is_Nil_conv last_appendR last_conv_nth length_append ) with ‹is_rule_R_app p D C E› have "is_rule_R_app p D ((𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{C}) ((𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{E})" using ‹(𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{C}= C› by fastforce moreover from ‹is_proof 𝒮⇩_{C}› and ‹is_proof 𝒮⇩_{E}› have "is_proof (𝒮⇩_{C}@ 𝒮⇩_{E})" by (fact proofs_concatenation_is_proof) ultimately have "is_proof ((𝒮⇩_{C}@ 𝒮⇩_{E}) @ [D])" using rule_R_app_appended_to_proof_is_proof by presburger with ‹𝒮⇩_{C}≠ []› show ?case unfolding is_proof_of_def and is_theorem_def by (metis snoc_eq_iff_butlast) qed theorem theorem_is_derivable_form: assumes "is_theorem A" shows "is_derivable A" proof - from assms obtain 𝒮 where "is_proof 𝒮" and "𝒮 ≠ []" and "last 𝒮 = A" by fastforce then show ?thesis proof (induction "length 𝒮" arbitrary: 𝒮 A rule: less_induct) case less let ?i' = "length 𝒮 - 1" from ‹𝒮 ≠ []› and ‹last 𝒮 = A› have "𝒮 ! ?i' = A" by (simp add: last_conv_nth) from ‹is_proof 𝒮› and ‹𝒮 ≠ []› and ‹last 𝒮 = A› have "is_proof_step 𝒮 ?i'" using added_suffix_proof_preservation[where 𝒮' = "[]"] by simp then consider (axiom) "𝒮 ! ?i' ∈ axioms" | (rule_R) "∃p j k. {j, k} ⊆ {0..<?i'} ∧ is_rule_R_app p (𝒮 ! ?i') (𝒮 ! j) (𝒮 ! k)" by fastforce then show ?case proof cases case axiom with ‹𝒮 ! ?i' = A› show ?thesis by (fastforce intro: dv_axiom) next case rule_R then obtain p and j and k where "{j, k} ⊆ {0..<?i'}" and "is_rule_R_app p (𝒮 ! ?i') (𝒮 ! j) (𝒮 ! k)" by force let ?𝒮⇩_{j}= "take (Suc j) 𝒮" let ?𝒮⇩_{k}= "take (Suc k) 𝒮" obtain 𝒮⇩_{j}' and 𝒮⇩_{k}' where "𝒮 = ?𝒮⇩_{j}@ 𝒮⇩_{j}'" and "𝒮 = ?𝒮⇩_{k}@ 𝒮⇩_{k}'" by (metis append_take_drop_id) with ‹is_proof 𝒮› have "is_proof (?𝒮⇩_{j}@ 𝒮⇩_{j}')" and "is_proof (?𝒮⇩_{k}@ 𝒮⇩_{k}')" by (simp_all only:) moreover from ‹𝒮 = ?𝒮⇩_{j}@ 𝒮⇩_{j}'› and ‹𝒮 = ?𝒮⇩_{k}@ 𝒮⇩_{k}'› and ‹last 𝒮 = A› and ‹{j, k} ⊆ {0..<length 𝒮 - 1}› have "last 𝒮⇩_{j}' = A" and "last 𝒮⇩_{k}' = A" using length_Cons and less_le_not_le and take_Suc and take_tl and append.right_neutral by (metis atLeastLessThan_iff diff_Suc_1 insert_subset last_appendR take_all_iff)+ moreover from ‹𝒮 ≠ []› have "?𝒮⇩_{j}≠ []" and "?𝒮⇩_{k}≠ []" by simp_all ultimately have "is_proof_of ?𝒮⇩_{j}(last ?𝒮⇩_{j})" and "is_proof_of ?𝒮⇩_{k}(last ?𝒮⇩_{k})" using proof_prefix_is_proof_of_last [where 𝒮 = ?𝒮⇩_{j}and 𝒮' = 𝒮⇩_{j}'] and proof_prefix_is_proof_of_last [where 𝒮 = ?𝒮⇩_{k}and 𝒮' = 𝒮⇩_{k}'] by fastforce+ moreover from ‹last 𝒮⇩_{j}' = A› and ‹last 𝒮⇩_{k}' = A› have "length ?𝒮⇩_{j}< length 𝒮" and "length ?𝒮⇩_{k}< length 𝒮" using ‹{j, k} ⊆ {0..<length 𝒮 - 1}› by force+ moreover from calculation(3,4) have "last ?𝒮⇩_{j}= 𝒮 ! j" and "last ?𝒮⇩_{k}= 𝒮 ! k" by (metis Suc_lessD last_snoc linorder_not_le nat_neq_iff take_Suc_conv_app_nth take_all_iff)+ ultimately have "is_derivable (𝒮 ! j)" and "is_derivable (𝒮 ! k)" using ‹?𝒮⇩_{j}≠ []› and ‹?𝒮⇩_{k}≠ []› and less(1) by blast+ with ‹is_rule_R_app p (𝒮 ! ?i') (𝒮 ! j) (𝒮 ! k)› and ‹𝒮 ! ?i' = A› show ?thesis by (blast intro: dv_rule_R) qed qed qed theorem theoremhood_derivability_equivalence: shows "is_theorem A ⟷ is_derivable A" using derivable_form_is_theorem and theorem_is_derivable_form by blast lemma theorem_is_wffo: assumes "is_theorem A" shows "A ∈ wffs⇘o⇙" proof - from assms obtain 𝒮 where "is_proof_of 𝒮 A" by blast then have "A ∈ lset 𝒮" by auto with ‹is_proof_of 𝒮 A› show ?thesis using proof_form_is_wffo by blast qed lemma equality_reflexivity: assumes "A ∈ wffs⇘α⇙" shows "is_theorem (A =⇘α⇙ A)" (is "is_theorem ?A⇩_{2}") proof - let ?A⇩_{1}= "(λ𝔵⇘α⇙. 𝔵⇘α⇙) · A =⇘α⇙ A" let ?𝒮 = "[?A⇩_{1}, ?A⇩_{2}]" ― ‹ (.1) Axiom 4.2 › have "is_proof_step ?𝒮 0" proof - from assms have "?A⇩_{1}∈ axioms" by (intro axiom_4_2) then show ?thesis by simp qed ― ‹ (.2) Rule R: .1,.1 › moreover have "is_proof_step ?𝒮 1" proof - let ?p = "[«, »]" have "∃p j k. {j::nat, k} ⊆ {0..<1} ∧ is_rule_R_app ?p ?A⇩_{2}(?𝒮 ! j) (?𝒮 ! k)" proof - let ?D = "?A⇩_{2}" and ?j = "0::nat" and ?k = "0" have "{?j, ?k} ⊆ {0..<1}" by simp moreover have "is_rule_R_app ?p ?A⇩_{2}(?𝒮 ! ?j) (?𝒮 ! ?k)" proof - have "(λ𝔵⇘α⇙. 𝔵⇘α⇙) · A ≼⇘?p⇙ (?𝒮 ! ?j)" by force moreover have "(?𝒮 ! ?j)⦉?p ← A⦊ ⊳ ?D" by force moreover from ‹A ∈ wffs⇘α⇙› have "?D ∈ wffs⇘o⇙" by (intro equality_wff) moreover from ‹A ∈ wffs⇘α⇙› have "(λ𝔵⇘α⇙. 𝔵⇘α⇙) · A ∈ wffs⇘α⇙" by (meson wffs_of_type_simps) ultimately show ?thesis using ‹A ∈ wffs⇘α⇙› by simp qed ultimately show ?thesis by meson qed then show ?thesis by auto qed moreover have "last ?𝒮 = ?A⇩_{2}" by simp moreover have "{0..<length ?𝒮} = {0, 1}" by (simp add: atLeast0_lessThan_Suc insert_commute) ultimately show ?thesis unfolding is_theorem_def and is_proof_def and is_proof_of_def by (metis One_nat_def Suc_1 length_Cons less_2_cases list.distinct(1) list.size(3)) qed lemma equality_reflexivity': assumes "A ∈ wffs⇘α⇙" shows "is_theorem (A =⇘α⇙ A)" (is "is_theorem ?A⇩_{2}") proof (intro derivable_form_is_theorem) let ?A⇩_{1}= "(λ𝔵⇘α⇙. 𝔵⇘α⇙) · A =⇘α⇙ A" ― ‹ (.1) Axiom 4.2 › from assms have "?A⇩_{1}∈ axioms" by (intro axiom_4_2) then have step_1: "is_derivable ?A⇩_{1}" by (intro dv_axiom) ― ‹ (.2) Rule R: .1,.1 › then show "is_derivable ?A⇩_{2}" proof - let ?p = "[«, »]" and ?C = "?A⇩_{1}" and ?E = "?A⇩_{1}" and ?D = "?A⇩_{2}" have "is_rule_R_app ?p ?D ?C ?E" proof - have "(λ𝔵⇘α⇙. 𝔵⇘α⇙) · A ≼⇘?p⇙ ?C" by force moreover have "?C⦉?p ← A⦊ ⊳ ?D" by force moreover from ‹A ∈ wffs⇘α⇙› have "?D ∈ wffs⇘o⇙" by (intro equality_wff) moreover from ‹A ∈ wffs⇘α⇙› have "(λ𝔵⇘α⇙. 𝔵⇘α⇙) · A ∈ wffs⇘α⇙" by (meson wffs_of_type_simps) ultimately show ?thesis using ‹A ∈ wffs⇘α⇙› by simp qed with step_1 show ?thesis by (blast intro: dv_rule_R) qed qed subsection ‹Hypothetical proof and derivability› text ‹The set of free variables in ‹𝒳› that are exposed to capture at position ‹p› in ‹A›:› definition capture_exposed_vars_at :: "position ⇒ form ⇒ 'a ⇒ var set" where [simp]: "capture_exposed_vars_at p A 𝒳 = {(x, β) | x β p' E. strict_prefix p' p ∧ λx⇘β⇙. E ≼⇘p'⇙ A ∧ (x, β) ∈ free_vars 𝒳}" lemma capture_exposed_vars_at_alt_def: assumes "p ∈ positions A" shows "capture_exposed_vars_at p A 𝒳 = binders_at A p ∩ free_vars 𝒳" unfolding binders_at_alt_def[OF assms] and in_scope_of_abs_alt_def using is_subform_implies_in_positions by auto text ‹Inference rule R$'$:› definition rule_R'_side_condition :: "form set ⇒ position ⇒ form ⇒ form ⇒ form ⇒ bool" where [iff]: "rule_R'_side_condition ℋ p D C E ⟷ capture_exposed_vars_at p C E ∩ capture_exposed_vars_at p C ℋ = {}" lemma rule_R'_side_condition_alt_def: fixes ℋ :: "form set" assumes "C ∈ wffs⇘α⇙" shows " rule_R'_side_condition ℋ p D C (A =⇘α⇙ B) ⟷ ( ∄x β E p'. strict_prefix p' p ∧ λx⇘β⇙. E ≼⇘p'⇙ C ∧ (x, β) ∈ free_vars (A =⇘α⇙ B) ∧ (∃H ∈ ℋ. (x, β) ∈ free_vars H) )" proof - have " capture_exposed_vars_at p C (A =⇘α⇙ B) = {(x, β) | x β p' E. strict_prefix p' p ∧ λx⇘β⇙. E ≼⇘p'⇙ C ∧ (x, β) ∈ free_vars (A =⇘α⇙ B)}" using assms and capture_exposed_vars_at_alt_def unfolding capture_exposed_vars_at_def by fast moreover have " capture_exposed_vars_at p C ℋ = {(x, β) | x β p' E. strict_prefix p' p ∧ λx⇘β⇙. E ≼⇘p'⇙ C ∧ (x, β) ∈ free_vars ℋ}" using assms and capture_exposed_vars_at_alt_def unfolding capture_exposed_vars_at_def by fast ultimately have " capture_exposed_vars_at p C (A =⇘α⇙ B) ∩ capture_exposed_vars_at p C ℋ = {(x, β) | x β p' E. strict_prefix p' p ∧ λx⇘β⇙. E ≼⇘p'⇙ C ∧ (x, β) ∈ free_vars (A =⇘α⇙ B) ∧ (x, β) ∈ free_vars ℋ}" by auto also have " … = {(x, β) | x β p' E. strict_prefix p' p ∧ λx⇘β⇙. E ≼⇘p'⇙ C ∧ (x, β) ∈ free_vars (A =⇘α⇙ B) ∧ (∃H ∈ ℋ. (x, β) ∈ free_vars H)}" by auto finally show ?thesis by fast qed definition is_rule_R'_app :: "form set ⇒ position ⇒ form ⇒ form ⇒ form ⇒ bool" where [iff]: "is_rule_R'_app ℋ p D C E ⟷ is_rule_R_app p D C E ∧ rule_R'_side_condition ℋ p D C E" lemma is_rule_R'_app_alt_def: shows " is_rule_R'_app ℋ p D C E ⟷ ( ∃α A B. E = A =⇘α⇙ B ∧ A ∈ wffs⇘α⇙ ∧ B ∈ wffs⇘α⇙ ∧ ― ‹\<^term>‹E› is a well-formed equality› A ≼⇘p⇙ C ∧ D ∈ wffs⇘o⇙ ∧ C⦉p ← B⦊ ⊳ D ∧ ( ∄x β E p'. strict_prefix p' p ∧ λx⇘β⇙. E ≼⇘p'⇙ C ∧ (x, β) ∈ free_vars (A =⇘α⇙ B) ∧ (∃H ∈ ℋ. (x, β) ∈ free_vars H) ) )" using rule_R'_side_condition_alt_def by fastforce lemma rule_R'_preserves_typing: assumes "is_rule_R'_app ℋ p D C E" shows "C ∈ wffs⇘o⇙ ⟷ D ∈ wffs⇘o⇙" using assms and replacement_preserves_typing unfolding is_rule_R_app_def and is_rule_R'_app_def by meson abbreviation is_hyps :: "form set ⇒ bool" where "is_hyps ℋ ≡ ℋ ⊆ wffs⇘o⇙ ∧ finite ℋ" inductive is_derivable_from_hyps :: "form set ⇒ form ⇒ bool" ("_ ⊢ _" [50, 50] 50) for ℋ where dv_hyp: "ℋ ⊢ A" if "A ∈ ℋ" and "is_hyps ℋ" | dv_thm: "ℋ ⊢ A" if "is_theorem A" and "is_hyps ℋ" | dv_rule_R': "ℋ ⊢ D" if "ℋ ⊢ C" and "ℋ ⊢ E" and "is_rule_R'_app ℋ p D C E" and "is_hyps ℋ" lemma hyp_derivable_form_is_wffso: assumes "is_derivable_from_hyps ℋ A" shows "A ∈ wffs⇘o⇙" using assms and theorem_is_wffo by (cases rule: is_derivable_from_hyps.cases) auto definition is_hyp_proof_step :: "form set ⇒ form list ⇒ form list ⇒ nat ⇒ bool" where [iff]: "is_hyp_proof_step ℋ 𝒮⇩_{1}𝒮⇩_{2}i' ⟷ 𝒮⇩_{2}! i' ∈ ℋ ∨ 𝒮⇩_{2}! i' ∈ lset 𝒮⇩_{1}∨ (∃p j k. {j, k} ⊆ {0..<i'} ∧ is_rule_R'_app ℋ p (𝒮⇩_{2}! i') (𝒮⇩_{2}! j) (𝒮⇩_{2}! k))" type_synonym hyp_proof = "form list × form list" definition is_hyp_proof :: "form set ⇒ form list ⇒ form list ⇒ bool" where [iff]: "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}⟷ (∀i' < length 𝒮⇩_{2}. is_hyp_proof_step ℋ 𝒮⇩_{1}𝒮⇩_{2}i')" lemma common_prefix_is_hyp_subproof_from: assumes "is_hyp_proof ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ 𝒮⇩_{2}')" and "i' < length 𝒮⇩_{2}" shows "is_hyp_proof_step ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ 𝒮⇩_{2}'') i'" proof - let ?𝒮 = "𝒮⇩_{2}@ 𝒮⇩_{2}'" from assms(2) have "?𝒮 ! i' = (𝒮⇩_{2}@ 𝒮⇩_{2}'') ! i'" by (simp add: nth_append) moreover from assms(2) have "i' < length ?𝒮" by simp ultimately obtain p and j and k where " ?𝒮 ! i' ∈ ℋ ∨ ?𝒮 ! i' ∈ lset 𝒮⇩_{1}∨ {j, k} ⊆ {0..<i'} ∧ is_rule_R'_app ℋ p (?𝒮 ! i') (?𝒮 ! j) (?𝒮 ! k)" using assms(1) unfolding is_hyp_proof_def and is_hyp_proof_step_def by meson then consider (hyp) "?𝒮 ! i' ∈ ℋ" | (seq) "?𝒮 ! i' ∈ lset 𝒮⇩_{1}" | (rule_R') "{j, k} ⊆ {0..<i'} ∧ is_rule_R'_app ℋ p (?𝒮 ! i') (?𝒮 ! j) (?𝒮 ! k)" by blast then have " (𝒮⇩_{2}@ 𝒮⇩_{2}'') ! i' ∈ ℋ ∨ (𝒮⇩_{2}@ 𝒮⇩_{2}'') ! i' ∈ lset 𝒮⇩_{1}∨ ({j, k} ⊆ {0..<i'} ∧ is_rule_R'_app ℋ p ((𝒮⇩_{2}@ 𝒮⇩_{2}'') ! i') ((𝒮⇩_{2}@ 𝒮⇩_{2}'') ! j) ((𝒮⇩_{2}@ 𝒮⇩_{2}'') ! k))" proof cases case hyp with assms(2) have "(𝒮⇩_{2}@ 𝒮⇩_{2}'') ! i' ∈ ℋ" by (simp add: nth_append) then show ?thesis .. next case seq with assms(2) have "(𝒮⇩_{2}@ 𝒮⇩_{2}'') ! i' ∈ lset 𝒮⇩_{1}" by (simp add: nth_append) then show ?thesis by (intro disjI1 disjI2) next case rule_R' with assms(2) have "?𝒮 ! j = (𝒮⇩_{2}@ 𝒮⇩_{2}'') ! j" and "?𝒮 ! k = (𝒮⇩_{2}@ 𝒮⇩_{2}'') ! k" by (simp_all add: nth_append) with assms(2) and rule_R' have " {j, k} ⊆ {0..<i'} ∧ is_rule_R'_app ℋ p ((𝒮⇩_{2}@ 𝒮⇩_{2}'') ! i') ((𝒮⇩_{2}@ 𝒮⇩_{2}'') ! j) ((𝒮⇩_{2}@ 𝒮⇩_{2}'') ! k)" by (metis nth_append) then show ?thesis by (intro disjI2) qed then show ?thesis unfolding is_hyp_proof_step_def by meson qed lemma added_suffix_thms_hyp_proof_preservation: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" shows "is_hyp_proof ℋ (𝒮⇩_{1}@ 𝒮⇩_{1}') 𝒮⇩_{2}" using assms by auto lemma added_suffix_hyp_proof_preservation: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "i' < length (𝒮⇩_{2}@ 𝒮⇩_{2}') - length 𝒮⇩_{2}'" shows "is_hyp_proof_step ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ 𝒮⇩_{2}') i'" using assms and common_prefix_is_hyp_subproof_from[where 𝒮⇩_{2}' = "[]"] by auto lemma appended_hyp_proof_step_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "is_hyp_proof_step ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ [A]) (length (𝒮⇩_{2}@ [A]) - 1)" shows "is_hyp_proof ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ [A])" proof (standard, intro allI impI) fix i' assume "i' < length (𝒮⇩_{2}@ [A])" then consider (a) "i' < length 𝒮⇩_{2}" | (b) "i' = length 𝒮⇩_{2}" by fastforce then show "is_hyp_proof_step ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ [A]) i'" proof cases case a with assms(1) show ?thesis using added_suffix_hyp_proof_preservation by simp next case b with assms(2) show ?thesis by simp qed qed lemma added_prefix_hyp_proof_preservation: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}'" and "i' ∈ {length 𝒮⇩_{2}..<length (𝒮⇩_{2}@ 𝒮⇩_{2}')}" shows "is_hyp_proof_step ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ 𝒮⇩_{2}') i'" proof - let ?𝒮 = "𝒮⇩_{2}@ 𝒮⇩_{2}'" let ?i = "i' - length 𝒮⇩_{2}" from assms(2) have "?𝒮 ! i' = 𝒮⇩_{2}' ! ?i" and "?i < length 𝒮⇩_{2}'" by (simp_all add: nth_append less_diff_conv2) then have "is_hyp_proof_step ℋ 𝒮⇩_{1}?𝒮 i' = is_hyp_proof_step ℋ 𝒮⇩_{1}𝒮⇩_{2}' ?i" proof - from assms(1) and ‹?i < length 𝒮⇩_{2}'› obtain j and k and p where " 𝒮⇩_{2}' ! ?i ∈ ℋ ∨ 𝒮⇩_{2}' ! ?i ∈ lset 𝒮⇩_{1}∨ ({j, k} ⊆ {0..<?i} ∧ is_rule_R'_app ℋ p (𝒮⇩_{2}' ! ?i) (𝒮⇩_{2}' ! j) (𝒮⇩_{2}' ! k))" unfolding is_hyp_proof_def and is_hyp_proof_step_def by meson then consider (hyp) "𝒮⇩_{2}' ! ?i ∈ ℋ" | (seq) "𝒮⇩_{2}' ! ?i ∈ lset 𝒮⇩_{1}" | (rule_R') "{j, k} ⊆ {0..<?i} ∧ is_rule_R'_app ℋ p (𝒮⇩_{2}' ! ?i) (𝒮⇩_{2}' ! j) (𝒮⇩_{2}' ! k)" by blast then have " ?𝒮 ! i' ∈ ℋ ∨ ?𝒮 ! i' ∈ lset 𝒮⇩_{1}∨ ({j + length 𝒮⇩_{2}, k + length 𝒮⇩_{2}} ⊆ {0..<i'} ∧ is_rule_R'_app ℋ p (?𝒮 ! i') (?𝒮 ! (j + length 𝒮⇩_{2})) (?𝒮 ! (k + length 𝒮⇩_{2})))" proof cases case hyp with ‹?𝒮 ! i' = 𝒮⇩_{2}' ! ?i› have "?𝒮 ! i' ∈ ℋ" by (simp only:) then show ?thesis .. next case seq with ‹?𝒮 ! i' = 𝒮⇩_{2}' ! ?i› have "?𝒮 ! i' ∈ lset 𝒮⇩_{1}" by (simp only:) then show ?thesis by (intro disjI1 disjI2) next case rule_R' with assms(2) have "?𝒮 ! (j + length 𝒮⇩_{2}) = 𝒮⇩_{2}' ! j" and "?𝒮 ! (k + length 𝒮⇩_{2}) = 𝒮⇩_{2}' ! k" by (simp_all add: nth_append) with ‹?𝒮 ! i' = 𝒮⇩_{2}' ! ?i› and rule_R' have " {j + length 𝒮⇩_{2}, k + length 𝒮⇩_{2}} ⊆ {0..<i'} ∧ is_rule_R'_app ℋ p (?𝒮 ! i') (?𝒮 ! (j + length 𝒮⇩_{2})) (?𝒮 ! (k + length 𝒮⇩_{2}))" by auto then show ?thesis by (intro disjI2) qed with assms(1) and ‹?i < length 𝒮⇩_{2}'› show ?thesis unfolding is_hyp_proof_def and is_hyp_proof_step_def by meson qed with assms(1) and ‹?i < length 𝒮⇩_{2}'› show ?thesis by simp qed lemma hyp_proof_but_last_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ [A])" shows "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" using assms and common_prefix_is_hyp_subproof_from[where 𝒮⇩_{2}' = "[A]" and 𝒮⇩_{2}'' = "[]"] by simp lemma hyp_proof_prefix_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ 𝒮⇩_{2}')" shows "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" using assms and hyp_proof_but_last_is_hyp_proof by (induction 𝒮⇩_{2}' arbitrary: 𝒮⇩_{2}rule: rev_induct) (simp, metis append.assoc) lemma single_hyp_is_hyp_proof: assumes "A ∈ ℋ" shows "is_hyp_proof ℋ 𝒮⇩_{1}[A]" using assms by fastforce lemma single_thm_is_hyp_proof: assumes "A ∈ lset 𝒮⇩_{1}" shows "is_hyp_proof ℋ 𝒮⇩_{1}[A]" using assms by fastforce lemma hyp_proofs_from_concatenation_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{1}'" and "is_hyp_proof ℋ 𝒮⇩_{2}𝒮⇩_{2}'" shows "is_hyp_proof ℋ (𝒮⇩_{1}@ 𝒮⇩_{2}) (𝒮⇩_{1}' @ 𝒮⇩_{2}')" proof (standard, intro allI impI) let ?𝒮 = "𝒮⇩_{1}@ 𝒮⇩_{2}" and ?𝒮' = "𝒮⇩_{1}' @ 𝒮⇩_{2}'" fix i' assume "i' < length ?𝒮'" then consider (a) "i' < length 𝒮⇩_{1}'" | (b) "i' ∈ {length 𝒮⇩_{1}'..<length ?𝒮'}" by fastforce then show "is_hyp_proof_step ℋ ?𝒮 ?𝒮' i'" proof cases case a from ‹is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{1}'› have "is_hyp_proof ℋ (𝒮⇩_{1}@ 𝒮⇩_{2}) 𝒮⇩_{1}'" by auto with assms(1) and a show ?thesis using added_suffix_hyp_proof_preservation[where 𝒮⇩_{1}= "𝒮⇩_{1}@ 𝒮⇩_{2}"] by auto next case b from assms(2) have "is_hyp_proof ℋ (𝒮⇩_{1}@ 𝒮⇩_{2}) 𝒮⇩_{2}'" by auto with b show ?thesis using added_prefix_hyp_proof_preservation[where 𝒮⇩_{1}= "𝒮⇩_{1}@ 𝒮⇩_{2}"] by auto qed qed lemma elem_of_hyp_proof_is_wffo: assumes "is_hyps ℋ" and "lset 𝒮⇩_{1}⊆ wffs⇘o⇙" and "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "A ∈ lset 𝒮⇩_{2}" shows "A ∈ wffs⇘o⇙" using assms proof (induction 𝒮⇩_{2}rule: rev_induct) case Nil then show ?case by simp next case (snoc A' 𝒮⇩_{2}) from ‹is_hyp_proof ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ [A'])› have "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" using hyp_proof_prefix_is_hyp_proof[where 𝒮⇩_{2}' = "[A']"] by presburger then show ?case proof (cases "A ∈ lset 𝒮⇩_{2}") case True with snoc.prems(1,2) and ‹is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}› show ?thesis by (fact snoc.IH) next case False with snoc.prems(4) have "A' = A" by simp with snoc.prems(3) have " (𝒮⇩_{2}@ [A]) ! i' ∈ ℋ ∨ (𝒮⇩_{2}@ [A]) ! i' ∈ lset 𝒮⇩_{1}∨ (𝒮⇩_{2}@ [A]) ! i' ∈ wffs⇘o⇙" if "i' ∈ {0..<length (𝒮⇩_{2}@ [A])}" for i' using that by auto then have "A ∈ wffs⇘o⇙ ∨ A ∈ ℋ ∨ A ∈ lset 𝒮⇩_{1}∨ length 𝒮⇩_{2}∉ {0..<Suc (length 𝒮⇩_{2})}" by (metis (no_types) length_append_singleton nth_append_length) with assms(1) and ‹lset 𝒮⇩_{1}⊆ wffs⇘o⇙› show ?thesis using atLeast0_lessThan_Suc by blast qed qed lemma hyp_prepended_to_hyp_proof_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "A ∈ ℋ" shows "is_hyp_proof ℋ 𝒮⇩_{1}([A] @ 𝒮⇩_{2})" using hyp_proofs_from_concatenation_is_hyp_proof [ OF single_hyp_is_hyp_proof[OF assms(2)] assms(1), where 𝒮⇩_{1}= "[]" ] by simp lemma hyp_appended_to_hyp_proof_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "A ∈ ℋ" shows "is_hyp_proof ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ [A])" using hyp_proofs_from_concatenation_is_hyp_proof [ OF assms(1) single_hyp_is_hyp_proof[OF assms(2)], where 𝒮⇩_{2}= "[]" ] by simp lemma dropped_duplicated_thm_in_hyp_proof_is_hyp_proof: assumes "is_hyp_proof ℋ (A # 𝒮⇩_{1}) 𝒮⇩_{2}" and "A ∈ lset 𝒮⇩_{1}" shows "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" using assms by auto lemma thm_prepended_to_hyp_proof_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "A ∈ lset 𝒮⇩_{1}" shows "is_hyp_proof ℋ 𝒮⇩_{1}([A] @ 𝒮⇩_{2})" using hyp_proofs_from_concatenation_is_hyp_proof[OF single_thm_is_hyp_proof[OF assms(2)] assms(1)] and dropped_duplicated_thm_in_hyp_proof_is_hyp_proof by simp lemma thm_appended_to_hyp_proof_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "A ∈ lset 𝒮⇩_{1}" shows "is_hyp_proof ℋ 𝒮⇩_{1}(𝒮⇩_{2}@ [A])" using hyp_proofs_from_concatenation_is_hyp_proof[OF assms(1) single_thm_is_hyp_proof[OF assms(2)]] and dropped_duplicated_thm_in_hyp_proof_is_hyp_proof by simp lemma rule_R'_app_appended_to_hyp_proof_is_hyp_proof: assumes "is_hyp_proof ℋ 𝒮' 𝒮" and "i⇩_{C}< length 𝒮" and "𝒮 ! i⇩_{C}= C" and "i⇩_{E}< length 𝒮" and "𝒮 ! i⇩_{E}= E" and "is_rule_R'_app ℋ p D C E" shows "is_hyp_proof ℋ 𝒮' (𝒮 @ [D])" proof (standard, intro allI impI) let ?𝒮 = "𝒮 @ [D]" fix i' assume "i' < length ?𝒮" then consider (a) "i' < length 𝒮" | (b) "i' = length 𝒮" by fastforce then show "is_hyp_proof_step ℋ 𝒮' (𝒮 @ [D]) i'" proof cases case a with assms(1) show ?thesis using added_suffix_hyp_proof_preservation by auto next case b let ?i⇩_{D}= "length 𝒮" from assms(2,4) have "i⇩_{C}< ?i⇩_{D}" and "i⇩_{E}< ?i⇩_{D}" by fastforce+ with assms(3,5,6) have "is_rule_R'_app ℋ p (?𝒮 ! ?i⇩_{D}) (?𝒮 ! i⇩_{C}) (?𝒮 ! i⇩_{E})" by (simp add: nth_append) with assms(2,4) have " ∃p j k. {j, k} ⊆ {0..<?i⇩_{D}} ∧ is_rule_R'_app ℋ p (?𝒮 ! ?i⇩_{D}) (?𝒮 ! j) (?𝒮 ! k)" by (intro exI)+ auto then have "is_hyp_proof_step ℋ 𝒮' ?𝒮 (length ?𝒮 - 1)" by simp moreover from b have "i' = length ?𝒮 - 1" by simp ultimately show ?thesis by fast qed qed definition is_hyp_proof_of :: "form set ⇒ form list ⇒ form list ⇒ form ⇒ bool" where [iff]: "is_hyp_proof_of ℋ 𝒮⇩_{1}𝒮⇩_{2}A ⟷ is_hyps ℋ ∧ is_proof 𝒮⇩_{1}∧ 𝒮⇩_{2}≠ [] ∧ is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}∧ last 𝒮⇩_{2}= A" lemma hyp_proof_prefix_is_hyp_proof_of_last: assumes "is_hyps ℋ" and "is_proof 𝒮''" and "is_hyp_proof ℋ 𝒮'' (𝒮 @ 𝒮')" and "𝒮 ≠ []" shows "is_hyp_proof_of ℋ 𝒮'' 𝒮 (last 𝒮)" using assms and hyp_proof_prefix_is_hyp_proof by simp theorem hyp_derivability_implies_hyp_proof_existence: assumes "ℋ ⊢ A" shows "∃𝒮⇩_{1}𝒮⇩_{2}. is_hyp_proof_of ℋ 𝒮⇩_{1}𝒮⇩_{2}A" using assms proof (induction rule: is_derivable_from_hyps.induct) case (dv_hyp A) from ‹A ∈ ℋ› have "is_hyp_proof ℋ [] [A]" by (fact single_hyp_is_hyp_proof) moreover have "last [A] = A" by simp moreover have "is_proof []" by simp ultimately show ?case using ‹is_hyps ℋ› unfolding is_hyp_proof_of_def by (meson list.discI) next case (dv_thm A) then obtain 𝒮 where "is_proof 𝒮" and "𝒮 ≠ []" and "last 𝒮 = A" by fastforce then have "is_hyp_proof ℋ 𝒮 [A]" using single_thm_is_hyp_proof by auto with ‹is_hyps ℋ› and ‹is_proof 𝒮› have "is_hyp_proof_of ℋ 𝒮 [A] A" by fastforce then show ?case by (intro exI) next case (dv_rule_R' C E p D) from dv_rule_R'.IH obtain 𝒮⇩_{C}and 𝒮⇩_{C}' and 𝒮⇩_{E}and 𝒮⇩_{E}' where "is_hyp_proof ℋ 𝒮⇩_{C}' 𝒮⇩_{C}" and "is_proof 𝒮⇩_{C}'" and "𝒮⇩_{C}≠ []" and "last 𝒮⇩_{C}= C" and "is_hyp_proof ℋ 𝒮⇩_{E}' 𝒮⇩_{E}" and "is_proof 𝒮⇩_{E}'" and "𝒮⇩_{E}≠ []" and "last 𝒮⇩_{E}= E" by auto let ?i⇩_{C}= "length 𝒮⇩_{C}- 1" and ?i⇩_{E}= "length 𝒮⇩_{C}+ length 𝒮⇩_{E}- 1" and ?i⇩_{D}= "length 𝒮⇩_{C}+ length 𝒮⇩_{E}" let ?𝒮 = "𝒮⇩_{C}@ 𝒮⇩_{E}@ [D]" from ‹𝒮⇩_{C}≠ []› have "?i⇩_{C}< length (𝒮⇩_{C}@ 𝒮⇩_{E})" and "?i⇩_{E}< length (𝒮⇩_{C}@ 𝒮⇩_{E})" using linorder_not_le by fastforce+ moreover have "(𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{C}= C" and "(𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{E}= E" using ‹𝒮⇩_{C}≠ []› and ‹last 𝒮⇩_{C}= C› and ‹𝒮⇩_{E}≠ []› and ‹last 𝒮⇩_{E}= E› by ( simp add: last_conv_nth nth_append, metis append_is_Nil_conv last_appendR last_conv_nth length_append ) with ‹is_rule_R'_app ℋ p D C E› have "is_rule_R'_app ℋ p D ((𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{C}) ((𝒮⇩_{C}@ 𝒮⇩_{E}) ! ?i⇩_{E})" by fastforce moreover from ‹is_hyp_proof ℋ 𝒮⇩_{C}' 𝒮⇩_{C}› and ‹is_hyp_proof ℋ 𝒮⇩_{E}' 𝒮⇩_{E}› have "is_hyp_proof ℋ (𝒮⇩_{C}' @ 𝒮⇩_{E}') (𝒮⇩_{C}@ 𝒮⇩_{E})" by (fact hyp_proofs_from_concatenation_is_hyp_proof) ultimately have "is_hyp_proof ℋ (𝒮⇩_{C}' @ 𝒮⇩_{E}') ((𝒮⇩_{C}@ 𝒮⇩_{E}) @ [D])" using rule_R'_app_appended_to_hyp_proof_is_hyp_proof by presburger moreover from ‹is_proof 𝒮⇩_{C}'› and ‹is_proof 𝒮⇩_{E}'› have "is_proof (𝒮⇩_{C}' @ 𝒮⇩_{E}')" by (fact proofs_concatenation_is_proof) ultimately have "is_hyp_proof_of ℋ (𝒮⇩_{C}' @ 𝒮⇩_{E}') ((𝒮⇩_{C}@ 𝒮⇩_{E}) @ [D]) D" using ‹is_hyps ℋ› by fastforce then show ?case by (intro exI) qed theorem hyp_proof_existence_implies_hyp_derivability: assumes "∃𝒮⇩_{1}𝒮⇩_{2}. is_hyp_proof_of ℋ 𝒮⇩_{1}𝒮⇩_{2}A" shows "ℋ ⊢ A" proof - from assms obtain 𝒮⇩_{1}and 𝒮⇩_{2}where "is_hyps ℋ" and "is_proof 𝒮⇩_{1}" and "𝒮⇩_{2}≠ []" and "is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}" and "last 𝒮⇩_{2}= A" by fastforce then show ?thesis proof (induction "length 𝒮⇩_{2}" arbitrary: 𝒮⇩_{2}A rule: less_induct) case less let ?i' = "length 𝒮⇩_{2}- 1" from ‹𝒮⇩_{2}≠ []› and ‹last 𝒮⇩_{2}= A› have "𝒮⇩_{2}! ?i' = A" by (simp add: last_conv_nth) from ‹is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}› and ‹𝒮⇩_{2}≠ []› have "is_hyp_proof_step ℋ 𝒮⇩_{1}𝒮⇩_{2}?i'" by simp then consider (hyp) "𝒮⇩_{2}! ?i' ∈ ℋ" | (seq) "𝒮⇩_{2}! ?i' ∈ lset 𝒮⇩_{1}" | (rule_R') "∃p j k. {j, k} ⊆ {0..<?i'} ∧ is_rule_R'_app ℋ p (𝒮⇩_{2}! ?i') (𝒮⇩_{2}! j) (𝒮⇩_{2}! k)" by force then show ?case proof cases case hyp with ‹𝒮⇩_{2}! ?i' = A› and ‹is_hyps ℋ› show ?thesis by (fastforce intro: dv_hyp) next case seq from ‹𝒮⇩_{2}! ?i' ∈ lset 𝒮⇩_{1}› and ‹𝒮⇩_{2}! ?i' = A› obtain j where "𝒮⇩_{1}! j = A" and "𝒮⇩_{1}≠ []" and "j < length 𝒮⇩_{1}" by (metis empty_iff in_set_conv_nth list.set(1)) with ‹is_proof 𝒮⇩_{1}› have "is_proof (take (Suc j) 𝒮⇩_{1})" and "take (Suc j) 𝒮⇩_{1}≠ []" using proof_prefix_is_proof[where 𝒮⇩_{1}= "take (Suc j) 𝒮⇩_{1}" and 𝒮⇩_{2}= "drop (Suc j) 𝒮⇩_{1}"] by simp_all moreover from ‹𝒮⇩_{1}! j = A› and ‹j < length 𝒮⇩_{1}› have "last (take (Suc j) 𝒮⇩_{1}) = A" by (simp add: take_Suc_conv_app_nth) ultimately have "is_proof_of (take (Suc j) 𝒮⇩_{1}) A" by fastforce then have "is_theorem A" using is_theorem_def by blast with ‹is_hyps ℋ› show ?thesis by (intro dv_thm) next case rule_R' then obtain p and j and k where "{j, k} ⊆ {0..<?i'}" and "is_rule_R'_app ℋ p (𝒮⇩_{2}! ?i') (𝒮⇩_{2}! j) (𝒮⇩_{2}! k)" by force let ?𝒮⇩_{j}= "take (Suc j) 𝒮⇩_{2}" and ?𝒮⇩_{k}= "take (Suc k) 𝒮⇩_{2}" obtain 𝒮⇩_{j}' and 𝒮⇩_{k}' where "𝒮⇩_{2}= ?𝒮⇩_{j}@ 𝒮⇩_{j}'" and "𝒮⇩_{2}= ?𝒮⇩_{k}@ 𝒮⇩_{k}'" by (metis append_take_drop_id) then have "is_hyp_proof ℋ 𝒮⇩_{1}(?𝒮⇩_{j}@ 𝒮⇩_{j}')" and "is_hyp_proof ℋ 𝒮⇩_{1}(?𝒮⇩_{k}@ 𝒮⇩_{k}')" by (simp_all only: ‹is_hyp_proof ℋ 𝒮⇩_{1}𝒮⇩_{2}›) moreover from ‹𝒮⇩_{2}≠ []› and ‹𝒮⇩_{2}= ?𝒮⇩_{j}@ 𝒮⇩_{j}'› and ‹𝒮⇩_{2}= ?𝒮⇩_{k}@ 𝒮⇩_{k}'› and ‹last 𝒮⇩_{2}= A› have "last 𝒮⇩_{j}' = A" and "last 𝒮⇩_{k}' = A" using ‹{j, k} ⊆ {0..<length 𝒮⇩_{2}- 1}› and take_tl and less_le_not_le and append.right_neutral by (metis atLeastLessThan_iff insert_subset last_appendR length_tl take_all_iff)+ moreover from ‹𝒮⇩_{2}≠ []› have "?𝒮⇩_{j}≠ []" and "?𝒮⇩_{k}≠ []" by simp_all ultimately have "is_hyp_proof_of ℋ 𝒮⇩_{1}?𝒮⇩_{j}(last ?𝒮⇩_{j})" and "is_hyp_proof_of ℋ 𝒮⇩_{1}?𝒮⇩_{k}(last ?𝒮⇩_{k})" using hyp_proof_prefix_is_hyp_proof_of_last [OF ‹is_hyps ℋ› ‹is_proof 𝒮⇩_{1}› ‹is_hyp_proof ℋ 𝒮⇩_{1}(?𝒮⇩_{j}@ 𝒮⇩_{j}')› ‹?𝒮⇩_{j}≠ []›] and hyp_proof_prefix_is_hyp_proof_of_last [OF ‹is_hyps ℋ› ‹is_proof 𝒮⇩_{1}› ‹is_hyp_proof ℋ 𝒮⇩_{1}(?𝒮⇩_{k}@ 𝒮⇩_{k}')› ‹?𝒮⇩_{k}≠ []›] by fastforce+ moreover from ‹last 𝒮⇩_{j}' = A› and ‹last 𝒮⇩_{k}' = A› have "length ?𝒮⇩_{j}< length 𝒮⇩_{2}" and "length ?𝒮⇩_{k}< length 𝒮⇩_{2}" using ‹{j, k} ⊆ {0..<length 𝒮⇩_{2}- 1}› by force+ moreover from calculation(3,4) have "last ?𝒮⇩_{j}= 𝒮⇩_{2}! j" and "last ?𝒮⇩_{k}= 𝒮⇩_{2}! k" by (metis Suc_lessD last_snoc linorder_not_le nat_neq_iff take_Suc_conv_app_nth take_all_iff)+ ultimately have "ℋ ⊢ 𝒮⇩_{2}! j" and "ℋ ⊢ 𝒮⇩_{2}! k" using ‹is_hyps ℋ› and less(1)[OF ‹length ?𝒮⇩_{j}< length 𝒮⇩_{2}›] and less(1)[OF ‹length ?𝒮⇩_{k}< length 𝒮⇩_{2}›] by fast+ with ‹is_hyps ℋ› and ‹𝒮⇩_{2}! ?i' = A› show ?thesis using ‹is_rule_R'_app ℋ p (𝒮⇩_{2}! ?i') (𝒮⇩_{2}! j) (𝒮⇩_{2}! k)› by (blast intro: dv_rule_R') qed qed qed theorem hypothetical_derivability_proof_existence_equivalence: shows "ℋ ⊢ A ⟷ (∃𝒮⇩_{1}𝒮⇩_{2}. is_hyp_proof_of ℋ 𝒮⇩_{1}𝒮⇩_{2}A)" using hyp_derivability_implies_hyp_proof_existence and hyp_proof_existence_implies_hyp_derivability .. proposition derivability_from_no_hyps_theoremhood_equivalence: shows "{} ⊢ A ⟷ is_theorem A" proof assume "{} ⊢ A" then show "is_theorem A" proof (induction rule: is_derivable_from_hyps.induct) case (dv_rule_R' C E p D) from ‹is_rule_R'_app {} p D C E› have "is_rule_R_app p D C E" by simp moreover from ‹is_theorem C› and ‹is_theorem E› have "is_derivable C" and "is_derivable E" using theoremhood_derivability_equivalence by (simp_all only:) ultimately have "is_derivable D" by (fastforce intro: dv_rule_R) then show ?case using theoremhood_derivability_equivalence by (simp only:) qed simp next assume "is_theorem A" then show "{} ⊢ A" by (blast intro: dv_thm) qed abbreviation is_derivable_from_no_hyps ("⊢ _" [50] 50) where "⊢ A ≡ {} ⊢ A" corollary derivability_implies_hyp_derivability: assumes "⊢ A" and "is_hyps ℋ" shows "ℋ ⊢ A" using assms and derivability_from_no_hyps_theoremhood_equivalence and dv_thm by simp lemma axiom_is_derivable_from_no_hyps: assumes "A ∈ axioms" shows "⊢ A" using derivability_from_no_hyps_theoremhood_equivalence and derivable_form_is_theorem[OF dv_axiom[OF assms]] by (simp only:) lemma axiom_is_derivable_from_hyps: assumes "A ∈ axioms" and "is_hyps ℋ" shows "ℋ ⊢ A" using assms and axiom_is_derivable_from_no_hyps and derivability_implies_hyp_derivability by blast lemma rule_R [consumes 2, case_names occ_subform replacement]: assumes "⊢ C" and "⊢ A =⇘α⇙ B" and "A ≼⇘p⇙ C" and "C⦉p ← B⦊ ⊳ D" shows "⊢ D" proof - from assms(1,2) have "is_derivable C" and "is_derivable (A =⇘α⇙ B)" using derivability_from_no_hyps_theoremhood_equivalence and theoremhood_derivability_equivalence by blast+ moreover have "is_rule_R_app p D C (A =⇘α⇙ B)" proof - from assms(1-4) have "D ∈ wffs⇘o⇙" and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙" by (meson hyp_derivable_form_is_wffso replacement_preserves_typing wffs_from_equality)+ with assms(3,4) show ?thesis by fastforce qed ultimately have "is_derivable D" by (rule dv_rule_R) then show ?thesis using derivability_from_no_hyps_theoremhood_equivalence and derivable_form_is_theorem by simp qed lemma rule_R' [consumes 2, case_names occ_subform replacement no_capture]: assumes "ℋ ⊢ C" and "ℋ ⊢ A =⇘α⇙ B" and "A ≼⇘p⇙ C" and "C⦉p ← B⦊ ⊳ D" and "rule_R'_side_condition ℋ p D C (A =⇘α⇙ B)" shows "ℋ ⊢ D" using assms(1,2) proof (rule dv_rule_R') from assms(1) show "is_hyps ℋ" by (blast elim: is_derivable_from_hyps.cases) moreover from assms(1-4) have "D ∈ wffs⇘o⇙" by (meson hyp_derivable_form_is_wffso replacement_preserves_typing wffs_from_equality) ultimately show "is_rule_R'_app ℋ p D C (A =⇘α⇙ B)" using assms(2-5) and hyp_derivable_form_is_wffso and wffs_from_equality unfolding is_rule_R_app_def and is_rule_R'_app_def by metis qed end