theory PropLogic
imports Main LaTeXsugar OptionalSugar
begin


section "Metatheory of Propositional Logic"

text{*

  We formalize the meaning of propositional formulas and
  define a proof system. We prove completeness of the proof system 
  via Kalmar's variable elimination method.
  The material in this section is based on several
  texts on Mathematical Logic~\cite{Bilaniuk:fk,Mendelson:1997lr}
  and Paulson's completeness proof in Isabelle/ZF~\cite{Paulson:1995fk}.

*}


subsection "Formulas and their meaning"

datatype formula
  = Atom nat
  | Fls
  | Implies formula formula   (infixr "\<rightarrow>" 101)

primrec eval :: "(nat \<Rightarrow> bool) \<Rightarrow> formula \<Rightarrow> bool"
where
  "eval v (Atom a) = v a"
  | "eval v Fls = False"
  | "eval v (\<phi> \<rightarrow> \<psi>) = ((eval v \<phi>) \<longrightarrow> eval v \<psi>)"

definition tautology :: "formula \<Rightarrow> bool"
  where "tautology \<phi> \<equiv> (\<forall> v. eval v \<phi>)"
definition satisfies :: "(nat \<Rightarrow> bool) \<Rightarrow> formula set \<Rightarrow> bool" ("_ sats _" [80,80] 80)
  where "v sats \<Sigma> \<equiv> (\<forall> \<phi> \<in> \<Sigma>. eval v \<phi>)"
definition satisfiable :: "formula set \<Rightarrow> bool"
  where "satisfiable \<Sigma> \<equiv> (\<exists> v. v sats \<Sigma>)"
definition implies :: "formula set \<Rightarrow> formula \<Rightarrow> bool" ("_ \<Turnstile> _" [80,80] 80)
  where "\<Sigma> \<Turnstile> \<phi> \<equiv> (\<forall> v. v sats \<Sigma> \<longrightarrow> eval v \<phi> = True)"

subsection "Natural deduction"

definition Neg :: "formula \<Rightarrow> formula" ("\<not>") where
  "\<not> \<phi> \<equiv> \<phi> \<rightarrow> Fls"
declare Neg_def[simp]

inductive deduction :: "formula set \<Rightarrow> formula \<Rightarrow> bool" ("_ \<turnstile> _" [100,100] 100)
  where
  hyp: "\<lbrakk> \<phi> \<in> \<Sigma> \<rbrakk> \<Longrightarrow> \<Sigma> \<turnstile> \<phi>"
  | imp_elim: "\<lbrakk> \<Sigma> \<turnstile> (\<phi> \<rightarrow> \<psi>); \<Sigma> \<turnstile> \<phi> \<rbrakk> \<Longrightarrow> \<Sigma> \<turnstile> \<psi>"
  | imp_intro: "\<lbrakk> insert \<phi> \<Sigma> \<turnstile> \<psi> \<rbrakk> \<Longrightarrow> \<Sigma> \<turnstile> \<phi> \<rightarrow> \<psi>"
  | false_elim: "\<Sigma> \<turnstile> Fls \<Longrightarrow> \<Sigma> \<turnstile> \<phi>"
  | excluded_middle: "\<lbrakk> insert \<phi> \<Sigma> \<turnstile> \<psi>; insert (\<not> \<phi>) \<Sigma> \<turnstile> \<psi> \<rbrakk> \<Longrightarrow> \<Sigma> \<turnstile> \<psi>"

constdefs emp :: "nat \<Rightarrow> formula"
  "emp \<equiv> (\<lambda> x. (Atom x))"

subsection "Basic properties of the proof system"

lemma weakening: assumes gp: "\<Gamma> \<turnstile> \<phi>" and gd: "\<Gamma> \<subseteq> \<Delta>" shows "\<Delta> \<turnstile> \<phi>"
using gp gd 
proof (induct arbitrary: \<Delta> rule: deduction.induct)
  fix \<phi> and \<Sigma> and \<Delta>::"formula set" assume ps: "\<phi> \<in> \<Sigma>" and sd: "\<Sigma> \<subseteq> \<Delta>"
  from ps sd have "\<phi> \<in> \<Delta>" by blast
  thus "\<Delta> \<turnstile> \<phi>" by (rule hyp)
