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