0

1 
(* Examples taken from


2 
H. Barendregt. Introduction to Generalised Type Systems.


3 
J. Functional Programming.


4 
*)


5 


6 
Cube_build_completed; (*Cause examples to fail if Cube did*)


7 


8 
proof_timing := true;


9 


10 
fun strip_asms_tac thms i =


11 
REPEAT(resolve_tac[strip_b,strip_s]i THEN DEPTH_SOLVE_1(ares_tac thms i));


12 


13 
val imp_elim = prove_goal thy "[ f:A>B; a:A; f^a:B ==> PROP P ] ==> PROP P"


14 
(fn asms => [REPEAT(resolve_tac (app::asms) 1)]);


15 


16 
val pi_elim = prove_goal thy


17 
"[ F:Prod(A,B); a:A; F^a:B(a) ==> PROP P ] ==> PROP P"


18 
(fn asms => [REPEAT(resolve_tac (app::asms) 1)]);


19 


20 
(* SIMPLE TYPES *)


21 


22 
goal thy "A:*  A>A : ?T";


23 
by (DEPTH_SOLVE (ares_tac simple 1));


24 
uresult();


25 


26 
goal thy "A:*  Lam a:A.a : ?T";


27 
by (DEPTH_SOLVE (ares_tac simple 1));


28 
uresult();


29 


30 
goal thy "A:* B:* b:B  Lam x:A.b : ?T";


31 
by (DEPTH_SOLVE (ares_tac simple 1));


32 
uresult();


33 


34 
goal thy "A:* b:A  (Lam a:A.a)^b: ?T";


35 
by (DEPTH_SOLVE (ares_tac simple 1));


36 
uresult();


37 


38 
goal thy "A:* B:* c:A b:B  (Lam x:A.b)^ c: ?T";


39 
by (DEPTH_SOLVE (ares_tac simple 1));


40 
uresult();


41 


42 
goal thy "A:* B:*  Lam a:A.Lam b:B.a : ?T";


43 
by (DEPTH_SOLVE (ares_tac simple 1));


44 
uresult();


45 


46 
(* SECONDORDER TYPES *)


47 


48 
goal L2_thy " Lam A:*. Lam a:A.a : ?T";


49 
by (DEPTH_SOLVE (ares_tac L2 1));


50 
uresult();


51 


52 
goal L2_thy "A:*  (Lam B:*.Lam b:B.b)^A : ?T";


53 
by (DEPTH_SOLVE (ares_tac L2 1));


54 
uresult();


55 


56 
goal L2_thy "A:* b:A  (Lam B:*.Lam b:B.b) ^ A ^ b: ?T";


57 
by (DEPTH_SOLVE (ares_tac L2 1));


58 
uresult();


59 


60 
goal L2_thy " Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)>B) ^ a: ?T";


61 
by (DEPTH_SOLVE (ares_tac L2 1));


62 
uresult();


63 


64 
(* Weakly higherorder proposiional logic *)


65 


66 
goal Lomega_thy " Lam A:*.A>A : ?T";


67 
by (DEPTH_SOLVE (ares_tac Lomega 1));


68 
uresult();


69 


70 
goal Lomega_thy "B:*  (Lam A:*.A>A) ^ B : ?T";


71 
by (DEPTH_SOLVE (ares_tac Lomega 1));


72 
uresult();


73 


74 
goal Lomega_thy "B:* b:B  (Lam y:B.b): ?T";


75 
by (DEPTH_SOLVE (ares_tac Lomega 1));


76 
uresult();


77 


78 
goal Lomega_thy "A:* F:*>*  F^(F^A): ?T";


79 
by (DEPTH_SOLVE (ares_tac Lomega 1));


80 
uresult();


81 


82 
goal Lomega_thy "A:*  Lam F:*>*.F^(F^A): ?T";


83 
by (DEPTH_SOLVE (ares_tac Lomega 1));


84 
uresult();


85 


86 
(* LF *)


87 


88 
goal LP_thy "A:*  A > * : ?T";


89 
by (DEPTH_SOLVE (ares_tac LP 1));


90 
uresult();


91 


92 
goal LP_thy "A:* P:A>* a:A  P^a: ?T";


93 
by (DEPTH_SOLVE (ares_tac LP 1));


94 
uresult();


95 


96 
goal LP_thy "A:* P:A>A>* a:A  Pi a:A.P^a^a: ?T";


97 
by (DEPTH_SOLVE (ares_tac LP 1));


98 
uresult();


99 


100 
goal LP_thy "A:* P:A>* Q:A>*  Pi a:A.P^a > Q^a: ?T";


101 
by (DEPTH_SOLVE (ares_tac LP 1));


102 
uresult();


103 


104 
goal LP_thy "A:* P:A>*  Pi a:A.P^a > P^a: ?T";


105 
by (DEPTH_SOLVE (ares_tac LP 1));


106 
uresult();


107 


108 
goal LP_thy "A:* P:A>*  Lam a:A.Lam x:P^a.x: ?T";


109 
by (DEPTH_SOLVE (ares_tac LP 1));


110 
uresult();


111 


112 
goal LP_thy "A:* P:A>* Q:*  (Pi a:A.P^a>Q) > (Pi a:A.P^a) > Q : ?T";


113 
by (DEPTH_SOLVE (ares_tac LP 1));


114 
uresult();


115 


116 
goal LP_thy "A:* P:A>* Q:* a0:A  \


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


