src/HOL/Data_Structures/AA_Set.thy
 changeset 62526 347150095fd2 parent 62496 f187aaf602c4 child 63411 e051eea34990
```     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Sat Mar 05 23:05:07 2016 +0100
1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Sun Mar 06 10:33:34 2016 +0100
1.3 @@ -120,10 +120,10 @@
1.4  by(cases t) auto
1.5
1.6  lemma lvl_skew: "lvl (skew t) = lvl t"
1.7 -by(induction t rule: skew.induct) auto
1.8 +by(cases t rule: skew.cases) auto
1.9
1.10  lemma lvl_split: "lvl (split t) = lvl t \<or> lvl (split t) = lvl t + 1 \<and> sngl (split t)"
1.11 -by(induction t rule: split.induct) auto
1.12 +by(cases t rule: split.cases) auto
1.13
1.14  lemma invar_2Nodes:"invar (Node lv l x (Node rlv rl rx rr)) =
1.15       (invar l \<and> invar \<langle>rlv, rl, rx, rr\<rangle> \<and> lv = Suc (lvl l) \<and>
1.16 @@ -155,7 +155,7 @@
1.17  using lvl_insert_aux by blast
1.18
1.19  lemma lvl_insert_sngl: "invar t \<Longrightarrow> sngl t \<Longrightarrow> lvl(insert x t) = lvl t"
1.20 -proof (induction t rule: "insert.induct" )
1.21 +proof (induction t rule: insert.induct)
1.22    case (2 x lv t1 a t2)
1.23    consider (LT) "x < a" | (GT) "x > a" | (EQ) "x = a"
1.24      using less_linear by blast
1.25 @@ -174,10 +174,10 @@
1.26  qed simp
1.27
1.28  lemma skew_invar: "invar t \<Longrightarrow> skew t = t"
1.29 -by(induction t rule: skew.induct) auto
1.30 +by(cases t rule: skew.cases) auto
1.31
1.32  lemma split_invar: "invar t \<Longrightarrow> split t = t"
1.33 -by(induction t rule: split.induct) clarsimp+
1.34 +by(cases t rule: split.cases) clarsimp+
1.35
1.36  lemma invar_NodeL:
1.37    "\<lbrakk> invar(Node n l x r); invar l'; lvl l' = lvl l \<rbrakk> \<Longrightarrow> invar(Node n l' x r)"
1.38 @@ -468,7 +468,7 @@
1.39  subsubsection "Proofs for delete"
1.40