266 apply (rename_tac l r lst h t hl hr) |
266 apply (rename_tac l r lst h t hl hr) |
267 apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh) |
267 apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh) |
268 apply simp |
268 apply simp |
269 apply simp |
269 apply simp |
270 apply simp |
270 apply simp |
271 (* The last subgoal would be obvious if we'd define it with a recusor |
271 apply clarify |
272 and have eqvt for the function *) |
272 apply (rule_tac s="(x \<leftrightarrow> xa) \<bullet> swapequal_sumC ((hla \<leftrightarrow> x) \<bullet> la, (hra \<leftrightarrow> x) \<bullet> ra, ta)" in trans) |
273 sorry |
273 apply (simp only: permute_pure) |
|
274 apply (simp add: eqvt_at_def fresh_Pair_elim) |
|
275 apply (simp add: flip_fresh_fresh) |
|
276 apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hla \<leftrightarrow> x) \<bullet> la = (hla \<leftrightarrow> xa) \<bullet> la") |
|
277 apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hra \<leftrightarrow> x) \<bullet> ra = (hra \<leftrightarrow> xa) \<bullet> ra") |
|
278 apply simp |
|
279 apply (subst permute_eqvt) |
|
280 apply (simp add: flip_fresh_fresh flip_eqvt) |
|
281 apply (subst permute_eqvt) |
|
282 apply (simp add: flip_fresh_fresh flip_eqvt) |
|
283 done |
274 |
284 |
275 termination (eqvt) by lexicographic_order |
285 termination (eqvt) by lexicographic_order |
276 |
286 |
277 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs" |
287 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs" |
278 apply (induct xs) |
288 apply (induct xs) |
339 done |
349 done |
340 |
350 |
341 lemma swapequal_reorder: " |
351 lemma swapequal_reorder: " |
342 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
352 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
343 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
353 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
344 sorry |
354 apply (rule_tac x="(a, b, x, y, t, s, xs)" and ?'a="name" in obtain_fresh) |
|
355 apply (rule_tac x="(a, b, x, y, t, s, xs, aa)" and ?'a="name" in obtain_fresh) |
|
356 apply (rename_tac f g) |
|
357 apply (simp add: fresh_Pair_elim fresh_at_base) |
|
358 apply (subst swapequal.simps) |
|
359 apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1] |
|
360 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) |
|
364 apply (simp add: fresh_Pair fresh_Cons fresh_permute_left) |
|
365 apply rule apply assumption |
|
366 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
|
367 apply (subst swapequal.simps) |
|
368 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
|
369 apply rule apply (rotate_tac 12) |
|
370 apply assumption |
|
371 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
|
372 apply (subst swapequal.simps) |
|
373 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") |
|
375 prefer 2 |
|
376 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) |
|
379 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") |
|
381 apply simp |
|
382 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) |
|
384 done |
345 |
385 |
346 lemma swapequal_lambda: |
386 lemma swapequal_lambda: |
347 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
387 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
348 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |
388 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |
349 using assms |
389 using assms |