src/HOL/Library/RBT_Impl.thy
changeset 63040 eb4ddd18d635
parent 62390 842917225d56
child 63649 e690d6f2185b
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -906,7 +906,7 @@
     1.4    qed simp+
     1.5  next    
     1.6    case (3 xx lta zz vv rta yy ss bb)
     1.7 -  def mt[simp]: mt == "Branch B lta zz vv rta"
     1.8 +  define mt where [simp]: "mt = Branch B lta zz vv rta"
     1.9    from 3 have "inv2 mt \<and> inv1 mt" by simp
    1.10    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)
    1.11    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)
    1.12 @@ -936,7 +936,7 @@
    1.13    qed auto
    1.14  next
    1.15    case (5 xx aa yy ss lta zz vv rta)
    1.16 -  def mt[simp]: mt == "Branch B lta zz vv rta"
    1.17 +  define mt where [simp]: "mt = Branch B lta zz vv rta"
    1.18    from 5 have "inv2 mt \<and> inv1 mt" by simp
    1.19    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)
    1.20    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)
    1.21 @@ -1924,7 +1924,7 @@
    1.22    assumes "is_rbt t1"
    1.23    shows "is_rbt (fold (rbt_insert_with_key f) t2 t1)"
    1.24  proof -
    1.25 -  def xs \<equiv> "entries t2"
    1.26 +  define xs where "xs = entries t2"
    1.27    from assms show ?thesis unfolding fold_def xs_def[symmetric]
    1.28      by(induct xs rule: rev_induct)(auto simp add: rbt_insertwk_is_rbt)
    1.29  qed
    1.30 @@ -1936,7 +1936,7 @@
    1.31     | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> Some v
    1.32                 | Some w \<Rightarrow> Some (f k w v))"
    1.33  proof -
    1.34 -  def xs \<equiv> "entries t1"
    1.35 +  define xs where "xs = entries t1"
    1.36    hence dt1: "distinct (map fst xs)" using t1 by(simp add: distinct_entries)
    1.37    with t2 show ?thesis
    1.38      unfolding fold_def map_of_entries[OF t1, symmetric]