Quelle  PropLog.thy

(*  Title:      ZF/Induct/PropLog.thy
  Author: Tobias Nipkow & Lawrence C Paulson
  Copyright 1993 University of Cambridge
*)

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"
  by (simp add: is_true_def)

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

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


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)"
    unfolding 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])
    apply (simp_all add: thms_in_pl)
  done

lemma thms_FlsE: "[H |- Fls; p ∈ propn] ==> H |- p"
  apply (rule thms.DN [THEN thms_MP])
   apply (rule_tac [2] weaken_right)
    apply (simp_all add: propn.intros)
  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"
    unfolding 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 (simp_all add: thms_I thms.H)
  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)
  apply (simp add: logcon_def)
  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 🍋‹hyps(p,t)-cons(#v,Y) |- p› we also have 🍋‹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 🍋‹hyps(p,t)-cons(#v ==> Fls,Y) |- p› we also have
  🍋‹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 🍋‹hyps(p,t)› is finite, and elements have the form
  🍋‹#v› or 🍋‹#v==>Fls›; could probably prove the stronger
  🍋‹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 🍋‹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)
   apply (simp add: logcon_thms_p Diff_0)
  txt ‹inductive step›
  apply safe
   txt ‹Case 🍋‹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 🍋‹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›
  by (simp add: logcon_def)

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