author  wenzelm 
Tue, 08 Jan 2002 00:03:42 +0100  
changeset 12662  a9bbba3473f3 
parent 12116  4027b15377a5 
child 14565  c6dc17aab88a 
permissions  rwrr 
7093  1 
(* Title: LK/LK0 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Classical FirstOrder Sequent Calculus 

7 

8 
There may be printing problems if a seqent is in expanded normal form 

9 
(etaexpanded, betacontracted) 

10 
*) 

11 

12 
LK0 = Sequents + 

13 

14 
global 

15 

16 
classes 

17 
term < logic 

18 

19 
default 

20 
term 

21 

22 
consts 

23 

24 
Trueprop :: "two_seqi" 

25 
"@Trueprop" :: "two_seqe" ("((_)/  (_))" [6,6] 5) 

26 

27 
True,False :: o 

28 
"=" :: ['a,'a] => o (infixl 50) 

29 
Not :: o => o ("~ _" [40] 40) 

30 
"&" :: [o,o] => o (infixr 35) 

31 
"" :: [o,o] => o (infixr 30) 

32 
">","<>" :: [o,o] => o (infixr 25) 

33 
The :: ('a => o) => 'a (binder "THE " 10) 

34 
All :: ('a => o) => o (binder "ALL " 10) 

35 
Ex :: ('a => o) => o (binder "EX " 10) 

36 

37 
syntax 

12662  38 
"_not_equal" :: ['a, 'a] => o (infixl "~=" 50) 
7093  39 

40 
translations 

41 
"x ~= y" == "~ (x = y)" 

42 

12116  43 
syntax (xsymbols) 
7093  44 
Not :: o => o ("\\<not> _" [40] 40) 
45 
"op &" :: [o, o] => o (infixr "\\<and>" 35) 

46 
"op " :: [o, o] => o (infixr "\\<or>" 30) 

12116  47 
"op >" :: [o, o] => o (infixr "\\<longrightarrow>" 25) 
48 
"op <>" :: [o, o] => o (infixr "\\<longleftrightarrow>" 25) 

7093  49 
"ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10) 
50 
"EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10) 

51 
"EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) 

12662  52 
"_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50) 
7093  53 

54 
syntax (HTML output) 

55 
Not :: o => o ("\\<not> _" [40] 40) 

56 

57 

58 
local 

59 

60 
rules 

61 

62 
(*Structural rules: contraction, thinning, exchange [Soren Heilmann] *) 

63 

64 
contRS "$H  $E, $S, $S, $F ==> $H  $E, $S, $F" 

65 
contLS "$H, $S, $S, $G  $E ==> $H, $S, $G  $E" 

66 

67 
thinRS "$H  $E, $F ==> $H  $E, $S, $F" 

68 
thinLS "$H, $G  $E ==> $H, $S, $G  $E" 

69 

70 
exchRS "$H  $E, $R, $S, $F ==> $H  $E, $S, $R, $F" 

71 
exchLS "$H, $R, $S, $G  $E ==> $H, $S, $R, $G  $E" 

72 

73 
cut "[ $H  $E, P; $H, P  $E ] ==> $H  $E" 

74 

75 
(*Propositional rules*) 

76 

77 
basic "$H, P, $G  $E, P, $F" 

78 

79 
conjR "[ $H $E, P, $F; $H $E, Q, $F ] ==> $H $E, P&Q, $F" 

80 
conjL "$H, P, Q, $G  $E ==> $H, P & Q, $G  $E" 

81 

82 
disjR "$H  $E, P, Q, $F ==> $H  $E, PQ, $F" 

83 
disjL "[ $H, P, $G  $E; $H, Q, $G  $E ] ==> $H, PQ, $G  $E" 

84 

85 
impR "$H, P  $E, Q, $F ==> $H  $E, P>Q, $F" 

86 
impL "[ $H,$G  $E,P; $H, Q, $G  $E ] ==> $H, P>Q, $G  $E" 

87 

88 
notR "$H, P  $E, $F ==> $H  $E, ~P, $F" 

89 
notL "$H, $G  $E, P ==> $H, ~P, $G  $E" 

90 

91 
FalseL "$H, False, $G  $E" 

92 

93 
True_def "True == False>False" 

94 
iff_def "P<>Q == (P>Q) & (Q>P)" 

95 

96 
(*Quantifiers*) 

97 

98 
allR "(!!x.$H  $E, P(x), $F) ==> $H  $E, ALL x. P(x), $F" 

99 
allL "$H, P(x), $G, ALL x. P(x)  $E ==> $H, ALL x. P(x), $G  $E" 

100 

101 
exR "$H  $E, P(x), $F, EX x. P(x) ==> $H  $E, EX x. P(x), $F" 

102 
exL "(!!x.$H, P(x), $G  $E) ==> $H, EX x. P(x), $G  $E" 

103 

104 
(*Equality*) 

105 

106 
refl "$H  $E, a=a, $F" 

107 
subst "$H(a), $G(a)  $E(a) ==> $H(b), a=b, $G(b)  $E(b)" 

108 

109 
(* Reflection *) 

110 

111 
eq_reflection " x=y ==> (x==y)" 

112 
iff_reflection " P<>Q ==> (P==Q)" 

113 

114 
(*Descriptions*) 

115 

116 
The "[ $H  $E, P(a), $F; !!x.$H, P(x)  $E, x=a, $F ] ==> 

117 
$H  $E, P(THE x. P(x)), $F" 

118 

119 
constdefs 

120 
If :: [o, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10) 

121 
"If(P,x,y) == THE z::'a. (P > z=x) & (~P > z=y)" 

122 

123 

124 
setup 

125 
Simplifier.setup 

126 

127 
setup 

128 
prover_setup 

129 

130 
end 

131 

7118
ee384c7b7416
adding missing declarations for the <<...>> notation
paulson
parents:
7093
diff
changeset

132 
ML 
ee384c7b7416
adding missing declarations for the <<...>> notation
paulson
parents:
7093
diff
changeset

133 

7093  134 

7166
a4a870ec2e67
Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents:
7118
diff
changeset

135 
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; 
7093  136 
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")]; 
7118
ee384c7b7416
adding missing declarations for the <<...>> notation
paulson
parents:
7093
diff
changeset

137 