Quelle  PropLog.thy   Sprache: Isabelle

(*  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 (\#_\ [1000])
  | 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)

qed (simp_all add: thms_I thms.H)

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 🍋‹hyps p t - insert #v Y ⊨ p› we also have 🍋‹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 🍋‹hyps p t - insert (#v ⇀ Fls) Y ⊨ p› we also have
  🍋‹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 🍋‹hyps p t› is finite, and elements have the form
  🍋‹#v› or 🍋‹#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 🍋‹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
        by (simp add: assms sat_thms_p)
    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
    by (simp add: completeness_0)
next
  case insert
  then show ?case
    by (meson H MP insertI1 sat_imp weaken_left_insert)
qed

theorem syntax_iff_semantics: "finite H \ (H \ p) = (H \ p)"
  by (blast intro: soundness completeness)

end