# HG changeset patch
# User hoelzl
# Date 1497017408 14400
# Node ID d20d5a3bf6cfc7fe67a22e8347e8355b5f7b296d
# Parent  d244a895da50fd5d0fec898df7b7428c9381d7e8
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections

diff -r d244a895da50 -r d20d5a3bf6cf src/HOL/Probability/Tree_Space.thy
--- a/src/HOL/Probability/Tree_Space.thy	Fri Jun 09 14:25:00 2017 +0200
+++ b/src/HOL/Probability/Tree_Space.thy	Fri Jun 09 10:10:08 2017 -0400
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, CMU *)
 
 theory Tree_Space
-  imports Analysis
+  imports Analysis "~~/src/HOL/Library/Tree"
 begin
 
 lemma countable_lfp:
@@ -22,12 +22,20 @@
   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"
@@ -340,4 +348,8 @@
   qed
 qed
 
+hide_const (open) val
+hide_const (open) left
+hide_const (open) right
+
 end