Impressum PropLog.thy Sprache: Isabelle

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

section \<open>Meta-theory of propositional logic\<close>

theory PropLog imports Main begin

text \<open>
  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 \<open>H \<Turnstile> p\<close> then \<open>G \<Turnstile> p\<close> where \<open>G \<in>
  Fin(H)\<close>
\<close>

subsection \<open>The datatype of propositions\<close>

datatype 'a pl =
    false
  | var 'a (\#_\ [1000])
  | imp "'a pl" "'a pl" (infixr \<open>\<rightharpoonup>\<close> 90)

subsection \<open>The proof system\<close>

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 \<open>The semantics\<close>

subsubsection \<open>Semantics of propositional logic.\<close>

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

text \<open>
  A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in
  \<open>p\<close>.
\<close>

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 \<open>Logical consequence\<close>

text \<open>
  For every valuation, if all elements of \<open>H\<close> are true then so
  is \<open>p\<close>.
\<close>

definition sat :: "['a pl set, 'a pl] => bool"  (infixl \<open>\<Turnstile>\<close> 50)
  where "H \ p = (\tt. (\q\H. tt[[q]]) \ tt[[p]])"

subsection \<open>Proof theory of propositional logic\<close>

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 \<open>auto intro: thms.intros\<close>)
  then show ?thesis
    by blast
qed

lemma thms_I: "H \ p\p"
  \<comment> \<open>Called \<open>I\<close> for Identity Combinator, not for Introduction.\<close>
  by (best intro: thms.K thms.S thms.MP)

subsubsection \<open>Weakening, left and right\<close>

lemma weaken_left: "\G \ H; G\p\ \ H\p"
  \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close>
  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 \<open>The deduction theorem\<close>

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 \<open>The cut rule\<close>

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 \<open>Soundness of the rules wrt truth-table semantics\<close>

theorem soundness: "H \ p \ H \ p"
  by (induct set: thms) (auto simp: sat_def)

subsection \<open>Completeness\<close>

subsubsection \<open>Towards the completeness proof\<close>

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)"
  \<comment> \<open>Typical example of strengthening the induction statement.\<close>
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"
  \<comment> \<open>Key lemma for completeness; yields a set of assumptions
        satisfying \<open>p\<close>\<close>
  by (metis (full_types) empty_iff hyps_thms_if sat_def)

text \<open>
  For proving certain theorems in our new propositional logic.
\<close>

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

text \<open>
  The excluded middle in the form of an elimination rule.
\<close>

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"
  \<comment> \<open>Hard to prove directly because it requires cuts\<close>
  by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto)

subsection\<open>Completeness -- lemmas for reducing the set of assumptions\<close>

text \<open>
  For the case \<^prop>\<open>hyps p t - insert #v Y \<turnstile> p\<close> we also have \<^prop>\<open>hyps p t - {#v} \<subseteq> hyps p (t-{v})\<close>.
\<close>

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

text \<open>
  For the case \<^prop>\<open>hyps p t - insert (#v \<rightharpoonup> Fls) Y \<turnstile> p\<close> we also have
  \<^prop>\<open>hyps p t-{#v\<rightharpoonup>Fls} \<subseteq> hyps p (insert v t)\<close>.
\<close>

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

text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close>

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 \<open>
  The set \<^term>\<open>hyps p t\<close> is finite, and elements have the form
  \<^term>\<open>#v\<close> or \<^term>\<open>#v\<rightharpoonup>Fls\<close>.
\<close>

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 \<open>Completeness theorem\<close>

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

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\<open>A semantic analogue of the Deduction Theorem\<close>
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

quality98%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.