equal
deleted
inserted
replaced
151 proof (cases "a = b") |
151 proof (cases "a = b") |
152 assume "a = b" |
152 assume "a = b" |
153 thus "h a = h b" by simp |
153 thus "h a = h b" by simp |
154 next |
154 next |
155 assume "a \<noteq> b" |
155 assume "a \<noteq> b" |
156 hence "atom a \<sharp> b" by (simp add: fresh_at) |
156 hence "atom a \<sharp> b" by (simp add: fresh_at_base) |
157 with a3 have "atom a \<sharp> h b" by (rule fresh_apply) |
157 with a3 have "atom a \<sharp> h b" by (rule fresh_apply) |
158 with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)" |
158 with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)" |
159 by (rule swap_fresh_fresh) |
159 by (rule swap_fresh_fresh) |
160 from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h" |
160 from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h" |
161 by (rule swap_fresh_fresh) |
161 by (rule swap_fresh_fresh) |