286 done |
286 done |
287 |
287 |
288 |
288 |
289 termination (eqvt) by lexicographic_order |
289 termination (eqvt) by lexicographic_order |
290 |
290 |
291 thm subst_substs.eqvt[no_vars] |
|
292 thm subst_def |
|
293 thm substs_def |
|
294 thm Sum_Type.Projr.simps |
|
295 |
|
296 lemma |
|
297 shows "(p \<bullet> subst x y) = subst (p \<bullet> x) (p \<bullet> y)" |
|
298 and "(p \<bullet> substs x' y') = substs (p \<bullet> x') (p \<bullet> y')" |
|
299 unfolding subst_def substs_def |
|
300 thm permute_fun_app_eq |
|
301 thm Sum_Type.Projl_def sum_rec_def |
|
302 apply(simp add: permute_fun_def) |
|
303 unfolding subst_substs_sumC_def |
|
304 thm subst_substs.eqvt |
|
305 apply(case_tac x) |
|
306 apply(simp) |
|
307 apply(case_tac a) |
|
308 apply(simp) |
|
309 thm subst_def |
|
310 apply(simp) |
|
311 |
291 |
312 section {* defined as two separate nominal datatypes *} |
292 section {* defined as two separate nominal datatypes *} |
313 |
293 |
314 nominal_datatype ty2 = |
294 nominal_datatype ty2 = |
315 Var2 "name" |
295 Var2 "name" |
381 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)" |
361 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)" |
382 unfolding eqvt_def substs2_graph_def |
362 unfolding eqvt_def substs2_graph_def |
383 apply (rule, perm_simp, rule) |
363 apply (rule, perm_simp, rule) |
384 apply auto[2] |
364 apply auto[2] |
385 apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) |
365 apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) |
386 apply auto |
366 apply auto[1] |
|
367 apply(simp) |
|
368 apply(erule conjE) |
387 apply (erule Abs_res_fcb) |
369 apply (erule Abs_res_fcb) |
388 apply (simp add: Abs_fresh_iff) |
370 apply (simp add: Abs_fresh_iff) |
389 apply (simp add: Abs_fresh_iff) |
371 apply(simp add: fresh_def) |
390 apply auto[1] |
372 apply(simp add: supp_Abs) |
391 apply (simp add: fresh_def fresh_star_def) |
373 apply(rule impI) |
392 apply (rule contra_subsetD[OF supp_subst]) |
374 apply(subgoal_tac "x \<notin> supp \<theta>") |
393 apply simp |
375 prefer 2 |
394 apply blast |
376 apply(auto simp add: fresh_star_def fresh_def)[1] |
|
377 apply(subgoal_tac "x \<in> supp t") |
|
378 using supp_subst |
|
379 apply(blast) |
|
380 using supp_subst |
|
381 apply(blast) |
395 apply clarify |
382 apply clarify |
396 apply (simp add: subst_eqvt) |
383 apply (simp add: subst2.eqvt) |
397 apply (subst Abs_eq_iff) |
384 apply (subst Abs_eq_iff) |
398 apply (rule_tac x="0::perm" in exI) |
385 apply (rule_tac x="0::perm" in exI) |
399 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
386 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
400 apply (simp add: alphas fresh_star_zero) |
387 apply (simp add: alphas fresh_star_zero) |
401 apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
388 apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
413 apply (rule perm_supp_eq) |
400 apply (rule perm_supp_eq) |
414 apply (simp add: fresh_def fresh_star_def) |
401 apply (simp add: fresh_def fresh_star_def) |
415 apply blast |
402 apply blast |
416 done |
403 done |
417 |
404 |
418 |
|
419 text {* Some Tests about Alpha-Equality *} |
405 text {* Some Tests about Alpha-Equality *} |
420 |
406 |
421 lemma |
407 lemma |
422 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
408 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
423 apply(simp add: ty_tys.eq_iff Abs_eq_iff) |
409 apply(simp add: ty_tys.eq_iff Abs_eq_iff) |