next
  fix \<Sigma> \<phi> \<psi> \<Delta>
  assume "\<Sigma> \<turnstile> \<phi> \<rightarrow> \<psi>" and IH1: "\<And>\<Delta>. \<Sigma> \<subseteq> \<Delta> \<Longrightarrow> \<Delta> \<turnstile> \<phi> \<rightarrow> \<psi>"
    and "\<Sigma> \<turnstile> \<phi>" and IH2: "\<And>\<Delta>. \<Sigma> \<subseteq> \<Delta> \<Longrightarrow> \<Delta> \<turnstile> \<phi>" and sd: "\<Sigma> \<subseteq> \<Delta>"
  from IH1 sd have pp: "\<Delta> \<turnstile> \<phi> \<rightarrow> \<psi>" by simp
  from IH2 sd have dp: "\<Delta> \<turnstile> \<phi>" by simp
  from pp dp show "\<Delta> \<turnstile> \<psi>" by (rule imp_elim)
next
  fix \<phi> \<Sigma> \<psi> \<Delta>
  assume IH: "\<And>\<Delta>. insert \<phi> \<Sigma> \<subseteq> \<Delta> \<Longrightarrow> \<Delta> \<turnstile> \<psi>"
    and sd: "\<Sigma> \<subseteq> \<Delta>"
  show "\<Delta> \<turnstile> \<phi> \<rightarrow> \<psi>"
  proof (rule imp_intro)
    from sd have sd2: "insert \<phi> \<Sigma> \<subseteq> insert \<phi> \<Delta>" by blast
    with IH show "insert \<phi> \<Delta> \<turnstile> \<psi>" by blast
  qed
next
  fix \<Sigma> \<phi> and \<Delta>::"formula set"
  assume IH: "\<And>\<Delta>. \<Sigma> \<subseteq> \<Delta> \<Longrightarrow> \<Delta> \<turnstile> Fls" and sd: "\<Sigma> \<subseteq> \<Delta>"
  from IH sd have "\<Delta> \<turnstile> Fls" by simp 
  thus "\<Delta> \<turnstile> \<phi>" by (rule false_elim)
next
  fix \<phi> \<Sigma> \<psi> \<Delta>
  assume IH1: "\<And>\<Delta>. insert \<phi> \<Sigma> \<subseteq> \<Delta> \<Longrightarrow> \<Delta> \<turnstile> \<psi>"
    and IH2: "\<And>\<Delta>. insert (\<not> \<phi>) \<Sigma> \<subseteq> \<Delta> \<Longrightarrow> \<Delta> \<turnstile> \<psi>"
    and sd: "\<Sigma> \<subseteq> \<Delta>"
  from IH1 sd have 1: "insert \<phi> \<Delta> \<turnstile> \<psi>" by auto
  from IH2 sd have 2: "insert (\<not> \<phi>) \<Delta> \<turnstile> \<psi>" by auto
  from 1 2 show "\<Delta> \<turnstile> \<psi>" by (rule excluded_middle)
qed

theorem soundness: assumes d: "\<Delta> \<turnstile> \<phi>" shows "\<Delta> \<Turnstile> \<phi>"
  using d 
  by (induct rule: deduction.induct) (auto simp add: implies_def satisfies_def)

lemma lem_1_11_c: "\<Gamma> \<turnstile> (Neg \<phi> \<rightarrow> (\<phi> \<rightarrow> \<psi>))" 
proof (rule imp_intro)
  show "insert (\<not> \<phi>) \<Gamma> \<turnstile> \<phi> \<rightarrow> \<psi>"
  proof (rule imp_intro)
    let ?G = "insert \<phi> (insert (Neg \<phi>) \<Gamma>)"
    have 1: "?G \<turnstile> \<phi> \<rightarrow> Fls" by (rule hyp) simp
    have 2: "?G \<turnstile> \<phi>" by (rule hyp) simp
    from 1 2 have 3: "?G \<turnstile> Fls" by (rule imp_elim)
    from 3 show "?G \<turnstile> \<psi>" by (rule false_elim)
  qed
qed

