# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1693046185 -3600
# Node ID 7ed1759fe1bdbefd82c6be7e381549589ece652f
# Parent  d96dd69903fb3abd5bf55ee38cf82b473e6422f9
tidying up old apply-style proofs

diff -r d96dd69903fb -r 7ed1759fe1bd src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Fri Aug 25 09:56:45 2023 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Sat Aug 26 11:36:25 2023 +0100
@@ -3,50 +3,49 @@
 section "Arrays via Braun Trees"
 
 theory Array_Braun
-imports
-  Array_Specs
-  Braun_Tree
+  imports
+    Array_Specs
+    Braun_Tree
 begin
 
 subsection "Array"
 
 fun lookup1 :: "'a tree \<Rightarrow> nat \<Rightarrow> 'a" where
-"lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))"
+  "lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))"
 
 fun update1 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"update1 n x Leaf = Node Leaf x Leaf" |
-"update1 n x (Node l a r) =
+  "update1 n x Leaf = Node Leaf x Leaf" |
+  "update1 n x (Node l a r) =
   (if n=1 then Node l x r else
    if even n then Node (update1 (n div 2) x l) a r
             else Node l a (update1 (n div 2) x r))"
 
 fun adds :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"adds [] n t = t" |
-"adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)"
+  "adds [] n t = t" |
+  "adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)"
 
 fun list :: "'a tree \<Rightarrow> 'a list" where
-"list Leaf = []" |
-"list (Node l x r) = x # splice (list l) (list r)"
+  "list Leaf = []" |
+  "list (Node l x r) = x # splice (list l) (list r)"
 
 
 subsubsection "Functional Correctness"
 
 lemma size_list: "size(list t) = size t"
-by(induction t)(auto)
+  by(induction t)(auto)
 
 lemma minus1_div2: "(n - Suc 0) div 2 = (if odd n then n div 2 else n div 2 - 1)"
-by auto arith
+  by auto arith
 
 lemma nth_splice: "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk>
   \<Longrightarrow> splice xs ys ! n = (if even n then xs else ys) ! (n div 2)"
-apply(induction xs ys arbitrary: n rule: splice.induct)
-apply (auto simp: nth_Cons' minus1_div2)
-done
+proof(induction xs ys arbitrary: n rule: splice.induct)
+qed (auto simp: nth_Cons' minus1_div2)
 
 lemma div2_in_bounds:
   "\<lbrakk> braun (Node l x r); n \<in> {1..size(Node l x r)}; n > 1 \<rbrakk> \<Longrightarrow>
    (odd n \<longrightarrow> n div 2 \<in> {1..size r}) \<and> (even n \<longrightarrow> n div 2 \<in> {1..size l})"
-by auto arith
+  by auto arith
 
 declare upt_Suc[simp del]
 
@@ -63,7 +62,7 @@
 qed
 
 lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]"
-by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
+  by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
 
 
 paragraph \<open>\<^const>\<open>update1\<close>\<close>
@@ -96,18 +95,18 @@
 qed
 
 lemma list_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
-by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1)
+  by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1)
 
 text \<open>A second proof of @{thm list_update1}:\<close>
 
 lemma diff1_eq_iff: "n > 0 \<Longrightarrow> n - Suc 0 = m \<longleftrightarrow> n = m+1"
-by arith
+  by arith
 
 lemma list_update_splice:
   "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk> \<Longrightarrow>
   (splice xs ys) [n := x] =
   (if even n then splice (xs[n div 2 := x]) ys else splice xs (ys[n div 2 := x]))"
-by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split)
+  by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split)
 
 lemma list_update2: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
 proof(induction t arbitrary: n)
@@ -122,35 +121,35 @@
 
 lemma splice_last: shows
   "size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"
-and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"
-by(induction xs ys arbitrary: x y rule: splice.induct) (auto)
+  and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"
+  by(induction xs ys arbitrary: x y rule: splice.induct) (auto)
 
 lemma list_add_hi: "braun t \<Longrightarrow> list(update1 (Suc(size t)) x t) = list t @ [x]"
-by(induction t)(auto simp: splice_last size_list)
+  by(induction t)(auto simp: splice_last size_list)
 
 lemma size_add_hi: "braun t \<Longrightarrow> m = size t \<Longrightarrow> size(update1 (Suc m) x t) = size t + 1"
-by(induction t arbitrary: m)(auto)
+  by(induction t arbitrary: m)(auto)
 
 lemma braun_add_hi: "braun t \<Longrightarrow> braun(update1 (Suc(size t)) x t)"
-by(induction t)(auto simp: size_add_hi)
+  by(induction t)(auto simp: size_add_hi)
 
 lemma size_braun_adds:
   "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> size(adds xs n t) = size t + length xs \<and> braun (adds xs n t)"
-by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi)
+  by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi)
 
 lemma list_adds: "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> list(adds xs n t) = list t @ xs"
-by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi)
+  by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi)
 
 
 subsubsection "Array Implementation"
 
 interpretation A: Array
-where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
-and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
-and len = "\<lambda>(t,l). l"
-and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
-and invar = "\<lambda>(t,l). braun t \<and> l = size t"
-and list = "\<lambda>(t,l). list t"
+  where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
+    and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
+    and len = "\<lambda>(t,l). l"
+    and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
+    and invar = "\<lambda>(t,l). braun t \<and> l = size t"
+    and list = "\<lambda>(t,l). list t"
 proof (standard, goal_cases)
   case 1 thus ?case by (simp add: nth_list_lookup1 split: prod.splits)
 next
@@ -169,20 +168,20 @@
 subsection "Flexible Array"
 
 fun add_lo where
-"add_lo x Leaf = Node Leaf x Leaf" |
-"add_lo x (Node l a r) = Node (add_lo a r) x l"
+  "add_lo x Leaf = Node Leaf x Leaf" |
+  "add_lo x (Node l a r) = Node (add_lo a r) x l"
 
 fun merge where
-"merge Leaf r = r" |
-"merge (Node l a r) rr = Node rr a (merge l r)"
+  "merge Leaf r = r" |
+  "merge (Node l a r) rr = Node rr a (merge l r)"
 
 fun del_lo where
-"del_lo Leaf = Leaf" |
-"del_lo (Node l a r) = merge l r"
+  "del_lo Leaf = Leaf" |
+  "del_lo (Node l a r) = merge l r"
 
 fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"del_hi n Leaf = Leaf" |
-"del_hi n (Node l x r) =
+  "del_hi n Leaf = Leaf" |
+  "del_hi n (Node l x r) =
   (if n = 1 then Leaf
    else if even n
        then Node (del_hi (n div 2) l) x r
@@ -195,58 +194,56 @@
 paragraph \<open>\<^const>\<open>add_lo\<close>\<close>
 
 lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"
-by(induction t arbitrary: a) auto
+  by(induction t arbitrary: a) auto
 
 lemma braun_add_lo: "braun t \<Longrightarrow> braun(add_lo x t)"
-by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
+  by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
 
 
 paragraph \<open>\<^const>\<open>del_lo\<close>\<close>
 
 lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"
-by (induction l r rule: merge.induct) auto
+  by (induction l r rule: merge.induct) auto
 
 lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)"
-by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list)
+  by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list)
 
 lemma list_del_lo: "braun t \<Longrightarrow> list(del_lo t) = tl (list t)"
-by (cases t) (simp_all add: list_merge)
+  by (cases t) (simp_all add: list_merge)
 
 lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)"
-by (cases t) (simp_all add: braun_merge)
+  by (cases t) (simp_all add: braun_merge)
 
 
 paragraph \<open>\<^const>\<open>del_hi\<close>\<close>
 
 lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"
-by(cases t) simp_all
+  by(cases t) simp_all
 
 lemma butlast_splice: "butlast (splice xs ys) =
   (if size xs > size ys then splice (butlast xs) ys else splice xs (butlast ys))"
-by(induction xs ys rule: splice.induct) (auto)
+  by(induction xs ys rule: splice.induct) (auto)
 
 lemma list_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> list(del_hi st t) = butlast(list t)"
-apply(induction t arbitrary: st)
-by(auto simp: list_Nil_iff size_list butlast_splice)
+  by (induction t arbitrary: st) (auto simp: list_Nil_iff size_list butlast_splice)
 
 lemma braun_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> braun(del_hi st t)"
-apply(induction t arbitrary: st)
-by(auto simp: list_del_hi simp flip: size_list)
+  by (induction t arbitrary: st) (auto simp: list_del_hi simp flip: size_list)
 
 
 subsubsection "Flexible Array Implementation"
 
 interpretation AF: Array_Flex
