|
9015
|
1 |
val prog_Type = prog_Func @ [good_typeof,common_typeof];
|
|
|
2 |
fun pgoal s = (case Goal s of _ => by(prolog_tac prog_Type));
|
|
|
3 |
val p = ptac prog_Type 1;
|
|
|
4 |
|
|
|
5 |
pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";
|
|
|
6 |
|
|
|
7 |
pgoal "typeof (fix (%x. x)) ?T";
|
|
|
8 |
|
|
|
9 |
pgoal "typeof (fix (%fact. abs(%n. (app fact (n-0))))) ?T";
|
|
|
10 |
|
|
|
11 |
pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \
|
|
|
12 |
\(n * (app fact (n - (S 0))))))) ?T";
|
|
|
13 |
|
|
|
14 |
pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *)
|
|
|
15 |
Goal "typeof (abs(%v. 0)) ?T";
|
|
|
16 |
by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
|
|
|
17 |
back(); (* 2nd result (?A1 -> ?A1) wrong *)
|
|
|
18 |
|
|
|
19 |
(*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*)
|
|
|
20 |
Goal "typeof (abs(%v. abs(%v. app v v))) ?T";
|
|
|
21 |
by (prolog_tac [bad2_typeof,common_typeof]);
|
|
|
22 |
(* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
|