lemma lem_1_11_f: "\<Gamma> \<turnstile> (\<phi> \<rightarrow> (Neg \<psi> \<rightarrow> Neg (\<phi> \<rightarrow> \<psi>)))" 
proof (rule imp_intro)
  show "insert \<phi> \<Gamma> \<turnstile> (Neg \<psi> \<rightarrow> Neg (\<phi> \<rightarrow> \<psi>))"
  proof (rule imp_intro)
    show "insert (Neg \<psi>) (insert \<phi> \<Gamma>) \<turnstile> Neg (\<phi> \<rightarrow> \<psi>)"
    proof (simp, rule imp_intro)
      let ?G = "insert (\<phi> \<rightarrow> \<psi>) (insert (\<psi> \<rightarrow> Fls) (insert \<phi> \<Gamma>))"
      have 1: "?G \<turnstile> \<phi>" by (rule hyp) simp
      have 2: "?G \<turnstile> \<phi> \<rightarrow> \<psi>" by (rule hyp) simp
      from 2 1 have 3: "?G \<turnstile> \<psi>" by (rule imp_elim)
      have 4: "?G \<turnstile> \<psi> \<rightarrow> Fls" by (rule hyp) simp
      from 4 3 show "?G \<turnstile> Fls" by (rule imp_elim)
    qed
  qed
qed


subsection "Completeness"

(*
  A basis of phi is a set of formulas H such that H |- phi.
  We'll show that for any valuation T, hyps T phi is a basis for phi.
*)
primrec hyps :: "nat set \<Rightarrow> formula \<Rightarrow> formula set"
  where
  "hyps T (Atom n) = (if n \<in> T then {Atom n} else {Neg (Atom n)})"
  | "hyps T Fls = {}"
  | "hyps T (\<phi> \<rightarrow> \<psi>) = hyps T \<phi> \<union> hyps T \<psi>"

lemma hyps_finite: "finite (hyps T \<phi>)"
  by (induct \<phi>, auto)

lemma hyps_member: "\<forall> T x. x \<in> hyps T \<phi> \<longrightarrow> (\<exists> \<alpha>. (x = Atom \<alpha> \<and> \<alpha> \<in> T)
     \<or> (x = Neg (Atom \<alpha>) \<and> \<alpha> \<notin> T))"
  by (induct \<phi>, auto)

lemma hyps_diff:
  "hyps (T-{\<alpha>}) \<phi> \<subseteq> insert (Neg (Atom \<alpha>)) ((hyps T \<phi>) - {Atom \<alpha>})"
  by (induct \<phi>, auto)

lemma hyps_cons:
    "hyps (insert \<alpha> T) \<phi> \<subseteq> insert (Atom \<alpha>) ((hyps T \<phi>)-{Neg (Atom \<alpha>)})"
  by (induct_tac \<phi>, auto)

definition flip :: "(nat set) \<Rightarrow> formula \<Rightarrow> formula"
  where "flip T \<phi> \<equiv> (if eval (\<lambda> x. x \<in> T) \<phi> then \<phi> else Neg \<phi>)"
lemma "eval (\<lambda> x. x \<in> T) (flip T \<phi>)" by (simp add: flip_def)

lemma kalmar[rule_format]:
  "\<forall> \<phi>. size \<phi> = n \<longrightarrow> hyps v \<phi> \<turnstile> flip v \<phi>"
  apply (induct rule: nat_less_induct)
  apply clarify
