17481
|
1 |
(* Title: LK/LK0.thy
|
7093
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
There may be printing problems if a seqent is in expanded normal form
|
17481
|
7 |
(eta-expanded, beta-contracted)
|
7093
|
8 |
*)
|
|
9 |
|
17481
|
10 |
header {* Classical First-Order Sequent Calculus *}
|
|
11 |
|
|
12 |
theory LK0
|
|
13 |
imports Sequents
|
|
14 |
begin
|
7093
|
15 |
|
|
16 |
global
|
|
17 |
|
17481
|
18 |
classes "term"
|
|
19 |
defaultsort "term"
|
7093
|
20 |
|
|
21 |
consts
|
|
22 |
|
21524
|
23 |
Trueprop :: "two_seqi"
|
7093
|
24 |
|
17481
|
25 |
True :: o
|
|
26 |
False :: o
|
22894
|
27 |
equal :: "['a,'a] => o" (infixl "=" 50)
|
17481
|
28 |
Not :: "o => o" ("~ _" [40] 40)
|
22894
|
29 |
conj :: "[o,o] => o" (infixr "&" 35)
|
|
30 |
disj :: "[o,o] => o" (infixr "|" 30)
|
|
31 |
imp :: "[o,o] => o" (infixr "-->" 25)
|
|
32 |
iff :: "[o,o] => o" (infixr "<->" 25)
|
17481
|
33 |
The :: "('a => o) => 'a" (binder "THE " 10)
|
|
34 |
All :: "('a => o) => o" (binder "ALL " 10)
|
|
35 |
Ex :: "('a => o) => o" (binder "EX " 10)
|
7093
|
36 |
|
|
37 |
syntax
|
|