--- a/src/HOL/Data_Structures/Set2_Join.thy Mon Sep 10 21:33:14 2018 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Tue Sep 11 14:56:45 2018 +0200
@@ -27,8 +27,8 @@
"\<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 inv_Leaf: "inv \<langle>\<rangle>"
-assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
-assumes inv_Node: "\<lbrakk> inv (Node l x h r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
+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"
begin
declare set_join [simp]
@@ -36,11 +36,11 @@
subsection "\<open>split_min\<close>"
fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
-"split_min (Node l x _ r) =
- (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
+"split_min (Node l a _ r) =
+ (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 = (x,t'); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> x \<in> set_tree t \<and> set_tree t = Set.insert x (set_tree t')"
+ "\<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')"
proof(induction t arbitrary: t')
case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
next
@@ -48,7 +48,7 @@
qed
lemma split_min_bst:
- "\<lbrakk> split_min t = (x,t'); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
+ "\<lbrakk> split_min t = (m,t'); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> bst t' \<and> (\<forall>x \<in> set_tree t'. m < x)"
proof(induction t arbitrary: t')
case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
next
@@ -56,7 +56,7 @@
qed
lemma split_min_inv:
- "\<lbrakk> split_min t = (x,t'); inv t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> inv t'"
+ "\<lbrakk> split_min t = (m,t'); inv t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> inv t'"
proof(induction t arbitrary: t')
case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
next
@@ -67,7 +67,7 @@
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 (x,r') = split_min r in join l x r')"
+"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(simp add: join2_def split_min_set split: prod.split)
@@ -84,22 +84,22 @@
fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
"split Leaf k = (Leaf, False, Leaf)" |
-"split (Node l a _ r) k =
- (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else
- if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2)
+"split (Node l a _ r) x =
+ (if x < a then let (l1,b,l2) = split l x in (l1, b, join l2 a r) else
+ if a < x then let (r1,b,r2) = split r x in (join l a r1, b, r2)
else (l, True, r))"
-lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
- set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
- \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
-proof(induction t arbitrary: l kin r)
+lemma split: "split t x = (l,xin,r) \<Longrightarrow> bst t \<Longrightarrow>
+ set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a}
+ \<and> (xin = (x \<in> set_tree t)) \<and> bst l \<and> bst r"
+proof(induction t arbitrary: l xin r)
case Leaf thus ?case by simp
next
case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
qed
-lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
-proof(induction t arbitrary: l kin r)
+lemma split_inv: "split t x = (l,xin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
+proof(induction t arbitrary: l xin r)
case Leaf thus ?case by simp
next
case Node
@@ -112,7 +112,7 @@
subsection "\<open>insert\<close>"
definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
-"insert k t = (let (l,_,r) = split t k in join l k r)"
+"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)"
by(auto simp add: insert_def split split: prod.split)
@@ -127,9 +127,9 @@
subsection "\<open>delete\<close>"
definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
-"delete k t = (let (l,_,r) = split t k in join2 l r)"
+"delete x t = (let (l,_,r) = split t x in join2 l r)"
-lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
+lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete x t) = set_tree t - {x}"
by(auto simp: delete_def split split: prod.split)
lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
@@ -145,10 +145,10 @@
"union t1 t2 =
(if t1 = Leaf then t2 else
if t2 = Leaf then t1 else
- case t1 of Node l1 k _ r1 \<Rightarrow>
- let (l2,_ ,r2) = split t2 k;
+ case t1 of Node l1 a _ r1 \<Rightarrow>
+ let (l2,_ ,r2) = split t2 a;
l' = union l1 l2; r' = union r1 r2
- in join l' k r')"
+ in join l' a r')"
declare union.simps [simp del]
@@ -181,10 +181,10 @@
"inter t1 t2 =
(if t1 = Leaf then Leaf else
if t2 = Leaf then Leaf else
- case t1 of Node l1 k _ r1 \<Rightarrow>
- let (l2,kin,r2) = split t2 k;
+ case t1 of Node l1 a _ r1 \<Rightarrow>
+ let (l2,ain,r2) = split t2 a;
l' = inter l1 l2; r' = inter r1 r2
- in if kin then join l' k r' else join2 l' r')"
+ in if ain then join l' a r' else join2 l' r')"
declare inter.simps [simp del]
@@ -196,24 +196,24 @@
proof (cases t1)
case Leaf thus ?thesis by (simp add: inter.simps)
next
- case [simp]: (Node l1 k _ r1)
+ case [simp]: (Node l1 a _ r1)
show ?thesis
proof (cases "t2 = Leaf")
case True thus ?thesis by (simp add: inter.simps)
next
case False
let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
- have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
- obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
- let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
+ have *: "a \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
+ obtain l2 ain r2 where sp: "split t2 a = (l2,ain,r2)" using prod_cases3 by blast
+ let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if ain then {a} else {}"
have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
- **: "?L2 \<inter> ?R2 = {}" "k \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
+ **: "?L2 \<inter> ?R2 = {}" "a \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force)
have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2"
using "1.IH"(1)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2"
using "1.IH"(2)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
- have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
+ have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {a}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
by(simp add: t2)
also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
using * ** by auto
@@ -246,8 +246,8 @@
"diff t1 t2 =
(if t1 = Leaf then Leaf else
if t2 = Leaf then t1 else
- case t2 of Node l2 k _ r2 \<Rightarrow>
- let (l1,_,r1) = split t1 k;
+ case t2 of Node l2 a _ r2 \<Rightarrow>
+ let (l1,_,r1) = split t1 a;
l' = diff l1 l2; r' = diff r1 r2
in join2 l' r')"
@@ -261,23 +261,23 @@
proof (cases t2)
case Leaf thus ?thesis by (simp add: diff.simps)
next
- case [simp]: (Node l2 k _ r2)
+ case [simp]: (Node l2 a _ r2)
show ?thesis
proof (cases "t1 = Leaf")
case True thus ?thesis by (simp add: diff.simps)
next
case False
let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
- obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
- let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
+ obtain l1 ain r1 where sp: "split t1 a = (l1,ain,r1)" using prod_cases3 by blast
+ let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if ain then {a} else {}"
have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
- **: "k \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
+ **: "a \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force)
have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2"
using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
- have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2 \<union> {k})"
+ have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2 \<union> {a})"
by(simp add: t1)
also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
using ** by auto