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