|
1 header {* Simply-typed lambda-calculus with let and tuple patterns *} |
|
2 |
|
3 theory Pattern |
|
4 imports Nominal |
|
5 begin |
|
6 |
|
7 no_syntax |
|
8 "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])") |
|
9 |
|
10 atom_decl name |
|
11 |
|
12 nominal_datatype ty = |
|
13 Atom nat |
|
14 | Arrow ty ty (infixr "\<rightarrow>" 200) |
|
15 | TupleT ty ty (infixr "\<otimes>" 210) |
|
16 |
|
17 lemma fresh_type [simp]: "(a::name) \<sharp> (T::ty)" |
|
18 by (induct T rule: ty.induct) (simp_all add: fresh_nat) |
|
19 |
|
20 lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)" |
|
21 by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat) |
|
22 |
|
23 lemma perm_type: "(pi::name prm) \<bullet> (T::ty) = T" |
|
24 by (induct T rule: ty.induct) (simp_all add: perm_nat_def) |
|
25 |
|
26 nominal_datatype trm = |
|
27 Var name |
|
28 | Tuple trm trm ("(1'\<langle>_,/ _'\<rangle>)") |
|
29 | Abs ty "\<guillemotleft>name\<guillemotright>trm" |
|
30 | App trm trm (infixl "\<cdot>" 200) |
|
31 | Let ty trm btrm |
|
32 and btrm = |
|
33 Base trm |
|
34 | Bind ty "\<guillemotleft>name\<guillemotright>btrm" |
|
35 |
|
36 abbreviation |
|
37 Abs_syn :: "name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) |
|
38 where |
|
39 "\<lambda>x:T. t \<equiv> Abs T x t" |
|
40 |
|
41 datatype pat = |
|
42 PVar name ty |
|
43 | PTuple pat pat ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)") |
|
44 |
|
45 (* FIXME: The following should be done automatically by the nominal package *) |
|
46 overloading pat_perm \<equiv> "perm :: name prm \<Rightarrow> pat \<Rightarrow> pat" (unchecked) |
|
47 begin |
|
48 |
|
49 primrec pat_perm |
|
50 where |
|
51 "pat_perm pi (PVar x ty) = PVar (pi \<bullet> x) (pi \<bullet> ty)" |
|
52 | "pat_perm pi \<langle>\<langle>p, q\<rangle>\<rangle> = \<langle>\<langle>pat_perm pi p, pat_perm pi q\<rangle>\<rangle>" |
|
53 |
|
54 end |
|
55 |
|
56 declare pat_perm.simps [eqvt] |
|
57 |
|
58 lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x" |
|
59 by (simp add: supp_def perm_fresh_fresh) |
|
60 |
|
61 lemma supp_PTuple [simp]: "((supp \<langle>\<langle>p, q\<rangle>\<rangle>)::name set) = supp p \<union> supp q" |
|
62 by (simp add: supp_def Collect_disj_eq del: disj_not1) |
|
63 |
|
64 instance pat :: pt_name |
|
65 proof intro_classes |
|
66 case goal1 |
|
67 show ?case by (induct x) simp_all |
|
68 next |
|
69 case goal2 |
|
70 show ?case by (induct x) (simp_all add: pt_name2) |
|
71 next |
|
72 case goal3 |
|
73 then show ?case by (induct x) (simp_all add: pt_name3) |
|
74 qed |
|
75 |
|
76 instance pat :: fs_name |
|
77 proof intro_classes |
|
78 case goal1 |
|
79 show ?case by (induct x) (simp_all add: fin_supp) |
|
80 qed |
|
81 |
|
82 (* the following function cannot be defined using nominal_primrec, *) |
|
83 (* since variable parameters are currently not allowed. *) |
|
84 primrec abs_pat :: "pat \<Rightarrow> btrm \<Rightarrow> btrm" ("(3\<lambda>[_]./ _)" [0, 10] 10) |
|
85 where |
|
86 "(\<lambda>[PVar x T]. t) = Bind T x t" |
|
87 | "(\<lambda>[\<langle>\<langle>p, q\<rangle>\<rangle>]. t) = (\<lambda>[p]. \<lambda>[q]. t)" |
|
88 |
|
89 lemma abs_pat_eqvt [eqvt]: |
|
90 "(pi :: name prm) \<bullet> (\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. (pi \<bullet> t))" |
|
91 by (induct p arbitrary: t) simp_all |
|
92 |
|
93 lemma abs_pat_fresh [simp]: |
|
94 "(x::name) \<sharp> (\<lambda>[p]. t) = (x \<in> supp p \<or> x \<sharp> t)" |
|
95 by (induct p arbitrary: t) (simp_all add: abs_fresh supp_atm) |
|
96 |
|
97 lemma abs_pat_alpha: |
|
98 assumes fresh: "((pi::name prm) \<bullet> supp p::name set) \<sharp>* t" |
|
99 and pi: "set pi \<subseteq> supp p \<times> pi \<bullet> supp p" |
|
100 shows "(\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. pi \<bullet> t)" |
|
101 proof - |
|
102 note pt_name_inst at_name_inst pi |
|
103 moreover have "(supp p::name set) \<sharp>* (\<lambda>[p]. t)" |
|
104 by (simp add: fresh_star_def) |
|
105 moreover from fresh |
|
106 have "(pi \<bullet> supp p::name set) \<sharp>* (\<lambda>[p]. t)" |
|
107 by (simp add: fresh_star_def) |
|
108 ultimately have "pi \<bullet> (\<lambda>[p]. t) = (\<lambda>[p]. t)" |
|
109 by (rule pt_freshs_freshs) |
|
110 then show ?thesis by (simp add: eqvts) |
|
111 qed |
|
112 |
|
113 primrec pat_vars :: "pat \<Rightarrow> name list" |
|
114 where |
|
115 "pat_vars (PVar x T) = [x]" |
|
116 | "pat_vars \<langle>\<langle>p, q\<rangle>\<rangle> = pat_vars q @ pat_vars p" |
|
117 |
|
118 lemma pat_vars_eqvt [eqvt]: |
|
119 "(pi :: name prm) \<bullet> (pat_vars p) = pat_vars (pi \<bullet> p)" |
|
120 by (induct p rule: pat.induct) (simp_all add: eqvts) |
|
121 |
|
122 lemma set_pat_vars_supp: "set (pat_vars p) = supp p" |
|
123 by (induct p) (auto simp add: supp_atm) |
|
124 |
|
125 lemma distinct_eqvt [eqvt]: |
|
126 "(pi :: name prm) \<bullet> (distinct (xs::name list)) = distinct (pi \<bullet> xs)" |
|
127 by (induct xs) (simp_all add: eqvts) |
|
128 |
|
129 primrec pat_type :: "pat \<Rightarrow> ty" |
|
130 where |
|
131 "pat_type (PVar x T) = T" |
|
132 | "pat_type \<langle>\<langle>p, q\<rangle>\<rangle> = pat_type p \<otimes> pat_type q" |
|
133 |
|
134 lemma pat_type_eqvt [eqvt]: |
|
135 "(pi :: name prm) \<bullet> (pat_type p) = pat_type (pi \<bullet> p)" |
|
136 by (induct p) simp_all |
|
137 |
|
138 lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \<bullet> p) = pat_type p" |
|
139 by (induct p) (simp_all add: perm_type) |
|
140 |
|
141 types ctx = "(name \<times> ty) list" |
|
142 |
|
143 inductive |
|
144 ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool" ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60) |
|
145 where |
|
146 PVar: "\<turnstile> PVar x T : T \<Rightarrow> [(x, T)]" |
|
147 | PTuple: "\<turnstile> p : T \<Rightarrow> \<Delta>\<^isub>1 \<Longrightarrow> \<turnstile> q : U \<Rightarrow> \<Delta>\<^isub>2 \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> : T \<otimes> U \<Rightarrow> \<Delta>\<^isub>2 @ \<Delta>\<^isub>1" |
|
148 |
|
149 lemma pat_vars_ptyping: |
|
150 assumes "\<turnstile> p : T \<Rightarrow> \<Delta>" |
|
151 shows "pat_vars p = map fst \<Delta>" using assms |
|
152 by induct simp_all |
|
153 |
|
154 inductive |
|
155 valid :: "ctx \<Rightarrow> bool" |
|
156 where |
|
157 Nil [intro!]: "valid []" |
|
158 | Cons [intro!]: "valid \<Gamma> \<Longrightarrow> x \<sharp> \<Gamma> \<Longrightarrow> valid ((x, T) # \<Gamma>)" |
|
159 |
|
160 inductive_cases validE[elim!]: "valid ((x, T) # \<Gamma>)" |
|
161 |
|
162 lemma fresh_ctxt_set_eq: "((x::name) \<sharp> (\<Gamma>::ctx)) = (x \<notin> fst ` set \<Gamma>)" |
|
163 by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm) |
|
164 |
|
165 lemma valid_distinct: "valid \<Gamma> = distinct (map fst \<Gamma>)" |
|
166 by (induct \<Gamma>) (auto simp add: fresh_ctxt_set_eq [symmetric]) |
|
167 |
|
168 abbreviation |
|
169 "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _") |
|
170 where |
|
171 "\<Gamma>\<^isub>1 \<sqsubseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^isub>1 \<longrightarrow> x \<in> set \<Gamma>\<^isub>2" |
|
172 |
|
173 abbreviation |
|
174 Let_syn :: "pat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("(LET (_ =/ _)/ IN (_))" 10) |
|
175 where |
|
176 "LET p = t IN u \<equiv> Let (pat_type p) t (\<lambda>[p]. Base u)" |
|
177 |
|
178 inductive typing :: "ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60) |
|
179 where |
|
180 Var [intro]: "valid \<Gamma> \<Longrightarrow> (x, T) \<in> set \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
|
181 | Tuple [intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> u : U \<Longrightarrow> \<Gamma> \<turnstile> \<langle>t, u\<rangle> : T \<otimes> U" |
|
182 | Abs [intro]: "(x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T. t) : T \<rightarrow> U" |
|
183 | App [intro]: "\<Gamma> \<turnstile> t : T \<rightarrow> U \<Longrightarrow> \<Gamma> \<turnstile> u : T \<Longrightarrow> \<Gamma> \<turnstile> t \<cdot> u : U" |
|
184 | Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow> |
|
185 \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> |
|
186 \<Gamma> \<turnstile> (LET p = t IN u) : U" |
|
187 |
|
188 equivariance ptyping |
|
189 |
|
190 equivariance valid |
|
191 |
|
192 equivariance typing |
|
193 |
|
194 lemma valid_typing: |
|
195 assumes "\<Gamma> \<turnstile> t : T" |
|
196 shows "valid \<Gamma>" using assms |
|
197 by induct auto |
|
198 |
|
199 lemma pat_var: |
|
200 assumes "\<turnstile> p : T \<Rightarrow> \<Delta>" |
|
201 shows "(supp p::name set) = supp \<Delta>" using assms |
|
202 by induct (auto simp add: supp_list_nil supp_list_cons supp_prod supp_list_append) |
|
203 |
|
204 lemma valid_app_fresh: |
|
205 assumes "valid (\<Delta> @ \<Gamma>)" and "(x::name) \<in> supp \<Delta>" |
|
206 shows "x \<sharp> \<Gamma>" using assms |
|
207 by (induct \<Delta>) |
|
208 (auto simp add: supp_list_nil supp_list_cons supp_prod supp_atm fresh_list_append) |
|
209 |
|
210 lemma pat_freshs: |
|
211 assumes "\<turnstile> p : T \<Rightarrow> \<Delta>" |
|
212 shows "(supp p::name set) \<sharp>* c = (supp \<Delta>::name set) \<sharp>* c" using assms |
|
213 by (auto simp add: fresh_star_def pat_var) |
|
214 |
|
215 lemma valid_app_mono: |
|
216 assumes "valid (\<Delta> @ \<Gamma>\<^isub>1)" and "(supp \<Delta>::name set) \<sharp>* \<Gamma>\<^isub>2" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<sqsubseteq> \<Gamma>\<^isub>2" |
|
217 shows "valid (\<Delta> @ \<Gamma>\<^isub>2)" using assms |
|
218 by (induct \<Delta>) |
|
219 (auto simp add: supp_list_cons fresh_star_Un_elim supp_prod |
|
220 fresh_list_append supp_atm fresh_star_insert_elim fresh_star_empty_elim) |
|
221 |
|
222 nominal_inductive2 typing |
|
223 avoids |
|
224 Abs: "{x}" |
|
225 | Let: "(supp p)::name set" |
|
226 by (auto simp add: fresh_star_def abs_fresh fin_supp pat_var |
|
227 dest!: valid_typing valid_app_fresh) |
|
228 |
|
229 lemma better_T_Let [intro]: |
|
230 assumes t: "\<Gamma> \<turnstile> t : T" and p: "\<turnstile> p : T \<Rightarrow> \<Delta>" and u: "\<Delta> @ \<Gamma> \<turnstile> u : U" |
|
231 shows "\<Gamma> \<turnstile> (LET p = t IN u) : U" |
|
232 proof - |
|
233 obtain pi::"name prm" where pi: "(pi \<bullet> (supp p::name set)) \<sharp>* (t, Base u, \<Gamma>)" |
|
234 and pi': "set pi \<subseteq> supp p \<times> (pi \<bullet> supp p)" |
|
235 by (rule at_set_avoiding [OF at_name_inst fin_supp fin_supp]) |
|
236 from p u have p_fresh: "(supp p::name set) \<sharp>* \<Gamma>" |
|
237 by (auto simp add: fresh_star_def pat_var dest!: valid_typing valid_app_fresh) |
|
238 from pi have p_fresh': "(pi \<bullet> (supp p::name set)) \<sharp>* \<Gamma>" |
|
239 by (simp add: fresh_star_prod_elim) |
|
240 from pi have p_fresh'': "(pi \<bullet> (supp p::name set)) \<sharp>* Base u" |
|
241 by (simp add: fresh_star_prod_elim) |
|
242 from pi have "(supp (pi \<bullet> p)::name set) \<sharp>* t" |
|
243 by (simp add: fresh_star_prod_elim eqvts) |
|
244 moreover note t |
|
245 moreover from p have "pi \<bullet> (\<turnstile> p : T \<Rightarrow> \<Delta>)" by (rule perm_boolI) |
|
246 then have "\<turnstile> (pi \<bullet> p) : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: eqvts perm_type) |
|
247 moreover from u have "pi \<bullet> (\<Delta> @ \<Gamma> \<turnstile> u : U)" by (rule perm_boolI) |
|
248 with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' p_fresh p_fresh'] |
|
249 have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> (pi \<bullet> u) : U" by (simp add: eqvts perm_type) |
|
250 ultimately have "\<Gamma> \<turnstile> (LET (pi \<bullet> p) = t IN (pi \<bullet> u)) : U" |
|
251 by (rule Let) |
|
252 then show ?thesis by (simp add: abs_pat_alpha [OF p_fresh'' pi'] pat_type_perm_eq) |
|
253 qed |
|
254 |
|
255 lemma weakening: |
|
256 assumes "\<Gamma>\<^isub>1 \<turnstile> t : T" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<sqsubseteq> \<Gamma>\<^isub>2" |
|
257 shows "\<Gamma>\<^isub>2 \<turnstile> t : T" using assms |
|
258 apply (nominal_induct \<Gamma>\<^isub>1 t T avoiding: \<Gamma>\<^isub>2 rule: typing.strong_induct) |
|
259 apply auto |
|
260 apply (drule_tac x="(x, T) # \<Gamma>\<^isub>2" in meta_spec) |
|
261 apply (auto intro: valid_typing) |
|
262 apply (drule_tac x="\<Gamma>\<^isub>2" in meta_spec) |
|
263 apply (drule_tac x="\<Delta> @ \<Gamma>\<^isub>2" in meta_spec) |
|
264 apply (auto intro: valid_typing) |
|
265 apply (rule typing.Let) |
|
266 apply assumption+ |
|
267 apply (drule meta_mp) |
|
268 apply (rule valid_app_mono) |
|
269 apply (rule valid_typing) |
|
270 apply assumption |
|
271 apply (auto simp add: pat_freshs) |
|
272 done |
|
273 |
|
274 inductive |
|
275 match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool" ("\<turnstile> _ \<rhd> _ \<Rightarrow> _" [50, 50, 50] 50) |
|
276 where |
|
277 PVar: "\<turnstile> PVar x T \<rhd> t \<Rightarrow> [(x, t)]" |
|
278 | PProd: "\<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> \<turnstile> q \<rhd> u \<Rightarrow> \<theta>' \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> \<langle>t, u\<rangle> \<Rightarrow> \<theta> @ \<theta>'" |
|
279 |
|
280 fun |
|
281 lookup :: "(name \<times> trm) list \<Rightarrow> name \<Rightarrow> trm" |
|
282 where |
|
283 "lookup [] x = Var x" |
|
284 | "lookup ((y, e) # \<theta>) x = (if x = y then e else lookup \<theta> x)" |
|
285 |
|
286 lemma lookup_eqvt[eqvt]: |
|
287 fixes pi :: "name prm" |
|
288 and \<theta> :: "(name \<times> trm) list" |
|
289 and X :: "name" |
|
290 shows "pi \<bullet> (lookup \<theta> X) = lookup (pi \<bullet> \<theta>) (pi \<bullet> X)" |
|
291 by (induct \<theta>) (auto simp add: eqvts) |
|
292 |
|
293 nominal_primrec |
|
294 psubst :: "(name \<times> trm) list \<Rightarrow> trm \<Rightarrow> trm" ("_\<lparr>_\<rparr>" [95,0] 210) |
|
295 and psubstb :: "(name \<times> trm) list \<Rightarrow> btrm \<Rightarrow> btrm" ("_\<lparr>_\<rparr>\<^sub>b" [95,0] 210) |
|
296 where |
|
297 "\<theta>\<lparr>Var x\<rparr> = (lookup \<theta> x)" |
|
298 | "\<theta>\<lparr>t \<cdot> u\<rparr> = \<theta>\<lparr>t\<rparr> \<cdot> \<theta>\<lparr>u\<rparr>" |
|
299 | "\<theta>\<lparr>\<langle>t, u\<rangle>\<rparr> = \<langle>\<theta>\<lparr>t\<rparr>, \<theta>\<lparr>u\<rparr>\<rangle>" |
|
300 | "\<theta>\<lparr>Let T t u\<rparr> = Let T (\<theta>\<lparr>t\<rparr>) (\<theta>\<lparr>u\<rparr>\<^sub>b)" |
|
301 | "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>x:T. t\<rparr> = (\<lambda>x:T. \<theta>\<lparr>t\<rparr>)" |
|
302 | "\<theta>\<lparr>Base t\<rparr>\<^sub>b = Base (\<theta>\<lparr>t\<rparr>)" |
|
303 | "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>Bind T x t\<rparr>\<^sub>b = Bind T x (\<theta>\<lparr>t\<rparr>\<^sub>b)" |
|
304 apply finite_guess+ |
|
305 apply (simp add: abs_fresh | fresh_guess)+ |
|
306 done |
|
307 |
|
308 lemma lookup_fresh: |
|
309 "x = y \<longrightarrow> x \<in> set (map fst \<theta>) \<Longrightarrow> \<forall>(y, t)\<in>set \<theta>. x \<sharp> t \<Longrightarrow> x \<sharp> lookup \<theta> y" |
|
310 apply (induct \<theta>) |
|
311 apply (simp_all add: split_paired_all fresh_atm) |
|
312 apply (case_tac "x = y") |
|
313 apply (auto simp add: fresh_atm) |
|
314 done |
|
315 |
|
316 lemma psubst_fresh: |
|
317 assumes "x \<in> set (map fst \<theta>)" and "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t" |
|
318 shows "x \<sharp> \<theta>\<lparr>t\<rparr>" and "x \<sharp> \<theta>\<lparr>t'\<rparr>\<^sub>b" using assms |
|
319 apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts) |
|
320 apply simp |
|
321 apply (rule lookup_fresh) |
|
322 apply (rule impI) |
|
323 apply (simp_all add: abs_fresh) |
|
324 done |
|
325 |
|
326 lemma psubst_eqvt[eqvt]: |
|
327 fixes pi :: "name prm" |
|
328 shows "pi \<bullet> (\<theta>\<lparr>t\<rparr>) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t\<rparr>" |
|
329 and "pi \<bullet> (\<theta>\<lparr>t'\<rparr>\<^sub>b) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t'\<rparr>\<^sub>b" |
|
330 by (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts) |
|
331 (simp_all add: eqvts fresh_bij) |
|
332 |
|
333 abbreviation |
|
334 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_\<mapsto>_]" [100,0,0] 100) |
|
335 where |
|
336 "t[x\<mapsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>" |
|
337 |
|
338 abbreviation |
|
339 substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" ("_[_\<mapsto>_]\<^sub>b" [100,0,0] 100) |
|
340 where |
|
341 "t[x\<mapsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b" |
|
342 |
|
343 lemma lookup_forget: |
|
344 "(supp (map fst \<theta>)::name set) \<sharp>* x \<Longrightarrow> lookup \<theta> x = Var x" |
|
345 by (induct \<theta>) (auto simp add: split_paired_all fresh_star_def fresh_atm supp_list_cons supp_atm) |
|
346 |
|
347 lemma supp_fst: "(x::name) \<in> supp (map fst (\<theta>::(name \<times> trm) list)) \<Longrightarrow> x \<in> supp \<theta>" |
|
348 by (induct \<theta>) (auto simp add: supp_list_nil supp_list_cons supp_prod) |
|
349 |
|
350 lemma psubst_forget: |
|
351 "(supp (map fst \<theta>)::name set) \<sharp>* t \<Longrightarrow> \<theta>\<lparr>t\<rparr> = t" |
|
352 "(supp (map fst \<theta>)::name set) \<sharp>* t' \<Longrightarrow> \<theta>\<lparr>t'\<rparr>\<^sub>b = t'" |
|
353 apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts) |
|
354 apply (auto simp add: fresh_star_def lookup_forget abs_fresh) |
|
355 apply (drule_tac x=\<theta> in meta_spec) |
|
356 apply (drule meta_mp) |
|
357 apply (rule ballI) |
|
358 apply (drule_tac x=x in bspec) |
|
359 apply assumption |
|
360 apply (drule supp_fst) |
|
361 apply (auto simp add: fresh_def) |
|
362 apply (drule_tac x=\<theta> in meta_spec) |
|
363 apply (drule meta_mp) |
|
364 apply (rule ballI) |
|
365 apply (drule_tac x=x in bspec) |
|
366 apply assumption |
|
367 apply (drule supp_fst) |
|
368 apply (auto simp add: fresh_def) |
|
369 done |
|
370 |
|
371 lemma psubst_nil: "[]\<lparr>t\<rparr> = t" "[]\<lparr>t'\<rparr>\<^sub>b = t'" |
|
372 by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil) |
|
373 |
|
374 lemma psubst_cons: |
|
375 assumes "(supp (map fst \<theta>)::name set) \<sharp>* u" |
|
376 shows "((x, u) # \<theta>)\<lparr>t\<rparr> = \<theta>\<lparr>t[x\<mapsto>u]\<rparr>" and "((x, u) # \<theta>)\<lparr>t'\<rparr>\<^sub>b = \<theta>\<lparr>t'[x\<mapsto>u]\<^sub>b\<rparr>\<^sub>b" |
|
377 using assms |
|
378 by (nominal_induct t and t' avoiding: x u \<theta> rule: trm_btrm.strong_inducts) |
|
379 (simp_all add: fresh_list_nil fresh_list_cons psubst_forget) |
|
380 |
|
381 lemma psubst_append: |
|
382 "(supp (map fst (\<theta>\<^isub>1 @ \<theta>\<^isub>2))::name set) \<sharp>* map snd (\<theta>\<^isub>1 @ \<theta>\<^isub>2) \<Longrightarrow> (\<theta>\<^isub>1 @ \<theta>\<^isub>2)\<lparr>t\<rparr> = \<theta>\<^isub>2\<lparr>\<theta>\<^isub>1\<lparr>t\<rparr>\<rparr>" |
|
383 by (induct \<theta>\<^isub>1 arbitrary: t) |
|
384 (simp_all add: psubst_nil split_paired_all supp_list_cons psubst_cons fresh_star_def |
|
385 fresh_list_cons fresh_list_append supp_list_append) |
|
386 |
|
387 lemma abs_pat_psubst [simp]: |
|
388 "(supp p::name set) \<sharp>* \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>[p]. t\<rparr>\<^sub>b = (\<lambda>[p]. \<theta>\<lparr>t\<rparr>\<^sub>b)" |
|
389 by (induct p arbitrary: t) (auto simp add: fresh_star_def supp_atm) |
|
390 |
|
391 lemma valid_insert: |
|
392 assumes "valid (\<Delta> @ [(x, T)] @ \<Gamma>)" |
|
393 shows "valid (\<Delta> @ \<Gamma>)" using assms |
|
394 by (induct \<Delta>) |
|
395 (auto simp add: fresh_list_append fresh_list_cons) |
|
396 |
|
397 lemma fresh_set: |
|
398 shows "y \<sharp> xs = (\<forall>x\<in>set xs. y \<sharp> x)" |
|
399 by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons) |
|
400 |
|
401 lemma context_unique: |
|
402 assumes "valid \<Gamma>" |
|
403 and "(x, T) \<in> set \<Gamma>" |
|
404 and "(x, U) \<in> set \<Gamma>" |
|
405 shows "T = U" using assms |
|
406 by induct (auto simp add: fresh_set fresh_prod fresh_atm) |
|
407 |
|
408 lemma subst_type_aux: |
|
409 assumes a: "\<Delta> @ [(x, U)] @ \<Gamma> \<turnstile> t : T" |
|
410 and b: "\<Gamma> \<turnstile> u : U" |
|
411 shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b |
|
412 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct) |
|
413 case (Var \<Gamma>' y T x u \<Delta>) |
|
414 then have a1: "valid (\<Delta> @ [(x, U)] @ \<Gamma>)" |
|
415 and a2: "(y, T) \<in> set (\<Delta> @ [(x, U)] @ \<Gamma>)" |
|
416 and a3: "\<Gamma> \<turnstile> u : U" by simp_all |
|
417 from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert) |
|
418 show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" |
|
419 proof cases |
|
420 assume eq: "x = y" |
|
421 from a1 a2 have "T = U" using eq by (auto intro: context_unique) |
|
422 with a3 show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using eq a4 by (auto intro: weakening) |
|
423 next |
|
424 assume ineq: "x \<noteq> y" |
|
425 from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp |
|
426 then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq a4 by auto |
|
427 qed |
|
428 next |
|
429 case (Tuple \<Gamma>' t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2) |
|
430 from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` |
|
431 have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T\<^isub>1" by (rule Tuple) |
|
432 moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` |
|
433 have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T\<^isub>2" by (rule Tuple) |
|
434 ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^isub>1[x\<mapsto>u], t\<^isub>2[x\<mapsto>u]\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2" .. |
|
435 then show ?case by simp |
|
436 next |
|
437 case (Let p t \<Gamma>' T \<Delta>' s S) |
|
438 from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` |
|
439 have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let) |
|
440 moreover note `\<turnstile> p : T \<Rightarrow> \<Delta>'` |
|
441 moreover from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` |
|
442 have "\<Delta>' @ \<Gamma>' = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp |
|
443 with `\<Gamma> \<turnstile> u : U` have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by (rule Let) |
|
444 then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp |
|
445 ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>u]) : S" |
|
446 by (rule better_T_Let) |
|
447 moreover from Let have "(supp p::name set) \<sharp>* [(x, u)]" |
|
448 by (simp add: fresh_star_def fresh_list_nil fresh_list_cons) |
|
449 ultimately show ?case by simp |
|
450 next |
|
451 case (Abs y T \<Gamma>' t S) |
|
452 from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` have "(y, T) # \<Gamma>' = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>" |
|
453 by simp |
|
454 with `\<Gamma> \<turnstile> u : U` have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by (rule Abs) |
|
455 then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp |
|
456 then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> S" |
|
457 by (rule typing.Abs) |
|
458 moreover from Abs have "y \<sharp> [(x, u)]" |
|
459 by (simp add: fresh_list_nil fresh_list_cons) |
|
460 ultimately show ?case by simp |
|
461 next |
|
462 case (App \<Gamma>' t\<^isub>1 T S t\<^isub>2) |
|
463 from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` |
|
464 have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App) |
|
465 moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` |
|
466 have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T" by (rule App) |
|
467 ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^isub>1[x\<mapsto>u]) \<cdot> (t\<^isub>2[x\<mapsto>u]) : S" |
|
468 by (rule typing.App) |
|
469 then show ?case by simp |
|
470 qed |
|
471 |
|
472 lemmas subst_type = subst_type_aux [of "[]", simplified] |
|
473 |
|
474 lemma match_supp_fst: |
|
475 assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map fst \<theta>)::name set) = supp p" using assms |
|
476 by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append) |
|
477 |
|
478 lemma match_supp_snd: |
|
479 assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map snd \<theta>)::name set) = supp u" using assms |
|
480 by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append trm.supp) |
|
481 |
|
482 lemma match_fresh: "\<turnstile> p \<rhd> u \<Rightarrow> \<theta> \<Longrightarrow> (supp p::name set) \<sharp>* u \<Longrightarrow> |
|
483 (supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>" |
|
484 by (simp add: fresh_star_def fresh_def match_supp_fst match_supp_snd) |
|
485 |
|
486 lemma match_type_aux: |
|
487 assumes "\<turnstile> p : U \<Rightarrow> \<Delta>" |
|
488 and "\<Gamma>\<^isub>2 \<turnstile> u : U" |
|
489 and "\<Gamma>\<^isub>1 @ \<Delta> @ \<Gamma>\<^isub>2 \<turnstile> t : T" |
|
490 and "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" |
|
491 and "(supp p::name set) \<sharp>* u" |
|
492 shows "\<Gamma>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<lparr>t\<rparr> : T" using assms |
|
493 proof (induct arbitrary: \<Gamma>\<^isub>1 \<Gamma>\<^isub>2 t u T \<theta>) |
|
494 case (PVar x U) |
|
495 from `\<Gamma>\<^isub>1 @ [(x, U)] @ \<Gamma>\<^isub>2 \<turnstile> t : T` `\<Gamma>\<^isub>2 \<turnstile> u : U` |
|
496 have "\<Gamma>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> t[x\<mapsto>u] : T" by (rule subst_type_aux) |
|
497 moreover from `\<turnstile> PVar x U \<rhd> u \<Rightarrow> \<theta>` have "\<theta> = [(x, u)]" |
|
498 by cases simp_all |
|
499 ultimately show ?case by simp |
|
500 next |
|
501 case (PTuple p S \<Delta>\<^isub>1 q U \<Delta>\<^isub>2) |
|
502 from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` obtain u\<^isub>1 u\<^isub>2 \<theta>\<^isub>1 \<theta>\<^isub>2 |
|
503 where u: "u = \<langle>u\<^isub>1, u\<^isub>2\<rangle>" and \<theta>: "\<theta> = \<theta>\<^isub>1 @ \<theta>\<^isub>2" |
|
504 and p: "\<turnstile> p \<rhd> u\<^isub>1 \<Rightarrow> \<theta>\<^isub>1" and q: "\<turnstile> q \<rhd> u\<^isub>2 \<Rightarrow> \<theta>\<^isub>2" |
|
505 by cases simp_all |
|
506 with PTuple have "\<Gamma>\<^isub>2 \<turnstile> \<langle>u\<^isub>1, u\<^isub>2\<rangle> : S \<otimes> U" by simp |
|
507 then obtain u\<^isub>1: "\<Gamma>\<^isub>2 \<turnstile> u\<^isub>1 : S" and u\<^isub>2: "\<Gamma>\<^isub>2 \<turnstile> u\<^isub>2 : U" |
|
508 by cases (simp_all add: ty.inject trm.inject) |
|
509 note u\<^isub>1 |
|
510 moreover from `\<Gamma>\<^isub>1 @ (\<Delta>\<^isub>2 @ \<Delta>\<^isub>1) @ \<Gamma>\<^isub>2 \<turnstile> t : T` |
|
511 have "(\<Gamma>\<^isub>1 @ \<Delta>\<^isub>2) @ \<Delta>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> t : T" by simp |
|
512 moreover note p |
|
513 moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u |
|
514 have "(supp p::name set) \<sharp>* u\<^isub>1" by (simp add: fresh_star_def) |
|
515 ultimately have \<theta>\<^isub>1: "(\<Gamma>\<^isub>1 @ \<Delta>\<^isub>2) @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<^isub>1\<lparr>t\<rparr> : T" |
|
516 by (rule PTuple) |
|
517 note u\<^isub>2 |
|
518 moreover from \<theta>\<^isub>1 |
|
519 have "\<Gamma>\<^isub>1 @ \<Delta>\<^isub>2 @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<^isub>1\<lparr>t\<rparr> : T" by simp |
|
520 moreover note q |
|
521 moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u |
|
522 have "(supp q::name set) \<sharp>* u\<^isub>2" by (simp add: fresh_star_def) |
|
523 ultimately have "\<Gamma>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<^isub>2\<lparr>\<theta>\<^isub>1\<lparr>t\<rparr>\<rparr> : T" |
|
524 by (rule PTuple) |
|
525 moreover from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` |
|
526 have "(supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>" |
|
527 by (rule match_fresh) |
|
528 ultimately show ?case using \<theta> by (simp add: psubst_append) |
|
529 qed |
|
530 |
|
531 lemmas match_type = match_type_aux [where \<Gamma>\<^isub>1="[]", simplified] |
|
532 |
|
533 inductive eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60) |
|
534 where |
|
535 TupleL: "t \<longmapsto> t' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t', u\<rangle>" |
|
536 | TupleR: "u \<longmapsto> u' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t, u'\<rangle>" |
|
537 | Abs: "t \<longmapsto> t' \<Longrightarrow> (\<lambda>x:T. t) \<longmapsto> (\<lambda>x:T. t')" |
|
538 | AppL: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u" |
|
539 | AppR: "u \<longmapsto> u' \<Longrightarrow> t \<cdot> u \<longmapsto> t \<cdot> u'" |
|
540 | Beta: "x \<sharp> u \<Longrightarrow> (\<lambda>x:T. t) \<cdot> u \<longmapsto> t[x\<mapsto>u]" |
|
541 | Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow> distinct (pat_vars p) \<Longrightarrow> |
|
542 \<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> (LET p = t IN u) \<longmapsto> \<theta>\<lparr>u\<rparr>" |
|
543 |
|
544 equivariance match |
|
545 |
|
546 equivariance eval |
|
547 |
|
548 lemma match_vars: |
|
549 assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "x \<in> supp p" |
|
550 shows "x \<in> set (map fst \<theta>)" using assms |
|
551 by induct (auto simp add: supp_atm) |
|
552 |
|
553 lemma match_fresh_mono: |
|
554 assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "(x::name) \<sharp> t" |
|
555 shows "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t" using assms |
|
556 by induct auto |
|
557 |
|
558 nominal_inductive2 eval |
|
559 avoids |
|
560 Abs: "{x}" |
|
561 | Beta: "{x}" |
|
562 | Let: "(supp p)::name set" |
|
563 apply (simp_all add: fresh_star_def abs_fresh fin_supp) |
|
564 apply (rule psubst_fresh) |
|
565 apply simp |
|
566 apply simp |
|
567 apply (rule ballI) |
|
568 apply (rule psubst_fresh) |
|
569 apply (rule match_vars) |
|
570 apply assumption+ |
|
571 apply (rule match_fresh_mono) |
|
572 apply auto |
|
573 done |
|
574 |
|
575 lemma typing_case_Abs: |
|
576 assumes ty: "\<Gamma> \<turnstile> (\<lambda>x:T. t) : S" |
|
577 and fresh: "x \<sharp> \<Gamma>" |
|
578 and R: "\<And>U. S = T \<rightarrow> U \<Longrightarrow> (x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> P" |
|
579 shows P using ty |
|
580 proof cases |
|
581 case (Abs x' T' \<Gamma>' t' U) |
|
582 obtain y::name where y: "y \<sharp> (x, \<Gamma>, \<lambda>x':T'. t')" |
|
583 by (rule exists_fresh) (auto intro: fin_supp) |
|
584 from `(\<lambda>x:T. t) = (\<lambda>x':T'. t')` [symmetric] |
|
585 have x: "x \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh) |
|
586 have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh) |
|
587 from `(x', T') # \<Gamma>' \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>'" |
|
588 by (auto dest: valid_typing) |
|
589 have "(\<lambda>x:T. t) = (\<lambda>x':T'. t')" by fact |
|
590 also from x x' y have "\<dots> = [(x, y)] \<bullet> [(x', y)] \<bullet> (\<lambda>x':T'. t')" |
|
591 by (simp only: perm_fresh_fresh fresh_prod) |
|
592 also have "\<dots> = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')" |
|
593 by (simp add: swap_simps perm_fresh_fresh) |
|
594 finally have "(\<lambda>x:T. t) = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')" . |
|
595 then have T: "T = T'" and t: "[(x, y)] \<bullet> [(x', y)] \<bullet> t' = t" |
|
596 by (simp_all add: trm.inject alpha) |
|
597 from Abs T have "S = T \<rightarrow> U" by simp |
|
598 moreover from `(x', T') # \<Gamma>' \<turnstile> t' : U` |
|
599 have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma>' \<turnstile> t' : U)" |
|
600 by (simp add: perm_bool) |
|
601 with T t y `\<Gamma> = \<Gamma>'` x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U" |
|
602 by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod) |
|
603 ultimately show ?thesis by (rule R) |
|
604 qed simp_all |
|
605 |
|
606 nominal_primrec ty_size :: "ty \<Rightarrow> nat" |
|
607 where |
|
608 "ty_size (Atom n) = 0" |
|
609 | "ty_size (T \<rightarrow> U) = ty_size T + ty_size U + 1" |
|
610 | "ty_size (T \<otimes> U) = ty_size T + ty_size U + 1" |
|
611 by (rule TrueI)+ |
|
612 |
|
613 lemma bind_tuple_ineq: |
|
614 "ty_size (pat_type p) < ty_size U \<Longrightarrow> Bind U x t \<noteq> (\<lambda>[p]. u)" |
|
615 by (induct p arbitrary: U x t u) (auto simp add: btrm.inject) |
|
616 |
|
617 lemma valid_appD: assumes "valid (\<Gamma> @ \<Delta>)" |
|
618 shows "valid \<Gamma>" "valid \<Delta>" using assms |
|
619 by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>) |
|
620 (auto simp add: Cons_eq_append_conv fresh_list_append) |
|
621 |
|
622 lemma valid_app_freshs: assumes "valid (\<Gamma> @ \<Delta>)" |
|
623 shows "(supp \<Gamma>::name set) \<sharp>* \<Delta>" "(supp \<Delta>::name set) \<sharp>* \<Gamma>" using assms |
|
624 by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>) |
|
625 (auto simp add: Cons_eq_append_conv fresh_star_def |
|
626 fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append |
|
627 supp_prod fresh_prod supp_atm fresh_atm |
|
628 dest: notE [OF iffD1 [OF fresh_def [THEN meta_eq_to_obj_eq]]]) |
|
629 |
|
630 lemma perm_mem_left: "(x::name) \<in> ((pi::name prm) \<bullet> A) \<Longrightarrow> (rev pi \<bullet> x) \<in> A" |
|
631 by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp) |
|
632 |
|
633 lemma perm_mem_right: "(rev (pi::name prm) \<bullet> (x::name)) \<in> A \<Longrightarrow> x \<in> (pi \<bullet> A)" |
|
634 by (drule perm_boolI [of _ pi]) (simp add: eqvts perm_pi_simp) |
|
635 |
|
636 lemma perm_cases: |
|
637 assumes pi: "set pi \<subseteq> A \<times> A" |
|
638 shows "((pi::name prm) \<bullet> B) \<subseteq> A \<union> B" |
|
639 proof |
|
640 fix x assume "x \<in> pi \<bullet> B" |
|
641 then show "x \<in> A \<union> B" using pi |
|
642 apply (induct pi arbitrary: x B rule: rev_induct) |
|
643 apply simp |
|
644 apply (simp add: split_paired_all supp_eqvt) |
|
645 apply (drule perm_mem_left) |
|
646 apply (simp add: calc_atm split: split_if_asm) |
|
647 apply (auto dest: perm_mem_right) |
|
648 done |
|
649 qed |
|
650 |
|
651 lemma abs_pat_alpha': |
|
652 assumes eq: "(\<lambda>[p]. t) = (\<lambda>[q]. u)" |
|
653 and ty: "pat_type p = pat_type q" |
|
654 and pv: "distinct (pat_vars p)" |
|
655 and qv: "distinct (pat_vars q)" |
|
656 shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and> |
|
657 set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)" |
|
658 using assms |
|
659 proof (induct p arbitrary: q t u \<Delta>) |
|
660 case (PVar x T) |
|
661 note PVar' = this |
|
662 show ?case |
|
663 proof (cases q) |
|
664 case (PVar x' T') |
|
665 with `(\<lambda>[PVar x T]. t) = (\<lambda>[q]. u)` |
|
666 have "x = x' \<and> t = u \<or> x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u" |
|
667 by (simp add: btrm.inject alpha) |
|
668 then show ?thesis |
|
669 proof |
|
670 assume "x = x' \<and> t = u" |
|
671 with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and> |
|
672 t = ([]::name prm) \<bullet> u \<and> |
|
673 set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times> |
|
674 (supp (PVar x T) \<union> supp q)" by simp |
|
675 then show ?thesis .. |
|
676 next |
|
677 assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u" |
|
678 with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and> |
|
679 t = [(x, x')] \<bullet> u \<and> |
|
680 set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times> |
|
681 (supp (PVar x T) \<union> supp q)" |
|
682 by (simp add: perm_swap swap_simps supp_atm perm_type) |
|
683 then show ?thesis .. |
|
684 qed |
|
685 next |
|
686 case (PTuple p\<^isub>1 p\<^isub>2) |
|
687 with PVar have "ty_size (pat_type p\<^isub>1) < ty_size T" by simp |
|
688 then have "Bind T x t \<noteq> (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. u)" |
|
689 by (rule bind_tuple_ineq) |
|
690 moreover from PTuple PVar |
|
691 have "Bind T x t = (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. u)" by simp |
|
692 ultimately show ?thesis .. |
|
693 qed |
|
694 next |
|
695 case (PTuple p\<^isub>1 p\<^isub>2) |
|
696 note PTuple' = this |
|
697 show ?case |
|
698 proof (cases q) |
|
699 case (PVar x T) |
|
700 with PTuple have "ty_size (pat_type p\<^isub>1) < ty_size T" by auto |
|
701 then have "Bind T x u \<noteq> (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. t)" |
|
702 by (rule bind_tuple_ineq) |
|
703 moreover from PTuple PVar |
|
704 have "Bind T x u = (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. t)" by simp |
|
705 ultimately show ?thesis .. |
|
706 next |
|
707 case (PTuple p\<^isub>1' p\<^isub>2') |
|
708 with PTuple' have "(\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. t) = (\<lambda>[p\<^isub>1']. \<lambda>[p\<^isub>2']. u)" by simp |
|
709 moreover from PTuple PTuple' have "pat_type p\<^isub>1 = pat_type p\<^isub>1'" |
|
710 by (simp add: ty.inject) |
|
711 moreover from PTuple' have "distinct (pat_vars p\<^isub>1)" by simp |
|
712 moreover from PTuple PTuple' have "distinct (pat_vars p\<^isub>1')" by simp |
|
713 ultimately have "\<exists>pi::name prm. p\<^isub>1 = pi \<bullet> p\<^isub>1' \<and> |
|
714 (\<lambda>[p\<^isub>2]. t) = pi \<bullet> (\<lambda>[p\<^isub>2']. u) \<and> |
|
715 set pi \<subseteq> (supp p\<^isub>1 \<union> supp p\<^isub>1') \<times> (supp p\<^isub>1 \<union> supp p\<^isub>1')" |
|
716 by (rule PTuple') |
|
717 then obtain pi::"name prm" where |
|
718 "p\<^isub>1 = pi \<bullet> p\<^isub>1'" "(\<lambda>[p\<^isub>2]. t) = pi \<bullet> (\<lambda>[p\<^isub>2']. u)" and |
|
719 pi: "set pi \<subseteq> (supp p\<^isub>1 \<union> supp p\<^isub>1') \<times> (supp p\<^isub>1 \<union> supp p\<^isub>1')" by auto |
|
720 from `(\<lambda>[p\<^isub>2]. t) = pi \<bullet> (\<lambda>[p\<^isub>2']. u)` |
|
721 have "(\<lambda>[p\<^isub>2]. t) = (\<lambda>[pi \<bullet> p\<^isub>2']. pi \<bullet> u)" |
|
722 by (simp add: eqvts) |
|
723 moreover from PTuple PTuple' have "pat_type p\<^isub>2 = pat_type (pi \<bullet> p\<^isub>2')" |
|
724 by (simp add: ty.inject pat_type_perm_eq) |
|
725 moreover from PTuple' have "distinct (pat_vars p\<^isub>2)" by simp |
|
726 moreover from PTuple PTuple' have "distinct (pat_vars (pi \<bullet> p\<^isub>2'))" |
|
727 by (simp add: pat_vars_eqvt [symmetric] distinct_eqvt [symmetric]) |
|
728 ultimately have "\<exists>pi'::name prm. p\<^isub>2 = pi' \<bullet> pi \<bullet> p\<^isub>2' \<and> |
|
729 t = pi' \<bullet> pi \<bullet> u \<and> |
|
730 set pi' \<subseteq> (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2')) \<times> (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2'))" |
|
731 by (rule PTuple') |
|
732 then obtain pi'::"name prm" where |
|
733 "p\<^isub>2 = pi' \<bullet> pi \<bullet> p\<^isub>2'" "t = pi' \<bullet> pi \<bullet> u" and |
|
734 pi': "set pi' \<subseteq> (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2')) \<times> |
|
735 (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2'))" by auto |
|
736 from PTuple PTuple' have "pi \<bullet> distinct (pat_vars \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>)" by simp |
|
737 then have "distinct (pat_vars \<langle>\<langle>pi \<bullet> p\<^isub>1', pi \<bullet> p\<^isub>2'\<rangle>\<rangle>)" by (simp only: eqvts) |
|
738 with `p\<^isub>1 = pi \<bullet> p\<^isub>1'` PTuple' |
|
739 have fresh: "(supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2') :: name set) \<sharp>* p\<^isub>1" |
|
740 by (auto simp add: set_pat_vars_supp fresh_star_def fresh_def eqvts) |
|
741 from `p\<^isub>1 = pi \<bullet> p\<^isub>1'` have "pi' \<bullet> (p\<^isub>1 = pi \<bullet> p\<^isub>1')" by (rule perm_boolI) |
|
742 with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh fresh] |
|
743 have "p\<^isub>1 = pi' \<bullet> pi \<bullet> p\<^isub>1'" by (simp add: eqvts) |
|
744 with `p\<^isub>2 = pi' \<bullet> pi \<bullet> p\<^isub>2'` have "\<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>" |
|
745 by (simp add: pt_name2) |
|
746 moreover |
|
747 have "((supp p\<^isub>2 \<union> (pi \<bullet> supp p\<^isub>2')) \<times> (supp p\<^isub>2 \<union> (pi \<bullet> supp p\<^isub>2'))::(name \<times> name) set) \<subseteq> |
|
748 (supp p\<^isub>2 \<union> (supp p\<^isub>1 \<union> supp p\<^isub>1' \<union> supp p\<^isub>2')) \<times> (supp p\<^isub>2 \<union> (supp p\<^isub>1 \<union> supp p\<^isub>1' \<union> supp p\<^isub>2'))" |
|
749 by (rule subset_refl Sigma_mono Un_mono perm_cases [OF pi])+ |
|
750 with pi' have "set pi' \<subseteq> \<dots>" by (simp add: supp_eqvt [symmetric]) |
|
751 with pi have "set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>) \<times> |
|
752 (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>)" |
|
753 by (simp add: Sigma_Un_distrib1 Sigma_Un_distrib2 Un_ac) blast |
|
754 moreover note `t = pi' \<bullet> pi \<bullet> u` |
|
755 ultimately have "\<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> q \<and> t = (pi' @ pi) \<bullet> u \<and> |
|
756 set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp q) \<times> |
|
757 (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp q)" using PTuple |
|
758 by (simp add: pt_name2) |
|
759 then show ?thesis .. |
|
760 qed |
|
761 qed |
|
762 |
|
763 lemma typing_case_Let: |
|
764 assumes ty: "\<Gamma> \<turnstile> (LET p = t IN u) : U" |
|
765 and fresh: "(supp p::name set) \<sharp>* \<Gamma>" |
|
766 and distinct: "distinct (pat_vars p)" |
|
767 and R: "\<And>T \<Delta>. \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> P" |
|
768 shows P using ty |
|
769 proof cases |
|
770 case (Let p' t' \<Gamma>' T \<Delta> u' U') |
|
771 then have "(supp \<Delta>::name set) \<sharp>* \<Gamma>" |
|
772 by (auto intro: valid_typing valid_app_freshs) |
|
773 with Let have "(supp p'::name set) \<sharp>* \<Gamma>" |
|
774 by (simp add: pat_var) |
|
775 with fresh have fresh': "(supp p \<union> supp p' :: name set) \<sharp>* \<Gamma>" |
|
776 by (auto simp add: fresh_star_def) |
|
777 from Let have "(\<lambda>[p]. Base u) = (\<lambda>[p']. Base u')" |
|
778 by (simp add: trm.inject) |
|
779 moreover from Let have "pat_type p = pat_type p'" |
|
780 by (simp add: trm.inject) |
|
781 moreover note distinct |
|
782 moreover from `\<Delta> @ \<Gamma>' \<turnstile> u' : U'` have "valid (\<Delta> @ \<Gamma>')" |
|
783 by (rule valid_typing) |
|
784 then have "valid \<Delta>" by (rule valid_appD) |
|
785 with `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "distinct (pat_vars p')" |
|
786 by (simp add: valid_distinct pat_vars_ptyping) |
|
787 ultimately have "\<exists>pi::name prm. p = pi \<bullet> p' \<and> Base u = pi \<bullet> Base u' \<and> |
|
788 set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')" |
|
789 by (rule abs_pat_alpha') |
|
790 then obtain pi::"name prm" where pi: "p = pi \<bullet> p'" "u = pi \<bullet> u'" |
|
791 and pi': "set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')" |
|
792 by (auto simp add: btrm.inject) |
|
793 from Let have "\<Gamma> \<turnstile> t : T" by (simp add: trm.inject) |
|
794 moreover from `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "\<turnstile> (pi \<bullet> p') : (pi \<bullet> T) \<Rightarrow> (pi \<bullet> \<Delta>)" |
|
795 by (simp add: ptyping.eqvt) |
|
796 with pi have "\<turnstile> p : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: perm_type) |
|
797 moreover from Let |
|
798 have "(pi \<bullet> \<Delta>) @ (pi \<bullet> \<Gamma>) \<turnstile> (pi \<bullet> u') : (pi \<bullet> U)" |
|
799 by (simp add: append_eqvt [symmetric] typing.eqvt) |
|
800 with pi have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> u : U" |
|
801 by (simp add: perm_type pt_freshs_freshs |
|
802 [OF pt_name_inst at_name_inst pi' fresh' fresh']) |
|
803 ultimately show ?thesis by (rule R) |
|
804 qed simp_all |
|
805 |
|
806 lemma preservation: |
|
807 assumes "t \<longmapsto> t'" and "\<Gamma> \<turnstile> t : T" |
|
808 shows "\<Gamma> \<turnstile> t' : T" using assms |
|
809 proof (nominal_induct avoiding: \<Gamma> T rule: eval.strong_induct) |
|
810 case (TupleL t t' u) |
|
811 from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^isub>1 T\<^isub>2 |
|
812 where "T = T\<^isub>1 \<otimes> T\<^isub>2" "\<Gamma> \<turnstile> t : T\<^isub>1" "\<Gamma> \<turnstile> u : T\<^isub>2" |
|
813 by cases (simp_all add: trm.inject) |
|
814 from `\<Gamma> \<turnstile> t : T\<^isub>1` have "\<Gamma> \<turnstile> t' : T\<^isub>1" by (rule TupleL) |
|
815 then have "\<Gamma> \<turnstile> \<langle>t', u\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2" using `\<Gamma> \<turnstile> u : T\<^isub>2` |
|
816 by (rule Tuple) |
|
817 with `T = T\<^isub>1 \<otimes> T\<^isub>2` show ?case by simp |
|
818 next |
|
819 case (TupleR u u' t) |
|
820 from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^isub>1 T\<^isub>2 |
|
821 where "T = T\<^isub>1 \<otimes> T\<^isub>2" "\<Gamma> \<turnstile> t : T\<^isub>1" "\<Gamma> \<turnstile> u : T\<^isub>2" |
|
822 by cases (simp_all add: trm.inject) |
|
823 from `\<Gamma> \<turnstile> u : T\<^isub>2` have "\<Gamma> \<turnstile> u' : T\<^isub>2" by (rule TupleR) |
|
824 with `\<Gamma> \<turnstile> t : T\<^isub>1` have "\<Gamma> \<turnstile> \<langle>t, u'\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2" |
|
825 by (rule Tuple) |
|
826 with `T = T\<^isub>1 \<otimes> T\<^isub>2` show ?case by simp |
|
827 next |
|
828 case (Abs t t' x S) |
|
829 from `\<Gamma> \<turnstile> (\<lambda>x:S. t) : T` `x \<sharp> \<Gamma>` obtain U where |
|
830 T: "T = S \<rightarrow> U" and U: "(x, S) # \<Gamma> \<turnstile> t : U" |
|
831 by (rule typing_case_Abs) |
|
832 from U have "(x, S) # \<Gamma> \<turnstile> t' : U" by (rule Abs) |
|
833 then have "\<Gamma> \<turnstile> (\<lambda>x:S. t') : S \<rightarrow> U" |
|
834 by (rule typing.Abs) |
|
835 with T show ?case by simp |
|
836 next |
|
837 case (Beta x u S t) |
|
838 from `\<Gamma> \<turnstile> (\<lambda>x:S. t) \<cdot> u : T` `x \<sharp> \<Gamma>` |
|
839 obtain "(x, S) # \<Gamma> \<turnstile> t : T" and "\<Gamma> \<turnstile> u : S" |
|
840 by cases (auto simp add: trm.inject ty.inject elim: typing_case_Abs) |
|
841 then show ?case by (rule subst_type) |
|
842 next |
|
843 case (Let p t \<theta> u) |
|
844 from `\<Gamma> \<turnstile> (LET p = t IN u) : T` `supp p \<sharp>* \<Gamma>` `distinct (pat_vars p)` |
|
845 obtain U \<Delta> where "\<turnstile> p : U \<Rightarrow> \<Delta>" "\<Gamma> \<turnstile> t : U" "\<Delta> @ \<Gamma> \<turnstile> u : T" |
|
846 by (rule typing_case_Let) |
|
847 then show ?case using `\<turnstile> p \<rhd> t \<Rightarrow> \<theta>` `supp p \<sharp>* t` |
|
848 by (rule match_type) |
|
849 next |
|
850 case (AppL t t' u) |
|
851 from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where |
|
852 t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U" |
|
853 by cases (auto simp add: trm.inject) |
|
854 from t have "\<Gamma> \<turnstile> t' : U \<rightarrow> T" by (rule AppL) |
|
855 then show ?case using u by (rule typing.App) |
|
856 next |
|
857 case (AppR u u' t) |
|
858 from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where |
|
859 t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U" |
|
860 by cases (auto simp add: trm.inject) |
|
861 from u have "\<Gamma> \<turnstile> u' : U" by (rule AppR) |
|
862 with t show ?case by (rule typing.App) |
|
863 qed |
|
864 |
|
865 end |