author nipkow Wed, 06 May 2020 15:31:24 +0200 changeset 71820 dd5b8072ca90 parent 71819 eeff463c49e8 child 71821 541e68d1a964 child 71824 95d2d5e60419
simplified and tuned
```--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Wed May 06 13:52:01 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Wed May 06 15:31:24 2020 +0200
@@ -32,11 +32,12 @@
"tree(Same t) = t" |
"tree(Diff t) = t"

-fun rot21 :: "bal \<Rightarrow> bal" where
-"rot21 b = (if b=Rh then Lh else Bal)"
-
-fun rot22 :: "bal \<Rightarrow> bal" where
-"rot22 b = (if b=Lh then Rh else Bal)"
+fun rot2 where
+"rot2 A a B c C = (case B of
+  (Node B\<^sub>1 (b, bb) B\<^sub>2) \<Rightarrow>
+    let b\<^sub>1 = if bb = Rh then Lh else Bal;
+        b\<^sub>2 = if bb = Lh then Rh else Bal
+    in Node (Node A (a,b\<^sub>1) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,b\<^sub>2) C))"

fun balL :: "'a tree_bal2 \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
"balL AB' c bc C = (case AB' of
@@ -46,9 +47,7 @@
Rh \<Rightarrow> Same (Node AB (c,Bal) C) |
Lh \<Rightarrow> Same(case AB of
Node A (a,Lh) B \<Rightarrow> Node A (a,Bal) (Node B (c,Bal) C) |
-       Node A (a,Rh) B \<Rightarrow> (case B of
-         Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
-           Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C)))))"
+       Node A (a,Rh) B \<Rightarrow> rot2 A a B c C)))"

fun balR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal2 \<Rightarrow> 'a tree_bal2" where
"balR A a ba BC' = (case BC' of
@@ -58,9 +57,7 @@
Lh \<Rightarrow> Same (Node A (a,Bal) BC) |
Rh \<Rightarrow> Same(case BC of
Node B (c,Rh) C \<Rightarrow> Node (Node A (a,Bal) B) (c,Bal) C |
-       Node B (c,Lh) C \<Rightarrow> (case B of
-         Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
-           Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C)))))"
+       Node B (c,Lh) C \<Rightarrow> rot2 A a B c C)))"

fun insert :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
"insert x Leaf = Diff(Node Leaf (x, Bal) Leaf)" |
@@ -78,9 +75,7 @@
Lh \<Rightarrow> (case AB of
Node A (a,Lh) B \<Rightarrow> Diff(Node A (a,Bal) (Node B (c,Bal) C)) |
Node A (a,Bal) B \<Rightarrow> Same(Node A (a,Rh) (Node B (c,Lh) C)) |
-       Node A (a,Rh) B \<Rightarrow> (case B of
-         Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
-           Diff(Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C))))))"
+       Node A (a,Rh) B \<Rightarrow> Diff(rot2 A a B c C))))"

fun baldL :: "'a tree_bal2 \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
"baldL A' a ba BC = (case A' of
@@ -91,9 +86,7 @@
Rh \<Rightarrow> (case BC of
Node B (c,Rh) C \<Rightarrow> Diff(Node (Node A (a,Bal) B) (c,Bal) C) |
Node B (c,Bal) C \<Rightarrow> Same(Node (Node A (a,Rh) B) (c,Lh) C) |
-       Node B (c,Lh) C \<Rightarrow> (case B of
-         Node B\<^sub>1 (b, bb) B\<^sub>2 \<Rightarrow>
-           Diff(Node (Node A (a,rot21 bb) B\<^sub>1) (b,Bal) (Node B\<^sub>2 (c,rot22 bb) C))))))"
+       Node B (c,Lh) C \<Rightarrow> Diff(rot2 A a B c C))))"

fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal2 * 'a" where
"split_max (Node l (a, ba) r) =```