proof -
  fix n and \<phi>::formula
  assume IH: "\<forall> m<size \<phi>. \<forall> \<phi>. size \<phi> = m \<longrightarrow> hyps v \<phi> \<turnstile> flip v \<phi>"
  show "hyps v \<phi> \<turnstile> flip v \<phi>"
  proof (cases \<phi>)
    fix \<alpha> assume p: "\<phi> = Atom \<alpha>"
    thus ?thesis apply (simp add: flip_def) using hyp by blast
  next
    assume p: "\<phi> = Fls"
    have "hyps v \<phi> \<turnstile> Fls \<rightarrow> Fls" by (rule imp_intro, rule hyp, simp)
    with p show ?thesis by (simp add: flip_def)
  next
    fix \<psi>1 \<psi>2 assume p: "\<phi> = \<psi>1 \<rightarrow> \<psi>2"
    from p have s1: "size \<psi>1 < size \<phi>" by simp
    from s1 IH have IH1: "hyps v \<psi>1 \<turnstile> flip v \<psi>1" by blast
    from p have s2: "size \<psi>2 < size \<phi>" by simp
    from s2 IH have IH2: "hyps v \<psi>2 \<turnstile> flip v \<psi>2" by blast
    show ?thesis
    proof (cases "eval (\<lambda> x. x \<in> v) \<psi>1")
      assume ev1: "eval (\<lambda> x. x \<in> v) \<psi>1"
      from ev1 have f1: "flip v \<psi>1 = \<psi>1" by (simp add: flip_def)
      show ?thesis
      proof (cases "eval (\<lambda> x. x \<in> v) \<psi>2")
        assume ev2: "eval (\<lambda> x. x \<in> v) \<psi>2"
        from ev2 IH2 have ps2: "hyps v \<psi>2 \<turnstile> \<psi>2" by (simp add: flip_def)
	have "hyps v \<phi> \<turnstile> \<psi>1 \<rightarrow> \<psi>2" apply (rule imp_intro) 
	  using ps2 apply (rule weakening) using p by auto
	with p ev1 ev2 show ?thesis by (simp add: flip_def)
      next
	assume ev2: "\<not> eval (\<lambda> x. x \<in> v) \<psi>2"
	have 1: "hyps v \<phi> \<turnstile> (\<psi>1 \<rightarrow> (Neg \<psi>2 \<rightarrow> Neg (\<psi>1 \<rightarrow> \<psi>2)))" 
	  by (rule lem_1_11_f)
	from p IH1 ev1 have p1: "hyps v \<phi> \<turnstile> \<psi>1"
	  apply (simp add: flip_def) by (rule weakening) auto
	from p IH2 ev2 have p2: "hyps v \<phi> \<turnstile> Neg \<psi>2" 
	  apply (simp add: flip_def) by (rule weakening) auto
	from 1 p1 have "hyps v \<phi> \<turnstile> Neg \<psi>2 \<rightarrow> Neg (\<psi>1 \<rightarrow> \<psi>2)" 
	  using imp_elim by blast
	with p2 have "hyps v \<phi> \<turnstile> Neg (\<psi>1 \<rightarrow> \<psi>2)"  
	  using imp_elim by blast
	with p ev1 ev2 show ?thesis by (simp add: flip_def)
      qed
    next
      assume ev1: "\<not> eval (\<lambda> x. x \<in> v) \<psi>1"
      from ev1 p IH1 have ps1: "hyps v \<psi>1 \<turnstile> Neg \<psi>1" by (simp add: flip_def)
     have p12: "hyps v \<psi>1 \<turnstile> (Neg \<psi>1 \<rightarrow> (\<psi>1 \<rightarrow> \<psi>2))" by (rule lem_1_11_c)
      from p12 ps1 have "hyps v \<psi>1 \<turnstile> \<psi>1 \<rightarrow> \<psi>2" by (rule imp_elim)
      with p ev1 show ?thesis
	apply (simp add: flip_def) apply (rule weakening) by auto
    qed
  qed
qed

lemma variable_elimination:
  "finite H \<Longrightarrow> (\<forall> \<phi>. tautology \<phi> \<and> H \<subseteq> hyps T0 \<phi> \<longrightarrow>
     (\<forall> T.  (hyps T \<phi> - H) \<turnstile> \<phi>))"
  apply (induct rule: finite_induct) apply clarify defer apply clarify defer
proof -
  fix \<phi> T assume taut: "tautology \<phi>" 
  have "hyps T \<phi> \<turnstile> flip T \<phi>" apply (rule kalmar) by simp
  with taut show "(hyps T \<phi> - {}) \<turnstile> \<phi>" by (simp add: flip_def tautology_def)
