reverted back to the old version of the equivariance lemma for ALL
authorurbanc
Fri Sep 14 13:32:07 2007 +0200 (2007-09-14)
changeset 245727be5353ec4bd
parent 24571 a6d0428dea8e
child 24573 5bbdc9b60648
reverted back to the old version of the equivariance lemma for ALL
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Sep 13 23:58:38 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Fri Sep 14 13:32:07 2007 +0200
     1.3 @@ -1766,7 +1766,6 @@
     1.4  
     1.5  section {* equivaraince for some connectives *}
     1.6  
     1.7 -(*
     1.8  lemma pt_all_eqvt:
     1.9    fixes  pi :: "'x prm"
    1.10    and     x :: "'a"
    1.11 @@ -1777,18 +1776,6 @@
    1.12  apply(drule_tac x="pi\<bullet>x" in spec)
    1.13  apply(simp add: pt_rev_pi[OF pt, OF at])
    1.14  done
    1.15 -*)
    1.16 -
    1.17 -lemma pt_all_eqvt:
    1.18 -  fixes  pi :: "'x prm"
    1.19 -  and     x :: "'a"
    1.20 -  assumes pt: "pt TYPE('a) TYPE('x)"
    1.21 -  and     at: "at TYPE('x)"
    1.22 -  shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). P ((rev pi)\<bullet>x))"
    1.23 -apply(auto simp add: perm_bool)
    1.24 -apply(drule_tac x="pi\<bullet>x" in spec)
    1.25 -apply(simp add: pt_rev_pi[OF pt, OF at])
    1.26 -done
    1.27  
    1.28  lemma pt_ex_eqvt:
    1.29    fixes  pi :: "'x prm"