-where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
-and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
-and len = "\<lambda>(t,l). l"
-and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
-and invar = "\<lambda>(t,l). braun t \<and> l = size t"
-and list = "\<lambda>(t,l). list t"
-and add_lo = "\<lambda>x (t,l). (add_lo x t, l+1)"
-and del_lo = "\<lambda>(t,l). (del_lo t, l-1)"
-and add_hi = "\<lambda>x (t,l). (update1 (Suc l) x t, l+1)"
-and del_hi = "\<lambda>(t,l). (del_hi l t, l-1)"
+  where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
+    and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
+    and len = "\<lambda>(t,l). l"
+    and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
+    and invar = "\<lambda>(t,l). braun t \<and> l = size t"
+    and list = "\<lambda>(t,l). list t"
+    and add_lo = "\<lambda>x (t,l). (add_lo x t, l+1)"
+    and del_lo = "\<lambda>(t,l). (del_lo t, l-1)"
+    and add_hi = "\<lambda>x (t,l). (update1 (Suc l) x t, l+1)"
+    and del_hi = "\<lambda>(t,l). (del_hi l t, l-1)"
 proof (standard, goal_cases)
   case 1 thus ?case by (simp add: list_add_lo split: prod.splits)
 next
@@ -272,37 +269,37 @@
 subsubsection \<open>Size\<close>
 
 fun diff :: "'a tree \<Rightarrow> nat \<Rightarrow> nat" where
-"diff Leaf _ = 0" |
-"diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))"
+  "diff Leaf _ = 0" |
+  "diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))"
 
 fun size_fast :: "'a tree \<Rightarrow> nat" where
-"size_fast Leaf = 0" |
-"size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
+  "size_fast Leaf = 0" |
+  "size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
 
 declare Let_def[simp]
 
 lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n"
-by(induction t arbitrary: n) auto
+  by (induction t arbitrary: n) auto
 
 lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"
-by(induction t) (auto simp add: diff)
+  by (induction t) (auto simp add: diff)
 
 
 subsubsection \<open>Initialization with 1 element\<close>
 
 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
-"braun_of_naive x n = (if n=0 then Leaf
+  "braun_of_naive x n = (if n=0 then Leaf
   else let m = (n-1) div 2
        in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
        else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
 
 fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where
-"braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
+  "braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
   else let (s,t) = braun2_of x ((n-1) div 2)
        in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))"
 
 definition braun_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
-"braun_of x n = fst (braun2_of x n)"
+  "braun_of x n = fst (braun2_of x n)"
 
 declare braun2_of.simps [simp del]
 
@@ -325,10 +322,10 @@
 qed
 
 corollary braun_braun_of: "braun(braun_of x n)"
-unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)
+  unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)
 
 corollary list_braun_of: "list(braun_of x n) = replicate n x"
-unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)
+  unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)
 
 
 subsubsection "Proof Infrastructure"
@@ -338,8 +335,8 @@
 paragraph \<open>\<open>take_nths\<close>\<close>
 
 fun take_nths :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"take_nths i k [] = []" |
-"take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
+  "take_nths i k [] = []" |
+  "take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
   else take_nths (i - 1) k xs)"
 
 text \<open>This is the more concise definition but seems to complicate the proofs:\<close>
@@ -353,60 +350,62 @@
   show ?case
   proof cases
     assume [simp]: "i = 0"
-    have "(\<Union>n. {(n+1) * 2 ^ k - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k}"
-      apply (auto simp del: mult_Suc)
+    have "\<And>x n. Suc x = n * 2 ^ k \<Longrightarrow> \<exists>xa. x = Suc xa * 2 ^ k - Suc 0"
       by (metis diff_Suc_Suc diff_zero mult_eq_0_iff not0_implies_Suc)
+    then have "(\<Union>n. {(n+1) * 2 ^ k - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k}"
+      by (auto simp del: mult_Suc)
     thus ?thesis by (simp add: Cons.IH ac_simps nths_Cons)
   next
     assume [arith]: "i \<noteq> 0"
-    have "(\<Union>n. {n * 2 ^ k + i - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k + i}"
-      apply auto
+    have "\<And>x n. Suc x = n * 2 ^ k + i \<Longrightarrow> \<exists>xa. x = xa * 2 ^ k + i - Suc 0"
       by (metis diff_Suc_Suc diff_zero)
+    then have "(\<Union>n. {n * 2 ^ k + i - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k + i}"
+      by auto
     thus ?thesis by (simp add: Cons.IH nths_Cons)
   qed
 qed
 
 lemma take_nths_drop:
   "take_nths i k (drop j xs) = take_nths (i + j) k xs"
-by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)
+  by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)
 
 lemma take_nths_00:
   "take_nths 0 0 xs = xs"
-by (induct xs; simp)
+  by (induct xs; simp)
 
 lemma splice_take_nths:
   "splice (take_nths 0 (Suc 0) xs) (take_nths (Suc 0) (Suc 0) xs) = xs"
-by (induct xs; simp)
+  by (induct xs; simp)
 
 lemma take_nths_take_nths:
   "take_nths i m (take_nths j n xs) = take_nths ((i * 2^n) + j) (m + n) xs"
-by (induct xs arbitrary: i j; simp add: algebra_simps power_add)
+  by (induct xs arbitrary: i j; simp add: algebra_simps power_add)
 
 lemma take_nths_empty:
   "(take_nths i k xs = []) = (length xs \<le> i)"
-by (induction xs arbitrary: i k) auto
+  by (induction xs arbitrary: i k) auto
 
 lemma hd_take_nths:
   "i < length xs \<Longrightarrow> hd(take_nths i k xs) = xs ! i"
-by (induction xs arbitrary: i k) auto
+  by (induction xs arbitrary: i k) auto
 
 lemma take_nths_01_splice:
   "\<lbrakk> length xs = length ys \<or> length xs = length ys + 1 \<rbrakk> \<Longrightarrow>
    take_nths 0 (Suc 0) (splice xs ys) = xs \<and>
    take_nths (Suc 0) (Suc 0) (splice xs ys) = ys"
-by (induct xs arbitrary: ys; case_tac ys; simp)
+  by (induct xs arbitrary: ys; case_tac ys; simp)
 
 lemma length_take_nths_00:
   "length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) \<or>
    length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) + 1"
-by (induct xs) auto
+  by (induct xs) auto
 
 
 paragraph \<open>\<open>braun_list\<close>\<close>
 
 fun braun_list :: "'a tree \<Rightarrow> 'a list \<Rightarrow> bool" where
-"braun_list Leaf xs = (xs = [])" |
-"braun_list (Node l x r) xs = (xs \<noteq> [] \<and> x = hd xs \<and>
+  "braun_list Leaf xs = (xs = [])" |
+  "braun_list (Node l x r) xs = (xs \<noteq> [] \<and> x = hd xs \<and>
     braun_list l (take_nths 1 1 xs) \<and>
     braun_list r (take_nths 2 1 xs))"
 
@@ -426,14 +425,14 @@
 subsubsection \<open>Converting a list of elements into a Braun tree\<close>
 
 fun nodes :: "'a tree list \<Rightarrow> 'a list \<Rightarrow> 'a tree list \<Rightarrow> 'a tree list" where
-"nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" |
-"nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" |
-"nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" |
-"nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" |
-"nodes ls [] rs = []"
+  "nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" |
+  "nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" |
+  "nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" |
+  "nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" |
+  "nodes ls [] rs = []"
 
 fun brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree list" where
-"brauns k xs = (if xs = [] then [] else
+  "brauns k xs = (if xs = [] then [] else
    let ys = take (2^k) xs;
        zs = drop (2^k) xs;
        ts = brauns (k+1) zs
@@ -442,10 +441,10 @@
 declare brauns.simps[simp del]
 
 definition brauns1 :: "'a list \<Rightarrow> 'a tree" where
-"brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"
+  "brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"
 
 fun T_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
-"T_brauns k xs = (if xs = [] then 0 else
+  "T_brauns k xs = (if xs = [] then 0 else
    let ys = take (2^k) xs;
        zs = drop (2^k) xs;
        ts = brauns (k+1) zs
@@ -458,14 +457,14 @@
 
 lemma length_nodes:
   "length (nodes ls xs rs) = length xs"
-by (induct ls xs rs rule: nodes.induct; simp)
+  by (induct ls xs rs rule: nodes.induct; simp)
 
 lemma nth_nodes:
   "i < length xs \<Longrightarrow> nodes ls xs rs ! i =
   Node (if i < length ls then ls ! i else Leaf) (xs ! i)
     (if i < length rs then rs ! i else Leaf)"
-by (induct ls xs rs arbitrary: i rule: nodes.induct;
-    simp add: nth_Cons split: nat.split)
+  by (induct ls xs rs arbitrary: i rule: nodes.induct;
+      simp add: nth_Cons split: nat.split)
 
 theorem length_brauns:
   "length (brauns k xs) = min (length xs) (2 ^ k)"
@@ -487,13 +486,13 @@
   show ?case
     using less.prems
     by (auto simp: brauns.simps[of k xs] nth_nodes take_nths_take_nths
-                   IH take_nths_empty hd_take_nths length_brauns)
+        IH take_nths_empty hd_take_nths length_brauns)
 qed
 
 corollary brauns1_correct:
   "braun (brauns1 xs) \<and> list (brauns1 xs) = xs"
