added and renamed functions
authornipkow
Thu Nov 01 11:26:38 2018 +0100 (6 months ago)
changeset 6921859aefb3b9e95
parent 69217 a8c707352ccc
child 69219 d4cec24a1d87
added and renamed functions
src/HOL/Library/Tree.thy
src/HOL/Probability/Tree_Space.thy
     1.1 --- a/src/HOL/Library/Tree.thy	Thu Nov 01 09:25:58 2018 +0100
     1.2 +++ b/src/HOL/Library/Tree.thy	Thu Nov 01 11:26:38 2018 +0100
     1.3 @@ -9,9 +9,17 @@
     1.4  
     1.5  datatype 'a tree =
     1.6    Leaf ("\<langle>\<rangle>") |
     1.7 -  Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
     1.8 +  Node "'a tree" (root: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
     1.9  datatype_compat tree
    1.10  
    1.11 +primrec left :: "'a tree \<Rightarrow> 'a tree" where
    1.12 +"left (Node l v r) = l" |
    1.13 +"left Leaf = Leaf"
    1.14 +
    1.15 +primrec right :: "'a tree \<Rightarrow> 'a tree" where
    1.16 +"right (Node l v r) = r" |
    1.17 +"right Leaf = Leaf"
    1.18 +
    1.19  text\<open>Counting the number of leaves rather than nodes:\<close>
    1.20  
    1.21  fun size1 :: "'a tree \<Rightarrow> nat" where
     2.1 --- a/src/HOL/Probability/Tree_Space.thy	Thu Nov 01 09:25:58 2018 +0100
     2.2 +++ b/src/HOL/Probability/Tree_Space.thy	Thu Nov 01 11:26:38 2018 +0100
     2.3 @@ -22,16 +22,6 @@
     2.4    thus ?thesis using cont by(simp add: sup_continuous_lfp)
     2.5  qed
     2.6  
     2.7 -primrec left :: "'a tree \<Rightarrow> 'a tree"
     2.8 -where
     2.9 -  "left (Node l v r) = l"
    2.10 -| "left Leaf = Leaf"
    2.11 -
    2.12 -primrec right :: "'a tree \<Rightarrow> 'a tree"
    2.13 -where
    2.14 -  "right (Node l v r) = r"
    2.15 -| "right Leaf = Leaf"
    2.16 -
    2.17  inductive_set trees :: "'a set \<Rightarrow> 'a tree set" for S :: "'a set" where
    2.18    [intro!]: "Leaf \<in> trees S"
    2.19  | "l \<in> trees S \<Longrightarrow> r \<in> trees S \<Longrightarrow> v \<in> S \<Longrightarrow> Node l v r \<in> trees S"
    2.20 @@ -241,18 +231,18 @@
    2.21      unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
    2.22  qed
    2.23  
    2.24 -lemma measurable_root_val': "root_val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
    2.25 +lemma measurable_root': "root \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
    2.26  proof (rule measurableI)
    2.27 -  show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root_val t \<in> space M" for t
    2.28 +  show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root t \<in> space M" for t
    2.29      by (cases t) (auto simp: space_restrict_space space_tree_sigma)
    2.30    fix A assume A: "A \<in> sets M"
    2.31    from sets.sets_into_space[OF this]
    2.32 -  have "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
    2.33 +  have "root -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) =
    2.34      {Node l a r | l a r. (a, l, r) \<in> A \<times> space (tree_sigma M) \<times> space (tree_sigma M)}"
    2.35      by (auto simp: space_tree_sigma space_restrict_space elim: trees.cases)
    2.36    also have "\<dots> \<in> sets (tree_sigma M)"
    2.37      using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
    2.38 -  finally show "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
    2.39 +  finally show "root -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
    2.40        sets (restrict_space (tree_sigma M) (- {Leaf}))"
    2.41      by (auto simp: sets_restrict_space_iff space_restrict_space)
    2.42  qed
    2.43 @@ -264,14 +254,14 @@
    2.44     (insert \<open>B \<subseteq> A\<close>, auto)
    2.45  
    2.46  
    2.47 -lemma measurable_root_val[measurable (raw)]:
    2.48 +lemma measurable_root[measurable (raw)]:
    2.49    assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
    2.50      and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"
    2.51 -  shows "(\<lambda>\<omega>. root_val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
    2.52 +  shows "(\<lambda>\<omega>. root (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
    2.53  proof -
    2.54    from assms have "f \<in> X \<rightarrow>\<^sub>M restrict_space (tree_sigma M) (- {Leaf})"
    2.55      by (intro measurable_restrict_space2) auto
    2.56 -  from this and measurable_root_val' show ?thesis by (rule measurable_compose)
    2.57 +  from this and measurable_root' show ?thesis by (rule measurable_compose)
    2.58  qed
    2.59  
    2.60  
    2.61 @@ -354,7 +344,7 @@
    2.62      qed
    2.63    next
    2.64      case (Node ls u rs)
    2.65 -    let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root_val (t \<omega>), right (t \<omega>),
    2.66 +    let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root (t \<omega>), right (t \<omega>),
    2.67          rec_tree (l \<omega>) (n \<omega>) (left (t \<omega>)), rec_tree (l \<omega>) (n \<omega>) (right (t \<omega>)))"
    2.68      show ?case
    2.69      proof (rule measurable_cong[THEN iffD2])
    2.70 @@ -376,7 +366,7 @@
    2.71            by (rule measurable_restrict_space1)
    2.72               (rule measurable_compose[OF Node(3) measurable_right])
    2.73          subgoal
    2.74 -          apply (rule measurable_compose[OF _ measurable_root_val'])
    2.75 +          apply (rule measurable_compose[OF _ measurable_root'])
    2.76            apply (rule measurable_restrict_space3[OF Node(3)])
    2.77            by auto
    2.78          subgoal