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.6  lemma inorder_paint: "inorder(paint c t) = inorder t"
1.7 -by(induction t) (auto)
1.8 +by(cases t) (auto)
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.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.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.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.29  lemma inorder_combine:
1.30    "inorder(combine l r) = inorder l @ inorder r"