# Theory PropLog

Up to index of Isabelle/HOL/Induct

theory PropLog
imports Main
begin

    (*  Title:      HOL/Induct/PropLog.thy
        ID:         $Id: PropLog.thy,v 1.9 2005/09/22 21:56:28 nipkow Exp $
        Author:     Tobias Nipkow
        Copyright   1994  TU Muenchen & University of Cambridge
    *)

    header {* 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 @{text "H |= p"} then @{text "G |= p"} where @{text "G ∈
      Fin(H)"}
    *}

    subsection {* The datatype of propositions *}

    datatype
        'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90)

    subsection {* The proof system *}

    consts
      thms  :: "'a pl set => 'a pl set"
      "|-"  :: "['a pl set, 'a pl] => bool"   (infixl 50)

    translations
      "H |- p" == "p ∈ thms(H)"

    inductive "thms(H)"
      intros
      H [intro]:  "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. *}

    consts
      eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100)

    primrec     "tt[[false]] = False"
                "tt[[#v]]    = (v ∈ tt)"
      eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"

    text {*
      A finite set of hypotheses from @{text t} and the @{text Var}s in
      @{text p}.
    *}

    consts
      hyps  :: "['a pl, 'a set] => 'a pl set"

    primrec
      "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 @{text H} are true then so
      is @{text p}.
    *}

    constdefs
      sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50)
        "H |= p  ==  (∀tt. (∀q∈H. tt[[q]]) --> tt[[p]])"

    subsection {* Proof theory of propositional logic *}

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

    lemma thms_I: "H |- p->p"
      -- {*Called @{text 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 @{text THEN} *}
      by (erule thms_mono [THEN subsetD])

    lemmas weaken_left_insert = subset_insertI [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 ==> H |- p->q"
    by (fast intro: thms.K thms.MP)

    subsubsection {* The deduction theorem *}

    theorem deduction: "insert p H |- q  ==>  H |- p->q"
    apply (erule thms.induct)
    apply (fast intro: thms_I thms.H thms.K thms.S thms.DN
                       thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+
    done

    subsubsection {* The cut rule *}

    lemmas cut = deduction [THEN thms.MP]

    lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]

    lemmas thms_notE = thms.MP [THEN thms_falseE, standard]

    subsubsection {* Soundness of the rules wrt truth-table semantics *}

    theorem soundness: "H |- p ==> H |= p"
    apply (unfold sat_def)
    apply (erule thms.induct, auto)
    done

    subsection {* Completeness *}

    subsubsection {* Towards the completeness proof *}

    lemma false_imp: "H |- p->false ==> H |- p->q"
    apply (rule deduction)
    apply (erule weaken_left_insert [THEN thms_notE])
    apply blast
    done

    lemma imp_false:
        "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
    apply (rule deduction)
    apply (blast intro: weaken_left_insert thms.MP thms.H)
    done

    lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
      -- {* Typical example of strengthening the induction statement. *}
    apply simp
    apply (induct_tac "p")
    apply (simp_all add: thms_I thms.H)
    apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right
                        imp_false false_imp)
    done

    lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
      -- {* Key lemma for completeness; yields a set of assumptions
            satisfying @{text p} *}
    apply (unfold sat_def)
    apply (drule spec, erule mp [THEN if_P, THEN subst],
           rule_tac [2] hyps_thms_if, simp)
    done

    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"
    apply (rule deduction [THEN deduction])
    apply (rule thms.DN [THEN thms.MP], best)
    done

    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 @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
      "hyps p t - {#v} ⊆ hyps p (t-{v})"}.
    *}

    lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
    by (induct_tac "p", auto)

    text {*
      For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
      @{prop "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_tac "p", auto)

    text {* Two lemmas for use with @{text 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 @{term "hyps p t"} is finite, and elements have the form
      @{term "#v"} or @{term "#v->Fls"}.
    *}

    lemma hyps_finite: "finite(hyps p t)"
    by (induct_tac "p", auto)

    lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
    by (induct_tac "p", auto)

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

    subsubsection {* Completeness theorem *}

    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:
        "{} |= p ==> ∀t. hyps p t - hyps p t0 |- p"
    apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
     apply (simp add: sat_thms_p, safe)
     txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
     apply (iprover intro: thms_excluded_middle_rule
                         insert_Diff_same [THEN weaken_left]
                         insert_Diff_subset2 [THEN weaken_left]
                         hyps_Diff [THEN Diff_weaken_left])
    txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
     apply (iprover intro: thms_excluded_middle_rule
                         insert_Diff_same [THEN weaken_left]
                         insert_Diff_subset2 [THEN weaken_left]
                         hyps_insert [THEN Diff_weaken_left])
    done

    text{*The base case for completeness*}
    lemma completeness_0:  "{} |= p ==> {} |- p"
    apply (rule Diff_cancel [THEN subst])
    apply (erule completeness_0_lemma [THEN spec])
    done

    text{*A semantic analogue of the Deduction Theorem*}
    lemma sat_imp: "insert p H |= q ==> H |= p->q"
    by (unfold sat_def, auto)

    theorem completeness [rule_format]: "finite H ==> ∀p. H |= p --> H |- p"
    apply (erule finite_induct)
     apply (blast intro: completeness_0)
    apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
    done

    theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
    by (blast intro: soundness completeness)

    end

### The datatype of propositions

### The proof system

### The semantics

#### Semantics of propositional logic.

#### Logical consequence

### Proof theory of propositional logic

lemma thms_mono:

      G ⊆ H ==> thms G ⊆ thms H

lemma thms_I:

      H |- p -> p

#### Weakening, left and right

lemma weaken_left:

      [| G ⊆ H; G |- p |] ==> H |- p

lemmas weaken_left_insert:

      G |- p ==> insert a1 G |- p

lemmas weaken_left_insert:

      G |- p ==> insert a1 G |- p

lemmas weaken_left_Un1:

      G |- p ==> G ∪ B1 |- p

lemmas weaken_left_Un1:

      G |- p ==> G ∪ B1 |- p

lemmas weaken_left_Un2:

      G |- p ==> A1 ∪ G |- p

lemmas weaken_left_Un2:

      G |- p ==> A1 ∪ G |- p

lemma weaken_right:

      H |- q ==> H |- p -> q

#### The deduction theorem

theorem deduction:

      insert p H |- q ==> H |- p -> q

#### The cut rule

lemmas cut:

      [| insert p H |- q; H |- p |] ==> H |- q

lemmas cut:

      [| insert p H |- q; H |- p |] ==> H |- q

lemmas thms_falseE:

      H |- false ==> H |- q

lemmas thms_falseE:

      H |- false ==> H |- q

lemmas thms_notE:

      [| H |- p -> false; H |- p |] ==> H |- q

lemmas thms_notE:

      [| H |- p -> false; H |- p |] ==> H |- q

#### Soundness of the rules wrt truth-table semantics

theorem soundness:

      H |- p ==> H |= p

### Completeness

#### Towards the completeness proof

lemma false_imp:

      H |- p -> false ==> H |- p -> q

lemma imp_false:

      [| H |- p; H |- q -> false |] ==> H |- (p -> q) -> false

lemma hyps_thms_if:

      hyps p tt |- (if tt[[p]] then p else p -> false)

lemma sat_thms_p:

      {} |= p ==> hyps p tt |- p

lemma thms_excluded_middle:

      H |- (p -> q) -> ((p -> false) -> q) -> q

lemma thms_excluded_middle_rule:

      [| insert p H |- q; insert (p -> false) H |- q |] ==> H |- q

### Completeness -- lemmas for reducing the set of assumptions

lemma hyps_Diff:

      hyps p (t - {v}) ⊆ insert (#v -> false) (hyps p t - {#v})

lemma hyps_insert:

      hyps p (insert v t) ⊆ insert #v (hyps p t - {#v -> false})

lemma insert_Diff_same:

      B - C ⊆ insert a (B - insert a C)

lemma insert_Diff_subset2:

      insert a (B - {c}) - D ⊆ insert a (B - insert c D)

lemma hyps_finite:

      finite (hyps p t)

lemma hyps_subset:

      hyps p t ⊆ (UN v. {#v, #v -> false})

lemmas Diff_weaken_left:

      [| A1 ⊆ C1; A1 - B1 |- p |] ==> C1 - B1 |- p

lemmas Diff_weaken_left:

      [| A1 ⊆ C1; A1 - B1 |- p |] ==> C1 - B1 |- p

#### Completeness theorem

lemma completeness_0_lemma:

      {} |= p ==> ∀t. hyps p t - hyps p t0.0 |- p

lemma completeness_0:

      {} |= p ==> {} |- p

lemma sat_imp:

      insert p H |= q ==> H |= p -> q

theorem completeness:

      [| finite H; H |= p |] ==> H |- p

theorem syntax_iff_semantics:

      finite H ==> (H |- p) = (H |= p)