src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

   { assume rl: "rl ` s \<noteq> {..Suc n}"
     show "card ?S = 0 \<or> card ?S = 2"
     proof cases
       assume *: "{..n} \<subseteq> rl ` s"
       with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
-        by (auto simp add: atMost_Suc subset_insert_iff split: split_if_asm)
+        by (auto simp add: atMost_Suc subset_insert_iff split: if_split_asm)
       then have "\<not> inj_on rl s"
         by (intro pigeonhole) simp
       then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
         by (auto simp: inj_on_def)
       then have eq: "rl ` (s - {a}) = rl ` s"

   with * a have "\<And>a'. a' \<in> s \<Longrightarrow> a' j = p'"
     by auto
   then have "\<And>i. i \<le> n \<Longrightarrow> enum i j = p'"
     unfolding s_eq by auto
   from this[of 0] this[of n] have "j \<notin> upd ` {..< n}"
-    by (auto simp: enum_def fun_eq_iff split: split_if_asm)
+    by (auto simp: enum_def fun_eq_iff split: if_split_asm)
   with upd \<open>j < n\<close> show False
     by (auto simp: bij_betw_def)
 qed
 
 lemma upd_inj: "i < n \<Longrightarrow> j < n \<Longrightarrow> upd i = upd j \<longleftrightarrow> i = j"

   moreover
   { fix j assume "Suc j < n"
     with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
     have "u_s (Suc j) = u_t (Suc j)"
       using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
-      by (auto simp: fun_eq_iff split: split_if_asm) }
+      by (auto simp: fun_eq_iff split: if_split_asm) }
   then have "\<And>j. 0 < j \<Longrightarrow> j < n \<Longrightarrow> u_s j = u_t j"
     by (auto simp: gr0_conv_Suc)
   with \<open>n \<noteq> 0\<close> have "u_t 0 = u_s 0"
     by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
   ultimately have "a = b"

   moreover
   { fix j assume "j < n'"
     with enum_eq[of j] enum_eq[of "Suc j"]
     have "u_s j = u_t j"
       using s.enum_Suc[of j] t.enum_Suc[of j]
-      by (auto simp: Suc fun_eq_iff split: split_if_asm) }
+      by (auto simp: Suc fun_eq_iff split: if_split_asm) }
   then have "\<And>j. j < n' \<Longrightarrow> u_s j = u_t j"
     by (auto simp: gr0_conv_Suc)
   then have "u_t n' = u_s n'"
     by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
   ultimately have "a = b"

   { fix a s assume "ksimplex p n s" "a \<in> s"
     then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
     then interpret kuhn_simplex p n b u s .
     from s_space \<open>a \<in> s\<close> out_eq_p[OF \<open>a \<in> s\<close>]
     have "a \<in> (\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p})"
-      by (auto simp: image_iff subset_eq Pi_iff split: split_if_asm
+      by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm
                intro!: bexI[of _ "restrict a {..< n}"]) }
   then show "{s. ksimplex p n s} \<subseteq> Pow ((\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p}))"
     by auto
 qed (simp add: finite_PiE)
 

       using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident Zero_notin_Suc in_enum_image subset_eq)
     then have "enum 1 \<in> s - {a}"
       by auto
     then have "upd 0 = n"
       using \<open>a n < p\<close> \<open>a = enum 0\<close> na[rule_format, of "enum 1"]
-      by (auto simp: fun_eq_iff enum_Suc split: split_if_asm)
+      by (auto simp: fun_eq_iff enum_Suc split: if_split_asm)
     then have "bij_betw upd (Suc ` {..< n}) {..< n}"
       using upd
       by (subst notIn_Un_bij_betw3[where b=0])
          (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
     then have "bij_betw (upd\<circ>Suc) {..<n} {..<n}"

       { assume "Suc l = k"
         have "enum (Suc (Suc i')) = t.enum (Suc l)"
           using i by (simp add: k \<open>Suc l = k\<close> i'_def)
         then have False
           using \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
-          by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: split_if_asm)
+          by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm)
              (metis Suc_lessD n_not_Suc_n upd_inj) }
       with \<open>l < k\<close> have "Suc l < k"
         by arith
       have c_eq: "c = t.enum (Suc l)"
       proof (rule ccontr)

         using i by (simp add: k i'_def)
       also have "\<dots> = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
         using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (simp add: t.enum_Suc l t.upd_inj)
       finally have "(u l = upd i' \<and> u (Suc l) = upd (Suc i')) \<or>
         (u l = upd (Suc i') \<and> u (Suc l) = upd i')"
-        using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: split_if_asm)
+        using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: if_split_asm)
 
       then have "t = s \<or> t = b.enum ` {..n}"
       proof (elim disjE conjE)
         assume u: "u l = upd i'"
         have "c = t.enum (Suc l)" unfolding c_eq ..