-using brauns_correct[of 0 xs 0]
-by (simp add: brauns1_def braun_list_eq take_nths_00)
+  using brauns_correct[of 0 xs 0]
+  by (simp add: brauns1_def braun_list_eq take_nths_00)
 
 
 paragraph "Running Time Analysis"
@@ -510,7 +509,7 @@
     assume "xs \<noteq> []"
     let ?zs = "drop (2^k) xs"
     have "T_brauns k xs = T_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
-     using \<open>xs \<noteq> []\<close> by(simp)
+      using \<open>xs \<noteq> []\<close> by(simp)
     also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)"
       using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
       by (simp)
@@ -526,10 +525,10 @@
 text \<open>The code and the proof are originally due to Thomas Sewell (except running time).\<close>
 
 function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
-"list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts in
+  "list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts in
   if us = [] then [] else
   map value us @ list_fast_rec (map left us @ map right us))"
-by (pat_completeness, auto)
+  by (pat_completeness, auto)
 
 lemma list_fast_rec_term1: "ts \<noteq> [] \<Longrightarrow> Leaf \<notin> set ts \<Longrightarrow>
   sum_list (map (size o left) ts) + sum_list (map (size o right) ts) < sum_list (map size ts)"
@@ -545,27 +544,21 @@
   done
 
 termination
-  apply (relation "measure (sum_list o map size)")
-   apply simp
-  apply (simp add: list_fast_rec_term)
-  done
+  by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term)
 
 declare list_fast_rec.simps[simp del]
 
 definition list_fast :: "'a tree \<Rightarrow> 'a list" where
-"list_fast t = list_fast_rec [t]"
+  "list_fast t = list_fast_rec [t]"
 
 function T_list_fast_rec :: "'a tree list \<Rightarrow> nat" where
-"T_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts
+  "T_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts
   in length ts + (if us = [] then 0 else
   5 * length us + T_list_fast_rec (map left us @ map right us)))"
-by (pat_completeness, auto)
+  by (pat_completeness, auto)
 
 termination
-  apply (relation "measure (sum_list o map size)")
-   apply simp
-  apply (simp add: list_fast_rec_term)
-  done
+  by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term)
 
 declare T_list_fast_rec.simps[simp del]
 
@@ -573,22 +566,22 @@
 
 lemma list_fast_rec_all_Leaf:
   "\<forall>t \<in> set ts. t = Leaf \<Longrightarrow> list_fast_rec ts = []"
-by (simp add: filter_empty_conv list_fast_rec.simps)
+  by (simp add: filter_empty_conv list_fast_rec.simps)
 
 lemma take_nths_eq_single:
   "length xs - i < 2^n \<Longrightarrow> take_nths i n xs = take 1 (drop i xs)"
-by (induction xs arbitrary: i n; simp add: drop_Cons')
+  by (induction xs arbitrary: i n; simp add: drop_Cons')
 
 lemma braun_list_Nil:
   "braun_list t [] = (t = Leaf)"
-by (cases t; simp)
+  by (cases t; simp)
 
 lemma braun_list_not_Nil: "xs \<noteq> [] \<Longrightarrow>
   braun_list t xs =
- (\<exists>l x r. t = Node l x r \<and> x = hd xs \<and>
-    braun_list l (take_nths 1 1 xs) \<and>
-    braun_list r (take_nths 2 1 xs))"
-by(cases t; simp)
+     (\<exists>l x r. t = Node l x r \<and> x = hd xs \<and>
+        braun_list l (take_nths 1 1 xs) \<and>
+        braun_list r (take_nths 2 1 xs))"
+  by(cases t; simp)
 
 theorem list_fast_rec_correct:
   "\<lbrakk> length ts = 2 ^ k; \<forall>i < 2 ^ k. braun_list (ts ! i) (take_nths i k xs) \<rbrakk>
@@ -615,13 +608,13 @@
          \<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
                  \<longrightarrow> braun_list (right (ts ! i)) ys)"
       by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
-                     algebra_simps)
+          algebra_simps)
     have 1: "map value ts = take (2 ^ k) xs"
       using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
     have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
       using less.prems(1) False
       by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"]
-               simp: nth_append * take_nths_drop algebra_simps)
+          simp: nth_append * take_nths_drop algebra_simps)
     from less.prems(1) False show ?thesis
       by (auto simp: list_fast_rec.simps[of ts] 1 2 * all_set_conv_all_nth)
   qed
@@ -629,13 +622,13 @@
 
 corollary list_fast_correct:
   "braun t \<Longrightarrow> list_fast t = list t"
-by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])
+  by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])
 
 paragraph "Running Time Analysis"
 
 lemma sum_tree_list_children: "\<forall>t \<in> set ts. t \<noteq> Leaf \<Longrightarrow>
   (\<Sum>t\<leftarrow>ts. k * size t) = (\<Sum>t \<leftarrow> map left ts @ map right ts. k * size t) + k * length ts"
-by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)
+  by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)
 
 theorem T_list_fast_rec_ub:
   "T_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)"
@@ -647,11 +640,11 @@
     assume "?us = []"
     thus ?thesis using T_list_fast_rec.simps[of ts]
       by(simp add: sum_list_Suc)
-    next
+  next
     assume "?us \<noteq> []"
     let ?children = "map left ?us @ map right ?us"
     have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts"
-     using \<open>?us \<noteq> []\<close> T_list_fast_rec.simps[of ts] by(simp)
+      using \<open>?us \<noteq> []\<close> T_list_fast_rec.simps[of ts] by(simp)
     also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts"
       using less[of "?children"] list_fast_rec_term[of "?us"] \<open>?us \<noteq> []\<close>
       by (simp)
diff -r d96dd69903fb -r 7ed1759fe1bd src/HOL/Data_Structures/Brother12_Set.thy
--- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Aug 25 09:56:45 2023 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sat Aug 26 11:36:25 2023 +0100
@@ -3,10 +3,10 @@
 section \<open>1-2 Brother Tree Implementation of Sets\<close>
 
 theory Brother12_Set
-imports
-  Cmp
-  Set_Specs
-  "HOL-Number_Theory.Fib"
+  imports
+    Cmp
+    Set_Specs
+    "HOL-Number_Theory.Fib"
 begin
 
 subsection \<open>Data Type and Operations\<close>
@@ -20,28 +20,28 @@
   N3 "'a bro" 'a "'a bro" 'a "'a bro"
 
 definition empty :: "'a bro" where
-"empty = N0"
+  "empty = N0"
 
 fun inorder :: "'a bro \<Rightarrow> 'a list" where
-"inorder N0 = []" |
-"inorder (N1 t) = inorder t" |
-"inorder (N2 l a r) = inorder l @ a # inorder r" |
-"inorder (L2 a) = [a]" |
-"inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
+  "inorder N0 = []" |
+  "inorder (N1 t) = inorder t" |
+  "inorder (N2 l a r) = inorder l @ a # inorder r" |
+  "inorder (L2 a) = [a]" |
+  "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
 
 fun isin :: "'a bro \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
-"isin N0 x = False" |
-"isin (N1 t) x = isin t x" |
-"isin (N2 l a r) x =
+  "isin N0 x = False" |
+  "isin (N1 t) x = isin t x" |
+  "isin (N2 l a r) x =
   (case cmp x a of
      LT \<Rightarrow> isin l x |
      EQ \<Rightarrow> True |
      GT \<Rightarrow> isin r x)"
 
 fun n1 :: "'a bro \<Rightarrow> 'a bro" where
-"n1 (L2 a) = N2 N0 a N0" |
-"n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
-"n1 t = N1 t"
+  "n1 (L2 a) = N2 N0 a N0" |
+  "n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
+  "n1 t = N1 t"
 
 hide_const (open) insert
 
@@ -49,30 +49,30 @@
 begin
 
 fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
-"n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
-"n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
-"n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
-"n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
-"n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
-"n2 t1 a t2 = N2 t1 a t2"
+  "n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
+  "n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
+  "n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
+  "n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
+  "n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
+  "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
+  "n2 t1 a t2 = N2 t1 a t2"
 
 fun ins :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"ins x N0 = L2 x" |
-"ins x (N1 t) = n1 (ins x t)" |
-"ins x (N2 l a r) =
+  "ins x N0 = L2 x" |
+  "ins x (N1 t) = n1 (ins x t)" |
+  "ins x (N2 l a r) =
   (case cmp x a of
      LT \<Rightarrow> n2 (ins x l) a r |
      EQ \<Rightarrow> N2 l a r |
      GT \<Rightarrow> n2 l a (ins x r))"
 
 fun tree :: "'a bro \<Rightarrow> 'a bro" where
-"tree (L2 a) = N2 N0 a N0" |
-"tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
-"tree t = t"
+  "tree (L2 a) = N2 N0 a N0" |
+  "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
+  "tree t = t"
 
 definition insert :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"insert x t = tree(ins x t)"
+  "insert x t = tree(ins x t)"
 
 end
 
