36 height :: "lam \<Rightarrow> int" |
36 height :: "lam \<Rightarrow> int" |
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(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") |
|
42 unfolding eqvt_def |
|
43 apply(rule allI) |
|
44 apply(simp add: permute_fun_def) |
|
45 apply(rule ext) |
|
46 apply(rule ext) |
|
47 apply(simp add: permute_bool_def) |
|
48 apply(rule iffI) |
|
49 apply(drule_tac x="p" in meta_spec) |
|
50 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
51 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
52 apply(simp) |
|
53 apply(drule_tac x="-p" in meta_spec) |
|
54 apply(drule_tac x="x" in meta_spec) |
|
55 apply(drule_tac x="xa" in meta_spec) |
|
56 apply(simp) |
|
57 apply(erule height_graph.induct) |
|
58 apply(perm_simp) |
|
59 apply(rule height_graph.intros) |
|
60 apply(perm_simp) |
|
61 apply(rule height_graph.intros) |
|
62 apply(assumption) |
|
63 apply(assumption) |
|
64 apply(perm_simp) |
|
65 apply(rule height_graph.intros) |
|
66 apply(assumption) |
41 apply(rule_tac y="x" in lam.exhaust) |
67 apply(rule_tac y="x" in lam.exhaust) |
42 apply(auto simp add: lam.distinct lam.eq_iff) |
68 apply(auto simp add: lam.distinct lam.eq_iff) |
43 apply(simp add: Abs_eq_iff alphas) |
69 apply(simp add: Abs_eq_iff alphas) |
44 apply(clarify) |
70 apply(clarify) |
45 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
71 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
46 apply(simp add: pure_supp fresh_star_def) |
72 apply(simp add: pure_supp fresh_star_def) |
47 apply(simp add: eqvt_at_def) |
73 apply(simp add: eqvt_at_def) |
48 done |
74 done |
49 |
75 |
50 termination |
76 termination |
51 by (relation "measure size") (simp_all add: lam.size) |
77 by (relation "measure size") (simp_all add: lam.size) |
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
83 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
58 where |
84 where |
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
85 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
86 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
87 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
88 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
|
89 unfolding eqvt_def |
|
90 apply(rule allI) |
|
91 apply(simp add: permute_fun_def) |
|
92 apply(rule ext) |
|
93 apply(rule ext) |
|
94 apply(simp add: permute_bool_def) |
|
95 apply(rule iffI) |
|
96 apply(drule_tac x="p" in meta_spec) |
|
97 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
98 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
99 apply(simp) |
|
100 apply(drule_tac x="-p" in meta_spec) |
|
101 apply(drule_tac x="x" in meta_spec) |
|
102 apply(drule_tac x="xa" in meta_spec) |
|
103 apply(simp) |
|
104 apply(erule subst_graph.induct) |
|
105 apply(perm_simp) |
|
106 apply(rule subst_graph.intros) |
|
107 apply(perm_simp) |
|
108 apply(rule subst_graph.intros) |
|
109 apply(assumption) |
|
110 apply(assumption) |
|
111 apply(perm_simp) |
|
112 apply(rule subst_graph.intros) |
|
113 apply(simp add: fresh_Pair) |
|
114 apply(assumption) |
62 apply(auto simp add: lam.distinct lam.eq_iff) |
115 apply(auto simp add: lam.distinct lam.eq_iff) |
63 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
116 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
64 apply(blast)+ |
117 apply(blast)+ |
65 apply(simp add: fresh_star_def) |
118 apply(simp add: fresh_star_def) |
66 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
119 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |