168 apply (erule alpha.cases) |
168 apply (erule alpha.cases) |
169 apply (simp_all add: rlam.inject alpha_refl) |
169 apply (simp_all add: rlam.inject alpha_refl) |
170 done |
170 done |
171 |
171 |
172 ML {* val qty = @{typ "lam"} *} |
172 ML {* val qty = @{typ "lam"} *} |
173 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
|
174 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
173 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
175 |
174 |
176 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
175 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
177 ML {* val consts = lookup_quot_consts defs *} |
|
178 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
176 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
179 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
177 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] [quot] *} |
180 |
178 |
181 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
179 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
182 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
180 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
183 done |
181 done |
184 |
182 |
210 apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *}) |
208 apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *}) |
211 done |
209 done |
212 |
210 |
213 lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa" |
211 lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa" |
214 apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) |
212 apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) |
|
213 apply (simp add:perm_lam_def) |
215 done |
214 done |
216 |
215 |
217 lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
216 lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
218 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
217 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
219 \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
218 \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
220 \<Longrightarrow> P" |
219 \<Longrightarrow> P" |
221 apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) |
220 apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) |
|
221 apply (simp add:perm_lam_def) |
222 done |
222 done |
223 |
223 |
224 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b); |
224 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b); |
225 \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
225 \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
226 \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. |
226 \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. |
227 \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk> |
227 \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk> |
228 \<Longrightarrow> qxb qx qxa" |
228 \<Longrightarrow> qxb qx qxa" |
229 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) |
229 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) |
|
230 apply (simp add:perm_lam_def) |
230 done |
231 done |
231 |
232 |
232 lemma var_inject: "(Var a = Var b) = (a = b)" |
233 lemma var_inject: "(Var a = Var b) = (a = b)" |
233 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) |
234 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) |
234 done |
235 done |
335 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
336 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
336 apply (simp only: perm_prs) |
337 apply (simp only: perm_prs) |
337 prefer 2 |
338 prefer 2 |
338 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
339 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
339 prefer 3 |
340 prefer 3 |
340 apply (tactic {* clean_tac @{context} [quot] defs 1 *}) |
341 apply (tactic {* clean_tac @{context} [quot] 1 *}) |
341 |
342 |
342 thm all_prs |
343 thm all_prs |
343 thm REP_ABS_RSP |
344 thm REP_ABS_RSP |
344 thm ball_reg_eqv_range |
345 thm ball_reg_eqv_range |
345 |
346 |