@@ -80,36 +80,36 @@
 begin
 
 fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
-"n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
+  "n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
+  "n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
+  "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
+  "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
   N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" |
-"n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
+  "n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
+  "n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
-"n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
+  "n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
   N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
-"n2 t1 a1 t2 = N2 t1 a1 t2"
+  "n2 t1 a1 t2 = N2 t1 a1 t2"
 
 fun split_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
-"split_min N0 = None" |
-"split_min (N1 t) =
+  "split_min N0 = None" |
+  "split_min (N1 t) =
   (case split_min t of
      None \<Rightarrow> None |
      Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
-"split_min (N2 t1 a t2) =
+  "split_min (N2 t1 a t2) =
   (case split_min t1 of
      None \<Rightarrow> Some (a, N1 t2) |
      Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
 
 fun del :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"del _ N0         = N0" |
-"del x (N1 t)     = N1 (del x t)" |
-"del x (N2 l a r) =
+  "del _ N0         = N0" |
+  "del x (N1 t)     = N1 (del x t)" |
+  "del x (N2 l a r) =
   (case cmp x a of
      LT \<Rightarrow> n2 (del x l) a r |
      GT \<Rightarrow> n2 l a (del x r) |
@@ -118,35 +118,35 @@
               Some (b, r') \<Rightarrow> n2 l b r'))"
 
 fun tree :: "'a bro \<Rightarrow> 'a bro" where
-"tree (N1 t) = t" |
-"tree t = t"
+  "tree (N1 t) = t" |
+  "tree t = t"
 
 definition delete :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"delete a t = tree (del a t)"
+  "delete a t = tree (del a t)"
 
 end
 
 subsection \<open>Invariants\<close>
 
 fun B :: "nat \<Rightarrow> 'a bro set"
-and U :: "nat \<Rightarrow> 'a bro set" where
-"B 0 = {N0}" |
-"B (Suc h) = { N2 t1 a t2 | t1 a t2. 
+  and U :: "nat \<Rightarrow> 'a bro set" where
+  "B 0 = {N0}" |
+  "B (Suc h) = { N2 t1 a t2 | t1 a t2. 
   t1 \<in> B h \<union> U h \<and> t2 \<in> B h \<or> t1 \<in> B h \<and> t2 \<in> B h \<union> U h}" |
-"U 0 = {}" |
-"U (Suc h) = N1 ` B h"
+  "U 0 = {}" |
+  "U (Suc h) = N1 ` B h"
 
 abbreviation "T h \<equiv> B h \<union> U h"
 
 fun Bp :: "nat \<Rightarrow> 'a bro set" where
-"Bp 0 = B 0 \<union> L2 ` UNIV" |
-"Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" |
-"Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union>
+  "Bp 0 = B 0 \<union> L2 ` UNIV" |
+  "Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" |
+  "Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union>
   {N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \<in> B (Suc h) \<and> t2 \<in> U (Suc h) \<and> t3 \<in> B (Suc h)}"
 
 fun Um :: "nat \<Rightarrow> 'a bro set" where
-"Um 0 = {}" |
-"Um (Suc h) = N1 ` T h"
+  "Um 0 = {}" |
+  "Um (Suc h) = N1 ` T h"
 
 
 subsection "Functional Correctness Proofs"
@@ -155,29 +155,29 @@
 
 lemma isin_set:
   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
-by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+
+  by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+
 
 subsubsection "Proofs for insertion"
 
 lemma inorder_n1: "inorder(n1 t) = inorder t"
-by(cases t rule: n1.cases) (auto simp: sorted_lems)
+  by(cases t rule: n1.cases) (auto simp: sorted_lems)
 
 context insert
 begin
 
 lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
+  by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
 
 lemma inorder_tree: "inorder(tree t) = inorder t"
-by(cases t) auto
+  by(cases t) auto
 
 lemma inorder_ins: "t \<in> T h \<Longrightarrow>
   sorted(inorder t) \<Longrightarrow> inorder(ins a t) = ins_list a (inorder t)"
-by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
+  by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
 
 lemma inorder_insert: "t \<in> T h \<Longrightarrow>
   sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
-by(simp add: insert_def inorder_ins inorder_tree)
+  by(simp add: insert_def inorder_ins inorder_tree)
 
 end
 
@@ -187,27 +187,27 @@
 begin
 
 lemma inorder_tree: "inorder(tree t) = inorder t"
-by(cases t) auto
+  by(cases t) auto
 
 lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: n2.cases) (auto)
+  by(cases "(l,a,r)" rule: n2.cases) (auto)
 
 lemma inorder_split_min:
   "t \<in> T h \<Longrightarrow> (split_min t = None \<longleftrightarrow> inorder t = []) \<and>
   (split_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
-by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
+  by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
 
 lemma inorder_del:
   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
   apply (induction h arbitrary: t) 
   apply (auto simp: del_list_simps inorder_n2 split: option.splits)
   apply (auto simp: del_list_simps inorder_n2
-     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
+      inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
   done
 
 lemma inorder_delete:
   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(simp add: delete_def inorder_del inorder_tree)
+  by(simp add: delete_def inorder_del inorder_tree)
 
 end
 
@@ -217,38 +217,41 @@
 subsubsection \<open>Proofs for insertion\<close>
 
 lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)"
-by(cases h rule: Bp.cases) auto
+  by(cases h rule: Bp.cases) auto
 
 context insert
 begin
 
 lemma tree_type: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)"
-by(cases h rule: Bp.cases) auto
+  by(cases h rule: Bp.cases) auto
 
 lemma n2_type:
   "(t1 \<in> Bp h \<and> t2 \<in> T h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h)) \<and>
    (t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))"
-apply(cases h rule: Bp.cases)
-apply (auto)[2]
-apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
-done
+  apply(cases h rule: Bp.cases)
+    apply (auto)[2]
+  apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
+  done
 
 lemma Bp_if_B: "t \<in> B h \<Longrightarrow> t \<in> Bp h"
-by (cases h rule: Bp.cases) simp_all
+  by (cases h rule: Bp.cases) simp_all
 
 text\<open>An automatic proof:\<close>
 
 lemma
   "(t \<in> B h \<longrightarrow> ins x t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> ins x t \<in> T h)"
-apply(induction h arbitrary: t)
- apply (simp)
-apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
-done
+proof (induction h arbitrary: t)
+  case 0
+  then show ?case by simp
+next
+  case (Suc h)
+  then show ?case by (fastforce simp: Bp_if_B n2_type dest: n1_type)
+qed
 
 text\<open>A detailed proof:\<close>
 
 lemma ins_type:
-shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h"
+  shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h"
 proof(induction h arbitrary: t)
   case 0
   { case 1 thus ?case by simp
@@ -300,7 +303,7 @@
 
 lemma insert_type:
   "t \<in> B h \<Longrightarrow> insert x t \<in> B h \<union> B (Suc h)"
-unfolding insert_def by (metis ins_type(1) tree_type)
+  unfolding insert_def by (metis ins_type(1) tree_type)
 
 end
 
@@ -311,37 +314,38 @@
   "L2 y \<in> B h = False"
   "(N3 t1 a1 t2 a2 t3) \<in> B h = False"
   "N0 \<in> B h \<longleftrightarrow> h = 0"
-by (cases h, auto)+
+  by (cases h, auto)+
 
 context delete
 begin
 
 lemma n2_type1:
   "\<lbrakk>t1 \<in> Um h; t2 \<in> B h\<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
-apply(cases h rule: Bp.cases)
-apply auto[2]
-apply(erule exE bexE conjE imageE | simp | erule disjE)+
-done
+  apply(cases h rule: Bp.cases)
+    apply auto[2]
+  apply(erule exE bexE conjE imageE | simp | erule disjE)+
+  done
 
 lemma n2_type2:
   "\<lbrakk>t1 \<in> B h ; t2 \<in> Um h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
-apply(cases h rule: Bp.cases)
-apply auto[2]
-apply(erule exE bexE conjE imageE | simp | erule disjE)+
-done
+  apply(cases h rule: Bp.cases)
+  using Um.simps(1) apply blast
+   apply force
+  apply(erule exE bexE conjE imageE | simp | erule disjE)+
+  done
 
 lemma n2_type3:
   "\<lbrakk>t1 \<in> T h ; t2 \<in> T h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
-apply(cases h rule: Bp.cases)
-apply auto[2]
-apply(erule exE bexE conjE imageE | simp | erule disjE)+
-done
+  apply(cases h rule: Bp.cases)
+    apply auto[2]
+  apply(erule exE bexE conjE imageE | simp | erule disjE)+
+  done
 
 lemma split_minNoneN0: "\<lbrakk>t \<in> B h; split_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
-by (cases t) (auto split: option.splits)
+  by (cases t) (auto split: option.splits)
 
 lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
-by (cases h) (auto simp: split_minNoneN0  split: option.splits)
+  by (cases h) (auto simp: split_minNoneN0  split: option.splits)
 
 lemma split_min_type:
   "t \<in> B h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
@@ -459,11 +463,11 @@
 qed auto
 
 lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t \<in> B (h+1) \<union> B h"
-by(auto)
+  by(auto)
 
 lemma delete_type: "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
-unfolding delete_def
-by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
+  unfolding delete_def
+  by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
 
 end
 
@@ -471,8 +475,8 @@
 subsection "Overall correctness"
 
 interpretation Set_by_Ordered
-where empty = empty and isin = isin and insert = insert.insert
-and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
+  where empty = empty and isin = isin and insert = insert.insert
+    and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
 proof (standard, goal_cases)
   case 2 thus ?case by(auto intro!: isin_set)
 next
@@ -506,27 +510,27 @@
 | "size (N2 t1 _ t2) = 1 + size t1 + size t2"
 
 lemma fib_tree_B: "fib_tree h \<in> B h"
-by (induction h rule: fib_tree.induct) auto
+  by (induction h rule: fib_tree.induct) auto
 
 declare [[names_short]]
 
 lemma size_fib': "size (fib_tree h) = fib' h"
-by (induction h rule: fib_tree.induct) auto
+  by (induction h rule: fib_tree.induct) auto
 
 lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))"
