1(* Title: HOL/Prolog/Type.thy 2 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) 3*) 4 5section \<open>Type inference\<close> 6 7theory Type 8imports Func 9begin 10 11typedecl ty 12 13axiomatization 14 bool :: ty and 15 nat :: ty and 16 arrow :: "ty \<Rightarrow> ty \<Rightarrow> ty" (infixr "->" 20) and 17 typeof :: "[tm, ty] \<Rightarrow> bool" and 18 anyterm :: tm 19where common_typeof: " 20typeof (app M N) B :- typeof M (A -> B) \<and> typeof N A.. 21 22typeof (cond C L R) A :- typeof C bool \<and> typeof L A \<and> typeof R A.. 23typeof (fix F) A :- (\<forall>x. typeof x A => typeof (F x) A).. 24 25typeof true bool.. 26typeof false bool.. 27typeof (M and N) bool :- typeof M bool & typeof N bool.. 28 29typeof (M eq N) bool :- typeof M T & typeof N T .. 30 31typeof Z nat.. 32typeof (S N) nat :- typeof N nat.. 33typeof (M + N) nat :- typeof M nat & typeof N nat.. 34typeof (M - N) nat :- typeof M nat & typeof N nat.. 35typeof (M * N) nat :- typeof M nat & typeof N nat" 36 37axiomatization where good_typeof: " 38typeof (abs Bo) (A -> B) :- (\<forall>x. typeof x A => typeof (Bo x) B)" 39 40axiomatization where bad1_typeof: " 41typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)" 42 43axiomatization where bad2_typeof: " 44typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)" 45 46 47lemmas prog_Type = prog_Func good_typeof common_typeof 48 49schematic_goal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T" 50 apply (prolog prog_Type) 51 done 52 53schematic_goal "typeof (fix (%x. x)) ?T" 54 apply (prolog prog_Type) 55 done 56 57schematic_goal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T" 58 apply (prolog prog_Type) 59 done 60 61schematic_goal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) 62 (n * (app fact (n - (S Z))))))) ?T" 63 apply (prolog prog_Type) 64 done 65 66schematic_goal "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *) 67 apply (prolog prog_Type) 68 done 69 70schematic_goal "typeof (abs(%v. Z)) ?T" 71 apply (prolog bad1_typeof common_typeof) (* 1st result ok*) 72 done 73 74schematic_goal "typeof (abs(%v. Z)) ?T" 75 apply (prolog bad1_typeof common_typeof) 76 back (* 2nd result (?A1 -> ?A1) wrong *) 77 done 78 79schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T" 80 apply (prolog prog_Type)? (*correctly fails*) 81 oops 82 83schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T" 84 apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*) 85 done 86 87end 88