src/HOL/Probability/Infinite_Product_Measure.thy

       from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
 
       let ?P =
         "\<lambda>k wk w. w \<in> space (Pi\<^sub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
           (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
-      def w \<equiv> "nat_rec w0 (\<lambda>k wk. Eps (?P k wk))"
+      def w \<equiv> "rec_nat w0 (\<lambda>k wk. Eps (?P k wk))"
 
       { fix k have w: "w k \<in> space (Pi\<^sub>M (J k) M) \<and>
           (\<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))"
         proof (induct k)
           case 0 with w0 show ?case
-            unfolding w_def nat_rec_0 by auto
+            unfolding w_def rec_nat_0 by auto
         next
           case (Suc k)
           then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
           have "\<exists>w'. ?P k (w k) w'"
           proof cases

               using w' J_mono[of k "Suc k"] wk unfolding *
               by (intro exI[of _ ?w])
                  (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
           qed
           then have "?P k (w k) (w (Suc k))"
-            unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
+            unfolding w_def rec_nat_Suc unfolding w_def[symmetric]
             by (rule someI_ex)
           then show ?case by auto
         qed
         moreover
         from w have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto

   using measurable_compose[OF measurable_Pair[OF f g] measurable_comb_seq] by simp
 
 lemma comb_seq_0: "comb_seq 0 \<omega> \<omega>' = \<omega>'"
   by (auto simp add: comb_seq_def)
 
-lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (nat_case (\<omega> n) \<omega>')"
+lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (case_nat (\<omega> n) \<omega>')"
   by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)
 
-lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = nat_case (\<omega> 0)"
+lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = case_nat (\<omega> 0)"
   by (intro ext) (simp add: comb_seq_Suc comb_seq_0)
 
 lemma comb_seq_less: "i < n \<Longrightarrow> comb_seq n \<omega> \<omega>' i = \<omega> i"
   by (auto split: split_comb_seq)
 
 lemma comb_seq_add: "comb_seq n \<omega> \<omega>' (i + n) = \<omega>' i"
   by (auto split: nat.split split_comb_seq)
 
-lemma nat_case_comb_seq: "nat_case s' (comb_seq n \<omega> \<omega>') (i + n) = nat_case (nat_case s' \<omega> n) \<omega>' i"
+lemma case_nat_comb_seq: "case_nat s' (comb_seq n \<omega> \<omega>') (i + n) = case_nat (case_nat s' \<omega> n) \<omega>' i"
   by (auto split: nat.split split_comb_seq)
 
-lemma nat_case_comb_seq':
-  "nat_case s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (nat_case s \<omega>) \<omega>'"
+lemma case_nat_comb_seq':
+  "case_nat s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (case_nat s \<omega>) \<omega>'"
   by (auto split: split_comb_seq nat.split)
 
 locale sequence_space = product_prob_space "\<lambda>i. M" "UNIV :: nat set" for M
 begin
 

     by (subst mult_commute) (auto simp: J setprod_subset_diff[symmetric])
   finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .
 qed simp_all
 
 lemma PiM_iter:
-  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). nat_case s \<omega>) = S" (is "?D = _")
+  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). case_nat s \<omega>) = S" (is "?D = _")
 proof (rule PiM_eq)
   let ?I = "UNIV::nat set" and ?M = "\<lambda>n. M"
   let "distr _ _ ?f" = "?D"
 
   fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"