src/HOL/Induct/PropLog.ML
author paulson
Wed May 07 12:50:26 1997 +0200 (1997-05-07)
changeset 3120 c58423c20740
child 3414 804c8a178a7f
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
paulson@3120
     1
(*  Title:      HOL/ex/pl.ML
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Tobias Nipkow & Lawrence C Paulson
paulson@3120
     4
    Copyright   1994  TU Muenchen & University of Cambridge
paulson@3120
     5
paulson@3120
     6
Soundness and completeness of propositional logic w.r.t. truth-tables.
paulson@3120
     7
paulson@3120
     8
Prove: If H|=p then G|=p where G:Fin(H)
paulson@3120
     9
*)
paulson@3120
    10
paulson@3120
    11
open PropLog;
paulson@3120
    12
paulson@3120
    13
(** Monotonicity **)
paulson@3120
    14
goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
paulson@3120
    15
by (rtac lfp_mono 1);
paulson@3120
    16
by (REPEAT (ares_tac basic_monos 1));
paulson@3120
    17
qed "thms_mono";
paulson@3120
    18
paulson@3120
    19
(*Rule is called I for Identity Combinator, not for Introduction*)
paulson@3120
    20
goal PropLog.thy "H |- p->p";
paulson@3120
    21
by (best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
paulson@3120
    22
qed "thms_I";
paulson@3120
    23
paulson@3120
    24
(** Weakening, left and right **)
paulson@3120
    25
paulson@3120
    26
(* "[| G<=H;  G |- p |] ==> H |- p"
paulson@3120
    27
   This order of premises is convenient with RS
paulson@3120
    28
*)
paulson@3120
    29
bind_thm ("weaken_left", (thms_mono RS subsetD));
paulson@3120
    30
paulson@3120
    31
(* H |- p ==> insert(a,H) |- p *)
paulson@3120
    32
val weaken_left_insert = subset_insertI RS weaken_left;
paulson@3120
    33
paulson@3120
    34
val weaken_left_Un1  =    Un_upper1 RS weaken_left;
paulson@3120
    35
val weaken_left_Un2  =    Un_upper2 RS weaken_left;
paulson@3120
    36
paulson@3120
    37
goal PropLog.thy "!!H. H |- q ==> H |- p->q";
paulson@3120
    38
by (fast_tac (!claset addIs [thms.K,thms.MP]) 1);
paulson@3120
    39
qed "weaken_right";
paulson@3120
    40
paulson@3120
    41
(*The deduction theorem*)
paulson@3120
    42
goal PropLog.thy "!!H. insert p H |- q  ==>  H |- p->q";
paulson@3120
    43
by (etac thms.induct 1);
paulson@3120
    44
by (ALLGOALS 
paulson@3120
    45
    (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
paulson@3120
    46
                             thms.S RS thms.MP RS thms.MP, weaken_right])));
paulson@3120
    47
qed "deduction";
paulson@3120
    48
paulson@3120
    49
paulson@3120
    50
(* "[| insert p H |- q; H |- p |] ==> H |- q"
paulson@3120
    51
    The cut rule - not used
paulson@3120
    52
*)
paulson@3120
    53
val cut = deduction RS thms.MP;
paulson@3120
    54
paulson@3120
    55
(* H |- false ==> H |- p *)
paulson@3120
    56
val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
paulson@3120
    57
paulson@3120
    58
(* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
paulson@3120
    59
bind_thm ("thms_notE", (thms.MP RS thms_falseE));
paulson@3120
    60
paulson@3120
    61
(** The function eval **)
paulson@3120
    62
paulson@3120
    63
goalw PropLog.thy [eval_def] "tt[false] = False";
paulson@3120
    64
by (Simp_tac 1);
paulson@3120
    65
qed "eval_false";
paulson@3120
    66
paulson@3120
    67
goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)";
paulson@3120
    68
by (Simp_tac 1);
paulson@3120
    69
qed "eval_var";
paulson@3120
    70
paulson@3120
    71
goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
paulson@3120
    72
by (Simp_tac 1);
paulson@3120
    73
qed "eval_imp";
paulson@3120
    74
paulson@3120
    75
Addsimps [eval_false, eval_var, eval_imp];
paulson@3120
    76
paulson@3120
    77
(*Soundness of the rules wrt truth-table semantics*)
paulson@3120
    78
goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p";
paulson@3120
    79
by (etac thms.induct 1);
paulson@3120
    80
by (fast_tac (!claset addSDs [eval_imp RS iffD1 RS mp]) 5);
paulson@3120
    81
by (ALLGOALS Asm_simp_tac);
paulson@3120
    82
qed "soundness";
paulson@3120
    83
paulson@3120
    84
(*** Towards the completeness proof ***)
paulson@3120
    85
paulson@3120
    86
goal PropLog.thy "!!H. H |- p->false ==> H |- p->q";
paulson@3120
    87
by (rtac deduction 1);
paulson@3120
    88
by (etac (weaken_left_insert RS thms_notE) 1);
paulson@3120
    89
by (rtac thms.H 1);
paulson@3120
    90
by (rtac insertI1 1);
paulson@3120
    91
qed "false_imp";
paulson@3120
    92
paulson@3120
    93
val [premp,premq] = goal PropLog.thy
paulson@3120
    94
    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false";
paulson@3120
    95
by (rtac deduction 1);
paulson@3120
    96
by (rtac (premq RS weaken_left_insert RS thms.MP) 1);
paulson@3120
    97
by (rtac (thms.H RS thms.MP) 1);
paulson@3120
    98
by (rtac insertI1 1);
paulson@3120
    99
by (rtac (premp RS weaken_left_insert) 1);
paulson@3120
   100
qed "imp_false";
paulson@3120
   101
paulson@3120
   102
(*This formulation is required for strong induction hypotheses*)
paulson@3120
   103
goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)";
paulson@3120
   104
by (rtac (expand_if RS iffD2) 1);
paulson@3120
   105
by (PropLog.pl.induct_tac "p" 1);
paulson@3120
   106
by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H])));
paulson@3120
   107
by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2, 
paulson@3120
   108
                           weaken_right, imp_false]
paulson@3120
   109
                    addSEs [false_imp]) 1);
paulson@3120
   110
qed "hyps_thms_if";
paulson@3120
   111
paulson@3120
   112
(*Key lemma for completeness; yields a set of assumptions satisfying p*)
paulson@3120
   113
val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
paulson@3120
   114
by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
paulson@3120
   115
    rtac hyps_thms_if 2);
paulson@3120
   116
by (Fast_tac 1);
paulson@3120
   117
qed "sat_thms_p";
paulson@3120
   118
paulson@3120
   119
(*For proving certain theorems in our new propositional logic*)
paulson@3120
   120
paulson@3120
   121
AddSIs [deduction];
paulson@3120
   122
AddIs [thms.H, thms.H RS thms.MP];
paulson@3120
   123
paulson@3120
   124
(*The excluded middle in the form of an elimination rule*)
paulson@3120
   125
goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q";
paulson@3120
   126
by (rtac (deduction RS deduction) 1);
paulson@3120
   127
by (rtac (thms.DN RS thms.MP) 1);
paulson@3120
   128
by (ALLGOALS (best_tac (!claset addSIs prems)));
paulson@3120
   129
qed "thms_excluded_middle";
paulson@3120
   130
paulson@3120
   131
(*Hard to prove directly because it requires cuts*)
paulson@3120
   132
val prems = goal PropLog.thy
paulson@3120
   133
    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q";
paulson@3120
   134
by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1);
paulson@3120
   135
by (REPEAT (resolve_tac (prems@[deduction]) 1));
paulson@3120
   136
qed "thms_excluded_middle_rule";
paulson@3120
   137
paulson@3120
   138
(*** Completeness -- lemmas for reducing the set of assumptions ***)
paulson@3120
   139
paulson@3120
   140
