10 |
10 |
11 |
11 |
12 subsection {* Environments *} |
12 subsection {* Environments *} |
13 |
13 |
14 definition |
14 definition |
15 shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91) |
15 shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91) where |
16 "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))" |
16 "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))" |
17 |
17 |
18 notation (xsymbols) |
18 notation (xsymbols) |
19 shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) |
19 shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) |
20 |
20 |
48 consts |
48 consts |
49 typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set" |
49 typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set" |
50 typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
50 typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
51 |
51 |
52 abbreviation |
52 abbreviation |
53 funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200) |
53 funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200) where |
54 "Ts =>> T == foldr Fun Ts T" |
54 "Ts =>> T == foldr Fun Ts T" |
55 |
55 |
56 typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50) |
56 abbreviation |
|
57 typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50) where |
57 "env |- t : T == (env, t, T) \<in> typing" |
58 "env |- t : T == (env, t, T) \<in> typing" |
58 |
59 |
|
60 abbreviation |
59 typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
61 typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
60 ("_ ||- _ : _" [50, 50, 50] 50) |
62 ("_ ||- _ : _" [50, 50, 50] 50) where |
61 "env ||- ts : Ts == typings env ts Ts" |
63 "env ||- ts : Ts == typings env ts Ts" |
62 |
64 |
63 notation (xsymbols) |
65 notation (xsymbols) |
64 typing_rel ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
66 typing_rel ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
65 |
67 |
66 notation (latex) |
68 notation (latex) |
67 funs (infixr "\<Rrightarrow>" 200) |
69 funs (infixr "\<Rrightarrow>" 200) and |
68 typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50) |
70 typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50) |
69 |
71 |
70 inductive typing |
72 inductive typing |
71 intros |
73 intros |
72 Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T" |
74 Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T" |