author  blanchet 
Wed, 02 Jun 2010 15:18:48 +0200  
changeset 37321  9d7cfae95b30 
parent 35256  b73ae1a8fe7e 
child 39557  fe5722fce758 
permissions  rwrr 
22809  1 
(* Title: Cube/Cube.thy 
2 
Author: Tobias Nipkow 

3 
*) 

3773  4 

17252  5 
header {* Barendregt's LambdaCube *} 
6 

7 
theory Cube 

8 
imports Pure 

9 
begin 

10 

26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
24783
diff
changeset

11 
setup PureThy.old_appl_syntax_setup 
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
24783
diff
changeset

12 

17252  13 
typedecl "term" 
14 
typedecl "context" 

15 
typedecl typing 

16 

17 
nonterminals 

24783  18 
context' typing' 
17252  19 

20 
consts 

35256  21 
Abs :: "[term, term => term] => term" 
22 
Prod :: "[term, term => term] => term" 

23 
Trueprop :: "[context, typing] => prop" 

24 
MT_context :: "context" 

25 
Context :: "[typing, context] => context" 

26 
star :: "term" ("*") 

27 
box :: "term" ("[]") 

28 
app :: "[term, term] => term" (infixl "^" 20) 

29 
Has_type :: "[term, term] => typing" 

17252  30 

31 
syntax 

35256  32 
"\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/  _)") 
33 
"_Trueprop1" :: "typing' => prop" ("(_)") 

34 
"" :: "id => context'" ("_") 

35 
"" :: "var => context'" ("_") 

36 
"\<^const>Cube.MT_context" :: "context'" ("") 

37 
"\<^const>Cube.Context" :: "[typing', context'] => context'" ("_ _") 

38 
"\<^const>Cube.Has_type" :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5) 

39 
"_Lam" :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) 

40 
"_Pi" :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) 

41 
"_arrow" :: "[term, term] => term" (infixr ">" 10) 

17252  42 

43 
translations 

17260  44 
("prop") "x:X" == ("prop") " x:X" 
35256  45 
"Lam x:A. B" == "CONST Abs(A, %x. B)" 
46 
"Pi x:A. B" => "CONST Prod(A, %x. B)" 

47 
"A > B" => "CONST Prod(A, %_. B)" 

17252  48 

49 
syntax (xsymbols) 

35256  50 
"\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)") 
51 
"\<^const>Cube.box" :: "term" ("\<box>") 

52 
"_Lam" :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10) 

53 
"_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) 

54 
"_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10) 

17252  55 

35113  56 
print_translation {* 
35256  57 
[(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] 
35113  58 
*} 
17252  59 

60 
axioms 

61 
s_b: "*: []" 

62 

63 
strip_s: "[ A:*; a:A ==> G  x:X ] ==> a:A G  x:X" 

64 
strip_b: "[ A:[]; a:A ==> G  x:X ] ==> a:A G  x:X" 

65 

66 
app: "[ F:Prod(A, B); C:A ] ==> F^C: B(C)" 

0  67 

17252  68 
pi_ss: "[ A:*; !!x. x:A ==> B(x):* ] ==> Prod(A, B):*" 
69 

70 
lam_ss: "[ A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* ] 

71 
==> Abs(A, f) : Prod(A, B)" 

72 

73 
beta: "Abs(A, f)^a == f(a)" 

74 

75 
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss 

76 
lemmas rules = simple 

77 

78 
lemma imp_elim: 

79 
assumes "f:A>B" and "a:A" and "f^a:B ==> PROP P" 

80 
shows "PROP P" by (rule app prems)+ 

81 

82 
lemma pi_elim: 

83 
assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P" 

84 
shows "PROP P" by (rule app prems)+ 

85 

86 

87 
locale L2 = 

88 
assumes pi_bs: "[ A:[]; !!x. x:A ==> B(x):* ] ==> Prod(A,B):*" 

89 
and lam_bs: "[ A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* ] 

90 
==> Abs(A,f) : Prod(A,B)" 

91 

92 
lemmas (in L2) rules = simple lam_bs pi_bs 

93 

17260  94 

17252  95 
locale Lomega = 
96 
assumes 

97 
pi_bb: "[ A:[]; !!x. x:A ==> B(x):[] ] ==> Prod(A,B):[]" 

98 
and lam_bb: "[ A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] ] 

99 
==> Abs(A,f) : Prod(A,B)" 

100 

101 
lemmas (in Lomega) rules = simple lam_bb pi_bb 

102 

103 

104 
locale LP = 

105 
assumes pi_sb: "[ A:*; !!x. x:A ==> B(x):[] ] ==> Prod(A,B):[]" 

106 
and lam_sb: "[ A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] ] 

107 
==> Abs(A,f) : Prod(A,B)" 

108 

109 
lemmas (in LP) rules = simple lam_sb pi_sb 

110 

17260  111 

17252  112 
locale LP2 = LP + L2 
113 

114 
lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb 

115 

17260  116 

17252  117 
locale Lomega2 = L2 + Lomega 
118 

119 
lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb 

120 

17260  121 

17252  122 
locale LPomega = LP + Lomega 
123 

124 
lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb 

125 

17260  126 

17252  127 
locale CC = L2 + LP + Lomega 
128 

129 
lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb 

130 

131 
end 