section \<open>Propositional Logic - Soundness and Completeness\<close>

text \<open>
Soundness and completeness of a logic establish that the syntactic notion
of provability is equivalent to the semantic notation of logical entailment.

In this project you will formally prove soundness and completeness of a specific
set of natural deduction rules for propositional logic.
\<close>

theory Project_Logic
  imports Main
begin

subsection \<open>Syntax and Semantics\<close>

text \<open>
Propositional formulas are defined by the following data type (that comes with some
syntactic sugar):
\<close>
type_synonym id = string
datatype form =
    Atom id
  | Bot ("\<bottom>\<^sub>p")
  | Neg form ("\<not>\<^sub>p _" [68] 68)
  | Conj form form (infixr "\<and>\<^sub>p" 67)
  | Disj form form (infixr "\<or>\<^sub>p" 67)
  | Impl form form (infixr "\<rightarrow>\<^sub>p" 66)


text \<open>
Define a function \<open>eval\<close> that evaluates the truth value of a formula with respect
to a given truth assignment.
\<close>
fun eval :: "(id \<Rightarrow> bool) \<Rightarrow> form \<Rightarrow> bool"
  where
    "eval v \<phi> \<longleftrightarrow> undefined"

text \<open>
Using @{const eval}, define semantic entailment of a formula from a list of formulas.
\<close>
definition entails :: "form list \<Rightarrow> form \<Rightarrow> bool" (infix "\<Turnstile>" 51)
  where
    "\<Gamma> \<Turnstile> \<phi> \<longleftrightarrow> undefined"


subsection \<open>Natural Deduction\<close>

text \<open>
The natural deduction rules we consider are captured by the following
inductive predicate \<open>proves P \<phi>\<close>, with infix syntax \<open>P \<turnstile> \<phi>\<close>, that holds
whenever a formula \<open>\<phi>\<close> is provable from a list of premises \<open>P\<close>.
\<close>
inductive proves (infix "\<turnstile>" 58)
  where
    premise: "\<phi> \<in> set P \<Longrightarrow> P \<turnstile> \<phi>"
  | conjI: "P \<turnstile> \<phi> \<Longrightarrow> P \<turnstile> \<psi> \<Longrightarrow> P \<turnstile> \<phi> \<and>\<^sub>p \<psi>"
  | conjE1: "P \<turnstile> \<phi> \<and>\<^sub>p \<psi> \<Longrightarrow> P \<turnstile> \<phi>"
  | conjE2: "P \<turnstile> \<phi> \<and>\<^sub>p \<psi> \<Longrightarrow> P \<turnstile> \<psi>"
  | impI: "\<phi> # P \<turnstile> \<psi> \<Longrightarrow> P \<turnstile> (\<phi> \<rightarrow>\<^sub>p \<psi>)"
  | impE: "P \<turnstile> \<phi> \<Longrightarrow> P \<turnstile> \<phi> \<rightarrow>\<^sub>p \<psi> \<Longrightarrow> P \<turnstile> \<psi>"
  | disjI1: "P \<turnstile> \<phi> \<Longrightarrow> P \<turnstile> \<phi> \<or>\<^sub>p \<psi>"
  | disjI2: "P \<turnstile> \<psi> \<Longrightarrow> P \<turnstile> \<phi> \<or>\<^sub>p \<psi>"
  | disjE: "P \<turnstile> \<phi> \<or>\<^sub>p \<psi> \<Longrightarrow> \<phi> # P \<turnstile> \<chi> \<Longrightarrow> \<psi> # P \<turnstile> \<chi> \<Longrightarrow> P \<turnstile> \<chi>"
  | negI: "\<phi> # P \<turnstile> \<bottom>\<^sub>p \<Longrightarrow> P \<turnstile> \<not>\<^sub>p \<phi>"
  | negE: "P \<turnstile> \<phi> \<Longrightarrow> P \<turnstile> \<not>\<^sub>p \<phi> \<Longrightarrow> P \<turnstile> \<bottom>\<^sub>p"
  | botE: "P \<turnstile> \<bottom>\<^sub>p \<Longrightarrow> P \<turnstile> \<phi>"
  | dnegE: "P \<turnstile> \<not>\<^sub>p\<not>\<^sub>p \<phi> \<Longrightarrow> P \<turnstile> \<phi>"

text \<open>
Prove that \<open>\<turnstile>\<close> is monotone with respect to premises, that is, we can arbitrarily
extend the list of premises in a valid prove.
\<close>
lemma proves_mono:
  assumes "P \<turnstile> \<phi>" and "set P \<subseteq> set Q"
  shows "Q \<turnstile> \<phi>"
  sorry

text \<open>
Prove the following derived natural deduction rules that might be useful later on:
\<close>
lemma dnegI:
  assumes "P \<turnstile> \<phi>"
  shows "P \<turnstile> \<not>\<^sub>p\<not>\<^sub>p \<phi>"
  sorry

lemma pbc:
  assumes "\<not>\<^sub>p \<phi> # P \<turnstile> \<bottom>\<^sub>p"
  shows "P \<turnstile> \<phi>"
  sorry

lemma lem:
  "P \<turnstile> \<phi> \<or>\<^sub>p \<not>\<^sub>p \<phi>"
  sorry

lemma neg_conj:
  assumes "\<chi> \<in> {\<phi>, \<psi>}" and "P \<turnstile> \<not>\<^sub>p \<chi>"
  shows "P \<turnstile> \<not>\<^sub>p (\<phi> \<and>\<^sub>p \<psi>)"
  sorry

lemma neg_disj:
  assumes "P \<turnstile> \<not>\<^sub>p \<phi>" and "P \<turnstile> \<not>\<^sub>p \<psi>"
  shows "P \<turnstile> \<not>\<^sub>p (\<phi> \<or>\<^sub>p \<psi>)"
  sorry

lemma trivial_imp:
  assumes "P \<turnstile> \<psi>"
  shows "P \<turnstile> \<phi> \<rightarrow>\<^sub>p \<psi>"
  sorry

lemma vacuous_imp:
  assumes "P \<turnstile> \<not>\<^sub>p \<phi>"
  shows "P \<turnstile> \<phi> \<rightarrow>\<^sub>p \<psi>"
  sorry

lemma neg_imp:
  assumes "P \<turnstile> \<phi>" and "P \<turnstile> \<not>\<^sub>p \<psi>"
  shows "P \<turnstile> \<not>\<^sub>p (\<phi> \<rightarrow>\<^sub>p \<psi>)"
  sorry


subsection \<open>Soundness\<close>

text \<open>
Prove soundness of \<open>\<turnstile>\<close> with respect to \<open>\<Turnstile>\<close>.
\<close>
lemma proves_sound:
  assumes "P \<turnstile> \<phi>"
  shows "P \<Turnstile> \<phi>"
  sorry


subsection \<open>Completeness\<close>

text \<open>
Prove completeness of \<open>\<turnstile>\<close> with respect to \<open>\<Turnstile>\<close> in absence of premises.
\<close>
lemma prove_complete_Nil:
  assumes "[] \<Turnstile> \<phi>"
  shows "[] \<turnstile> \<phi>"
  sorry

text \<open>
No extend the above result to also incorporate premises.
\<close>
lemma proves_complete:
  assumes "P \<Turnstile> \<phi>"
  shows "P \<turnstile> \<phi>"
  sorry

text \<open>
Conclude that semantic entailment is equivalent to provability.
\<close>
lemma entails_proves_conv:
  "P \<Turnstile> \<phi> \<longleftrightarrow> P \<turnstile> \<phi>"
  sorry

end