src/Sequents/LK0.thy
author paulson
Wed Jul 28 13:45:54 1999 +0200 (1999-07-28)
changeset 7118 ee384c7b7416
parent 7093 b2ee0e5d1a7f
child 7166 a4a870ec2e67
permissions -rw-r--r--
adding missing declarations for the <<...>> notation
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
  (*Constant to allow definitions of SEQUENCES of formulas*)
paulson@7093
    28
  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
paulson@7093
    29
paulson@7093
    30
  True,False   :: o
paulson@7093
    31
  "="          :: ['a,'a] => o       (infixl 50)
paulson@7093
    32
  Not          :: o => o             ("~ _" [40] 40)
paulson@7093
    33
  "&"          :: [o,o] => o         (infixr 35)
paulson@7093
    34
  "|"          :: [o,o] => o         (infixr 30)
paulson@7093
    35
  "-->","<->"  :: [o,o] => o         (infixr 25)
paulson@7093
    36
  The          :: ('a => o) => 'a    (binder "THE " 10)
paulson@7093
    37
  All          :: ('a => o) => o     (binder "ALL " 10)
paulson@7093
    38
  Ex           :: ('a => o) => o     (binder "EX " 10)
paulson@7093
    39
paulson@7093
    40
syntax
paulson@7093
    41
  "~="          :: ['a, 'a] => o                (infixl 50)
paulson@7093
    42
paulson@7093
    43
translations
paulson@7093
    44
  "x ~= y"      == "~ (x = y)"
paulson@7093
    45
paulson@7093
    46
syntax (symbols)
paulson@7093
    47
  Not           :: o => o               ("\\<not> _" [40] 40)
paulson@7093
    48
  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
paulson@7093
    49
  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
paulson@7093
    50
  "op -->"      :: [o, o] => o          (infixr "\\<midarrow>\\<rightarrow>" 25)
paulson@7093
    51
  "op <->"      :: [o, o] => o          (infixr "\\<leftarrow>\\<rightarrow>" 25)
paulson@7093
    52
  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
paulson@7093
    53
  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
paulson@7093
    54
  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
paulson@7093
    55
  "op ~="       :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
paulson@7093
    56
paulson@7093
    57
syntax (xsymbols)
paulson@7093
    58
  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
paulson@7093
    59
  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 25)
paulson@7093
    60
paulson@7093
    61
syntax (HTML output)
paulson@7093
    62
  Not           :: o => o               ("\\<not> _" [40] 40)
paulson@7093
    63
paulson@7093
    64
paulson@7093
    65
local
paulson@7093
    66
  
paulson@7093
    67
rules
paulson@7093
    68
paulson@7093
    69
  (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
paulson@7093
    70
paulson@7093
    71
  contRS "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
paulson@7093
    72
  contLS "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
paulson@7093
    73
paulson@7093
    74
  thinRS "$H |- $E, $F ==> $H |- $E, $S, $F"
paulson@7093
    75
  thinLS "$H, $G |- $E ==> $H, $S, $G |- $E"
paulson@7093
    76
paulson@7093
    77
  exchRS "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
paulson@7093
    78
  exchLS "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
paulson@7093
    79
paulson@7093
    80
  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
paulson@7093
    81
paulson@7093
    82
  (*Propositional rules*)
paulson@7093
    83
paulson@7093
    84
  basic "$H, P, $G |- $E, P, $F"
paulson@7093
    85
paulson@7093
    86
  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
paulson@7093
    87
  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
paulson@7093
    88
paulson@7093
    89
  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
paulson@7093
    90
  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
paulson@7093
    91
paulson@7093
    92
  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
paulson@7093
    93
  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
paulson@7093
    94
paulson@7093
    95
  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
paulson@7093
    96
  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
paulson@7093
    97
paulson@7093
    98
  FalseL "$H, False, $G |- $E"
paulson@7093
    99
paulson@7093
   100
  True_def "True == False-->False"
paulson@7093
   101
  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
paulson@7093
   102
paulson@7093
   103
  (*Quantifiers*)
paulson@7093
   104
paulson@7093
   105
  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
paulson@7093
   106
  allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
paulson@7093
   107
paulson@7093
   108
  exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
paulson@7093
   109
  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
paulson@7093
   110
paulson@7093
   111
  (*Equality*)
paulson@7093
   112
paulson@7093
   113
  refl  "$H |- $E, a=a, $F"
paulson@7093
   114
  subst "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
paulson@7093
   115
paulson@7093
   116
  (* Reflection *)
paulson@7093
   117
paulson@7093
   118
  eq_reflection  "|- x=y ==> (x==y)"
paulson@7093
   119
  iff_reflection "|- P<->Q ==> (P==Q)"
paulson@7093
   120
paulson@7093
   121
  (*Descriptions*)
paulson@7093
   122
paulson@7093
   123
  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
paulson@7093
   124
          $H |- $E, P(THE x. P(x)), $F"
paulson@7093
   125
paulson@7093
   126
constdefs
paulson@7093
   127
  If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
paulson@7093
   128
   "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
paulson@7093
   129
paulson@7093
   130
paulson@7093
   131
setup
paulson@7093
   132
  Simplifier.setup
paulson@7093
   133
paulson@7093
   134
setup
paulson@7093
   135
  prover_setup
paulson@7093
   136
paulson@7093
   137
end
paulson@7093
   138
paulson@7118
   139
ML
paulson@7118
   140
paulson@7118
   141
fun side_tr [s1] = Sequents.seq_tr s1;
paulson@7093
   142
paulson@7118
   143
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop"),
paulson@7118
   144
			 ("@Side", side_tr)];
paulson@7093
   145
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
paulson@7118
   146