# 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 \ 'a tree" +where + "left (Node l v r) = l" +| "left Leaf = Leaf" + +primrec right :: "'a tree \ 'a tree" +where + "right (Node l v r) = r" +| "right Leaf = Leaf" + +primrec val :: "'a tree \ 'a" +where + "val (Node l v r) = v" +| "val Leaf = undefined" inductive_set trees :: "'a set \ 'a tree set" for S :: "'a set" where [intro!]: "Leaf \ trees S" @@ -340,4 +348,8 @@ qed qed +hide_const (open) val +hide_const (open) left +hide_const (open) right + end