Nominal/Abs.thy
changeset 1664 aa999d263b10
parent 1657 d7dc35222afc
child 1665 d00dd828f7af
equal deleted inserted replaced
1660:d1293d30c657 1664:aa999d263b10
   585   unfolding alphas
   585   unfolding alphas
   586   unfolding fresh_star_def
   586   unfolding fresh_star_def
   587   by (simp_all add: fresh_zero_perm)
   587   by (simp_all add: fresh_zero_perm)
   588 
   588 
   589 lemma alpha_gen_sym:
   589 lemma alpha_gen_sym:
   590   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
   590   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
       
   591   and     b: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
   591   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
   592   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
   592   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
   593   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
   593   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
   594   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
       
   595   unfolding alphas fresh_star_def
       
   596   apply (erule_tac [1] conjE)+
       
   597   apply (erule_tac [2] conjE)+
       
   598   apply (erule_tac [3] conjE)+
   594   using a
   599   using a
   595   unfolding alphas
   600   apply (simp_all add: fresh_minus_perm)
   596   unfolding fresh_star_def
   601   apply (rotate_tac [!] -1)
   597   by (auto simp add:  fresh_minus_perm)
   602   apply (drule_tac [!] p="-p" in b)
   598 
   603   apply (simp_all)
       
   604   apply (metis permute_minus_cancel(2))
       
   605   apply (metis permute_minus_cancel(2))
       
   606   done
   599 lemma alpha_gen_trans:
   607 lemma alpha_gen_trans:
   600   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
   608   assumes a: "(\<forall>c. R y c \<longrightarrow> R (p \<bullet> x) c)"
       
   609   and b: "R (p \<bullet> x) y"
       
   610   and c: "R (q \<bullet> y) z"
       
   611   and d: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
   601   shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
   612   shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
   602   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
   613   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
   603   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
   614   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
   604   using a 
       
   605   unfolding alphas
   615   unfolding alphas
   606   unfolding fresh_star_def
   616   unfolding fresh_star_def
   607   by (simp_all add: fresh_plus_perm)
   617   apply (simp_all add: fresh_plus_perm)
       
   618   apply (metis a c d permute_minus_cancel(2))+
       
   619   done
   608 
   620 
   609 lemma alpha_gen_eqvt:
   621 lemma alpha_gen_eqvt:
   610   assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
   622   assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
   611   and     b: "p \<bullet> (f x) = f (p \<bullet> x)"
   623   and     b: "p \<bullet> (f x) = f (p \<bullet> x)"
   612   and     c: "p \<bullet> (f y) = f (p \<bullet> y)"
   624   and     c: "p \<bullet> (f y) = f (p \<bullet> y)"