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 "\" 101)
primrec eval :: "(nat \ bool) \ formula \ bool"
where
"eval v (Atom a) = v a"
| "eval v Fls = False"
| "eval v (\ \ \) = ((eval v \) \ eval v \)"
definition tautology :: "formula \ bool"
where "tautology \ \ (\ v. eval v \)"
definition satisfies :: "(nat \ bool) \ formula set \ bool" ("_ sats _" [80,80] 80)
where "v sats \ \ (\ \ \ \. eval v \)"
definition satisfiable :: "formula set \ bool"
where "satisfiable \ \ (\ v. v sats \)"
definition implies :: "formula set \ formula \ bool" ("_ \ _" [80,80] 80)
where "\ \ \ \ (\ v. v sats \ \ eval v \ = True)"
subsection "Natural deduction"
definition Neg :: "formula \ formula" ("\") where
"\ \ \ \ \ Fls"
declare Neg_def[simp]
inductive deduction :: "formula set \ formula \ bool" ("_ \ _" [100,100] 100)
where
hyp: "\ \ \ \ \ \ \ \ \"
| imp_elim: "\ \ \ (\ \ \); \ \ \ \ \ \ \ \"
| imp_intro: "\ insert \ \ \ \ \ \ \ \ \ \ \"
| false_elim: "\ \ Fls \ \ \ \"
| excluded_middle: "\ insert \ \ \ \; insert (\ \) \ \ \ \ \ \ \ \"
constdefs emp :: "nat \ formula"
"emp \ (\ x. (Atom x))"
subsection "Basic properties of the proof system"
lemma weakening: assumes gp: "\ \ \" and gd: "\ \ \" shows "\ \ \"
using gp gd
proof (induct arbitrary: \ rule: deduction.induct)
fix \ and \ and \::"formula set" assume ps: "\ \ \" and sd: "\ \ \"
from ps sd have "\ \ \" by blast
thus "\ \ \" by (rule hyp)
next
fix \ \ \ \
assume "\ \ \ \ \" and IH1: "\\. \ \ \ \ \ \ \ \ \"
and "\ \ \" and IH2: "\\. \ \ \ \ \ \ \" and sd: "\ \ \"
from IH1 sd have pp: "\ \ \ \ \" by simp
from IH2 sd have dp: "\ \ \" by simp
from pp dp show "\ \ \" by (rule imp_elim)
next
fix \ \ \ \
assume IH: "\\. insert \ \ \ \ \ \ \ \"
and sd: "\ \ \"
show "\ \ \ \ \"
proof (rule imp_intro)
from sd have sd2: "insert \ \ \ insert \ \" by blast
with IH show "insert \ \ \ \" by blast
qed
next
fix \ \ and \::"formula set"
assume IH: "\\. \ \ \ \ \ \ Fls" and sd: "\ \ \"
from IH sd have "\ \ Fls" by simp
thus "\ \ \" by (rule false_elim)
next
fix \ \ \ \
assume IH1: "\\. insert \ \ \ \ \ \ \ \"
and IH2: "\\. insert (\ \) \ \ \ \ \ \ \