# HG changeset patch
# User nipkow
# Date 1536670605 -7200
# Node ID 7a9118e63cad2f5515d6478aa7da3c6c563150a0
# Parent  6c4421b006fb7cf01b389f8f547156dde0830f31
tuned

diff -r 6c4421b006fb -r 7a9118e63cad src/HOL/Data_Structures/Set2_Join.thy
--- 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