34 \<not>(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s' |
34 \<not>(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s' |
35 \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow> |
35 \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow> |
36 lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False" |
36 lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False" |
37 apply (simp add: eqvt_def lam2_rec_graph_def) |
37 apply (simp add: eqvt_def lam2_rec_graph_def) |
38 apply (rule, perm_simp, rule, rule) |
38 apply (rule, perm_simp, rule, rule) |
39 defer |
|
40 apply (simp_all)[53] |
|
41 apply clarify |
|
42 apply metis |
|
43 apply simp |
|
44 apply (case_tac x) |
39 apply (case_tac x) |
45 apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust) |
40 apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust) |
46 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
41 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
47 apply simp_all[3] |
42 apply simp_all[3] apply (metis, metis, metis) |
48 apply (metis, metis, metis) |
|
49 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
43 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
50 apply simp_all[3] |
44 apply simp_all[3] apply (metis, metis, metis) |
51 apply (metis, metis, metis) |
|
52 apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust) |
45 apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust) |
53 apply simp_all[2] |
46 apply simp_all[2] apply (metis, metis) |
54 apply (metis, metis) |
|
55 apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P") |
47 apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P") |
56 apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P") |
48 apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P") |
57 apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P") |
49 apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P") |
58 apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P") |
50 apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P") |
59 apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P") |
51 apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P") |
66 apply (drule_tac x="lama" in meta_spec) |
58 apply (drule_tac x="lama" in meta_spec) |
67 apply (drule_tac x="lama" in meta_spec) |
59 apply (drule_tac x="lama" in meta_spec) |
68 apply (drule_tac x="lam" in meta_spec)+ |
60 apply (drule_tac x="lam" in meta_spec)+ |
69 apply (drule_tac x="b" in meta_spec)+ |
61 apply (drule_tac x="b" in meta_spec)+ |
70 apply (drule_tac x="a" in meta_spec)+ |
62 apply (drule_tac x="a" in meta_spec)+ |
|
63 unfolding fresh_star_def |
71 apply (case_tac " |
64 apply (case_tac " |
72 (\<forall>x' y' t' s'. |
65 (\<forall>x' y' t' s'. |
73 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
66 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
74 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
67 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
75 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
68 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
76 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s') |
69 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s') |
77 ") |
70 ") |
78 apply clarify |
71 apply clarify |
79 apply (simp add: fresh_star_def) |
72 apply (simp) |
80 apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and> |
73 apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and> |
81 atom namea \<sharp> (name, c, Lam [name]. lam) \<and> |
74 atom namea \<sharp> (name, c, Lam [name]. lam) \<and> |
82 (\<forall>x' y' t' s'. |
75 (\<forall>x' y' t' s'. |
83 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
76 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
84 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
77 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
85 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
78 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
86 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s'); |
79 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s'); |
87 x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk> |
80 x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk> |
88 \<Longrightarrow> P") |
81 \<Longrightarrow> P") |
89 apply (simp add: fresh_star_def) |
82 apply (simp) |
|
83 apply (simp_all)[53] |
|
84 apply clarify |
|
85 apply metis |
|
86 apply simp |
90 done |
87 done |
91 |
88 |
92 termination (eqvt) by lexicographic_order |
89 termination (eqvt) by lexicographic_order |
93 |
90 |
94 lemma lam_rec2_cong[fundef_cong]: |
91 lemma lam_rec2_cong[fundef_cong]: |
107 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
104 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
108 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> |
105 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> |
109 fll name lam namea lama = fll x' t' y' s')") |
106 fll name lam namea lama = fll x' t' y' s')") |
110 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
107 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
111 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
108 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
112 using Abs1_eq_iff lam.eq_iff apply metis |
109 apply metis |
113 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
110 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
114 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
111 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
115 apply rule |
112 apply rule |
116 done |
113 done |
117 |
114 |
220 apply (simp add: fresh_star_def) |
217 apply (simp add: fresh_star_def) |
221 apply metis |
218 apply metis |
222 apply lexicographic_order |
219 apply lexicographic_order |
223 done |
220 done |
224 |
221 |
225 lemma foldr_eqvt[eqvt]: |
|
226 "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)" |
|
227 apply (induct b) |
|
228 apply simp_all |
|
229 apply (perm_simp) |
|
230 apply simp |
|
231 done |
|
232 |
|
233 nominal_primrec |
|
234 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
|
235 where |
|
236 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
237 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
238 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
239 unfolding eqvt_def subst_graph_def |
|
240 apply (rule, perm_simp, rule) |
|
241 apply(rule TrueI) |
|
242 apply(auto) |
|
243 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
244 apply(blast)+ |
|
245 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
|
246 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
|
247 apply(simp_all add: Abs_fresh_iff) |
|
248 apply(simp add: fresh_star_def fresh_Pair) |
|
249 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
250 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
251 done |
|
252 |
|
253 termination (eqvt) by lexicographic_order |
|
254 |
|
255 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
222 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
256 "swapequal l r [] \<longleftrightarrow> l = r" |
223 "swapequal l r [] \<longleftrightarrow> l = r" |
257 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
224 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
258 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
225 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
259 unfolding eqvt_def swapequal_graph_def |
226 unfolding eqvt_def swapequal_graph_def |
308 apply (simp add: fresh_Pair_elim) |
275 apply (simp add: fresh_Pair_elim) |
309 apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
276 apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
310 apply (subgoal_tac "ab \<noteq> (b \<leftrightarrow> aba) \<bullet> m") |
277 apply (subgoal_tac "ab \<noteq> (b \<leftrightarrow> aba) \<bullet> m") |
311 apply simp |
278 apply simp |
312 by (metis (lifting) permute_flip_at) |
279 by (metis (lifting) permute_flip_at) |
|
280 |
313 lemma var_neq_swapequal2: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs" |
281 lemma var_neq_swapequal2: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs" |
314 apply (induct xs arbitrary: m) |
282 apply (induct xs arbitrary: m) |
315 apply simp |
283 apply simp |
316 apply (case_tac a) |
284 apply (case_tac a) |
317 apply (simp add: fresh_Cons) |
285 apply (simp add: fresh_Cons) |
356 apply (rename_tac f g) |
323 apply (rename_tac f g) |
357 apply (simp add: fresh_Pair_elim fresh_at_base) |
324 apply (simp add: fresh_Pair_elim fresh_at_base) |
358 apply (subst swapequal.simps) |
325 apply (subst swapequal.simps) |
359 apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1] |
326 apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1] |
360 apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t") |
327 apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t") |
361 prefer 2 |
|
362 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
|
363 apply (subst swapequal.simps) |
328 apply (subst swapequal.simps) |
364 apply (simp add: fresh_Pair fresh_Cons fresh_permute_left) |
329 apply (simp add: fresh_Pair fresh_Cons fresh_permute_left) |
365 apply rule apply assumption |
330 apply rule apply assumption |
366 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
331 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
367 apply (subst swapequal.simps) |
332 apply (subst swapequal.simps) |
370 apply assumption |
335 apply assumption |
371 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
336 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
372 apply (subst swapequal.simps) |
337 apply (subst swapequal.simps) |
373 apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left) |
338 apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left) |
374 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t") |
339 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t") |
375 prefer 2 |
340 apply rule apply assumption |
376 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
341 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
377 apply rule apply assumption |
|
378 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
342 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
379 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t") |
343 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t") |
380 apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s") |
344 apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s") |
381 apply simp |
345 apply simp |
382 apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt) |
346 apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt) |
383 apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt) |
347 apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt) |
|
348 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
384 done |
349 done |
385 |
350 |
386 lemma swapequal_lambda: |
351 lemma swapequal_lambda: |
387 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
352 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
388 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |
353 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |