| author | kleing |
| Tue, 13 May 2003 08:59:21 +0200 | |
| changeset 14024 | 213dcc39358f |
| parent 13208 | 965f95a3abd9 |
| child 14981 | e73f8140af78 |
| permissions | -rw-r--r-- |
| 13208 | 1 |
(* Title: HOL/Prolog/Type.ML |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
*) |
|
6 |
||
| 9015 | 7 |
val prog_Type = prog_Func @ [good_typeof,common_typeof]; |
| 12486 | 8 |
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type)); |
| 9015 | 9 |
val p = ptac prog_Type 1; |
10 |
||
11 |
pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"; |
|
12 |
||
13 |
pgoal "typeof (fix (%x. x)) ?T"; |
|
14 |
||
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
9015
diff
changeset
|
15 |
pgoal "typeof (fix (%fact. abs(%n. (app fact (n - 0))))) ?T"; |
| 9015 | 16 |
|
17 |
pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \ |
|
18 |
\(n * (app fact (n - (S 0))))))) ?T"; |
|
19 |
||
20 |
pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *) |
|
21 |
Goal "typeof (abs(%v. 0)) ?T"; |
|
22 |
by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*) |
|
23 |
back(); (* 2nd result (?A1 -> ?A1) wrong *) |
|
24 |
||
25 |
(*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*) |
|
26 |
Goal "typeof (abs(%v. abs(%v. app v v))) ?T"; |
|
27 |
by (prolog_tac [bad2_typeof,common_typeof]); |
|
28 |
(* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*) |