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 -