163 |
163 |
164 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
164 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
165 |
165 |
166 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
166 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
167 |
167 |
|
168 lemma supports: |
|
169 "{} supports TYP" |
|
170 "(supp (atom i)) supports (TCONST i)" |
|
171 "(supp A \<union> supp M) supports (TAPP A M)" |
|
172 "(supp (atom i)) supports (CONS i)" |
|
173 "(supp (atom x)) supports (VAR x)" |
|
174 "(supp M \<union> supp N) supports (APP M N)" |
|
175 "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)" |
|
176 "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)" |
|
177 "(supp ty \<union> supp (atom na) \<union> supp trm) supports (LAM ty na trm)" |
|
178 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh) |
|
179 apply(rule_tac [!] allI)+ |
|
180 apply(rule_tac [!] impI) |
|
181 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
|
182 apply(simp_all add: fresh_atom) |
|
183 done |
|
184 |
|
185 lemma kind_ty_trm_fs: |
|
186 "finite (supp (x\<Colon>kind))" |
|
187 "finite (supp (y\<Colon>ty))" |
|
188 "finite (supp (z\<Colon>trm))" |
|
189 apply(induct x and y and z rule: kind_ty_trm_inducts) |
|
190 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
|
191 apply(simp_all add: supp_atom) |
|
192 done |
|
193 |
|
194 instance kind and ty and trm :: fs |
|
195 apply(default) |
|
196 apply(simp_all only: kind_ty_trm_fs) |
|
197 done |
|
198 |
168 lemma supp_rkind_rty_rtrm_easy: |
199 lemma supp_rkind_rty_rtrm_easy: |
169 "supp TYP = {}" |
200 "supp TYP = {}" |
170 "supp (TCONST i) = {atom i}" |
201 "supp (TCONST i) = {atom i}" |
171 "supp (TAPP A M) = supp A \<union> supp M" |
202 "supp (TAPP A M) = supp A \<union> supp M" |
172 "supp (CONS i) = {atom i}" |
203 "supp (CONS i) = {atom i}" |
176 apply (simp_all only: kind_ty_trm_INJECT) |
207 apply (simp_all only: kind_ty_trm_INJECT) |
177 apply (simp_all only: supp_at_base[simplified supp_def]) |
208 apply (simp_all only: supp_at_base[simplified supp_def]) |
178 apply (simp_all add: Collect_imp_eq Collect_neg_eq) |
209 apply (simp_all add: Collect_imp_eq Collect_neg_eq) |
179 done |
210 done |
180 |
211 |
181 lemma supp_bind: |
|
182 "(supp (atom na, (ty, ki))) supports (KPI ty na ki)" |
|
183 "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)" |
|
184 "(supp (atom na, (ty, rtrm))) supports (LAM ty na rtrm)" |
|
185 apply(simp_all add: supports_def) |
|
186 apply(fold fresh_def) |
|
187 apply(simp_all add: fresh_Pair swap_fresh_fresh) |
|
188 apply(clarify) |
|
189 apply(subst swap_at_base_simps(3)) |
|
190 apply(simp_all add: fresh_atom) |
|
191 apply(clarify) |
|
192 apply(subst swap_at_base_simps(3)) |
|
193 apply(simp_all add: fresh_atom) |
|
194 apply(clarify) |
|
195 apply(subst swap_at_base_simps(3)) |
|
196 apply(simp_all add: fresh_atom) |
|
197 done |
|
198 |
|
199 lemma kind_ty_trm_fs: |
|
200 "finite (supp (x\<Colon>kind))" |
|
201 "finite (supp (y\<Colon>ty))" |
|
202 "finite (supp (z\<Colon>trm))" |
|
203 apply(induct x and y and z rule: kind_ty_trm_inducts) |
|
204 apply(simp_all add: supp_rkind_rty_rtrm_easy) |
|
205 apply(rule supports_finite) |
|
206 apply(rule supp_bind(1)) |
|
207 apply(simp add: supp_Pair supp_atom) |
|
208 apply(rule supports_finite) |
|
209 apply(rule supp_bind(2)) |
|
210 apply(simp add: supp_Pair supp_atom) |
|
211 apply(rule supports_finite) |
|
212 apply(rule supp_bind(3)) |
|
213 apply(simp add: supp_Pair supp_atom) |
|
214 done |
|
215 |
|
216 instance kind and ty and trm :: fs |
|
217 apply(default) |
|
218 apply(simp_all only: kind_ty_trm_fs) |
|
219 done |
|
220 |
|
221 lemma supp_fv: |
212 lemma supp_fv: |
222 "supp t1 = fv_kind t1" |
213 "supp t1 = fv_kind t1" |
223 "supp t2 = fv_ty t2" |
214 "supp t2 = fv_ty t2" |
224 "supp t3 = fv_trm t3" |
215 "supp t3 = fv_trm t3" |
225 apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts) |
216 apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts) |
226 apply (simp_all add: supp_rkind_rty_rtrm_easy) |
217 apply (simp_all add: supp_rkind_rty_rtrm_easy) |
227 apply (simp_all add: fv_kind_ty_trm) |
218 apply (simp_all add: fv_kind_ty_trm) |
228 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)") |
219 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)") |
229 apply(simp add: supp_Abs Set.Un_commute) |
220 apply(simp only: supp_Abs) |
230 apply(simp (no_asm) add: supp_def) |
221 apply(simp (no_asm) add: supp_def) |
231 apply(simp add: kind_ty_trm_INJECT) |
222 apply(simp add: kind_ty_trm_INJECT) |
232 apply(simp add: Abs_eq_iff) |
223 apply(simp add: Abs_eq_iff) |
233 apply(simp add: alpha_gen) |
224 apply(simp add: alpha_gen) |
234 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt) |
225 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt) |
235 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
226 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
236 apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)") |
227 apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)") |
237 apply(simp add: supp_Abs Set.Un_commute) |
228 apply(simp add: supp_Abs) |
238 apply(simp (no_asm) add: supp_def) |
229 apply(simp (no_asm) add: supp_def) |
239 apply(simp add: kind_ty_trm_INJECT) |
230 apply(simp add: kind_ty_trm_INJECT) |
240 apply(simp add: Abs_eq_iff) |
231 apply(simp add: Abs_eq_iff) |
241 apply(simp add: alpha_gen) |
232 apply(simp add: alpha_gen) |
242 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
233 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
243 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
234 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
244 apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)") |
235 apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)") |
245 apply(simp add: supp_Abs Set.Un_commute) |
236 apply(simp add: supp_Abs) |
246 apply(simp (no_asm) add: supp_def) |
237 apply(simp (no_asm) add: supp_def) |
247 apply(simp add: kind_ty_trm_INJECT) |
238 apply(simp add: kind_ty_trm_INJECT) |
248 apply(simp add: Abs_eq_iff) |
239 apply(simp add: Abs_eq_iff) |
249 apply(simp add: alpha_gen) |
240 apply(simp add: alpha_gen) |
250 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
241 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
251 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
242 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
252 done |
243 done |
253 |
244 |
254 (* Not needed anymore *) |
245 (* Not needed anymore *) |
255 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A" |
246 lemma supp_kpi: "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)" |
256 apply (simp add: permute_set_eq supp_def Abs_eq_iff kind_ty_trm_INJECT) |
247 apply (simp add: permute_set_eq supp_def Abs_eq_iff kind_ty_trm_INJECT) |
257 apply (simp add: alpha_gen supp_fv) |
248 apply (simp add: alpha_gen supp_fv) |
258 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute) |
249 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute) |
259 done |
250 done |
260 |
251 |