merged

--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy	Tue Nov 05 23:01:09 2024 +0100
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Tue Nov 05 23:27:47 2024 +0100
@@ -227,6 +227,7 @@
 where join = join and inv = "\<lambda>t. invc t \<and> invh t"
 defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split
 and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min
+and inter_rbt = RBT.inter and union_rbt = RBT.union and diff_rbt = RBT.diff 
 proof (standard, goal_cases)
   case 1 show ?case by (rule set_join)
 next

--- a/src/HOL/Library/While_Combinator.thy	Tue Nov 05 23:01:09 2024 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Tue Nov 05 23:27:47 2024 +0100
@@ -70,8 +70,8 @@
     by (simp add: while_option_def k_def split: if_splits)
   have 1: "\<forall>i<k. b ((c ^^ i) s)"
     by (auto simp: k_def dest: not_less_Least)
-  have "P ((c ^^ i) s)" if "i \<le> k" for i
-    using that by (induct i) (auto simp: init step 1)
+  have "i \<le> k \<Longrightarrow> P ((c ^^ i) s)" for i
+    by (induct i) (auto simp: init step 1)
   thus "P t" by (auto simp: t)
 qed
 
@@ -137,17 +137,17 @@
     have "\<not> b' ((c' ^^ Suc k') (f s))"
       unfolding Suc[symmetric] by (rule LeastI) (rule k)
     moreover
-    have b': "b' ((c' ^^ k) (f s))" if "k \<le> k'" for k
+    have b': "b' ((c' ^^ k) (f s))" if asm: "k \<le> k'" for k
     proof -
-      from that have "k < ?k'" unfolding Suc by simp
+      from asm have "k < ?k'" unfolding Suc by simp
       thus ?thesis by (rule iffD1[OF not_not, OF not_less_Least])
     qed
     have b: "b ((c ^^ k) s)"
       and body: "f ((c ^^ k) s) = (c' ^^ k) (f s)"
       and inv: "P ((c ^^ k) s)"
-      if "k \<le> k'" for k
+      if asm: "k \<le> k'" for k
     proof -
-      from that have "f ((c ^^ k) s) = (c' ^^ k) (f s)"
+      from asm have "f ((c ^^ k) s) = (c' ^^ k) (f s)"
         and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
         and "P ((c ^^ k) s)"
         by (induct k) (auto simp: b' assms)