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