equal
deleted
inserted
replaced
80 quotient_definition |
80 quotient_definition |
81 "fv :: lam \<Rightarrow> name set" |
81 "fv :: lam \<Rightarrow> name set" |
82 as |
82 as |
83 "rfv" |
83 "rfv" |
84 |
84 |
85 thm Var_def |
|
86 thm App_def |
|
87 thm Lam_def |
|
88 thm fv_def |
|
89 |
|
90 (* definition of overloaded permutation function *) |
85 (* definition of overloaded permutation function *) |
91 (* for the lifted type lam *) |
86 (* for the lifted type lam *) |
92 overloading |
87 overloading |
93 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
88 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
94 begin |
89 begin |
97 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
92 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
98 as |
93 as |
99 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
94 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
100 |
95 |
101 end |
96 end |
102 |
|
103 thm perm_lam_def |
|
104 |
97 |
105 (* lemmas that need to be lifted *) |
98 (* lemmas that need to be lifted *) |
106 lemma pi_var_eqvt1: |
99 lemma pi_var_eqvt1: |
107 fixes pi::"'x prm" |
100 fixes pi::"'x prm" |
108 shows "(pi \<bullet> rVar a) \<approx> rVar (pi \<bullet> a)" |
101 shows "(pi \<bullet> rVar a) \<approx> rVar (pi \<bullet> a)" |
365 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
358 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
366 apply(simp add: fresh_def) |
359 apply(simp add: fresh_def) |
367 apply(simp add: var_supp1) |
360 apply(simp add: var_supp1) |
368 done |
361 done |
369 |
362 |
370 (* TODO: make a proper definition of substitution *) |
|
371 definition |
|
372 subs :: "rlam \<Rightarrow> (name \<times> rlam) \<Rightarrow> rlam" ("_ \<guillemotleft>\<guillemotright> _" [70, 71] 70) |
|
373 where |
|
374 "x \<guillemotleft>\<guillemotright> S \<equiv> x" |
|
375 |
363 |
376 lemma " |
364 lemma " |
377 \<exists>hom\<in>Respects(alpha ===> op =). ( |
365 \<exists>hom \<in> Respects(alpha ===> op =). ( |
378 (\<forall>x. hom (rVar x) = var x) \<and> |
366 (\<forall>x. hom (rVar x) = f_var x) \<and> |
379 (\<forall>l r. hom (rApp l r) = app (hom l) (hom r)) \<and> |
367 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
380 (\<forall>x a. hom (rLam a x) = lam (\<lambda>y. hom (a \<guillemotleft>\<guillemotright> (x, rVar y)) (\<lambda>y. a \<guillemotleft>\<guillemotright> (x, rVar y)))) |
368 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) |
381 )" |
369 )" |
382 |
370 |
383 end |
371 end |