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