too many clashes with "root" on reals
authornipkow
Thu Nov 01 12:23:54 2018 +0100 (6 months ago)
changeset 69219d4cec24a1d87
parent 69218 59aefb3b9e95
child 69220 c6b15fc78f78
child 69222 8365124a86ae
too many clashes with "root" on reals
src/HOL/Library/Tree.thy
src/HOL/Probability/Tree_Space.thy
     1.1 --- a/src/HOL/Library/Tree.thy	Thu Nov 01 11:26:38 2018 +0100
     1.2 +++ b/src/HOL/Library/Tree.thy	Thu Nov 01 12:23:54 2018 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  datatype 'a tree =
     1.6    Leaf ("\<langle>\<rangle>") |
     1.7 -  Node "'a tree" (root: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
     1.8 +  Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
     1.9  datatype_compat tree
    1.10  
    1.11  primrec left :: "'a tree \<Rightarrow> 'a tree" where
     2.1 --- a/src/HOL/Probability/Tree_Space.thy	Thu Nov 01 11:26:38 2018 +0100
     2.2 +++ b/src/HOL/Probability/Tree_Space.thy	Thu Nov 01 12:23:54 2018 +0100
     2.3 @@ -231,18 +231,18 @@
     2.4      unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
     2.5  qed
     2.6  
     2.7 -lemma measurable_root': "root \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
     2.8 +lemma measurable_root_val': "root_val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
     2.9  proof (rule measurableI)
    2.10 -  show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root t \<in> space M" for t
    2.11 +  show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root_val t \<in> space M" for t
    2.12      by (cases t) (auto simp: space_restrict_space space_tree_sigma)
    2.13    fix A assume A: "A \<in> sets M"
    2.14    from sets.sets_into_space[OF this]
    2.15 -  have "root -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
    2.16 +  have "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
    2.17      {Node l a r | l a r. (a, l, r) \<in> A \<times> space (tree_sigma M) \<times> space (tree_sigma M)}"
    2.18      by (auto simp: space_tree_sigma space_restrict_space elim: trees.cases)
    2.19    also have "\<dots> \<in> sets (tree_sigma M)"
    2.20      using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
    2.21 -  finally show "root -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
    2.22 +  finally show "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
    2.23        sets (restrict_space (tree_sigma M) (- {Leaf}))"
    2.24      by (auto simp: sets_restrict_space_iff space_restrict_space)
    2.25  qed
    2.26 @@ -254,14 +254,14 @@
    2.27     (insert \<open>B \<subseteq> A\<close>, auto)
    2.28  
    2.29  
    2.30 -lemma measurable_root[measurable (raw)]:
    2.31 +lemma measurable_root_val[measurable (raw)]:
    2.32    assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
    2.33      and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"
    2.34 -  shows "(\<lambda>\<omega>. root (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
    2.35 +  shows "(\<lambda>\<omega>. root_val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
    2.36  proof -
    2.37    from assms have "f \<in> X \<rightarrow>\<^sub>M restrict_space (tree_sigma M) (- {Leaf})"
    2.38      by (intro measurable_restrict_space2) auto
    2.39 -  from this and measurable_root' show ?thesis by (rule measurable_compose)
    2.40 +  from this and measurable_root_val' show ?thesis by (rule measurable_compose)
    2.41  qed
    2.42  
    2.43  
    2.44 @@ -344,7 +344,7 @@
    2.45      qed
    2.46    next
    2.47      case (Node ls u rs)
    2.48 -    let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root (t \<omega>), right (t \<omega>),
    2.49 +    let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root_val (t \<omega>), right (t \<omega>),
    2.50          rec_tree (l \<omega>) (n \<omega>) (left (t \<omega>)), rec_tree (l \<omega>) (n \<omega>) (right (t \<omega>)))"
    2.51      show ?case
    2.52      proof (rule measurable_cong[THEN iffD2])
    2.53 @@ -366,7 +366,7 @@
    2.54            by (rule measurable_restrict_space1)
    2.55               (rule measurable_compose[OF Node(3) measurable_right])
    2.56          subgoal
    2.57 -          apply (rule measurable_compose[OF _ measurable_root'])
    2.58 +          apply (rule measurable_compose[OF _ measurable_root_val'])
    2.59            apply (rule measurable_restrict_space3[OF Node(3)])
    2.60            by auto
    2.61          subgoal