16 (** conversion rules **) |
16 (** conversion rules **) |
17 |
17 |
18 goal PropLog.thy "prop_rec(Fls,b,c,d) = b"; |
18 goal PropLog.thy "prop_rec(Fls,b,c,d) = b"; |
19 by (rtac (prop_rec_def RS def_Vrec RS trans) 1); |
19 by (rtac (prop_rec_def RS def_Vrec RS trans) 1); |
20 by (rewrite_goals_tac prop.con_defs); |
20 by (rewrite_goals_tac prop.con_defs); |
21 by (simp_tac rank_ss 1); |
21 by (Simp_tac 1); |
22 qed "prop_rec_Fls"; |
22 qed "prop_rec_Fls"; |
23 |
23 |
24 goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)"; |
24 goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)"; |
25 by (rtac (prop_rec_def RS def_Vrec RS trans) 1); |
25 by (rtac (prop_rec_def RS def_Vrec RS trans) 1); |
26 by (rewrite_goals_tac prop.con_defs); |
26 by (rewrite_goals_tac prop.con_defs); |
27 by (simp_tac rank_ss 1); |
27 by (Simp_tac 1); |
28 qed "prop_rec_Var"; |
28 qed "prop_rec_Var"; |
29 |
29 |
30 goal PropLog.thy "prop_rec(p=>q,b,c,d) = \ |
30 goal PropLog.thy "prop_rec(p=>q,b,c,d) = \ |
31 \ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))"; |
31 \ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))"; |
32 by (rtac (prop_rec_def RS def_Vrec RS trans) 1); |
32 by (rtac (prop_rec_def RS def_Vrec RS trans) 1); |
33 by (rewrite_goals_tac prop.con_defs); |
33 by (rewrite_goals_tac prop.con_defs); |
34 by (simp_tac rank_ss 1); |
34 by (simp_tac rank_ss 1); |
35 qed "prop_rec_Imp"; |
35 qed "prop_rec_Imp"; |
36 |
36 |
37 val prop_rec_ss = |
37 Addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp]; |
38 arith_ss addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp]; |
|
39 |
38 |
40 (*** Semantics of propositional logic ***) |
39 (*** Semantics of propositional logic ***) |
41 |
40 |
42 (** The function is_true **) |
41 (** The function is_true **) |
43 |
42 |
44 goalw PropLog.thy [is_true_def] "is_true(Fls,t) <-> False"; |
43 goalw PropLog.thy [is_true_def] "is_true(Fls,t) <-> False"; |
45 by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1); |
44 by (simp_tac (!simpset addsimps [one_not_0 RS not_sym]) 1); |
46 qed "is_true_Fls"; |
45 qed "is_true_Fls"; |
47 |
46 |
48 goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t"; |
47 goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t"; |
49 by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym] |
48 by (simp_tac (!simpset addsimps [one_not_0 RS not_sym] |
50 setloop (split_tac [expand_if])) 1); |
49 setloop (split_tac [expand_if])) 1); |
51 qed "is_true_Var"; |
50 qed "is_true_Var"; |
52 |
51 |
53 goalw PropLog.thy [is_true_def] |
52 goalw PropLog.thy [is_true_def] |
54 "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"; |
53 "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"; |
55 by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1); |
54 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
56 qed "is_true_Imp"; |
55 qed "is_true_Imp"; |
57 |
56 |
58 (** The function hyps **) |
57 (** The function hyps **) |
59 |
58 |
60 goalw PropLog.thy [hyps_def] "hyps(Fls,t) = 0"; |
59 goalw PropLog.thy [hyps_def] "hyps(Fls,t) = 0"; |
61 by (simp_tac prop_rec_ss 1); |
60 by (Simp_tac 1); |
62 qed "hyps_Fls"; |
61 qed "hyps_Fls"; |
63 |
62 |
64 goalw PropLog.thy [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}"; |
63 goalw PropLog.thy [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}"; |
65 by (simp_tac prop_rec_ss 1); |
64 by (Simp_tac 1); |
66 qed "hyps_Var"; |
65 qed "hyps_Var"; |
67 |
66 |
68 goalw PropLog.thy [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)"; |
67 goalw PropLog.thy [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)"; |
69 by (simp_tac prop_rec_ss 1); |
68 by (Simp_tac 1); |
70 qed "hyps_Imp"; |
69 qed "hyps_Imp"; |
71 |
70 |
72 val prop_ss = prop_rec_ss |
71 Addsimps prop.intrs; |
73 addsimps prop.intrs |
72 Addsimps [is_true_Fls, is_true_Var, is_true_Imp, |
74 addsimps [is_true_Fls, is_true_Var, is_true_Imp, |
73 hyps_Fls, hyps_Var, hyps_Imp]; |
75 hyps_Fls, hyps_Var, hyps_Imp]; |
|
76 |
74 |
77 (*** Proof theory of propositional logic ***) |
75 (*** Proof theory of propositional logic ***) |
78 |
76 |
79 goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)"; |
77 goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)"; |
80 by (rtac lfp_mono 1); |
78 by (rtac lfp_mono 1); |
173 (*Typical example of strengthening the induction formula*) |
171 (*Typical example of strengthening the induction formula*) |
174 val [major] = goal PropLog.thy |
172 val [major] = goal PropLog.thy |
175 "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)"; |
173 "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)"; |
176 by (rtac (expand_if RS iffD2) 1); |
174 by (rtac (expand_if RS iffD2) 1); |
177 by (rtac (major RS prop.induct) 1); |
175 by (rtac (major RS prop.induct) 1); |
178 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms.H]))); |
176 by (ALLGOALS (asm_simp_tac (!simpset addsimps [thms_I, thms.H]))); |
179 by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1, |
177 by (safe_tac (!claset addSEs [Fls_Imp RS weaken_left_Un1, |
180 Fls_Imp RS weaken_left_Un2])); |
178 Fls_Imp RS weaken_left_Un2])); |
181 by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, |
179 by (ALLGOALS (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2, |
182 weaken_right, Imp_Fls]))); |
180 weaken_right, Imp_Fls]))); |
183 qed "hyps_thms_if"; |
181 qed "hyps_thms_if"; |
184 |
182 |
185 (*Key lemma for completeness; yields a set of assumptions satisfying p*) |
183 (*Key lemma for completeness; yields a set of assumptions satisfying p*) |
186 val [premp,sat] = goalw PropLog.thy [logcon_def] |
184 val [premp,sat] = goalw PropLog.thy [logcon_def] |
187 "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p"; |
185 "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p"; |
188 by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN |
186 by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN |
189 rtac (premp RS hyps_thms_if) 2); |
187 rtac (premp RS hyps_thms_if) 2); |
190 by (fast_tac ZF_cs 1); |
188 by (Fast_tac 1); |
191 qed "logcon_thms_p"; |
189 qed "logcon_thms_p"; |
192 |
190 |
193 (*For proving certain theorems in our new propositional logic*) |
191 (*For proving certain theorems in our new propositional logic*) |
194 val thms_cs = |
192 val thms_cs = |
195 ZF_cs addSIs (prop.intrs @ [deduction]) |
193 ZF_cs addSIs (prop.intrs @ [deduction]) |
215 (*For the case hyps(p,t)-cons(#v,Y) |- p; |
213 (*For the case hyps(p,t)-cons(#v,Y) |- p; |
216 we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *) |
214 we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *) |
217 val [major] = goal PropLog.thy |
215 val [major] = goal PropLog.thy |
218 "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})"; |
216 "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})"; |
219 by (rtac (major RS prop.induct) 1); |
217 by (rtac (major RS prop.induct) 1); |
220 by (simp_tac prop_ss 1); |
218 by (Simp_tac 1); |
221 by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1); |
219 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
222 by (fast_tac (ZF_cs addSEs prop.free_SEs) 1); |
220 by (fast_tac (!claset addSEs prop.free_SEs) 1); |
223 by (asm_simp_tac prop_ss 1); |
221 by (Asm_simp_tac 1); |
224 by (fast_tac ZF_cs 1); |
222 by (Fast_tac 1); |
225 qed "hyps_Diff"; |
223 qed "hyps_Diff"; |
226 |
224 |
227 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p; |
225 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p; |
228 we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *) |
226 we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *) |
229 val [major] = goal PropLog.thy |
227 val [major] = goal PropLog.thy |
230 "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})"; |
228 "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})"; |
231 by (rtac (major RS prop.induct) 1); |
229 by (rtac (major RS prop.induct) 1); |
232 by (simp_tac prop_ss 1); |
230 by (Simp_tac 1); |
233 by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1); |
231 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
234 by (fast_tac (ZF_cs addSEs prop.free_SEs) 1); |
232 by (fast_tac (!claset addSEs prop.free_SEs) 1); |
235 by (asm_simp_tac prop_ss 1); |
233 by (Asm_simp_tac 1); |
236 by (fast_tac ZF_cs 1); |
234 by (Fast_tac 1); |
237 qed "hyps_cons"; |
235 qed "hyps_cons"; |
238 |
236 |
239 (** Two lemmas for use with weaken_left **) |
237 (** Two lemmas for use with weaken_left **) |
240 |
238 |
241 goal ZF.thy "B-C <= cons(a, B-cons(a,C))"; |
239 goal upair.thy "B-C <= cons(a, B-cons(a,C))"; |
242 by (fast_tac ZF_cs 1); |
240 by (Fast_tac 1); |
243 qed "cons_Diff_same"; |
241 qed "cons_Diff_same"; |
244 |
242 |
245 goal ZF.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))"; |
243 goal upair.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))"; |
246 by (fast_tac ZF_cs 1); |
244 by (Fast_tac 1); |
247 qed "cons_Diff_subset2"; |
245 qed "cons_Diff_subset2"; |
248 |
246 |
249 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls; |
247 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls; |
250 could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*) |
248 could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*) |
251 val [major] = goal PropLog.thy |
249 val [major] = goal PropLog.thy |
252 "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})"; |
250 "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})"; |
253 by (rtac (major RS prop.induct) 1); |
251 by (rtac (major RS prop.induct) 1); |
254 by (asm_simp_tac (prop_ss addsimps (Fin.intrs @ [UN_I, cons_iff]) |
252 by (asm_simp_tac (!simpset addsimps [UN_I] |
255 setloop (split_tac [expand_if])) 2); |
253 setloop (split_tac [expand_if])) 2); |
256 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin.emptyI, Fin_UnI]))); |
254 by (ALLGOALS Asm_simp_tac); |
|
255 by (fast_tac (!claset addIs Fin.intrs) 1); |
257 qed "hyps_finite"; |
256 qed "hyps_finite"; |
258 |
257 |
259 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; |
258 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; |
260 |
259 |
261 (*Induction on the finite set of assumptions hyps(p,t0). |
260 (*Induction on the finite set of assumptions hyps(p,t0). |
262 We may repeatedly subtract assumptions until none are left!*) |
261 We may repeatedly subtract assumptions until none are left!*) |
263 val [premp,sat] = goal PropLog.thy |
262 val [premp,sat] = goal PropLog.thy |
264 "[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p"; |
263 "[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p"; |
265 by (rtac (premp RS hyps_finite RS Fin_induct) 1); |
264 by (rtac (premp RS hyps_finite RS Fin_induct) 1); |
266 by (simp_tac (prop_ss addsimps [premp, sat, logcon_thms_p, Diff_0]) 1); |
265 by (simp_tac (!simpset addsimps [premp, sat, logcon_thms_p, Diff_0]) 1); |
267 by (safe_tac ZF_cs); |
266 by (safe_tac (!claset)); |
268 (*Case hyps(p,t)-cons(#v,Y) |- p *) |
267 (*Case hyps(p,t)-cons(#v,Y) |- p *) |
269 by (rtac thms_excluded_middle_rule 1); |
268 by (rtac thms_excluded_middle_rule 1); |
270 by (etac prop.Var_I 3); |
269 by (etac prop.Var_I 3); |
271 by (rtac (cons_Diff_same RS weaken_left) 1); |
270 by (rtac (cons_Diff_same RS weaken_left) 1); |
272 by (etac spec 1); |
271 by (etac spec 1); |
289 by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1); |
288 by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1); |
290 qed "completeness_0"; |
289 qed "completeness_0"; |
291 |
290 |
292 (*A semantic analogue of the Deduction Theorem*) |
291 (*A semantic analogue of the Deduction Theorem*) |
293 goalw PropLog.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q"; |
292 goalw PropLog.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q"; |
294 by (simp_tac prop_ss 1); |
293 by (Simp_tac 1); |
295 by (fast_tac ZF_cs 1); |
294 by (Fast_tac 1); |
296 qed "logcon_Imp"; |
295 qed "logcon_Imp"; |
297 |
296 |
298 goal PropLog.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p"; |
297 goal PropLog.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p"; |
299 by (etac Fin_induct 1); |
298 by (etac Fin_induct 1); |
300 by (safe_tac (ZF_cs addSIs [completeness_0])); |
299 by (safe_tac (!claset addSIs [completeness_0])); |
301 by (rtac (weaken_left_cons RS thms_MP) 1); |
300 by (rtac (weaken_left_cons RS thms_MP) 1); |
302 by (fast_tac (ZF_cs addSIs (logcon_Imp::prop.intrs)) 1); |
301 by (fast_tac (!claset addSIs (logcon_Imp::prop.intrs)) 1); |
303 by (fast_tac thms_cs 1); |
302 by (fast_tac thms_cs 1); |
304 qed "completeness_lemma"; |
303 qed "completeness_lemma"; |
305 |
304 |
306 val completeness = completeness_lemma RS bspec RS mp; |
305 val completeness = completeness_lemma RS bspec RS mp; |
307 |
306 |
308 val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop"; |
307 val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop"; |
309 by (fast_tac (ZF_cs addSEs [soundness, finite RS completeness, |
308 by (fast_tac (!claset addSEs [soundness, finite RS completeness, |
310 thms_in_pl]) 1); |
309 thms_in_pl]) 1); |
311 qed "thms_iff"; |
310 qed "thms_iff"; |
312 |
311 |
313 writeln"Reached end of file."; |
312 writeln"Reached end of file."; |