# HG changeset patch
# User nipkow
# Date 1586271837 -7200
# Node ID 5bbd80875e02d84357cbb263b7f34c6a6a8e3c1d
# Parent  df68b82c818d8d01a2bb9d2c3aadb0bcd5aecf4f# Parent  1cffe8f4d7b3850174cf92499eba39cd9ee7d3b7
merged

diff -r df68b82c818d -r 5bbd80875e02 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Tue Apr 07 09:35:59 2020 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Apr 07 17:03:57 2020 +0200
@@ -127,13 +127,13 @@
 text \<open>First, a fast but relatively manual proof with many lemmas:\<close>
 
 lemma height_balL:
-  "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
+  "\<lbrakk> avl l; avl r; height l = height r + 2 \<rbrakk> \<Longrightarrow>
    height (balL l a r) = height r + 2 \<or>
    height (balL l a r) = height r + 3"
 by (cases l) (auto simp:node_def balL_def split:tree.split)
        
 lemma height_balR:
-  "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
+  "\<lbrakk> avl l; avl r; height r = height l + 2 \<rbrakk> \<Longrightarrow>
    height (balR l a r) = height l + 2 \<or>
    height (balR l a r) = height l + 3"
 by (cases r) (auto simp add:node_def balR_def split:tree.split)
@@ -141,61 +141,25 @@
 lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1"
 by (simp add: node_def)
 
-lemma avl_node:
-  "\<lbrakk> avl l; avl r;
-     height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
-   \<rbrakk> \<Longrightarrow> avl(node l a r)"
-by (auto simp add:max_def node_def)
-
 lemma height_balL2:
   "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
-   height (balL l a r) = (1 + max (height l) (height r))"
+   height (balL l a r) = 1 + max (height l) (height r)"
 by (cases l, cases r) (simp_all add: balL_def)
 
 lemma height_balR2:
   "\<lbrakk> avl l;  avl r;  height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
-   height (balR l a r) = (1 + max (height l) (height r))"
+   height (balR l a r) = 1 + max (height l) (height r)"
 by (cases l, cases r) (simp_all add: balR_def)
 
 lemma avl_balL: 
-  assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
-    \<or> height r = height l + 1 \<or> height l = height r + 2" 
-  shows "avl(balL l a r)"
-proof(cases l rule: tree2_cases)
-  case Leaf
-  with assms show ?thesis by (simp add: node_def balL_def)
-next
-  case Node
-  with assms show ?thesis
-  proof(cases "height l = height r + 2")
-    case True
-    from True Node assms show ?thesis
-      by (auto simp: balL_def intro!: avl_node split: tree.split) arith+
-  next
-    case False
-    with assms show ?thesis by (simp add: avl_node balL_def)
-  qed
-qed
+  "\<lbrakk> avl l; avl r; height r - 1 \<le> height l \<and> height l \<le> height r + 2 \<rbrakk> \<Longrightarrow> avl(balL l a r)"
+by(cases l, cases r)
+  (auto simp: balL_def node_def split!: if_split tree.split)
 
 lemma avl_balR: 
-  assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
-    \<or> height r = height l + 1 \<or> height r = height l + 2" 
-  shows "avl(balR l a r)"
-proof(cases r rule: tree2_cases)
-  case Leaf
-  with assms show ?thesis by (simp add: node_def balR_def)
-next
-  case Node
-  with assms show ?thesis
-  proof(cases "height r = height l + 2")
-    case True
-      from True Node assms show ?thesis
-        by (auto simp: balR_def intro!: avl_node split: tree.split) arith+
-  next
-    case False
-    with assms show ?thesis by (simp add: balR_def avl_node)
-  qed
-qed
+  "\<lbrakk> avl l; avl r; height l - 1 \<le> height r \<and> height r \<le> height l + 2 \<rbrakk> \<Longrightarrow> avl(balR l a r)"
+by(cases r, cases l)
+  (auto simp: balR_def node_def split!: if_split tree.split)
 
 text\<open>Insertion maintains the AVL property. Requires simultaneous proof.\<close>
 
@@ -269,31 +233,19 @@
 theorem avl_insert_auto: "avl t \<Longrightarrow>
   avl(insert x t) \<and> height (insert x t) \<in> {height t, height t + 1}"
 apply (induction t rule: tree2_induct)
- apply (auto split!: if_splits)
- apply (auto simp: balL_def balR_def node_def max_absorb2 split!: tree.splits)
+ (* if you want to save a few secs: apply (auto split!: if_split) *)
+ apply (auto simp: balL_def balR_def node_def max_absorb2 split!: if_split tree.split)
 done
 
 
 subsubsection \<open>Deletion maintains AVL balance\<close>
 
 lemma avl_split_max:
-  assumes "avl x" and "x \<noteq> Leaf"
-  shows "avl (fst (split_max x))" "height x = height(fst (split_max x)) \<or>
-         height x = height(fst (split_max x)) + 1"
-using assms
-proof (induct x rule: split_max_induct)
-  case Node
-  case 1
-  thus ?case using Node
-    by (auto simp: height_balL height_balL2 avl_balL split:prod.split)
-next
-  case (Node l a _ r)
-  case 2
-  let ?r' = "fst (split_max r)"
-  from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all
-  thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a]
-    apply (auto split:prod.splits simp del:avl.simps) by arith+
-qed auto
+  "\<lbrakk> avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
+  avl (fst (split_max t)) \<and>
+  height t \<in> {height(fst (split_max t)), height(fst (split_max t)) + 1}"
+by(induct t rule: split_max_induct)
+  (auto simp: balL_def node_def max_absorb2 split!: prod.split if_split tree.split)
 
 text\<open>Deletion maintains the AVL property:\<close>
 
@@ -304,19 +256,8 @@
 proof (induct t rule: tree2_induct)
   case (Node l a n r)
   case 1
-  show ?case
-  proof(cases "x = a")
-    case True with Node 1 show ?thesis
-      using avl_split_max[of l] by (auto simp: avl_balR split: prod.split)
-  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
+  thus ?case
+    using Node avl_split_max[of l] by (auto simp: avl_balL avl_balR split: prod.split)
   case 2
   show ?case
   proof(cases "x = a")
@@ -363,6 +304,37 @@
   qed
 qed simp_all
 
+text \<open>A more automatic proof.
+Complete automation as for insertion seems hard due to resource requirements.\<close>
+
+theorem avl_delete_auto:
+  assumes "avl t" 
+  shows "avl(delete x t)" and "height t \<in> {height (delete x t), height (delete x t) + 1}"
+using assms
+proof (induct t rule: tree2_induct)
+  case (Node l a n r)
+  case 1
+  show ?case
+  proof(cases "x = a")
+    case True thus ?thesis
+      using 1 avl_split_max[of l] by (auto simp: avl_balR split: prod.split)
+  next
+    case False thus ?thesis
+      using Node 1 by (auto simp: avl_balL avl_balR)
+  qed
+  case 2
+  show ?case
+  proof(cases "x = a")
+    case True thus ?thesis
+      using 1 avl_split_max[of l]
+      by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split)
+  next
+    case False thus ?thesis 
+      using height_balL[of l "delete x r" a] height_balR[of "delete x l" r a] Node 1
+        by(auto simp: balL_def balR_def split!: if_split)
+  qed
+qed simp_all
+
 
 subsection "Overall correctness"