# HG changeset patch
# User nipkow
# Date 1528780698 -7200
# Node ID c1db7503dbaa1ee53d79813c6933b8510724b496
# Parent  e082a36dc35d67f3eb847eeec28c5d80350ce177# Parent  0a3a36fa1d639fe28493408f94f08e3e75df256a
merged

diff -r e082a36dc35d -r c1db7503dbaa src/HOL/Data_Structures/AVL_Map.thy
--- a/src/HOL/Data_Structures/AVL_Map.thy	Mon Jun 11 22:43:52 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Tue Jun 12 07:18:18 2018 +0200
@@ -23,7 +23,7 @@
    GT \<Rightarrow> balL l (a,b) (delete x r))"
 
 
-subsection \<open>Functional Correctness Proofs\<close>
+subsection \<open>Functional Correctness\<close>
 
 theorem inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
@@ -36,9 +36,153 @@
   (auto simp: del_list_simps inorder_balL inorder_balR
      inorder_del_root inorder_split_maxD split: prod.splits)
 
+
+subsection \<open>AVL invariants\<close>
+
+
+subsubsection \<open>Insertion maintains AVL balance\<close>
+
+theorem avl_update:
+  assumes "avl t"
+  shows "avl(update x y t)"
+        "(height (update x y t) = height t \<or> height (update x y t) = height t + 1)"
+using assms
+proof (induction x y t rule: update.induct)
+  case eq2: (2 x y l a b h r)
+  case 1
+  show ?case
+  proof(cases "x = a")
+    case True with eq2 1 show ?thesis by simp
+  next
+    case False
+    with eq2 1 show ?thesis 
+    proof(cases "x<a")
+      case True with eq2 1 show ?thesis by (auto simp add:avl_balL)
+    next
+      case False with eq2 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
+    qed
+  qed
+  case 2
+  show ?case
+  proof(cases "x = a")
+    case True with eq2 1 show ?thesis by simp
+  next
+    case False
+    show ?thesis 
+    proof(cases "x<a")
+      case True
+      show ?thesis
+      proof(cases "height (update x y l) = height r + 2")
+        case False with eq2 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
+      next
+        case True 
+        hence "(height (balL (update x y l) (a,b) r) = height r + 2) \<or>
+          (height (balL (update x y l) (a,b) r) = height r + 3)" (is "?A \<or> ?B")
+          using eq2 2 \<open>x<a\<close> by (intro height_balL) simp_all
+        thus ?thesis
+        proof
+          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
+        next
+          assume ?B with True 1 eq2(2) \<open>x < a\<close> show ?thesis by (simp) arith
+        qed
+      qed
+    next
+      case False
+      show ?thesis
+      proof(cases "height (update x y r) = height l + 2")
+        case False with eq2 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
+      next
+        case True 
+        hence "(height (balR l (a,b) (update x y r)) = height l + 2) \<or>
+          (height (balR l (a,b) (update x y r)) = height l + 3)"  (is "?A \<or> ?B")
+          using eq2 2 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by (intro height_balR) simp_all
+        thus ?thesis 
+        proof
+          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
+        next
+          assume ?B with True 1 eq2(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
+        qed
+      qed
+    qed
+  qed
+qed simp_all
+
+
+subsubsection \<open>Deletion maintains AVL balance\<close>
+
+theorem avl_delete:
+  assumes "avl t" 
+  shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
+using assms
+proof (induct t)
+  case (Node l n h r)
+  obtain a b where [simp]: "n = (a,b)" by fastforce
+  case 1
+  show ?case
+  proof(cases "x = a")
+    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
+  next
+    case False
+    show ?thesis 
+    proof(cases "x<a")
+      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
+    next
+      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL)
+    qed
+  qed
+  case 2
+  show ?case
+  proof(cases "x = a")
+    case True
+    with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
+      \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1"
+      by (subst height_del_root,simp_all)
+    with True show ?thesis by simp
+  next
+    case False
+    show ?thesis 
+    proof(cases "x<a")
+      case True
+      show ?thesis
+      proof(cases "height r = height (delete x l) + 2")
+        case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def)
+      next
+        case True 
+        hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
+          height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
+          using Node 2 by (intro height_balR) auto
+        thus ?thesis 
+        proof
+          assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
+        next
+          assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
+        qed
+      qed
+    next
+      case False
+      show ?thesis
+      proof(cases "height l = height (delete x r) + 2")
+        case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def)
+      next
+        case True 
+        hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
+          height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
+          using Node 2 by (intro height_balL) auto
+        thus ?thesis 
+        proof
+          assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
+        next
+          assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
+        qed
+      qed
+    qed
+  qed
+qed simp_all
+
+
 interpretation Map_by_Ordered
 where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and inv = "\<lambda>_. True"
+and inorder = inorder and inv = avl
 proof (standard, goal_cases)
   case 1 show ?case by simp
 next
@@ -47,6 +191,12 @@
   case 3 thus ?case by(simp add: inorder_update)
 next
   case 4 thus ?case by(simp add: inorder_delete)
-qed auto
+next
+  case 5 show ?case by simp
+next
+  case 6 thus ?case by(simp add: avl_update(1))
+next
+  case 7 thus ?case by(simp add: avl_delete(1))
+qed
 
 end
diff -r e082a36dc35d -r c1db7503dbaa src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Mon Jun 11 22:43:52 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Jun 12 07:18:18 2018 +0200
@@ -121,22 +121,6 @@
     inorder_del_root inorder_split_maxD split: prod.splits)
 
 