-by (induction h rule: fib_tree.induct) auto
+  by (induction h rule: fib_tree.induct) auto
 
 lemma B_N2_cases[consumes 1]:
-assumes "N2 t1 a t2 \<in> B (Suc n)"
-obtains 
-  (BB) "t1 \<in> B n" and "t2 \<in> B n" |
-  (UB) "t1 \<in> U n" and "t2 \<in> B n" |
-  (BU) "t1 \<in> B n" and "t2 \<in> U n"
-using assms by auto
+  assumes "N2 t1 a t2 \<in> B (Suc n)"
+  obtains 
+    (BB) "t1 \<in> B n" and "t2 \<in> B n" |
+    (UB) "t1 \<in> U n" and "t2 \<in> B n" |
+    (BU) "t1 \<in> B n" and "t2 \<in> U n"
+  using assms by auto
 
 lemma size_bounded: "t \<in> B h \<Longrightarrow> size t \<ge> size (fib_tree h)"
-unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
-case (3 h t')
+  unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
+  case (3 h t')
   note main = 3
   then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto
   with main have "N2 t1 a t2 \<in> B (Suc (Suc h))" by auto
@@ -546,7 +550,7 @@
 qed auto
 
 theorem "t \<in> B h \<Longrightarrow> fib (h + 2) \<le> size t + 1"
-using size_bounded
-by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
+  using size_bounded
+  by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
 
 end
diff -r d96dd69903fb -r 7ed1759fe1bd src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Fri Aug 25 09:56:45 2023 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Sat Aug 26 11:36:25 2023 +0100
@@ -3,9 +3,9 @@
 section "Sorting"
 
 theory Sorting
-imports
-  Complex_Main
-  "HOL-Library.Multiset"
+  imports
+    Complex_Main
+    "HOL-Library.Multiset"
 begin
 
 hide_const List.insort
@@ -16,40 +16,31 @@
 subsection "Insertion Sort"
 
 fun insort1 :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort1 x [] = [x]" |
-"insort1 x (y#ys) =
+  "insort1 x [] = [x]" |
+  "insort1 x (y#ys) =
   (if x \<le> y then x#y#ys else y#(insort1 x ys))"
 
 fun insort :: "'a::linorder list \<Rightarrow> 'a list" where
-"insort [] = []" |
-"insort (x#xs) = insort1 x (insort xs)"
+  "insort [] = []" |
+  "insort (x#xs) = insort1 x (insort xs)"
 
 
 subsubsection "Functional Correctness"
 
 lemma mset_insort1: "mset (insort1 x xs) = {#x#} + mset xs"
-apply(induction xs)
-apply auto
-done
+  by (induction xs) auto
 
 lemma mset_insort: "mset (insort xs) = mset xs"
-apply(induction xs)
-apply simp
-apply (simp add: mset_insort1)
-done
+  by (induction xs) (auto simp: mset_insort1)
 
 lemma set_insort1: "set (insort1 x xs) = {x} \<union> set xs"
-by(simp add: mset_insort1 flip: set_mset_mset)
+  by(simp add: mset_insort1 flip: set_mset_mset)
 
 lemma sorted_insort1: "sorted (insort1 a xs) = sorted xs"
-apply(induction xs)
-apply(auto simp add: set_insort1)
-done
+  by (induction xs) (auto simp: set_insort1)
 
 lemma sorted_insort: "sorted (insort xs)"
-apply(induction xs)
-apply(auto simp: sorted_insort1)
-done
+  by (induction xs) (auto simp: sorted_insort1)
 
 
 subsubsection "Time Complexity"
@@ -62,8 +53,8 @@
   (if x \<le> y then x#y#ys else y#(insort1 x ys))\<close>
 \<close>
 fun T_insort1 :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where
-"T_insort1 x [] = 1" |
-"T_insort1 x (y#ys) =
+  "T_insort1 x [] = 1" |
+  "T_insort1 x (y#ys) =
   (if x \<le> y then 0 else T_insort1 x ys) + 1"
 
 text\<open>
@@ -71,24 +62,18 @@
 \<open>insort (x#xs) = insort1 x (insort xs)\<close>
 \<close>
 fun T_insort :: "'a::linorder list \<Rightarrow> nat" where
-"T_insort [] = 1" |
-"T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1"
+  "T_insort [] = 1" |
+  "T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1"
 
 
 lemma T_insort1_length: "T_insort1 x xs \<le> length xs + 1"
-apply(induction xs)
-apply auto
-done
+  by (induction xs) auto
 
 lemma length_insort1: "length (insort1 x xs) = length xs + 1"
-apply(induction xs)
-apply auto
-done
+  by (induction xs) auto
 
 lemma length_insort: "length (insort xs) = length xs"
-apply(induction xs)
-apply (auto simp: length_insort1)
-done
+  by (metis Sorting.mset_insort size_mset)
 
 lemma T_insort_length: "T_insort xs \<le> (length xs + 1) ^ 2"
 proof(induction xs)
@@ -109,12 +94,12 @@
 subsection "Merge Sort"
 
 fun merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"merge [] ys = ys" |
-"merge xs [] = xs" |
-"merge (x#xs) (y#ys) = (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
+  "merge [] ys = ys" |
+  "merge xs [] = xs" |
+  "merge (x#xs) (y#ys) = (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
 
 fun msort :: "'a::linorder list \<Rightarrow> 'a list" where
-"msort xs = (let n = length xs in
+  "msort xs = (let n = length xs in
   if n \<le> 1 then xs
   else merge (msort (take (n div 2) xs)) (msort (drop (n div 2) xs)))"
 
@@ -124,7 +109,7 @@
 subsubsection "Functional Correctness"
 
 lemma mset_merge: "mset(merge xs ys) = mset xs + mset ys"
-by(induction xs ys rule: merge.induct) auto
+  by(induction xs ys rule: merge.induct) auto
 
 lemma mset_msort: "mset (msort xs) = mset xs"
 proof(induction xs rule: msort.induct)
@@ -151,13 +136,13 @@
 text \<open>Via the previous lemma or directly:\<close>
 
 lemma set_merge: "set(merge xs ys) = set xs \<union> set ys"
-by (metis mset_merge set_mset_mset set_mset_union)
+  by (metis mset_merge set_mset_mset set_mset_union)
 
 lemma "set(merge xs ys) = set xs \<union> set ys"
-by(induction xs ys rule: merge.induct) (auto)
+  by(induction xs ys rule: merge.induct) (auto)
 
 lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)"
-by(induction xs ys rule: merge.induct) (auto simp: set_merge)
+  by(induction xs ys rule: merge.induct) (auto simp: set_merge)
 
 lemma sorted_msort: "sorted (msort xs)"
 proof(induction xs rule: msort.induct)
@@ -180,15 +165,15 @@
 text \<open>We only count the number of comparisons between list elements.\<close>
 
 fun C_merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> nat" where
-"C_merge [] ys = 0" |
-"C_merge xs [] = 0" |
-"C_merge (x#xs) (y#ys) = 1 + (if x \<le> y then C_merge xs (y#ys) else C_merge (x#xs) ys)"
+  "C_merge [] ys = 0" |
+  "C_merge xs [] = 0" |
+  "C_merge (x#xs) (y#ys) = 1 + (if x \<le> y then C_merge xs (y#ys) else C_merge (x#xs) ys)"
 
 lemma C_merge_ub: "C_merge xs ys \<le> length xs + length ys"
-by (induction xs ys rule: C_merge.induct) auto
+  by (induction xs ys rule: C_merge.induct) auto
 
 fun C_msort :: "'a::linorder list \<Rightarrow> nat" where
-"C_msort xs =
+  "C_msort xs =
   (let n = length xs;
        ys = take (n div 2) xs;
        zs = drop (n div 2) xs
@@ -198,9 +183,7 @@
 declare C_msort.simps [simp del]
 
 lemma length_merge: "length(merge xs ys) = length xs + length ys"
-apply (induction xs ys rule: merge.induct)
-apply auto
-done
+  by (induction xs ys rule: merge.induct) auto
 
 lemma length_msort: "length(msort xs) = length xs"
 proof (induction xs rule: msort.induct)
@@ -245,78 +228,77 @@
 
 (* Beware of implicit conversions: *)
 lemma C_msort_log: "length xs = 2^k \<Longrightarrow> C_msort xs \<le> length xs * log 2 (length xs)"
-using C_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
-by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
+  using C_msort_le[of xs k]
+  by (metis log2_of_power_eq mult.commute of_nat_mono of_nat_mult) 
 
 
 subsection "Bottom-Up Merge Sort"
 
 fun merge_adj :: "('a::linorder) list list \<Rightarrow> 'a list list" where
-"merge_adj [] = []" |
-"merge_adj [xs] = [xs]" |
-"merge_adj (xs # ys # zss) = merge xs ys # merge_adj zss"
+  "merge_adj [] = []" |
+  "merge_adj [xs] = [xs]" |
+  "merge_adj (xs # ys # zss) = merge xs ys # merge_adj zss"
 
 text \<open>For the termination proof of \<open>merge_all\<close> below.\<close>
 lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2"
-by (induction xs rule: merge_adj.induct) auto
+  by (induction xs rule: merge_adj.induct) auto
 
 fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where
-"merge_all [] = []" |
-"merge_all [xs] = xs" |
-"merge_all xss = merge_all (merge_adj xss)"
+  "merge_all [] = []" |
+  "merge_all [xs] = xs" |
+  "merge_all xss = merge_all (merge_adj xss)"
 
 definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where
-"msort_bu xs = merge_all (map (\<lambda>x. [x]) xs)"
+  "msort_bu xs = merge_all (map (\<lambda>x. [x]) xs)"
 
 
 subsubsection "Functional Correctness"
 
 abbreviation mset_mset :: "'a list list \<Rightarrow> 'a multiset" where
-"mset_mset xss \<equiv> \<Sum>\<^sub># (image_mset mset (mset xss))"
+  "mset_mset xss \<equiv> \<Sum>\<^sub># (image_mset mset (mset xss))"
 
 lemma mset_merge_adj:
   "mset_mset (merge_adj xss) = mset_mset xss"
-by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
+  by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
 
 lemma mset_merge_all:
   "mset (merge_all xss) = mset_mset xss"
-by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
+  by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
 
 lemma mset_msort_bu: "mset (msort_bu xs) = mset xs"
-by(simp add: msort_bu_def mset_merge_all multiset.map_comp comp_def)
+  by(simp add: msort_bu_def mset_merge_all multiset.map_comp comp_def)
 
 lemma sorted_merge_adj:
   "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs"
-by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge)
+  by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge)
 
 lemma sorted_merge_all:
   "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> sorted (merge_all xss)"
-apply(induction xss rule: merge_all.induct)
-using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj)
+  by (induction xss rule: merge_all.induct) (auto simp add: sorted_merge_adj)
 
 lemma sorted_msort_bu: "sorted (msort_bu xs)"
-by(simp add: msort_bu_def sorted_merge_all)
+  by(simp add: msort_bu_def sorted_merge_all)
 
 
 subsubsection "Time Complexity"
 
 fun C_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where
-"C_merge_adj [] = 0" |
-"C_merge_adj [xs] = 0" |
-"C_merge_adj (xs # ys # zss) = C_merge xs ys + C_merge_adj zss"
+  "C_merge_adj [] = 0" |
+  "C_merge_adj [xs] = 0" |
+  "C_merge_adj (xs # ys # zss) = C_merge xs ys + C_merge_adj zss"
 
 fun C_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where
-"C_merge_all [] = 0" |
-"C_merge_all [xs] = 0" |
-"C_merge_all xss = C_merge_adj xss + C_merge_all (merge_adj xss)"
+  "C_merge_all [] = 0" |
+  "C_merge_all [xs] = 0" |
+  "C_merge_all xss = C_merge_adj xss + C_merge_all (merge_adj xss)"
 
 definition C_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where
-"C_msort_bu xs = C_merge_all (map (\<lambda>x. [x]) xs)"
+  "C_msort_bu xs = C_merge_all (map (\<lambda>x. [x]) xs)"
 
 lemma length_merge_adj:
   "\<lbrakk> even(length xss); \<forall>xs \<in> set xss. length xs = m \<rbrakk>
   \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m"
-by(induction xss rule: merge_adj.induct) (auto simp: length_merge)
+  by(induction xss rule: merge_adj.induct) (auto simp: length_merge)
 
 lemma C_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> C_merge_adj xss \<le> m * length xss"
 proof(induction xss rule: C_merge_adj.induct)
@@ -354,27 +336,24 @@
 qed
 
 corollary C_msort_bu: "length xs = 2 ^ k \<Longrightarrow> C_msort_bu xs \<le> k * 2 ^ k"
-using C_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: C_msort_bu_def)
+  using C_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: C_msort_bu_def)
 
 
 subsection "Quicksort"
 
 fun quicksort :: "('a::linorder) list \<Rightarrow> 'a list" where
