# HG changeset patch
# User nipkow
# Date 1547478656 -3600
# Node ID 2b56cbb02e8ab2e1417f1bf99aafe6bc1473b8f1
# Parent  bc758f4f09e56f01a3f4b8909144168a0ce14842
root_val -> value

diff -r bc758f4f09e5 -r 2b56cbb02e8a src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Mon Jan 14 14:46:12 2019 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Mon Jan 14 16:10:56 2019 +0100
@@ -501,7 +501,7 @@
 function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
 "list_fast_rec ts = (if ts = [] then [] else
   let us = filter (\<lambda>t. t \<noteq> Leaf) ts
-  in map root_val us @ list_fast_rec (map left us @ map right us))"
+  in map value us @ list_fast_rec (map left us @ map right us))"
 by (pat_completeness, auto)
 
 lemma list_fast_rec_term: "\<lbrakk> ts \<noteq> []; us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<rbrakk> \<Longrightarrow>
@@ -576,13 +576,13 @@
     case False
     with less.prems(2) have *:
       "\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf
-         \<and> root_val (ts ! i) = xs ! i
+         \<and> value (ts ! i) = xs ! i
          \<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
          \<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
                  \<longrightarrow> braun_list (right (ts ! i)) ys)"
       by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
                      algebra_simps)
-    have 1: "map root_val ts = take (2 ^ k) xs"
+    have 1: "map value ts = take (2 ^ k) xs"
       using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
     have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
       using less.prems(1) False
diff -r bc758f4f09e5 -r 2b56cbb02e8a src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Mon Jan 14 14:46:12 2019 +0100
+++ b/src/HOL/Library/Tree.thy	Mon Jan 14 16:10:56 2019 +0100
@@ -9,7 +9,7 @@
 
 datatype 'a tree =
   Leaf ("\<langle>\<rangle>") |
-  Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
+  Node "'a tree" ("value": 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
 datatype_compat tree
 
 primrec left :: "'a tree \<Rightarrow> 'a tree" where
diff -r bc758f4f09e5 -r 2b56cbb02e8a src/HOL/Probability/Tree_Space.thy
--- a/src/HOL/Probability/Tree_Space.thy	Mon Jan 14 14:46:12 2019 +0100
+++ b/src/HOL/Probability/Tree_Space.thy	Mon Jan 14 16:10:56 2019 +0100
@@ -231,18 +231,18 @@
     unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
 qed
 
-lemma measurable_root_val': "root_val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
+lemma measurable_value': "value \<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_val t \<in> space M" for t
+  show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> value 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_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
+  have "value -` 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_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
+  finally show "value -` 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_val[measurable (raw)]:
+lemma measurable_value[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_val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
+  shows "(\<lambda>\<omega>. value (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_val' show ?thesis by (rule measurable_compose)
+  from this and measurable_value' 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_val (t \<omega>), right (t \<omega>),
+    let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), value (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_val'])
+          apply (rule measurable_compose[OF _ measurable_value'])
           apply (rule measurable_restrict_space3[OF Node(3)])
           by auto
         subgoal