equal
deleted
inserted
replaced
176 by (rule alpha_equivp) |
176 by (rule alpha_equivp) |
177 |
177 |
178 |
178 |
179 quotient_definition |
179 quotient_definition |
180 "Var :: name \<Rightarrow> lam" |
180 "Var :: name \<Rightarrow> lam" |
181 as |
181 is |
182 "rVar" |
182 "rVar" |
183 |
183 |
184 quotient_definition |
184 quotient_definition |
185 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
185 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
186 as |
186 is |
187 "rApp" |
187 "rApp" |
188 |
188 |
189 quotient_definition |
189 quotient_definition |
190 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
190 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
191 as |
191 is |
192 "rLam" |
192 "rLam" |
193 |
193 |
194 quotient_definition |
194 quotient_definition |
195 "fv :: lam \<Rightarrow> name set" |
195 "fv :: lam \<Rightarrow> name set" |
196 as |
196 is |
197 "rfv" |
197 "rfv" |
198 |
198 |
199 (* definition of overloaded permutation function *) |
199 (* definition of overloaded permutation function *) |
200 (* for the lifted type lam *) |
200 (* for the lifted type lam *) |
201 overloading |
201 overloading |
202 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
202 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
203 begin |
203 begin |
204 |
204 |
205 quotient_definition |
205 quotient_definition |
206 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
206 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
207 as |
207 is |
208 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
208 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
209 |
209 |
210 end |
210 end |
211 |
211 |
212 lemma perm_rsp[quot_respect]: |
212 lemma perm_rsp[quot_respect]: |