# HG changeset patch
# User nipkow
# Date 1588754779 -7200
# Node ID 986d5abbe77c188a4534c8f7c6b44d50916a9602
# Parent  e8e0313881b9a6db51fb17565a22f21457469623
tuned

diff -r e8e0313881b9 -r 986d5abbe77c src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Wed May 06 10:46:19 2020 +0200
@@ -1,6 +1,6 @@
 (* Tobias Nipkow *)
 
-section "AVL Tree with Balance Tags (Set Implementation)"
+section "AVL Tree with Balance Factors"
 
 theory AVL_Bal_Set
 imports
@@ -9,7 +9,6 @@
 begin
 
 datatype bal = Lh | Bal | Rh
-(* Exercise: use 3 Node constructors instead *)
 
 type_synonym 'a tree_bal = "('a * bal) tree"
 
@@ -27,9 +26,9 @@
 
 subsection \<open>Code\<close>
 
-datatype 'a change = Same 'a | Diff 'a
+datatype 'a tree_bal2 = Same "'a tree_bal" | Diff "'a tree_bal"
 
-fun tree :: "'a change \<Rightarrow> 'a" where
+fun tree :: "'a tree_bal2 \<Rightarrow> 'a tree_bal" where
 "tree(Same t) = t" |
 "tree(Diff t) = t"
 
@@ -39,7 +38,7 @@
 fun rot22 :: "bal \<Rightarrow> bal" where
 "rot22 b = (if b=Lh then Rh else Bal)"
 
-fun balL :: "'a tree_bal change \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+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
    Same AB \<Rightarrow> Same (Node AB (c,bc) C) |
    Diff AB \<Rightarrow> (case bc of
@@ -51,7 +50,7 @@
          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)))))"
 
-fun balR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal change \<Rightarrow> 'a tree_bal change" where
+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
    Same BC \<Rightarrow> Same (Node A (a,ba) BC) |
    Diff BC \<Rightarrow> (case ba of
@@ -63,14 +62,14 @@
          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)))))"
 
-fun insert :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
 "insert x Leaf = Diff(Node Leaf (x, Bal) Leaf)" |
 "insert x (Node l (a, b) r) = (case cmp x a of
    EQ \<Rightarrow> Same(Node l (a, b) r) |
    LT \<Rightarrow> balL (insert x l) a b r |
    GT \<Rightarrow> balR l a b (insert x r))"
 
-fun baldR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal change \<Rightarrow> 'a tree_bal change" where
+fun baldR :: "'a tree_bal \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal2 \<Rightarrow> 'a tree_bal2" where
 "baldR AB c bc C' = (case C' of
    Same C \<Rightarrow> Same (Node AB (c,bc) C) |
    Diff C \<Rightarrow> (case bc of
@@ -83,7 +82,7 @@
          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))))))"
 
-fun baldL :: "'a tree_bal change \<Rightarrow> 'a \<Rightarrow> bal \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+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
    Same A \<Rightarrow> Same (Node A (a,ba) BC) |
    Diff A \<Rightarrow> (case ba of
@@ -96,11 +95,11 @@
          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))))))"
 
-fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal change * 'a" where
+fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal2 * 'a" where
 "split_max (Node l (a, ba) r) =
   (if r = Leaf then (Diff l,a) else let (r',a') = split_max r in (baldR l a ba r', a'))"
 
-fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal change" where
+fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal2" where
 "delete _ Leaf = Same Leaf" |
 "delete x (Node l (a, ba) r) =
   (case cmp x a of
@@ -111,7 +110,7 @@
 
 lemmas split_max_induct = split_max.induct[case_names Node Leaf]
 
-lemmas splits =  if_splits tree.splits tree.splits change.splits bal.splits
+lemmas splits = if_splits tree.splits tree.splits tree_bal2.splits bal.splits
 
 subsection \<open>Proofs\<close>
 
diff -r e8e0313881b9 -r 986d5abbe77c src/HOL/Data_Structures/AVL_Map.thy
--- a/src/HOL/Data_Structures/AVL_Map.thy	Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Wed May 06 10:46:19 2020 +0200
@@ -8,14 +8,14 @@
   Lookup2
 begin
 
-fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree_ht \<Rightarrow> ('a*'b) tree_ht" where
 "update x y Leaf = Node Leaf ((x,y), 1) Leaf" |
 "update x y (Node l ((a,b), h) r) = (case cmp x a of
    EQ \<Rightarrow> Node l ((x,y), h) r |
    LT \<Rightarrow> balL (update x y l) (a,b) r |
    GT \<Rightarrow> balR l (a,b) (update x y r))"
 
-fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree_ht \<Rightarrow> ('a*'b) tree_ht" where
 "delete _ Leaf = Leaf" |
 "delete x (Node l ((a,b), h) r) = (case cmp x a of
    EQ \<Rightarrow> if l = Leaf then r
diff -r e8e0313881b9 -r 986d5abbe77c src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Wed May 06 10:46:19 2020 +0200
@@ -8,7 +8,7 @@
   "HOL-Number_Theory.Fib"
 begin
 
-fun avl :: "'a avl_tree \<Rightarrow> bool" where
+fun avl :: "'a tree_ht \<Rightarrow> bool" where
 "avl Leaf = True" |
 "avl (Node l (a,n) r) =
  (abs(int(height l) - int(height r)) \<le> 1 \<and>
@@ -26,16 +26,12 @@
 lemma height_balL:
   "\<lbrakk> avl l; avl r; height l = height r + 2 \<rbrakk> \<Longrightarrow>
    height (balL l a r) \<in> {height r + 2, height r + 3}"
-apply (cases l)
- apply (auto simp:node_def balL_def split:tree.split)
- by arith+
+by (auto simp:node_def balL_def split:tree.split)
 
 lemma height_balR:
   "\<lbrakk> avl l; avl r; height r = height l + 2 \<rbrakk> \<Longrightarrow>
    height (balR l a r) : {height l + 2, height l + 3}"
-apply (cases r)
- apply(auto simp add:node_def balR_def split:tree.split)
- by arith+
+by(auto simp add:node_def balR_def split:tree.split)
 
 lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1"
 by (simp add: node_def)
diff -r e8e0313881b9 -r 986d5abbe77c src/HOL/Data_Structures/AVL_Set_Code.thy
--- a/src/HOL/Data_Structures/AVL_Set_Code.thy	Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set_Code.thy	Wed May 06 10:46:19 2020 +0200
@@ -13,19 +13,19 @@
 
 subsection \<open>Code\<close>
 
-type_synonym 'a avl_tree = "('a*nat) tree"
+type_synonym 'a tree_ht = "('a*nat) tree"
 
-definition empty :: "'a avl_tree" where
+definition empty :: "'a tree_ht" where
 "empty = Leaf"
 
-fun ht :: "'a avl_tree \<Rightarrow> nat" where
+fun ht :: "'a tree_ht \<Rightarrow> nat" where
 "ht Leaf = 0" |
 "ht (Node l (a,n) r) = n"
 
-definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+definition node :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "node l a r = Node l (a, max (ht l) (ht r) + 1) r"
 
-definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+definition balL :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "balL AB c C =
   (if ht AB = ht C + 2 then
      case AB of 
@@ -36,7 +36,7 @@
              Node B\<^sub>1 (b, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) b (node B\<^sub>2 c C)
    else node AB c C)"
 
-definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+definition balR :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "balR A a BC =
    (if ht BC = ht A + 2 then
       case BC of
@@ -47,20 +47,20 @@
               Node B\<^sub>1 (b, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) b (node B\<^sub>2 c C)
   else node A a BC)"
 
-fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "insert x Leaf = Node Leaf (x, 1) Leaf" |
 "insert x (Node l (a, n) r) = (case cmp x a of
    EQ \<Rightarrow> Node l (a, n) r |
    LT \<Rightarrow> balL (insert x l) a r |
    GT \<Rightarrow> balR l a (insert x r))"
 
-fun split_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
+fun split_max :: "'a tree_ht \<Rightarrow> 'a tree_ht * 'a" where
 "split_max (Node l (a, _) r) =
   (if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))"
 
 lemmas split_max_induct = split_max.induct[case_names Node Leaf]
 
-fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun delete :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "delete _ Leaf = Leaf" |
 "delete x (Node l (a, n) r) =
   (case cmp x a of
diff -r e8e0313881b9 -r 986d5abbe77c src/HOL/Data_Structures/Height_Balanced_Tree.thy
--- a/src/HOL/Data_Structures/Height_Balanced_Tree.thy	Tue May 05 20:32:57 2020 +0200
+++ b/src/HOL/Data_Structures/Height_Balanced_Tree.thy	Wed May 06 10:46:19 2020 +0200
@@ -12,9 +12,9 @@
 The code and the proofs were obtained by small modifications of the AVL theories.
 This is an implementation of sets via HBTs.\<close>
 
-type_synonym 'a hbt = "('a*nat) tree"
+type_synonym 'a tree_ht = "('a*nat) tree"
 
-definition empty :: "'a hbt" where
+definition empty :: "'a tree_ht" where
 "empty = Leaf"
 
 text \<open>The maximal amount by which the height of two siblings may differ:\<close>
@@ -26,20 +26,20 @@
 
 text \<open>Invariant:\<close>
 
