author nipkow Sun Mar 06 10:33:34 2016 +0100 (2016-03-06) changeset 62526 347150095fd2 parent 62525 0c9081056829 child 62527 aae9a2a855e0 child 62531 b5d656bf0441
tuned
```     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.42 -by(induction t)
1.43 +by(cases t)
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"
```