# HG changeset patch
# User blanchet
# Date 1370621347 -3600
# Node ID 7e352bb7600915c423dc21f0fa913594a56a13ea
# Parent  07fd21c01e93bceac61cb064f60baa048d2a4980
adapted example (cf. 78a3d5006cf1)

diff -r 07fd21c01e93 -r 7e352bb76009 src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Fri Jun 07 17:04:55 2013 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Fri Jun 07 17:09:07 2013 +0100
@@ -23,10 +23,10 @@
 definition "Node n as \<equiv> NNode n (the_inv fset as)"
 definition "cont \<equiv> fset o ccont"
 definition "unfold rt ct \<equiv> dtree_unfold rt (the_inv fset o ct)"
-definition "corec rt qt ct dt \<equiv> dtree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)"
+definition "corec rt ct \<equiv> dtree_corec rt (the_inv fset o ct)"
 
 lemma finite_cont[simp]: "finite (cont tr)"
-  unfolding cont_def o_apply by (cases tr, clarsimp) (transfer, simp) 
+  unfolding cont_def o_apply by (cases tr, clarsimp) (transfer, simp)
 
 lemma Node_root_cont[simp]:
   "Node (root tr) (cont tr) = tr"
@@ -83,12 +83,9 @@
 by simp
 
 lemma corec:
-"root (corec rt qt ct dt b) = rt b"
-"\<lbrakk>finite (ct b); finite (dt b)\<rbrakk> \<Longrightarrow>
- cont (corec rt qt ct dt b) =
- (if qt b then ct b else image (id \<oplus> corec rt qt ct dt) (dt b))"
-using dtree.sel_corec[of rt qt "the_inv fset \<circ> ct" "the_inv fset \<circ> dt" b]
-unfolding corec_def
+"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