Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/ZF/Induct/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 12 kB

Quelle PropLog.thy Sprache: Isabelle

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

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

theory PropLog imports ZF 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 |= p\<close> then \<open>G |= p\<close> where \<open>G \<in>
  Fin(H)\<close>
\<close>

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

consts
  propn :: i

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

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

consts thms     :: "i \ i"

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

inductive
  domains "thms(H)" \<subseteq> "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\
         \<Longrightarrow> H |- (p\<Rightarrow>q\<Rightarrow>r) \<Rightarrow> (p\<Rightarrow>q) \<Rightarrow> p\<Rightarrow>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 \<open>The semantics\<close>

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

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"
  \<comment> \<open>this definition is required since predicates can't be recursive\<close>

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 \<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
  logcon :: "[i,i] \ o" (infixl \|=\ 50) where
  "H |= p \ \t. (\q \ H. is_true(q,t)) \ is_true(p,t)"

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

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 \<open>Proof theory of propositional logic\<close>

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"
  \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close>
  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"
  \<comment> \<open>Rule is called \<open>I\<close> for Identity Combinator, not for Introduction.\<close>
  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 \<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 (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 \<open>The deduction theorem\<close>

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

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

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

subsection \<open>Completeness\<close>

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

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)"
  \<comment> \<open>Typical example of strengthening the induction statement.\<close>
  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"
  \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close>
  apply (drule hyps_thms_if)
  apply (simp add: logcon_def)
  done

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

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

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

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"
  \<comment> \<open>Hard to prove directly because it requires cuts\<close>
  apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
     apply (blast intro!: propn_SIs intro: propn_Is)+
  done

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

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

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

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

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

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

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 \<open>
  The set \<^term>\<open>hyps(p,t)\<close> is finite, and elements have the form
  \<^term>\<open>#v\<close> or \<^term>\<open>#v\<Rightarrow>Fls\<close>; could probably prove the stronger
  \<^prop>\<open>hyps(p,t) \<in> Fin(hyps(p,0) \<union> hyps(p,nat))\<close>.
\<close>

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 \<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_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 \<open>inductive step\<close>
  apply safe
   txt \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v,Y) |- p\<close>\<close>
   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 \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v \<Rightarrow> Fls,Y) |- p\<close>\<close>
  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 \<open>Completeness theorem\<close>

lemma completeness_0: "\p \ propn; 0 |= p\ \ 0 |- p"
  \<comment> \<open>The base case for completeness\<close>
  apply (rule Diff_cancel [THEN subst])
  apply (blast intro: completeness_0_lemma)
  done

lemma logcon_Imp: "\cons(p,H) |= q\ \ H |= p\q"
  \<comment> \<open>A semantic analogue of the Deduction Theorem\<close>
  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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

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.