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  
    1.41  lemma inorder_adjust: "t \<noteq> Leaf \<Longrightarrow> pre_adjust t \<Longrightarrow> inorder(adjust t) = inorder t"
    1.42 -by(induction t)
    1.43 +by(cases t)
    1.44    (auto simp: adjust_def inorder_skew inorder_split invar.simps(2) pre_adjust.simps
    1.45       split: tree.splits)
    1.46