# HG changeset patch
# User blanchet
# Date 1348736350 -7200
# Node ID afc7f88370a81575128013fcd3151e01d6c625b9
# Parent  ea566f5e1724c6bfefb95ad10211795fdb161c94
partly ported "TreeFI" example to new syntax

diff -r ea566f5e1724 -r afc7f88370a8 src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Thu Sep 27 10:59:10 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Thu Sep 27 10:59:10 2012 +0200
@@ -14,36 +14,27 @@
 
 hide_const (open) Sublist.sub
 
-codata_raw treeFI: 'tree = "'a \<times> 'tree listF"
+codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs
 by (auto simp add: listF.set_natural')
 
-(* selectors for trees *)
-definition "lab tr \<equiv> fst (treeFI_dtor tr)"
-definition "sub tr \<equiv> snd (treeFI_dtor tr)"
-
 lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
-unfolding lab_def sub_def by simp
+unfolding lab_def sub_def treeFI_case_def
+by (metis fst_def pair_collapse snd_def)
 
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
 
-lemma unfold_pair_fun_lab: "lab (treeFI_dtor_unfold (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFI.dtor_unfold pre_treeFI_map_def by simp
-
-lemma unfold_pair_fun_sub: "sub (treeFI_dtor_unfold (f \<odot> g) t) = listF_map (treeFI_dtor_unfold (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFI.dtor_unfold pre_treeFI_map_def by simp
-
 (* Tree reverse:*)
-definition "trev \<equiv> treeFI_dtor_unfold (lab \<odot> lrev o sub)"
+definition "trev \<equiv> treeFI_unfold lab (lrev o sub)"
 
 lemma trev_simps1[simp]: "lab (trev t) = lab t"
-unfolding trev_def by (simp add: unfold_pair_fun_lab)
+unfolding trev_def by simp
 
 lemma trev_simps2[simp]: "sub (trev t) = listF_map trev (lrev (sub t))"
-unfolding trev_def by (simp add: unfold_pair_fun_sub)
+unfolding trev_def by simp
 
 lemma treeFI_coinduct:
 assumes *: "phi x y"