author | wenzelm |
Fri, 08 Jan 2021 22:30:32 +0100 | |
changeset 73110 | c87ca43ebd3b |
parent 69605 | a96320074298 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: Sequents/LK.thy |
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 |
61386 | 6 |
link between \<turnstile> and \<Longrightarrow>, 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 |
begin |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
18 |
|
27149 | 19 |
axiomatization where |
61386 | 20 |
monotonic: "($H \<turnstile> P \<Longrightarrow> $H \<turnstile> Q) \<Longrightarrow> $H, P \<turnstile> Q" and |
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
21 |
|
61386 | 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')" |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
24 |
|
27149 | 25 |
|
60770 | 26 |
subsection \<open>Rewrite rules\<close> |
27149 | 27 |
|
28 |
lemma conj_simps: |
|
61386 | 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)" |
|
55228 | 38 |
by (fast add!: subst)+ |
27149 | 39 |
|
40 |
lemma disj_simps: |
|
61386 | 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)" |
|
55228 | 48 |
by (fast add!: subst)+ |
27149 | 49 |
|
50 |
lemma not_simps: |
|
61386 | 51 |
"\<turnstile> \<not> False \<longleftrightarrow> True" |
52 |
"\<turnstile> \<not> True \<longleftrightarrow> False" |
|
55228 | 53 |
by (fast add!: subst)+ |
27149 | 54 |
|
55 |
lemma imp_simps: |
|
61386 | 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" |
|
55228 | 62 |
by (fast add!: subst)+ |
27149 | 63 |
|
64 |
lemma iff_simps: |
|
61386 | 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" |
|
55228 | 70 |
by (fast add!: subst)+ |
27149 | 71 |
|
72 |
lemma quant_simps: |
|
61386 | 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)" |
|
55228 | 79 |
by (fast add!: subst)+ |
27149 | 80 |
|
81 |
||
60770 | 82 |
subsection \<open>Miniscoping: pushing quantifiers in\<close> |
27149 | 83 |
|
60770 | 84 |
text \<open> |
61385 | 85 |
We do NOT distribute of \<forall> over \<and>, or dually that of \<exists> over \<or> |
27149 | 86 |
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) |
87 |
show that this step can increase proof length! |
|
60770 | 88 |
\<close> |
27149 | 89 |
|
60770 | 90 |
text \<open>existential miniscoping\<close> |
27149 | 91 |
lemma ex_simps: |
61386 | 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))" |
|
55228 | 98 |
by (fast add!: subst)+ |
27149 | 99 |
|
60770 | 100 |
text \<open>universal miniscoping\<close> |
27149 | 101 |
lemma all_simps: |
61386 | 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))" |
|
55228 | 108 |
by (fast add!: subst)+ |
27149 | 109 |
|
60770 | 110 |
text \<open>These are NOT supplied by default!\<close> |
27149 | 111 |
lemma distrib_simps: |
61386 | 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)" |
|
55228 | 115 |
by (fast add!: subst)+ |
27149 | 116 |
|
61386 | 117 |
lemma P_iff_F: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> False)" |
27149 | 118 |
apply (erule thinR [THEN cut]) |
55228 | 119 |
apply fast |
27149 | 120 |
done |
121 |
||
45602 | 122 |
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection] |
27149 | 123 |
|
61386 | 124 |
lemma P_iff_T: "\<turnstile> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> True)" |
27149 | 125 |
apply (erule thinR [THEN cut]) |
55228 | 126 |
apply fast |
27149 | 127 |
done |
128 |
||
45602 | 129 |
lemmas iff_reflection_T = P_iff_T [THEN iff_reflection] |
27149 | 130 |
|
131 |
||
132 |
lemma LK_extra_simps: |
|
61386 | 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)" |
|
55228 | 138 |
by (fast add!: subst)+ |
27149 | 139 |
|
140 |
||
60770 | 141 |
subsection \<open>Named rewrite rules\<close> |
27149 | 142 |
|
61386 | 143 |
lemma 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)" |
|
55228 | 145 |
by (fast add!: subst)+ |
27149 | 146 |
|
147 |
lemmas conj_comms = conj_commute conj_left_commute |
|
148 |
||
61386 | 149 |
lemma 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)" |
|
55228 | 151 |
by (fast add!: subst)+ |
27149 | 152 |
|
153 |
lemmas disj_comms = disj_commute disj_left_commute |
|
154 |
||
61386 | 155 |
lemma 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)" |
|
27149 | 157 |
|
61386 | 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)" |
|
27149 | 160 |
|
61386 | 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)" |
|
27149 | 164 |
|
61386 | 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)" |
|
27149 | 167 |
|
61386 | 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)" |
|
27149 | 170 |
|
61386 | 171 |
and not_iff: "\<turnstile> \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" |
55228 | 172 |
by (fast add!: subst)+ |
27149 | 173 |
|
174 |
lemma imp_cong: |
|
61386 | 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')" |
|
55233 | 178 |
apply (lem p1) |
55228 | 179 |
apply safe |
60770 | 180 |
apply (tactic \<open> |
69593 | 181 |
REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN |
27149 | 182 |
DEPTH_SOLVE_1 |
69593 | 183 |
(resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
184 |
Cla.safe_tac \<^context> 1)\<close>) |
|
27149 | 185 |
done |
186 |
||
187 |
lemma conj_cong: |
|
61386 | 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')" |
|
55233 | 191 |
apply (lem p1) |
55228 | 192 |
apply safe |
60770 | 193 |
apply (tactic \<open> |
69593 | 194 |
REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN |
27149 | 195 |
DEPTH_SOLVE_1 |
69593 | 196 |
(resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN |
197 |
Cla.safe_tac \<^context> 1)\<close>) |
|
27149 | 198 |
done |
199 |
||
61386 | 200 |
lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x" |
55228 | 201 |
by (fast add!: subst) |
27149 | 202 |
|
69605 | 203 |
ML_file \<open>simpdata.ML\<close> |
60770 | 204 |
setup \<open>map_theory_simpset (put_simpset LK_ss)\<close> |
205 |
setup \<open>Simplifier.method_setup []\<close> |
|
17481 | 206 |
|
27149 | 207 |
|
63530 | 208 |
text \<open>To create substitution rules\<close> |
27149 | 209 |
|
61386 | 210 |
lemma eq_imp_subst: "\<turnstile> a = b \<Longrightarrow> $H, A(a), $G \<turnstile> $E, A(b), $F" |
55230 | 211 |
by simp |
27149 | 212 |
|
61386 | 213 |
lemma split_if: "\<turnstile> P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) \<and> (\<not> Q \<longrightarrow> P(y)))" |
27149 | 214 |
apply (rule_tac P = Q in cut) |
55230 | 215 |
prefer 2 |
216 |
apply (simp add: if_P) |
|
61385 | 217 |
apply (rule_tac P = "\<not> Q" in cut) |
55230 | 218 |
prefer 2 |
219 |
apply (simp add: if_not_P) |
|
55228 | 220 |
apply fast |
27149 | 221 |
done |
222 |
||
61386 | 223 |
lemma if_cancel: "\<turnstile> (if P then x else x) = x" |
55233 | 224 |
apply (lem split_if) |
55228 | 225 |
apply fast |
27149 | 226 |
done |
227 |
||
61386 | 228 |
lemma if_eq_cancel: "\<turnstile> (if x = y then y else x) = x" |
55233 | 229 |
apply (lem split_if) |
55228 | 230 |
apply safe |
27149 | 231 |
apply (rule symL) |
232 |
apply (rule basic) |
|
233 |
done |
|
234 |
||
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
235 |
end |