src/HOL/Induct/PropLog.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58310 91ea607a34d8 child 60530 44f9873d6f6f permissions -rw-r--r--
```     1 (*  Title:      HOL/Induct/PropLog.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   1994  TU Muenchen & University of Cambridge
```
```     4 *)
```
```     5
```
```     6 section {* Meta-theory of propositional logic *}
```
```     7
```
```     8 theory PropLog imports Main begin
```
```     9
```
```    10 text {*
```
```    11   Datatype definition of propositional logic formulae and inductive
```
```    12   definition of the propositional tautologies.
```
```    13
```
```    14   Inductive definition of propositional logic.  Soundness and
```
```    15   completeness w.r.t.\ truth-tables.
```
```    16
```
```    17   Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
```
```    18   Fin(H)"}
```
```    19 *}
```
```    20
```
```    21 subsection {* The datatype of propositions *}
```
```    22
```
```    23 datatype 'a pl =
```
```    24   false |
```
```    25   var 'a ("#_" [1000]) |
```
```    26   imp "'a pl" "'a pl" (infixr "->" 90)
```
```    27
```
```    28
```
```    29 subsection {* The proof system *}
```
```    30
```
```    31 inductive thms :: "['a pl set, 'a pl] => bool"  (infixl "|-" 50)
```
```    32   for H :: "'a pl set"
```
```    33 where
```
```    34   H: "p\<in>H ==> H |- p"
```
```    35 | K: "H |- p->q->p"
```
```    36 | S: "H |- (p->q->r) -> (p->q) -> p->r"
```
```    37 | DN: "H |- ((p->false) -> false) -> p"
```
```    38 | MP: "[| H |- p->q; H |- p |] ==> H |- q"
```
```    39
```
```    40
```
```    41 subsection {* The semantics *}
```
```    42
```
```    43 subsubsection {* Semantics of propositional logic. *}
```
```    44
```
```    45 primrec eval :: "['a set, 'a pl] => bool"  ("_[[_]]" [100,0] 100)
```
```    46 where
```
```    47   "tt[[false]] = False"
```
```    48 | "tt[[#v]] = (v \<in> tt)"
```
```    49 | eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
```
```    50
```
```    51 text {*
```
```    52   A finite set of hypotheses from @{text t} and the @{text Var}s in
```
```    53   @{text p}.
```
```    54 *}
```
```    55
```
```    56 primrec hyps :: "['a pl, 'a set] => 'a pl set"
```
```    57 where
```
```    58   "hyps false  tt = {}"
```
```    59 | "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
```
```    60 | "hyps (p->q) tt = hyps p tt Un hyps q tt"
```
```    61
```
```    62
```
```    63 subsubsection {* Logical consequence *}
```
```    64
```
```    65 text {*
```
```    66   For every valuation, if all elements of @{text H} are true then so
```
```    67   is @{text p}.
```
```    68 *}
```
```    69
```
```    70 definition sat :: "['a pl set, 'a pl] => bool"  (infixl "|=" 50)
```
```    71   where "H |= p = (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
```
```    72
```
```    73
```
```    74 subsection {* Proof theory of propositional logic *}
```
```    75
```
```    76 lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
```
```    77 apply (rule predicate1I)
```
```    78 apply (erule thms.induct)
```
```    79 apply (auto intro: thms.intros)
```
```    80 done
```
```    81
```
```    82 lemma thms_I: "H |- p->p"
```
```    83   -- {*Called @{text I} for Identity Combinator, not for Introduction. *}
```
```    84 by (best intro: thms.K thms.S thms.MP)
```
```    85
```
```    86
```
```    87 subsubsection {* Weakening, left and right *}
```
```    88
```
```    89 lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
```
```    90   -- {* Order of premises is convenient with @{text THEN} *}
```
```    91   by (erule thms_mono [THEN predicate1D])
```
```    92
```
```    93 lemma weaken_left_insert: "G |- p \<Longrightarrow> insert a G |- p"
```
```    94 by (rule weaken_left) (rule subset_insertI)
```
```    95
```
```    96 lemma weaken_left_Un1: "G |- p \<Longrightarrow> G \<union> B |- p"
```
```    97 by (rule weaken_left) (rule Un_upper1)
```
```    98
```
```    99 lemma weaken_left_Un2: "G |- p \<Longrightarrow> A \<union> G |- p"
```
```   100 by (rule weaken_left) (rule Un_upper2)
```
```   101
```
```   102 lemma weaken_right: "H |- q ==> H |- p->q"
```
```   103 by (fast intro: thms.K thms.MP)
```
```   104
```
```   105
```
```   106 subsubsection {* The deduction theorem *}
```
```   107
```
```   108 theorem deduction: "insert p H |- q  ==>  H |- p->q"
```
```   109 apply (induct set: thms)
```
```   110 apply (fast intro: thms_I thms.H thms.K thms.S thms.DN
```
```   111                    thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+
```
```   112 done
```
```   113
```
```   114
```
```   115 subsubsection {* The cut rule *}
```
```   116
```
```   117 lemma cut: "insert p H |- q \<Longrightarrow> H |- p \<Longrightarrow> H |- q"
```
```   118 by (rule thms.MP) (rule deduction)
```
```   119
```
```   120 lemma thms_falseE: "H |- false \<Longrightarrow> H |- q"
```
```   121 by (rule thms.MP, rule thms.DN) (rule weaken_right)
```
```   122
```
```   123 lemma thms_notE: "H |- p -> false \<Longrightarrow> H |- p \<Longrightarrow> H |- q"
```
```   124 by (rule thms_falseE) (rule thms.MP)
```
```   125
```
```   126
```
```   127 subsubsection {* Soundness of the rules wrt truth-table semantics *}
```
```   128
```
```   129 theorem soundness: "H |- p ==> H |= p"
```
```   130 by (induct set: thms) (auto simp: sat_def)
```
```   131
```
```   132
```
```   133 subsection {* Completeness *}
```
```   134
```
```   135 subsubsection {* Towards the completeness proof *}
```
```   136
```
```   137 lemma false_imp: "H |- p->false ==> H |- p->q"
```
```   138 apply (rule deduction)
```
```   139 apply (metis H insert_iff weaken_left_insert thms_notE)
```
```   140 done
```
```   141
```
```   142 lemma imp_false:
```
```   143     "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
```
```   144 apply (rule deduction)
```
```   145 apply (metis H MP insert_iff weaken_left_insert)
```
```   146 done
```
```   147
```
```   148 lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
```
```   149   -- {* Typical example of strengthening the induction statement. *}
```
```   150 apply simp
```
```   151 apply (induct p)
```
```   152 apply (simp_all add: thms_I thms.H)
```
```   153 apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right
```
```   154                     imp_false false_imp)
```
```   155 done
```
```   156
```
```   157 lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
```
```   158   -- {* Key lemma for completeness; yields a set of assumptions
```
```   159         satisfying @{text p} *}
```
```   160 unfolding sat_def
```
```   161 by (metis (full_types) empty_iff hyps_thms_if)
```
```   162
```
```   163 text {*
```
```   164   For proving certain theorems in our new propositional logic.
```
```   165 *}
```
```   166
```
```   167 declare deduction [intro!]
```
```   168 declare thms.H [THEN thms.MP, intro]
```
```   169
```
```   170 text {*
```
```   171   The excluded middle in the form of an elimination rule.
```
```   172 *}
```
```   173
```
```   174 lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
```
```   175 apply (rule deduction [THEN deduction])
```
```   176 apply (rule thms.DN [THEN thms.MP], best intro: H)
```
```   177 done
```
```   178
```
```   179 lemma thms_excluded_middle_rule:
```
```   180     "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q"
```
```   181   -- {* Hard to prove directly because it requires cuts *}
```
```   182 by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto)
```
```   183
```
```   184
```
```   185 subsection{* Completeness -- lemmas for reducing the set of assumptions*}
```
```   186
```
```   187 text {*
```
```   188   For the case @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
```
```   189   "hyps p t - {#v} \<subseteq> hyps p (t-{v})"}.
```
```   190 *}
```
```   191
```
```   192 lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
```
```   193 by (induct p) auto
```
```   194
```
```   195 text {*
```
```   196   For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
```
```   197   @{prop "hyps p t-{#v->Fls} \<subseteq> hyps p (insert v t)"}.
```
```   198 *}
```
```   199
```
```   200 lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"
```
```   201 by (induct p) auto
```
```   202
```
```   203 text {* Two lemmas for use with @{text weaken_left} *}
```
```   204
```
```   205 lemma insert_Diff_same: "B-C <= insert a (B-insert a C)"
```
```   206 by fast
```
```   207
```
```   208 lemma insert_Diff_subset2: "insert a (B-{c}) - D <= insert a (B-insert c D)"
```
```   209 by fast
```
```   210
```
```   211 text {*
```
```   212   The set @{term "hyps p t"} is finite, and elements have the form
```
```   213   @{term "#v"} or @{term "#v->Fls"}.
```
```   214 *}
```
```   215
```
```   216 lemma hyps_finite: "finite(hyps p t)"
```
```   217 by (induct p) auto
```
```   218
```
```   219 lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
```
```   220 by (induct p) auto
```
```   221
```
```   222 lemma Diff_weaken_left: "A \<subseteq> C \<Longrightarrow> A - B |- p \<Longrightarrow> C - B |- p"
```
```   223   by (rule Diff_mono [OF _ subset_refl, THEN weaken_left])
```
```   224
```
```   225
```
```   226 subsubsection {* Completeness theorem *}
```
```   227
```
```   228 text {*
```
```   229   Induction on the finite set of assumptions @{term "hyps p t0"}.  We
```
```   230   may repeatedly subtract assumptions until none are left!
```
```   231 *}
```
```   232
```
```   233 lemma completeness_0_lemma:
```
```   234     "{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p"
```
```   235 apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
```
```   236  apply (simp add: sat_thms_p, safe)
```
```   237  txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
```
```   238  apply (iprover intro: thms_excluded_middle_rule
```
```   239                      insert_Diff_same [THEN weaken_left]
```
```   240                      insert_Diff_subset2 [THEN weaken_left]
```
```   241                      hyps_Diff [THEN Diff_weaken_left])
```
```   242 txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
```
```   243  apply (iprover intro: thms_excluded_middle_rule
```
```   244                      insert_Diff_same [THEN weaken_left]
```
```   245                      insert_Diff_subset2 [THEN weaken_left]
```
```   246                      hyps_insert [THEN Diff_weaken_left])
```
```   247 done
```
```   248
```
```   249 text{*The base case for completeness*}
```
```   250 lemma completeness_0:  "{} |= p ==> {} |- p"
```
```   251   by (metis Diff_cancel completeness_0_lemma)
```
```   252
```
```   253 text{*A semantic analogue of the Deduction Theorem*}
```
```   254 lemma sat_imp: "insert p H |= q ==> H |= p->q"
```
```   255 by (auto simp: sat_def)
```
```   256
```
```   257 theorem completeness: "finite H ==> H |= p ==> H |- p"
```
```   258 apply (induct arbitrary: p rule: finite_induct)
```
```   259  apply (blast intro: completeness_0)
```
```   260 apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
```
```   261 done
```
```   262
```
```   263 theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
```
```   264 by (blast intro: soundness completeness)
```
```   265
```
```   266 end
```