494 

   726 

   727 lemma Abs1_eq:

   728   fixes x::"'a::fs"

   729   shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"

   730   and   "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y"

   731   and   "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y"

   732 unfolding Abs_eq_iff2 alphas

   733 apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)

   734 apply(blast)+

   735 done

   736 

   737 

   738 lemma Abs1_eq_iff:

   739   fixes x::"'a::fs"

   740   assumes "sort_of a = sort_of b"

   741   and     "sort_of c = sort_of d"

   742   shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   743   and   "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   744   and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"

   745 proof -

   746   { assume "a = b"

   747     then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)"

   748       by (simp add: Abs1_eq)

   749   }

   750   moreover

   751   { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"

   752     have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)

   753     have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms)

   754     also have "\<dots> = Abs_set {b} y"

   755       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   756     also have "\<dots> = Abs_set {a} x" using ** by simp

   757     finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)

   758   }

   759   moreover 

   760   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"

   761     have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp

   762     also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_eq assms)

   763     also have "\<dots> = Abs_set {b} y"

   764       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   765     finally have "Abs_set {a} x = Abs_set {b} y" .

   766   }

   767   ultimately 

   768   show "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   769     by blast

   770 next

   771   { assume "a = b"

   772     then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)"

   773       by (simp add: Abs1_eq)

   774   }

   775   moreover

   776   { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"

   777     have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)

   778     have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms)

   779     also have "\<dots> = Abs_res {b} y"

   780       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   781     also have "\<dots> = Abs_res {a} x" using ** by simp

   782     finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)

   783   }

   784   moreover 

   785   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"

   786     have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp

   787     also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_eq assms)

   788     also have "\<dots> = Abs_res {b} y"

   789       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   790     finally have "Abs_res {a} x = Abs_res {b} y" .

   791   }

   792   ultimately 

   793   show "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   794     by blast

   795 next

   796   { assume "c = d"

   797     then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)"

   798       by (simp add: Abs1_eq)

   799   }

   800   moreover

   801   { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y"

   802     have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff)

   803     have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms)

   804     also have "\<dots> = Abs_lst [d] y"

   805       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   806     also have "\<dots> = Abs_lst [c] x" using ** by simp

   807     finally have "c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)

   808   }

   809   moreover 

   810   { assume *: "c \<noteq> d" and **: "x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y"

   811     have "Abs_lst [c] x = Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y)" using ** by simp

   812     also have "\<dots> = (c \<rightleftharpoons> d) \<bullet> Abs_lst [d] y" by (simp add: assms)

   813     also have "\<dots> = Abs_lst [d] y"

   814       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   815     finally have "Abs_lst [c] x = Abs_lst [d] y" .

   816   }

   817   ultimately 

   818   show "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"

   819     by blast

   820 qed