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

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

   853   }

   853   }

   854   moreover 

   854   moreover 

   855   { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"

   855   { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"

   856     have "[{atom a}]set. x = [{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp

   856     have "[{atom a}]set. x = [{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp

   858     also have "\<dots> = [{atom b}]set. y"

   858     also have "\<dots> = [{atom b}]set. y"

   859       by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   859       by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   860     finally have "[{atom a}]set. x = [{atom b}]set. y" .

   860     finally have "[{atom a}]set. x = [{atom b}]set. y" .

   861   }

   861   }

   862   ultimately 

   862   ultimately 

   867     then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   867     then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   868   }

   868   }

   869   moreover

   869   moreover

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

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

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

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

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

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

   874       by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   874       by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

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

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

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

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

   877   }

   877   }

   878   moreover 

   878   moreover 

   879   { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"

   879   { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"

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

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

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

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

   883       by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   883       by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

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

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

   885   }

   885   }

   886   ultimately 

   886   ultimately 

   891     then have "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   891     then have "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   892   }

   892   }

   893   moreover

   893   moreover

   894   { assume *: "a \<noteq> b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y"

   894   { assume *: "a \<noteq> b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y"

   895     have #: "atom a \<sharp> Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff)

   895     have #: "atom a \<sharp> Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff)

   897     also have "\<dots> = Abs_lst [atom b] y"

   897     also have "\<dots> = Abs_lst [atom b] y"

   898       by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   898       by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   899     also have "\<dots> = Abs_lst [atom a] x" using ** by simp

   899     also have "\<dots> = Abs_lst [atom a] x" using ** by simp

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

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

   901   }

   901   }

   902   moreover 

   902   moreover 

   903   { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"

   903   { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"

   904     have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp

   904     have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp

   906     also have "\<dots> = Abs_lst [atom b] y"

   906     also have "\<dots> = Abs_lst [atom b] y"

   907       by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   907       by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   908     finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" .

   908     finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" .

   909   }

   909   }

   910   ultimately 

   910   ultimately 

   916   fixes x::"'a::fs"

   916   fixes x::"'a::fs"

   917   and a b::"'b::at"

   917   and a b::"'b::at"

   918   shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"

   918   shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"

   919   and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"

   919   and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"

   920   and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"

   920   and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"

   922 

   922 

   923 

   923 

   924 ML {*

   924 ML {*

   925 fun alpha_single_simproc thm _ ctxt ctrm =

   925 fun alpha_single_simproc thm _ ctxt ctrm =

   926   let

   926   let