-"quicksort []     = []" |
-"quicksort (x#xs) = quicksort (filter (\<lambda>y. y < x) xs) @ [x] @ quicksort (filter (\<lambda>y. x \<le> y) xs)"
+  "quicksort []     = []" |
+  "quicksort (x#xs) = quicksort (filter (\<lambda>y. y < x) xs) @ [x] @ quicksort (filter (\<lambda>y. x \<le> y) xs)"
 
 lemma mset_quicksort: "mset (quicksort xs) = mset xs"
-apply (induction xs rule: quicksort.induct)
-apply (auto simp: not_le)
-done
+  by (induction xs rule: quicksort.induct) (auto simp: not_le)
 
 lemma set_quicksort: "set (quicksort xs) = set xs"
-by(rule mset_eq_setD[OF mset_quicksort])
+  by(rule mset_eq_setD[OF mset_quicksort])
 
 lemma sorted_quicksort: "sorted (quicksort xs)"
-apply (induction xs rule: quicksort.induct)
-apply (auto simp add: sorted_append set_quicksort)
-done
+proof (induction xs rule: quicksort.induct)
+qed (auto simp: sorted_append set_quicksort)
 
 
 subsection "Insertion Sort w.r.t. Keys and Stability"
@@ -382,45 +361,45 @@
 hide_const List.insort_key
 
 fun insort1_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort1_key f x [] = [x]" |
-"insort1_key f x (y # ys) = (if f x \<le> f y then x # y # ys else y # insort1_key f x ys)"
+  "insort1_key f x [] = [x]" |
+  "insort1_key f x (y # ys) = (if f x \<le> f y then x # y # ys else y # insort1_key f x ys)"
 
 fun insort_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort_key f [] = []" |
-"insort_key f (x # xs) = insort1_key f x (insort_key f xs)"
+  "insort_key f [] = []" |
+  "insort_key f (x # xs) = insort1_key f x (insort_key f xs)"
 
 
 subsubsection "Standard functional correctness"
 
 lemma mset_insort1_key: "mset (insort1_key f x xs) = {#x#} + mset xs"
-by(induction xs) simp_all
+  by(induction xs) simp_all
 
 lemma mset_insort_key: "mset (insort_key f xs) = mset xs"
-by(induction xs) (simp_all add: mset_insort1_key)
+  by(induction xs) (simp_all add: mset_insort1_key)
 
 (* Inductive proof simpler than derivation from mset lemma: *)
 lemma set_insort1_key: "set (insort1_key f x xs) = {x} \<union> set xs"
-by (induction xs) auto
+  by (induction xs) auto
 
 lemma sorted_insort1_key: "sorted (map f (insort1_key f a xs)) = sorted (map f xs)"
-by(induction xs)(auto simp: set_insort1_key)
+  by(induction xs)(auto simp: set_insort1_key)
 
 lemma sorted_insort_key: "sorted (map f (insort_key f xs))"
-by(induction xs)(simp_all add: sorted_insort1_key)
+  by(induction xs)(simp_all add: sorted_insort1_key)
 
 
 subsubsection "Stability"
 
 lemma insort1_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort1_key f a xs = a # xs"
-by (cases xs) auto
+  by (cases xs) auto
 
 lemma filter_insort1_key_neg:
   "\<not> P x \<Longrightarrow> filter P (insort1_key f x xs) = filter P xs"
-by (induction xs) simp_all
+  by (induction xs) simp_all
 
 lemma filter_insort1_key_pos:
   "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort1_key f x xs) = insort1_key f x (filter P xs)"
-by (induction xs) (auto, subst insort1_is_Cons, auto)
+  by (induction xs) (auto, subst insort1_is_Cons, auto)
 
 lemma sort_key_stable: "filter (\<lambda>y. f y = k) (insort_key f xs) = filter (\<lambda>y. f y = k) xs"
 proof (induction xs)
