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 = {*


18 
Method.thms_args (fn thms => Method.METHOD (fn facts =>

19943

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

17453

20 
*} ""


21 


22 
method_setup depth_solve1 = {*


23 
Method.thms_args (fn thms => Method.METHOD (fn facts =>


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


25 
*} ""


26 


27 
method_setup strip_asms = {*


28 
let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in


29 
Method.thms_args (fn thms => Method.METHOD (fn facts =>


30 
REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))


31 
end


32 
*} ""


33 


34 


35 
subsection {* Simple types *}


36 


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


38 
by (depth_solve rules)


39 


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


41 
by (depth_solve rules)


42 


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


44 
by (depth_solve rules)


45 


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


47 
by (depth_solve rules)


48 


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


50 
by (depth_solve rules)


51 


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


53 
by (depth_solve rules)


54 


55 


56 
subsection {* Secondorder types *}


57 


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


59 
by (depth_solve rules)


60 


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


62 
by (depth_solve rules)


63 


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


65 
by (depth_solve rules)


66 


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


68 
by (depth_solve rules)


69 


70 


71 
subsection {* Weakly higherorder propositional logic *}


72 


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


74 
by (depth_solve rules)


75 


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


77 
by (depth_solve rules)


78 


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


80 
by (depth_solve rules)


81 


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


83 
by (depth_solve rules)


84 


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


86 
by (depth_solve rules)


87 


88 


89 
subsection {* LP *}


90 


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


92 
by (depth_solve rules)


93 


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


95 
by (depth_solve rules)


96 


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


98 
by (depth_solve rules)


99 


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


101 
by (depth_solve rules)


102 


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


104 
by (depth_solve rules)


105 


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


107 
by (depth_solve rules)


108 


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


110 
by (depth_solve rules)


111 


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


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


114 
by (depth_solve rules)


115 


116 


117 
subsection {* Omegaorder types *}


118 


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


120 
by (depth_solve rules)


121 


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


123 
by (depth_solve rules)


124 


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


126 
by (depth_solve rules)


127 


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


129 
apply (strip_asms 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 (depth_solve1 rules)


136 
prefer 2


137 
apply (depth_solve1 rules)


138 
apply (rule lam_ss)


139 
apply assumption


140 
prefer 2


141 
apply (depth_solve1 rules)


142 
apply (erule pi_elim)


143 
apply assumption


144 
apply (erule pi_elim)


145 
apply assumption


146 
apply assumption


147 
done


148 


149 


150 
subsection {* Secondorder Predicate Logic *}


151 


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


153 
by (depth_solve rules)


154 


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


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


157 
by (depth_solve rules)


158 


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


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


161 
 {* Antisymmetry implies irreflexivity: *}


162 
apply (strip_asms rules)


163 
apply (rule lam_ss)


164 
apply (depth_solve1 rules)


165 
prefer 2


166 
apply (depth_solve1 rules)


167 
apply (rule lam_ss)


168 
apply assumption


169 
prefer 2


170 
apply (depth_solve1 rules)


171 
apply (rule lam_ss)


172 
apply (depth_solve1 rules)


173 
prefer 2


174 
apply (depth_solve1 rules)


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


176 
done


177 


178 


179 
subsection {* LPomega *}


180 


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


182 
by (depth_solve rules)


183 


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


185 
by (depth_solve rules)


186 


187 


188 
subsection {* Constructions *}


189 


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


191 
by (depth_solve rules)


192 


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


194 
by (depth_solve rules)


195 


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


197 
apply (strip_asms rules)


198 
apply (rule lam_ss)


199 
apply (depth_solve1 rules)


200 
prefer 2


201 
apply (depth_solve1 rules)


202 
apply (erule pi_elim, assumption, assumption)


203 
done


204 


205 


206 
subsection {* Some random examples *}


207 


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


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 


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


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


214 
by (depth_solve rules)


215 


216 
lemma (in LP2)


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


218 
 {* Symmetry of Leibnitz equality *}


219 
apply (strip_asms rules)


220 
apply (rule lam_ss)


221 
apply (depth_solve1 rules)


222 
prefer 2


223 
apply (depth_solve1 rules)


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


225 
apply (depth_solve1 rules)


226 
apply (unfold beta)


227 
apply (erule imp_elim)


228 
apply (rule lam_bs)


229 
apply (depth_solve1 rules)


230 
prefer 2


231 
apply (depth_solve1 rules)


232 
apply (rule lam_ss)


233 
apply (depth_solve1 rules)


234 
prefer 2


235 
apply (depth_solve1 rules)


236 
apply assumption


237 
apply assumption


238 
done


239 


240 
end
