equal
deleted
inserted
replaced
37 where |
37 where |
38 "height (Var x) = 1" |
38 "height (Var x) = 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
40 | "height (Lam [x].t) = height t + 1" |
40 | "height (Lam [x].t) = height t + 1" |
41 apply(simp add: eqvt_def height_graph_def) |
41 apply(simp add: eqvt_def height_graph_def) |
42 apply (rule, perm_simp, rule) |
|
43 apply(rule TrueI) |
42 apply(rule TrueI) |
44 apply(rule_tac y="x" in lam.exhaust) |
43 apply(rule_tac y="x" in lam.exhaust) |
45 apply(auto) |
44 apply(auto) |
46 apply(erule_tac c="()" in Abs_lst1_fcb2) |
45 apply(erule_tac c="()" in Abs_lst1_fcb2) |
47 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
46 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
67 apply(blast)+ |
66 apply(blast)+ |
68 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
67 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
69 apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
68 apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
70 apply(simp_all add: Abs_fresh_iff) |
69 apply(simp_all add: Abs_fresh_iff) |
71 apply(simp add: fresh_star_def fresh_Pair) |
70 apply(simp add: fresh_star_def fresh_Pair) |
72 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
71 apply(simp add: eqvt_at_def) |
73 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
72 apply(simp add: perm_supp_eq fresh_star_Pair) |
|
73 apply(simp add: eqvt_at_def) |
|
74 apply(simp add: perm_supp_eq fresh_star_Pair) |
74 done |
75 done |
75 |
76 |
76 termination (eqvt) |
77 termination (eqvt) |
77 by lexicographic_order |
78 by lexicographic_order |
78 |
79 |
80 assumes a: "atom z \<sharp> s" |
81 assumes a: "atom z \<sharp> s" |
81 and b: "z = y \<or> atom z \<sharp> t" |
82 and b: "z = y \<or> atom z \<sharp> t" |
82 shows "atom z \<sharp> t[y ::= s]" |
83 shows "atom z \<sharp> t[y ::= s]" |
83 using a b |
84 using a b |
84 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
85 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
85 (auto simp add: lam.fresh fresh_at_base) |
86 (auto simp add: fresh_at_base) |
86 |
87 |
87 |
88 |
88 end |
89 end |
89 |
90 |
90 |
91 |