Quot/Nominal/LamEx2.thy
changeset 1024 b3deb964ad26
parent 1023 7c12f5476d1b
child 1025 559419060d99
equal deleted inserted replaced
1023:7c12f5476d1b 1024:b3deb964ad26
   118   assumes "rLam a t \<approx> rLam b s"
   118   assumes "rLam a t \<approx> rLam b s"
   119   shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))"
   119   shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))"
   120 using assms
   120 using assms
   121 apply(erule_tac alpha.cases)
   121 apply(erule_tac alpha.cases)
   122 apply(auto)
   122 apply(auto)
   123 done
       
   124 
       
   125 lemma alpha_gen_eqvt_atom:
       
   126   assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
       
   127   shows "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s) \<Longrightarrow> \<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
       
   128 apply(erule exE)
       
   129 apply(rule_tac x="pi \<bullet> pia" in exI)
       
   130 apply(simp add: alpha_gen.simps)
       
   131 apply(erule conjE)+
       
   132 apply(rule conjI)+
       
   133 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
       
   134 apply(simp add: a[symmetric] atom_eqvt eqvts)
       
   135 apply(rule conjI)
       
   136 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
       
   137 apply(simp add: a[symmetric] eqvts atom_eqvt)
       
   138 apply(subst permute_eqvt[symmetric])
       
   139 apply(simp)
       
   140 done
   123 done
   141 
   124 
   142 text {* should be automatic with new version of eqvt-machinery *}
   125 text {* should be automatic with new version of eqvt-machinery *}
   143 lemma alpha_eqvt:
   126 lemma alpha_eqvt:
   144   shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
   127   shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"