src/HOL/Prolog/Type.thy
changeset 9015 8006e9009621
child 12338 de0f4a63baa5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Prolog/Type.thy	Fri Jun 02 12:44:04 2000 +0200
     1.3 @@ -0,0 +1,42 @@
     1.4 +(* type inference *)
     1.5 +
     1.6 +Type = Func +
     1.7 +
     1.8 +types ty
     1.9 +
    1.10 +arities ty :: term
    1.11 +
    1.12 +consts  bool	:: ty
    1.13 +	nat	:: ty
    1.14 +	"->"	:: ty => ty => ty	(infixr 20)
    1.15 +	typeof	:: [tm, ty] => bool
    1.16 +        anyterm :: tm
    1.17 +
    1.18 +rules	common_typeof	"
    1.19 +typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
    1.20 +
    1.21 +typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
    1.22 +typeof (fix F)   A       :- (!x. typeof x A => typeof (F  x) A)..
    1.23 +
    1.24 +typeof true  bool..
    1.25 +typeof false bool..
    1.26 +typeof (M and N) bool :- typeof M bool & typeof N bool..
    1.27 +
    1.28 +typeof (M eq  N) bool :- typeof M T    & typeof N T   ..
    1.29 +
    1.30 +typeof  Z    nat..
    1.31 +typeof (S N) nat :- typeof N nat..
    1.32 +typeof (M + N) nat :- typeof M nat & typeof N nat..
    1.33 +typeof (M - N) nat :- typeof M nat & typeof N nat..
    1.34 +typeof (M * N) nat :- typeof M nat & typeof N nat"
    1.35 +
    1.36 +rules	good_typeof	"
    1.37 +typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
    1.38 +
    1.39 +rules	bad1_typeof	"
    1.40 +typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
    1.41 +
    1.42 +rules	bad2_typeof	"
    1.43 +typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
    1.44 +
    1.45 +end