# Theory PropLog

```(*  Title:      HOL/Induct/PropLog.thy
Author:     Tobias Nipkow
Copyright   1994  TU Muenchen & University of Cambridge
*)

section ‹Meta-theory of propositional logic›

theory PropLog imports Main begin

text ‹
Datatype definition of propositional logic formulae and inductive
definition of the propositional tautologies.

Inductive definition of propositional logic.  Soundness and
completeness w.r.t.\ truth-tables.

Prove: If ‹H ⊨ p› then ‹G ⊨ p› where ‹G ∈
Fin(H)›
›

subsection ‹The datatype of propositions›

datatype 'a pl =
false
| var 'a ("#_" )
| imp "'a pl" "'a pl" (infixr "⇀" 90)

subsection ‹The proof system›

inductive thms :: "['a pl set, 'a pl] ⇒ bool"  (infixl "⊢" 50)
for H :: "'a pl set"
where
H: "p ∈ H ⟹ H ⊢ p"
| K: "H ⊢ p⇀q⇀p"
| S: "H ⊢ (p⇀q⇀r) ⇀ (p⇀q) ⇀ p⇀r"
| DN: "H ⊢ ((p⇀false) ⇀ false) ⇀ p"
| MP: "⟦H ⊢ p⇀q; H ⊢ p⟧ ⟹ H ⊢ q"

subsection ‹The semantics›

subsubsection ‹Semantics of propositional logic.›

primrec eval :: "['a set, 'a pl] => bool"  ("_[[_]]" [100,0] 100)
where
"tt[[false]] = False"
| "tt[[#v]] = (v ∈ tt)"
| eval_imp: "tt[[p⇀q]] = (tt[[p]] ⟶ tt[[q]])"

text ‹
A finite set of hypotheses from ‹t› and the ‹Var›s in
‹p›.
›

primrec hyps :: "['a pl, 'a set] => 'a pl set"
where
"hyps false  tt = {}"
| "hyps (#v)   tt = {if v ∈ tt then #v else #v⇀false}"
| "hyps (p⇀q) tt = hyps p tt Un hyps q tt"

subsubsection ‹Logical consequence›

text ‹
For every valuation, if all elements of ‹H› are true then so
is ‹p›.
›

definition sat :: "['a pl set, 'a pl] => bool"  (infixl "⊨" 50)
where "H ⊨ p = (∀tt. (∀q∈H. tt[[q]]) ⟶ tt[[p]])"

subsection ‹Proof theory of propositional logic›

lemma thms_mono:
assumes "G ⊆ H" shows "thms(G) ≤ thms(H)"
proof -
have "G ⊢ p ⟹ H ⊢ p" for p
by (induction rule: thms.induct) (use assms in ‹auto intro: thms.intros›)
then show ?thesis
by blast
qed

lemma thms_I: "H ⊢ p⇀p"
― ‹Called ‹I› for Identity Combinator, not for Introduction.›
by (best intro: thms.K thms.S thms.MP)

subsubsection ‹Weakening, left and right›

lemma weaken_left: "⟦G ⊆ H;  G⊢p⟧ ⟹ H⊢p"
― ‹Order of premises is convenient with ‹THEN››
by (meson predicate1D thms_mono)

lemma weaken_left_insert: "G ⊢ p ⟹ insert a G ⊢ p"
by (meson subset_insertI weaken_left)

lemma weaken_left_Un1: "G ⊢ p ⟹ G ∪ B ⊢ p"
by (rule weaken_left) (rule Un_upper1)

lemma weaken_left_Un2: "G ⊢ p ⟹ A ∪ G ⊢ p"
by (metis Un_commute weaken_left_Un1)

lemma weaken_right: "H ⊢ q ⟹ H ⊢ p⇀q"
using K MP by blast

subsubsection ‹The deduction theorem›

theorem deduction: "insert p H ⊢ q  ⟹  H ⊢ p⇀q"
proof (induct set: thms)
case (H p)
then show ?case
using thms.H thms_I weaken_right by fastforce
qed (metis thms.simps)+

subsubsection ‹The cut rule›

lemma cut: "insert p H ⊢ q ⟹ H ⊢ p ⟹ H ⊢ q"
using MP deduction by blast

lemma thms_falseE: "H ⊢ false ⟹ H ⊢ q"
by (metis thms.simps)

lemma thms_notE: "H ⊢ p ⇀ false ⟹ H ⊢ p ⟹ H ⊢ q"
using MP thms_falseE by blast

subsubsection ‹Soundness of the rules wrt truth-table semantics›

theorem soundness: "H ⊢ p ⟹ H ⊨ p"
by (induct set: thms) (auto simp: sat_def)

subsection ‹Completeness›

subsubsection ‹Towards the completeness proof›

lemma false_imp: "H ⊢ p⇀false ⟹ H ⊢ p⇀q"
by (metis thms.simps)

lemma imp_false:
"⟦H ⊢ p;  H ⊢ q⇀false⟧ ⟹ H ⊢ (p⇀q)⇀false"
by (meson MP S weaken_right)

lemma hyps_thms_if: "hyps p tt ⊢ (if tt[[p]] then p else p⇀false)"
― ‹Typical example of strengthening the induction statement.›
proof (induction p)
case (imp p1 p2)
then show ?case
by (metis (full_types) eval_imp false_imp hyps.simps(3) imp_false weaken_left_Un1 weaken_left_Un2 weaken_right)

lemma sat_thms_p: "{} ⊨ p ⟹ hyps p tt ⊢ p"
― ‹Key lemma for completeness; yields a set of assumptions
satisfying ‹p››
by (metis (full_types) empty_iff hyps_thms_if sat_def)

text ‹
For proving certain theorems in our new propositional logic.
›

declare deduction [intro!]
declare thms.H [THEN thms.MP, intro]

text ‹
The excluded middle in the form of an elimination rule.
›

lemma thms_excluded_middle: "H ⊢ (p⇀q) ⇀ ((p⇀false)⇀q) ⇀ q"
proof -
have "insert ((p ⇀ false) ⇀ q) (insert (p ⇀ q) H) ⊢ (q ⇀ false) ⇀ false"
by (best intro: H)
then show ?thesis
by (metis deduction thms.simps)
qed

lemma thms_excluded_middle_rule:
"⟦insert p H ⊢ q;  insert (p⇀false) H ⊢ q⟧ ⟹ H ⊢ q"
― ‹Hard to prove directly because it requires cuts›
by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto)

subsection‹Completeness -- lemmas for reducing the set of assumptions›

text ‹
For the case \<^prop>‹hyps p t - insert #v Y ⊢ p› we also have \<^prop>‹hyps p t - {#v} ⊆ hyps p (t-{v})›.
›

lemma hyps_Diff: "hyps p (t-{v}) ⊆ insert (#v⇀false) ((hyps p t)-{#v})"
by (induct p) auto

text ‹
For the case \<^prop>‹hyps p t - insert (#v ⇀ Fls) Y ⊢ p› we also have
\<^prop>‹hyps p t-{#v⇀Fls} ⊆ hyps p (insert v t)›.
›

lemma hyps_insert: "hyps p (insert v t) ⊆ insert (#v) (hyps p t-{#v⇀false})"
by (induct p) auto

text ‹Two lemmas for use with ‹weaken_left››

lemma insert_Diff_same: "B-C ⊆ insert a (B-insert a C)"
by fast

lemma insert_Diff_subset2: "insert a (B-{c}) - D ⊆ insert a (B-insert c D)"
by fast

text ‹
The set \<^term>‹hyps p t› is finite, and elements have the form
\<^term>‹#v› or \<^term>‹#v⇀Fls›.
›

lemma hyps_finite: "finite(hyps p t)"
by (induct p) auto

lemma hyps_subset: "hyps p t ⊆ (UN v. {#v, #v⇀false})"
by (induct p) auto

lemma Diff_weaken_left: "A ⊆ C ⟹ A - B ⊢ p ⟹ C - B ⊢ p"
by (rule Diff_mono [OF _ subset_refl, THEN weaken_left])

subsubsection ‹Completeness theorem›

text ‹
Induction on the finite set of assumptions \<^term>‹hyps p t0›.  We
may repeatedly subtract assumptions until none are left!
›

lemma completeness_0:
assumes "{} ⊨ p"
shows "{} ⊢ p"
proof -
{ fix t t0
have "hyps p t - hyps p t0 ⊢ p"
using hyps_finite hyps_subset
proof (induction arbitrary: t rule: finite_subset_induct)
case empty
then show ?case
next
case (insert q H)
then consider v where "q = #v" | v where "q = #v ⇀ false"
by blast
then show ?case
proof cases
case 1
then show ?thesis
by (metis (no_types, lifting) insert.IH thms_excluded_middle_rule insert_Diff_same
insert_Diff_subset2 weaken_left Diff_weaken_left hyps_Diff)
next
case 2
then show ?thesis
by (metis (no_types, lifting) insert.IH thms_excluded_middle_rule insert_Diff_same
insert_Diff_subset2 weaken_left Diff_weaken_left hyps_insert)
qed
qed
}
then show ?thesis
by (metis Diff_cancel)
qed

text‹A semantic analogue of the Deduction Theorem›
lemma sat_imp: "insert p H ⊨ q ⟹ H ⊨ p⇀q"
by (auto simp: sat_def)

theorem completeness: "finite H ⟹ H ⊨ p ⟹ H ⊢ p"
proof (induction arbitrary: p rule: finite_induct)
case empty
then show ?case