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