author hoelzl Fri, 09 Jun 2017 10:10:08 -0400 changeset 66049 d20d5a3bf6cf parent 66048 d244a895da50 child 66050 3804a9640088
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
```--- 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```