author | wenzelm |
Sat, 27 Oct 2001 00:09:59 +0200 | |
changeset 11963 | a6608d44a46b |
parent 11316 | b4e71bd751e4 |
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 |
||
11316 | 9 |
Prove: If H|=p then G|=p where G \\<in> Fin(H) |
0 | 10 |
*) |
11 |
||
6046 | 12 |
Addsimps prop.intrs; |
0 | 13 |
|
14 |
(*** Semantics of propositional logic ***) |
|
15 |
||
16 |
(** The function is_true **) |
|
17 |
||
5068 | 18 |
Goalw [is_true_def] "is_true(Fls,t) <-> False"; |
5618 | 19 |
by (Simp_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
20 |
qed "is_true_Fls"; |
0 | 21 |
|
11316 | 22 |
Goalw [is_true_def] "is_true(#v,t) <-> v \\<in> t"; |
5618 | 23 |
by (Simp_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
24 |
qed "is_true_Var"; |
0 | 25 |
|
5618 | 26 |
Goalw [is_true_def] "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"; |
27 |
by (Simp_tac 1); |
|
760 | 28 |
qed "is_true_Imp"; |
0 | 29 |
|
6046 | 30 |
Addsimps [is_true_Fls, is_true_Var, is_true_Imp]; |
0 | 31 |
|
32 |
||
33 |
(*** Proof theory of propositional logic ***) |
|
34 |
||
11316 | 35 |
Goalw thms.defs "G \\<subseteq> H ==> thms(G) \\<subseteq> thms(H)"; |
0 | 36 |
by (rtac lfp_mono 1); |
515 | 37 |
by (REPEAT (rtac thms.bnd_mono 1)); |
0 | 38 |
by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
39 |
qed "thms_mono"; |
0 | 40 |
|
515 | 41 |
val thms_in_pl = thms.dom_subset RS subsetD; |
0 | 42 |
|
11316 | 43 |
val ImpE = prop.mk_cases "p=>q \\<in> prop"; |
0 | 44 |
|
515 | 45 |
(*Stronger Modus Ponens rule: no typechecking!*) |
5137 | 46 |
Goal "[| H |- p=>q; H |- p |] ==> H |- q"; |
515 | 47 |
by (rtac thms.MP 1); |
0 | 48 |
by (REPEAT (eresolve_tac [asm_rl, thms_in_pl, thms_in_pl RS ImpE] 1)); |
760 | 49 |
qed "thms_MP"; |
0 | 50 |
|
51 |
(*Rule is called I for Identity Combinator, not for Introduction*) |
|
11316 | 52 |
Goal "p \\<in> prop ==> H |- p=>p"; |
515 | 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)); |
|
760 | 57 |
qed "thms_I"; |
0 | 58 |
|
59 |
(** Weakening, left and right **) |
|
60 |
||
11316 | 61 |
(* [| G \\<subseteq> 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
|
62 |
bind_thm ("weaken_left", (thms_mono RS subsetD)); |
0 | 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 |
||
11316 | 70 |
Goal "[| H |- q; p \\<in> prop |] ==> H |- p=>q"; |
515 | 71 |
by (rtac (thms.K RS thms_MP) 1); |
0 | 72 |
by (REPEAT (ares_tac [thms_in_pl] 1)); |
760 | 73 |
qed "weaken_right"; |
0 | 74 |
|
75 |
(*The deduction theorem*) |
|
11316 | 76 |
Goal "[| cons(p,H) |- q; p \\<in> prop |] ==> H |- p=>q"; |
515 | 77 |
by (etac thms.induct 1); |
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
78 |
by (blast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1); |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
79 |
by (blast_tac (claset() addIs [thms.K RS weaken_right]) 1); |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
80 |
by (blast_tac (claset() addIs [thms.S RS weaken_right]) 1); |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
81 |
by (blast_tac (claset() addIs [thms.DN RS weaken_right]) 1); |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
82 |
by (blast_tac (claset() addIs [thms.S RS thms_MP RS thms_MP]) 1); |
760 | 83 |
qed "deduction"; |
0 | 84 |
|
85 |
||
86 |
(*The cut rule*) |
|
5137 | 87 |
Goal "[| H|-p; cons(p,H) |- q |] ==> H |- q"; |
0 | 88 |
by (rtac (deduction RS thms_MP) 1); |
89 |
by (REPEAT (ares_tac [thms_in_pl] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
90 |
qed "cut"; |
0 | 91 |
|
11316 | 92 |
Goal "[| H |- Fls; p \\<in> prop |] ==> H |- p"; |
515 | 93 |
by (rtac (thms.DN RS thms_MP) 1); |
0 | 94 |
by (rtac weaken_right 2); |
515 | 95 |
by (REPEAT (ares_tac (prop.intrs@[consI1]) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
96 |
qed "thms_FlsE"; |
0 | 97 |
|
11316 | 98 |
(* [| H |- p=>Fls; H |- p; q \\<in> prop |] ==> H |- q *) |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
99 |
bind_thm ("thms_notE", (thms_MP RS thms_FlsE)); |
0 | 100 |
|
101 |
(*Soundness of the rules wrt truth-table semantics*) |
|
5137 | 102 |
Goalw [logcon_def] "H |- p ==> H |= p"; |
515 | 103 |
by (etac thms.induct 1); |
6046 | 104 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
105 |
qed "soundness"; |
0 | 106 |
|
107 |
(*** Towards the completeness proof ***) |
|
108 |
||
515 | 109 |
val [premf,premq] = goal PropLog.thy |
11316 | 110 |
"[| H |- p=>Fls; q \\<in> prop |] ==> H |- p=>q"; |
0 | 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); |
|
515 | 114 |
by (REPEAT (ares_tac [premq, consI1, thms.H] 1)); |
760 | 115 |
qed "Fls_Imp"; |
0 | 116 |
|
515 | 117 |
val [premp,premq] = goal PropLog.thy |
0 | 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); |
|
515 | 123 |
by (rtac (consI1 RS thms.H RS thms_MP) 1); |
0 | 124 |
by (rtac (premp RS weaken_left_cons) 2); |
515 | 125 |
by (REPEAT (ares_tac prop.intrs 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
126 |
qed "Imp_Fls"; |
0 | 127 |
|
128 |
(*Typical example of strengthening the induction formula*) |
|
11316 | 129 |
Goal "p \\<in> prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"; |
6046 | 130 |
by (Simp_tac 1); |
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
131 |
by (induct_tac "p" 1); |
4091 | 132 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H]))); |
133 |
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
|
134 |
Fls_Imp RS weaken_left_Un2])); |
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
135 |
by (ALLGOALS (blast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, |
5618 | 136 |
weaken_right, Imp_Fls]))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
137 |
qed "hyps_thms_if"; |
0 | 138 |
|
139 |
(*Key lemma for completeness; yields a set of assumptions satisfying p*) |
|
11316 | 140 |
Goalw [logcon_def] "[| p \\<in> prop; 0 |= p |] ==> hyps(p,t) |- p"; |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5137
diff
changeset
|
141 |
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
|
142 |
by (Asm_full_simp_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
143 |
qed "logcon_thms_p"; |
0 | 144 |
|
145 |
(*For proving certain theorems in our new propositional logic*) |
|
146 |
val thms_cs = |
|
515 | 147 |
ZF_cs addSIs (prop.intrs @ [deduction]) |
148 |
addIs [thms_in_pl, thms.H, thms.H RS thms_MP]; |
|
0 | 149 |
|
150 |
(*The excluded middle in the form of an elimination rule*) |
|
11316 | 151 |
Goal "[| p \\<in> prop; q \\<in> prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"; |
0 | 152 |
by (rtac (deduction RS deduction) 1); |
515 | 153 |
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
|
154 |
by (ALLGOALS (blast_tac thms_cs)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
155 |
qed "thms_excluded_middle"; |
0 | 156 |
|
157 |
(*Hard to prove directly because it requires cuts*) |
|
11316 | 158 |
Goal "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \\<in> prop |] ==> H |- q"; |
0 | 159 |
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
|
160 |
by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1)); |
760 | 161 |
qed "thms_excluded_middle_rule"; |
0 | 162 |
|
163 |
(*** Completeness -- lemmas for reducing the set of assumptions ***) |
|
164 |
||
165 |
(*For the case hyps(p,t)-cons(#v,Y) |- p; |
|
11316 | 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})"; |
|
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
168 |
by (induct_tac "p" 1); |
6141 | 169 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
170 |
qed "hyps_Diff"; |
0 | 171 |
|
172 |
(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p; |
|
11316 | 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})"; |
|
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
175 |
by (induct_tac "p" 1); |
6141 | 176 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
177 |
qed "hyps_cons"; |
0 | 178 |
|
179 |
(** Two lemmas for use with weaken_left **) |
|
180 |
||
11316 | 181 |
Goal "B-C \\<subseteq> cons(a, B-cons(a,C))"; |
2469 | 182 |
by (Fast_tac 1); |
760 | 183 |
qed "cons_Diff_same"; |
0 | 184 |
|
11316 | 185 |
Goal "cons(a, B-{c}) - D \\<subseteq> cons(a, B-cons(c,D))"; |
2469 | 186 |
by (Fast_tac 1); |
760 | 187 |
qed "cons_Diff_subset2"; |
0 | 188 |
|
189 |
(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls; |
|
11316 | 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})"; |
|
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
192 |
by (induct_tac "p" 1); |
11233 | 193 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
194 |
qed "hyps_finite"; |
0 | 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!*) |
|
515 | 200 |
val [premp,sat] = goal PropLog.thy |
11316 | 201 |
"[| p \\<in> prop; 0 |= p |] ==> \\<forall>t. hyps(p,t) - hyps(p,t0) |- p"; |
0 | 202 |
by (rtac (premp RS hyps_finite RS Fin_induct) 1); |
4091 | 203 |
by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1); |
4152 | 204 |
by Safe_tac; |
0 | 205 |
(*Case hyps(p,t)-cons(#v,Y) |- p *) |
206 |
by (rtac thms_excluded_middle_rule 1); |
|
515 | 207 |
by (etac prop.Var_I 3); |
0 | 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); |
|
515 | 215 |
by (etac prop.Var_I 3); |
0 | 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); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
221 |
qed "completeness_0_lemma"; |
0 | 222 |
|
223 |
(*The base case for completeness*) |
|
11316 | 224 |
val [premp,sat] = goal PropLog.thy "[| p \\<in> prop; 0 |= p |] ==> 0 |- p"; |
0 | 225 |
by (rtac (Diff_cancel RS subst) 1); |
226 |
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
|
227 |
qed "completeness_0"; |
0 | 228 |
|
229 |
(*A semantic analogue of the Deduction Theorem*) |
|
5137 | 230 |
Goalw [logcon_def] "[| cons(p,H) |= q |] ==> H |= p=>q"; |
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
231 |
by Auto_tac; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
232 |
qed "logcon_Imp"; |
0 | 233 |
|
11316 | 234 |
Goal "H \\<in> Fin(prop) ==> \\<forall>p \\<in> prop. H |= p --> H |- p"; |
0 | 235 |
by (etac Fin_induct 1); |
4091 | 236 |
by (safe_tac (claset() addSIs [completeness_0])); |
0 | 237 |
by (rtac (weaken_left_cons RS thms_MP) 1); |
5137 | 238 |
by (blast_tac (claset() addSIs (logcon_Imp::prop.intrs)) 1); |
239 |
by (blast_tac thms_cs 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
240 |
qed "completeness_lemma"; |
0 | 241 |
|
242 |
val completeness = completeness_lemma RS bspec RS mp; |
|
243 |
||
11316 | 244 |
val [finite] = goal PropLog.thy "H \\<in> Fin(prop) ==> H |- p <-> H |= p & p \\<in> prop"; |
4091 | 245 |
by (fast_tac (claset() addSEs [soundness, finite RS completeness, |
5618 | 246 |
thms_in_pl]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
247 |
qed "thms_iff"; |
0 | 248 |
|
249 |
writeln"Reached end of file."; |