equal
deleted
inserted
replaced
155 apply (simp_all add: perm_zero_ok perm_add_ok) |
155 apply (simp_all add: perm_zero_ok perm_add_ok) |
156 done |
156 done |
157 |
157 |
158 end |
158 end |
159 |
159 |
160 lemmas ALPHA_kind_ALPHA_ty_ALPHA_trm_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
160 (* |
161 |
161 Lifts, but slow and not needed?. |
162 lemmas kind_ty_trm_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
162 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
163 *) |
|
164 |
|
165 lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
163 |
166 |
164 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
167 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
165 |
168 |
166 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
169 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
167 |
170 |
205 "supp (CONS i) = {atom i}" |
208 "supp (CONS i) = {atom i}" |
206 "supp (VAR x) = {atom x}" |
209 "supp (VAR x) = {atom x}" |
207 "supp (APP M N) = supp M \<union> supp N" |
210 "supp (APP M N) = supp M \<union> supp N" |
208 "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
211 "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
209 apply(simp_all (no_asm) add: supp_def) |
212 apply(simp_all (no_asm) add: supp_def) |
210 apply(simp_all only: kind_ty_trm_INJECT Abs_eq_iff alpha_gen) |
213 apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen) |
211 apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric]) |
214 apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric]) |
212 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute) |
215 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute) |
213 apply(simp_all add: supp_at_base[simplified supp_def]) |
216 apply(simp_all add: supp_at_base[simplified supp_def]) |
214 done |
217 done |
215 |
218 |