2817

1 
(* Examples taken from


2 
H. Barendregt. Introduction to Generalised Type Systems.


3 
J. Functional Programming.


4 
*)


5 


6 
fun strip_asms_tac thms i =


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


8 


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


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


11 


12 
val pi_elim = prove_goal thy


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


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


15 


16 
(* SIMPLE TYPES *)


17 


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


19 
by (DEPTH_SOLVE (ares_tac simple 1));


20 
uresult();


21 


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


23 
by (DEPTH_SOLVE (ares_tac simple 1));


24 
uresult();


25 


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


27 
by (DEPTH_SOLVE (ares_tac simple 1));


28 
uresult();


29 


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


31 
by (DEPTH_SOLVE (ares_tac simple 1));


32 
uresult();


33 


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


35 
by (DEPTH_SOLVE (ares_tac simple 1));


36 
uresult();


37 


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


39 
by (DEPTH_SOLVE (ares_tac simple 1));


40 
uresult();


41 


42 
(* SECONDORDER TYPES *)


43 


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


45 
by (DEPTH_SOLVE (ares_tac L2 1));


46 
uresult();


47 


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


49 
by (DEPTH_SOLVE (ares_tac L2 1));


50 
uresult();


51 


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


53 
by (DEPTH_SOLVE (ares_tac L2 1));


54 
uresult();


55 


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


57 
by (DEPTH_SOLVE (ares_tac L2 1));


58 
uresult();


59 


60 
(* Weakly higherorder proposiional logic *)


61 


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


63 
by (DEPTH_SOLVE (ares_tac Lomega 1));


64 
uresult();


65 


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


67 
by (DEPTH_SOLVE (ares_tac Lomega 1));


68 
uresult();


69 


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


71 
by (DEPTH_SOLVE (ares_tac Lomega 1));


72 
uresult();


73 


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


75 
by (DEPTH_SOLVE (ares_tac Lomega 1));


76 
uresult();


77 


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


79 
by (DEPTH_SOLVE (ares_tac Lomega 1));


80 
uresult();


81 


82 
(* LF *)


83 


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


85 
by (DEPTH_SOLVE (ares_tac LP 1));


86 
uresult();


87 


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


89 
by (DEPTH_SOLVE (ares_tac LP 1));


90 
uresult();


91 


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


93 
by (DEPTH_SOLVE (ares_tac LP 1));


94 
uresult();


95 


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


97 
by (DEPTH_SOLVE (ares_tac LP 1));


98 
uresult();


99 


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


101 
by (DEPTH_SOLVE (ares_tac LP 1));


102 
uresult();


103 


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


105 
by (DEPTH_SOLVE (ares_tac LP 1));


106 
uresult();


107 


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


109 
by (DEPTH_SOLVE (ares_tac LP 1));


110 
uresult();


111 


112 
goal LP_thy "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 (ares_tac LP 1));


115 
uresult();


116 


117 
(* OMEGAORDER TYPES *)


118 


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


120 
by (DEPTH_SOLVE (ares_tac L2 1));


121 
uresult();


122 


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


124 
by (DEPTH_SOLVE (ares_tac LOmega 1));


125 
uresult();


126 


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


128 
by (DEPTH_SOLVE (ares_tac LOmega 1));


129 
uresult();


130 


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


132 
by (strip_asms_tac LOmega 1);


133 
by (rtac lam_ss 1);


134 
by (DEPTH_SOLVE_1(ares_tac LOmega 1));


135 
by (DEPTH_SOLVE_1(ares_tac LOmega 2));


136 
by (rtac lam_ss 1);


137 
by (DEPTH_SOLVE_1(ares_tac LOmega 1));


138 
by (DEPTH_SOLVE_1(ares_tac LOmega 2));


139 
by (rtac lam_ss 1);


140 
by (assume_tac 1);


141 
by (DEPTH_SOLVE_1(ares_tac LOmega 2));


142 
by (etac pi_elim 1);


143 
by (assume_tac 1);


144 
by (etac pi_elim 1);


145 
by (assume_tac 1);


146 
by (assume_tac 1);


147 
uresult();


148 


149 
(* Secondorder Predicate Logic *)


150 


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


152 
by (DEPTH_SOLVE (ares_tac LP2 1));


153 
uresult();


154 


155 
goal LP2_thy "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 (ares_tac LP2 1));


158 
uresult();


159 


160 
(* Antisymmetry implies irreflexivity: *)


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


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


163 
by (strip_asms_tac LP2 1);


164 
by (rtac lam_ss 1);


165 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


166 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


167 
by (rtac lam_ss 1);


168 
by (assume_tac 1);


169 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


170 
by (rtac lam_ss 1);


171 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


172 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


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


174 
uresult();


175 


176 
(* LPomega *)


177 


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


179 
by (DEPTH_SOLVE (ares_tac LPomega 1));


180 
uresult();


181 


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


183 
by (DEPTH_SOLVE (ares_tac LPomega 1));


184 
uresult();


185 


186 
(* CONSTRUCTIONS *)


187 


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


189 
by (DEPTH_SOLVE (ares_tac CC 1));


190 
uresult();


191 


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


193 
by (DEPTH_SOLVE (ares_tac CC 1));


194 
uresult();


195 


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


197 
by (strip_asms_tac CC 1);


198 
by (rtac lam_ss 1);


199 
by (DEPTH_SOLVE_1(ares_tac CC 1));


200 
by (DEPTH_SOLVE_1(ares_tac CC 2));


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


202 
uresult();


203 


204 
(* Some random examples *)


205 


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


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


208 
by (DEPTH_SOLVE(ares_tac LP2 1));


209 
uresult();


210 


211 
goal CC_thy "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(ares_tac CC 1));


214 
uresult();


215 


216 
(* Symmetry of Leibnitz equality *)


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


218 
by (strip_asms_tac LP2 1);


219 
by (rtac lam_ss 1);


220 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


221 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


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


223 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


224 
by (rewtac beta);


225 
by (etac imp_elim 1);


226 
by (rtac lam_bs 1);


227 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


228 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


229 
by (rtac lam_ss 1);


230 
by (DEPTH_SOLVE_1(ares_tac LP2 1));


231 
by (DEPTH_SOLVE_1(ares_tac LP2 2));


232 
by (assume_tac 1);


233 
by (assume_tac 1);


234 
uresult();
