1(*  Title:      Sequents/LK0.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1993  University of Cambridge
4
5There may be printing problems if a seqent is in expanded normal form
6(eta-expanded, beta-contracted).
7*)
8
9section \<open>Classical First-Order Sequent Calculus\<close>
10
11theory LK0
12imports Sequents
13begin
14
15setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
16
17class "term"
18default_sort "term"
19
20consts
21
22  Trueprop       :: "two_seqi"
23
24  True         :: o
25  False        :: o
26  equal        :: "['a,'a] \<Rightarrow> o"     (infixl "=" 50)
27  Not          :: "o \<Rightarrow> o"           ("\<not> _" [40] 40)
28  conj         :: "[o,o] \<Rightarrow> o"       (infixr "\<and>" 35)
29  disj         :: "[o,o] \<Rightarrow> o"       (infixr "\<or>" 30)
30  imp          :: "[o,o] \<Rightarrow> o"       (infixr "\<longrightarrow>" 25)
31  iff          :: "[o,o] \<Rightarrow> o"       (infixr "\<longleftrightarrow>" 25)
32  The          :: "('a \<Rightarrow> o) \<Rightarrow> 'a"  (binder "THE " 10)
33  All          :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder "\<forall>" 10)
34  Ex           :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder "\<exists>" 10)
35
36syntax
37 "_Trueprop"    :: "two_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
38
39parse_translation \<open>[(\<^syntax_const>\<open>_Trueprop\<close>, K (two_seq_tr \<^const_syntax>\<open>Trueprop\<close>))]\<close>
40print_translation \<open>[(\<^const_syntax>\<open>Trueprop\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Trueprop\<close>))]\<close>
41
42abbreviation
43  not_equal  (infixl "\<noteq>" 50) where
44  "x \<noteq> y \<equiv> \<not> (x = y)"
45
46axiomatization where
47
48  (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
49
50  contRS: "$H \<turnstile> $E, $S, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
51  contLS: "$H, $S, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and
52
53  thinRS: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
54  thinLS: "$H, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and
55
56  exchRS: "$H \<turnstile> $E, $R, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $R, $F" and
57  exchLS: "$H, $R, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $R, $G \<turnstile> $E" and
58
59  cut:   "\<lbrakk>$H \<turnstile> $E, P;  $H, P \<turnstile> $E\<rbrakk> \<Longrightarrow> $H \<turnstile> $E" and
60
61  (*Propositional rules*)
62
63  basic: "$H, P, $G \<turnstile> $E, P, $F" and
64
65  conjR: "\<lbrakk>$H\<turnstile> $E, P, $F;  $H\<turnstile> $E, Q, $F\<rbrakk> \<Longrightarrow> $H\<turnstile> $E, P \<and> Q, $F" and
66  conjL: "$H, P, Q, $G \<turnstile> $E \<Longrightarrow> $H, P \<and> Q, $G \<turnstile> $E" and
67
68  disjR: "$H \<turnstile> $E, P, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<or> Q, $F" and
69  disjL: "\<lbrakk>$H, P, $G \<turnstile> $E;  $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<or> Q, $G \<turnstile> $E" and
70
71  impR:  "$H, P \<turnstile> $E, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<longrightarrow> Q, $F" and
72  impL:  "\<lbrakk>$H,$G \<turnstile> $E,P;  $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longrightarrow> Q, $G \<turnstile> $E" and
73
74  notR:  "$H, P \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, \<not> P, $F" and
75  notL:  "$H, $G \<turnstile> $E, P \<Longrightarrow> $H, \<not> P, $G \<turnstile> $E" and
76
77  FalseL: "$H, False, $G \<turnstile> $E" and
78
79  True_def: "True \<equiv> False \<longrightarrow> False" and
80  iff_def:  "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
81
82axiomatization where
83  (*Quantifiers*)
84
85  allR:  "(\<And>x. $H \<turnstile> $E, P(x), $F) \<Longrightarrow> $H \<turnstile> $E, \<forall>x. P(x), $F" and
86  allL:  "$H, P(x), $G, \<forall>x. P(x) \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $E" and
87
88  exR:   "$H \<turnstile> $E, P(x), $F, \<exists>x. P(x) \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F" and
89  exL:   "(\<And>x. $H, P(x), $G \<turnstile> $E) \<Longrightarrow> $H, \<exists>x. P(x), $G \<turnstile> $E" and
90
91  (*Equality*)
92  refl:  "$H \<turnstile> $E, a = a, $F" and
93  subst: "\<And>G H E. $H(a), $G(a) \<turnstile> $E(a) \<Longrightarrow> $H(b), a=b, $G(b) \<turnstile> $E(b)"
94
95  (* Reflection *)
96
97axiomatization where
98  eq_reflection:  "\<turnstile> x = y \<Longrightarrow> (x \<equiv> y)" and
99  iff_reflection: "\<turnstile> P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> Q)"
100
101  (*Descriptions*)
102
103axiomatization where
104  The: "\<lbrakk>$H \<turnstile> $E, P(a), $F;  \<And>x.$H, P(x) \<turnstile> $E, x=a, $F\<rbrakk> \<Longrightarrow>
105         $H \<turnstile> $E, P(THE x. P(x)), $F"
106
107definition If :: "[o, 'a, 'a] \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" 10)
108  where "If(P,x,y) \<equiv> THE z::'a. (P \<longrightarrow> z = x) \<and> (\<not> P \<longrightarrow> z = y)"
109
110
111(** Structural Rules on formulas **)
112
113(*contraction*)
114
115lemma contR: "$H \<turnstile> $E, P, P, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
116  by (rule contRS)
117
118lemma contL: "$H, P, P, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
119  by (rule contLS)
120
121(*thinning*)
122
123lemma thinR: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
124  by (rule thinRS)
125
126lemma thinL: "$H, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
127  by (rule thinLS)
128
129(*exchange*)
130
131lemma exchR: "$H \<turnstile> $E, Q, P, $F \<Longrightarrow> $H \<turnstile> $E, P, Q, $F"
132  by (rule exchRS)
133
134lemma exchL: "$H, Q, P, $G \<turnstile> $E \<Longrightarrow> $H, P, Q, $G \<turnstile> $E"
135  by (rule exchLS)
136
137ML \<open>
138(*Cut and thin, replacing the right-side formula*)
139fun cutR_tac ctxt s i =
140  Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
141  resolve_tac ctxt @{thms thinR} i
142
143(*Cut and thin, replacing the left-side formula*)
144fun cutL_tac ctxt s i =
145  Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
146  resolve_tac ctxt @{thms thinL} (i + 1)
147\<close>
148
149
150(** If-and-only-if rules **)
151lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F;  $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
152  apply (unfold iff_def)
153  apply (assumption | rule conjR impR)+
154  done
155
156lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q;  $H,Q,P,$G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
157  apply (unfold iff_def)
158  apply (assumption | rule conjL impL basic)+
159  done
160
161lemma iff_refl: "$H \<turnstile> $E, (P \<longleftrightarrow> P), $F"
162  apply (rule iffR basic)+
163  done
164
165lemma TrueR: "$H \<turnstile> $E, True, $F"
166  apply (unfold True_def)
167  apply (rule impR)
168  apply (rule basic)
169  done
170
171(*Descriptions*)
172lemma the_equality:
173  assumes p1: "$H \<turnstile> $E, P(a), $F"
174    and p2: "\<And>x. $H, P(x) \<turnstile> $E, x=a, $F"
175  shows "$H \<turnstile> $E, (THE x. P(x)) = a, $F"
176  apply (rule cut)
177   apply (rule_tac [2] p2)
178  apply (rule The, rule thinR, rule exchRS, rule p1)
179  apply (rule thinR, rule exchRS, rule p2)
180  done
181
182
183(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
184
185lemma allL_thin: "$H, P(x), $G \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $E"
186  apply (rule allL)
187  apply (erule thinL)
188  done
189
190lemma exR_thin: "$H \<turnstile> $E, P(x), $F \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F"
191  apply (rule exR)
192  apply (erule thinR)
193  done
194
195(*The rules of LK*)
196
197lemmas [safe] =
198  iffR iffL
199  notR notL
200  impR impL
201  disjR disjL
202  conjR conjL
203  FalseL TrueR
204  refl basic
205ML \<open>val prop_pack = Cla.get_pack \<^context>\<close>
206
207lemmas [safe] = exL allR
208lemmas [unsafe] = the_equality exR_thin allL_thin
209ML \<open>val LK_pack = Cla.get_pack \<^context>\<close>
210
211ML \<open>
212  val LK_dup_pack =
213    Cla.put_pack prop_pack \<^context>
214    |> fold_rev Cla.add_safe @{thms allR exL}
215    |> fold_rev Cla.add_unsafe @{thms allL exR the_equality}
216    |> Cla.get_pack;
217\<close>
218
219method_setup fast_prop =
220  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack prop_pack ctxt)))\<close>
221
222method_setup fast_dup =
223  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack LK_dup_pack ctxt)))\<close>
224
225method_setup best_dup =
226  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt)))\<close>
227
228method_setup lem = \<open>
229  Attrib.thm >> (fn th => fn ctxt =>
230    SIMPLE_METHOD' (fn i =>
231      resolve_tac ctxt [@{thm thinR} RS @{thm cut}] i THEN
232      REPEAT (resolve_tac ctxt @{thms thinL} i) THEN
233      resolve_tac ctxt [th] i))
234\<close>
235
236
237lemma mp_R:
238  assumes major: "$H \<turnstile> $E, $F, P \<longrightarrow> Q"
239    and minor: "$H \<turnstile> $E, $F, P"
240  shows "$H \<turnstile> $E, Q, $F"
241  apply (rule thinRS [THEN cut], rule major)
242  apply step
243  apply (rule thinR, rule minor)
244  done
245
246lemma mp_L:
247  assumes major: "$H, $G \<turnstile> $E, P \<longrightarrow> Q"
248    and minor: "$H, $G, Q \<turnstile> $E"
249  shows "$H, P, $G \<turnstile> $E"
250  apply (rule thinL [THEN cut], rule major)
251  apply step
252  apply (rule thinL, rule minor)
253  done
254
255
256(** Two rules to generate left- and right- rules from implications **)
257
258lemma R_of_imp:
259  assumes major: "\<turnstile> P \<longrightarrow> Q"
260    and minor: "$H \<turnstile> $E, $F, P"
261  shows "$H \<turnstile> $E, Q, $F"
262  apply (rule mp_R)
263   apply (rule_tac [2] minor)
264  apply (rule thinRS, rule major [THEN thinLS])
265  done
266
267lemma L_of_imp:
268  assumes major: "\<turnstile> P \<longrightarrow> Q"
269    and minor: "$H, $G, Q \<turnstile> $E"
270  shows "$H, P, $G \<turnstile> $E"
271  apply (rule mp_L)
272   apply (rule_tac [2] minor)
273  apply (rule thinRS, rule major [THEN thinLS])
274  done
275
276(*Can be used to create implications in a subgoal*)
277lemma backwards_impR:
278  assumes prem: "$H, $G \<turnstile> $E, $F, P \<longrightarrow> Q"
279  shows "$H, P, $G \<turnstile> $E, Q, $F"
280  apply (rule mp_L)
281   apply (rule_tac [2] basic)
282  apply (rule thinR, rule prem)
283  done
284
285lemma conjunct1: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>P"
286  apply (erule thinR [THEN cut])
287  apply fast
288  done
289
290lemma conjunct2: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>Q"
291  apply (erule thinR [THEN cut])
292  apply fast
293  done
294
295lemma spec: "\<turnstile> (\<forall>x. P(x)) \<Longrightarrow> \<turnstile> P(x)"
296  apply (erule thinR [THEN cut])
297  apply fast
298  done
299
300
301(** Equality **)
302
303lemma sym: "\<turnstile> a = b \<longrightarrow> b = a"
304  by (safe add!: subst)
305
306lemma trans: "\<turnstile> a = b \<longrightarrow> b = c \<longrightarrow> a = c"
307  by (safe add!: subst)
308
309(* Symmetry of equality in hypotheses *)
310lemmas symL = sym [THEN L_of_imp]
311
312(* Symmetry of equality in hypotheses *)
313lemmas symR = sym [THEN R_of_imp]
314
315lemma transR: "\<lbrakk>$H\<turnstile> $E, $F, a = b;  $H\<turnstile> $E, $F, b=c\<rbrakk> \<Longrightarrow> $H\<turnstile> $E, a = c, $F"
316  by (rule trans [THEN R_of_imp, THEN mp_R])
317
318(* Two theorms for rewriting only one instance of a definition:
319   the first for definitions of formulae and the second for terms *)
320
321lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A \<longleftrightarrow> B"
322  apply unfold
323  apply (rule iff_refl)
324  done
325
326lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A = B"
327  apply unfold
328  apply (rule refl)
329  done
330
331
332(** if-then-else rules **)
333
334lemma if_True: "\<turnstile> (if True then x else y) = x"
335  unfolding If_def by fast
336
337lemma if_False: "\<turnstile> (if False then x else y) = y"
338  unfolding If_def by fast
339
340lemma if_P: "\<turnstile> P \<Longrightarrow> \<turnstile> (if P then x else y) = x"
341  apply (unfold If_def)
342  apply (erule thinR [THEN cut])
343  apply fast
344  done
345
346lemma if_not_P: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (if P then x else y) = y"
347  apply (unfold If_def)
348  apply (erule thinR [THEN cut])
349  apply fast
350  done
351
352end
353