src/HOL/Probability/Infinite_Product_Measure.thy
changeset 55415 05f5fdb8d093
parent 55414 eab03e9cee8a
child 55417 01fbfb60c33e
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -190,13 +190,13 @@
     1.4        let ?P =
     1.5          "\<lambda>k wk w. w \<in> space (Pi\<^sub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
     1.6            (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
     1.7 -      def w \<equiv> "nat_rec w0 (\<lambda>k wk. Eps (?P k wk))"
     1.8 +      def w \<equiv> "rec_nat w0 (\<lambda>k wk. Eps (?P k wk))"
     1.9  
    1.10        { fix k have w: "w k \<in> space (Pi\<^sub>M (J k) M) \<and>
    1.11            (\<forall>n. ?a / 2 ^ (k + 1) \<le> ?q k n (w k)) \<and> (k \<noteq> 0 \<longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1))"
    1.12          proof (induct k)
    1.13            case 0 with w0 show ?case
    1.14 -            unfolding w_def nat_rec_0 by auto
    1.15 +            unfolding w_def rec_nat_0 by auto
    1.16          next
    1.17            case (Suc k)
    1.18            then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
    1.19 @@ -241,7 +241,7 @@
    1.20                   (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
    1.21            qed
    1.22            then have "?P k (w k) (w (Suc k))"
    1.23 -            unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
    1.24 +            unfolding w_def rec_nat_Suc unfolding w_def[symmetric]
    1.25              by (rule someI_ex)
    1.26            then show ?case by auto
    1.27          qed
    1.28 @@ -480,10 +480,10 @@
    1.29  lemma comb_seq_0: "comb_seq 0 \<omega> \<omega>' = \<omega>'"
    1.30    by (auto simp add: comb_seq_def)
    1.31  
    1.32 -lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (nat_case (\<omega> n) \<omega>')"
    1.33 +lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (case_nat (\<omega> n) \<omega>')"
    1.34    by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)
    1.35  
    1.36 -lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = nat_case (\<omega> 0)"
    1.37 +lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = case_nat (\<omega> 0)"
    1.38    by (intro ext) (simp add: comb_seq_Suc comb_seq_0)
    1.39  
    1.40  lemma comb_seq_less: "i < n \<Longrightarrow> comb_seq n \<omega> \<omega>' i = \<omega> i"
    1.41 @@ -492,11 +492,11 @@
    1.42  lemma comb_seq_add: "comb_seq n \<omega> \<omega>' (i + n) = \<omega>' i"
    1.43    by (auto split: nat.split split_comb_seq)
    1.44  
    1.45 -lemma nat_case_comb_seq: "nat_case s' (comb_seq n \<omega> \<omega>') (i + n) = nat_case (nat_case s' \<omega> n) \<omega>' i"
    1.46 +lemma case_nat_comb_seq: "case_nat s' (comb_seq n \<omega> \<omega>') (i + n) = case_nat (case_nat s' \<omega> n) \<omega>' i"
    1.47    by (auto split: nat.split split_comb_seq)
    1.48  
    1.49 -lemma nat_case_comb_seq':
    1.50 -  "nat_case s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (nat_case s \<omega>) \<omega>'"
    1.51 +lemma case_nat_comb_seq':
    1.52 +  "case_nat s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (case_nat s \<omega>) \<omega>'"
    1.53    by (auto split: split_comb_seq nat.split)
    1.54  
    1.55  locale sequence_space = product_prob_space "\<lambda>i. M" "UNIV :: nat set" for M
    1.56 @@ -570,7 +570,7 @@
    1.57  qed simp_all
    1.58  
    1.59  lemma PiM_iter:
    1.60 -  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). nat_case s \<omega>) = S" (is "?D = _")
    1.61 +  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). case_nat s \<omega>) = S" (is "?D = _")
    1.62  proof (rule PiM_eq)
    1.63    let ?I = "UNIV::nat set" and ?M = "\<lambda>n. M"
    1.64    let "distr _ _ ?f" = "?D"