diff -r d96dd69903fb -r 7ed1759fe1bd src/HOL/Data_Structures/Tries_Binary.thy
--- a/src/HOL/Data_Structures/Tries_Binary.thy	Fri Aug 25 09:56:45 2023 +0100
+++ b/src/HOL/Data_Structures/Tries_Binary.thy	Sat Aug 26 11:36:25 2023 +0100
@@ -3,7 +3,7 @@
 section "Binary Tries and Patricia Tries"
 
 theory Tries_Binary
-imports Set_Specs
+  imports Set_Specs
 begin
 
 hide_const (open) insert
@@ -11,10 +11,10 @@
 declare Let_def[simp]
 
 fun sel2 :: "bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a" where
-"sel2 b (a1,a2) = (if b then a2 else a1)"
+  "sel2 b (a1,a2) = (if b then a2 else a1)"
 
 fun mod2 :: "('a \<Rightarrow> 'a) \<Rightarrow> bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a * 'a" where
-"mod2 f b (a1,a2) = (if b then (a1,f a2) else (f a1,a2))"
+  "mod2 f b (a1,a2) = (if b then (a1,f a2) else (f a1,a2))"
 
 
 subsection "Trie"
@@ -22,82 +22,78 @@
 datatype trie = Lf | Nd bool "trie * trie"
 
 definition empty :: trie where
-[simp]: "empty = Lf"
+  [simp]: "empty = Lf"
 
 fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
