26 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
27 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
27 where |
28 where |
28 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
29 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
29 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
30 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
30 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
31 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
|
32 |
|
33 print_theorems |
31 |
34 |
32 quotient lam = rlam / alpha |
35 quotient lam = rlam / alpha |
33 sorry |
36 sorry |
34 |
37 |
35 print_quotients |
38 print_quotients |
174 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *} |
177 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *} |
175 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *} |
178 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *} |
176 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} |
179 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} |
177 |
180 |
178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
181 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
179 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} |
182 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
183 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
181 |
184 |
182 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
185 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
183 |
186 |
184 local_setup {* |
187 local_setup {* |
277 |
281 |
278 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
282 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
279 |
283 |
280 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
284 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
281 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
285 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
282 |
|
283 ML {* |
|
284 |
|
285 |
|
286 *} |
|
287 |
|
288 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *} |
286 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *} |
|
287 ML {* val thm = |
|
288 @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *} |
|
289 ML {* val t_a = simp_allex_prs quot [thm] t_t *} |
289 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
290 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
290 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
291 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
291 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_t *} |
292 |
292 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
293 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_a *} |
293 ML {* val thm = |
|
294 @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]], symmetric]} *} |
|
295 ML {* val t_a1 = eqsubst_thm @{context} [thm] t_a *} |
|
296 ML {* val defs_sym = add_lower_defs @{context} defs; *} |
294 ML {* val defs_sym = add_lower_defs @{context} defs; *} |
297 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a1 *} |
295 ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *} |
|
296 ML t_l |
|
297 ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *} |
|
298 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *} |
298 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
299 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
299 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} |
300 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} |
300 ML {* val t_r2 = repeat_eqsubst_thm @{context} @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} |
301 ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} |
301 ML {* val t_r3 = repeat_eqsubst_thm @{context} @{thms id_apply} t_r2 *} |
302 ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *} |
302 |
|
303 ML {* val alpha_induct = ObjectLogic.rulify t_r3 *} |
303 ML {* val alpha_induct = ObjectLogic.rulify t_r3 *} |
304 |
304 |
305 local_setup {* |
305 local_setup {* |
306 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd |
306 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd |
307 *} |
307 *} |
308 |
308 |
|
309 thm alpha_induct |
|
310 thm alpha.induct |
|
311 |
|
312 lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)" |
|
313 apply (rule alpha.cases) |
|
314 apply (assumption) |
|
315 apply (assumption) |
|
316 apply (simp_all) |
|
317 apply (cases "a = b") |
|
318 apply (simp_all) |
|
319 apply (cases "ba = b") |
|
320 apply (simp_all) |
|
321 |
|
322 |
|
323 lemma var_inject_test: |
|
324 fixes a b |
|
325 assumes a: "Var a = Var b" |
|
326 shows "(a = b)" |
|
327 using a apply (cases "a = b") |
|
328 apply (simp_all) |
|
329 apply (rule_tac x="Var a" and xa = "Var b" in alpha_cases) |
|
330 apply (rule a) |
|
331 |
|
332 |
309 lemma |
333 lemma |
310 assumes a: "(a::lam) = b" |
334 assumes a: "(x::lam) = y" |
311 shows "False" |
335 shows "P x y" |
312 using a |
336 apply (induct rule: alpha_induct) |
313 apply (rule alpha_induct) |
337 apply (rule a) |
314 |
338 thm alpha.induct |
|
339 thm alpha_induct |
315 fun |
340 fun |
316 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
341 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
317 where |
342 where |
318 "option_map f (nSome x) = nSome (f x)" |
343 "option_map f (nSome x) = nSome (f x)" |
319 | "option_map f nNone = nNone" |
344 | "option_map f nNone = nNone" |