# Theory Type

Up to index of Isabelle/HOL/Prolog

theory Type
imports Func
uses [Type.ML]
begin

    (*  Title:    HOL/Prolog/Type.thy
        ID:       $Id: Type.thy,v 1.5 2005/09/07 19:07:09 wenzelm Exp $
        Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    *)

    header {* Type inference *}

    theory Type
    imports Func
    begin

    typedecl ty

    consts
      bool    :: ty
      nat     :: ty
      "->"    :: "ty => ty => ty"       (infixr 20)
      typeof  :: "[tm, ty] => bool"
      anyterm :: tm

    axioms  common_typeof:   "
    typeof (app M N) B       :- typeof M (A -> B) & typeof N A..

    typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
    typeof (fix F)   A       :- (!x. typeof x A => typeof (F  x) A)..

    typeof true  bool..
    typeof false bool..
    typeof (M and N) bool :- typeof M bool & typeof N bool..

    typeof (M eq  N) bool :- typeof M T    & typeof N T   ..

    typeof  Z    nat..
    typeof (S N) nat :- typeof N nat..
    typeof (M + N) nat :- typeof M nat & typeof N nat..
    typeof (M - N) nat :- typeof M nat & typeof N nat..
    typeof (M * N) nat :- typeof M nat & typeof N nat"

    axioms good_typeof:     "
    typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"

    axioms bad1_typeof:     "
    typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"

    axioms bad2_typeof:     "
    typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"

    ML {* use_legacy_bindings (the_context ()) *}

    end