src/Sequents/LK0.thy
author kleing
Sat, 30 Apr 2005 14:18:36 +0200
changeset 15900 d6156cb8dc2e
parent 14854 61bdf2ae4dc5
child 16019 0e1405402d53
permissions -rw-r--r--
fixed typo
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
14854
61bdf2ae4dc5 removed obsolete sort 'logic';
wenzelm
parents: 14765
diff changeset
    16
classes term
61bdf2ae4dc5 removed obsolete sort 'logic';
wenzelm
parents: 14765
diff changeset
    17
default term
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    18
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    19
consts
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    20
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    21
 Trueprop	:: "two_seqi"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    22
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    23
  True,False   :: o
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    24
  "="          :: ['a,'a] => o       (infixl 50)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    25
  Not          :: o => o             ("~ _" [40] 40)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    26
  "&"          :: [o,o] => o         (infixr 35)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    27
  "|"          :: [o,o] => o         (infixr 30)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    28
  "-->","<->"  :: [o,o] => o         (infixr 25)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    29
  The          :: ('a => o) => 'a    (binder "THE " 10)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    30
  All          :: ('a => o) => o     (binder "ALL " 10)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    31
  Ex           :: ('a => o) => o     (binder "EX " 10)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    32
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    33
syntax
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 14565
diff changeset
    34
 "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
12662
a9bbba3473f3 syntax "_not_equal";
wenzelm
parents: 12116
diff changeset
    35
  "_not_equal" :: ['a, 'a] => o                (infixl "~=" 50)
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    36
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    37
translations
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    38
  "x ~= y"      == "~ (x = y)"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    39
12116
4027b15377a5 got rid of obsolete input filtering;
wenzelm
parents: 7166
diff changeset
    40
syntax (xsymbols)
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    41
  Not           :: o => o               ("\\<not> _" [40] 40)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    42
  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    43
  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
12116
4027b15377a5 got rid of obsolete input filtering;
wenzelm
parents: 7166
diff changeset
    44
  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
4027b15377a5 got rid of obsolete input filtering;
wenzelm
parents: 7166
diff changeset
    45
  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 25)
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    46
  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    47
  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    48
  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
12662
a9bbba3473f3 syntax "_not_equal";
wenzelm
parents: 12116
diff changeset
    49
  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    50
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    51
syntax (HTML output)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    52
  Not           :: o => o               ("\\<not> _" [40] 40)
14565
c6dc17aab88a use more symbols in HTML output
kleing
parents: 12662
diff changeset
    53
  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 12662
diff changeset
    54
  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 12662
diff changeset
    55
  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 12662
diff changeset
    56
  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 12662
diff changeset
    57
  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 12662
diff changeset
    58
  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    59
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    60
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    61
local
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    62
  
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    63
rules
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    64
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    65
  (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    66
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    67
  contRS "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    68
  contLS "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    69
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    70
  thinRS "$H |- $E, $F ==> $H |- $E, $S, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    71
  thinLS "$H, $G |- $E ==> $H, $S, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    72
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    73
  exchRS "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    74
  exchLS "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    75
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    76
  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    77
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    78
  (*Propositional rules*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    79
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    80
  basic "$H, P, $G |- $E, P, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    81
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    82
  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    83
  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    84
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    85
  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    86
  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    87
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    88
  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    89
  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    90
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    91
  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    92
  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    93
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    94
  FalseL "$H, False, $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    95
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    96
  True_def "True == False-->False"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    97
  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    98
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    99
  (*Quantifiers*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   100
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   101
  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   102
  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
   103
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   104
  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
   105
  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   106
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   107
  (*Equality*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   108
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   109
  refl  "$H |- $E, a=a, $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   110
  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
   111
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   112
  (* Reflection *)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   113
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   114
  eq_reflection  "|- x=y ==> (x==y)"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   115
  iff_reflection "|- P<->Q ==> (P==Q)"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   116
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   117
  (*Descriptions*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   118
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   119
  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   120
          $H |- $E, P(THE x. P(x)), $F"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   121
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   122
constdefs
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   123
  If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   124
   "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   125
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   126
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   127
setup
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   128
  Simplifier.setup
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   129
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   130
setup
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   131
  prover_setup
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   132
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   133
end
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   134
7118
ee384c7b7416 adding missing declarations for the <<...>> notation
paulson
parents: 7093
diff changeset
   135
ML
ee384c7b7416 adding missing declarations for the <<...>> notation
paulson
parents: 7093
diff changeset
   136
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   137
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7118
diff changeset
   138
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
   139
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
7118
ee384c7b7416 adding missing declarations for the <<...>> notation
paulson
parents: 7093
diff changeset
   140