src/HOL/Prolog/Type.ML
changeset 21425 c11ab38b78a7
parent 21424 5295ffa18285
child 21426 87ac12bed1ab
     1.1 --- a/src/HOL/Prolog/Type.ML	Mon Nov 20 11:51:10 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,27 +0,0 @@
     1.4 -(*  Title:    HOL/Prolog/Type.ML
     1.5 -    ID:       $Id$
     1.6 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.7 -*)
     1.8 -
     1.9 -val prog_Type = prog_Func @ [good_typeof,common_typeof];
    1.10 -fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
    1.11 -val p = ptac prog_Type 1;
    1.12 -
    1.13 -pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";
    1.14 -
    1.15 -pgoal "typeof (fix (%x. x)) ?T";
    1.16 -
    1.17 -pgoal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T";
    1.18 -
    1.19 -pgoal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
    1.20 -  \(n * (app fact (n - (S Z))))))) ?T";
    1.21 -
    1.22 -pgoal "typeof (abs(%v. Z)) ?T"; (*correct only solution (?A1 -> nat) *)
    1.23 -Goal "typeof (abs(%v. Z)) ?T";
    1.24 -by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
    1.25 -back(); (* 2nd result (?A1 -> ?A1) wrong *)
    1.26 -
    1.27 -(*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*)
    1.28 -Goal "typeof (abs(%v. abs(%v. app v v))) ?T";
    1.29 -by (prolog_tac [bad2_typeof,common_typeof]); 
    1.30 -	(* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)