118 
by (DEPTH_SOLVE (ares_tac LP 1));


119 
uresult();


120 


121 
(* OMEGAORDER TYPES *)


122 


123 
goal L2_thy "A:* B:*  Pi C:*.(A>B>C)>C : ?T";


124 
by (DEPTH_SOLVE (ares_tac L2 1));


125 
uresult();


126 


127 
goal LOmega_thy " Lam A:*.Lam B:*.Pi C:*.(A>B>C)>C : ?T";


128 
by (DEPTH_SOLVE (ares_tac LOmega 1));


129 
uresult();


130 


131 
goal LOmega_thy " Lam A:*.Lam B:*.Lam x:A.Lam y:B.x : ?T";


132 
by (DEPTH_SOLVE (ares_tac LOmega 1));


133 
uresult();


134 


135 
goal LOmega_thy "A:* B:*  ?p : (A>B) > ((B>Pi P:*.P)>(A>Pi P:*.P))";


136 
by (strip_asms_tac LOmega 1);


137 
by (rtac lam_ss 1);


138 
by (DEPTH_SOLVE_1(ares_tac LOmega 1));


139 
by (DEPTH_SOLVE_1(ares_tac LOmega 2));


140 
by (rtac lam_ss 1);


141 
by (DEPTH_SOLVE_1(ares_tac LOmega 1));


142 
by (DEPTH_SOLVE_1(ares_tac LOmega 2));


143 
by (rtac lam_ss 1);


144 
by (assume_tac 1);


145 
by (DEPTH_SOLVE_1(ares_tac LOmega 2));


146 
by (etac pi_elim 1);


147 
by (assume_tac 1);


148 
by (etac pi_elim 1);


149 
by (assume_tac 1);


150 
by (assume_tac 1);


151 
uresult();


152 


153 
(* Secondorder Predicate Logic *)


154 


155 
goal LP2_thy "A:* P:A>*  Lam a:A.P^a>(Pi A:*.A) : ?T";


156 
by (DEPTH_SOLVE (ares_tac LP2 1));


157 
uresult();


158 


159 
goal LP2_thy "A:* P:A>A>*  \


160 
\ (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";


161 
by (DEPTH_SOLVE (ares_tac LP2 1));


162 
uresult();


163 


164 
(* Antisymmetry implies irreflexivity: *)


165 
goal LP2_thy "A:* P:A>A>*  \


166 
\ ?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";


167 
by (strip_asms_tac LP2 1);


168 
by (rtac lam_ss 1);


169 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


170 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


171 
by (rtac lam_ss 1);


172 
by (assume_tac 1);


173 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


174 
by (rtac lam_ss 1);


175 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


176 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


177 
by (REPEAT(EVERY[etac pi_elim 1, assume_tac 1, TRY(assume_tac 1)]));


178 
uresult();


179 


180 
(* LPomega *)


181 


182 
goal LPomega_thy "A:*  Lam P:A>A>*.Lam a:A.P^a^a : ?T";


183 
by (DEPTH_SOLVE (ares_tac LPomega 1));


184 
uresult();


185 


186 
goal LPomega_thy " Lam A:*.Lam P:A>A>*.Lam a:A.P^a^a : ?T";


187 
by (DEPTH_SOLVE (ares_tac LPomega 1));


188 
uresult();


189 


190 
(* CONSTRUCTIONS *)


191 


192 
goal CC_thy " Lam A:*.Lam P:A>*.Lam a:A.P^a>Pi P:*.P: ?T";


193 
by (DEPTH_SOLVE (ares_tac CC 1));


194 
uresult();


195 


196 
goal CC_thy " Lam A:*.Lam P:A>*.Pi a:A.P^a: ?T";


197 
by (DEPTH_SOLVE (ares_tac CC 1));


198 
uresult();


199 


200 
goal CC_thy "A:* P:A>* a:A  ?p : (Pi a:A.P^a)>P^a";


201 
by (strip_asms_tac CC 1);


202 
by (rtac lam_ss 1);


203 
by (DEPTH_SOLVE_1(ares_tac CC 1));


204 
by (DEPTH_SOLVE_1(ares_tac CC 2));


205 
by (EVERY[etac pi_elim 1, assume_tac 1, assume_tac 1]);


206 
uresult();


207 


208 
(* Some random examples *)


209 


210 
goal LP2_thy "A:* c:A f:A>A  \


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


212 
by (DEPTH_SOLVE(ares_tac LP2 1));


213 
uresult();


214 


215 
goal CC_thy "Lam A:*.Lam c:A.Lam f:A>A. \


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


217 
by (DEPTH_SOLVE(ares_tac CC 1));


218 
uresult();


219 


220 
(* Symmetry of Leibnitz equality *)


221 
goal LP2_thy "A:* a:A b:A  ?p: (Pi P:A>*.P^a>P^b) > (Pi P:A>*.P^b>P^a)";


222 
by (strip_asms_tac LP2 1);


223 
by (rtac lam_ss 1);


224 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


225 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


226 
by (eres_inst_tac [("a","Lam x:A.Pi Q:A>*.Q^x>Q^a")] pi_elim 1);


227 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


228 
by (rewtac beta);


229 
by (etac imp_elim 1);


230 
by (rtac lam_bs 1);


231 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


232 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


233 
by (rtac lam_ss 1);


234 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


235 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


236 
by (assume_tac 1);


237 
by (assume_tac 1);


238 
uresult();


239 


240 
maketest"END: file for LambdaCube examples";
