src/Sequents/LK.thy
 author wenzelm Mon Mar 19 21:10:33 2012 +0100 (2012-03-19) changeset 47022 8eac39af4ec0 parent 45602 2a858377c3d2 child 48891 c0eafbd55de3 permissions -rw-r--r--
moved some legacy stuff;
1 (*  Title:      Sequents/LK.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1993  University of Cambridge
5 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
6 link between |- and ==>, needed for instance to prove imp_cong.
8 Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
9 should be derived from lower-level axioms.
11 CANNOT be added to LK0.thy because modal logic is built upon it, and
12 various modal rules would become inconsistent.
13 *)
15 theory LK
16 imports LK0
17 uses ("simpdata.ML")
18 begin
20 axiomatization where
21   monotonic:  "(\$H |- P ==> \$H |- Q) ==> \$H, P |- Q" and
23   left_cong:  "[| P == P';  |- P' ==> (\$H |- \$F) == (\$H' |- \$F') |]
24                ==> (P, \$H |- \$F) == (P', \$H' |- \$F')"
27 subsection {* Rewrite rules *}
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
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
53 lemma not_simps:
54   "|- ~ False <-> True"
55   "|- ~ True <-> False"
56   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
57   done
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
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
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
89 subsection {* Miniscoping: pushing quantifiers in *}
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 *}
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
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
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
127 lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
128   apply (erule thinR [THEN cut])
129   apply (tactic {* fast_tac LK_pack 1 *})
130   done
132 lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
134 lemma P_iff_T: "|- P ==> |- (P <-> True)"
135   apply (erule thinR [THEN cut])
136   apply (tactic {* fast_tac LK_pack 1 *})
137   done
139 lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
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
152 subsection {* Named rewrite rules *}
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
159 lemmas conj_comms = conj_commute conj_left_commute
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
166 lemmas disj_comms = disj_commute disj_left_commute
168 lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)"
169   and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)"
171   and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)"
172   and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)"
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)"
178   and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)"
179   and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)"
181   and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)"
182   and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
184   and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
185   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
186   done
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
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
214 lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
215   apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
216   done
218 use "simpdata.ML"
219 setup {* Simplifier.map_simpset_global (K LK_ss) *}
222 text {* To create substition rules *}
224 lemma eq_imp_subst: "|- a=b ==> \$H, A(a), \$G |- \$E, A(b), \$F"
225   apply (tactic {* asm_simp_tac LK_basic_ss 1 *})
226   done
228 lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
229   apply (rule_tac P = Q in cut)
230    apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *})
231   apply (rule_tac P = "~Q" in cut)
232    apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *})
233   apply (tactic {* fast_tac LK_pack 1 *})
234   done
236 lemma if_cancel: "|- (if P then x else x) = x"
237   apply (tactic {* lemma_tac @{thm split_if} 1 *})
238   apply (tactic {* fast_tac LK_pack 1 *})
239   done
241 lemma if_eq_cancel: "|- (if x=y then y else x) = x"
242   apply (tactic {* lemma_tac @{thm split_if} 1 *})
243   apply (tactic {* safe_tac LK_pack 1 *})
244   apply (rule symL)
245   apply (rule basic)
246   done
248 end