17453

1 


2 
(* $Id$ *)


3 


4 
header {* Lambda Cube Examples *}


5 


6 
theory Example


7 
imports Cube


8 
begin


9 


10 
text {*


11 
Examples taken from:


12 


13 
H. Barendregt. Introduction to Generalised Type Systems.


14 
J. Functional Programming.


15 
*}


16 


17 
method_setup depth_solve = {*

30549

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


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

17453

20 
*} ""


21 


22 
method_setup depth_solve1 = {*

30549

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


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

17453

25 
*} ""


26 


27 
method_setup strip_asms = {*

30549

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


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


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

17453

31 
*} ""


32 


33 


34 
subsection {* Simple types *}


35 


36 
lemma "A:*  A>A : ?T"


37 
by (depth_solve rules)


38 


39 
lemma "A:*  Lam a:A. a : ?T"


40 
by (depth_solve rules)


41 


42 
lemma "A:* B:* b:B  Lam x:A. b : ?T"


43 
by (depth_solve rules)


44 


45 
lemma "A:* b:A  (Lam a:A. a)^b: ?T"


46 
by (depth_solve rules)


47 


48 
lemma "A:* B:* c:A b:B  (Lam x:A. b)^ c: ?T"


49 
by (depth_solve rules)


50 


51 
lemma "A:* B:*  Lam a:A. Lam b:B. a : ?T"


52 
by (depth_solve rules)


53 


54 


55 
subsection {* Secondorder types *}


56 


57 
lemma (in L2) " Lam A:*. Lam a:A. a : ?T"


58 
by (depth_solve rules)


59 


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


61 
by (depth_solve rules)


62 


63 
lemma (in L2) "A:* b:A  (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"


64 
by (depth_solve rules)


65 


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


67 
by (depth_solve rules)


68 


69 


70 
subsection {* Weakly higherorder propositional logic *}


71 


72 
lemma (in Lomega) " Lam A:*.A>A : ?T"


73 
by (depth_solve rules)


74 


75 
lemma (in Lomega) "B:*  (Lam A:*.A>A) ^ B : ?T"


76 
by (depth_solve rules)


77 


78 
lemma (in Lomega) "B:* b:B  (Lam y:B. b): ?T"


79 
by (depth_solve rules)


80 


81 
lemma (in Lomega) "A:* F:*>*  F^(F^A): ?T"


82 
by (depth_solve rules)


83 


84 
lemma (in Lomega) "A:*  Lam F:*>*.F^(F^A): ?T"


85 
by (depth_solve rules)


86 


87 


88 
subsection {* LP *}


89 


90 
lemma (in LP) "A:*  A > * : ?T"


91 
by (depth_solve rules)


92 


93 
lemma (in LP) "A:* P:A>* a:A  P^a: ?T"


94 
by (depth_solve rules)


95 


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


97 
by (depth_solve rules)


98 


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


100 
by (depth_solve rules)


101 


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


103 
by (depth_solve rules)


104 


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


106 
by (depth_solve rules)


107 


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


109 
by (depth_solve rules)


110 


111 
lemma (in LP) "A:* P:A>* Q:* a0:A 


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


113 
by (depth_solve rules)


114 


115 


116 
subsection {* Omegaorder types *}


117 


118 
lemma (in L2) "A:* B:*  Pi C:*.(A>B>C)>C : ?T"


119 
by (depth_solve rules)


120 


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


122 
by (depth_solve rules)


123 


124 
lemma (in Lomega2) " Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"


125 
by (depth_solve rules)


126 


127 
lemma (in Lomega2) "A:* B:*  ?p : (A>B) > ((B>Pi P:*.P)>(A>Pi P:*.P))"


128 
apply (strip_asms rules)


129 
apply (rule lam_ss)


130 
apply (depth_solve1 rules)


131 
prefer 2


132 
apply (depth_solve1 rules)


133 
apply (rule lam_ss)


134 
apply (depth_solve1 rules)


135 
prefer 2


136 
apply (depth_solve1 rules)


137 
apply (rule lam_ss)


138 
apply assumption


139 
prefer 2


140 
apply (depth_solve1 rules)


141 
apply (erule pi_elim)


142 
apply assumption


143 
apply (erule pi_elim)


144 
apply assumption


145 
apply assumption


146 
done


147 


148 


149 
subsection {* Secondorder Predicate Logic *}


150 


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


152 
by (depth_solve rules)


153 


154 
lemma (in LP2) "A:* P:A>A>* 


155 
(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"


156 
by (depth_solve rules)


157 


158 
lemma (in LP2) "A:* P:A>A>* 


159 
?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"


160 
 {* Antisymmetry implies irreflexivity: *}


161 
apply (strip_asms rules)


162 
apply (rule lam_ss)


163 
apply (depth_solve1 rules)


164 
prefer 2


165 
apply (depth_solve1 rules)


166 
apply (rule lam_ss)


167 
apply assumption


168 
prefer 2


169 
apply (depth_solve1 rules)


170 
apply (rule lam_ss)


171 
apply (depth_solve1 rules)


172 
prefer 2


173 
apply (depth_solve1 rules)


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


175 
done


176 


177 


178 
subsection {* LPomega *}


179 


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


181 
by (depth_solve rules)


182 


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


184 
by (depth_solve rules)


185 


186 


187 
subsection {* Constructions *}


188 


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


190 
by (depth_solve rules)


191 


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


193 
by (depth_solve rules)


194 


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


196 
apply (strip_asms rules)


197 
apply (rule lam_ss)


198 
apply (depth_solve1 rules)


199 
prefer 2


200 
apply (depth_solve1 rules)


201 
apply (erule pi_elim, assumption, assumption)


202 
done


203 


204 


205 
subsection {* Some random examples *}


206 


207 
lemma (in LP2) "A:* c:A f:A>A 


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


209 
by (depth_solve rules)


210 


211 
lemma (in CC) "Lam A:*.Lam c:A. Lam f:A>A.


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


213 
by (depth_solve rules)


214 


215 
lemma (in LP2)


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


217 
 {* Symmetry of Leibnitz equality *}


218 
apply (strip_asms rules)


219 
apply (rule lam_ss)


220 
apply (depth_solve1 rules)


221 
prefer 2


222 
apply (depth_solve1 rules)


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


224 
apply (depth_solve1 rules)


225 
apply (unfold beta)


226 
apply (erule imp_elim)


227 
apply (rule lam_bs)


228 
apply (depth_solve1 rules)


229 
prefer 2


230 
apply (depth_solve1 rules)


231 
apply (rule lam_ss)


232 
apply (depth_solve1 rules)


233 
prefer 2


234 
apply (depth_solve1 rules)


235 
apply assumption


236 
apply assumption


237 
done


238 


239 
end
