18 equivariance triv |
18 equivariance triv |
19 nominal_inductive triv avoids Var : "{}::name set" |
19 nominal_inductive triv avoids Var : "{}::name set" |
20 apply(auto simp add: fresh_star_def) |
20 apply(auto simp add: fresh_star_def) |
21 done |
21 done |
22 |
22 |
|
23 lemma Abs1_eq_fdest: |
|
24 fixes x y :: "'a :: at_base" |
|
25 and S T :: "'b :: fs" |
|
26 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
|
27 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T" |
|
28 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T" |
|
29 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S" |
|
30 and "sort_of (atom x) = sort_of (atom y)" |
|
31 shows "f x T = f y S" |
|
32 using assms apply - |
|
33 apply (subst (asm) Abs1_eq_iff') |
|
34 apply simp_all |
|
35 apply (elim conjE disjE) |
|
36 apply simp |
|
37 apply(rule trans) |
|
38 apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric]) |
|
39 apply(rule fresh_star_supp_conv) |
|
40 apply(simp add: supp_swap fresh_star_def) |
|
41 apply(simp add: swap_commute) |
|
42 done |
23 |
43 |
24 text {* height function *} |
44 text {* height function *} |
25 |
45 |
26 nominal_primrec |
46 nominal_primrec |
27 height :: "lam \<Rightarrow> int" |
47 height :: "lam \<Rightarrow> int" |
30 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
50 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
31 | "height (Lam [x].t) = height t + 1" |
51 | "height (Lam [x].t) = height t + 1" |
32 defer |
52 defer |
33 apply(rule_tac y="x" in lam.exhaust) |
53 apply(rule_tac y="x" in lam.exhaust) |
34 apply(auto simp add: lam.distinct lam.eq_iff) |
54 apply(auto simp add: lam.distinct lam.eq_iff) |
35 apply(simp add: Abs_eq_iff alphas) |
55 apply (erule Abs1_eq_fdest) |
36 apply(clarify) |
56 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
37 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
|
38 apply(simp add: pure_supp fresh_star_def) |
|
39 apply(simp add: eqvt_at_def) |
|
40 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
57 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
41 unfolding eqvt_def |
58 unfolding eqvt_def |
42 apply(rule allI) |
59 apply(rule allI) |
43 apply(simp add: permute_fun_def) |
60 apply(simp add: permute_fun_def) |
44 apply(rule ext) |
61 apply(rule ext) |
80 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
97 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
81 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
98 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
82 defer |
99 defer |
83 apply(rule_tac y="x" in lam.exhaust) |
100 apply(rule_tac y="x" in lam.exhaust) |
84 apply(simp_all)[3] |
101 apply(simp_all)[3] |
85 apply(simp_all only: lam.distinct) |
102 apply(simp_all add: lam.distinct lam.eq_iff) |
86 apply(simp add: lam.eq_iff) |
103 apply (erule Abs1_eq_fdest) |
87 apply(simp add: lam.eq_iff) |
104 apply(simp add: supp_removeAll fresh_def) |
88 apply(simp add: lam.eq_iff) |
|
89 apply(simp add: Abs_eq_iff) |
|
90 apply(erule exE) |
|
91 apply(simp add: alphas) |
|
92 apply(simp add: atom_eqvt) |
|
93 apply(clarify) |
|
94 apply(rule trans) |
|
95 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
96 apply(simp (no_asm) add: supp_removeAll) |
|
97 apply(drule supp_eqvt_at) |
105 apply(drule supp_eqvt_at) |
98 apply(simp add: finite_supp) |
106 apply(simp add: finite_supp) |
99 apply(auto simp add: fresh_star_def)[1] |
107 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
100 unfolding eqvt_at_def |
|
101 apply(simp only: removeAll_eqvt atom_eqvt) |
|
102 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") |
108 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") |
103 unfolding eqvt_def |
109 unfolding eqvt_def |
104 apply(rule allI) |
110 apply(rule allI) |
105 apply(simp add: permute_fun_def) |
111 apply(simp add: permute_fun_def) |
106 apply(rule ext) |
112 apply(rule ext) |
149 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
155 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
150 defer |
156 defer |
151 apply(auto simp add: lam.distinct lam.eq_iff) |
157 apply(auto simp add: lam.distinct lam.eq_iff) |
152 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
158 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
153 apply(blast)+ |
159 apply(blast)+ |
154 apply(simp add: fresh_star_def) |
160 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
155 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
161 apply (erule Abs1_eq_fdest) |
156 apply(subst (asm) Abs_eq_iff2) |
162 apply(simp_all add: Abs_fresh_iff) |
157 apply(simp add: alphas atom_eqvt) |
163 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
158 apply(clarify) |
164 apply(simp_all add: finite_supp fresh_Pair) |
159 apply(rule trans) |
165 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
160 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
166 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
161 apply(rule fresh_star_supp_conv) |
167 apply(simp add: eqvt_at_def) |
162 apply(drule fresh_star_perm_set_conv) |
168 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ |
163 apply(simp add: finite_supp) |
|
164 apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))") |
|
165 apply(auto simp add: fresh_star_def)[1] |
|
166 apply(simp (no_asm) add: fresh_star_def) |
|
167 apply(rule conjI) |
|
168 apply(simp (no_asm) add: Abs_fresh_iff) |
|
169 apply(clarify) |
|
170 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
171 apply(simp add: finite_supp) |
|
172 apply(simp (no_asm_use) add: fresh_Pair) |
|
173 apply(simp add: Abs_fresh_iff) |
|
174 apply(simp) |
|
175 apply(simp add: Abs_fresh_iff) |
|
176 apply(subgoal_tac "p \<bullet> ya = ya") |
|
177 apply(subgoal_tac "p \<bullet> sa = sa") |
|
178 apply(simp add: atom_eqvt eqvt_at_def) |
|
179 apply(rule perm_supp_eq) |
|
180 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
181 apply(rule perm_supp_eq) |
|
182 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
183 apply(simp add: Abs_fresh_iff) |
|
184 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
169 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
185 unfolding eqvt_def |
170 unfolding eqvt_def |
186 apply(rule allI) |
171 apply(rule allI) |
187 apply(simp add: permute_fun_def) |
172 apply(simp add: permute_fun_def) |
188 apply(rule ext) |
173 apply(rule ext) |
254 using a |
239 using a |
255 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct) |
240 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct) |
256 apply (auto simp add: lam.fresh fresh_at_base) |
241 apply (auto simp add: lam.fresh fresh_at_base) |
257 done |
242 done |
258 |
243 |
|
244 lemma height_ge_one: |
|
245 shows "1 \<le> (height e)" |
|
246 by (induct e rule: lam.induct) (simp_all) |
|
247 |
|
248 theorem height_subst: |
|
249 shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')" |
|
250 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) |
|
251 case (Var y) |
|
252 have "1 \<le> height e'" by (rule height_ge_one) |
|
253 then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp |
|
254 next |
|
255 case (Lam y e1) |
|
256 hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp |
|
257 moreover |
|
258 have vc: "atom y\<sharp>x" "atom y\<sharp>e'" by fact+ (* usual variable convention *) |
|
259 ultimately show "height ((Lam [y]. e1)[x::=e']) \<le> height (Lam [y]. e1) - 1 + height e'" by simp |
|
260 next |
|
261 case (App e1 e2) |
|
262 hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" |
|
263 and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all |
|
264 then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp |
|
265 qed |
259 |
266 |
260 subsection {* single-step beta-reduction *} |
267 subsection {* single-step beta-reduction *} |
261 |
268 |
262 inductive |
269 inductive |
263 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
270 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
330 "lookup [] n x = LNVar x" |
337 "lookup [] n x = LNVar x" |
331 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
338 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
332 |
339 |
333 lemma [eqvt]: |
340 lemma [eqvt]: |
334 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
341 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
335 apply(induct xs arbitrary: n) |
342 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
336 apply(simp_all add: permute_pure) |
|
337 done |
|
338 |
343 |
339 nominal_primrec |
344 nominal_primrec |
340 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
345 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
341 where |
346 where |
342 "trans (Var x) xs = lookup xs 0 x" |
347 "trans (Var x) xs = lookup xs 0 x" |
347 apply(simp) |
352 apply(simp) |
348 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
353 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
349 apply(simp_all add: fresh_star_def)[3] |
354 apply(simp_all add: fresh_star_def)[3] |
350 apply(blast) |
355 apply(blast) |
351 apply(blast) |
356 apply(blast) |
352 apply(simp_all add: lam.distinct) |
357 apply(simp_all add: lam.distinct lam.eq_iff) |
353 apply(simp add: lam.eq_iff) |
358 apply(elim conjE) |
354 apply(simp add: lam.eq_iff) |
359 apply clarify |
355 apply(simp add: lam.eq_iff) |
360 apply (erule Abs1_eq_fdest) |
356 apply(erule conjE) |
361 apply (simp_all add: ln.fresh) |
357 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
|
358 prefer 2 |
362 prefer 2 |
359 apply(simp add: Abs_fresh_iff) |
363 apply(drule supp_eqvt_at) |
360 apply(subst (asm) Abs_eq_iff2) |
364 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
361 apply(auto) |
|
362 apply(simp add: alphas) |
|
363 apply(simp add: atom_eqvt) |
|
364 apply(clarify) |
|
365 apply(rule trans) |
|
366 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
367 prefer 2 |
365 prefer 2 |
368 apply (subgoal_tac "p \<bullet> xsa = xsa") |
366 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
369 apply (simp add: eqvt_at_def) |
367 apply (simp add: eqvt_at_def) |
370 apply (rule supp_perm_eq) |
368 apply (metis atom_name_def swap_fresh_fresh) |
371 apply (rule fresh_star_supp_conv) |
|
372 apply (subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* xsa") |
|
373 apply (simp add: fresh_star_def fresh_def) |
|
374 apply blast |
|
375 apply (simp add: fresh_star_def fresh_def) |
|
376 apply (simp add: ln.supp) |
|
377 apply(rule fresh_star_supp_conv) |
|
378 apply (subst (asm) supp_perm_pair) |
|
379 apply (elim disjE) |
|
380 apply (simp add: fresh_star_def supp_zero_perm) |
|
381 apply (simp add: flip_def[symmetric]) |
|
382 apply(subgoal_tac "supp (x \<leftrightarrow> p \<bullet> x) \<sharp>* trans_sumC (t, x # xsa)") |
|
383 apply simp |
|
384 apply (subst flip_def) |
|
385 apply (simp add: supp_swap) |
|
386 apply (simp add: fresh_star_def) |
|
387 apply (rule) |
|
388 apply rule |
|
389 prefer 2 |
|
390 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
391 apply(simp add: finite_supp) |
|
392 apply(simp (no_asm_use) add: fresh_Pair) |
|
393 apply(simp add: Abs_fresh_iff fresh_Cons)[1] |
|
394 apply (metis Rep_name_inverse atom_name_def fresh_at_base) |
|
395 apply assumption |
|
396 oops |
369 oops |
397 |
370 |
398 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
371 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
399 apply (case_tac "x = xa") |
372 apply (case_tac "x = xa") |
400 apply simp |
373 apply simp |