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