# HG changeset patch
# User nipkow
# Date 1541071434 -3600
# Node ID d4cec24a1d87d97fa18de436ad42ba016e9dec7e
# Parent  59aefb3b9e95570f3bd37e32ae37c8258f20aaa3
too many clashes with "root" on reals

diff -r 59aefb3b9e95 -r d4cec24a1d87 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Nov 01 11:26:38 2018 +0100
+++ b/src/HOL/Library/Tree.thy	Thu Nov 01 12:23:54 2018 +0100
@@ -9,7 +9,7 @@
 
 datatype 'a tree =
   Leaf ("\<langle>\<rangle>") |
-  Node "'a tree" (root: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
+  Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
 datatype_compat tree
 
 primrec left :: "'a tree \<Rightarrow> 'a tree" where
diff -r 59aefb3b9e95 -r d4cec24a1d87 src/HOL/Probability/Tree_Space.thy
--- a/src/HOL/Probability/Tree_Space.thy	Thu Nov 01 11:26:38 2018 +0100
+++ b/src/HOL/Probability/Tree_Space.thy	Thu Nov 01 12:23:54 2018 +0100
@@ -231,18 +231,18 @@
     unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
 qed
 
-lemma measurable_root': "root \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
+lemma measurable_root_val': "root_val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
 proof (rule measurableI)
-  show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root t \<in> space M" for t
+  show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root_val t \<in> space M" for t
     by (cases t) (auto simp: space_restrict_space space_tree_sigma)
   fix A assume A: "A \<in> sets M"
   from sets.sets_into_space[OF this]
-  have "root -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
+  have "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
     {Node l a r | l a r. (a, l, r) \<in> A \<times> space (tree_sigma M) \<times> space (tree_sigma M)}"
     by (auto simp: space_tree_sigma space_restrict_space elim: trees.cases)
   also have "\<dots> \<in> sets (tree_sigma M)"
     using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
-  finally show "root -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
+  finally show "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
       sets (restrict_space (tree_sigma M) (- {Leaf}))"
     by (auto simp: sets_restrict_space_iff space_restrict_space)
 qed
@@ -254,14 +254,14 @@
    (insert \<open>B \<subseteq> A\<close>, auto)
 
 
-lemma measurable_root[measurable (raw)]:
+lemma measurable_root_val[measurable (raw)]:
   assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
     and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"
-  shows "(\<lambda>\<omega>. root (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
+  shows "(\<lambda>\<omega>. root_val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
 proof -
   from assms have "f \<in> X \<rightarrow>\<^sub>M restrict_space (tree_sigma M) (- {Leaf})"
     by (intro measurable_restrict_space2) auto
-  from this and measurable_root' show ?thesis by (rule measurable_compose)
+  from this and measurable_root_val' show ?thesis by (rule measurable_compose)
 qed
 
 
@@ -344,7 +344,7 @@
     qed
   next
     case (Node ls u rs)
-    let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root (t \<omega>), right (t \<omega>),
+    let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root_val (t \<omega>), right (t \<omega>),
         rec_tree (l \<omega>) (n \<omega>) (left (t \<omega>)), rec_tree (l \<omega>) (n \<omega>) (right (t \<omega>)))"
     show ?case
     proof (rule measurable_cong[THEN iffD2])
@@ -366,7 +366,7 @@
           by (rule measurable_restrict_space1)
              (rule measurable_compose[OF Node(3) measurable_right])
         subgoal
-          apply (rule measurable_compose[OF _ measurable_root'])
+          apply (rule measurable_compose[OF _ measurable_root_val'])
           apply (rule measurable_restrict_space3[OF Node(3)])
           by auto
         subgoal