Theory Proof_System
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⇘α⇙ ∧
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]"
have "is_proof_step ?𝒮 0"
proof -
from assms have "?A⇩1 ∈ axioms"
by (intro axiom_4_2)
then show ?thesis
by simp
qed
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"
from assms have "?A⇩1 ∈ axioms"
by (intro axiom_4_2)
then have step_1: "is_derivable ?A⇩1"
by (intro dv_axiom)
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⇘α⇙ ∧
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