author | haftmann |
Wed, 21 Oct 2009 10:15:31 +0200 | |
changeset 33040 | cffdb7b28498 |
parent 30607 | c3d1590debd8 |
child 41959 | b460124855b8 |
permissions | -rw-r--r-- |
17481 | 1 |
(* Title: LK/LK.ML |
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
3 |
Copyright 1993 University of Cambridge |
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
4 |
|
7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset
|
5 |
Axiom to express monotonicity (a variant of the deduction theorem). Makes the |
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset
|
6 |
link between |- and ==>, needed for instance to prove imp_cong. |
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
7 |
|
7117 | 8 |
Axiom left_cong allows the simplifier to use left-side formulas. Ideally it |
9 |
should be derived from lower-level axioms. |
|
10 |
||
7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset
|
11 |
CANNOT be added to LK0.thy because modal logic is built upon it, and |
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset
|
12 |
various modal rules would become inconsistent. |
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
13 |
*) |
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
14 |
|
17481 | 15 |
theory LK |
16 |
imports LK0 |
|
17 |
uses ("simpdata.ML") |
|
18 |
begin |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
19 |
|
27149 | 20 |
axiomatization where |
21 |
monotonic: "($H |- P ==> $H |- Q) ==> $H, P |- Q" and |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
22 |
|
17481 | 23 |
left_cong: "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |] |
24 |
==> (P, $H |- $F) == (P', $H' |- $F')" |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
25 |
|
27149 | 26 |
|
27 |
subsection {* Rewrite rules *} |
|
28 |
||
29 |
lemma conj_simps: |
|
30 |
"|- P & True <-> P" |
|
31 |
"|- True & P <-> P" |
|
32 |
"|- P & False <-> False" |
|
33 |
"|- False & P <-> False" |
|
34 |
"|- P & P <-> P" |
|
35 |
"|- P & P & Q <-> P & Q" |
|
36 |
"|- P & ~P <-> False" |
|
37 |
"|- ~P & P <-> False" |
|
38 |
"|- (P & Q) & R <-> P & (Q & R)" |
|
39 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
40 |
done |
|
41 |
||
42 |
lemma disj_simps: |
|
43 |
"|- P | True <-> True" |
|
44 |
"|- True | P <-> True" |
|
45 |
"|- P | False <-> P" |
|
46 |
"|- False | P <-> P" |
|
47 |
"|- P | P <-> P" |
|
48 |
"|- P | P | Q <-> P | Q" |
|
49 |
"|- (P | Q) | R <-> P | (Q | R)" |
|
50 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
51 |
done |
|
52 |
||
53 |
lemma not_simps: |
|
54 |
"|- ~ False <-> True" |
|
55 |
"|- ~ True <-> False" |
|
56 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
57 |
done |
|
58 |
||
59 |
lemma imp_simps: |
|
60 |
"|- (P --> False) <-> ~P" |
|
61 |
"|- (P --> True) <-> True" |
|
62 |
"|- (False --> P) <-> True" |
|
63 |
"|- (True --> P) <-> P" |
|
64 |
"|- (P --> P) <-> True" |
|
65 |
"|- (P --> ~P) <-> ~P" |
|
66 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
67 |
done |
|
68 |
||
69 |
lemma iff_simps: |
|
70 |
"|- (True <-> P) <-> P" |
|
71 |
"|- (P <-> True) <-> P" |
|
72 |
"|- (P <-> P) <-> True" |
|
73 |
"|- (False <-> P) <-> ~P" |
|
74 |
"|- (P <-> False) <-> ~P" |
|
75 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
76 |
done |
|
77 |
||
78 |
lemma quant_simps: |
|
79 |
"!!P. |- (ALL x. P) <-> P" |
|
80 |
"!!P. |- (ALL x. x=t --> P(x)) <-> P(t)" |
|
81 |
"!!P. |- (ALL x. t=x --> P(x)) <-> P(t)" |
|
82 |
"!!P. |- (EX x. P) <-> P" |
|
83 |
"!!P. |- (EX x. x=t & P(x)) <-> P(t)" |
|
84 |
"!!P. |- (EX x. t=x & P(x)) <-> P(t)" |
|
85 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
86 |
done |
|
87 |
||
88 |
||
89 |
subsection {* Miniscoping: pushing quantifiers in *} |
|
90 |
||
91 |
text {* |
|
92 |
We do NOT distribute of ALL over &, or dually that of EX over | |
|
93 |
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) |
|
94 |
show that this step can increase proof length! |
|
95 |
*} |
|
96 |
||
97 |
text {*existential miniscoping*} |
|
98 |
lemma ex_simps: |
|
99 |
"!!P Q. |- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q" |
|
100 |
"!!P Q. |- (EX x. P & Q(x)) <-> P & (EX x. Q(x))" |
|
101 |
"!!P Q. |- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q" |
|
102 |
"!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))" |
|
103 |
"!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q" |
|
104 |
"!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))" |
|
105 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
106 |
done |
|
107 |
||
108 |
text {*universal miniscoping*} |
|
109 |
lemma all_simps: |
|
110 |
"!!P Q. |- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q" |
|
111 |
"!!P Q. |- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))" |
|
112 |
"!!P Q. |- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q" |
|
113 |
"!!P Q. |- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))" |
|
114 |
"!!P Q. |- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q" |
|
115 |
"!!P Q. |- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))" |
|
116 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
117 |
done |
|
118 |
||
119 |
text {*These are NOT supplied by default!*} |
|
120 |
lemma distrib_simps: |
|
121 |
"|- P & (Q | R) <-> P&Q | P&R" |
|
122 |
"|- (Q | R) & P <-> Q&P | R&P" |
|
123 |
"|- (P | Q --> R) <-> (P --> R) & (Q --> R)" |
|
124 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
125 |
done |
|
126 |
||
127 |
lemma P_iff_F: "|- ~P ==> |- (P <-> False)" |
|
128 |
apply (erule thinR [THEN cut]) |
|
129 |
apply (tactic {* fast_tac LK_pack 1 *}) |
|
130 |
done |
|
131 |
||
132 |
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard] |
|
133 |
||
134 |
lemma P_iff_T: "|- P ==> |- (P <-> True)" |
|
135 |
apply (erule thinR [THEN cut]) |
|
136 |
apply (tactic {* fast_tac LK_pack 1 *}) |
|
137 |
done |
|
138 |
||
139 |
lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard] |
|
140 |
||
141 |
||
142 |
lemma LK_extra_simps: |
|
143 |
"|- P | ~P" |
|
144 |
"|- ~P | P" |
|
145 |
"|- ~ ~ P <-> P" |
|
146 |
"|- (~P --> P) <-> P" |
|
147 |
"|- (~P <-> ~Q) <-> (P<->Q)" |
|
148 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
149 |
done |
|
150 |
||
151 |
||
152 |
subsection {* Named rewrite rules *} |
|
153 |
||
154 |
lemma conj_commute: "|- P&Q <-> Q&P" |
|
155 |
and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)" |
|
156 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
157 |
done |
|
158 |
||
159 |
lemmas conj_comms = conj_commute conj_left_commute |
|
160 |
||
161 |
lemma disj_commute: "|- P|Q <-> Q|P" |
|
162 |
and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)" |
|
163 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
164 |
done |
|
165 |
||
166 |
lemmas disj_comms = disj_commute disj_left_commute |
|
167 |
||
168 |
lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)" |
|
169 |
and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)" |
|
170 |
||
171 |
and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)" |
|
172 |
and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)" |
|
173 |
||
174 |
and imp_conj_distrib: "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)" |
|
175 |
and imp_conj: "|- ((P&Q)-->R) <-> (P --> (Q --> R))" |
|
176 |
and imp_disj: "|- (P|Q --> R) <-> (P-->R) & (Q-->R)" |
|
177 |
||
178 |
and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)" |
|
179 |
and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)" |
|
180 |
||
181 |
and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)" |
|
182 |
and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)" |
|
183 |
||
184 |
and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)" |
|
185 |
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) |
|
186 |
done |
|
187 |
||
188 |
lemma imp_cong: |
|
189 |
assumes p1: "|- P <-> P'" |
|
190 |
and p2: "|- P' ==> |- Q <-> Q'" |
|
191 |
shows "|- (P-->Q) <-> (P'-->Q')" |
|
192 |
apply (tactic {* lemma_tac @{thm p1} 1 *}) |
|
193 |
apply (tactic {* safe_tac LK_pack 1 *}) |
|
194 |
apply (tactic {* |
|
195 |
REPEAT (rtac @{thm cut} 1 THEN |
|
196 |
DEPTH_SOLVE_1 |
|
197 |
(resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
|
198 |
safe_tac LK_pack 1) *}) |
|
199 |
done |
|
200 |
||
201 |
lemma conj_cong: |
|
202 |
assumes p1: "|- P <-> P'" |
|
203 |
and p2: "|- P' ==> |- Q <-> Q'" |
|
204 |
shows "|- (P&Q) <-> (P'&Q')" |
|
205 |
apply (tactic {* lemma_tac @{thm p1} 1 *}) |
|
206 |
apply (tactic {* safe_tac LK_pack 1 *}) |
|
207 |
apply (tactic {* |
|
208 |
REPEAT (rtac @{thm cut} 1 THEN |
|
209 |
DEPTH_SOLVE_1 |
|
210 |
(resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
|
211 |
safe_tac LK_pack 1) *}) |
|
212 |
done |
|
213 |
||
214 |
lemma eq_sym_conv: "|- (x=y) <-> (y=x)" |
|
215 |
apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *}) |
|
216 |
done |
|
217 |
||
17481 | 218 |
use "simpdata.ML" |
219 |
||
27149 | 220 |
|
221 |
text {* To create substition rules *} |
|
222 |
||
223 |
lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F" |
|
224 |
apply (tactic {* asm_simp_tac LK_basic_ss 1 *}) |
|
225 |
done |
|
226 |
||
227 |
lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" |
|
228 |
apply (rule_tac P = Q in cut) |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
28952
diff
changeset
|
229 |
apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *}) |
27149 | 230 |
apply (rule_tac P = "~Q" in cut) |
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
28952
diff
changeset
|
231 |
apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *}) |
27149 | 232 |
apply (tactic {* fast_tac LK_pack 1 *}) |
233 |
done |
|
234 |
||
235 |
lemma if_cancel: "|- (if P then x else x) = x" |
|
236 |
apply (tactic {* lemma_tac @{thm split_if} 1 *}) |
|
237 |
apply (tactic {* fast_tac LK_pack 1 *}) |
|
238 |
done |
|
239 |
||
240 |
lemma if_eq_cancel: "|- (if x=y then y else x) = x" |
|
241 |
apply (tactic {* lemma_tac @{thm split_if} 1 *}) |
|
242 |
apply (tactic {* safe_tac LK_pack 1 *}) |
|
243 |
apply (rule symL) |
|
244 |
apply (rule basic) |
|
245 |
done |
|
246 |
||
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
247 |
end |