equal
deleted
inserted
replaced
15 rfv_var: "rfv (rVar a) = {a}" |
15 rfv_var: "rfv (rVar a) = {a}" |
16 | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
16 | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
17 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
17 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
18 |
18 |
19 overloading |
19 overloading |
20 perm_rlam \<equiv> "perm :: 'x prm \<Rightarrow> rlam \<Rightarrow> rlam" (unchecked) |
20 perm_rlam \<equiv> "perm :: 'x prm \<Rightarrow> rlam \<Rightarrow> rlam" (unchecked) |
21 begin |
21 begin |
22 |
22 |
23 fun |
23 fun |
24 perm_rlam |
24 perm_rlam |
25 where |
25 where |
61 quotient_type lam = rlam / alpha |
61 quotient_type lam = rlam / alpha |
62 by (rule alpha_equivp) |
62 by (rule alpha_equivp) |
63 |
63 |
64 |
64 |
65 quotient_definition |
65 quotient_definition |
66 "Var :: name \<Rightarrow> lam" |
66 "Var :: name \<Rightarrow> lam" |
67 as |
67 as |
68 "rVar" |
68 "rVar" |
69 |
69 |
70 quotient_definition |
70 quotient_definition |
71 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
71 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
72 as |
72 as |
73 "rApp" |
73 "rApp" |
74 |
74 |
75 quotient_definition |
75 quotient_definition |
76 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
76 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
77 as |
77 as |
78 "rLam" |
78 "rLam" |
79 |
79 |
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 |
85 thm Var_def |
86 thm App_def |
86 thm App_def |
153 (* this is probably only true if some type conditions are imposed *) |
153 (* this is probably only true if some type conditions are imposed *) |
154 sorry |
154 sorry |
155 |
155 |
156 lemma rVar_rsp[quot_respect]: |
156 lemma rVar_rsp[quot_respect]: |
157 "(op = ===> alpha) rVar rVar" |
157 "(op = ===> alpha) rVar rVar" |
158 by (auto intro: a1) |
158 by (auto intro: a1) |
159 |
159 |
160 lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp" |
160 lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp" |
161 by (auto intro: a2) |
161 by (auto intro: a2) |
162 |
162 |
163 lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam" |
163 lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam" |
164 apply(auto) |
164 apply(auto) |
165 apply(rule a3) |
165 apply(rule a3) |
166 apply(simp add: helper) |
166 apply(simp add: helper) |
170 lemma rfv_rsp[quot_respect]: |
170 lemma rfv_rsp[quot_respect]: |
171 "(alpha ===> op =) rfv rfv" |
171 "(alpha ===> op =) rfv rfv" |
172 sorry |
172 sorry |
173 |
173 |
174 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
174 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
175 apply (auto) |
175 apply (auto) |
176 apply (erule alpha.cases) |
176 apply (erule alpha.cases) |
177 apply (simp_all add: rlam.inject alpha_refl) |
177 apply (simp_all add: rlam.inject alpha_refl) |
178 done |
178 done |
179 |
|
180 |
179 |
181 lemma pi_var1: |
180 lemma pi_var1: |
182 fixes pi::"'x prm" |
181 fixes pi::"'x prm" |
183 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
182 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
184 by (lifting pi_var_eqvt1) |
183 by (lifting pi_var_eqvt1) |