-subsubsection "Overall functional correctness"
-
-interpretation Set_by_Ordered
-where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and inv = "\<lambda>_. True"
-proof (standard, goal_cases)
-  case 1 show ?case by simp
-next
-  case 2 thus ?case by(simp add: isin_set_inorder)
-next
-  case 3 thus ?case by(simp add: inorder_insert)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
-
-
 subsection \<open>AVL invariants\<close>
 
 text\<open>Essentially the AFP/AVL proofs\<close>
@@ -224,7 +208,7 @@
 
 text\<open>Insertion maintains the AVL property:\<close>
 
-theorem avl_insert_aux:
+theorem avl_insert:
   assumes "avl t"
   shows "avl(insert x t)"
         "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
@@ -232,32 +216,28 @@
 proof (induction t)
   case (Node l a h r)
   case 1
-  with Node show ?case
+  show ?case
   proof(cases "x = a")
-    case True
-    with Node 1 show ?thesis by simp
+    case True with Node 1 show ?thesis by simp
   next
     case False
-    with Node 1 show ?thesis 
+    show ?thesis 
     proof(cases "x<a")
-      case True
-      with Node 1 show ?thesis by (auto simp add:avl_balL)
+      case True with Node 1 show ?thesis by (auto simp add:avl_balL)
     next
-      case False
-      with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
+      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
     qed
   qed
   case 2
-  from 2 Node show ?case
+  show ?case
   proof(cases "x = a")
-    case True
-    with Node 1 show ?thesis by simp
+    case True with Node 1 show ?thesis by simp
   next
     case False
-    with Node 1 show ?thesis 
-     proof(cases "x<a")
+    show ?thesis 
+    proof(cases "x<a")
       case True
-      with Node 2 show ?thesis
+      show ?thesis
       proof(cases "height (insert x l) = height r + 2")
         case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
       next
@@ -267,19 +247,16 @@
           using Node 2 by (intro height_balL) simp_all
         thus ?thesis
         proof
-          assume ?A
-          with 2 \<open>x < a\<close> show ?thesis by (auto)
+          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
         next
-          assume ?B
-          with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
+          assume ?B with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
         qed
       qed
     next
       case False
-      with Node 2 show ?thesis 
+      show ?thesis 
       proof(cases "height (insert x r) = height l + 2")
-        case False
-        with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
+        case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
       next
         case True 
         hence "(height (balR l a (insert x r)) = height l + 2) \<or>
@@ -287,11 +264,9 @@
           using Node 2 by (intro height_balR) simp_all
         thus ?thesis 
         proof
-          assume ?A
-          with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
+          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
         next
-          assume ?B
-          with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
+          assume ?B with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
         qed
       qed
     qed
@@ -310,9 +285,7 @@
   case (Node l a h r)
   case 1
   thus ?case using Node
-    by (auto simp: height_balL height_balL2 avl_balL
-      linorder_class.max.absorb1 linorder_class.max.absorb2
-      split:prod.split)
+    by (auto simp: height_balL height_balL2 avl_balL split:prod.split)
 next
   case (Node l a h r)
   case 2
@@ -360,16 +333,15 @@
   have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
   proof(cases "height ?r = height ?l' + 2")
     case False
-    show ?thesis using l'_height t_height False by (subst  height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
+    show ?thesis using l'_height t_height False
+      by (subst height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
   next
     case True
     show ?thesis
     proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (split_max ?l)"]])
-      case 1
-      thus ?thesis using l'_height t_height True by arith
+      case 1 thus ?thesis using l'_height t_height True by arith
     next
-      case 2
-      thus ?thesis using l'_height t_height True by arith
+      case 2 thus ?thesis using l'_height t_height True by arith
     qed
   qed
   thus ?thesis using Node_Node by (auto split:prod.splits)
@@ -377,30 +349,27 @@
 
 text\<open>Deletion maintains the AVL property:\<close>
 
-theorem avl_delete_aux:
+theorem avl_delete:
   assumes "avl t" 
   shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
 using assms
 proof (induct t)
   case (Node l n h r)
   case 1
-  with Node show ?case
+  show ?case
   proof(cases "x = n")
-    case True
-    with Node 1 show ?thesis by (auto simp:avl_del_root)
+    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
   next
     case False
-    with Node 1 show ?thesis 
+    show ?thesis 
     proof(cases "x<n")
-      case True
-      with Node 1 show ?thesis by (auto simp add:avl_balR)
+      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
     next
-      case False
-      with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
+      case False with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
     qed
   qed
   case 2
-  with Node show ?case
+  show ?case
   proof(cases "x = n")
     case True
     with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
@@ -409,8 +378,8 @@
     with True show ?thesis by simp
   next
     case False
-    with Node 1 show ?thesis 
-     proof(cases "x<n")
+    show ?thesis 
+    proof(cases "x<n")
       case True
       show ?thesis
       proof(cases "height r = height (delete x l) + 2")
@@ -422,11 +391,9 @@
           using Node 2 by (intro height_balR) auto
         thus ?thesis 
         proof
-          assume ?A
-          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
+          assume ?A with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
         next
-          assume ?B
-          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
+          assume ?B with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
         qed
       qed
     next
@@ -441,11 +408,9 @@
           using Node 2 by (intro height_balL) auto
         thus ?thesis 
         proof
-          assume ?A
-          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
+          assume ?A with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
         next
-          assume ?B
-          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
+          assume ?B with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
         qed
       qed
     qed
@@ -453,6 +418,28 @@
 qed simp_all
 
 
+subsection "Overall correctness"
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and inv = avl
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: isin_set_inorder)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 5 thus ?case by simp
+next
+  case 6 thus ?case by (simp add: avl_insert(1))
+next
+  case 7 thus ?case by (simp add: avl_delete(1))
+qed
+
+
 subsection \<open>Height-Size Relation\<close>
 
 text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>