src/HOL/Probability/Tree_Space.thy

 (*  Title:      HOL/Probability/Tree_Space.thy
     Author:     Johannes Hölzl, CMU *)
 
 theory Tree_Space
-  imports Analysis
+  imports Analysis "~~/src/HOL/Library/Tree"
 begin
 
 lemma countable_lfp:
   assumes step: "\<And>Y. countable Y \<Longrightarrow> countable (F Y)"
   and cont: "Order_Continuity.sup_continuous F"

     have "\<And>x. countable ((F ^^ n) bot x)"
       by(induct n)(auto intro: step) }
   thus ?thesis using cont by(simp add: sup_continuous_lfp)
 qed
 
-datatype 'a tree = Leaf
-  | Node (left: "'a tree") (val: 'a) (right: "'a tree")
-  where
-    "left Leaf = Leaf"
-  | "right Leaf = Leaf"
-  | "val Leaf = undefined"
+primrec left :: "'a tree \<Rightarrow> 'a tree"
+where
+  "left (Node l v r) = l"
+| "left Leaf = Leaf"
+
+primrec right :: "'a tree \<Rightarrow> 'a tree"
+where
+  "right (Node l v r) = r"
+| "right Leaf = Leaf"
+
+primrec val :: "'a tree \<Rightarrow> 'a"
+where
+  "val (Node l v r) = v"
+| "val Leaf = undefined"
 
 inductive_set trees :: "'a set \<Rightarrow> 'a tree set" for S :: "'a set" where
   [intro!]: "Leaf \<in> trees S"
 | "l \<in> trees S \<Longrightarrow> r \<in> trees S \<Longrightarrow> v \<in> S \<Longrightarrow> Node l v r \<in> trees S"
 

         by (rule measurable_restrict_space1) auto
     qed
   qed
 qed
 
+hide_const (open) val
+hide_const (open) left
+hide_const (open) right
+
 end