165 ML {* val consts = lookup_quot_consts defs *} |
165 ML {* val consts = lookup_quot_consts defs *} |
166 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *} |
166 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *} |
167 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
167 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
168 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
168 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
169 |
169 |
170 ML {* lift_thm_lam @{context} @{thm pi_var_com} *} |
170 ML {* val pi_var = lift_thm_lam @{context} @{thm pi_var_com} *} |
171 ML {* lift_thm_lam @{context} @{thm pi_app_com} *} |
171 ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *} |
172 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *} |
172 ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *} |
173 |
173 |
174 ML {* lift_thm_lam @{context} @{thm rfv_var} *} |
174 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *} |
175 ML {* lift_thm_lam @{context} @{thm rfv_app} *} |
175 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *} |
176 ML {* lift_thm_lam @{context} @{thm rfv_lam} *} |
176 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} |
177 |
177 |
178 ML {* lift_thm_lam @{context} @{thm a3} *} |
178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
|
179 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} |
|
180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
|
181 |
|
182 |
|
183 local_setup {* |
|
184 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
|
185 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
|
186 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
|
187 Quotient.note (@{binding "a1"}, a1) #> snd #> |
|
188 Quotient.note (@{binding "a2"}, a2) #> snd #> |
|
189 Quotient.note (@{binding "a3"}, a3) #> snd |
|
190 *} |
|
191 |
|
192 thm alpha.cases |
|
193 |
|
194 thm rlam.inject |
|
195 thm pi_var |
|
196 |
|
197 lemma var_inject: |
|
198 shows "(Var a = Var b) = (a = b)" |
|
199 sorry |
|
200 |
|
201 lemma var_supp: |
|
202 shows "supp (Var a) = ((supp a)::name set)" |
|
203 apply(simp add: supp_def) |
|
204 apply(simp add: pi_var) |
|
205 apply(simp add: var_inject) |
|
206 done |
|
207 |
|
208 lemma var_fresh: |
|
209 fixes a::"name" |
|
210 shows "(a\<sharp>(Var b)) = (a\<sharp>b)" |
|
211 apply(simp add: fresh_def) |
|
212 apply(simp add: var_supp) |
|
213 done |
179 |
214 |
180 |
215 |
181 |
216 |
182 |
217 |
183 |
218 |