author blanchet Mon, 03 Mar 2014 12:48:20 +0100 changeset 55857 b7a652b0bfb2 parent 55856 bddaada24074 child 55858 693ddbbab913
```--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Mar 03 12:48:20 2014 +0100
@@ -20,7 +20,7 @@

definition "Node n as \<equiv> NNode n (the_inv fset as)"
definition "cont \<equiv> fset o ccont"
-definition "unfold rt ct \<equiv> unfold_dtree rt (the_inv fset o ct)"
+definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (sum_map id Inr) o ct)"
definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"

lemma finite_cont[simp]: "finite (cont tr)"
@@ -75,18 +75,16 @@
lemma unfold:
"root (unfold rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
-using dtree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def
-apply - apply metis
+using dtree.sel_corec[of rt "the_inv fset o image (sum_map id Inr) o ct" b] unfolding unfold_def
+apply blast
unfolding cont_def comp_def
-by simp
+by (simp add: case_sum_o_inj sum_map.compositionality image_image)

lemma corec:
"root (corec rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
-apply -
-apply simp
unfolding cont_def comp_def id_def
-by simp
+by simp_all

end```