# HG changeset patch
# User nipkow
# Date 1587675263 -7200
# Node ID 8ad9b2d3dd81fad3f0166e961c5d7cdb102aa221
# Parent  3b6547bdf6e29e8f8006773dad2761bca38d3cf9
split AVL_Set.thy

diff -r 3b6547bdf6e2 -r 8ad9b2d3dd81 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Apr 23 09:57:41 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Apr 23 22:54:23 2020 +0200
@@ -3,119 +3,20 @@
 Based on the AFP entry AVL.
 *)
 
-section "AVL Tree Implementation of Sets"
+subsection \<open>Invariant\<close>
 
 theory AVL_Set
 imports
-  Cmp
-  Isin2
+  AVL_Set_Code
   "HOL-Number_Theory.Fib"
 begin
 
-type_synonym 'a avl_tree = "('a*nat) tree"
-
-definition empty :: "'a avl_tree" where
-"empty = Leaf"
-
-text \<open>Invariant:\<close>
-
 fun avl :: "'a avl_tree \<Rightarrow> bool" where
 "avl Leaf = True" |
 "avl (Node l (a,n) r) =
  ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> 
   n = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
 
-fun ht :: "'a avl_tree \<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
-"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
-"balL AB b C =
-  (if ht AB = ht C + 2 then
-     case AB of 
-       Node A (a, _) B \<Rightarrow>
-         if ht A \<ge> ht B then node A a (node B b C)
-         else
-           case B of
-             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 avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
-"balR A a BC =
-   (if ht BC = ht A + 2 then
-      case BC of
-        Node B (b, _) C \<Rightarrow>
-          if ht B \<le> ht C then node (node A a B) b C
-          else
-            case B of
-              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 avl_tree \<Rightarrow> 'a avl_tree" 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
-"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
-"delete _ Leaf = Leaf" |
-"delete x (Node l (a, n) r) =
-  (case cmp x a of
-     EQ \<Rightarrow> if l = Leaf then r
-           else let (l', a') = split_max l in balR l' a' r |
-     LT \<Rightarrow> balR (delete x l) a r |
-     GT \<Rightarrow> balL l a (delete x r))"
-
-
-subsection \<open>Functional Correctness Proofs\<close>
-
-text\<open>Very different from the AFP/AVL proofs\<close>
-
-
-subsubsection "Proofs for insert"
-
-lemma inorder_balL:
-  "inorder (balL l a r) = inorder l @ a # inorder r"
-by (auto simp: node_def balL_def split:tree.splits)
-
-lemma inorder_balR:
-  "inorder (balR l a r) = inorder l @ a # inorder r"
-by (auto simp: node_def balR_def split:tree.splits)
-
-theorem inorder_insert:
-  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
-by (induct t) 
-   (auto simp: ins_list_simps inorder_balL inorder_balR)
-
-
-subsubsection "Proofs for delete"
-
-lemma inorder_split_maxD:
-  "\<lbrakk> split_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
-   inorder t' @ [a] = inorder t"
-by(induction t arbitrary: t' rule: split_max.induct)
-  (auto simp: inorder_balL split: if_splits prod.splits tree.split)
-
-theorem inorder_delete:
-  "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
-by(induction t)
-  (auto simp: del_list_simps inorder_balL inorder_balR inorder_split_maxD split: prod.splits)
-
-
-subsection \<open>AVL invariants\<close>
-
-text\<open>Essentially the AFP/AVL proofs\<close>
-
 
 subsubsection \<open>Insertion maintains AVL balance\<close>
 
diff -r 3b6547bdf6e2 -r 8ad9b2d3dd81 src/HOL/Data_Structures/AVL_Set_Code.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/AVL_Set_Code.thy	Thu Apr 23 22:54:23 2020 +0200
@@ -0,0 +1,107 @@
+(*
+Author:     Tobias Nipkow, Daniel Stüwe
+Based on the AFP entry AVL.
+*)
+
+section "AVL Tree Implementation of Sets"
+
+theory AVL_Set_Code
+imports
+  Cmp
+  Isin2
+begin
+
+subsection \<open>Code\<close>
+
+type_synonym 'a avl_tree = "('a*nat) tree"
+
+definition empty :: "'a avl_tree" where
+"empty = Leaf"
+
+fun ht :: "'a avl_tree \<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
+"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
+"balL AB b C =
+  (if ht AB = ht C + 2 then
+     case AB of 
+       Node A (a, _) B \<Rightarrow>
+         if ht A \<ge> ht B then node A a (node B b C)
+         else
+           case B of
+             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 avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+"balR A a BC =
+   (if ht BC = ht A + 2 then
+      case BC of
+        Node B (b, _) C \<Rightarrow>
+          if ht B \<le> ht C then node (node A a B) b C
+          else
+            case B of
+              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 avl_tree \<Rightarrow> 'a avl_tree" 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
+"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
+"delete _ Leaf = Leaf" |
+"delete x (Node l (a, n) r) =
+  (case cmp x a of
+     EQ \<Rightarrow> if l = Leaf then r
+           else let (l', a') = split_max l in balR l' a' r |
+     LT \<Rightarrow> balR (delete x l) a r |
+     GT \<Rightarrow> balL l a (delete x r))"
+
+
+subsection \<open>Functional Correctness Proofs\<close>
+
+text\<open>Very different from the AFP/AVL proofs\<close>
+
+
+subsubsection "Proofs for insert"
+
+lemma inorder_balL:
+  "inorder (balL l a r) = inorder l @ a # inorder r"
+by (auto simp: node_def balL_def split:tree.splits)
+
+lemma inorder_balR:
+  "inorder (balR l a r) = inorder l @ a # inorder r"
+by (auto simp: node_def balR_def split:tree.splits)
+
+theorem inorder_insert:
+  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
+by (induct t) 
+   (auto simp: ins_list_simps inorder_balL inorder_balR)
+
+
+subsubsection "Proofs for delete"
+
+lemma inorder_split_maxD:
+  "\<lbrakk> split_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
+   inorder t' @ [a] = inorder t"
+by(induction t arbitrary: t' rule: split_max.induct)
+  (auto simp: inorder_balL split: if_splits prod.splits tree.split)
+
+theorem inorder_delete:
+  "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
+by(induction t)
+  (auto simp: del_list_simps inorder_balL inorder_balR inorder_split_maxD split: prod.splits)
+
+end