14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
15 where |
15 where |
16 Var: "triv (Var x) n" |
16 Var: "triv (Var x) n" |
17 |
17 |
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 inductive |
|
24 triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
25 where |
|
26 Var1: "triv2 (Var x) 0" |
|
27 | Var2: "triv2 (Var x) (n + n)" |
|
28 | Var3: "triv2 (Var x) n" |
|
29 |
|
30 equivariance triv2 |
|
31 nominal_inductive triv2 . |
|
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 |
23 |
53 |
24 text {* height function *} |
54 text {* height function *} |
25 |
55 |
26 nominal_primrec |
56 nominal_primrec |
27 height :: "lam \<Rightarrow> int" |
57 height :: "lam \<Rightarrow> int" |
30 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
60 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
31 | "height (Lam [x].t) = height t + 1" |
61 | "height (Lam [x].t) = height t + 1" |
32 defer |
62 defer |
33 apply(rule_tac y="x" in lam.exhaust) |
63 apply(rule_tac y="x" in lam.exhaust) |
34 apply(auto simp add: lam.distinct lam.eq_iff) |
64 apply(auto simp add: lam.distinct lam.eq_iff) |
35 apply(simp add: Abs_eq_iff alphas) |
65 apply (erule Abs1_eq_fdest) |
36 apply(clarify) |
66 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)") |
67 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
41 unfolding eqvt_def |
68 unfolding eqvt_def |
42 apply(rule allI) |
69 apply(rule allI) |
43 apply(simp add: permute_fun_def) |
70 apply(simp add: permute_fun_def) |
44 apply(rule ext) |
71 apply(rule ext) |
80 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
107 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
81 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
108 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
82 defer |
109 defer |
83 apply(rule_tac y="x" in lam.exhaust) |
110 apply(rule_tac y="x" in lam.exhaust) |
84 apply(simp_all)[3] |
111 apply(simp_all)[3] |
85 apply(simp_all only: lam.distinct) |
112 apply(simp_all add: lam.distinct lam.eq_iff) |
86 apply(simp add: lam.eq_iff) |
113 apply (erule Abs1_eq_fdest) |
87 apply(simp add: lam.eq_iff) |
114 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) |
115 apply(drule supp_eqvt_at) |
98 apply(simp add: finite_supp) |
116 apply(simp add: finite_supp) |
99 apply(auto simp add: fresh_star_def)[1] |
117 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)") |
118 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 |
119 unfolding eqvt_def |
104 apply(rule allI) |
120 apply(rule allI) |
105 apply(simp add: permute_fun_def) |
121 apply(simp add: permute_fun_def) |
106 apply(rule ext) |
122 apply(rule ext) |
149 | "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])" |
150 defer |
166 defer |
151 apply(auto simp add: lam.distinct lam.eq_iff) |
167 apply(auto simp add: lam.distinct lam.eq_iff) |
152 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) |
153 apply(blast)+ |
169 apply(blast)+ |
154 apply(simp add: fresh_star_def) |
170 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
155 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
171 apply (erule Abs1_eq_fdest) |
156 apply(subst (asm) Abs_eq_iff2) |
172 apply(simp_all add: Abs_fresh_iff) |
157 apply(simp add: alphas atom_eqvt) |
173 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
158 apply(clarify) |
174 apply(simp_all add: finite_supp fresh_Pair) |
159 apply(rule trans) |
175 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
160 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
176 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
161 apply(rule fresh_star_supp_conv) |
177 apply(simp add: eqvt_at_def) |
162 apply(drule fresh_star_perm_set_conv) |
178 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)") |
179 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
185 unfolding eqvt_def |
180 unfolding eqvt_def |
186 apply(rule allI) |
181 apply(rule allI) |
187 apply(simp add: permute_fun_def) |
182 apply(simp add: permute_fun_def) |
188 apply(rule ext) |
183 apply(rule ext) |
254 using a |
249 using a |
255 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) |
256 apply (auto simp add: lam.fresh fresh_at_base) |
251 apply (auto simp add: lam.fresh fresh_at_base) |
257 done |
252 done |
258 |
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 |
259 |
276 |
260 subsection {* single-step beta-reduction *} |
277 subsection {* single-step beta-reduction *} |
261 |
278 |
262 inductive |
279 inductive |
263 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
280 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
330 "lookup [] n x = LNVar x" |
347 "lookup [] n x = LNVar x" |
331 | "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))" |
332 |
349 |
333 lemma [eqvt]: |
350 lemma [eqvt]: |
334 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)" |
335 apply(induct xs arbitrary: n) |
352 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
336 apply(simp_all add: permute_pure) |
|
337 done |
|
338 |
353 |
339 nominal_primrec |
354 nominal_primrec |
340 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
355 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
341 where |
356 where |
342 "trans (Var x) xs = lookup xs 0 x" |
357 "trans (Var x) xs = lookup xs 0 x" |
347 apply(simp) |
362 apply(simp) |
348 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) |
349 apply(simp_all add: fresh_star_def)[3] |
364 apply(simp_all add: fresh_star_def)[3] |
350 apply(blast) |
365 apply(blast) |
351 apply(blast) |
366 apply(blast) |
352 apply(simp_all add: lam.distinct) |
367 apply(simp_all add: lam.distinct lam.eq_iff) |
353 apply(simp add: lam.eq_iff) |
368 apply(elim conjE) |
354 apply(simp add: lam.eq_iff) |
369 apply clarify |
355 apply(simp add: lam.eq_iff) |
370 apply (erule Abs1_eq_fdest) |
356 apply(erule conjE) |
371 apply (simp_all add: ln.fresh) |
357 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
|
358 prefer 2 |
372 prefer 2 |
359 apply(simp add: Abs_fresh_iff) |
373 apply(drule supp_eqvt_at) |
360 apply(subst (asm) Abs_eq_iff2) |
374 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 |
375 prefer 2 |
368 apply (subgoal_tac "p \<bullet> xsa = xsa") |
376 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
369 apply (simp add: eqvt_at_def) |
377 apply (simp add: eqvt_at_def) |
370 apply (rule supp_perm_eq) |
378 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 |
379 oops |
397 |
380 |
398 (* 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)" |
399 apply (case_tac "x = xa") |
382 apply (case_tac "x = xa") |
400 apply simp |
383 apply simp |