126 Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], |
131 Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], |
127 atac ]) |
132 atac ]) |
128 *} |
133 *} |
129 |
134 |
130 |
135 |
131 lemma |
136 lemma |
132 assumes a: "valid Gamma" |
137 assumes a: "valid Gamma" |
133 shows "valid (p \<bullet> Gamma)" |
138 shows "valid (p \<bullet> Gamma)" |
134 using a |
139 using a |
135 apply(induct) |
140 apply(induct) |
136 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
141 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
137 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
142 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
|
143 done |
|
144 |
|
145 lemma |
|
146 "(p \<bullet> valid) = valid" |
|
147 oops |
|
148 |
|
149 lemma temp[eqvt_raw]: |
|
150 "(p \<bullet> valid) \<equiv> valid" |
|
151 sorry |
|
152 |
|
153 inductive |
|
154 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
|
155 where |
|
156 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
|
157 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
|
158 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
|
159 |
|
160 lemma |
|
161 assumes a: "Gamma \<turnstile> t : T" |
|
162 shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)" |
|
163 using a |
|
164 apply(induct) |
|
165 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
|
166 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
|
167 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) |
138 done |
168 done |
139 |
169 |
140 declare permute_lam_raw.simps[eqvt] |
170 declare permute_lam_raw.simps[eqvt] |
141 |
171 |
142 thm alpha_gen_real_eqvt[no_vars] |
172 thm alpha_gen_real_eqvt[no_vars] |
171 apply(simp add: alphas) |
201 apply(simp add: alphas) |
172 apply(rule_tac p="- p" in permute_boolE) |
202 apply(rule_tac p="- p" in permute_boolE) |
173 apply(perm_simp permute_minus_cancel(2)) |
203 apply(perm_simp permute_minus_cancel(2)) |
174 oops |
204 oops |
175 |
205 |
|
206 thm alpha_lam_raw.intros[no_vars] |
|
207 |
|
208 inductive |
|
209 alpha_lam_raw' |
|
210 where |
|
211 "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)" |
|
212 | "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow> |
|
213 alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)" |
|
214 | "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow> |
|
215 alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" |
|
216 |
|
217 lemma |
|
218 assumes a: "alpha_lam_raw' t1 t2" |
|
219 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
|
220 using a |
|
221 apply(induct) |
|
222 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *}) |
|
223 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *}) |
|
224 apply(perm_strict_simp) |
|
225 apply(rule alpha_lam_raw'.intros) |
|
226 apply(simp add: alphas) |
|
227 apply(rule_tac p="- p" in permute_boolE) |
|
228 apply(perm_simp permute_minus_cancel(2)) |
|
229 oops |
176 |
230 |
177 |
231 |
178 section {* size function *} |
232 section {* size function *} |
179 |
233 |
180 lemma size_eqvt_raw: |
234 lemma size_eqvt_raw: |