equal
deleted
inserted
replaced
31 apply(simp add: perm_supp_eq fresh_star_Pair) |
31 apply(simp add: perm_supp_eq fresh_star_Pair) |
32 apply(simp add: eqvt_at_def) |
32 apply(simp add: eqvt_at_def) |
33 apply(simp add: perm_supp_eq fresh_star_Pair) |
33 apply(simp add: perm_supp_eq fresh_star_Pair) |
34 done |
34 done |
35 |
35 |
36 termination (eqvt) by lexicographic_order |
36 nominal_termination (eqvt) by lexicographic_order |
37 |
37 |
38 lemma forget[simp]: |
38 lemma forget[simp]: |
39 shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M" |
39 shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M" |
40 by (nominal_induct M avoiding: x s rule: lt.strong_induct) |
40 by (nominal_induct M avoiding: x s rule: lt.strong_induct) |
41 (auto simp add: lt.fresh fresh_at_base) |
41 (auto simp add: lt.fresh fresh_at_base) |
52 | "isValue (A $$ B) = False" |
52 | "isValue (A $$ B) = False" |
53 unfolding eqvt_def isValue_graph_aux_def |
53 unfolding eqvt_def isValue_graph_aux_def |
54 by (auto) |
54 by (auto) |
55 (erule lt.exhaust, auto) |
55 (erule lt.exhaust, auto) |
56 |
56 |
57 termination (eqvt) |
57 nominal_termination (eqvt) |
58 by (relation "measure size") (simp_all) |
58 by (relation "measure size") (simp_all) |
59 |
59 |
60 inductive |
60 inductive |
61 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
61 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
62 where |
62 where |