author  lcp 
Fri, 21 Oct 1994 09:47:02 +0100  
changeset 649  237fce674bfb 
parent 283  76caebd18756 
child 1474  3f7d67927fe2 
permissions  rwrr 
0  1 
(* Title: LCF/lcf.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1992 University of Cambridge 

5 

6 
Natural Deduction Rules for LCF 

7 
*) 

8 

9 
LCF = FOL + 

10 

11 
classes cpo < term 

12 

13 
default cpo 

14 

283  15 
types 
16 
tr 

17 
void 

18 
('a,'b) "*" (infixl 6) 

19 
('a,'b) "+" (infixl 5) 

0  20 

283  21 
arities 
22 
fun, "*", "+" :: (cpo,cpo)cpo 

23 
tr,void :: cpo 

0  24 

25 
consts 

26 
UU :: "'a" 

27 
TT,FF :: "tr" 

28 
FIX :: "('a => 'a) => 'a" 

29 
FST :: "'a*'b => 'a" 

30 
SND :: "'a*'b => 'b" 

31 
INL :: "'a => 'a+'b" 

32 
INR :: "'b => 'a+'b" 

33 
WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c" 

34 
adm :: "('a => o) => o" 

649
237fce674bfb
LCF/LCF.thy: the constant VOID had mixfix syntax "()" !! Added quotes.
lcp
parents:
283
diff
changeset

35 
VOID :: "void" ("'(')") 
0  36 
PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) 
37 
COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ / _))" [60,60,60] 60) 

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

39 
rules 

40 
(** DOMAIN THEORY **) 

41 

42 
eq_def "x=y == x << y & y << x" 

43 

44 
less_trans "[ x << y; y << z ] ==> x << z" 

45 

46 
less_ext "(ALL x. f(x) << g(x)) ==> f << g" 

47 

48 
mono "[ f << g; x << y ] ==> f(x) << g(y)" 

49 

50 
minimal "UU << x" 

51 

52 
FIX_eq "f(FIX(f)) = FIX(f)" 

53 

54 
(** TR **) 

55 

56 
tr_cases "p=UU  p=TT  p=FF" 

57 

58 
not_TT_less_FF "~ TT << FF" 

59 
not_FF_less_TT "~ FF << TT" 

60 
not_TT_less_UU "~ TT << UU" 

61 
not_FF_less_UU "~ FF << UU" 

62 

63 
COND_UU "UU => x  y = UU" 

64 
COND_TT "TT => x  y = x" 

65 
COND_FF "FF => x  y = y" 

66 

67 
(** PAIRS **) 

68 

69 
surj_pairing "<FST(z),SND(z)> = z" 

70 

71 
FST "FST(<x,y>) = x" 

72 
SND "SND(<x,y>) = y" 

73 

74 
(*** STRICT SUM ***) 

75 

76 
INL_DEF "~x=UU ==> ~INL(x)=UU" 

77 
INR_DEF "~x=UU ==> ~INR(x)=UU" 

78 

79 
INL_STRICT "INL(UU) = UU" 

80 
INR_STRICT "INR(UU) = UU" 

81 

82 
WHEN_UU "WHEN(f,g,UU) = UU" 

83 
WHEN_INL "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" 

84 
WHEN_INR "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" 

85 

86 
SUM_EXHAUSTION 

87 
"z = UU  (EX x. ~x=UU & z = INL(x))  (EX y. ~y=UU & z = INR(y))" 

88 

89 
(** VOID **) 

90 

91 
void_cases "(x::void) = UU" 

92 

93 
(** INDUCTION **) 

94 

95 
induct "[ adm(P); P(UU); ALL x. P(x) > P(f(x)) ] ==> P(FIX(f))" 

96 

97 
(** Admissibility / Chain Completeness **) 

98 
(* All rules can be found on pages 199200 of Larry's LCF book. 

99 
Note that "easiness" of types is not taken into account 

100 
because it cannot be expressed schematically; flatness could be. *) 

101 

102 
adm_less "adm(%x.t(x) << u(x))" 

103 
adm_not_less "adm(%x.~ t(x) << u)" 

104 
adm_not_free "adm(%x.A)" 

105 
adm_subst "adm(P) ==> adm(%x.P(t(x)))" 

106 
adm_conj "[ adm(P); adm(Q) ] ==> adm(%x.P(x)&Q(x))" 

107 
adm_disj "[ adm(P); adm(Q) ] ==> adm(%x.P(x)Q(x))" 

108 
adm_imp "[ adm(%x.~P(x)); adm(Q) ] ==> adm(%x.P(x)>Q(x))" 

109 
adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))" 

110 
end 