# HG changeset patch
# User nipkow
# Date 1457256814 -3600
# Node ID 347150095fd25aabab32df27ec33c0f2027db222
# Parent  0c90810568299a4d070aefa4de9e5bbea02df57f
tuned

diff -r 0c9081056829 -r 347150095fd2 src/HOL/Data_Structures/AA_Set.thy
--- 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)
 
diff -r 0c9081056829 -r 347150095fd2 src/HOL/Data_Structures/AVL_Set.thy
--- 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:
diff -r 0c9081056829 -r 347150095fd2 src/HOL/Data_Structures/Brother12_Set.thy
--- 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>
diff -r 0c9081056829 -r 347150095fd2 src/HOL/Data_Structures/RBT_Set.thy
--- 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"