1 (* Title: ZF/ex/prop-log.ML |
1 (* Title: ZF/ex/prop-log.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow & Lawrence C Paulson |
3 Author: Tobias Nipkow & Lawrence C Paulson |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 For ex/prop-log.thy. Inductive definition of propositional logic. |
6 For ex/prop-log.thy. Inductive definition of propositional logic. |
7 Soundness and completeness w.r.t. truth-tables. |
7 Soundness and completeness w.r.t. truth-tables. |
8 |
8 |
45 by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1); |
45 by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1); |
46 qed "is_true_Fls"; |
46 qed "is_true_Fls"; |
47 |
47 |
48 goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t"; |
48 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] |
49 by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym] |
50 setloop (split_tac [expand_if])) 1); |
50 setloop (split_tac [expand_if])) 1); |
51 qed "is_true_Var"; |
51 qed "is_true_Var"; |
52 |
52 |
53 goalw PropLog.thy [is_true_def] |
53 goalw PropLog.thy [is_true_def] |
54 "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"; |
54 "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); |
55 by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1); |
70 qed "hyps_Imp"; |
70 qed "hyps_Imp"; |
71 |
71 |
72 val prop_ss = prop_rec_ss |
72 val prop_ss = prop_rec_ss |
73 addsimps prop.intrs |
73 addsimps prop.intrs |
74 addsimps [is_true_Fls, is_true_Var, is_true_Imp, |
74 addsimps [is_true_Fls, is_true_Var, is_true_Imp, |
75 hyps_Fls, hyps_Var, hyps_Imp]; |
75 hyps_Fls, hyps_Var, hyps_Imp]; |
76 |
76 |
77 (*** Proof theory of propositional logic ***) |
77 (*** Proof theory of propositional logic ***) |
78 |
78 |
79 goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)"; |
79 goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)"; |
80 by (rtac lfp_mono 1); |
80 by (rtac lfp_mono 1); |
175 "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)"; |
175 "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)"; |
176 by (rtac (expand_if RS iffD2) 1); |
176 by (rtac (expand_if RS iffD2) 1); |
177 by (rtac (major RS prop.induct) 1); |
177 by (rtac (major RS prop.induct) 1); |
178 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms.H]))); |
178 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms.H]))); |
179 by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1, |
179 by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1, |
180 Fls_Imp RS weaken_left_Un2])); |
180 Fls_Imp RS weaken_left_Un2])); |
181 by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, |
181 by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, |
182 weaken_right, Imp_Fls]))); |
182 weaken_right, Imp_Fls]))); |
183 qed "hyps_thms_if"; |
183 qed "hyps_thms_if"; |
184 |
184 |
185 (*Key lemma for completeness; yields a set of assumptions satisfying p*) |
185 (*Key lemma for completeness; yields a set of assumptions satisfying p*) |
186 val [premp,sat] = goalw PropLog.thy [logcon_def] |
186 val [premp,sat] = goalw PropLog.thy [logcon_def] |
187 "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p"; |
187 "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p"; |
250 could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*) |
250 could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*) |
251 val [major] = goal PropLog.thy |
251 val [major] = goal PropLog.thy |
252 "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})"; |
252 "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})"; |
253 by (rtac (major RS prop.induct) 1); |
253 by (rtac (major RS prop.induct) 1); |
254 by (asm_simp_tac (prop_ss addsimps (Fin.intrs @ [UN_I, cons_iff]) |
254 by (asm_simp_tac (prop_ss addsimps (Fin.intrs @ [UN_I, cons_iff]) |
255 setloop (split_tac [expand_if])) 2); |
255 setloop (split_tac [expand_if])) 2); |
256 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin.emptyI, Fin_UnI]))); |
256 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin.emptyI, Fin_UnI]))); |
257 qed "hyps_finite"; |
257 qed "hyps_finite"; |
258 |
258 |
259 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; |
259 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; |
260 |
260 |
305 |
305 |
306 val completeness = completeness_lemma RS bspec RS mp; |
306 val completeness = completeness_lemma RS bspec RS mp; |
307 |
307 |
308 val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop"; |
308 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, |
309 by (fast_tac (ZF_cs addSEs [soundness, finite RS completeness, |
310 thms_in_pl]) 1); |
310 thms_in_pl]) 1); |
311 qed "thms_iff"; |
311 qed "thms_iff"; |
312 |
312 |
313 writeln"Reached end of file."; |
313 writeln"Reached end of file."; |