src/Sequents/LK0.thy
author haftmann
Wed, 21 Oct 2009 10:15:31 +0200
changeset 33040 cffdb7b28498
parent 30549 d2d7874648bd
child 35113 1a0c129bb2e0
permissions -rw-r--r--
removed old-style \ and \\ infixes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
     1
(*  Title:      LK/LK0.thy
7093
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
There may be printing problems if a seqent is in expanded normal form
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
     7
        (eta-expanded, beta-contracted)
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     8
*)
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
     9
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    10
header {* Classical First-Order Sequent Calculus *}
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    11
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    12
theory LK0
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    13
imports Sequents
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    14
begin
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    15
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    16
global
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    17
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    18
classes "term"
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    19
defaultsort "term"
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    20
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    21
consts
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    22
21524
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 21428
diff changeset
    23
  Trueprop       :: "two_seqi"
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    24
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    25
  True         :: o
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    26
  False        :: o
22894
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    27
  equal        :: "['a,'a] => o"     (infixl "=" 50)
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    28
  Not          :: "o => o"           ("~ _" [40] 40)
22894
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    29
  conj         :: "[o,o] => o"       (infixr "&" 35)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    30
  disj         :: "[o,o] => o"       (infixr "|" 30)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    31
  imp          :: "[o,o] => o"       (infixr "-->" 25)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    32
  iff          :: "[o,o] => o"       (infixr "<->" 25)
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    33
  The          :: "('a => o) => 'a"  (binder "THE " 10)
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    34
  All          :: "('a => o) => o"   (binder "ALL " 10)
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16019
diff changeset
    35
  Ex           :: "('a => o) => o"   (binder "EX " 10)
7093
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    36
b2ee0e5d1a7f renamed theory LK to LK0
paulson
parents:
diff changeset
    37
syntax