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)