--- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Sat Mar 15 08:31:33 2014 +0100
@@ -480,7 +480,7 @@
proof-
{fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
apply(induct rule: wf_raw_coind) apply safe
- unfolding deftr_simps image_compose[symmetric] map_sum.comp id_comp
+ unfolding deftr_simps image_comp map_sum.comp id_comp
root_o_deftr map_sum.id image_id id_apply apply(rule S_P)
unfolding inj_on_def by auto
}
@@ -565,7 +565,7 @@
show "(root (hsubst tr), prodOf (hsubst tr)) \<in> P"
unfolding tr1 apply(cases "root tr = root tr0")
using wf_P[OF dtr] wf_P[OF tr0]
- by (auto simp add: image_compose[symmetric] map_sum.comp)
+ by (auto simp add: image_comp map_sum.comp)
show "inj_on root (Inr -` cont (hsubst tr))"
apply(cases "root tr = root tr0") using wf_inj_on[OF dtr] wf_inj_on[OF tr0]
unfolding inj_on_def by (auto, blast)
@@ -959,8 +959,8 @@
lemma cont_H[simp]:
"cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
apply(subst id_comp[symmetric, of id]) unfolding map_sum.comp[symmetric]
-unfolding image_compose unfolding H_c_def[symmetric]
-using unfold(2)[of H_c n H_r, OF finite_H_c]
+unfolding image_comp [symmetric] H_c_def [symmetric]
+using unfold(2) [of H_c n H_r, OF finite_H_c]
unfolding H_def ..
lemma Inl_cont_H[simp]:
@@ -1011,7 +1011,7 @@
shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
proof-
have "?L = (n, (id \<oplus> root) ` cont (pick n))"
- unfolding cont_H image_compose[symmetric] map_sum.comp id_comp comp_assoc[symmetric]
+ unfolding cont_H image_comp map_sum.comp id_comp comp_assoc[symmetric]
unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
by (rule root_H_root[OF n])
moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)