equal
deleted
inserted
replaced
173 quotient_type lam = rlam / alpha |
173 quotient_type lam = rlam / alpha |
174 by (rule alpha_equivp) |
174 by (rule alpha_equivp) |
175 |
175 |
176 quotient_definition |
176 quotient_definition |
177 "Var :: name \<Rightarrow> lam" |
177 "Var :: name \<Rightarrow> lam" |
178 as |
178 is |
179 "rVar" |
179 "rVar" |
180 |
180 |
181 quotient_definition |
181 quotient_definition |
182 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
182 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
183 as |
183 is |
184 "rApp" |
184 "rApp" |
185 |
185 |
186 quotient_definition |
186 quotient_definition |
187 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
187 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
188 as |
188 is |
189 "rLam" |
189 "rLam" |
190 |
190 |
191 quotient_definition |
191 quotient_definition |
192 "fv :: lam \<Rightarrow> atom set" |
192 "fv :: lam \<Rightarrow> atom set" |
193 as |
193 is |
194 "rfv" |
194 "rfv" |
195 |
195 |
196 lemma perm_rsp[quot_respect]: |
196 lemma perm_rsp[quot_respect]: |
197 "(op = ===> alpha ===> alpha) permute permute" |
197 "(op = ===> alpha ===> alpha) permute permute" |
198 apply(auto) |
198 apply(auto) |
237 instantiation lam :: pt |
237 instantiation lam :: pt |
238 begin |
238 begin |
239 |
239 |
240 quotient_definition |
240 quotient_definition |
241 "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam" |
241 "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam" |
242 as |
242 is |
243 "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam" |
243 "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam" |
244 |
244 |
245 lemma permute_lam [simp]: |
245 lemma permute_lam [simp]: |
246 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
246 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
247 and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |
247 and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |