oheimb@13208: (*  Title:    HOL/Prolog/Type.thy
oheimb@13208:     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
oheimb@13208: *)
oheimb@9015: 
wenzelm@17311: header {* Type inference *}
oheimb@9015: 
wenzelm@17311: theory Type
wenzelm@17311: imports Func
wenzelm@17311: begin
oheimb@9015: 
wenzelm@17311: typedecl ty
oheimb@9015: 
wenzelm@51311: axiomatization
wenzelm@51311:   bool    :: ty and
wenzelm@51311:   nat     :: ty and
wenzelm@51311:   arrow   :: "ty => ty => ty"       (infixr "->" 20) and
wenzelm@51311:   typeof  :: "[tm, ty] => bool" and
wenzelm@17311:   anyterm :: tm
wenzelm@51311: where common_typeof:   "
oheimb@9015: typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
oheimb@9015: 
oheimb@9015: typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
oheimb@9015: typeof (fix F)   A       :- (!x. typeof x A => typeof (F  x) A)..
oheimb@9015: 
oheimb@9015: typeof true  bool..
oheimb@9015: typeof false bool..
oheimb@9015: typeof (M and N) bool :- typeof M bool & typeof N bool..
oheimb@9015: 
oheimb@9015: typeof (M eq  N) bool :- typeof M T    & typeof N T   ..
oheimb@9015: 
oheimb@9015: typeof  Z    nat..
oheimb@9015: typeof (S N) nat :- typeof N nat..
oheimb@9015: typeof (M + N) nat :- typeof M nat & typeof N nat..
oheimb@9015: typeof (M - N) nat :- typeof M nat & typeof N nat..
oheimb@9015: typeof (M * N) nat :- typeof M nat & typeof N nat"
oheimb@9015: 
wenzelm@51311: axiomatization where good_typeof:     "
oheimb@9015: typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
oheimb@9015: 
wenzelm@51311: axiomatization where bad1_typeof:     "
oheimb@9015: typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
oheimb@9015: 
wenzelm@51311: axiomatization where bad2_typeof:     "
oheimb@9015: typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
oheimb@9015: 
wenzelm@21425: 
wenzelm@21425: lemmas prog_Type = prog_Func good_typeof common_typeof
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
wenzelm@21425:   apply (prolog prog_Type)
wenzelm@21425:   done
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (fix (%x. x)) ?T"
wenzelm@21425:   apply (prolog prog_Type)
wenzelm@21425:   done
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
wenzelm@21425:   apply (prolog prog_Type)
wenzelm@21425:   done
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
wenzelm@21425:   (n * (app fact (n - (S Z))))))) ?T"
wenzelm@21425:   apply (prolog prog_Type)
wenzelm@21425:   done
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
wenzelm@21425:   apply (prolog prog_Type)
wenzelm@21425:   done
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (abs(%v. Z)) ?T"
wenzelm@21425:   apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
wenzelm@21425:   done
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (abs(%v. Z)) ?T"
wenzelm@21425:   apply (prolog bad1_typeof common_typeof)
wenzelm@21425:   back (* 2nd result (?A1 -> ?A1) wrong *)
wenzelm@21425:   done
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
wenzelm@21425:   apply (prolog prog_Type)?  (*correctly fails*)
wenzelm@21425:   oops
wenzelm@21425: 
wenzelm@36319: schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
wenzelm@21425:   apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
wenzelm@21425:   done
wenzelm@17311: 
oheimb@9015: end