src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
changeset 57983 6edc3529bb4e
parent 55943 5c2df04e97d1
child 57991 f50b3726266f
     1.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4  lemma unfold:
     1.5  "root (unfold rt ct b) = rt b"
     1.6  "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
     1.7 -using dtree.sel_corec[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
     1.8 +using dtree.corec_sel[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
     1.9  apply blast
    1.10  unfolding cont_def comp_def
    1.11  by (simp add: case_sum_o_inj map_sum.compositionality image_image)
    1.12 @@ -83,7 +83,7 @@
    1.13  lemma corec:
    1.14  "root (corec rt ct b) = rt b"
    1.15  "finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
    1.16 -using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
    1.17 +using dtree.corec_sel[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
    1.18  unfolding cont_def comp_def id_def
    1.19  by simp_all
    1.20