-"isin Lf ks = False" |
-"isin (Nd b lr) ks =
+  "isin Lf ks = False" |
+  "isin (Nd b lr) ks =
    (case ks of
       [] \<Rightarrow> b |
       k#ks \<Rightarrow> isin (sel2 k lr) ks)"
 
 fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
-"insert [] Lf = Nd True (Lf,Lf)" |
-"insert [] (Nd b lr) = Nd True lr" |
-"insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
-"insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
+  "insert [] Lf = Nd True (Lf,Lf)" |
+  "insert [] (Nd b lr) = Nd True lr" |
+  "insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
+  "insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
 
 lemma isin_insert: "isin (insert xs t) ys = (xs = ys \<or> isin t ys)"
-apply(induction xs t arbitrary: ys rule: insert.induct)
-apply (auto split: list.splits if_splits)
-done
+proof (induction xs t arbitrary: ys rule: insert.induct)
+qed (auto split: list.splits if_splits)
 
 text \<open>A simple implementation of delete; does not shrink the trie!\<close>
 
 fun delete0 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
-"delete0 ks Lf = Lf" |
-"delete0 ks (Nd b lr) =
+  "delete0 ks Lf = Lf" |
+  "delete0 ks (Nd b lr) =
    (case ks of
       [] \<Rightarrow> Nd False lr |
       k#ks' \<Rightarrow> Nd b (mod2 (delete0 ks') k lr))"
 
 lemma isin_delete0: "isin (delete0 as t) bs = (as \<noteq> bs \<and> isin t bs)"
-apply(induction as t arbitrary: bs rule: delete0.induct)
-apply (auto split: list.splits if_splits)
-done
+proof (induction as t arbitrary: bs rule: delete0.induct)
+qed (auto split: list.splits if_splits)
 
 text \<open>Now deletion with shrinking:\<close>
 
 fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
-"node b lr = (if \<not> b \<and> lr = (Lf,Lf) then Lf else Nd b lr)"
+  "node b lr = (if \<not> b \<and> lr = (Lf,Lf) then Lf else Nd b lr)"
 
 fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
-"delete ks Lf = Lf" |
-"delete ks (Nd b lr) =
+  "delete ks Lf = Lf" |
+  "delete ks (Nd b lr) =
    (case ks of
       [] \<Rightarrow> node False lr |
       k#ks' \<Rightarrow> node b (mod2 (delete ks') k lr))"
 
 lemma isin_delete: "isin (delete xs t) ys = (xs \<noteq> ys \<and> isin t ys)"
-apply(induction xs t arbitrary: ys rule: delete.induct)
- apply simp
-apply (auto split: list.splits if_splits)
-  apply (metis isin.simps(1))
- apply (metis isin.simps(1))
+  apply(induction xs t arbitrary: ys rule: delete.induct)
+   apply (auto split: list.splits if_splits)
+   apply (metis isin.simps(1))+
   done
 
 definition set_trie :: "trie \<Rightarrow> bool list set" where
-"set_trie t = {xs. isin t xs}"
+  "set_trie t = {xs. isin t xs}"
 
 lemma set_trie_empty: "set_trie empty = {}"
-by(simp add: set_trie_def)
+  by(simp add: set_trie_def)
 
 lemma set_trie_isin: "isin t xs = (xs \<in> set_trie t)"
-by(simp add: set_trie_def)
+  by(simp add: set_trie_def)
 
 lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \<union> {xs}"
-by(auto simp add: isin_insert set_trie_def)
+  by(auto simp add: isin_insert set_trie_def)
 
 lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
-by(auto simp add: isin_delete set_trie_def)
+  by(auto simp add: isin_delete set_trie_def)
 
 text \<open>Invariant: tries are fully shrunk:\<close>
 fun invar where
-"invar Lf = True" |
-"invar (Nd b (l,r)) = (invar l \<and> invar r \<and> (l = Lf \<and> r = Lf \<longrightarrow> b))"
+  "invar Lf = True" |
+  "invar (Nd b (l,r)) = (invar l \<and> invar r \<and> (l = Lf \<and> r = Lf \<longrightarrow> b))"
 
 lemma insert_Lf: "insert xs t \<noteq> Lf"
-using insert.elims by blast
+  using insert.elims by blast
 
 lemma invar_insert: "invar t \<Longrightarrow> invar(insert xs t)"
 proof(induction xs t rule: insert.induct)
@@ -122,23 +118,10 @@
 qed
 
 interpretation S: Set
-where empty = empty and isin = isin and insert = insert and delete = delete
-and set = set_trie and invar = invar
-proof (standard, goal_cases)
-  case 1 show ?case by (rule set_trie_empty)
-next
-  case 2 show ?case by(rule set_trie_isin)
-next
-  case 3 thus ?case by(auto simp: set_trie_insert)
-next
-  case 4 show ?case by(rule set_trie_delete)
-next
-  case 5 show ?case by(simp)
-next
-  case 6 thus ?case by(rule invar_insert)
-next
-  case 7 thus ?case by(rule invar_delete)
-qed
+  where empty = empty and isin = isin and insert = insert and delete = delete
+    and set = set_trie and invar = invar
+  unfolding Set_def
+  by (smt (verit, best) Tries_Binary.empty_def invar.simps(1) invar_delete invar_insert set_trie_delete set_trie_empty set_trie_insert set_trie_isin)
 
 
 subsection "Patricia Trie"
@@ -147,24 +130,24 @@
 
 text \<open>Fully shrunk:\<close>
 fun invarP where
-"invarP LfP = True" |
-"invarP (NdP ps b (l,r)) = (invarP l \<and> invarP r \<and> (l = LfP \<or> r = LfP \<longrightarrow> b))"
+  "invarP LfP = True" |
+  "invarP (NdP ps b (l,r)) = (invarP l \<and> invarP r \<and> (l = LfP \<or> r = LfP \<longrightarrow> b))"
 
 fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
-"isinP LfP ks = False" |
-"isinP (NdP ps b lr) ks =
+  "isinP LfP ks = False" |
+  "isinP (NdP ps b lr) ks =
   (let n = length ps in
    if ps = take n ks
    then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (sel2 k lr) ks'
    else False)"
 
 definition emptyP :: trieP where
-[simp]: "emptyP = LfP"
+  [simp]: "emptyP = LfP"
 
 fun lcp :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list" where
-"lcp [] ys = ([],[],ys)" |
-"lcp xs [] = ([],xs,[])" |
-"lcp (x#xs) (y#ys) =
+  "lcp [] ys = ([],[],ys)" |
+  "lcp xs [] = ([],xs,[])" |
+  "lcp (x#xs) (y#ys) =
   (if x\<noteq>y then ([],x#xs,y#ys)
    else let (ps,xs',ys') = lcp xs ys in (x#ps,xs',ys'))"
 
@@ -172,12 +155,12 @@
 lemma mod2_cong[fundef_cong]:
   "\<lbrakk> lr = lr'; k = k'; \<And>a b. lr'=(a,b) \<Longrightarrow> f (a) = f' (a) ; \<And>a b. lr'=(a,b) \<Longrightarrow> f (b) = f' (b) \<rbrakk>
   \<Longrightarrow> mod2 f k lr= mod2 f' k' lr'"
-by(cases lr, cases lr', auto)
+  by(cases lr, cases lr', auto)
 
 
 fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
-"insertP ks LfP  = NdP ks True (LfP,LfP)" |
-"insertP ks (NdP ps b lr) =
+  "insertP ks LfP  = NdP ks True (LfP,LfP)" |
+  "insertP ks (NdP ps b lr) =
   (case lcp ks ps of
      (qs, k#ks', p#ps') \<Rightarrow>
        let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
@@ -192,7 +175,7 @@
 
 text \<open>Smart constructor that shrinks:\<close>
 definition nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> trieP * trieP \<Rightarrow> trieP" where
-"nodeP ps b lr =
+  "nodeP ps b lr =
  (if b then  NdP ps b lr
   else case lr of
    (LfP,LfP) \<Rightarrow> LfP |
@@ -201,8 +184,8 @@
    _ \<Rightarrow> NdP ps b lr)"
 
 fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
-"deleteP ks LfP  = LfP" |
-"deleteP ks (NdP ps b lr) =
+  "deleteP ks LfP  = LfP" |
+  "deleteP ks (NdP ps b lr) =
   (case lcp ks ps of
      (_, _, _#_) \<Rightarrow> NdP ps b lr |
      (_, k#ks', []) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
@@ -215,13 +198,13 @@
 text \<open>First step: @{typ trieP} implements @{typ trie} via the abstraction function \<open>abs_trieP\<close>:\<close>
 
 fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
-"prefix_trie [] t = t" |
-"prefix_trie (k#ks) t =
+  "prefix_trie [] t = t" |
+  "prefix_trie (k#ks) t =
   (let t' = prefix_trie ks t in Nd False (if k then (Lf,t') else (t',Lf)))"
 
 fun abs_trieP :: "trieP \<Rightarrow> trie" where
-"abs_trieP LfP = Lf" |
-"abs_trieP (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_trieP l, abs_trieP r))"
+  "abs_trieP LfP = Lf" |
+  "abs_trieP (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_trieP l, abs_trieP r))"
 
 
 text \<open>Correctness of @{const isinP}:\<close>
@@ -229,96 +212,82 @@
 lemma isin_prefix_trie:
   "isin (prefix_trie ps t) ks
    = (ps = take (length ps) ks \<and> isin t (drop (length ps) ks))"
-apply(induction ps arbitrary: ks)
-apply(auto split: list.split)
-done
+  by (induction ps arbitrary: ks) (auto split: list.split)
 
 lemma abs_trieP_isinP:
   "isinP t ks = isin (abs_trieP t) ks"
-apply(induction t arbitrary: ks rule: abs_trieP.induct)
- apply(auto simp: isin_prefix_trie split: list.split)
-done
+proof (induction t arbitrary: ks rule: abs_trieP.induct)
+qed (auto simp: isin_prefix_trie split: list.split)
 
 
 text \<open>Correctness of @{const insertP}:\<close>
 
 lemma prefix_trie_Lfs: "prefix_trie ks (Nd True (Lf,Lf)) = insert ks Lf"
-apply(induction ks)
-apply auto
-done
+  by (induction ks) auto
 
 lemma insert_prefix_trie_same:
   "insert ps (prefix_trie ps (Nd b lr)) = prefix_trie ps (Nd True lr)"
-apply(induction ps)
-apply auto
-done
+  by (induction ps) auto
 
 lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
-apply(induction ks)
-apply auto
-done
+  by (induction ks) auto
 
 lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
-apply(induction ps)
-apply auto
-done
+  by (induction ps) auto
 
 lemma lcp_if: "lcp ks ps = (qs, ks', ps') \<Longrightarrow>
   ks = qs @ ks' \<and> ps = qs @ ps' \<and> (ks' \<noteq> [] \<and> ps' \<noteq> [] \<longrightarrow> hd ks' \<noteq> hd ps')"
-apply(induction ks ps arbitrary: qs ks' ps' rule: lcp.induct)
-apply(auto split: prod.splits if_splits)
-done
+proof (induction ks ps arbitrary: qs ks' ps' rule: lcp.induct)
+qed (auto split: prod.splits if_splits)
 
 lemma abs_trieP_insertP:
   "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
-apply(induction t arbitrary: ks)
-apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
-           dest!: lcp_if split: list.split prod.split if_splits)
-done
+proof (induction t arbitrary: ks)
+qed (auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
+    dest!: lcp_if split: list.split prod.split if_splits)
 
 
 text \<open>Correctness of @{const deleteP}:\<close>
 
 lemma prefix_trie_Lf: "prefix_trie xs t = Lf \<longleftrightarrow> xs = [] \<and> t = Lf"
-by(cases xs)(auto)
+  by(cases xs)(auto)
 
 lemma abs_trieP_Lf: "abs_trieP t = Lf \<longleftrightarrow> t = LfP"
-by(cases t) (auto simp: prefix_trie_Lf)
+  by(cases t) (auto simp: prefix_trie_Lf)
 
 lemma delete_prefix_trie:
   "delete xs (prefix_trie xs (Nd b (l,r)))
    = (if (l,r) = (Lf,Lf) then Lf else prefix_trie xs (Nd False (l,r)))"
-by(induction xs)(auto simp: prefix_trie_Lf)
+  by(induction xs)(auto simp: prefix_trie_Lf)
 
 lemma delete_append_prefix_trie:
   "delete (xs @ ys) (prefix_trie xs t)
    = (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
-by(induction xs)(auto simp: prefix_trie_Lf)
+  by(induction xs)(auto simp: prefix_trie_Lf)
 
 lemma nodeP_LfP2: "nodeP xs False (LfP, LfP) = LfP"
-by(simp add: nodeP_def)
+  by(simp add: nodeP_def)
 
 text \<open>Some non-inductive aux. lemmas:\<close>
 
 lemma abs_trieP_nodeP: "a\<noteq>LfP \<or> b \<noteq> LfP \<Longrightarrow>
   abs_trieP (nodeP xs f (a, b)) = prefix_trie xs (Nd f (abs_trieP a, abs_trieP b))"
-by(auto simp add: nodeP_def prefix_trie_append split: trieP.split)
+  by(auto simp add: nodeP_def prefix_trie_append split: trieP.split)
 
 lemma nodeP_True: "nodeP ps True lr = NdP ps True lr"
-by(simp add: nodeP_def)
+  by(simp add: nodeP_def)
 
 lemma delete_abs_trieP:
   "delete ks (abs_trieP t) = abs_trieP (deleteP ks t)"
-apply(induction t arbitrary: ks)
-apply(auto simp: delete_prefix_trie delete_append_prefix_trie
-        prefix_trie_append prefix_trie_Lf abs_trieP_Lf nodeP_LfP2 abs_trieP_nodeP nodeP_True
-        dest!: lcp_if split: if_splits list.split prod.split)
-done
+proof (induction t arbitrary: ks)
+qed (auto simp: delete_prefix_trie delete_append_prefix_trie
+    prefix_trie_append prefix_trie_Lf abs_trieP_Lf nodeP_LfP2 abs_trieP_nodeP nodeP_True
+    dest!: lcp_if split: if_splits list.split prod.split)
 
 text \<open>Invariant preservation:\<close>
 
 lemma insertP_LfP: "insertP xs t \<noteq> LfP"
-by(cases t)(auto split: prod.split list.split)
+  by(cases t)(auto split: prod.split list.split)
 
 lemma invarP_insertP: "invarP t \<Longrightarrow> invarP(insertP xs t)"
 proof(induction t arbitrary: xs)
@@ -331,7 +300,7 @@
 
 (* Inlining this proof leads to nontermination *)
 lemma invarP_nodeP: "\<lbrakk> invarP t1; invarP t2\<rbrakk> \<Longrightarrow> invarP (nodeP xs b (t1, t2))"
-by (auto simp add: nodeP_def split: trieP.split)
+  by (auto simp add: nodeP_def split: trieP.split)
 
 lemma invarP_deleteP: "invarP t \<Longrightarrow> invarP(deleteP xs t)"
 proof(induction t arbitrary: xs)
@@ -345,20 +314,20 @@
 text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>
 
 definition set_trieP :: "trieP \<Rightarrow> bool list set" where
-"set_trieP = set_trie o abs_trieP"
+  "set_trieP = set_trie o abs_trieP"
 
 lemma isinP_set_trieP: "isinP t xs = (xs \<in> set_trieP t)"
-by(simp add: abs_trieP_isinP set_trie_isin set_trieP_def)
+  by(simp add: abs_trieP_isinP set_trie_isin set_trieP_def)
 
 lemma set_trieP_insertP: "set_trieP (insertP xs t) = set_trieP t \<union> {xs}"
-by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)
+  by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)
 
 lemma set_trieP_deleteP: "set_trieP (deleteP xs t) = set_trieP t - {xs}"
-by(auto simp: set_trie_delete set_trieP_def simp flip: delete_abs_trieP)
+  by(auto simp: set_trie_delete set_trieP_def simp flip: delete_abs_trieP)
 
 interpretation SP: Set
-where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
-and set = set_trieP and invar = invarP
+  where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
+    and set = set_trieP and invar = invarP
 proof (standard, goal_cases)
   case 1 show ?case by (simp add: set_trieP_def set_trie_def)
 next