section ‹Propositional Well-Formed Formulas› theory Propositional_Wff imports Syntax Boolean_Algebra begin subsection ‹Syntax› inductive_set pwffs :: "form set" where T_pwff: "T⇘_{o}⇙ ∈ pwffs" | F_pwff: "F⇘_{o}⇙ ∈ pwffs" | var_pwff: "p⇘o⇙ ∈ pwffs" | neg_pwff: "∼⇧^{𝒬}A ∈ pwffs" if "A ∈ pwffs" | conj_pwff: "A ∧⇧^{𝒬}B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs" | disj_pwff: "A ∨⇧^{𝒬}B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs" | imp_pwff: "A ⊃⇧^{𝒬}B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs" | eqv_pwff: "A ≡⇧^{𝒬}B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs" lemmas [intro!] = pwffs.intros lemma pwffs_distinctnesses [induct_simp]: shows "T⇘_{o}⇙ ≠ F⇘_{o}⇙" and "T⇘_{o}⇙ ≠ p⇘o⇙" and "T⇘_{o}⇙ ≠ ∼⇧^{𝒬}A" and "T⇘_{o}⇙ ≠ A ∧⇧^{𝒬}B" and "T⇘_{o}⇙ ≠ A ∨⇧^{𝒬}B" and "T⇘_{o}⇙ ≠ A ⊃⇧^{𝒬}B" and "T⇘_{o}⇙ ≠ A ≡⇧^{𝒬}B" and "F⇘_{o}⇙ ≠ p⇘o⇙" and "F⇘_{o}⇙ ≠ ∼⇧^{𝒬}A" and "F⇘_{o}⇙ ≠ A ∧⇧^{𝒬}B" and "F⇘_{o}⇙ ≠ A ∨⇧^{𝒬}B" and "F⇘_{o}⇙ ≠ A ⊃⇧^{𝒬}B" and "F⇘_{o}⇙ ≠ A ≡⇧^{𝒬}B" and "p⇘o⇙ ≠ ∼⇧^{𝒬}A" and "p⇘o⇙ ≠ A ∧⇧^{𝒬}B" and "p⇘o⇙ ≠ A ∨⇧^{𝒬}B" and "p⇘o⇙ ≠ A ⊃⇧^{𝒬}B" and "p⇘o⇙ ≠ A ≡⇧^{𝒬}B" and "∼⇧^{𝒬}A ≠ B ∧⇧^{𝒬}C" and "∼⇧^{𝒬}A ≠ B ∨⇧^{𝒬}C" and "∼⇧^{𝒬}A ≠ B ⊃⇧^{𝒬}C" and "¬ (B = F⇘_{o}⇙ ∧ A = C) ⟹ ∼⇧^{𝒬}A ≠ B ≡⇧^{𝒬}C" ― ‹\<^term>‹∼⇧^{𝒬}A› is the same as \<^term>‹F⇘_{o}⇙ ≡⇧^{𝒬}A›› and "A ∧⇧^{𝒬}B ≠ C ∨⇧^{𝒬}D" and "A ∧⇧^{𝒬}B ≠ C ⊃⇧^{𝒬}D" and "A ∧⇧^{𝒬}B ≠ C ≡⇧^{𝒬}D" and "A ∨⇧^{𝒬}B ≠ C ⊃⇧^{𝒬}D" and "A ∨⇧^{𝒬}B ≠ C ≡⇧^{𝒬}D" and "A ⊃⇧^{𝒬}B ≠ C ≡⇧^{𝒬}D" by simp_all lemma pwffs_injectivities [induct_simp]: shows "∼⇧^{𝒬}A = ∼⇧^{𝒬}A' ⟹ A = A'" and "A ∧⇧^{𝒬}B = A' ∧⇧^{𝒬}B' ⟹ A = A' ∧ B = B'" and "A ∨⇧^{𝒬}B = A' ∨⇧^{𝒬}B' ⟹ A = A' ∧ B = B'" and "A ⊃⇧^{𝒬}B = A' ⊃⇧^{𝒬}B' ⟹ A = A' ∧ B = B'" and "A ≡⇧^{𝒬}B = A' ≡⇧^{𝒬}B' ⟹ A = A' ∧ B = B'" by simp_all lemma pwff_from_neg_pwff [elim!]: assumes "∼⇧^{𝒬}A ∈ pwffs" shows "A ∈ pwffs" using assms by cases simp_all lemma pwffs_from_conj_pwff [elim!]: assumes "A ∧⇧^{𝒬}B ∈ pwffs" shows "{A, B} ⊆ pwffs" using assms by cases simp_all lemma pwffs_from_disj_pwff [elim!]: assumes "A ∨⇧^{𝒬}B ∈ pwffs" shows "{A, B} ⊆ pwffs" using assms by cases simp_all lemma pwffs_from_imp_pwff [elim!]: assumes "A ⊃⇧^{𝒬}B ∈ pwffs" shows "{A, B} ⊆ pwffs" using assms by cases simp_all lemma pwffs_from_eqv_pwff [elim!]: assumes "A ≡⇧^{𝒬}B ∈ pwffs" shows "{A, B} ⊆ pwffs" using assms by cases (simp_all, use F_pwff in fastforce) lemma pwffs_subset_of_wffso: shows "pwffs ⊆ wffs⇘o⇙" proof fix A assume "A ∈ pwffs" then show "A ∈ wffs⇘o⇙" by induction auto qed lemma pwff_free_vars_simps [simp]: shows T_fv: "free_vars T⇘_{o}⇙ = {}" and F_fv: "free_vars F⇘_{o}⇙ = {}" and var_fv: "free_vars (p⇘o⇙) = {(p, o)}" and neg_fv: "free_vars (∼⇧^{𝒬}A) = free_vars A" and conj_fv: "free_vars (A ∧⇧^{𝒬}B) = free_vars A ∪ free_vars B" and disj_fv: "free_vars (A ∨⇧^{𝒬}B) = free_vars A ∪ free_vars B" and imp_fv: "free_vars (A ⊃⇧^{𝒬}B) = free_vars A ∪ free_vars B" and eqv_fv: "free_vars (A ≡⇧^{𝒬}B) = free_vars A ∪ free_vars B" by force+ lemma pwffs_free_vars_are_propositional: assumes "A ∈ pwffs" and "v ∈ free_vars A" obtains p where "v = (p, o)" using assms by (induction A arbitrary: thesis) auto lemma is_free_for_in_pwff [intro]: assumes "A ∈ pwffs" and "v ∈ free_vars A" shows "is_free_for B v A" using assms proof (induction A) case (neg_pwff C) then show ?case using is_free_for_in_neg by simp next case (conj_pwff C D) from conj_pwff.prems consider (a) "v ∈ free_vars C" and "v ∈ free_vars D" | (b) "v ∈ free_vars C" and "v ∉ free_vars D" | (c) "v ∉ free_vars C" and "v ∈ free_vars D" by auto then show ?case proof cases case a then show ?thesis using conj_pwff.IH by (intro is_free_for_in_conj) next case b have "is_free_for B v C" by (fact conj_pwff.IH(1)[OF b(1)]) moreover from b(2) have "is_free_for B v D" using is_free_at_in_free_vars by blast ultimately show ?thesis by (rule is_free_for_in_conj) next case c from c(1) have "is_free_for B v C" using is_free_at_in_free_vars by blast moreover have "is_free_for B v D" by (fact conj_pwff.IH(2)[OF c(2)]) ultimately show ?thesis by (rule is_free_for_in_conj) qed next case (disj_pwff C D) from disj_pwff.prems consider (a) "v ∈ free_vars C" and "v ∈ free_vars D" | (b) "v ∈ free_vars C" and "v ∉ free_vars D" | (c) "v ∉ free_vars C" and "v ∈ free_vars D" by auto then show ?case proof cases case a then show ?thesis using disj_pwff.IH by (intro is_free_for_in_disj) next case b have "is_free_for B v C" by (fact disj_pwff.IH(1)[OF b(1)]) moreover from b(2) have "is_free_for B v D" using is_free_at_in_free_vars by blast ultimately show ?thesis by (rule is_free_for_in_disj) next case c from c(1) have "is_free_for B v C" using is_free_at_in_free_vars by blast moreover have "is_free_for B v D" by (fact disj_pwff.IH(2)[OF c(2)]) ultimately show ?thesis by (rule is_free_for_in_disj) qed next case (imp_pwff C D) from imp_pwff.prems consider (a) "v ∈ free_vars C" and "v ∈ free_vars D" | (b) "v ∈ free_vars C" and "v ∉ free_vars D" | (c) "v ∉ free_vars C" and "v ∈ free_vars D" by auto then show ?case proof cases case a then show ?thesis using imp_pwff.IH by (intro is_free_for_in_imp) next case b have "is_free_for B v C" by (fact imp_pwff.IH(1)[OF b(1)]) moreover from b(2) have "is_free_for B v D" using is_free_at_in_free_vars by blast ultimately show ?thesis by (rule is_free_for_in_imp) next case c from c(1) have "is_free_for B v C" using is_free_at_in_free_vars by blast moreover have "is_free_for B v D" by (fact imp_pwff.IH(2)[OF c(2)]) ultimately show ?thesis by (rule is_free_for_in_imp) qed next case (eqv_pwff C D) from eqv_pwff.prems consider (a) "v ∈ free_vars C" and "v ∈ free_vars D" | (b) "v ∈ free_vars C" and "v ∉ free_vars D" | (c) "v ∉ free_vars C" and "v ∈ free_vars D" by auto then show ?case proof cases case a then show ?thesis using eqv_pwff.IH by (intro is_free_for_in_equivalence) next case b have "is_free_for B v C" by (fact eqv_pwff.IH(1)[OF b(1)]) moreover from b(2) have "is_free_for B v D" using is_free_at_in_free_vars by blast ultimately show ?thesis by (rule is_free_for_in_equivalence) next case c from c(1) have "is_free_for B v C" using is_free_at_in_free_vars by blast moreover have "is_free_for B v D" by (fact eqv_pwff.IH(2)[OF c(2)]) ultimately show ?thesis by (rule is_free_for_in_equivalence) qed qed auto subsection ‹Semantics› text ‹Assignment of truth values to propositional variables:› definition is_tv_assignment :: "(nat ⇒ V) ⇒ bool" where [iff]: "is_tv_assignment φ ⟷ (∀p. φ p ∈ elts 𝔹)" text ‹Denotation of a pwff:› definition is_pwff_denotation_function where [iff]: "is_pwff_denotation_function 𝒱 ⟷ ( ∀φ. is_tv_assignment φ ⟶ ( 𝒱 φ T⇘_{o}⇙ = ❙T∧ 𝒱 φ F⇘_{o}⇙ = ❙F∧ (∀p. 𝒱 φ (p⇘o⇙) = φ p) ∧ (∀A. A ∈ pwffs ⟶ 𝒱 φ (∼⇧^{𝒬}A) = ∼ 𝒱 φ A) ∧ (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ∧⇧^{𝒬}B) = 𝒱 φ A ❙∧𝒱 φ B) ∧ (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ∨⇧^{𝒬}B) = 𝒱 φ A ❙∨𝒱 φ B) ∧ (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ⊃⇧^{𝒬}B) = 𝒱 φ A ❙⊃𝒱 φ B) ∧ (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ≡⇧^{𝒬}B) = 𝒱 φ A ❙≡𝒱 φ B) ) )" lemma pwff_denotation_is_truth_value: assumes "A ∈ pwffs" and "is_tv_assignment φ" and "is_pwff_denotation_function 𝒱" shows "𝒱 φ A ∈ elts 𝔹" using assms(1) proof induction case (neg_pwff A) then have "𝒱 φ (∼⇧^{𝒬}A) = ∼ 𝒱 φ A" using assms(2,3) by auto then show ?case using neg_pwff.IH by auto next case (conj_pwff A B) then have "𝒱 φ (A ∧⇧^{𝒬}B) = 𝒱 φ A ❙∧𝒱 φ B" using assms(2,3) by auto then show ?case using conj_pwff.IH by auto next case (disj_pwff A B) then have "𝒱 φ (A ∨⇧^{𝒬}B) = 𝒱 φ A ❙∨𝒱 φ B" using assms(2,3) by auto then show ?case using disj_pwff.IH by auto next case (imp_pwff A B) then have "𝒱 φ (A ⊃⇧^{𝒬}B) = 𝒱 φ A ❙⊃𝒱 φ B" using assms(2,3) by blast then show ?case using imp_pwff.IH by auto next case (eqv_pwff A B) then have "𝒱 φ (A ≡⇧^{𝒬}B) = 𝒱 φ A ❙≡𝒱 φ B" using assms(2,3) by blast then show ?case using eqv_pwff.IH by auto qed (use assms(2,3) in auto) lemma closed_pwff_is_meaningful_regardless_of_assignment: assumes "A ∈ pwffs" and "free_vars A = {}" and "is_tv_assignment φ" and "is_tv_assignment ψ" and "is_pwff_denotation_function 𝒱" shows "𝒱 φ A = 𝒱 ψ A" using assms(1,2) proof induction case T_pwff have "𝒱 φ T⇘_{o}⇙ = ❙T" using assms(3,5) by blast also have "… = 𝒱 ψ T⇘_{o}⇙" using assms(4,5) by force finally show ?case . next case F_pwff have "𝒱 φ F⇘_{o}⇙ = ❙F" using assms(3,5) by blast also have "… = 𝒱 ψ F⇘_{o}⇙" using assms(4,5) by force finally show ?case . next case (var_pwff p) ― ‹impossible case› then show ?case by simp next case (neg_pwff A) from ‹free_vars (∼⇧^{𝒬}A) = {}› have "free_vars A = {}" by simp have "𝒱 φ (∼⇧^{𝒬}A) = ∼ 𝒱 φ A" using assms(3,5) and neg_pwff.hyps by auto also from ‹free_vars A = {}› have "… = ∼ 𝒱 ψ A" using assms(3-5) and neg_pwff.IH by presburger also have "… = 𝒱 ψ (∼⇧^{𝒬}A)" using assms(4,5) and neg_pwff.hyps by simp finally show ?case . next case (conj_pwff A B) from ‹free_vars (A ∧⇧^{𝒬}B) = {}› have "free_vars A = {}" and "free_vars B = {}" by simp_all have "𝒱 φ (A ∧⇧^{𝒬}B) = 𝒱 φ A ❙∧𝒱 φ B" using assms(3,5) and conj_pwff.hyps(1,2) by auto also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙∧𝒱 ψ B" using conj_pwff.IH(1,2) by presburger also have "… = 𝒱 ψ (A ∧⇧^{𝒬}B)" using assms(4,5) and conj_pwff.hyps(1,2) by fastforce finally show ?case . next case (disj_pwff A B) from ‹free_vars (A ∨⇧^{𝒬}B) = {}› have "free_vars A = {}" and "free_vars B = {}" by simp_all have "𝒱 φ (A ∨⇧^{𝒬}B) = 𝒱 φ A ❙∨𝒱 φ B" using assms(3,5) and disj_pwff.hyps(1,2) by auto also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙∨𝒱 ψ B" using disj_pwff.IH(1,2) by presburger also have "… = 𝒱 ψ (A ∨⇧^{𝒬}B)" using assms(4,5) and disj_pwff.hyps(1,2) by fastforce finally show ?case . next case (imp_pwff A B) from ‹free_vars (A ⊃⇧^{𝒬}B) = {}› have "free_vars A = {}" and "free_vars B = {}" by simp_all have "𝒱 φ (A ⊃⇧^{𝒬}B) = 𝒱 φ A ❙⊃𝒱 φ B" using assms(3,5) and imp_pwff.hyps(1,2) by auto also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙⊃𝒱 ψ B" using imp_pwff.IH(1,2) by presburger also have "… = 𝒱 ψ (A ⊃⇧^{𝒬}B)" using assms(4,5) and imp_pwff.hyps(1,2) by fastforce finally show ?case . next case (eqv_pwff A B) from ‹free_vars (A ≡⇧^{𝒬}B) = {}› have "free_vars A = {}" and "free_vars B = {}" by simp_all have "𝒱 φ (A ≡⇧^{𝒬}B) = 𝒱 φ A ❙≡𝒱 φ B" using assms(3,5) and eqv_pwff.hyps(1,2) by auto also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙≡𝒱 ψ B" using eqv_pwff.IH(1,2) by presburger also have "… = 𝒱 ψ (A ≡⇧^{𝒬}B)" using assms(4,5) and eqv_pwff.hyps(1,2) by fastforce finally show ?case . qed inductive 𝒱⇩_{B}_graph for φ where 𝒱⇩_{B}_graph_T: "𝒱⇩_{B}_graph φ T⇘_{o}⇙ ❙T" | 𝒱⇩_{B}_graph_F: "𝒱⇩_{B}_graph φ F⇘_{o}⇙ ❙F" | 𝒱⇩_{B}_graph_var: "𝒱⇩_{B}_graph φ (p⇘o⇙) (φ p)" | 𝒱⇩_{B}_graph_neg: "𝒱⇩_{B}_graph φ (∼⇧^{𝒬}A) (∼ b⇩_{A})" if "𝒱⇩_{B}_graph φ A b⇩_{A}" | 𝒱⇩_{B}_graph_conj: "𝒱⇩_{B}_graph φ (A ∧⇧^{𝒬}B) (b⇩_{A}❙∧b⇩_{B})" if "𝒱⇩_{B}_graph φ A b⇩_{A}" and "𝒱⇩_{B}_graph φ B b⇩_{B}" | 𝒱⇩_{B}_graph_disj: "𝒱⇩_{B}_graph φ (A ∨⇧^{𝒬}B) (b⇩_{A}❙∨b⇩_{B})" if "𝒱⇩_{B}_graph φ A b⇩_{A}" and "𝒱⇩_{B}_graph φ B b⇩_{B}" | 𝒱⇩_{B}_graph_imp: "𝒱⇩_{B}_graph φ (A ⊃⇧^{𝒬}B) (b⇩_{A}❙⊃b⇩_{B})" if "𝒱⇩_{B}_graph φ A b⇩_{A}" and "𝒱⇩_{B}_graph φ B b⇩_{B}" | 𝒱⇩_{B}_graph_eqv: "𝒱⇩_{B}_graph φ (A ≡⇧^{𝒬}B) (b⇩_{A}❙≡b⇩_{B})" if "𝒱⇩_{B}_graph φ A b⇩_{A}" and "𝒱⇩_{B}_graph φ B b⇩_{B}" and "A ≠ F⇘_{o}⇙" lemmas [intro!] = 𝒱⇩_{B}_graph.intros lemma 𝒱⇩_{B}_graph_denotation_is_truth_value [elim!]: assumes "𝒱⇩_{B}_graph φ A b" and "is_tv_assignment φ" shows "b ∈ elts 𝔹" using assms proof induction case (𝒱⇩_{B}_graph_neg A b⇩_{A}) show ?case using 𝒱⇩_{B}_graph_neg.IH[OF assms(2)] by force next case (𝒱⇩_{B}_graph_conj A b⇩_{A}B b⇩_{B}) then show ?case using 𝒱⇩_{B}_graph_conj.IH and assms(2) by force next case (𝒱⇩_{B}_graph_disj A b⇩_{A}B b⇩_{B}) then show ?case using 𝒱⇩_{B}_graph_disj.IH and assms(2) by force next case (𝒱⇩_{B}_graph_imp A b⇩_{A}B b⇩_{B}) then show ?case using 𝒱⇩_{B}_graph_imp.IH and assms(2) by force next case (𝒱⇩_{B}_graph_eqv A b⇩_{A}B b⇩_{B}) then show ?case using 𝒱⇩_{B}_graph_eqv.IH and assms(2) by force qed simp_all lemma 𝒱⇩_{B}_graph_denotation_uniqueness: assumes "A ∈ pwffs" and "is_tv_assignment φ" and "𝒱⇩_{B}_graph φ A b" and "𝒱⇩_{B}_graph φ A b'" shows "b = b'" using assms(3,1,4) proof (induction arbitrary: b') case 𝒱⇩_{B}_graph_T from ‹𝒱⇩_{B}_graph φ T⇘_{o}⇙ b'› show ?case by (cases rule: 𝒱⇩_{B}_graph.cases) simp_all next case 𝒱⇩_{B}_graph_F from ‹𝒱⇩_{B}_graph φ F⇘_{o}⇙ b'› show ?case by (cases rule: 𝒱⇩_{B}_graph.cases) simp_all next case (𝒱⇩_{B}_graph_var p) from ‹𝒱⇩_{B}_graph φ (p⇘o⇙) b'› show ?case by (cases rule: 𝒱⇩_{B}_graph.cases) simp_all next case (𝒱⇩_{B}_graph_neg A b⇩_{A}) with ‹𝒱⇩_{B}_graph φ (∼⇧^{𝒬}A) b'› have "𝒱⇩_{B}_graph φ A (∼ b')" proof (cases rule: 𝒱⇩_{B}_graph.cases) case (𝒱⇩_{B}_graph_neg A' b⇩_{A}) from ‹∼⇧^{𝒬}A = ∼⇧^{𝒬}A'› have "A = A'" by simp with ‹𝒱⇩_{B}_graph φ A' b⇩_{A}› have "𝒱⇩_{B}_graph φ A b⇩_{A}" by simp moreover have "b⇩_{A}= ∼ b'" proof - have "b⇩_{A}∈ elts 𝔹" by (fact 𝒱⇩_{B}_graph_denotation_is_truth_value[OF 𝒱⇩_{B}_graph_neg(3) assms(2)]) moreover from ‹b⇩_{A}∈ elts 𝔹› and 𝒱⇩_{B}_graph_neg(2) have "∼ b' ∈ elts 𝔹" by fastforce ultimately show ?thesis using 𝒱⇩_{B}_graph_neg(2) by fastforce qed ultimately show ?thesis by blast qed simp_all moreover from 𝒱⇩_{B}_graph_neg.prems(1) have "A ∈ pwffs" by (force elim: pwffs.cases) moreover have "b⇩_{A}∈ elts 𝔹" and "b' ∈ elts 𝔹" and "b⇩_{A}= ∼ b'" proof - show "b⇩_{A}∈ elts 𝔹" by (fact 𝒱⇩_{B}_graph_denotation_is_truth_value[OF ‹𝒱⇩_{B}_graph φ A b⇩_{A}› assms(2)]) show "b' ∈ elts 𝔹" by (fact 𝒱⇩_{B}_graph_denotation_is_truth_value[OF ‹𝒱⇩_{B}_graph φ (∼⇧^{𝒬}A) b'› assms(2)]) show "b⇩_{A}= ∼ b'" by (fact 𝒱⇩_{B}_graph_neg(2)[OF ‹A ∈ pwffs› ‹𝒱⇩_{B}_graph φ A (∼ b')›]) qed ultimately show ?case by force next case (𝒱⇩_{B}_graph_conj A b⇩_{A}B b⇩_{B}) with ‹𝒱⇩_{B}_graph φ (A ∧⇧^{𝒬}B) b'› obtain b⇩_{A}' and b⇩_{B}' where "b' = b⇩_{A}' ❙∧b⇩_{B}'" and "𝒱⇩_{B}_graph φ A b⇩_{A}'" and "𝒱⇩_{B}_graph φ B b⇩_{B}'" by (cases rule: 𝒱⇩_{B}_graph.cases) simp_all moreover have "A ∈ pwffs" and "B ∈ pwffs" using pwffs_from_conj_pwff[OF 𝒱⇩_{B}_graph_conj.prems(1)] by blast+ ultimately show ?case using 𝒱⇩_{B}_graph_conj.IH and 𝒱⇩_{B}_graph_conj.prems(2) by blast next case (𝒱⇩_{B}_graph_disj A b⇩_{A}B b⇩_{B}) from ‹𝒱⇩_{B}_graph φ (A ∨⇧^{𝒬}B) b'› obtain b⇩_{A}' and b⇩_{B}' where "b' = b⇩_{A}' ❙∨b⇩_{B}'" and "𝒱⇩_{B}_graph φ A b⇩_{A}'" and "𝒱⇩_{B}_graph φ B b⇩_{B}'" by (cases rule: 𝒱⇩_{B}_graph.cases) simp_all moreover have "A ∈ pwffs" and "B ∈ pwffs" using pwffs_from_disj_pwff[OF 𝒱⇩_{B}_graph_disj.prems(1)] by blast+ ultimately show ?case using 𝒱⇩_{B}_graph_disj.IH and 𝒱⇩_{B}_graph_disj.prems(2) by blast next case (𝒱⇩_{B}_graph_imp A b⇩_{A}B b⇩_{B}) from ‹𝒱⇩_{B}_graph φ (A ⊃⇧^{𝒬}B) b'› obtain b⇩_{A}' and b⇩_{B}' where "b' = b⇩_{A}' ❙⊃b⇩_{B}'" and "𝒱⇩_{B}_graph φ A b⇩_{A}'" and "𝒱⇩_{B}_graph φ B b⇩_{B}'" by (cases rule: 𝒱⇩_{B}_graph.cases) simp_all moreover have "A ∈ pwffs" and "B ∈ pwffs" using pwffs_from_imp_pwff[OF 𝒱⇩_{B}_graph_imp.prems(1)] by blast+ ultimately show ?case using 𝒱⇩_{B}_graph_imp.IH and 𝒱⇩_{B}_graph_imp.prems(2) by blast next case (𝒱⇩_{B}_graph_eqv A b⇩_{A}B b⇩_{B}) with ‹𝒱⇩_{B}_graph φ (A ≡⇧^{𝒬}B) b'› obtain b⇩_{A}' and b⇩_{B}' where "b' = b⇩_{A}' ❙≡b⇩_{B}'" and "𝒱⇩_{B}_graph φ A b⇩_{A}'" and "𝒱⇩_{B}_graph φ B b⇩_{B}'" by (cases rule: 𝒱⇩_{B}_graph.cases) simp_all moreover have "A ∈ pwffs" and "B ∈ pwffs" using pwffs_from_eqv_pwff[OF 𝒱⇩_{B}_graph_eqv.prems(1)] by blast+ ultimately show ?case using 𝒱⇩_{B}_graph_eqv.IH and 𝒱⇩_{B}_graph_eqv.prems(2) by blast qed lemma 𝒱⇩_{B}_graph_denotation_existence: assumes "A ∈ pwffs" and "is_tv_assignment φ" shows "∃b. 𝒱⇩_{B}_graph φ A b" using assms proof induction case (eqv_pwff A B) then obtain b⇩_{A}and b⇩_{B}where "𝒱⇩_{B}_graph φ A b⇩_{A}" and "𝒱⇩_{B}_graph φ B b⇩_{B}" by blast then show ?case proof (cases "A ≠ F⇘_{o}⇙") case True then show ?thesis using eqv_pwff.IH and eqv_pwff.prems by blast next case False then have "A = F⇘_{o}⇙" by blast then show ?thesis using 𝒱⇩_{B}_graph_neg[OF ‹𝒱⇩_{B}_graph φ B b⇩_{B}›] by auto qed qed blast+ lemma 𝒱⇩_{B}_graph_is_functional: assumes "A ∈ pwffs" and "is_tv_assignment φ" shows "∃!b. 𝒱⇩_{B}_graph φ A b" using assms and 𝒱⇩_{B}_graph_denotation_existence and 𝒱⇩_{B}_graph_denotation_uniqueness by blast definition 𝒱⇩_{B}:: "(nat ⇒ V) ⇒ form ⇒ V" where [simp]: "𝒱⇩_{B}φ A = (THE b. 𝒱⇩_{B}_graph φ A b)" lemma 𝒱⇩_{B}_equality: assumes "A ∈ pwffs" and "is_tv_assignment φ" and "𝒱⇩_{B}_graph φ A b" shows "𝒱⇩_{B}φ A = b" unfolding 𝒱⇩_{B}_def using assms using 𝒱⇩_{B}_graph_denotation_uniqueness by blast lemma 𝒱⇩_{B}_graph_𝒱⇩_{B}: assumes "A ∈ pwffs" and "is_tv_assignment φ" shows "𝒱⇩_{B}_graph φ A (𝒱⇩_{B}φ A)" using 𝒱⇩_{B}_equality[OF assms] and 𝒱⇩_{B}_graph_is_functional[OF assms] by blast named_theorems 𝒱⇩_{B}_simps lemma 𝒱⇩_{B}_T [𝒱⇩_{B}_simps]: assumes "is_tv_assignment φ" shows "𝒱⇩_{B}φ T⇘_{o}⇙ = ❙T" by (rule 𝒱⇩_{B}_equality[OF T_pwff assms], intro 𝒱⇩_{B}_graph_T) lemma 𝒱⇩_{B}_F [𝒱⇩_{B}_simps]: assumes "is_tv_assignment φ" shows "𝒱⇩_{B}φ F⇘_{o}⇙ = ❙F" by (rule 𝒱⇩_{B}_equality[OF F_pwff assms], intro 𝒱⇩_{B}_graph_F) lemma 𝒱⇩_{B}_var [𝒱⇩_{B}_simps]: assumes "is_tv_assignment φ" shows "𝒱⇩_{B}φ (p⇘o⇙) = φ p" by (rule 𝒱⇩_{B}_equality[OF var_pwff assms], intro 𝒱⇩_{B}_graph_var) lemma 𝒱⇩_{B}_neg [𝒱⇩_{B}_simps]: assumes "A ∈ pwffs" and "is_tv_assignment φ" shows "𝒱⇩_{B}φ (∼⇧^{𝒬}A) = ∼ 𝒱⇩_{B}φ A" by (rule 𝒱⇩_{B}_equality[OF neg_pwff[OF assms(1)] assms(2)], intro 𝒱⇩_{B}_graph_neg 𝒱⇩_{B}_graph_𝒱⇩_{B}[OF assms]) lemma 𝒱⇩_{B}_disj [𝒱⇩_{B}_simps]: assumes "A ∈ pwffs" and "B ∈ pwffs" and "is_tv_assignment φ" shows "𝒱⇩_{B}φ (A ∨⇧^{𝒬}B) = 𝒱⇩_{B}φ A ❙∨𝒱⇩_{B}φ B" proof - from assms(1,3) have "𝒱⇩_{B}_graph φ A (𝒱⇩_{B}φ A)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) moreover from assms(2,3) have "𝒱⇩_{B}_graph φ B (𝒱⇩_{B}φ B)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) ultimately have "𝒱⇩_{B}_graph φ (A ∨⇧^{𝒬}B) (𝒱⇩_{B}φ A ❙∨𝒱⇩_{B}φ B)" by (intro 𝒱⇩_{B}_graph_disj) with assms show ?thesis using disj_pwff by (intro 𝒱⇩_{B}_equality) qed lemma 𝒱⇩_{B}_conj [𝒱⇩_{B}_simps]: assumes "A ∈ pwffs" and "B ∈ pwffs" and "is_tv_assignment φ" shows "𝒱⇩_{B}φ (A ∧⇧^{𝒬}B) = 𝒱⇩_{B}φ A ❙∧𝒱⇩_{B}φ B" proof - from assms(1,3) have "𝒱⇩_{B}_graph φ A (𝒱⇩_{B}φ A)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) moreover from assms(2,3) have "𝒱⇩_{B}_graph φ B (𝒱⇩_{B}φ B)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) ultimately have "𝒱⇩_{B}_graph φ (A ∧⇧^{𝒬}B) (𝒱⇩_{B}φ A ❙∧𝒱⇩_{B}φ B)" by (intro 𝒱⇩_{B}_graph_conj) with assms show ?thesis using conj_pwff by (intro 𝒱⇩_{B}_equality) qed lemma 𝒱⇩_{B}_imp [𝒱⇩_{B}_simps]: assumes "A ∈ pwffs" and "B ∈ pwffs" and "is_tv_assignment φ" shows "𝒱⇩_{B}φ (A ⊃⇧^{𝒬}B) = 𝒱⇩_{B}φ A ❙⊃𝒱⇩_{B}φ B" proof - from assms(1,3) have "𝒱⇩_{B}_graph φ A (𝒱⇩_{B}φ A)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) moreover from assms(2,3) have "𝒱⇩_{B}_graph φ B (𝒱⇩_{B}φ B)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) ultimately have "𝒱⇩_{B}_graph φ (A ⊃⇧^{𝒬}B) (𝒱⇩_{B}φ A ❙⊃𝒱⇩_{B}φ B)" by (intro 𝒱⇩_{B}_graph_imp) with assms show ?thesis using imp_pwff by (intro 𝒱⇩_{B}_equality) qed lemma 𝒱⇩_{B}_eqv [𝒱⇩_{B}_simps]: assumes "A ∈ pwffs" and "B ∈ pwffs" and "is_tv_assignment φ" shows "𝒱⇩_{B}φ (A ≡⇧^{𝒬}B) = 𝒱⇩_{B}φ A ❙≡𝒱⇩_{B}φ B" proof (cases "A = F⇘_{o}⇙") case True then show ?thesis using 𝒱⇩_{B}_F[OF assms(3)] and 𝒱⇩_{B}_neg[OF assms(2,3)] by force next case False from assms(1,3) have "𝒱⇩_{B}_graph φ A (𝒱⇩_{B}φ A)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) moreover from assms(2,3) have "𝒱⇩_{B}_graph φ B (𝒱⇩_{B}φ B)" by (intro 𝒱⇩_{B}_graph_𝒱⇩_{B}) ultimately have "𝒱⇩_{B}_graph φ (A ≡⇧^{𝒬}B) (𝒱⇩_{B}φ A ❙≡𝒱⇩_{B}φ B)" using False by (intro 𝒱⇩_{B}_graph_eqv) with assms show ?thesis using eqv_pwff by (intro 𝒱⇩_{B}_equality) qed declare pwffs.intros [𝒱⇩_{B}_simps] lemma pwff_denotation_function_existence: shows "is_pwff_denotation_function 𝒱⇩_{B}" using 𝒱⇩_{B}_simps by simp text ‹Tautologies:› definition is_tautology :: "form ⇒ bool" where [iff]: "is_tautology A ⟷ A ∈ pwffs ∧ (∀φ. is_tv_assignment φ ⟶ 𝒱⇩_{B}φ A = ❙T)" lemma tautology_is_wffo: assumes "is_tautology A" shows "A ∈ wffs⇘o⇙" using assms and pwffs_subset_of_wffso by blast lemma propositional_implication_reflexivity_is_tautology: shows "is_tautology (p⇘o⇙ ⊃⇧^{𝒬}p⇘o⇙)" using 𝒱⇩_{B}_simps by simp lemma propositional_principle_of_simplification_is_tautology: shows "is_tautology (p⇘o⇙ ⊃⇧^{𝒬}(r⇘o⇙ ⊃⇧^{𝒬}p⇘o⇙))" using 𝒱⇩_{B}_simps by simp lemma closed_pwff_denotation_uniqueness: assumes "A ∈ pwffs" and "free_vars A = {}" obtains b where "∀φ. is_tv_assignment φ ⟶ 𝒱⇩_{B}φ A = b" using assms by (meson closed_pwff_is_meaningful_regardless_of_assignment pwff_denotation_function_existence) lemma pwff_substitution_simps: shows "❙S{(p, o) ↣ A} T⇘_{o}⇙ = T⇘_{o}⇙" and "❙S{(p, o) ↣ A} F⇘_{o}⇙ = F⇘_{o}⇙" and "❙S{(p, o) ↣ A} (p'⇘o⇙) = (if p = p' then A else (p'⇘o⇙))" and "❙S{(p, o) ↣ A} (∼⇧^{𝒬}B) = ∼⇧^{𝒬}(❙S{(p, o) ↣ A} B)" and "❙S{(p, o) ↣ A} (B ∧⇧^{𝒬}C) = (❙S{(p, o) ↣ A} B) ∧⇧^{𝒬}(❙S{(p, o) ↣ A} C)" and "❙S{(p, o) ↣ A} (B ∨⇧^{𝒬}C) = (❙S{(p, o) ↣ A} B) ∨⇧^{𝒬}(❙S{(p, o) ↣ A} C)" and "❙S{(p, o) ↣ A} (B ⊃⇧^{𝒬}C) = (❙S{(p, o) ↣ A} B) ⊃⇧^{𝒬}(❙S{(p, o) ↣ A} C)" and "❙S{(p, o) ↣ A} (B ≡⇧^{𝒬}C) = (❙S{(p, o) ↣ A} B) ≡⇧^{𝒬}(❙S{(p, o) ↣ A} C)" by simp_all lemma pwff_substitution_in_pwffs: assumes "A ∈ pwffs" and "B ∈ pwffs" shows "❙S{(p, o) ↣ A} B ∈ pwffs" using assms(2) proof induction case T_pwff then show ?case using pwffs.T_pwff by simp next case F_pwff then show ?case using pwffs.F_pwff by simp next case (var_pwff p) from assms(1) show ?case using pwffs.var_pwff by simp next case (neg_pwff A) then show ?case using pwff_substitution_simps(4) and pwffs.neg_pwff by simp next case (conj_pwff A B) then show ?case using pwff_substitution_simps(5) and pwffs.conj_pwff by simp next case (disj_pwff A B) then show ?case using pwff_substitution_simps(6) and pwffs.disj_pwff by simp next case (imp_pwff A B) then show ?case using pwff_substitution_simps(7) and pwffs.imp_pwff by simp next case (eqv_pwff A B) then show ?case using pwff_substitution_simps(8) and pwffs.eqv_pwff by simp qed lemma pwff_substitution_denotation: assumes "A ∈ pwffs" and "B ∈ pwffs" and "is_tv_assignment φ" shows "𝒱⇩_{B}φ (❙S{(p, o) ↣ A} B) = 𝒱⇩_{B}(φ(p := 𝒱⇩_{B}φ A)) B" proof - from assms(1,3) have "is_tv_assignment (φ(p := 𝒱⇩_{B}φ A))" using 𝒱⇩_{B}_graph_denotation_is_truth_value[OF 𝒱⇩_{B}_graph_𝒱⇩_{B}] by simp with assms(2,1,3) show ?thesis using 𝒱⇩_{B}_simps and pwff_substitution_in_pwffs by induction auto qed lemma pwff_substitution_tautology_preservation: assumes "is_tautology B" and "A ∈ pwffs" and "(p, o) ∈ free_vars B" shows "is_tautology (❙S{(p, o) ↣ A} B)" proof (safe, fold is_tv_assignment_def) from assms(1,2) show "❙S{(p, o) ↣ A} B ∈ pwffs" using pwff_substitution_in_pwffs by blast next fix φ assume "is_tv_assignment φ" with assms(1,2) have "𝒱⇩_{B}φ (❙S{(p, o) ↣ A} B) = 𝒱⇩_{B}(φ(p := 𝒱⇩_{B}φ A)) B" using pwff_substitution_denotation by blast moreover from ‹is_tv_assignment φ› and assms(2) have "is_tv_assignment (φ(p := 𝒱⇩_{B}φ A))" using 𝒱⇩_{B}_graph_denotation_is_truth_value[OF 𝒱⇩_{B}_graph_𝒱⇩_{B}] by simp with assms(1) have "𝒱⇩_{B}(φ(p := 𝒱⇩_{B}φ A)) B = ❙T" by fastforce ultimately show "𝒱⇩_{B}φ ❙S{(p, o) ↣ A} B = ❙T" by (simp only:) qed lemma closed_pwff_substitution_free_vars: assumes "A ∈ pwffs" and "B ∈ pwffs" and "free_vars A = {}" and "(p, o) ∈ free_vars B" shows "free_vars (❙S{(p, o) ↣ A} B) = free_vars B - {(p, o)}" (is ‹free_vars (❙S?θ B) = _›) using assms(2,4) proof induction case (conj_pwff C D) have "free_vars (❙S?θ (C ∧⇧^{𝒬}D)) = free_vars ((❙S?θ C) ∧⇧^{𝒬}(❙S?θ D))" by simp also have "… = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" by (fact conj_fv) finally have *: "free_vars (❙S?θ (C ∧⇧^{𝒬}D)) = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" . from conj_pwff.prems consider (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D" | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D" | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D" by auto from this and * and conj_pwff.IH show ?case using free_var_singleton_substitution_neutrality by cases auto next case (disj_pwff C D) have "free_vars (❙S?θ (C ∨⇧^{𝒬}D)) = free_vars ((❙S?θ C) ∨⇧^{𝒬}(❙S?θ D))" by simp also have "… = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" by (fact disj_fv) finally have *: "free_vars (❙S?θ (C ∨⇧^{𝒬}D)) = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" . from disj_pwff.prems consider (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D" | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D" | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D" by auto from this and * and disj_pwff.IH show ?case using free_var_singleton_substitution_neutrality by cases auto next case (imp_pwff C D) have "free_vars (❙S?θ (C ⊃⇧^{𝒬}D)) = free_vars ((❙S?θ C) ⊃⇧^{𝒬}(❙S?θ D))" by simp also have "… = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" by (fact imp_fv) finally have *: "free_vars (❙S?θ (C ⊃⇧^{𝒬}D)) = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" . from imp_pwff.prems consider (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D" | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D" | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D" by auto from this and * and imp_pwff.IH show ?case using free_var_singleton_substitution_neutrality by cases auto next case (eqv_pwff C D) have "free_vars (❙S?θ (C ≡⇧^{𝒬}D)) = free_vars ((❙S?θ C) ≡⇧^{𝒬}(❙S?θ D))" by simp also have "… = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" by (fact eqv_fv) finally have *: "free_vars (❙S?θ (C ≡⇧^{𝒬}D)) = free_vars (❙S?θ C) ∪ free_vars (❙S?θ D)" . from eqv_pwff.prems consider (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D" | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D" | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D" by auto from this and * and eqv_pwff.IH show ?case using free_var_singleton_substitution_neutrality by cases auto qed (use assms(3) in ‹force+›) text ‹Substitution in a pwff:› definition is_pwff_substitution where [iff]: "is_pwff_substitution θ ⟷ is_substitution θ ∧ (∀(x, α) ∈ fmdom' θ. α = o)" text ‹Tautologous pwff:› definition is_tautologous :: "form ⇒ bool" where [iff]: "is_tautologous B ⟷ (∃θ A. is_tautology A ∧ is_pwff_substitution θ ∧ B = ❙Sθ A)" lemma tautologous_is_wffo: assumes "is_tautologous A" shows "A ∈ wffs⇘o⇙" using assms and substitution_preserves_typing and tautology_is_wffo by blast lemma implication_reflexivity_is_tautologous: assumes "A ∈ wffs⇘o⇙" shows "is_tautologous (A ⊃⇧^{𝒬}A)" proof - let ?θ = "{(𝔵, o) ↣ A}" have "is_tautology (𝔵⇘o⇙ ⊃⇧^{𝒬}𝔵⇘o⇙)" by (fact propositional_implication_reflexivity_is_tautology) moreover have "is_pwff_substitution ?θ" using assms by auto moreover have "A ⊃⇧^{𝒬}A = ❙S?θ (𝔵⇘o⇙ ⊃⇧^{𝒬}𝔵⇘o⇙)" by simp ultimately show ?thesis by blast qed lemma principle_of_simplification_is_tautologous: assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙" shows "is_tautologous (A ⊃⇧^{𝒬}(B ⊃⇧^{𝒬}A))" proof - let ?θ = "{(𝔵, o) ↣ A, (𝔶, o) ↣ B}" have "is_tautology (𝔵⇘o⇙ ⊃⇧^{𝒬}(𝔶⇘o⇙ ⊃⇧^{𝒬}𝔵⇘o⇙))" by (fact propositional_principle_of_simplification_is_tautology) moreover have "is_pwff_substitution ?θ" using assms by auto moreover have "A ⊃⇧^{𝒬}(B ⊃⇧^{𝒬}A) = ❙S?θ (𝔵⇘o⇙ ⊃⇧^{𝒬}(𝔶⇘o⇙ ⊃⇧^{𝒬}𝔵⇘o⇙))" by simp ultimately show ?thesis by blast qed lemma pseudo_modus_tollens_is_tautologous: assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙" shows "is_tautologous ((A ⊃⇧^{𝒬}∼⇧^{𝒬}B) ⊃⇧^{𝒬}(B ⊃⇧^{𝒬}∼⇧^{𝒬}A))" proof - let ?θ = "{(𝔵, o) ↣ A, (𝔶, o) ↣ B}" have "is_tautology ((𝔵⇘o⇙ ⊃⇧^{𝒬}∼⇧^{𝒬}𝔶⇘o⇙) ⊃⇧^{𝒬}(𝔶⇘o⇙ ⊃⇧^{𝒬}∼⇧^{𝒬}𝔵⇘o⇙))" using 𝒱⇩_{B}_simps by (safe, fold is_tv_assignment_def, simp only:) simp moreover have "is_pwff_substitution ?θ" using assms by auto moreover have "(A ⊃⇧^{𝒬}∼⇧^{𝒬}B) ⊃⇧^{𝒬}(B ⊃⇧^{𝒬}∼⇧^{𝒬}A) = ❙S?θ ((𝔵⇘o⇙ ⊃⇧^{𝒬}∼⇧^{𝒬}𝔶⇘o⇙) ⊃⇧^{𝒬}(𝔶⇘o⇙ ⊃⇧^{𝒬}∼⇧^{𝒬}𝔵⇘o⇙))" by simp ultimately show ?thesis by blast qed end