src/HOL/Prolog/Type.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 13208 965f95a3abd9
child 20713 823967ef47f1
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:    HOL/Prolog/Type.ML
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4 *)
     5 
     6 val prog_Type = prog_Func @ [good_typeof,common_typeof];
     7 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
     8 val p = ptac prog_Type 1;
     9 
    10 pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";
    11 
    12 pgoal "typeof (fix (%x. x)) ?T";
    13 
    14 pgoal "typeof (fix (%fact. abs(%n. (app fact (n - 0))))) ?T";
    15 
    16 pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \
    17 				\(n * (app fact (n - (S 0))))))) ?T";
    18 
    19 pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *)
    20 Goal "typeof (abs(%v. 0)) ?T";
    21 by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
    22 back(); (* 2nd result (?A1 -> ?A1) wrong *)
    23 
    24 (*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*)
    25 Goal "typeof (abs(%v. abs(%v. app v v))) ?T";
    26 by (prolog_tac [bad2_typeof,common_typeof]); 
    27 	(* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)