src/Sequents/LK0.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 12662 a9bbba3473f3
child 14765 bafb24c150c1
permissions -rw-r--r--
use more symbols in HTML output
paulson@7093
     1
(*  Title:      LK/LK0
paulson@7093
     2
    ID:         $Id$
paulson@7093
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7093
     4
    Copyright   1993  University of Cambridge
paulson@7093
     5
paulson@7093
     6
Classical First-Order Sequent Calculus
paulson@7093
     7
paulson@7093
     8
There may be printing problems if a seqent is in expanded normal form
paulson@7093
     9
	(eta-expanded, beta-contracted)
paulson@7093
    10
*)
paulson@7093
    11
paulson@7093
    12
LK0 = Sequents +
paulson@7093
    13
paulson@7093
    14
global
paulson@7093
    15
paulson@7093
    16
classes
paulson@7093
    17
  term < logic
paulson@7093
    18
paulson@7093
    19
default
paulson@7093
    20
  term
paulson@7093
    21
paulson@7093
    22
consts
paulson@7093
    23
paulson@7093
    24
 Trueprop	:: "two_seqi"
paulson@7093
    25
 "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
paulson@7093
    26
paulson@7093
    27
  True,False   :: o
paulson@7093
    28
  "="          :: ['a,'a] => o       (infixl 50)
paulson@7093
    29
  Not          :: o => o             ("~ _" [40] 40)
paulson@7093
    30
  "&"          :: [o,o] => o         (infixr 35)
paulson@7093
    31
  "|"          :: [o,o] => o         (infixr 30)
paulson@7093
    32
  "-->","<->"  :: [o,o] => o         (infixr 25)
paulson@7093
    33
  The          :: ('a => o) => 'a    (binder "THE " 10)
paulson@7093
    34
  All          :: ('a => o) => o     (binder "ALL " 10)
paulson@7093
    35
  Ex           :: ('a => o) => o     (binder "EX " 10)
paulson@7093
    36
paulson@7093
    37
syntax
wenzelm@12662
    38
  "_not_equal" :: ['a, 'a] => o                (infixl "~=" 50)
paulson@7093
    39
paulson@7093
    40
translations
paulson@7093
    41
  "x ~= y"      == "~ (x = y)"
paulson@7093
    42
wenzelm@12116
    43
syntax (xsymbols)
paulson@7093
    44
  Not           :: o => o               ("\\<not> _" [40] 40)
paulson@7093
    45
  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
paulson@7093
    46
  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
wenzelm@12116
    47
  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
wenzelm@12116
    48
  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 25)
paulson@7093
    49
  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
paulson@7093
    50
  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
paulson@7093
    51
  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
wenzelm@12662
    52
  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
paulson@7093
    53
paulson@7093
    54
syntax (HTML output)
paulson@7093
    55
  Not           :: o => o               ("\\<not> _" [40] 40)
kleing@14565
    56
  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
kleing@14565
    57
  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
kleing@14565
    58
  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
kleing@14565
    59
  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
kleing@14565
    60
  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
kleing@14565
    61
  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
paulson@7093
    62
paulson@7093
    63
paulson@7093
    64
local
paulson@7093
    65
  
paulson@7093
    66
rules
paulson@7093
    67
paulson@7093
    68
  (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
paulson@7093
    69
paulson@7093
    70
  contRS "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
paulson@7093
    71
  contLS "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
paulson@7093
    72
paulson@7093
    73
  thinRS "$H |- $E, $F ==> $H |- $E, $S, $F"
paulson@7093
    74
  thinLS "$H, $G |- $E ==> $H, $S, $G |- $E"
paulson@7093
    75
paulson@7093
    76
  exchRS "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
paulson@7093
    77
  exchLS "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
paulson@7093
    78
paulson@7093
    79
  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
paulson@7093
    80
paulson@7093
    81
  (*Propositional rules*)
paulson@7093
    82
paulson@7093
    83
  basic "$H, P, $G |- $E, P, $F"
paulson@7093
    84
paulson@7093
    85
  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
paulson@7093
    86
  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
paulson@7093
    87
paulson@7093
    88
  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
paulson@7093
    89
  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
paulson@7093
    90
paulson@7093
    91
  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
paulson@7093
    92
  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
paulson@7093
    93
paulson@7093
    94
  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
paulson@7093
    95
  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
paulson@7093
    96
paulson@7093
    97
  FalseL "$H, False, $G |- $E"
paulson@7093
    98
paulson@7093
    99
  True_def "True == False-->False"
paulson@7093
   100
  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
paulson@7093
   101
paulson@7093
   102
  (*Quantifiers*)
paulson@7093
   103
paulson@7093
   104
  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
paulson@7093
   105
  allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
paulson@7093
   106
paulson@7093
   107
  exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
paulson@7093
   108
  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
paulson@7093
   109
paulson@7093
   110
  (*Equality*)
paulson@7093
   111
paulson@7093
   112
  refl  "$H |- $E, a=a, $F"
paulson@7093
   113
  subst "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
paulson@7093
   114
paulson@7093
   115
  (* Reflection *)
paulson@7093
   116
paulson@7093
   117
  eq_reflection  "|- x=y ==> (x==y)"
paulson@7093
   118
  iff_reflection "|- P<->Q ==> (P==Q)"
paulson@7093
   119
paulson@7093
   120
  (*Descriptions*)
paulson@7093
   121
paulson@7093
   122
  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
paulson@7093
   123
          $H |- $E, P(THE x. P(x)), $F"
paulson@7093
   124
paulson@7093
   125
constdefs
paulson@7093
   126
  If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
paulson@7093
   127
   "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
paulson@7093
   128
paulson@7093
   129
paulson@7093
   130
setup
paulson@7093
   131
  Simplifier.setup
paulson@7093
   132
paulson@7093
   133
setup
paulson@7093
   134
  prover_setup
paulson@7093
   135
paulson@7093
   136
end
paulson@7093
   137
paulson@7118
   138
ML
paulson@7118
   139
paulson@7093
   140
paulson@7166
   141
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
paulson@7093
   142
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
paulson@7118
   143