equal
deleted
inserted
replaced
31 apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> xa = xa") |
31 apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> xa = xa") |
32 apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute) |
32 apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute) |
33 apply (simp_all add: swap_fresh_fresh) |
33 apply (simp_all add: swap_fresh_fresh) |
34 done |
34 done |
35 |
35 |
36 termination |
36 termination (eqvt) by lexicographic_order |
37 by (relation "measure (\<lambda>(t, _, _). size t)") |
|
38 (simp_all add: lt.size) |
|
39 |
|
40 lemma subst_eqvt[eqvt]: |
|
41 shows "p\<bullet>(M[V/(x::name)]) = (p\<bullet>M)[(p\<bullet>V)/(p\<bullet>x)]" |
|
42 by (induct M V x rule: subst.induct) (simp_all) |
|
43 |
37 |
44 lemma forget[simp]: |
38 lemma forget[simp]: |
45 shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M" |
39 shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M" |
46 by (nominal_induct M avoiding: x s rule: lt.strong_induct) |
40 by (nominal_induct M avoiding: x s rule: lt.strong_induct) |
47 (auto simp add: lt.fresh fresh_at_base) |
41 (auto simp add: lt.fresh fresh_at_base) |
58 | "isValue (A $ B) = False" |
52 | "isValue (A $ B) = False" |
59 unfolding eqvt_def isValue_graph_def |
53 unfolding eqvt_def isValue_graph_def |
60 by (perm_simp, auto) |
54 by (perm_simp, auto) |
61 (erule lt.exhaust, auto) |
55 (erule lt.exhaust, auto) |
62 |
56 |
63 termination |
57 termination (eqvt) |
64 by (relation "measure size") |
58 by (relation "measure size") (simp_all) |
65 (simp_all add: lt.size) |
|
66 |
59 |
67 lemma is_Value_eqvt[eqvt]: |
60 lemma is_Value_eqvt[eqvt]: |
68 shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)" |
61 shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)" |
69 by (induct M rule: lt.induct) (simp_all add: eqvts) |
62 by (induct M rule: lt.induct) (simp_all add: eqvts) |
70 |
63 |