# HG changeset patch
# User nipkow
# Date 1588771884 -7200
# Node ID dd5b8072ca90ddb2670d27a1fb229f28c2a21768
# Parent  eeff463c49e8850c18ef6d2bdce81b76f5ae549a
simplified and tuned

diff -r eeff463c49e8 -r dd5b8072ca90 src/HOL/Data_Structures/AVL_Bal_Set.thy
--- 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) =