src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy
 changeset 55066 4e5ddf3162ac parent 49882 946efb120c42 child 55070 235c7661a96b
```     1.1 --- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
1.2 +++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
1.3 @@ -480,7 +480,7 @@
1.4  proof-
1.5    {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
1.6     apply(induct rule: wf_raw_coind) apply safe
1.7 -   unfolding deftr_simps image_compose[symmetric] sum_map.comp id_o
1.8 +   unfolding deftr_simps image_compose[symmetric] sum_map.comp id_comp
1.9     root_o_deftr sum_map.id image_id id_apply apply(rule S_P)
1.10     unfolding inj_on_def by auto
1.11    }
1.12 @@ -517,7 +517,7 @@
1.13  lemma cont_hsubst_eq[simp]:
1.14  assumes "root tr = root tr0"
1.15  shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr0)"
1.16 -apply(subst id_o[symmetric, of id]) unfolding id_o
1.17 +apply(subst id_comp[symmetric, of id]) unfolding id_comp
1.18  using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
1.19  unfolding hsubst_def hsubst_c_def using assms by simp
1.20
1.21 @@ -529,7 +529,7 @@
1.22  lemma cont_hsubst_neq[simp]:
1.23  assumes "root tr \<noteq> root tr0"
1.24  shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr)"
1.25 -apply(subst id_o[symmetric, of id]) unfolding id_o
1.26 +apply(subst id_comp[symmetric, of id]) unfolding id_comp
1.27  using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
1.28  unfolding hsubst_def hsubst_c_def using assms by simp
1.29
1.30 @@ -960,7 +960,7 @@
1.31
1.32  lemma cont_H[simp]:
1.33  "cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
1.34 -apply(subst id_o[symmetric, of id]) unfolding sum_map.comp[symmetric]
1.35 +apply(subst id_comp[symmetric, of id]) unfolding sum_map.comp[symmetric]
1.36  unfolding image_compose unfolding H_c_def[symmetric]
1.37  using unfold(2)[of H_c n H_r, OF finite_H_c]
1.38  unfolding H_def ..
1.39 @@ -989,7 +989,7 @@
1.40         obtain tr2' where tr2: "tr2 = H (root tr2')"
1.41         and tr2': "Inr tr2' \<in> cont (pick n1)"
1.42         using tr2 Inr_cont_H[of n1]
1.43 -       unfolding tr1 image_def o_def using vimage_eq by auto
1.44 +       unfolding tr1 image_def comp_def using vimage_eq by auto
1.45         have "inItr UNIV tr0 (root tr2')"
1.46         using inItr.Base inItr.Ind n1 pick subtr_inItr tr2' by (metis iso_tuple_UNIV_I)
1.47         thus "\<exists>n2. inItr UNIV tr0 n2 \<and> tr2 = H n2" using tr2 by blast
1.48 @@ -1005,7 +1005,7 @@
1.49  using assms apply(cases t_tr)
1.50    apply (metis (lifting) sum_map.simps(1))
1.51    using pick H_def H_r_def unfold(1)
1.52 -      inItr.Base o_apply subtr_StepL subtr_inItr sum_map.simps(2)
1.53 +      inItr.Base comp_apply subtr_StepL subtr_inItr sum_map.simps(2)
1.54    by (metis UNIV_I)
1.55
1.56  lemma H_P:
1.57 @@ -1013,7 +1013,7 @@
1.58  shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
1.59  proof-
1.60    have "?L = (n, (id \<oplus> root) ` cont (pick n))"
1.61 -  unfolding cont_H image_compose[symmetric] sum_map.comp id_o o_assoc
1.62 +  unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc
1.63    unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
1.64    by(rule root_H_root[OF n])
1.65    moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
```