src/HOL/List.thy

 
 fun tac ctxt [] =
       resolve_tac ctxt [set_singleton] 1 ORELSE
       resolve_tac ctxt [inst_Collect_mem_eq] 1
   | tac ctxt (If :: cont) =
-      Splitter.split_tac ctxt @{thms split_if} 1
+      Splitter.split_tac ctxt @{thms if_split} 1
       THEN resolve_tac ctxt @{thms conjI} 1
       THEN resolve_tac ctxt @{thms impI} 1
       THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
         CONVERSION (right_hand_set_comprehension_conv (K
           (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv

   "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
 proof (induct xs)
   case Nil thus ?case by simp
 next
   case (Cons x xs) thus ?case
-    apply (auto split:split_if_asm)
+    apply (auto split:if_split_asm)
     using length_filter_le[of P xs] apply arith
   done
 qed
 
 lemma length_filter_conv_card:

 lemma append_butlast_last_id [simp]:
   "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
 by (induct xs) auto
 
 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
-by (induct xs) (auto split: split_if_asm)
+by (induct xs) (auto split: if_split_asm)
 
 lemma in_set_butlast_appendI:
   "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
 by (auto dest: in_set_butlastD simp add: butlast_append)
 

 lemma dropWhile_last:
   "x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> last (dropWhile P xs) = last xs"
 by (auto simp add: dropWhile_append3 in_set_conv_decomp)
 
 lemma set_dropWhileD: "x \<in> set (dropWhile P xs) \<Longrightarrow> x \<in> set xs"
-by (induct xs) (auto split: split_if_asm)
+by (induct xs) (auto split: if_split_asm)
 
 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
-by (induct xs) (auto split: split_if_asm)
+by (induct xs) (auto split: if_split_asm)
 
 lemma takeWhile_eq_all_conv[simp]:
   "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
 by(induct xs, auto)
 

   proof (cases "x \<in> set xs")
     case False with Cons show ?thesis by simp
   next
     case True with Cons.prems
     have "card (set xs) = Suc (length xs)"
-      by (simp add: card_insert_if split: split_if_asm)
+      by (simp add: card_insert_if split: if_split_asm)
     moreover have "card (set xs) \<le> length xs" by (rule card_length)
     ultimately have False by simp
     thus ?thesis ..
   qed
 qed

 by (induct xs) (auto)
 
 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
 apply (induct n == "length ws" arbitrary:ws) apply simp
 apply(case_tac ws) apply simp
-apply (simp split:split_if_asm)
+apply (simp split:if_split_asm)
 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
 done
 
 lemma not_distinct_conv_prefix:
   defines "dec as xs y ys \<equiv> y \<in> set xs \<and> distinct xs \<and> as = xs @ y # ys"

   "remdups_adj (xs\<^sub>1 @ x # xs\<^sub>2) = remdups_adj (xs\<^sub>1 @ [x]) @ tl (remdups_adj (x # xs\<^sub>2))"
 by (induct xs\<^sub>1 rule: remdups_adj.induct, simp_all)
 
 lemma remdups_adj_singleton:
   "remdups_adj xs = [x] \<Longrightarrow> xs = replicate (length xs) x"
-by (induct xs rule: remdups_adj.induct, auto split: split_if_asm)
+by (induct xs rule: remdups_adj.induct, auto split: if_split_asm)
 
 lemma remdups_adj_map_injective:
   assumes "inj f"
   shows "remdups_adj (map f xs) = map f (remdups_adj xs)"
 by (induct xs rule: remdups_adj.induct) (auto simp add: injD[OF assms])

   "sorted l \<Longrightarrow> sorted (remdups l)"
 by (induct l) (auto simp: sorted_Cons)
 
 lemma sorted_remdups_adj[simp]:
   "sorted xs \<Longrightarrow> sorted (remdups_adj xs)"
-by (induct xs rule: remdups_adj.induct, simp_all split: split_if_asm add: sorted_Cons)
+by (induct xs rule: remdups_adj.induct, simp_all split: if_split_asm add: sorted_Cons)
 
 lemma sorted_distinct_set_unique:
 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
 shows "xs = ys"
 proof -

   "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
   by (auto simp add: Id_on_def)
 
 lemma [code]:
   "R `` S = List.map_project (%(x, y). if x : S then Some y else None) R"
-unfolding map_project_def by (auto split: prod.split split_if_asm)
+unfolding map_project_def by (auto split: prod.split if_split_asm)
 
 lemma trancl_set_ntrancl [code]:
   "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
   by (simp add: finite_trancl_ntranl)