src/HOL/Prolog/Type.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9015 8006e9009621
child 11701 3d51fbf81c17
permissions -rw-r--r--
improved theory reference in comment
     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)*)