17453

1 
header {* Lambda Cube Examples *}


2 


3 
theory Example


4 
imports Cube


5 
begin


6 


7 
text {*


8 
Examples taken from:


9 


10 
H. Barendregt. Introduction to Generalised Type Systems.


11 
J. Functional Programming.


12 
*}


13 


14 
method_setup depth_solve = {*

30549

15 
Attrib.thms >> (fn thms => K (METHOD (fn facts =>


16 
(DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))

17453

17 
*} ""


18 


19 
method_setup depth_solve1 = {*

30549

20 
Attrib.thms >> (fn thms => K (METHOD (fn facts =>


21 
(DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))

17453

22 
*} ""


23 


24 
method_setup strip_asms = {*

30549

25 
Attrib.thms >> (fn thms => K (METHOD (fn facts =>


26 
REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN


27 
DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))

17453

28 
*} ""


29 


30 


31 
subsection {* Simple types *}


32 

36319

33 
schematic_lemma "A:*  A>A : ?T"

17453

34 
by (depth_solve rules)


35 

36319

36 
schematic_lemma "A:*  Lam a:A. a : ?T"

17453

37 
by (depth_solve rules)


38 

36319

39 
schematic_lemma "A:* B:* b:B  Lam x:A. b : ?T"

17453

40 
by (depth_solve rules)


41 

36319

42 
schematic_lemma "A:* b:A  (Lam a:A. a)^b: ?T"

17453

43 
by (depth_solve rules)


44 

36319

45 
schematic_lemma "A:* B:* c:A b:B  (Lam x:A. b)^ c: ?T"

17453

46 
by (depth_solve rules)


47 

36319

48 
schematic_lemma "A:* B:*  Lam a:A. Lam b:B. a : ?T"

17453

49 
by (depth_solve rules)


50 


51 


52 
subsection {* Secondorder types *}


53 

36319

54 
schematic_lemma (in L2) " Lam A:*. Lam a:A. a : ?T"

17453

55 
by (depth_solve rules)


56 

36319

57 
schematic_lemma (in L2) "A:*  (Lam B:*.Lam b:B. b)^A : ?T"

17453

58 
by (depth_solve rules)


59 

36319

60 
schematic_lemma (in L2) "A:* b:A  (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"

17453

61 
by (depth_solve rules)


62 

36319

63 
schematic_lemma (in L2) " Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)>B) ^ a: ?T"

17453

64 
by (depth_solve rules)


65 


66 


67 
subsection {* Weakly higherorder propositional logic *}


68 

36319

69 
schematic_lemma (in Lomega) " Lam A:*.A>A : ?T"

17453

70 
by (depth_solve rules)


71 

36319

72 
schematic_lemma (in Lomega) "B:*  (Lam A:*.A>A) ^ B : ?T"

17453

73 
by (depth_solve rules)


74 

36319

75 
schematic_lemma (in Lomega) "B:* b:B  (Lam y:B. b): ?T"

17453

76 
by (depth_solve rules)


77 

36319

78 
schematic_lemma (in Lomega) "A:* F:*>*  F^(F^A): ?T"

17453

79 
by (depth_solve rules)


80 

36319

81 
schematic_lemma (in Lomega) "A:*  Lam F:*>*.F^(F^A): ?T"

17453

82 
by (depth_solve rules)


83 


84 


85 
subsection {* LP *}


86 

36319

87 
schematic_lemma (in LP) "A:*  A > * : ?T"

17453

88 
by (depth_solve rules)


89 

36319

90 
schematic_lemma (in LP) "A:* P:A>* a:A  P^a: ?T"

17453

91 
by (depth_solve rules)


92 

36319

93 
schematic_lemma (in LP) "A:* P:A>A>* a:A  Pi a:A. P^a^a: ?T"

17453

94 
by (depth_solve rules)


95 

36319

96 
schematic_lemma (in LP) "A:* P:A>* Q:A>*  Pi a:A. P^a > Q^a: ?T"

17453

97 
by (depth_solve rules)


98 

36319

99 
schematic_lemma (in LP) "A:* P:A>*  Pi a:A. P^a > P^a: ?T"

17453

100 
by (depth_solve rules)


101 

36319

102 
schematic_lemma (in LP) "A:* P:A>*  Lam a:A. Lam x:P^a. x: ?T"

17453

103 
by (depth_solve rules)


104 

36319

105 
schematic_lemma (in LP) "A:* P:A>* Q:*  (Pi a:A. P^a>Q) > (Pi a:A. P^a) > Q : ?T"

17453

106 
by (depth_solve rules)


107 

36319

108 
schematic_lemma (in LP) "A:* P:A>* Q:* a0:A 

17453

109 
Lam x:Pi a:A. P^a>Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T"


110 
by (depth_solve rules)


111 


112 


113 
subsection {* Omegaorder types *}


114 

36319

115 
schematic_lemma (in L2) "A:* B:*  Pi C:*.(A>B>C)>C : ?T"

17453

116 
by (depth_solve rules)


117 

36319

118 
schematic_lemma (in Lomega2) " Lam A:*.Lam B:*.Pi C:*.(A>B>C)>C : ?T"

17453

119 
by (depth_solve rules)


120 

36319

121 
schematic_lemma (in Lomega2) " Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"

17453

122 
by (depth_solve rules)


123 

36319

124 
schematic_lemma (in Lomega2) "A:* B:*  ?p : (A>B) > ((B>Pi P:*.P)>(A>Pi P:*.P))"

17453

125 
apply (strip_asms rules)


126 
apply (rule lam_ss)


127 
apply (depth_solve1 rules)


128 
prefer 2


129 
apply (depth_solve1 rules)


130 
apply (rule lam_ss)


131 
apply (depth_solve1 rules)


132 
prefer 2


133 
apply (depth_solve1 rules)


134 
apply (rule lam_ss)


135 
apply assumption


136 
prefer 2


137 
apply (depth_solve1 rules)


138 
apply (erule pi_elim)


139 
apply assumption


140 
apply (erule pi_elim)


141 
apply assumption


142 
apply assumption


143 
done


144 


145 


146 
subsection {* Secondorder Predicate Logic *}


147 

36319

148 
schematic_lemma (in LP2) "A:* P:A>*  Lam a:A. P^a>(Pi A:*.A) : ?T"

17453

149 
by (depth_solve rules)


150 

36319

151 
schematic_lemma (in LP2) "A:* P:A>A>* 

17453

152 
(Pi a:A. Pi b:A. P^a^b>P^b^a>Pi P:*.P) > Pi a:A. P^a^a>Pi P:*.P : ?T"


153 
by (depth_solve rules)


154 

36319

155 
schematic_lemma (in LP2) "A:* P:A>A>* 

17453

156 
?p: (Pi a:A. Pi b:A. P^a^b>P^b^a>Pi P:*.P) > Pi a:A. P^a^a>Pi P:*.P"


157 
 {* Antisymmetry implies irreflexivity: *}


158 
apply (strip_asms rules)


159 
apply (rule lam_ss)


160 
apply (depth_solve1 rules)


161 
prefer 2


162 
apply (depth_solve1 rules)


163 
apply (rule lam_ss)


164 
apply assumption


165 
prefer 2


166 
apply (depth_solve1 rules)


167 
apply (rule lam_ss)


168 
apply (depth_solve1 rules)


169 
prefer 2


170 
apply (depth_solve1 rules)


171 
apply (erule pi_elim, assumption, assumption?)+


172 
done


173 


174 


175 
subsection {* LPomega *}


176 

36319

177 
schematic_lemma (in LPomega) "A:*  Lam P:A>A>*.Lam a:A. P^a^a : ?T"

17453

178 
by (depth_solve rules)


179 

36319

180 
schematic_lemma (in LPomega) " Lam A:*.Lam P:A>A>*.Lam a:A. P^a^a : ?T"

17453

181 
by (depth_solve rules)


182 


183 


184 
subsection {* Constructions *}


185 

36319

186 
schematic_lemma (in CC) " Lam A:*.Lam P:A>*.Lam a:A. P^a>Pi P:*.P: ?T"

17453

187 
by (depth_solve rules)


188 

36319

189 
schematic_lemma (in CC) " Lam A:*.Lam P:A>*.Pi a:A. P^a: ?T"

17453

190 
by (depth_solve rules)


191 

36319

192 
schematic_lemma (in CC) "A:* P:A>* a:A  ?p : (Pi a:A. P^a)>P^a"

17453

193 
apply (strip_asms rules)


194 
apply (rule lam_ss)


195 
apply (depth_solve1 rules)


196 
prefer 2


197 
apply (depth_solve1 rules)


198 
apply (erule pi_elim, assumption, assumption)


199 
done


200 


201 


202 
subsection {* Some random examples *}


203 

36319

204 
schematic_lemma (in LP2) "A:* c:A f:A>A 

17453

205 
Lam a:A. Pi P:A>*.P^c > (Pi x:A. P^x>P^(f^x)) > P^a : ?T"


206 
by (depth_solve rules)


207 

36319

208 
schematic_lemma (in CC) "Lam A:*.Lam c:A. Lam f:A>A.

17453

209 
Lam a:A. Pi P:A>*.P^c > (Pi x:A. P^x>P^(f^x)) > P^a : ?T"


210 
by (depth_solve rules)


211 

36319

212 
schematic_lemma (in LP2)

17453

213 
"A:* a:A b:A  ?p: (Pi P:A>*.P^a>P^b) > (Pi P:A>*.P^b>P^a)"


214 
 {* Symmetry of Leibnitz equality *}


215 
apply (strip_asms rules)


216 
apply (rule lam_ss)


217 
apply (depth_solve1 rules)


218 
prefer 2


219 
apply (depth_solve1 rules)


220 
apply (erule_tac a = "Lam x:A. Pi Q:A>*.Q^x>Q^a" in pi_elim)


221 
apply (depth_solve1 rules)


222 
apply (unfold beta)


223 
apply (erule imp_elim)


224 
apply (rule lam_bs)


225 
apply (depth_solve1 rules)


226 
prefer 2


227 
apply (depth_solve1 rules)


228 
apply (rule lam_ss)


229 
apply (depth_solve1 rules)


230 
prefer 2


231 
apply (depth_solve1 rules)


232 
apply assumption


233 
apply assumption


234 
done


235 


236 
end
