equal
deleted
inserted
replaced
369 |
369 |
370 (* not sure whether needed *) |
370 (* not sure whether needed *) |
371 lemma alpha_induct: |
371 lemma alpha_induct: |
372 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
372 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
373 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
373 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
374 \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
374 \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2) fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
375 \<Longrightarrow> qxb qx qxa" |
375 \<Longrightarrow> qxb qx qxa" |
376 unfolding alpha_gen by (lifting alpha.induct[unfolded alpha_gen]) |
376 unfolding alpha_gen by (lifting alpha.induct[unfolded alpha_gen]) |
377 |
377 |
378 (* should they lift automatically *) |
378 (* should they lift automatically *) |
379 lemma lam_inject [simp]: |
379 lemma lam_inject [simp]: |