48 "(t1 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and> |
48 "(t1 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and> |
49 (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and> |
49 (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and> |
50 (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))" |
50 (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))" |
51 apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) |
51 apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) |
52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
53 apply (erule alpha_gen_compose_eqvt) |
53 apply (erule_tac [!] conjE)+ |
54 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
54 apply (erule_tac [!] exi[of _ _ "p"]) |
55 apply (erule alpha_gen_compose_eqvt) |
55 apply (erule_tac [!] alpha_gen_compose_eqvt) |
56 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
|
57 apply (erule alpha_gen_compose_eqvt) |
|
58 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
56 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
59 done |
57 done |
60 |
58 |
61 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
59 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
62 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
60 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
158 instance kind and ty and trm :: fs |
156 instance kind and ty and trm :: fs |
159 apply(default) |
157 apply(default) |
160 apply(simp_all only: kind_ty_trm_fs) |
158 apply(simp_all only: kind_ty_trm_fs) |
161 done |
159 done |
162 |
160 |
|
161 lemma ex_out: |
|
162 "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))" |
|
163 "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))" |
|
164 "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
165 "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
166 apply (blast)+ |
|
167 done |
|
168 |
163 lemma supp_eqs: |
169 lemma supp_eqs: |
164 "supp TYP = {}" |
170 "supp TYP = {}" |
165 "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)" |
171 "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)" |
166 "supp (TCONST i) = {atom i}" |
172 "supp (TCONST i) = {atom i}" |
167 "supp (TAPP A M) = supp A \<union> supp M" |
173 "supp (TAPP A M) = supp A \<union> supp M" |
168 "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)" |
174 "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)" |
169 "supp (CONS i) = {atom i}" |
175 "supp (CONS i) = {atom i}" |
170 "supp (VAR x) = {atom x}" |
176 "supp (VAR x) = {atom x}" |
171 "supp (APP M N) = supp M \<union> supp N" |
177 "supp (APP M N) = supp M \<union> supp N" |
172 "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
178 "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
173 apply(simp_all (no_asm) add: supp_def) |
179 apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt) |
174 apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen) |
180 apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen) |
175 apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric]) |
181 apply(simp_all only:ex_out) |
176 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute) |
182 apply(simp_all only: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts[symmetric]) |
177 apply(simp_all add: supp_at_base[simplified supp_def]) |
183 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
184 apply(simp_all add: supp_at_base[simplified supp_def] Un_commute) |
178 done |
185 done |
|
186 |
179 |
187 |
180 lemma supp_fv: |
188 lemma supp_fv: |
181 "supp t1 = fv_kind t1" |
189 "supp t1 = fv_kind t1" |
182 "supp t2 = fv_ty t2" |
190 "supp t2 = fv_ty t2" |
183 "supp t3 = fv_trm t3" |
191 "supp t3 = fv_trm t3" |