tuned
authornipkow
Sun Mar 06 10:33:34 2016 +0100 (2016-03-06)
changeset 62526347150095fd2
parent 62525 0c9081056829
child 62527 aae9a2a855e0
child 62531 b5d656bf0441
tuned
src/HOL/Data_Structures/AA_Set.thy
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/RBT_Set.thy
     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  
     2.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Sat Mar 05 23:05:07 2016 +0100
     2.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Sun Mar 06 10:33:34 2016 +0100
     2.3 @@ -108,7 +108,7 @@
     2.4  
     2.5  lemma inorder_del_root:
     2.6    "inorder (del_root (Node h l a r)) = inorder l @ inorder r"
     2.7 -by(induction "Node h l a r" arbitrary: l a r h rule: del_root.induct)
     2.8 +by(cases "Node h l a r" rule: del_root.cases)
     2.9    (auto simp: inorder_balL inorder_balR inorder_del_maxD split: if_splits prod.splits)
    2.10  
    2.11  theorem inorder_delete:
     3.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Sat Mar 05 23:05:07 2016 +0100
     3.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sun Mar 06 10:33:34 2016 +0100
     3.3 @@ -160,7 +160,7 @@
     3.4  subsubsection "Proofs for insertion"
     3.5  
     3.6  lemma inorder_n1: "inorder(n1 t) = inorder t"
     3.7 -by(induction t rule: n1.induct) (auto simp: sorted_lems)
     3.8 +by(cases t rule: n1.cases) (auto simp: sorted_lems)
     3.9  
    3.10  context insert
    3.11  begin
    3.12 @@ -190,7 +190,7 @@
    3.13  by(cases t) auto
    3.14  
    3.15  lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
    3.16 -by(induction l a r rule: n2.induct) (auto)
    3.17 +by(cases "(l,a,r)" rule: n2.cases) (auto)
    3.18  
    3.19  lemma inorder_del_min:
    3.20    "t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
     4.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Mar 05 23:05:07 2016 +0100
     4.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Mar 06 10:33:34 2016 +0100
     4.3 @@ -47,11 +47,11 @@
     4.4  subsection "Functional Correctness Proofs"
     4.5  
     4.6  lemma inorder_paint: "inorder(paint c t) = inorder t"
     4.7 -by(induction t) (auto)
     4.8 +by(cases t) (auto)
     4.9  
    4.10  lemma inorder_bal:
    4.11    "inorder(bal l a r) = inorder l @ a # inorder r"
    4.12 -by(induction l a r rule: bal.induct) (auto)
    4.13 +by(cases "(l,a,r)" rule: bal.cases) (auto)
    4.14  
    4.15  lemma inorder_ins:
    4.16    "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
    4.17 @@ -63,11 +63,11 @@
    4.18  
    4.19  lemma inorder_balL:
    4.20    "inorder(balL l a r) = inorder l @ a # inorder r"
    4.21 -by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_paint)
    4.22 +by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
    4.23  
    4.24  lemma inorder_balR:
    4.25    "inorder(balR l a r) = inorder l @ a # inorder r"
    4.26 -by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_paint)
    4.27 +by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
    4.28  
    4.29  lemma inorder_combine:
    4.30    "inorder(combine l r) = inorder l @ inorder r"