equal
deleted
inserted
replaced
16 typedecl N |
16 typedecl N |
17 typedecl T |
17 typedecl T |
18 |
18 |
19 codata dtree = NNode (root: N) (ccont: "(T + dtree) fset") |
19 codata dtree = NNode (root: N) (ccont: "(T + dtree) fset") |
20 |
20 |
21 |
21 subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *} |
22 subsection{* The characteristic lemmas transported from fset to set *} |
|
23 |
22 |
24 definition "Node n as \<equiv> NNode n (the_inv fset as)" |
23 definition "Node n as \<equiv> NNode n (the_inv fset as)" |
25 definition "cont \<equiv> fset o ccont" |
24 definition "cont \<equiv> fset o ccont" |
26 definition "unfold rt ct \<equiv> dtree_unfold rt (the_inv fset o ct)" |
25 definition "unfold rt ct \<equiv> dtree_unfold rt (the_inv fset o ct)" |
27 definition "corec rt qt ct dt \<equiv> dtree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)" |
26 definition "corec rt qt ct dt \<equiv> dtree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)" |