--- a/src/HOL/Data_Structures/AA_Set.thy Sat Mar 05 23:05:07 2016 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy Sun Mar 06 10:33:34 2016 +0100
@@ -120,10 +120,10 @@
by(cases t) auto
lemma lvl_skew: "lvl (skew t) = lvl t"
-by(induction t rule: skew.induct) auto
+by(cases t rule: skew.cases) auto
lemma lvl_split: "lvl (split t) = lvl t \<or> lvl (split t) = lvl t + 1 \<and> sngl (split t)"
-by(induction t rule: split.induct) auto
+by(cases t rule: split.cases) auto
lemma invar_2Nodes:"invar (Node lv l x (Node rlv rl rx rr)) =
(invar l \<and> invar \<langle>rlv, rl, rx, rr\<rangle> \<and> lv = Suc (lvl l) \<and>
@@ -155,7 +155,7 @@
using lvl_insert_aux by blast
lemma lvl_insert_sngl: "invar t \<Longrightarrow> sngl t \<Longrightarrow> lvl(insert x t) = lvl t"
-proof (induction t rule: "insert.induct" )
+proof (induction t rule: insert.induct)
case (2 x lv t1 a t2)
consider (LT) "x < a" | (GT) "x > a" | (EQ) "x = a"
using less_linear by blast
@@ -174,10 +174,10 @@
qed simp
lemma skew_invar: "invar t \<Longrightarrow> skew t = t"
-by(induction t rule: skew.induct) auto
+by(cases t rule: skew.cases) auto
lemma split_invar: "invar t \<Longrightarrow> split t = t"
-by(induction t rule: split.induct) clarsimp+
+by(cases t rule: split.cases) clarsimp+
lemma invar_NodeL:
"\<lbrakk> invar(Node n l x r); invar l'; lvl l' = lvl l \<rbrakk> \<Longrightarrow> invar(Node n l' x r)"
@@ -468,7 +468,7 @@
subsubsection "Proofs for delete"
lemma inorder_adjust: "t \<noteq> Leaf \<Longrightarrow> pre_adjust t \<Longrightarrow> inorder(adjust t) = inorder t"
-by(induction t)
+by(cases t)
(auto simp: adjust_def inorder_skew inorder_split invar.simps(2) pre_adjust.simps
split: tree.splits)
--- a/src/HOL/Data_Structures/AVL_Set.thy Sat Mar 05 23:05:07 2016 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy Sun Mar 06 10:33:34 2016 +0100
@@ -108,7 +108,7 @@
lemma inorder_del_root:
"inorder (del_root (Node h l a r)) = inorder l @ inorder r"
-by(induction "Node h l a r" arbitrary: l a r h rule: del_root.induct)
+by(cases "Node h l a r" rule: del_root.cases)
(auto simp: inorder_balL inorder_balR inorder_del_maxD split: if_splits prod.splits)
theorem inorder_delete:
--- a/src/HOL/Data_Structures/Brother12_Set.thy Sat Mar 05 23:05:07 2016 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Sun Mar 06 10:33:34 2016 +0100
@@ -160,7 +160,7 @@
subsubsection "Proofs for insertion"
lemma inorder_n1: "inorder(n1 t) = inorder t"
-by(induction t rule: n1.induct) (auto simp: sorted_lems)
+by(cases t rule: n1.cases) (auto simp: sorted_lems)
context insert
begin
@@ -190,7 +190,7 @@
by(cases t) auto
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: n2.induct) (auto)
+by(cases "(l,a,r)" rule: n2.cases) (auto)
lemma inorder_del_min:
"t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
--- a/src/HOL/Data_Structures/RBT_Set.thy Sat Mar 05 23:05:07 2016 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sun Mar 06 10:33:34 2016 +0100
@@ -47,11 +47,11 @@
subsection "Functional Correctness Proofs"
lemma inorder_paint: "inorder(paint c t) = inorder t"
-by(induction t) (auto)
+by(cases t) (auto)
lemma inorder_bal:
"inorder(bal l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: bal.induct) (auto)
+by(cases "(l,a,r)" rule: bal.cases) (auto)
lemma inorder_ins:
"sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
@@ -63,11 +63,11 @@
lemma inorder_balL:
"inorder(balL l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_paint)
+by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
lemma inorder_balR:
"inorder(balR l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_paint)
+by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
lemma inorder_combine:
"inorder(combine l r) = inorder l @ inorder r"