(*For the case hyps(p,t)-insert(#v,Y) |- p;
paulson@3120
   141
  we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
paulson@3120
   142
goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
paulson@3120
   143
by (PropLog.pl.induct_tac "p" 1);
paulson@3120
   144
by (Simp_tac 1);
paulson@3120
   145
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
paulson@3120
   146
by (Simp_tac 1);
paulson@3120
   147
by (Fast_tac 1);
paulson@3120
   148
qed "hyps_Diff";
paulson@3120
   149
paulson@3120
   150
(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
paulson@3120
   151
  we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
paulson@3120
   152
goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
paulson@3120
   153
by (PropLog.pl.induct_tac "p" 1);
paulson@3120
   154
by (Simp_tac 1);
paulson@3120
   155
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
paulson@3120
   156
by (Simp_tac 1);
paulson@3120
   157
by (Fast_tac 1);
paulson@3120
   158
qed "hyps_insert";
paulson@3120
   159
paulson@3120
   160
(** Two lemmas for use with weaken_left **)
paulson@3120
   161
paulson@3120
   162
goal Set.thy "B-C <= insert a (B-insert a C)";
paulson@3120
   163
by (Fast_tac 1);
paulson@3120
   164
qed "insert_Diff_same";
paulson@3120
   165
paulson@3120
   166
goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
paulson@3120
   167
by (Fast_tac 1);
paulson@3120
   168
qed "insert_Diff_subset2";
paulson@3120
   169
paulson@3120
   170
(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
paulson@3120
   171
 could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
paulson@3120
   172
goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
paulson@3120
   173
by (PropLog.pl.induct_tac "p" 1);
paulson@3120
   174
by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
paulson@3120
   175
by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
paulson@3120
   176
qed "hyps_finite";
paulson@3120
   177
paulson@3120
   178
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
paulson@3120
   179
paulson@3120
   180
(*Induction on the finite set of assumptions hyps(p,t0).
paulson@3120
   181
  We may repeatedly subtract assumptions until none are left!*)
paulson@3120
   182
val [sat] = goal PropLog.thy
paulson@3120
   183
    "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
paulson@3120
   184
by (rtac (hyps_finite RS Fin_induct) 1);
paulson@3120
   185
by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
paulson@3120
   186
by (safe_tac (!claset));
paulson@3120
   187
(*Case hyps(p,t)-insert(#v,Y) |- p *)
paulson@3120
   188
by (rtac thms_excluded_middle_rule 1);
paulson@3120
   189
by (rtac (insert_Diff_same RS weaken_left) 1);
paulson@3120
   190
by (etac spec 1);
paulson@3120
   191
by (rtac (insert_Diff_subset2 RS weaken_left) 1);
paulson@3120
   192
by (rtac (hyps_Diff RS Diff_weaken_left) 1);
paulson@3120
   193
by (etac spec 1);
paulson@3120
   194
(*Case hyps(p,t)-insert(#v -> false,Y) |- p *)
paulson@3120
   195
by (rtac thms_excluded_middle_rule 1);
paulson@3120
   196
by (rtac (insert_Diff_same RS weaken_left) 2);
paulson@3120
   197
by (etac spec 2);
paulson@3120
   198
by (rtac (insert_Diff_subset2 RS weaken_left) 1);
paulson@3120
   199
by (rtac (hyps_insert RS Diff_weaken_left) 1);
paulson@3120
   200
by (etac spec 1);
paulson@3120
   201
qed "completeness_0_lemma";
paulson@3120
   202
paulson@3120
   203
(*The base case for completeness*)
paulson@3120
   204
val [sat] = goal PropLog.thy "{} |= p ==> {} |- p";
paulson@3120
   205
by (rtac (Diff_cancel RS subst) 1);
paulson@3120
   206
by (rtac (sat RS (completeness_0_lemma RS spec)) 1);
paulson@3120
   207
qed "completeness_0";
paulson@3120
   208
paulson@3120
   209
(*A semantic analogue of the Deduction Theorem*)
paulson@3120
   210
goalw PropLog.thy [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
paulson@3120
   211
by (Simp_tac 1);
paulson@3120
   212
by (Fast_tac 1);
paulson@3120
   213
qed "sat_imp";
paulson@3120
   214
paulson@3120
   215
val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
paulson@3120
   216
by (rtac (finite RS Fin_induct) 1);
paulson@3120
   217
by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
paulson@3120
   218
by (rtac (weaken_left_insert RS thms.MP) 1);
paulson@3120
   219
by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
paulson@3120
   220
by (Fast_tac 1);
paulson@3120
   221
qed "completeness_lemma";
paulson@3120
   222
paulson@3120
   223
val completeness = completeness_lemma RS spec RS mp;
paulson@3120
   224
paulson@3120
   225
val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
paulson@3120
   226
by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
paulson@3120
   227
qed "thms_iff";
paulson@3120
   228
paulson@3120
   229
writeln"Reached end of file.";