1theory Type_Preservation
2  imports "HOL-Nominal.Nominal"
3begin
4
5text \<open>
6
7  This theory shows how to prove the type preservation
8  property for the simply-typed lambda-calculus and 
9  beta-reduction.
10 
11\<close>
12
13atom_decl name
14
15nominal_datatype lam =
16  Var "name"
17| App "lam" "lam" 
18| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._")
19
20text \<open>Capture-Avoiding Substitution\<close>
21
22nominal_primrec
23  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]")
24where
25  "(Var x)[y::=s] = (if x=y then s else (Var x))"
26| "(App t\<^sub>1 t\<^sub>2)[y::=s] = App (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])"
27| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
28apply(finite_guess)+
29apply(rule TrueI)+
30apply(simp add: abs_fresh)
31apply(fresh_guess)+
32done
33
34lemma  subst_eqvt[eqvt]:
35  fixes pi::"name prm"
36  shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
37by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
38   (auto simp add: perm_bij fresh_atm fresh_bij)
39
40lemma fresh_fact:
41  fixes z::"name"
42  shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
43by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
44   (auto simp add: abs_fresh fresh_prod fresh_atm)
45
46text \<open>Types\<close>
47
48nominal_datatype ty =
49    TVar "string"
50  | TArr "ty" "ty" ("_ \<rightarrow> _")
51
52lemma ty_fresh:
53  fixes x::"name"
54  and   T::"ty"
55  shows "x\<sharp>T"
56by (induct T rule: ty.induct)
57   (auto simp add: fresh_string)
58
59text \<open>Typing Contexts\<close>
60
61type_synonym ctx = "(name\<times>ty) list"
62
63abbreviation
64  "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<subseteq> _") 
65where
66  "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^sub>1 \<longrightarrow> x \<in> set \<Gamma>\<^sub>2"
67
68text \<open>Validity of Typing Contexts\<close>
69
70inductive
71  valid :: "(name\<times>ty) list \<Rightarrow> bool"
72where
73    v1[intro]: "valid []"
74  | v2[intro]: "\<lbrakk>valid \<Gamma>; x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)"
75
76equivariance valid
77
78lemma valid_elim[dest]:
79  assumes a: "valid ((x,T)#\<Gamma>)"
80  shows "x\<sharp>\<Gamma> \<and> valid \<Gamma>"
81using a by (cases) (auto)
82
83lemma valid_insert:
84  assumes a: "valid (\<Delta>@[(x,T)]@\<Gamma>)"
85  shows "valid (\<Delta> @ \<Gamma>)" 
86using a
87by (induct \<Delta>)
88   (auto simp add:  fresh_list_append fresh_list_cons dest!: valid_elim)
89
90lemma fresh_set: 
91  shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)"
92by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)
93
94lemma context_unique:
95  assumes a1: "valid \<Gamma>"
96  and     a2: "(x,T) \<in> set \<Gamma>"
97  and     a3: "(x,U) \<in> set \<Gamma>"
98  shows "T = U" 
99using a1 a2 a3
100by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)
101
102text \<open>Typing Relation\<close>
103
104inductive
105  typing :: "ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _") 
106where
107  t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
108| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t\<^sub>1 t\<^sub>2 : T\<^sub>2"
109| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2"
110
111equivariance typing
112nominal_inductive typing
113  by (simp_all add: abs_fresh ty_fresh)
114
115lemma t_Lam_inversion[dest]:
116  assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 
117  and     fc: "x\<sharp>\<Gamma>" 
118  shows "\<exists>T\<^sub>1 T\<^sub>2. T = T\<^sub>1 \<rightarrow> T\<^sub>2 \<and> (x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2"
119using ty fc 
120by (cases rule: typing.strong_cases) 
121   (auto simp add: alpha lam.inject abs_fresh ty_fresh)
122
123lemma t_App_inversion[dest]:
124  assumes ty: "\<Gamma> \<turnstile> App t1 t2 : T" 
125  shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
126using ty 
127by (cases) (auto simp add: lam.inject)
128
129lemma weakening: 
130  fixes \<Gamma>1 \<Gamma>2::"ctx"
131  assumes a: "\<Gamma>1 \<turnstile> t : T" 
132  and     b: "valid \<Gamma>2" 
133  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
134  shows "\<Gamma>2 \<turnstile> t : T"
135using a b c
136by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
137   (auto | atomize)+
138
139lemma type_substitution_aux:
140  assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T"
141  and     b: "\<Gamma> \<turnstile> e' : T'"
142  shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
143using a b 
144proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
145  case (t_Var y T x e' \<Delta>)
146  then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
147       and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
148       and  a3: "\<Gamma> \<turnstile> e' : T'" .
149  from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
150  { assume eq: "x=y"
151    from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
152    with a3 have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
153  }
154  moreover
155  { assume ineq: "x\<noteq>y"
156    from a2 have "(y,T) \<in> set (\<Delta>@\<Gamma>)" using ineq by simp
157    then have "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto
158  }
159  ultimately show "\<Delta>@\<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
160qed (force simp add: fresh_list_append fresh_list_cons)+
161
162corollary type_substitution:
163  assumes a: "(x,T')#\<Gamma> \<turnstile> e : T"
164  and     b: "\<Gamma> \<turnstile> e' : T'"
165  shows "\<Gamma> \<turnstile> e[x::=e'] : T"
166using a b
167by (auto intro: type_substitution_aux[where \<Delta>="[]",simplified])
168
169text \<open>Beta Reduction\<close>
170
171inductive 
172  "beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta> _")
173where
174  b1[intro]: "t1 \<longrightarrow>\<^sub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^sub>\<beta> App t2 s"
175| b2[intro]: "s1 \<longrightarrow>\<^sub>\<beta> s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^sub>\<beta> App t s2"
176| b3[intro]: "t1 \<longrightarrow>\<^sub>\<beta> t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^sub>\<beta> Lam [x].t2"
177| b4[intro]: "x\<sharp>s \<Longrightarrow> App (Lam [x].t) s \<longrightarrow>\<^sub>\<beta> t[x::=s]"
178
179equivariance beta
180nominal_inductive beta
181  by (auto simp add: abs_fresh fresh_fact)
182
183
184theorem type_preservation:
185  assumes a: "t \<longrightarrow>\<^sub>\<beta> t'"
186  and     b: "\<Gamma> \<turnstile> t : T" 
187  shows "\<Gamma> \<turnstile> t' : T" 
188using a b
189proof (nominal_induct avoiding: \<Gamma> T rule: beta.strong_induct)
190  case (b1 t1 t2 s \<Gamma> T)
191  have "\<Gamma> \<turnstile> App t1 s : T" by fact
192  then obtain T' where a1: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto
193  have ih: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<Longrightarrow> \<Gamma> \<turnstile> t2 : T' \<rightarrow> T" by fact
194  with a1 a2 show "\<Gamma> \<turnstile> App t2 s : T" by auto
195next 
196  case (b2 s1 s2 t \<Gamma> T)
197  have "\<Gamma> \<turnstile> App t s1 : T" by fact
198  then obtain T' where a1: "\<Gamma> \<turnstile> t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s1 : T'" by auto
199  have ih: "\<Gamma> \<turnstile> s1 : T' \<Longrightarrow> \<Gamma> \<turnstile> s2 : T'" by fact
200  with a1 a2 show "\<Gamma> \<turnstile> App t s2 : T" by auto
201next 
202  case (b3 t1 t2 x \<Gamma> T)
203  have vc: "x\<sharp>\<Gamma>" by fact
204  have "\<Gamma> \<turnstile> Lam [x].t1 : T" by fact
205  then obtain T1 T2 where a1: "(x,T1)#\<Gamma> \<turnstile> t1 : T2" and a2: "T = T1 \<rightarrow> T2" using vc by auto
206  have ih: "(x,T1)#\<Gamma> \<turnstile> t1 : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> t2 : T2" by fact
207  with a1 a2 show "\<Gamma> \<turnstile> Lam [x].t2 : T" using vc by auto
208next
209  case (b4 x s t \<Gamma> T)
210  have vc: "x\<sharp>\<Gamma>" by fact
211  have "\<Gamma> \<turnstile> App (Lam [x].t) s : T" by fact
212  then obtain T' where a1: "\<Gamma> \<turnstile> Lam [x].t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto
213  from a1 obtain T1 T2 where a3: "(x,T')#\<Gamma> \<turnstile> t : T" using vc by (auto simp add: ty.inject)
214  from a3 a2 show "\<Gamma> \<turnstile> t[x::=s] : T" by (simp add: type_substitution)
215qed
216
217
218theorem type_preservation_automatic:
219  assumes a: "t \<longrightarrow>\<^sub>\<beta> t'"
220  and     b: "\<Gamma> \<turnstile> t : T" 
221  shows "\<Gamma> \<turnstile> t' : T"
222using a b
223by (nominal_induct avoiding: \<Gamma> T rule: beta.strong_induct)
224   (auto dest!: t_Lam_inversion t_App_inversion simp add: ty.inject type_substitution)
225
226end
227