18 rfv_var: "rfv (rVar a) = {a}" |
18 rfv_var: "rfv (rVar a) = {a}" |
19 | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
19 | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
20 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
20 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
21 sorry |
21 sorry |
22 |
22 |
23 termination rfv sorry |
23 termination rfv sorry |
24 |
24 |
25 inductive |
25 inductive |
26 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
26 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
27 where |
27 where |
28 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
28 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
154 apply(simp add: pt_name1) |
154 apply(simp add: pt_name1) |
155 apply(assumption) |
155 apply(assumption) |
156 apply(simp add: abs_fresh) |
156 apply(simp add: abs_fresh) |
157 done |
157 done |
158 |
158 |
|
159 lemma rfv_rsp: "(alpha ===> op =) rfv rfv" |
|
160 sorry |
159 |
161 |
160 ML {* val qty = @{typ "lam"} *} |
162 ML {* val qty = @{typ "lam"} *} |
161 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
163 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
162 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *} |
164 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
163 ML {* val consts = lookup_quot_consts defs *} |
165 ML {* val consts = lookup_quot_consts defs *} |
164 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *} |
166 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *} |
165 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_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} *} |
166 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 *} |
167 |
169 |
168 ML {* lift_thm_lam @{context} @{thm pi_var_com} *} |
170 ML {* lift_thm_lam @{context} @{thm pi_var_com} *} |
169 ML {* lift_thm_lam @{context} @{thm pi_app_com} *} |
171 ML {* lift_thm_lam @{context} @{thm pi_app_com} *} |
170 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *} |
172 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *} |
|
173 |
|
174 ML {* lift_thm_lam @{context} @{thm rfv_var} *} |
|
175 ML {* lift_thm_lam @{context} @{thm rfv_app} *} |
|
176 ML {* lift_thm_lam @{context} @{thm rfv_lam} *} |
|
177 |
|
178 ML {* lift_thm_lam @{context} @{thm a3} *} |
|
179 |
|
180 |
|
181 |
|
182 |
|
183 |
|
184 |
|
185 |
|
186 |
|
187 |
|
188 |
|
189 |
171 |
190 |
172 fun |
191 fun |
173 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
192 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
174 where |
193 where |
175 "option_map f (nSome x) = nSome (f x)" |
194 "option_map f (nSome x) = nSome (f x)" |
239 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
258 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
240 thm a3 |
259 thm a3 |
241 ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *} |
260 ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *} |
242 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *} |
261 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *} |
243 |
262 |
244 ML {* val t_a = atomize_thm t_u *} |
263 (* T_U *) |
|
264 |
|
265 ML {* val t_a = atomize_thm @{thm rfv_var} *} |
245 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
266 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
|
267 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
|
268 |
246 ML {* fun r_mk_comb_tac_lam ctxt = |
269 ML {* fun r_mk_comb_tac_lam ctxt = |
247 r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms |
270 r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms |
248 *} |
271 *} |
249 |
272 |
250 instance lam :: fs_name |
273 instance lam :: fs_name |