163 done |
163 done |
164 |
164 |
165 lemma rfv_rsp: "(alpha ===> op =) rfv rfv" |
165 lemma rfv_rsp: "(alpha ===> op =) rfv rfv" |
166 sorry |
166 sorry |
167 |
167 |
|
168 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
|
169 apply (auto) |
|
170 apply (erule alpha.cases) |
|
171 apply (simp_all add: rlam.inject alpha_refl) |
|
172 done |
|
173 |
168 ML {* val qty = @{typ "lam"} *} |
174 ML {* val qty = @{typ "lam"} *} |
169 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
175 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
170 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
176 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
171 @{thms ho_all_prs ho_ex_prs} *} |
177 @{thms ho_all_prs ho_ex_prs} *} |
172 |
178 |
184 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
190 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
185 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
191 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
186 |
192 |
187 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
193 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
188 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} |
194 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} |
|
195 |
|
196 ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *} |
189 |
197 |
190 local_setup {* |
198 local_setup {* |
191 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
199 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
192 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
200 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
193 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
201 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
194 Quotient.note (@{binding "a1"}, a1) #> snd #> |
202 Quotient.note (@{binding "a1"}, a1) #> snd #> |
195 Quotient.note (@{binding "a2"}, a2) #> snd #> |
203 Quotient.note (@{binding "a2"}, a2) #> snd #> |
196 Quotient.note (@{binding "a3"}, a3) #> snd #> |
204 Quotient.note (@{binding "a3"}, a3) #> snd #> |
197 Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #> |
205 Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #> |
198 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd |
206 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd #> |
|
207 Quotient.note (@{binding "var_inject"}, var_inject) #> snd |
199 *} |
208 *} |
200 |
209 |
201 thm alpha.cases |
210 thm alpha.cases |
202 thm alpha_cases |
211 thm alpha_cases |
203 thm alpha.induct |
212 thm alpha.induct |
204 thm alpha_induct |
213 thm alpha_induct |
205 |
|
206 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
|
207 apply (auto) |
|
208 apply (erule alpha.cases) |
|
209 apply (simp_all add: rlam.inject alpha_refl) |
|
210 done |
|
211 |
|
212 ML {* val var_inject = Toplevel.program (fn () => lift_thm_lam @{context} @{thm rvar_inject}) *} |
|
213 |
|
214 local_setup {* |
|
215 Quotient.note (@{binding "var_inject"}, var_inject) #> snd |
|
216 *} |
|
217 |
214 |
218 lemma var_supp: |
215 lemma var_supp: |
219 shows "supp (Var a) = ((supp a)::name set)" |
216 shows "supp (Var a) = ((supp a)::name set)" |
220 apply(simp add: supp_def) |
217 apply(simp add: supp_def) |
221 apply(simp add: pi_var) |
218 apply(simp add: pi_var) |