src/HOL/Data_Structures/RBT_Set.thy
changeset 62526 347150095fd2
parent 61754 862daa8144f3
child 63411 e051eea34990
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Mar 05 23:05:07 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Mar 06 10:33:34 2016 +0100
     1.3 @@ -47,11 +47,11 @@
     1.4  subsection "Functional Correctness Proofs"
     1.5  
     1.6  lemma inorder_paint: "inorder(paint c t) = inorder t"
     1.7 -by(induction t) (auto)
     1.8 +by(cases t) (auto)
     1.9  
    1.10  lemma inorder_bal:
    1.11    "inorder(bal l a r) = inorder l @ a # inorder r"
    1.12 -by(induction l a r rule: bal.induct) (auto)
    1.13 +by(cases "(l,a,r)" rule: bal.cases) (auto)
    1.14  
    1.15  lemma inorder_ins:
    1.16    "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
    1.17 @@ -63,11 +63,11 @@
    1.18  
    1.19  lemma inorder_balL:
    1.20    "inorder(balL l a r) = inorder l @ a # inorder r"
    1.21 -by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_paint)
    1.22 +by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
    1.23  
    1.24  lemma inorder_balR:
    1.25    "inorder(balR l a r) = inorder l @ a # inorder r"
    1.26 -by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_paint)
    1.27 +by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
    1.28  
    1.29  lemma inorder_combine:
    1.30    "inorder(combine l r) = inorder l @ inorder r"