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