src/HOL/Library/RBT_Impl.thy
 changeset 53374 a14d2a854c02 parent 49810 53f14f62cca2 child 55412 eb2caacf3ba4
```     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Sep 03 00:51:08 2013 +0200
1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 03 01:12:40 2013 +0200
1.3 @@ -146,8 +146,7 @@
1.4      = Set.insert k (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
1.5  proof -
1.6    assume "rbt_sorted (Branch c t1 k v t2)"
1.7 -  moreover from this have "rbt_sorted t1" "rbt_sorted t2" by simp_all
1.8 -  ultimately show ?thesis by (simp add: rbt_lookup_keys)
1.9 +  then show ?thesis by (simp add: rbt_lookup_keys)
1.10  qed
1.11
1.12  lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))"
1.13 @@ -1405,14 +1404,14 @@
1.14        proof(cases "n mod 2 = 0")
1.15          case True note ge0
1.16          moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
1.17 -        moreover with True have "P (n div 2) kvs" by(rule IH)
1.18 +        moreover from True n2 have "P (n div 2) kvs" by(rule IH)
1.19          moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs'
1.20            where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
1.21            by(cases "snd (rbtreeify_f (n div 2) kvs)")
1.22              (auto simp add: snd_def split: prod.split_asm)
1.23          moreover from "1.prems" length_rbtreeify_f[OF n2] ge0
1.24 -        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
1.25 -        moreover with True kvs'[symmetric] refl refl
1.26 +        have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
1.27 +        moreover from True kvs'[symmetric] refl refl n2'
1.28          have "Q (n div 2) kvs'" by(rule IH)
1.29          moreover note feven[unfolded feven_def]
1.30            (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
1.31 @@ -1421,14 +1420,14 @@
1.32        next
1.33          case False note ge0
1.34          moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
1.35 -        moreover with False have "P (n div 2) kvs" by(rule IH)
1.36 +        moreover from False n2 have "P (n div 2) kvs" by(rule IH)
1.37          moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs'
1.38            where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
1.39            by(cases "snd (rbtreeify_f (n div 2) kvs)")
1.40              (auto simp add: snd_def split: prod.split_asm)
1.41          moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 False
1.42 -        have "n div 2 \<le> length kvs'" by(simp add: kvs') arith
1.43 -        moreover with False kvs'[symmetric] refl refl have "P (n div 2) kvs'" by(rule IH)
1.44 +        have n2': "n div 2 \<le> length kvs'" by(simp add: kvs') arith
1.45 +        moreover from False kvs'[symmetric] refl refl n2' have "P (n div 2) kvs'" by(rule IH)
1.46          moreover note fodd[unfolded fodd_def]
1.47          ultimately have "P (Suc (2 * (n div 2))) kvs" by -
1.48          thus ?thesis using False
1.49 @@ -1451,14 +1450,14 @@
1.50        proof(cases "n mod 2 = 0")
1.51          case True note ge0
1.52          moreover from "2.prems" have n2: "n div 2 \<le> Suc (length kvs)" by simp
1.53 -        moreover with True have "Q (n div 2) kvs" by(rule IH)
1.54 +        moreover from True n2 have "Q (n div 2) kvs" by(rule IH)
1.55          moreover from length_rbtreeify_g[OF ge0 n2] ge0 "2.prems" obtain t k v kvs'
1.56            where kvs': "rbtreeify_g (n div 2) kvs = (t, (k, v) # kvs')"
1.57            by(cases "snd (rbtreeify_g (n div 2) kvs)")
1.58              (auto simp add: snd_def split: prod.split_asm)
1.59          moreover from "2.prems" length_rbtreeify_g[OF ge0 n2] ge0
1.60 -        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
1.61 -        moreover with True kvs'[symmetric] refl refl
1.62 +        have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
1.63 +        moreover from True kvs'[symmetric] refl refl  n2'
1.64          have "Q (n div 2) kvs'" by(rule IH)
1.65          moreover note geven[unfolded geven_def]
1.66          ultimately have "Q (2 * (n div 2)) kvs" by -
1.67 @@ -1467,14 +1466,14 @@
1.68        next
1.69          case False note ge0
1.70          moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp
1.71 -        moreover with False have "P (n div 2) kvs" by(rule IH)
1.72 +        moreover from False n2 have "P (n div 2) kvs" by(rule IH)
1.73          moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs'
1.74            where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
1.75            by(cases "snd (rbtreeify_f (n div 2) kvs)")
1.76              (auto simp add: snd_def split: prod.split_asm, arith)
1.77          moreover from "2.prems" length_rbtreeify_f[OF n2] ge0 False
1.78 -        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
1.79 -        moreover with False kvs'[symmetric] refl refl
1.80 +        have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
1.81 +        moreover from False kvs'[symmetric] refl refl n2'
1.82          have "Q (n div 2) kvs'" by(rule IH)
1.83          moreover note godd[unfolded godd_def]
1.84          ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
```