# HG changeset patch
# User nipkow
# Date 1718722530 -7200
# Node ID 4953d52e04d282cf2efeca93107a729180c2a719
# Parent  7e0cbc6600b9df1b3e304a2aeb36c77604d7d059
tuned def: patter matching needs more beautification

diff -r 7e0cbc6600b9 -r 4953d52e04d2 src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Mon Jun 17 09:00:46 2024 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Tue Jun 18 16:55:30 2024 +0200
@@ -64,19 +64,18 @@
 
 subsection "\<open>join2\<close>"
 
-fun join2 :: "('a*'b) tree \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"join2 l \<langle>\<rangle> = l" |
-"join2 l r = (let (m,r') = split_min r in join l m r')"
+definition join2 :: "('a*'b) tree \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"join2 l r = (if r = Leaf then l else let (m,r') = split_min r in join l m r')"
 
 lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
-by(cases r)(simp_all add: split_min_set split: prod.split)
+by(cases r)(simp_all add: split_min_set join2_def split: prod.split)
 
 lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
   \<Longrightarrow> bst (join2 l r)"
-by(cases r)(simp_all add: bst_join split_min_set split_min_bst split: prod.split)
+by(cases r)(simp_all add: bst_join split_min_set split_min_bst join2_def split: prod.split)
 
 lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
-by(cases r)(simp_all add: inv_join split_min_set split_min_inv split: prod.split)
+by(cases r)(simp_all add: inv_join split_min_set split_min_inv join2_def split: prod.split)
 
 
 subsection "\<open>split\<close>"