--- a/src/HOL/Data_Structures/Set2_Join.thy Mon Aug 19 21:37:34 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Tue Aug 20 09:48:22 2019 +0200
@@ -23,12 +23,10 @@
fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
fixes inv :: "('a,'b) tree \<Rightarrow> bool"
assumes set_join: "set_tree (join l a r) = set_tree l \<union> {a} \<union> set_tree r"
-assumes bst_join:
- "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. x < a; \<forall>y \<in> set_tree r. a < y \<rbrakk>
- \<Longrightarrow> bst (join l a r)"
+assumes bst_join: "bst (Node l a b r) \<Longrightarrow> bst (join l a r)"
assumes inv_Leaf: "inv \<langle>\<rangle>"
assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l a r)"
-assumes inv_Node: "\<lbrakk> inv (Node l a h r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
+assumes inv_Node: "\<lbrakk> inv (Node l a b r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
begin
declare set_join [simp]
@@ -40,7 +38,7 @@
(if l = Leaf then (a,r) else let (m,l') = split_min l in (m, join l' a r))"
lemma split_min_set:
- "\<lbrakk> split_min t = (m,t'); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> m \<in> set_tree t \<and> set_tree t = Set.insert m (set_tree t')"
+ "\<lbrakk> split_min t = (m,t'); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> m \<in> set_tree t \<and> set_tree t = {m} \<union> set_tree t'"
proof(induction t arbitrary: t')
case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
next
@@ -115,7 +113,7 @@
definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
"insert x t = (let (l,_,r) = split t x in join l x r)"
-lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
+lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = {x} \<union> set_tree t"
by(auto simp add: insert_def split split: prod.split)
lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy Mon Aug 19 21:37:34 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy Tue Aug 20 09:48:22 2019 +0200
@@ -168,32 +168,32 @@
by(simp add: set_joinL set_joinR set_paint)
lemma bst_baliL:
- "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
- \<Longrightarrow> bst (baliL l k r)"
-by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un)
+ "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>x\<in>set_tree r. a < x\<rbrakk>
+ \<Longrightarrow> bst (baliL l a r)"
+by(cases "(l,a,r)" rule: baliL.cases) (auto simp: ball_Un)
lemma bst_baliR:
- "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
- \<Longrightarrow> bst (baliR l k r)"
-by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un)
+ "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>x\<in>set_tree r. a < x\<rbrakk>
+ \<Longrightarrow> bst (baliR l a r)"
+by(cases "(l,a,r)" rule: baliR.cases) (auto simp: ball_Un)
lemma bst_joinL:
- "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y; bheight l \<le> bheight r\<rbrakk>
- \<Longrightarrow> bst (joinL l k r)"
-proof(induction l k r rule: joinL.induct)
- case (1 l x r)
+ "\<lbrakk>bst (Node l a n r); bheight l \<le> bheight r\<rbrakk>
+ \<Longrightarrow> bst (joinL l a r)"
+proof(induction l a r rule: joinL.induct)
+ case (1 l a r)
thus ?case
- by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL
+ by(auto simp: set_baliL joinL.simps[of l a r] set_joinL ball_Un intro!: bst_baliL
split!: tree.splits color.splits)
qed
lemma bst_joinR:
- "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
- \<Longrightarrow> bst (joinR l k r)"
-proof(induction l k r rule: joinR.induct)
- case (1 l x r)
+ "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>y\<in>set_tree r. a < y \<rbrakk>
+ \<Longrightarrow> bst (joinR l a r)"
+proof(induction l a r rule: joinR.induct)
+ case (1 l a r)
thus ?case
- by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR
+ by(auto simp: set_baliR joinR.simps[of l a r] set_joinR ball_Un intro!: bst_baliR
split!: tree.splits color.splits)
qed
@@ -201,10 +201,11 @@
by(cases t) auto
lemma bst_join:
- "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
- \<Longrightarrow> bst (join l k r)"
+ "bst (Node l a n r) \<Longrightarrow> bst (join l a r)"
by(auto simp: bst_paint bst_joinL bst_joinR)
+lemma inv_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> invc(join l x r) \<and> invh(join l x r)"
+by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
subsubsection "Interpretation of \<^locale>\<open>Set2_Join\<close> with Red-Black Tree"
@@ -215,12 +216,11 @@
proof (standard, goal_cases)
case 1 show ?case by (rule set_join)
next
- case 2 thus ?case by (rule bst_join)
+ case 2 thus ?case by (simp add: bst_join del: join.simps)
next
case 3 show ?case by simp
next
- case 4 thus ?case
- by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
+ case 4 thus ?case by (simp add: inv_join del: join.simps)
next
case 5 thus ?case by simp
qed