42 apply simp_all[3] apply (metis, metis, metis) |
42 apply simp_all[3] apply (metis, metis, metis) |
43 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) |
44 apply simp_all[3] apply (metis, metis, metis) |
44 apply simp_all[3] apply (metis, metis, metis) |
45 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) |
46 apply simp_all[2] apply (metis, metis) |
46 apply simp_all[2] apply (metis, metis) |
|
47 unfolding fresh_star_def |
47 apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P") |
48 apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P") |
48 apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P") |
49 apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P") |
49 apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P") |
50 apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<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") |
51 apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P") |
51 apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P") |
52 apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P") |
58 apply (drule_tac x="lama" in meta_spec) |
59 apply (drule_tac x="lama" in meta_spec) |
59 apply (drule_tac x="lama" in meta_spec) |
60 apply (drule_tac x="lama" in meta_spec) |
60 apply (drule_tac x="lam" in meta_spec)+ |
61 apply (drule_tac x="lam" in meta_spec)+ |
61 apply (drule_tac x="b" in meta_spec)+ |
62 apply (drule_tac x="b" in meta_spec)+ |
62 apply (drule_tac x="a" in meta_spec)+ |
63 apply (drule_tac x="a" in meta_spec)+ |
63 unfolding fresh_star_def |
64 apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
64 apply (case_tac " |
65 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
65 (\<forall>x' y' t' s'. |
66 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')") |
66 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
|
67 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
|
68 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
|
69 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s') |
|
70 ") |
|
71 apply clarify |
67 apply clarify |
72 apply (simp) |
68 apply (simp) |
73 apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and> |
69 apply (simp only: fresh_Pair_elim) |
74 atom namea \<sharp> (name, c, Lam [name]. lam) \<and> |
70 apply blast |
75 (\<forall>x' y' t' s'. |
|
76 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
|
77 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
|
78 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
|
79 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s'); |
|
80 x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk> |
|
81 \<Longrightarrow> P") |
|
82 apply (simp) |
|
83 apply (simp_all)[53] |
71 apply (simp_all)[53] |
84 apply clarify |
72 apply clarify |
85 apply metis |
73 apply metis |
86 apply simp |
74 apply simp |
87 done |
75 done |
96 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
84 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
97 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
85 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
98 apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust) |
86 apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust) |
99 apply auto[2] |
87 apply auto[2] |
100 apply clarify |
88 apply clarify |
101 apply (case_tac "(\<forall>x' y' t' s'. |
89 apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> |
102 atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> |
90 atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
103 atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> |
91 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> fll name lam namea lama = fll x' t' y' s')") |
104 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
92 unfolding fresh_star_def |
105 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> |
93 apply (subst lam2_rec.simps) apply simp |
106 fll name lam namea lama = fll x' t' y' s')") |
94 apply (subst lam2_rec.simps) apply simp |
107 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
|
108 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
|
109 apply metis |
95 apply metis |
110 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
96 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) |
97 apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def) |
112 apply rule |
|
113 done |
98 done |
114 |
99 |
115 nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" |
100 nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" |
116 where |
101 where |
117 [simp del]: "aux l r xs = lam2_rec |
102 [simp del]: "aux l r xs = lam2_rec |
142 apply (subst aux.simps, simp) |
127 apply (subst aux.simps, simp) |
143 apply (subst aux.simps, simp) |
128 apply (subst aux.simps, simp) |
144 apply (subst aux.simps, simp) |
129 apply (subst aux.simps, simp) |
145 apply (subst aux.simps) |
130 apply (subst aux.simps) |
146 apply (subst lam2_rec.simps) |
131 apply (subst lam2_rec.simps) |
147 prefer 2 apply rule |
|
148 apply (rule, simp add: lam.fresh) |
132 apply (rule, simp add: lam.fresh) |
149 apply (rule, simp add: lam.fresh) |
133 apply (rule, simp add: lam.fresh) |
150 apply (intro allI impI) |
134 apply (intro allI impI) |
151 apply (rule_tac x="(x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
135 apply (rule_tac x="(x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
152 apply (rule_tac x="(a, x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
136 apply (rule_tac x="(a, x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
222 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
207 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where |
223 "swapequal l r [] \<longleftrightarrow> l = r" |
208 "swapequal l r [] \<longleftrightarrow> l = r" |
224 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
209 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow> |
225 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
210 swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t" |
226 unfolding eqvt_def swapequal_graph_def |
211 unfolding eqvt_def swapequal_graph_def |
227 apply (rule, perm_simp, rule) |
212 apply (rule, perm_simp, rule, rule TrueI) |
228 apply(rule TrueI) |
|
229 apply (case_tac x) |
213 apply (case_tac x) |
230 apply (case_tac c) |
214 apply (case_tac c) |
231 apply metis |
215 apply metis |
232 apply (case_tac aa) |
216 apply (case_tac aa) |
233 apply (rename_tac l r lst h t hl hr) |
217 apply (rename_tac l r lst h t hl hr) |
260 apply (subst swapequal.simps) |
244 apply (subst swapequal.simps) |
261 apply (simp add: fresh_Pair lam.fresh) |
245 apply (simp add: fresh_Pair lam.fresh) |
262 apply (simp add: fresh_Pair_elim) |
246 apply (simp add: fresh_Pair_elim) |
263 by (metis flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
247 by (metis flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
264 |
248 |
265 lemma var_neq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs" |
249 lemma var_neq_swapequal: |
|
250 "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs" |
|
251 "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs" |
266 apply (induct xs arbitrary: m) |
252 apply (induct xs arbitrary: m) |
267 apply simp |
253 apply simp_all[2] |
268 apply (case_tac a) |
254 apply (case_tac [!] a) |
269 apply (simp add: fresh_Cons) |
255 apply (simp_all add: fresh_Cons) |
270 apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh) |
256 apply (rule_tac [!] x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh) |
271 apply (subst swapequal.simps) |
257 apply (subst swapequal.simps) |
272 apply (simp add: fresh_Pair lam.fresh) |
258 apply (auto simp add: fresh_Pair lam.fresh)[1] |
273 apply auto[1] |
|
274 apply (elim conjE) |
259 apply (elim conjE) |
275 apply (simp add: fresh_Pair_elim) |
260 apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at) |
276 apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
261 apply (subst swapequal.simps) |
277 apply (subgoal_tac "ab \<noteq> (b \<leftrightarrow> aba) \<bullet> m") |
262 apply (auto simp add: fresh_Pair lam.fresh)[1] |
278 apply simp |
|
279 by (metis (lifting) permute_flip_at) |
|
280 |
|
281 lemma var_neq_swapequal2: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs" |
|
282 apply (induct xs arbitrary: m) |
|
283 apply simp |
|
284 apply (case_tac a) |
|
285 apply (simp add: fresh_Cons) |
|
286 apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh) |
|
287 apply (subst swapequal.simps) |
|
288 apply (simp add: fresh_Pair lam.fresh) |
|
289 apply auto[1] |
|
290 apply (elim conjE) |
263 apply (elim conjE) |
291 apply (simp add: fresh_Pair_elim) |
264 apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at) |
292 apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
265 done |
293 apply (subgoal_tac "ab \<noteq> (aa \<leftrightarrow> aba) \<bullet> m") |
|
294 apply simp |
|
295 by (metis (lifting) permute_flip_at) |
|
296 |
266 |
297 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs" |
267 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs" |
298 apply (induct xs arbitrary: m n) |
268 apply (induct xs arbitrary: m n) |
299 apply simp |
269 apply simp |
300 apply (case_tac a) |
270 apply (case_tac a) |
301 apply simp |
|
302 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
271 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
272 apply simp |
303 apply (subst swapequal.simps) |
273 apply (subst swapequal.simps) |
304 apply (simp add: fresh_Pair lam.fresh fresh_Nil) |
274 apply (simp add: fresh_Pair lam.fresh fresh_Nil) |
305 apply (case_tac "n = aa \<and> m = b") |
275 by (metis (hide_lams, mono_tags) flip_at_base_simps(3) flip_at_simps(1) fresh_Pair fresh_at_base(2) lam.perm_simps(1) var_eq_swapequal var_neq_swapequal(1) var_neq_swapequal(2)) |
306 apply simp |
|
307 apply (simp add: var_eq_swapequal fresh_Pair_elim) |
|
308 apply (case_tac "n = aa") |
|
309 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
310 apply (simp add: var_neq_swapequal fresh_Pair_elim) |
|
311 apply (simp add: fresh_Pair_elim fresh_at_base flip_def) |
|
312 apply (case_tac "m = b") |
|
313 apply simp |
|
314 apply (simp add: var_neq_swapequal2 fresh_at_base) |
|
315 apply simp |
|
316 done |
|
317 |
276 |
318 lemma swapequal_reorder: " |
277 lemma swapequal_reorder: " |
319 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
278 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
320 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
279 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
321 apply (rule_tac x="(a, b, x, y, t, s, xs)" and ?'a="name" in obtain_fresh) |
280 apply (rule_tac x="(a, b, x, y, t, s, xs)" and ?'a="name" in obtain_fresh) |
361 apply simp |
320 apply simp |
362 apply (subgoal_tac "[[atom x]]lst. t = [[atom a]]lst. ((x \<leftrightarrow> a) \<bullet> t)") |
321 apply (subgoal_tac "[[atom x]]lst. t = [[atom a]]lst. ((x \<leftrightarrow> a) \<bullet> t)") |
363 apply (subgoal_tac "[[atom y]]lst. s = [[atom a]]lst. ((y \<leftrightarrow> a) \<bullet> s)") |
322 apply (subgoal_tac "[[atom y]]lst. s = [[atom a]]lst. ((y \<leftrightarrow> a) \<bullet> s)") |
364 apply simp |
323 apply simp |
365 apply (simp add: Abs1_eq_iff) |
324 apply (simp add: Abs1_eq_iff) |
366 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1] |
325 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[2] |
367 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
326 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
368 apply (simp add: Abs1_eq_iff) |
|
369 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1] |
|
370 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
327 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
371 apply clarify |
328 apply clarify |
372 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
329 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
373 apply clarify |
330 apply clarify |
374 apply (subst swapequal_reorder) |
331 apply (simp add: swapequal_reorder) |
375 apply auto[4] |
|
376 apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh) |
332 apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh) |
377 apply (rename_tac f) |
333 apply (rename_tac f) |
378 apply (subst (2) swapequal.simps) |
334 apply (subst (2) swapequal.simps) |
379 apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons) |
335 apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1] |
380 apply auto[1] |
336 apply (subst swapequal.simps) |
381 apply (subst swapequal.simps) |
337 apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1] |
382 apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons) |
338 apply (simp add: flip_def fresh_Pair_elim fresh_at_base) |
383 apply auto[1] |
|
384 apply simp |
|
385 apply (simp add: flip_def) |
|
386 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
387 done |
339 done |
388 |
340 |
389 lemma distinct_swapequal: "\<forall>p q. p \<bullet> l \<noteq> q \<bullet> r \<Longrightarrow> \<not>swapequal l r xs" |
341 lemma distinct_swapequal: "\<forall>p q. p \<bullet> l \<noteq> q \<bullet> r \<Longrightarrow> \<not>swapequal l r xs" |
390 apply (induct xs rule:swapequal.induct) |
342 apply (induct xs rule:swapequal.induct) |
391 apply simp |
343 apply auto[1] |
392 apply metis |
|
393 apply (simp add: fresh_Pair_elim) |
344 apply (simp add: fresh_Pair_elim) |
394 apply (subgoal_tac "\<forall>(p\<Colon>perm) q\<Colon>perm. p \<bullet> (hl \<leftrightarrow> x) \<bullet> l \<noteq> q \<bullet> (hr \<leftrightarrow> x) \<bullet> r") |
345 apply (subgoal_tac "\<forall>(p\<Colon>perm) q\<Colon>perm. p \<bullet> (hl \<leftrightarrow> x) \<bullet> l \<noteq> q \<bullet> (hr \<leftrightarrow> x) \<bullet> r") |
395 apply simp |
346 apply simp |
396 apply (intro allI) |
347 apply (intro allI) |
397 apply (drule_tac x="p + (hl \<leftrightarrow> x)" in spec) |
348 apply (drule_tac x="p + (hl \<leftrightarrow> x)" in spec) |
427 assumes "distinct (map fst xs @ map snd xs)" |
377 assumes "distinct (map fst xs @ map snd xs)" |
428 shows "aux x y xs \<longleftrightarrow> swapequal x y xs" |
378 shows "aux x y xs \<longleftrightarrow> swapequal x y xs" |
429 using assms |
379 using assms |
430 apply (induct xs x y rule: aux_induct) |
380 apply (induct xs x y rule: aux_induct) |
431 apply (simp add: lookup_swapequal) |
381 apply (simp add: lookup_swapequal) |
432 apply (simp, rule distinct_swapequal, simp) |
382 apply (simp, rule distinct_swapequal, simp)+ |
433 apply (simp, rule distinct_swapequal, simp) |
|
434 apply (simp, rule distinct_swapequal, simp) |
|
435 apply (simp add: swapequal_app) |
383 apply (simp add: swapequal_app) |
436 apply (simp, rule distinct_swapequal, simp) |
384 apply (simp, rule distinct_swapequal, simp)+ |
437 apply (simp, rule distinct_swapequal, simp) |
385 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base conjE) |
438 apply (simp, rule distinct_swapequal, simp) |
|
439 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
|
440 apply (elim conjE) |
386 apply (elim conjE) |
441 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
387 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
442 apply (subgoal_tac "x \<notin> fst ` set xs \<and> |
388 apply (subgoal_tac "x \<notin> fst ` set xs \<and> |
443 x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs") |
389 x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs") |
444 apply (simp) |
|
445 apply (subst swapequal_lambda) |
390 apply (subst swapequal_lambda) |
446 apply auto[2] |
391 apply auto[2] |
447 apply simp |
392 apply simp |
448 done |
393 done |
449 |
394 |