equal
deleted
inserted
replaced
113 where |
113 where |
114 "height_trm (Var x) = 1" |
114 "height_trm (Var x) = 1" |
115 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
115 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
116 | "height_trm (Lam v b) = 1 + (height_trm b)" |
116 | "height_trm (Lam v b) = 1 + (height_trm b)" |
117 | "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)" |
117 | "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)" |
118 apply (simp only: eqvt_def height_trm_graph_def) |
118 apply (simp only: eqvt_def height_trm_graph_aux_def) |
119 apply (rule, perm_simp, rule, rule TrueI) |
119 apply (rule, perm_simp, rule, rule TrueI) |
120 apply (case_tac x rule: trm_assn.exhaust(1)) |
120 apply (case_tac x rule: trm_assn.exhaust(1)) |
121 apply (auto)[4] |
121 apply (auto)[4] |
122 apply (drule_tac x="assn" in meta_spec) |
122 apply (drule_tac x="assn" in meta_spec) |
123 apply (drule_tac x="trm" in meta_spec) |
123 apply (drule_tac x="trm" in meta_spec) |
167 where |
167 where |
168 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
168 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
169 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
169 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
170 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |
170 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |
171 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (apply_assn2 (subst s t) as) (subst s t b)" |
171 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (apply_assn2 (subst s t) as) (subst s t b)" |
172 apply (simp only: eqvt_def subst_graph_def) |
172 apply (simp only: eqvt_def subst_graph_aux_def) |
173 apply (rule, perm_simp, rule) |
173 apply (rule, perm_simp, rule) |
174 apply (rule TrueI) |
174 apply (rule TrueI) |
175 apply (case_tac x) |
175 apply (case_tac x) |
176 apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1)) |
176 apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1)) |
177 apply (auto simp add: fresh_star_def)[3] |
177 apply (auto simp add: fresh_star_def)[3] |