181 apply(subst test) |
186 apply(subst test) |
182 back |
187 back |
183 back |
188 back |
184 apply(assumption) |
189 apply(assumption) |
185 apply(rule subst_substs_graph.intros) |
190 apply(rule subst_substs_graph.intros) |
|
191 apply (simp add: eqvts) |
|
192 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)") |
|
193 apply (simp add: image_eqvt eqvts_raw eqvts) |
|
194 apply (simp add: fresh_star_permute_iff) |
|
195 apply(perm_simp) |
|
196 apply(assumption) |
|
197 apply(simp (no_asm_use) only: eqvts) |
|
198 apply(subst test) |
|
199 back |
|
200 back |
|
201 apply(assumption) |
|
202 apply(rule subst_substs_graph.intros) |
|
203 apply (simp add: eqvts) |
|
204 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)") |
|
205 apply (simp add: image_eqvt eqvts_raw eqvts) |
|
206 apply (simp add: fresh_star_permute_iff) |
|
207 apply(perm_simp) |
|
208 apply(assumption) |
|
209 apply(simp) |
|
210 --"Eqvt done" |
|
211 apply (case_tac x) |
|
212 apply simp apply clarify |
|
213 apply (rule_tac y="b" in ty_tys.exhaust(1)) |
|
214 apply (auto simp add: ty_tys.eq_iff)[1] |
|
215 apply (auto simp add: ty_tys.eq_iff)[1] |
|
216 apply blast |
|
217 apply simp apply clarify |
|
218 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) |
|
219 apply (auto simp add: ty_tys.eq_iff)[1] |
|
220 apply (auto simp add: ty_tys.distinct) |
|
221 apply (auto simp add: ty_tys.eq_iff ty_tys.distinct)[2] |
|
222 --"LAST GOAL" |
|
223 thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff] |
|
224 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
|
225 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
|
226 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
186 defer |
227 defer |
187 apply(perm_simp) |
228 apply (simp add: eqvt_at_def subst_def) |
188 apply(assumption) |
229 apply rule |
189 apply(simp (no_asm_use) only: eqvts) |
230 apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)") |
190 apply(subst test) |
231 apply (subst test2) |
191 back |
232 apply (drule_tac x="(\<theta>', T)" in meta_spec) |
192 back |
233 apply assumption |
193 apply(assumption) |
234 apply simp |
194 apply(rule subst_substs_graph.intros) |
235 --"We require that for Inl it returns Inl. It doesn't work for undefined, but it does work for the following" |
|
236 apply (subgoal_tac "\<And>y. \<exists>z. (\<lambda>x. THE_default (sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined) x) (subst_substs_graph x)) (Inl y) = (Inl z)") |
|
237 prefer 2 |
|
238 apply (simp add: THE_default_def) |
|
239 apply (case_tac "Ex1 (subst_substs_graph (Inl y))") |
|
240 prefer 2 |
|
241 apply simp |
|
242 apply (simp add: the1_equality) |
|
243 apply auto[1] |
|
244 apply (erule_tac x="x" in allE) |
|
245 apply simp |
|
246 apply(cases rule: subst_substs_graph.cases) |
|
247 apply assumption |
|
248 apply (rule_tac x="lookup \<theta> X" in exI) |
|
249 apply clarify |
|
250 apply (rule the1_equality) |
|
251 apply metis apply assumption |
|
252 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1)))) |
|
253 (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI) |
|
254 apply clarify |
|
255 apply (rule the1_equality) |
|
256 apply metis apply assumption |
|
257 apply clarify |
|
258 --"This is exactly the assumption for the properly defined function" |
195 defer |
259 defer |
196 apply(perm_simp) |
260 apply (simp add: ty_tys.eq_iff) |
197 apply(assumption) |
261 apply (subst (asm) Abs_eq_iff2) |
198 apply(simp) |
262 apply (simp add: alpha_res.simps) |
199 apply(simp_all add: ty_tys.distinct) |
263 apply (clarify) |
|
264 apply (rule trans) |
|
265 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
266 apply(rule fresh_star_supp_conv) |
|
267 thm fresh_star_perm_set_conv |
|
268 apply(drule fresh_star_perm_set_conv) |
|
269 apply (rule finite_Diff) |
|
270 apply (rule finite_supp) |
|
271 apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* ([atom ` fset xs]res. subst \<theta>' T)") |
|
272 apply (metis Un_absorb2 fresh_star_Un) |
|
273 apply (simp add: fresh_star_Un) |
|
274 apply (rule conjI) |
|
275 apply (simp add: fresh_star_def) |
|
276 apply rule |
|
277 apply(simp (no_asm) only: Abs_fresh_iff) |
|
278 apply(clarify) |
|
279 apply blast |
200 defer |
280 defer |
201 apply(simp add: ty_tys.eq_iff) |
281 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
202 apply(simp add: ty_tys.eq_iff) |
282 prefer 2 |
203 apply(erule conjE)+ |
283 apply (rule perm_supp_eq) |
204 apply(simp add: ty_tys.eq_iff) |
284 apply (metis Un_absorb2 fresh_star_Un) |
205 apply(subst (asm) Abs_eq_iff2) |
285 apply simp |
206 apply(erule exE) |
286 --"Would work for 'set' and 'list' bindings, not sure how to do 'set+'." |
207 apply(simp add: alphas) |
|
208 apply(clarify) |
|
209 thm subst_def |
|
210 |
|
211 |
|
212 apply(assumption) |
|
213 apply(subst test) |
|
214 back |
|
215 apply(assumption) |
|
216 apply(perm_simp) |
|
217 apply(rule subst_substs_graph.intros) |
|
218 apply(assumption) |
|
219 apply(assumption) |
|
220 apply(subst test) |
|
221 back |
|
222 apply(assumption) |
|
223 apply(perm_simp) |
|
224 apply(rule subst_substs_graph.intros) |
|
225 apply(assumption) |
|
226 apply(assumption) |
|
227 apply(simp) |
|
228 |
|
229 |
|
230 apply(rotate_tac 1) |
|
231 apply(erule subst_substs_graph.cases) |
|
232 apply(subst test) |
|
233 back |
|
234 apply(assumption) |
|
235 |
|
236 |
|
237 apply(auto)[4] |
|
238 thm subst_substs_graph.cases |
|
239 thm subst_substs_graph.intros |
|
240 thm subst_substs_graph.intros(2)[THEN permute_boolI] |
|
241 term subst_substs_graph |
|
242 apply(simp only: eqvts) |
|
243 thm Projl.simps |
|
244 term Inl |
|
245 term Inr |
|
246 apply(perm_simp) |
|
247 thm subst_substs_graph.intros |
|
248 apply(simp add: permute_fun_def) |
|
249 thm Projl.simps |
|
250 oops |
287 oops |
251 |
288 |
252 |
289 |
253 section {* defined as two separate nominal datatypes *} |
290 section {* defined as two separate nominal datatypes *} |
254 |
291 |