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