# HG changeset patch
# User nipkow
# Date 1659077151 -7200
# Node ID 1635ee32e6d823d7cee176e5fc2e0d2d953b62d7
# Parent  40af1efeadeeca49c2f0cf8da95eaaeedade0152
prettified def

diff -r 40af1efeadee -r 1635ee32e6d8 src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Thu Jul 28 19:14:49 2022 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Fri Jul 29 08:45:51 2022 +0200
@@ -64,18 +64,19 @@
 
 subsection "\<open>join2\<close>"
 
-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')"
+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')"
 
 lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
-by(simp add: join2_def split_min_set split: prod.split)
+by(cases r)(simp_all add: split_min_set 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(simp add: join2_def 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 split: prod.split)
 
 lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
-by(simp add: join2_def 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 split: prod.split)
 
 
 subsection "\<open>split\<close>"