1 (* Title: ZF/ex/prop-log.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Lawrence C Paulson |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Inductive definition of propositional logic. |
|
7 Soundness and completeness w.r.t. truth-tables. |
|
8 |
|
9 Prove: If H|=p then G|=p where G \\<in> Fin(H) |
|
10 *) |
|
11 |
|
12 Addsimps prop.intrs; |
|
13 |
|
14 (*** Semantics of propositional logic ***) |
|
15 |
|
16 (** The function is_true **) |
|
17 |
|
18 Goalw [is_true_def] "is_true(Fls,t) <-> False"; |
|
19 by (Simp_tac 1); |
|
20 qed "is_true_Fls"; |
|
21 |
|
22 Goalw [is_true_def] "is_true(#v,t) <-> v \\<in> t"; |
|
23 by (Simp_tac 1); |
|
24 qed "is_true_Var"; |
|
25 |
|
26 Goalw [is_true_def] "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"; |
|
27 by (Simp_tac 1); |
|
28 qed "is_true_Imp"; |
|
29 |
|
30 Addsimps [is_true_Fls, is_true_Var, is_true_Imp]; |
|
31 |
|
32 |
|
33 (*** Proof theory of propositional logic ***) |
|
34 |
|
35 Goalw thms.defs "G \\<subseteq> H ==> thms(G) \\<subseteq> thms(H)"; |
|
36 by (rtac lfp_mono 1); |
|
37 by (REPEAT (rtac thms.bnd_mono 1)); |
|
38 by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
|
39 qed "thms_mono"; |
|
40 |
|
41 val thms_in_pl = thms.dom_subset RS subsetD; |
|
42 |
|
43 val ImpE = prop.mk_cases "p=>q \\<in> prop"; |
|
44 |
|
45 (*Stronger Modus Ponens rule: no typechecking!*) |
|
46 Goal "[| H |- p=>q; H |- p |] ==> H |- q"; |
|
47 by (rtac thms.MP 1); |
|
48 by (REPEAT (eresolve_tac [asm_rl, thms_in_pl, thms_in_pl RS ImpE] 1)); |
|
49 qed "thms_MP"; |
|
50 |
|
51 (*Rule is called I for Identity Combinator, not for Introduction*) |
|
52 Goal "p \\<in> prop ==> H |- p=>p"; |
|
53 by (rtac (thms.S RS thms_MP RS thms_MP) 1); |
|
54 by (rtac thms.K 5); |
|
55 by (rtac thms.K 4); |
|
56 by (REPEAT (ares_tac prop.intrs 1)); |
|
57 qed "thms_I"; |
|
58 |
|
59 (** Weakening, left and right **) |
|
60 |
|
61 (* [| G \\<subseteq> H; G|-p |] ==> H|-p Order of premises is convenient with RS*) |
|
62 bind_thm ("weaken_left", (thms_mono RS subsetD)); |
|
63 |
|
64 (* H |- p ==> cons(a,H) |- p *) |
|
65 val weaken_left_cons = subset_consI RS weaken_left; |
|
66 |
|
67 val weaken_left_Un1 = Un_upper1 RS weaken_left; |
|
68 val weaken_left_Un2 = Un_upper2 RS weaken_left; |
|
69 |
|
70 Goal "[| H |- q; p \\<in> prop |] ==> H |- p=>q"; |
|
71 by (rtac (thms.K RS thms_MP) 1); |
|
72 by (REPEAT (ares_tac [thms_in_pl] 1)); |
|
73 qed "weaken_right"; |
|
74 |
|
75 (*The deduction theorem*) |
|
76 Goal "[| cons(p,H) |- q; p \\<in> prop |] ==> H |- p=>q"; |
|
77 by (etac thms.induct 1); |
|
78 by (blast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1); |
|
79 by (blast_tac (claset() addIs [thms.K RS weaken_right]) 1); |
|
80 by (blast_tac (claset() addIs [thms.S RS weaken_right]) 1); |
|
81 by (blast_tac (claset() addIs [thms.DN RS weaken_right]) 1); |
|
82 by (blast_tac (claset() addIs [thms.S RS thms_MP RS thms_MP]) 1); |
|
83 qed "deduction"; |
|
84 |
|
85 |
|
86 (*The cut rule*) |
|
87 Goal "[| H|-p; cons(p,H) |- q |] ==> H |- q"; |
|
88 by (rtac (deduction RS thms_MP) 1); |
|
89 by (REPEAT (ares_tac [thms_in_pl] 1)); |
|
90 qed "cut"; |
|
91 |
|
92 Goal "[| H |- Fls; p \\<in> prop |] ==> H |- p"; |
|
93 by (rtac (thms.DN RS thms_MP) 1); |
|
94 by (rtac weaken_right 2); |
|
95 by (REPEAT (ares_tac (prop.intrs@[consI1]) 1)); |
|
96 qed "thms_FlsE"; |
|
97 |
|
98 (* [| H |- p=>Fls; H |- p; q \\<in> prop |] ==> H |- q *) |
|
99 bind_thm ("thms_notE", (thms_MP RS thms_FlsE)); |
|
100 |
|
101 (*Soundness of the rules wrt truth-table semantics*) |
|
102 Goalw [logcon_def] "H |- p ==> H |= p"; |
|
103 by (etac thms.induct 1); |
|
104 by Auto_tac; |
|
105 qed "soundness"; |
|
106 |
|
107 (*** Towards the completeness proof ***) |
|
108 |
|
109 val [premf,premq] = goal PropLog.thy |
|
110 "[| H |- p=>Fls; q \\<in> prop |] ==> H |- p=>q"; |
|
111 by (rtac (premf RS thms_in_pl RS ImpE) 1); |
|
112 by (rtac deduction 1); |
|
113 by (rtac (premf RS weaken_left_cons RS thms_notE) 1); |
|
114 by (REPEAT (ares_tac [premq, consI1, thms.H] 1)); |
|
115 qed "Fls_Imp"; |
|
116 |
|
117 val [premp,premq] = goal PropLog.thy |
|
118 "[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls"; |
|
119 by (cut_facts_tac ([premp,premq] RL [thms_in_pl]) 1); |
|
120 by (etac ImpE 1); |
|
121 by (rtac deduction 1); |
|
122 by (rtac (premq RS weaken_left_cons RS thms_MP) 1); |
|
123 by (rtac (consI1 RS thms.H RS thms_MP) 1); |
|
124 by (rtac (premp RS weaken_left_cons) 2); |
|
125 by (REPEAT (ares_tac prop.intrs 1)); |
|
126 qed "Imp_Fls"; |
|
127 |
|
128 (*Typical example of strengthening the induction formula*) |
|
129 Goal "p \\<in> prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"; |
|
130 by (Simp_tac 1); |
|
131 by (induct_tac "p" 1); |
|
132 by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H]))); |
|
133 by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, |
|
134 Fls_Imp RS weaken_left_Un2])); |
|
135 by (ALLGOALS (blast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, |
|
136 weaken_right, Imp_Fls]))); |
|
137 qed "hyps_thms_if"; |
|
138 |
|
139 (*Key lemma for completeness; yields a set of assumptions satisfying p*) |
|
140 Goalw [logcon_def] "[| p \\<in> prop; 0 |= p |] ==> hyps(p,t) |- p"; |
|
141 by (dtac hyps_thms_if 1); |
|
142 by (Asm_full_simp_tac 1); |
|
143 qed "logcon_thms_p"; |
|
144 |
|
145 (*For proving certain theorems in our new propositional logic*) |
|
146 val thms_cs = |
|
147 ZF_cs addSIs (prop.intrs @ [deduction]) |
|
148 addIs [thms_in_pl, thms.H, thms.H RS thms_MP]; |
|
149 |
|
150 (*The excluded middle in the form of an elimination rule*) |
|
151 Goal "[| p \\<in> prop; q \\<in> prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"; |
|
152 by (rtac (deduction RS deduction) 1); |
|
153 by (rtac (thms.DN RS thms_MP) 1); |
|
154 by (ALLGOALS (blast_tac thms_cs)); |
|
155 qed "thms_excluded_middle"; |
|
156 |
|
157 (*Hard to prove directly because it requires cuts*) |
|
158 Goal "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \\<in> prop |] ==> H |- q"; |
|
159 by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1); |
|
160 by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1)); |
|
161 qed "thms_excluded_middle_rule"; |
|
162 |
|
163 (*** Completeness -- lemmas for reducing the set of assumptions ***) |
|
164 |
|
165 (*For the case hyps(p,t)-cons(#v,Y) |- p; |
|
166 we also have hyps(p,t)-{#v} \\<subseteq> hyps(p, t-{v}) *) |
|
167 Goal "p \\<in> prop ==> hyps(p, t-{v}) \\<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"; |
|
168 by (induct_tac "p" 1); |
|
169 by Auto_tac; |
|
170 qed "hyps_Diff"; |
|
171 |
|
172 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p; |
|
173 we also have hyps(p,t)-{#v=>Fls} \\<subseteq> hyps(p, cons(v,t)) *) |
|
174 Goal "p \\<in> prop ==> hyps(p, cons(v,t)) \\<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"; |
|
175 by (induct_tac "p" 1); |
|
176 by Auto_tac; |
|
177 qed "hyps_cons"; |
|
178 |
|
179 (** Two lemmas for use with weaken_left **) |
|
180 |
|
181 Goal "B-C \\<subseteq> cons(a, B-cons(a,C))"; |
|
182 by (Fast_tac 1); |
|
183 qed "cons_Diff_same"; |
|
184 |
|
185 Goal "cons(a, B-{c}) - D \\<subseteq> cons(a, B-cons(c,D))"; |
|
186 by (Fast_tac 1); |
|
187 qed "cons_Diff_subset2"; |
|
188 |
|
189 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls; |
|
190 could probably prove the stronger hyps(p,t) \\<in> Fin(hyps(p,0) Un hyps(p,nat))*) |
|
191 Goal "p \\<in> prop ==> hyps(p,t) \\<in> Fin(\\<Union>v \\<in> nat. {#v, #v=>Fls})"; |
|
192 by (induct_tac "p" 1); |
|
193 by Auto_tac; |
|
194 qed "hyps_finite"; |
|
195 |
|
196 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; |
|
197 |
|
198 (*Induction on the finite set of assumptions hyps(p,t0). |
|
199 We may repeatedly subtract assumptions until none are left!*) |
|
200 val [premp,sat] = goal PropLog.thy |
|
201 "[| p \\<in> prop; 0 |= p |] ==> \\<forall>t. hyps(p,t) - hyps(p,t0) |- p"; |
|
202 by (rtac (premp RS hyps_finite RS Fin_induct) 1); |
|
203 by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1); |
|
204 by Safe_tac; |
|
205 (*Case hyps(p,t)-cons(#v,Y) |- p *) |
|
206 by (rtac thms_excluded_middle_rule 1); |
|
207 by (etac prop.Var_I 3); |
|
208 by (rtac (cons_Diff_same RS weaken_left) 1); |
|
209 by (etac spec 1); |
|
210 by (rtac (cons_Diff_subset2 RS weaken_left) 1); |
|
211 by (rtac (premp RS hyps_Diff RS Diff_weaken_left) 1); |
|
212 by (etac spec 1); |
|
213 (*Case hyps(p,t)-cons(#v => Fls,Y) |- p *) |
|
214 by (rtac thms_excluded_middle_rule 1); |
|
215 by (etac prop.Var_I 3); |
|
216 by (rtac (cons_Diff_same RS weaken_left) 2); |
|
217 by (etac spec 2); |
|
218 by (rtac (cons_Diff_subset2 RS weaken_left) 1); |
|
219 by (rtac (premp RS hyps_cons RS Diff_weaken_left) 1); |
|
220 by (etac spec 1); |
|
221 qed "completeness_0_lemma"; |
|
222 |
|
223 (*The base case for completeness*) |
|
224 val [premp,sat] = goal PropLog.thy "[| p \\<in> prop; 0 |= p |] ==> 0 |- p"; |
|
225 by (rtac (Diff_cancel RS subst) 1); |
|
226 by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1); |
|
227 qed "completeness_0"; |
|
228 |
|
229 (*A semantic analogue of the Deduction Theorem*) |
|
230 Goalw [logcon_def] "[| cons(p,H) |= q |] ==> H |= p=>q"; |
|
231 by Auto_tac; |
|
232 qed "logcon_Imp"; |
|
233 |
|
234 Goal "H \\<in> Fin(prop) ==> \\<forall>p \\<in> prop. H |= p --> H |- p"; |
|
235 by (etac Fin_induct 1); |
|
236 by (safe_tac (claset() addSIs [completeness_0])); |
|
237 by (rtac (weaken_left_cons RS thms_MP) 1); |
|
238 by (blast_tac (claset() addSIs (logcon_Imp::prop.intrs)) 1); |
|
239 by (blast_tac thms_cs 1); |
|
240 qed "completeness_lemma"; |
|
241 |
|
242 val completeness = completeness_lemma RS bspec RS mp; |
|
243 |
|
244 val [finite] = goal PropLog.thy "H \\<in> Fin(prop) ==> H |- p <-> H |= p & p \\<in> prop"; |
|
245 by (fast_tac (claset() addSEs [soundness, finite RS completeness, |
|
246 thms_in_pl]) 1); |
|
247 qed "thms_iff"; |
|
248 |
|
249 writeln"Reached end of file."; |
|