88 "domain (X#\<Gamma>) = {fst X}\<union>(domain \<Gamma>)" |
88 "domain (X#\<Gamma>) = {fst X}\<union>(domain \<Gamma>)" |
89 |
89 |
90 lemma domain_eqvt: |
90 lemma domain_eqvt: |
91 fixes pi::"tyvrs prm" |
91 fixes pi::"tyvrs prm" |
92 shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)" |
92 shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)" |
93 by (induct \<Gamma>, auto simp add: perm_set_def) |
93 by (induct \<Gamma>, simp_all add: perm_empty perm_insert perm_fst) |
94 |
94 |
95 lemma finite_domain: |
95 lemma finite_domain: |
96 shows "finite (domain \<Gamma>)" |
96 shows "finite (domain \<Gamma>)" |
97 by (induct \<Gamma>, auto) |
97 by (induct \<Gamma>, auto) |
98 |
98 |
326 hence "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" |
326 hence "supp S \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" |
327 and "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: domain_supp closed_in_def) |
327 and "supp T \<subseteq> ((supp (domain \<Gamma>))::tyvrs set)" by (simp_all add: domain_supp closed_in_def) |
328 ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def) |
328 ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def) |
329 qed |
329 qed |
330 |
330 |
331 text {* Two silly lemmas that are helpful for showing that @{text "subtype_of"} is |
|
332 equivariant. They are needed until we have a tactic that shows the property |
|
333 of equivariance automatically. *} |
|
334 |
|
335 lemma silly_eqvt1: |
|
336 fixes X::"'a::pt_tyvrs" |
|
337 and S::"'b::pt_tyvrs" |
|
338 and pi::"tyvrs prm" |
|
339 shows "(X,S) \<in> set \<Gamma> \<Longrightarrow> (pi\<bullet>X,pi\<bullet>S) \<in> set (pi\<bullet>\<Gamma>)" |
|
340 apply(drule_tac pi="pi" in pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
341 apply(simp add: pt_list_set_pi[OF pt_tyvrs_inst]) |
|
342 done |
|
343 |
|
344 lemma silly_eqvt2: |
|
345 fixes X::"tyvrs" |
|
346 and pi::"tyvrs prm" |
|
347 shows "X \<in> (domain \<Gamma>) \<Longrightarrow> (pi\<bullet>X) \<in> (domain (pi\<bullet>\<Gamma>))" |
|
348 apply(drule_tac pi="pi" in pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]) |
|
349 apply(simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst] ) |
|
350 done |
|
351 |
|
352 lemma subtype_eqvt: |
331 lemma subtype_eqvt: |
353 fixes pi::"tyvrs prm" |
332 fixes pi::"tyvrs prm" |
354 shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" |
333 shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)" |
355 apply(erule subtype_of.induct) |
334 apply(erule subtype_of.induct) |
356 apply(force intro: valid_eqvt closed_in_eqvt) |
335 apply(force intro: valid_eqvt closed_in_eqvt) |
357 apply(force intro: closed_in_eqvt valid_eqvt silly_eqvt1) |
336 apply(force intro!: S_Var |
358 apply(force intro: valid_eqvt silly_eqvt2) |
337 intro: closed_in_eqvt valid_eqvt |
|
338 dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst] |
|
339 simp add: pt_list_set_pi[OF pt_tyvrs_inst, symmetric]) |
|
340 apply(force intro: valid_eqvt |
|
341 dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst] |
|
342 simp add: domain_eqvt) |
359 apply(force) |
343 apply(force) |
360 apply(force intro!: S_Forall simp add: fresh_prod fresh_eqvt) |
344 apply(force intro!: S_Forall simp add: fresh_prod fresh_eqvt) |
361 done |
345 done |
362 |
346 |
363 text {* The most painful part of the subtyping definition is the strengthening of the |
347 text {* The most painful part of the subtyping definition is the strengthening of the |