next
  fix x H \<phi> T
  assume IH: "\<forall>\<phi>. tautology \<phi> \<and> H \<subseteq> hyps T0 \<phi> \<longrightarrow> (\<forall> T. (hyps T \<phi> - H) \<turnstile> \<phi>)"
    and taut: "tautology \<phi>" and xfh: "insert x H \<subseteq> hyps T0 \<phi>"
  from xfh obtain \<alpha> where X: "(x = Atom \<alpha> \<and> \<alpha> \<in> T0)
    \<or> (x = Neg (Atom \<alpha>) \<and> \<alpha> \<notin> T0)" using hyps_member by blast
  thus "(hyps T \<phi> - insert x H) \<turnstile> \<phi>"
  proof
    assume X: "x = Atom \<alpha> \<and> \<alpha> \<in> T0"
    show "(hyps T \<phi> - insert x H) \<turnstile> \<phi>"
    proof (rule excluded_middle[of "Atom \<alpha>"])
      from taut xfh IH have a: "(hyps T \<phi> - H) \<turnstile> \<phi>" by blast
      have b: "hyps T \<phi> - H \<subseteq> insert (Atom \<alpha>) (hyps T \<phi> - insert (Atom \<alpha>) H)"
        by blast
      from a b X show "insert (Atom \<alpha>) (hyps T \<phi> - insert x H) \<turnstile> \<phi>" 
        using weakening by blast
    next
      from taut xfh IH have a: "(hyps (T-{\<alpha>}) \<phi> - H) \<turnstile> \<phi>" by blast
      have "hyps (T-{\<alpha>}) \<phi> \<subseteq> insert (Neg (Atom \<alpha>)) ((hyps T \<phi>) - {Atom \<alpha>})"
        by (rule hyps_diff)
      with X have b: "(hyps (T-{\<alpha>}) \<phi>) - H
             \<subseteq> insert (Neg (Atom \<alpha>)) (hyps T \<phi> - insert (Atom \<alpha>) H)" 
        by blast
      from a b X show "insert (Neg (Atom \<alpha>)) (hyps T \<phi> - insert x H) \<turnstile> \<phi>" 
        using weakening by blast
    qed
  next
    assume X: "x = Neg (Atom \<alpha>) \<and> \<alpha> \<notin> T0"
    show "(hyps T \<phi> - insert x H) \<turnstile> \<phi>"
    proof (rule excluded_middle[of "Atom \<alpha>"])
      from taut xfh IH have a: "(hyps (insert \<alpha> T) \<phi> - H) \<turnstile> \<phi>" by blast
      have b: "hyps (insert \<alpha> T) \<phi> \<subseteq> insert (Atom \<alpha>) (hyps T \<phi> - {Neg (Atom \<alpha>)})" 
	by (rule hyps_cons)
      from b have c: "hyps (insert \<alpha> T) \<phi> - H
                      \<subseteq> insert (Atom \<alpha>) (hyps T \<phi> - insert (Neg (Atom \<alpha>)) H)" 
	by blast
      from a c X show "insert (Atom \<alpha>) (hyps T \<phi> - insert x H) \<turnstile> \<phi>" 
        using weakening by blast 
    next
      from taut xfh IH have a: "(hyps T \<phi> - H) \<turnstile> \<phi>" by blast
      have b: "hyps T \<phi> - H \<subseteq> insert (Neg (Atom \<alpha>)) 
   	                              (hyps T \<phi> - insert (Neg (Atom \<alpha>)) H)" 
	by blast
      from a b X show "insert (Neg (Atom \<alpha>)) (hyps T \<phi> - (insert x H)) \<turnstile> \<phi>" 
        using weakening by blast
    qed
  qed
qed

lemma tautology_implies_deducible:
  assumes taut: "tautology \<phi>" shows "{} \<turnstile> \<phi>"
proof -
  have "finite (hyps T \<phi>)" by (rule hyps_finite)
  with taut have "(hyps T \<phi> - hyps T \<phi>) \<turnstile> \<phi>" using variable_elimination by blast
  thus ?thesis by simp
qed

theorem completeness:
  assumes dp: "\<Delta> \<Turnstile> \<phi>" and fd: "finite \<Delta>" shows "\<Delta> \<turnstile> \<phi>"
using fd dp
proof (induct arbitrary: \<phi> rule: finite_induct)
  fix \<phi> assume "{} \<Turnstile> \<phi>" hence "tautology \<phi>" 
    by (simp add: implies_def tautology_def satisfies_def)
  thus "{} \<turnstile> \<phi>" by (rule tautology_implies_deducible)
next
  fix x F \<phi> assume fF: "finite F" and xF: "x \<notin> F" 
    and IH: "\<And> \<phi>. F \<Turnstile> \<phi> \<Longrightarrow> F \<turnstile> \<phi>" and xfp: "insert x F \<Turnstile> \<phi>"
  from xfp have fxp: "F \<Turnstile> x \<rightarrow> \<phi>" by (simp add: implies_def satisfies_def)
  from IH fxp have "F \<turnstile> x \<rightarrow> \<phi>" by simp
  hence xp: "insert x F \<turnstile> x \<rightarrow> \<phi>" apply (rule weakening) by auto
  have xx: "insert x F \<turnstile> x" apply (rule hyp) by simp
  from xp xx show "insert x F \<turnstile> \<phi>" by (rule imp_elim)
qed


end