--- 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)