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