28 | Var3: "triv2 (Var x) n" |
28 | Var3: "triv2 (Var x) n" |
29 |
29 |
30 equivariance triv2 |
30 equivariance triv2 |
31 nominal_inductive triv2 . |
31 nominal_inductive triv2 . |
32 |
32 |
|
33 lemma Abs1_eq_fdest: |
|
34 fixes x y :: "'a :: at_base" |
|
35 and S T :: "'b :: fs" |
|
36 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
|
37 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T" |
|
38 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T" |
|
39 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" |
|
40 and "sort_of (atom x) = sort_of (atom y)" |
|
41 shows "f x T = f y S" |
|
42 using assms apply - |
|
43 apply (subst (asm) Abs1_eq_iff') |
|
44 apply simp_all |
|
45 apply (elim conjE disjE) |
|
46 apply simp |
|
47 apply(rule trans) |
|
48 apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric]) |
|
49 apply(rule fresh_star_supp_conv) |
|
50 apply(simp add: supp_swap fresh_star_def) |
|
51 apply(simp add: swap_commute) |
|
52 done |
33 |
53 |
34 text {* height function *} |
54 text {* height function *} |
35 |
55 |
36 nominal_primrec |
56 nominal_primrec |
37 height :: "lam \<Rightarrow> int" |
57 height :: "lam \<Rightarrow> int" |
40 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
60 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
41 | "height (Lam [x].t) = height t + 1" |
61 | "height (Lam [x].t) = height t + 1" |
42 defer |
62 defer |
43 apply(rule_tac y="x" in lam.exhaust) |
63 apply(rule_tac y="x" in lam.exhaust) |
44 apply(auto simp add: lam.distinct lam.eq_iff) |
64 apply(auto simp add: lam.distinct lam.eq_iff) |
45 apply(simp add: Abs_eq_iff alphas) |
65 apply (erule Abs1_eq_fdest) |
46 apply(clarify) |
66 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
47 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
|
48 apply(simp add: pure_supp fresh_star_def) |
|
49 apply(simp add: eqvt_at_def) |
|
50 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
67 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
51 unfolding eqvt_def |
68 unfolding eqvt_def |
52 apply(rule allI) |
69 apply(rule allI) |
53 apply(simp add: permute_fun_def) |
70 apply(simp add: permute_fun_def) |
54 apply(rule ext) |
71 apply(rule ext) |
90 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
107 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
91 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
108 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
92 defer |
109 defer |
93 apply(rule_tac y="x" in lam.exhaust) |
110 apply(rule_tac y="x" in lam.exhaust) |
94 apply(simp_all)[3] |
111 apply(simp_all)[3] |
95 apply(simp_all only: lam.distinct) |
112 apply(simp_all add: lam.distinct lam.eq_iff) |
96 apply(simp add: lam.eq_iff) |
113 apply (erule Abs1_eq_fdest) |
97 apply(simp add: lam.eq_iff) |
114 apply(simp add: supp_removeAll fresh_def) |
98 apply(simp add: lam.eq_iff) |
|
99 apply(simp add: Abs_eq_iff) |
|
100 apply(erule exE) |
|
101 apply(simp add: alphas) |
|
102 apply(simp add: atom_eqvt) |
|
103 apply(clarify) |
|
104 apply(rule trans) |
|
105 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
106 apply(simp (no_asm) add: supp_removeAll) |
|
107 apply(drule supp_eqvt_at) |
115 apply(drule supp_eqvt_at) |
108 apply(simp add: finite_supp) |
116 apply(simp add: finite_supp) |
109 apply(auto simp add: fresh_star_def)[1] |
117 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
110 unfolding eqvt_at_def |
|
111 apply(simp only: removeAll_eqvt atom_eqvt) |
|
112 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") |
118 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") |
113 unfolding eqvt_def |
119 unfolding eqvt_def |
114 apply(rule allI) |
120 apply(rule allI) |
115 apply(simp add: permute_fun_def) |
121 apply(simp add: permute_fun_def) |
116 apply(rule ext) |
122 apply(rule ext) |
159 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
165 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
160 defer |
166 defer |
161 apply(auto simp add: lam.distinct lam.eq_iff) |
167 apply(auto simp add: lam.distinct lam.eq_iff) |
162 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
168 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
163 apply(blast)+ |
169 apply(blast)+ |
164 apply(simp add: fresh_star_def) |
170 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
165 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
171 apply (erule Abs1_eq_fdest) |
166 apply(subst (asm) Abs_eq_iff2) |
172 apply(simp_all add: Abs_fresh_iff) |
167 apply(simp add: alphas atom_eqvt) |
173 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
168 apply(clarify) |
174 apply(simp_all add: finite_supp fresh_Pair) |
169 apply(rule trans) |
175 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
170 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
176 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
171 apply(rule fresh_star_supp_conv) |
177 apply(simp add: eqvt_at_def) |
172 apply(drule fresh_star_perm_set_conv) |
178 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ |
173 apply(simp add: finite_supp) |
|
174 apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))") |
|
175 apply(auto simp add: fresh_star_def)[1] |
|
176 apply(simp (no_asm) add: fresh_star_def) |
|
177 apply(rule conjI) |
|
178 apply(simp (no_asm) add: Abs_fresh_iff) |
|
179 apply(clarify) |
|
180 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
181 apply(simp add: finite_supp) |
|
182 apply(simp (no_asm_use) add: fresh_Pair) |
|
183 apply(simp add: Abs_fresh_iff) |
|
184 apply(simp) |
|
185 apply(simp add: Abs_fresh_iff) |
|
186 apply(subgoal_tac "p \<bullet> ya = ya") |
|
187 apply(subgoal_tac "p \<bullet> sa = sa") |
|
188 apply(simp add: atom_eqvt eqvt_at_def) |
|
189 apply(rule perm_supp_eq) |
|
190 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
191 apply(rule perm_supp_eq) |
|
192 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
193 apply(simp add: Abs_fresh_iff) |
|
194 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
179 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
195 unfolding eqvt_def |
180 unfolding eqvt_def |
196 apply(rule allI) |
181 apply(rule allI) |
197 apply(simp add: permute_fun_def) |
182 apply(simp add: permute_fun_def) |
198 apply(rule ext) |
183 apply(rule ext) |
264 using a |
249 using a |
265 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct) |
250 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct) |
266 apply (auto simp add: lam.fresh fresh_at_base) |
251 apply (auto simp add: lam.fresh fresh_at_base) |
267 done |
252 done |
268 |
253 |
|
254 lemma height_ge_one: |
|
255 shows "1 \<le> (height e)" |
|
256 by (induct e rule: lam.induct) (simp_all) |
|
257 |
|
258 theorem height_subst: |
|
259 shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')" |
|
260 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) |
|
261 case (Var y) |
|
262 have "1 \<le> height e'" by (rule height_ge_one) |
|
263 then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp |
|
264 next |
|
265 case (Lam y e1) |
|
266 hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp |
|
267 moreover |
|
268 have vc: "atom y\<sharp>x" "atom y\<sharp>e'" by fact+ (* usual variable convention *) |
|
269 ultimately show "height ((Lam [y]. e1)[x::=e']) \<le> height (Lam [y]. e1) - 1 + height e'" by simp |
|
270 next |
|
271 case (App e1 e2) |
|
272 hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" |
|
273 and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all |
|
274 then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp |
|
275 qed |
269 |
276 |
270 subsection {* single-step beta-reduction *} |
277 subsection {* single-step beta-reduction *} |
271 |
278 |
272 inductive |
279 inductive |
273 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
280 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
340 "lookup [] n x = LNVar x" |
347 "lookup [] n x = LNVar x" |
341 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
348 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
342 |
349 |
343 lemma [eqvt]: |
350 lemma [eqvt]: |
344 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
351 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
345 apply(induct xs arbitrary: n) |
352 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
346 apply(simp_all add: permute_pure) |
|
347 done |
|
348 |
353 |
349 nominal_primrec |
354 nominal_primrec |
350 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
355 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
351 where |
356 where |
352 "trans (Var x) xs = lookup xs 0 x" |
357 "trans (Var x) xs = lookup xs 0 x" |
357 apply(simp) |
362 apply(simp) |
358 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
363 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
359 apply(simp_all add: fresh_star_def)[3] |
364 apply(simp_all add: fresh_star_def)[3] |
360 apply(blast) |
365 apply(blast) |
361 apply(blast) |
366 apply(blast) |
362 apply(simp_all add: lam.distinct) |
367 apply(simp_all add: lam.distinct lam.eq_iff) |
363 apply(simp add: lam.eq_iff) |
368 apply(elim conjE) |
364 apply(simp add: lam.eq_iff) |
369 apply clarify |
365 apply(simp add: lam.eq_iff) |
370 apply (erule Abs1_eq_fdest) |
366 apply(erule conjE) |
371 apply (simp_all add: ln.fresh) |
367 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
|
368 prefer 2 |
372 prefer 2 |
369 apply(simp add: Abs_fresh_iff) |
373 apply(drule supp_eqvt_at) |
370 apply(subst (asm) Abs_eq_iff2) |
374 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
371 apply(auto) |
|
372 apply(simp add: alphas) |
|
373 apply(simp add: atom_eqvt) |
|
374 apply(clarify) |
|
375 apply(rule trans) |
|
376 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
377 prefer 2 |
375 prefer 2 |
378 apply (subgoal_tac "p \<bullet> xsa = xsa") |
376 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
379 apply (simp add: eqvt_at_def) |
377 apply (simp add: eqvt_at_def) |
380 apply (rule supp_perm_eq) |
378 apply (metis atom_name_def swap_fresh_fresh) |
381 apply (rule fresh_star_supp_conv) |
|
382 apply (subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* xsa") |
|
383 apply (simp add: fresh_star_def fresh_def) |
|
384 apply blast |
|
385 apply (simp add: fresh_star_def fresh_def) |
|
386 apply (simp add: ln.supp) |
|
387 apply(rule fresh_star_supp_conv) |
|
388 apply (subst (asm) supp_perm_pair) |
|
389 apply (elim disjE) |
|
390 apply (simp add: fresh_star_def supp_zero_perm) |
|
391 apply (simp add: flip_def[symmetric]) |
|
392 apply(subgoal_tac "supp (x \<leftrightarrow> p \<bullet> x) \<sharp>* trans_sumC (t, x # xsa)") |
|
393 apply simp |
|
394 apply (subst flip_def) |
|
395 apply (simp add: supp_swap) |
|
396 apply (simp add: fresh_star_def) |
|
397 apply (rule) |
|
398 apply rule |
|
399 prefer 2 |
|
400 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
401 apply(simp add: finite_supp) |
|
402 apply(simp (no_asm_use) add: fresh_Pair) |
|
403 apply(simp add: Abs_fresh_iff fresh_Cons)[1] |
|
404 apply (metis Rep_name_inverse atom_name_def fresh_at_base) |
|
405 apply assumption |
|
406 oops |
379 oops |
407 |
380 |
408 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
381 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
409 apply (case_tac "x = xa") |
382 apply (case_tac "x = xa") |
410 apply simp |
383 apply simp |