equal
deleted
inserted
replaced
300 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
300 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
301 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
301 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
302 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t") |
302 apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t") |
303 apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s") |
303 apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s") |
304 apply simp |
304 apply simp |
305 apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt) |
305 apply (subst permute_eqvt) apply (simp add: flip_eqvt) |
306 apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt) |
306 apply (subst permute_eqvt) apply (simp add: flip_eqvt) |
307 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
307 apply (simp add: flip_at_base_simps fresh_at_base flip_def) |
308 done |
308 done |
309 |
309 |
310 lemma swapequal_lambda: |
310 lemma swapequal_lambda: |
311 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
311 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
321 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)") |
322 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)") |
323 apply simp |
323 apply simp |
324 apply (simp add: Abs1_eq_iff) |
324 apply (simp add: Abs1_eq_iff) |
325 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[2] |
325 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[2] |
326 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
326 apply (simp add: fresh_permute_left) |
327 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
327 apply (simp add: fresh_permute_left) |
328 apply clarify |
328 apply clarify |
329 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
329 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
330 apply clarify |
330 apply clarify |
331 apply (simp add: swapequal_reorder) |
331 apply (simp add: swapequal_reorder) |
332 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) |