equal
deleted
inserted
replaced
360 apply(simp add: var_supp1) |
360 apply(simp add: var_supp1) |
361 done |
361 done |
362 |
362 |
363 (* lemma hom_reg: *) |
363 (* lemma hom_reg: *) |
364 |
364 |
365 lemma hom: " |
365 lemma hom: |
366 \<exists>hom\<in>Respects (alpha ===> op =). ( |
366 "\<exists>hom\<in>Respects (alpha ===> op =). |
367 (\<forall>x. hom (rVar x) = f_var x) \<and> |
367 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
368 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
368 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
369 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
369 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
370 )" |
370 apply(rule_tac x="rlam_rec f_var f_app XX" in bexI) |
|
371 apply(rule conjI) |
|
372 apply(simp) |
|
373 apply(rule conjI) |
|
374 apply(simp) |
|
375 apply(simp) |
371 sorry |
376 sorry |
372 |
377 |
373 lemma hom_reg:" |
378 lemma hom_reg:" |
374 (\<exists>hom\<in>Respects (alpha ===> op =). |
379 (\<exists>hom\<in>Respects (alpha ===> op =). |
375 (\<forall>x. hom (rVar x) = f_var x) \<and> |
380 (\<forall>x. hom (rVar x) = f_var x) \<and> |
379 (\<forall>x. hom (rVar x) = f_var x) \<and> |
384 (\<forall>x. hom (rVar x) = f_var x) \<and> |
380 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
385 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
381 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
386 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
382 by(regularize) |
387 by(regularize) |
383 |
388 |
384 thm impE[OF hom_reg] |
|
385 lemma hom_pre:" |
389 lemma hom_pre:" |
386 (\<exists>hom. |
390 (\<exists>hom. |
387 (\<forall>x. hom (rVar x) = f_var x) \<and> |
391 (\<forall>x. hom (rVar x) = f_var x) \<and> |
388 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
392 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
389 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
393 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
391 apply (rule hom) |
395 apply (rule hom) |
392 apply (assumption) |
396 apply (assumption) |
393 done |
397 done |
394 |
398 |
395 lemma hom': |
399 lemma hom': |
396 "\<exists>hom. ( |
400 "\<exists>hom. |
397 (\<forall>x. hom (Var x) = f_var x) \<and> |
401 ((\<forall>x. hom (Var x) = f_var x) \<and> |
398 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
402 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
399 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
403 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
400 )" |
|
401 apply (lifting hom) |
404 apply (lifting hom) |
402 done |
405 done |
403 |
406 |
404 thm bex_reg_eqv_range[OF identity_equivp, of "alpha"] |
407 thm bex_reg_eqv_range[OF identity_equivp, of "alpha"] |
405 |
408 |