-fun hbt :: "'a hbt \<Rightarrow> bool" where
+fun hbt :: "'a tree_ht \<Rightarrow> bool" where
 "hbt Leaf = True" |
 "hbt (Node l (a,n) r) =
  (abs(int(height l) - int(height r)) \<le> int(m) \<and>
   n = max (height l) (height r) + 1 \<and> hbt l \<and> hbt r)"
 
-fun ht :: "'a hbt \<Rightarrow> nat" where
+fun ht :: "'a tree_ht \<Rightarrow> nat" where
 "ht Leaf = 0" |
 "ht (Node l (a,n) r) = n"
 
-definition node :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+definition node :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "node l a r = Node l (a, max (ht l) (ht r) + 1) r"
 
-definition balL :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+definition balL :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "balL AB b C =
   (if ht AB = ht C + m + 1 then
      case AB of 
@@ -50,7 +50,7 @@
              Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C)
    else node AB b C)"
 
-definition balR :: "'a hbt \<Rightarrow> 'a \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+definition balR :: "'a tree_ht \<Rightarrow> 'a \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "balR A a BC =
    (if ht BC = ht A + m + 1 then
       case BC of
@@ -61,20 +61,20 @@
               Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C)
   else node A a BC)"
 
-fun insert :: "'a::linorder \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "insert x Leaf = Node Leaf (x, 1) Leaf" |
 "insert x (Node l (a, n) r) = (case cmp x a of
    EQ \<Rightarrow> Node l (a, n) r |
    LT \<Rightarrow> balL (insert x l) a r |
    GT \<Rightarrow> balR l a (insert x r))"
 
-fun split_max :: "'a hbt \<Rightarrow> 'a hbt * 'a" where
+fun split_max :: "'a tree_ht \<Rightarrow> 'a tree_ht * 'a" where
 "split_max (Node l (a, _) r) =
   (if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))"
 
 lemmas split_max_induct = split_max.induct[case_names Node Leaf]
 
-fun delete :: "'a::linorder \<Rightarrow> 'a hbt \<Rightarrow> 'a hbt" where
+fun delete :: "'a::linorder \<Rightarrow> 'a tree_ht \<Rightarrow> 'a tree_ht" where
 "delete _ Leaf = Leaf" |
 "delete x (Node l (a, n) r) =
   (case cmp x a of
@@ -132,16 +132,12 @@
 lemma height_balL:
   "\<lbrakk> hbt l; hbt r; height l = height r + m + 1 \<rbrakk> \<Longrightarrow>
    height (balL l a r) \<in> {height r + m + 1, height r + m + 2}"
-apply (cases l)
- apply (auto simp:node_def balL_def split:tree.split)
- by arith+
+by (auto simp:node_def balL_def split:tree.split)
 
 lemma height_balR:
   "\<lbrakk> hbt l; hbt r; height r = height l + m + 1 \<rbrakk> \<Longrightarrow>
    height (balR l a r) \<in> {height l + m + 1, height l + m + 2}"
-apply (cases r)
- apply(auto simp add:node_def balR_def split:tree.split)
- by arith+
+by(auto simp add:node_def balR_def split:tree.split)
 
 lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1"
 by (simp add: node_def)
@@ -149,22 +145,20 @@
 lemma height_balL2:
   "\<lbrakk> hbt l; hbt r; height l \<noteq> height r + m + 1 \<rbrakk> \<Longrightarrow>
    height (balL l a r) = 1 + max (height l) (height r)"
-by (cases l, cases r) (simp_all add: balL_def)
+by (simp_all add: balL_def)
 
 lemma height_balR2:
   "\<lbrakk> hbt l;  hbt r;  height r \<noteq> height l + m + 1 \<rbrakk> \<Longrightarrow>
    height (balR l a r) = 1 + max (height l) (height r)"
-by (cases l, cases r) (simp_all add: balR_def)
+by (simp_all add: balR_def)
 
 lemma hbt_balL: 
   "\<lbrakk> hbt l; hbt r; height r - m \<le> height l \<and> height l \<le> height r + m + 1 \<rbrakk> \<Longrightarrow> hbt(balL l a r)"
-by(cases l, cases r)
-  (auto simp: balL_def node_def max_def split!: if_splits tree.split)
+by(auto simp: balL_def node_def max_def split!: if_splits tree.split)
 
 lemma hbt_balR: 
   "\<lbrakk> hbt l; hbt r; height l - m \<le> height r \<and> height r \<le> height l + m + 1 \<rbrakk> \<Longrightarrow> hbt(balR l a r)"
-by(cases r, cases l)
-  (auto simp: balR_def node_def max_def split!: if_splits tree.split)
+by(auto simp: balR_def node_def max_def split!: if_splits tree.split)
 
 text\<open>Insertion maintains @{const hbt}. Requires simultaneous proof.\<close>