equal
deleted
inserted
replaced
66 inductive |
66 inductive |
67 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
67 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
68 where |
68 where |
69 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
69 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
70 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
70 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
71 | a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) |
71 | a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) |
72 \<Longrightarrow> rLam a t \<approx> rLam b s" |
72 \<Longrightarrow> rLam a t \<approx> rLam b s" |
73 |
73 |
74 (* should be automatic with new version of eqvt-machinery *) |
74 (* should be automatic with new version of eqvt-machinery *) |
75 lemma alpha_eqvt: |
75 lemma alpha_eqvt: |
76 fixes pi::"name prm" |
76 fixes pi::"name prm" |
493 apply - |
493 apply - |
494 apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)") |
494 apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)") |
495 apply(auto simp add: pi_size) |
495 apply(auto simp add: pi_size) |
496 done |
496 done |
497 |
497 |
|
498 (* |
|
499 function |
|
500 hom :: "(name \<Rightarrow> 'a) \<Rightarrow> |
|
501 (lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> |
|
502 ((name \<Rightarrow> lam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> lam \<Rightarrow> 'a" |
|
503 where |
|
504 "hom f_var f_app f_lam (Var x) = f_var x" |
|
505 | "hom f_var f_app f_lam (App l r) = f_app l r (hom f_var f_app f_lam l) (hom f_var f_app f_lam r)" |
|
506 | "hom f_var f_app f_lam (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom f_var f_app f_lam ([(a,b)] \<bullet> x))" |
|
507 apply(pat_completeness) |
|
508 apply(auto) |
|
509 done |
|
510 *) |
|
511 |
498 lemma term1_hom_rsp: |
512 lemma term1_hom_rsp: |
499 "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk> |
513 "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk> |
500 \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)" |
514 \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)" |
501 sorry |
515 sorry |
502 |
516 |