src/HOL/Prolog/Type.thy
author oheimb
Tue Jun 11 16:43:17 2002 +0200 (2002-06-11)
changeset 13208 965f95a3abd9
parent 12338 de0f4a63baa5
child 14981 e73f8140af78
permissions -rw-r--r--
added the usual file headers
     1 (*  Title:    HOL/Prolog/Type.thy
     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 type inference 
     7 *)
     8 
     9 Type = Func +
    10 
    11 types ty
    12 
    13 arities ty :: type
    14 
    15 consts  bool	:: ty
    16 	nat	:: ty
    17 	"->"	:: ty => ty => ty	(infixr 20)
    18 	typeof	:: [tm, ty] => bool
    19         anyterm :: tm
    20 
    21 rules	common_typeof	"
    22 typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
    23 
    24 typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
    25 typeof (fix F)   A       :- (!x. typeof x A => typeof (F  x) A)..
    26 
    27 typeof true  bool..
    28 typeof false bool..
    29 typeof (M and N) bool :- typeof M bool & typeof N bool..
    30 
    31 typeof (M eq  N) bool :- typeof M T    & typeof N T   ..
    32 
    33 typeof  Z    nat..
    34 typeof (S N) nat :- typeof N nat..
    35 typeof (M + N) nat :- typeof M nat & typeof N nat..
    36 typeof (M - N) nat :- typeof M nat & typeof N nat..
    37 typeof (M * N) nat :- typeof M nat & typeof N nat"
    38 
    39 rules	good_typeof	"
    40 typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
    41 
    42 rules	bad1_typeof	"
    43 typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
    44 
    45 rules	bad2_typeof	"
    46 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
    47 
    48 end