--- a/src/HOL/Data_Structures/Set2_Join.thy Tue Sep 24 17:36:14 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Wed Sep 25 17:22:57 2019 +0200
@@ -20,26 +20,26 @@
and recursion operators on it.\<close>
locale Set2_Join =
-fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
-fixes inv :: "('a,'b) tree \<Rightarrow> bool"
+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: "bst (Node l a b r) \<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 b 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]
subsection "\<open>split_min\<close>"
-fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
-"split_min (Node l a _ r) =
+fun split_min :: "('a*'b) tree \<Rightarrow> 'a \<times> ('a*'b) tree" where
+"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 = (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')
+proof(induction t arbitrary: t' rule: tree2_induct)
case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
next
case Leaf thus ?case by simp
@@ -47,7 +47,7 @@
lemma split_min_bst:
"\<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')
+proof(induction t arbitrary: t' rule: tree2_induct)
case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
next
case Leaf thus ?case by simp
@@ -55,7 +55,7 @@
lemma split_min_inv:
"\<lbrakk> split_min t = (m,t'); inv t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> inv t'"
-proof(induction t arbitrary: t')
+proof(induction t arbitrary: t' rule: tree2_induct)
case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
next
case Leaf thus ?case by simp
@@ -64,7 +64,7 @@
subsection "\<open>join2\<close>"
-definition join2 :: "('a,'b) tree \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
+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"
@@ -80,9 +80,9 @@
subsection "\<open>split\<close>"
-fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
+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) x =
+"split (Node l (a, _) r) x =
(case cmp x a of
LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) |
GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) |
@@ -91,14 +91,14 @@
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)
+proof(induction t arbitrary: l xin r rule: tree2_induct)
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 x = (l,xin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
-proof(induction t arbitrary: l xin r)
+proof(induction t arbitrary: l xin r rule: tree2_induct)
case Leaf thus ?case by simp
next
case Node
@@ -110,7 +110,7 @@
subsection "\<open>insert\<close>"
-definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
+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) = {x} \<union> set_tree t"
@@ -125,7 +125,7 @@
subsection "\<open>delete\<close>"
-definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
+definition delete :: "'a \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
"delete x t = (let (l,_,r) = split t x in join2 l r)"
lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete x t) = set_tree t - {x}"
@@ -140,11 +140,11 @@
subsection "\<open>union\<close>"
-fun union :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
+fun union :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where
"union t1 t2 =
(if t1 = Leaf then t2 else
if t2 = Leaf then t1 else
- case t1 of Node l1 a _ r1 \<Rightarrow>
+ 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' a r')"
@@ -176,11 +176,11 @@
subsection "\<open>inter\<close>"
-fun inter :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
+fun inter :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where
"inter t1 t2 =
(if t1 = Leaf then Leaf else
if t2 = Leaf then Leaf else
- case t1 of Node l1 a _ r1 \<Rightarrow>
+ 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 ain then join l' a r' else join2 l' r')"
@@ -192,7 +192,7 @@
proof(induction t1 t2 rule: inter.induct)
case (1 t1 t2)
show ?case
- proof (cases t1)
+ proof (cases t1 rule: tree2_cases)
case Leaf thus ?thesis by (simp add: inter.simps)
next
case [simp]: (Node l1 a _ r1)
@@ -209,9 +209,9 @@
**: "?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
+ 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
+ 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> {a}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
by(simp add: t2)
also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
@@ -241,11 +241,11 @@
subsection "\<open>diff\<close>"
-fun diff :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
+fun diff :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where
"diff t1 t2 =
(if t1 = Leaf then Leaf else
if t2 = Leaf then t1 else
- case t2 of Node l2 a _ r2 \<Rightarrow>
+ 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')"
@@ -257,7 +257,7 @@
proof(induction t1 t2 rule: diff.induct)
case (1 t1 t2)
show ?case
- proof (cases t2)
+ proof (cases t2 rule: tree2_cases)
case Leaf thus ?thesis by (simp add: diff.simps)
next
case [simp]: (Node l2 a _ r2)
@@ -273,9 +273,9 @@
**: "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
+ 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
+ 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> {a})"
by(simp add: t1)
also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
@@ -340,7 +340,7 @@
end
interpretation unbal: Set2_Join
-where join = "\<lambda>l x r. Node l x () r" and inv = "\<lambda>t. True"
+where join = "\<lambda>l x r. Node l (x, ()) r" and inv = "\<lambda>t. True"
proof (standard, goal_cases)
case 1 show ?case by simp
next