src/HOL/Library/RBT_Impl.thy

       with \<open>xx = yy\<close> 2 \<open>xx = k\<close> show ?thesis by (simp add: combine_in_tree)
     qed (simp add: combine_in_tree)
   qed simp+
 next    
   case (3 xx lta zz vv rta yy ss bb)
-  def mt[simp]: mt == "Branch B lta zz vv rta"
+  define mt where [simp]: "mt = Branch B lta zz vv rta"
   from 3 have "inv2 mt \<and> inv1 mt" by simp
   hence "inv2 (rbt_del xx mt) \<and> (color_of mt = R \<and> bheight (rbt_del xx mt) = bheight mt \<and> inv1 (rbt_del xx mt) \<or> color_of mt = B \<and> bheight (rbt_del xx mt) = bheight mt - 1 \<and> inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
   with 3 have 4: "entry_in_tree k v (rbt_del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree)
   thus ?case proof (cases "xx = k")
     case True

     hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
     with True "4_2" show ?thesis by (auto simp: rbt_greater_nit)
   qed auto
 next
   case (5 xx aa yy ss lta zz vv rta)
-  def mt[simp]: mt == "Branch B lta zz vv rta"
+  define mt where [simp]: "mt = Branch B lta zz vv rta"
   from 5 have "inv2 mt \<and> inv1 mt" by simp
   hence "inv2 (rbt_del xx mt) \<and> (color_of mt = R \<and> bheight (rbt_del xx mt) = bheight mt \<and> inv1 (rbt_del xx mt) \<or> color_of mt = B \<and> bheight (rbt_del xx mt) = bheight mt - 1 \<and> inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
   with 5 have 3: "entry_in_tree k v (rbt_del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree)
   thus ?case proof (cases "xx = k")
     case True

 
 lemma is_rbt_fold_rbt_insertwk:
   assumes "is_rbt t1"
   shows "is_rbt (fold (rbt_insert_with_key f) t2 t1)"
 proof -
-  def xs \<equiv> "entries t2"
+  define xs where "xs = entries t2"
   from assms show ?thesis unfolding fold_def xs_def[symmetric]
     by(induct xs rule: rev_induct)(auto simp add: rbt_insertwk_is_rbt)
 qed
 
 lemma rbt_lookup_fold_rbt_insertwk:

   shows "rbt_lookup (fold (rbt_insert_with_key f) t1 t2) k =
   (case rbt_lookup t1 k of None \<Rightarrow> rbt_lookup t2 k
    | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> Some v
                | Some w \<Rightarrow> Some (f k w v))"
 proof -
-  def xs \<equiv> "entries t1"
+  define xs where "xs = entries t1"
   hence dt1: "distinct (map fst xs)" using t1 by(simp add: distinct_entries)
   with t2 show ?thesis
     unfolding fold_def map_of_entries[OF t1, symmetric]
       xs_def[symmetric] distinct_map_of_rev[OF dt1, symmetric]
     apply(induct xs rule: rev_induct)