Quot/Nominal/Nominal2_Supp.thy
changeset 1080 2f1377bb4e1f
parent 1062 dfea9e739231
equal deleted inserted replaced
1079:c70e7545b738 1080:2f1377bb4e1f
   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)