# Theory PropLog

theory PropLog
imports ZF
```(*  Title:      ZF/Induct/PropLog.thy
Author:     Tobias Nipkow & Lawrence C Paulson
*)

section ‹Meta-theory of propositional logic›

theory PropLog imports ZF 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›

consts
propn :: i

datatype propn =
Fls
| Var ("n ∈ nat")    ("#_" [100] 100)
| Imp ("p ∈ propn", "q ∈ propn")    (infixr "=>" 90)

subsection ‹The proof system›

consts thms     :: "i => i"

abbreviation
thms_syntax :: "[i,i] => o"    (infixl "|-" 50)
where "H |- p == p ∈ thms(H)"

inductive
domains "thms(H)" ⊆ "propn"
intros
H:  "[| p ∈ H;  p ∈ propn |] ==> H |- p"
K:  "[| p ∈ propn;  q ∈ propn |] ==> H |- p=>q=>p"
S:  "[| p ∈ propn;  q ∈ propn;  r ∈ propn |]
==> H |- (p=>q=>r) => (p=>q) => p=>r"
DN: "p ∈ propn ==> H |- ((p=>Fls) => Fls) => p"
MP: "[| H |- p=>q;  H |- p;  p ∈ propn;  q ∈ propn |] ==> H |- q"
type_intros "propn.intros"

declare propn.intros [simp]

subsection ‹The semantics›

subsubsection ‹Semantics of propositional logic.›

consts
is_true_fun :: "[i,i] => i"
primrec
"is_true_fun(Fls, t) = 0"
"is_true_fun(Var(v), t) = (if v ∈ t then 1 else 0)"
"is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)"

definition
is_true :: "[i,i] => o"  where
"is_true(p,t) == is_true_fun(p,t) = 1"
― ‹this definition is required since predicates can't be recursive›

lemma is_true_Fls [simp]: "is_true(Fls,t) ⟷ False"

lemma is_true_Var [simp]: "is_true(#v,t) ⟷ v ∈ t"

lemma is_true_Imp [simp]: "is_true(p=>q,t) ⟷ (is_true(p,t)⟶is_true(q,t))"

subsubsection ‹Logical consequence›

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

definition
logcon :: "[i,i] => o"    (infixl "|=" 50)  where
"H |= p == ∀t. (∀q ∈ H. is_true(q,t)) ⟶ is_true(p,t)"

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

consts
hyps :: "[i,i] => i"
primrec
"hyps(Fls, t) = 0"
"hyps(Var(v), t) = (if v ∈ t then {#v} else {#v=>Fls})"
"hyps(p=>q, t) = hyps(p,t) ∪ hyps(q,t)"

subsection ‹Proof theory of propositional logic›

lemma thms_mono: "G ⊆ H ==> thms(G) ⊆ thms(H)"
apply (unfold thms.defs)
apply (rule lfp_mono)
apply (rule thms.bnd_mono)+
apply (assumption | rule univ_mono basic_monos)+
done

lemmas thms_in_pl = thms.dom_subset [THEN subsetD]

inductive_cases ImpE: "p=>q ∈ propn"

lemma thms_MP: "[| H |- p=>q;  H |- p |] ==> H |- q"
― ‹Stronger Modus Ponens rule: no typechecking!›
apply (rule thms.MP)
apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
done

lemma thms_I: "p ∈ propn ==> H |- p=>p"
― ‹Rule is called ‹I› for Identity Combinator, not for Introduction.›
apply (rule thms.S [THEN thms_MP, THEN thms_MP])
apply (rule_tac [5] thms.K)
apply (rule_tac [4] thms.K)
apply simp_all
done

subsubsection ‹Weakening, left and right›

lemma weaken_left: "[| G ⊆ H;  G|-p |] ==> H|-p"
― ‹Order of premises is convenient with ‹THEN››
by (erule thms_mono [THEN subsetD])

lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p"
by (erule subset_consI [THEN weaken_left])

lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]

lemma weaken_right: "[| H |- q;  p ∈ propn |] ==> H |- p=>q"
by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)

subsubsection ‹The deduction theorem›

theorem deduction: "[| cons(p,H) |- q;  p ∈ propn |] ==>  H |- p=>q"
apply (erule thms.induct)
apply (blast intro: thms_I thms.H [THEN weaken_right])
apply (blast intro: thms.K [THEN weaken_right])
apply (blast intro: thms.S [THEN weaken_right])
apply (blast intro: thms.DN [THEN weaken_right])
apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
done

subsubsection ‹The cut rule›

lemma cut: "[| H|-p;  cons(p,H) |- q |] ==>  H |- q"
apply (rule deduction [THEN thms_MP])
done

lemma thms_FlsE: "[| H |- Fls; p ∈ propn |] ==> H |- p"
apply (rule thms.DN [THEN thms_MP])
apply (rule_tac [2] weaken_right)
done

lemma thms_notE: "[| H |- p=>Fls;  H |- p;  q ∈ propn |] ==> H |- q"
by (erule thms_MP [THEN thms_FlsE])

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

theorem soundness: "H |- p ==> H |= p"
apply (unfold logcon_def)
apply (induct set: thms)
apply auto
done

subsection ‹Completeness›

subsubsection ‹Towards the completeness proof›

lemma Fls_Imp: "[| H |- p=>Fls; q ∈ propn |] ==> H |- p=>q"
apply (frule thms_in_pl)
apply (rule deduction)
apply (rule weaken_left_cons [THEN thms_notE])
apply (blast intro: thms.H elim: ImpE)+
done

lemma Imp_Fls: "[| H |- p;  H |- q=>Fls |] ==> H |- (p=>q)=>Fls"
apply (frule thms_in_pl)
apply (frule thms_in_pl [of concl: "q=>Fls"])
apply (rule deduction)
apply (erule weaken_left_cons [THEN thms_MP])
apply (rule consI1 [THEN thms.H, THEN thms_MP])
apply (blast intro: weaken_left_cons elim: ImpE)+
done

lemma hyps_thms_if:
"p ∈ propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
― ‹Typical example of strengthening the induction statement.›
apply simp
apply (induct_tac p)
apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2])
apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
done

lemma logcon_thms_p: "[| p ∈ propn;  0 |= p |] ==> hyps(p,t) |- p"
― ‹Key lemma for completeness; yields a set of assumptions satisfying ‹p››
apply (drule hyps_thms_if)
done

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

lemmas propn_SIs = propn.intros deduction
and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]

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

lemma thms_excluded_middle:
"[| p ∈ propn;  q ∈ propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
apply (rule deduction [THEN deduction])
apply (rule thms.DN [THEN thms_MP])
apply (best intro!: propn_SIs intro: propn_Is)+
done

lemma thms_excluded_middle_rule:
"[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p ∈ propn |] ==> H |- q"
― ‹Hard to prove directly because it requires cuts›
apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
apply (blast intro!: propn_SIs intro: propn_Is)+
done

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

text ‹
For the case @{prop "hyps(p,t)-cons(#v,Y) |- p"} we also have @{prop
"hyps(p,t)-{#v} ⊆ hyps(p, t-{v})"}.
›

lemma hyps_Diff:
"p ∈ propn ==> hyps(p, t-{v}) ⊆ cons(#v=>Fls, hyps(p,t)-{#v})"
by (induct set: propn) auto

text ‹
For the case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} we also have
@{prop "hyps(p,t)-{#v=>Fls} ⊆ hyps(p, cons(v,t))"}.
›

lemma hyps_cons:
"p ∈ propn ==> hyps(p, cons(v,t)) ⊆ cons(#v, hyps(p,t)-{#v=>Fls})"
by (induct set: propn) auto

text ‹Two lemmas for use with ‹weaken_left››

lemma cons_Diff_same: "B-C ⊆ cons(a, B-cons(a,C))"
by blast

lemma cons_Diff_subset2: "cons(a, B-{c}) - D ⊆ cons(a, B-cons(c,D))"
by blast

text ‹
The set @{term "hyps(p,t)"} is finite, and elements have the form
@{term "#v"} or @{term "#v=>Fls"}; could probably prove the stronger
@{prop "hyps(p,t) ∈ Fin(hyps(p,0) ∪ hyps(p,nat))"}.
›

lemma hyps_finite: "p ∈ propn ==> hyps(p,t) ∈ Fin(⋃v ∈ nat. {#v, #v=>Fls})"
by (induct set: propn) auto

lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]

text ‹
Induction on the finite set of assumptions @{term "hyps(p,t0)"}.  We
may repeatedly subtract assumptions until none are left!
›

lemma completeness_0_lemma [rule_format]:
"[| p ∈ propn;  0 |= p |] ==> ∀t. hyps(p,t) - hyps(p,t0) |- p"
apply (frule hyps_finite)
apply (erule Fin_induct)
txt ‹inductive step›
apply safe
txt ‹Case @{prop "hyps(p,t)-cons(#v,Y) |- p"}›
apply (rule thms_excluded_middle_rule)
apply (erule_tac [3] propn.intros)
apply (blast intro: cons_Diff_same [THEN weaken_left])
apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
hyps_Diff [THEN Diff_weaken_left])
txt ‹Case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"}›
apply (rule thms_excluded_middle_rule)
apply (erule_tac [3] propn.intros)
apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
hyps_cons [THEN Diff_weaken_left])
apply (blast intro: cons_Diff_same [THEN weaken_left])
done

subsubsection ‹Completeness theorem›

lemma completeness_0: "[| p ∈ propn;  0 |= p |] ==> 0 |- p"
― ‹The base case for completeness›
apply (rule Diff_cancel [THEN subst])
apply (blast intro: completeness_0_lemma)
done

lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
― ‹A semantic analogue of the Deduction Theorem›

lemma completeness:
"H ∈ Fin(propn) ==> p ∈ propn ⟹ H |= p ⟹ H |- p"
apply (induct arbitrary: p set: Fin)
apply (safe intro!: completeness_0)
apply (rule weaken_left_cons [THEN thms_MP])
apply (blast intro!: logcon_Imp propn.intros)
apply (blast intro: propn_Is)
done

theorem thms_iff: "H ∈ Fin(propn) ==> H |- p ⟷ H |= p ∧ p ∈ propn"
by (blast intro: soundness completeness thms_in_pl)

end
```