src/HOL/Data_Structures/AVL_Set.thy
 changeset 68422 0a3a36fa1d63 parent 68413 b56ed5010e69 child 68431 b294e095f64c
```     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Mon Jun 11 20:45:51 2018 +0200
1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Jun 12 07:18:09 2018 +0200
1.3 @@ -121,22 +121,6 @@
1.4      inorder_del_root inorder_split_maxD split: prod.splits)
1.5
1.6
1.7 -subsubsection "Overall functional correctness"
1.8 -
1.9 -interpretation Set_by_Ordered
1.10 -where empty = Leaf and isin = isin and insert = insert and delete = delete
1.11 -and inorder = inorder and inv = "\<lambda>_. True"
1.12 -proof (standard, goal_cases)
1.13 -  case 1 show ?case by simp
1.14 -next
1.15 -  case 2 thus ?case by(simp add: isin_set_inorder)
1.16 -next
1.17 -  case 3 thus ?case by(simp add: inorder_insert)
1.18 -next
1.19 -  case 4 thus ?case by(simp add: inorder_delete)
1.20 -qed (rule TrueI)+
1.21 -
1.22 -
1.23  subsection \<open>AVL invariants\<close>
1.24
1.25  text\<open>Essentially the AFP/AVL proofs\<close>
1.26 @@ -224,7 +208,7 @@
1.27
1.28  text\<open>Insertion maintains the AVL property:\<close>
1.29
1.30 -theorem avl_insert_aux:
1.31 +theorem avl_insert:
1.32    assumes "avl t"
1.33    shows "avl(insert x t)"
1.34          "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
1.35 @@ -232,32 +216,28 @@
1.36  proof (induction t)
1.37    case (Node l a h r)
1.38    case 1
1.39 -  with Node show ?case
1.40 +  show ?case
1.41    proof(cases "x = a")
1.42 -    case True
1.43 -    with Node 1 show ?thesis by simp
1.44 +    case True with Node 1 show ?thesis by simp
1.45    next
1.46      case False
1.47 -    with Node 1 show ?thesis
1.48 +    show ?thesis
1.49      proof(cases "x<a")
1.50 -      case True
1.51 -      with Node 1 show ?thesis by (auto simp add:avl_balL)
1.52 +      case True with Node 1 show ?thesis by (auto simp add:avl_balL)
1.53      next
1.54 -      case False
1.55 -      with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
1.56 +      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
1.57      qed
1.58    qed
1.59    case 2
1.60 -  from 2 Node show ?case
1.61 +  show ?case
1.62    proof(cases "x = a")
1.63 -    case True
1.64 -    with Node 1 show ?thesis by simp
1.65 +    case True with Node 1 show ?thesis by simp
1.66    next
1.67      case False
1.68 -    with Node 1 show ?thesis
1.69 -     proof(cases "x<a")
1.70 +    show ?thesis
1.71 +    proof(cases "x<a")
1.72        case True
1.73 -      with Node 2 show ?thesis
1.74 +      show ?thesis
1.75        proof(cases "height (insert x l) = height r + 2")
1.76          case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
1.77        next
1.78 @@ -267,19 +247,16 @@
1.79            using Node 2 by (intro height_balL) simp_all
1.80          thus ?thesis
1.81          proof
1.82 -          assume ?A
1.83 -          with 2 \<open>x < a\<close> show ?thesis by (auto)
1.84 +          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
1.85          next
1.86 -          assume ?B
1.87 -          with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
1.88 +          assume ?B with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
1.89          qed
1.90        qed
1.91      next
1.92        case False
1.93 -      with Node 2 show ?thesis
1.94 +      show ?thesis
1.95        proof(cases "height (insert x r) = height l + 2")
1.96 -        case False
1.97 -        with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
1.98 +        case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
1.99        next
1.100          case True
1.101          hence "(height (balR l a (insert x r)) = height l + 2) \<or>
1.102 @@ -287,11 +264,9 @@
1.103            using Node 2 by (intro height_balR) simp_all
1.104          thus ?thesis
1.105          proof
1.106 -          assume ?A
1.107 -          with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
1.108 +          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
1.109          next
1.110 -          assume ?B
1.111 -          with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
1.112 +          assume ?B with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
1.113          qed
1.114        qed
1.115      qed
1.116 @@ -310,9 +285,7 @@
1.117    case (Node l a h r)
1.118    case 1
1.119    thus ?case using Node
1.120 -    by (auto simp: height_balL height_balL2 avl_balL
1.121 -      linorder_class.max.absorb1 linorder_class.max.absorb2
1.122 -      split:prod.split)
1.123 +    by (auto simp: height_balL height_balL2 avl_balL split:prod.split)
1.124  next
1.125    case (Node l a h r)
1.126    case 2
1.127 @@ -360,16 +333,15 @@
1.128    have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
1.129    proof(cases "height ?r = height ?l' + 2")
1.130      case False
1.131 -    show ?thesis using l'_height t_height False by (subst  height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
1.132 +    show ?thesis using l'_height t_height False
1.133 +      by (subst height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
1.134    next
1.135      case True
1.136      show ?thesis
1.137      proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (split_max ?l)"]])
1.138 -      case 1
1.139 -      thus ?thesis using l'_height t_height True by arith
1.140 +      case 1 thus ?thesis using l'_height t_height True by arith
1.141      next
1.142 -      case 2
1.143 -      thus ?thesis using l'_height t_height True by arith
1.144 +      case 2 thus ?thesis using l'_height t_height True by arith
1.145      qed
1.146    qed
1.147    thus ?thesis using Node_Node by (auto split:prod.splits)
1.148 @@ -377,30 +349,27 @@
1.149
1.150  text\<open>Deletion maintains the AVL property:\<close>
1.151
1.152 -theorem avl_delete_aux:
1.153 +theorem avl_delete:
1.154    assumes "avl t"
1.155    shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
1.156  using assms
1.157  proof (induct t)
1.158    case (Node l n h r)
1.159    case 1
1.160 -  with Node show ?case
1.161 +  show ?case
1.162    proof(cases "x = n")
1.163 -    case True
1.164 -    with Node 1 show ?thesis by (auto simp:avl_del_root)
1.165 +    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
1.166    next
1.167      case False
1.168 -    with Node 1 show ?thesis
1.169 +    show ?thesis
1.170      proof(cases "x<n")
1.171 -      case True
1.172 -      with Node 1 show ?thesis by (auto simp add:avl_balR)
1.173 +      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
1.174      next
1.175 -      case False
1.176 -      with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
1.177 +      case False with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
1.178      qed
1.179    qed
1.180    case 2
1.181 -  with Node show ?case
1.182 +  show ?case
1.183    proof(cases "x = n")
1.184      case True
1.185      with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
1.186 @@ -409,8 +378,8 @@
1.187      with True show ?thesis by simp
1.188    next
1.189      case False
1.190 -    with Node 1 show ?thesis
1.191 -     proof(cases "x<n")
1.192 +    show ?thesis
1.193 +    proof(cases "x<n")
1.194        case True
1.195        show ?thesis
1.196        proof(cases "height r = height (delete x l) + 2")
1.197 @@ -422,11 +391,9 @@
1.198            using Node 2 by (intro height_balR) auto
1.199          thus ?thesis
1.200          proof
1.201 -          assume ?A
1.202 -          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
1.203 +          assume ?A with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
1.204          next
1.205 -          assume ?B
1.206 -          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
1.207 +          assume ?B with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
1.208          qed
1.209        qed
1.210      next
1.211 @@ -441,11 +408,9 @@
1.212            using Node 2 by (intro height_balL) auto
1.213          thus ?thesis
1.214          proof
1.215 -          assume ?A
1.216 -          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
1.217 +          assume ?A with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
1.218          next
1.219 -          assume ?B
1.220 -          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
1.221 +          assume ?B with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
1.222          qed
1.223        qed
1.224      qed
1.225 @@ -453,6 +418,28 @@
1.226  qed simp_all
1.227
1.228
1.229 +subsection "Overall correctness"
1.230 +
1.231 +interpretation Set_by_Ordered
1.232 +where empty = Leaf and isin = isin and insert = insert and delete = delete
1.233 +and inorder = inorder and inv = avl
1.234 +proof (standard, goal_cases)
1.235 +  case 1 show ?case by simp
1.236 +next
1.237 +  case 2 thus ?case by(simp add: isin_set_inorder)
1.238 +next
1.239 +  case 3 thus ?case by(simp add: inorder_insert)
1.240 +next
1.241 +  case 4 thus ?case by(simp add: inorder_delete)
1.242 +next
1.243 +  case 5 thus ?case by simp
1.244 +next
1.245 +  case 6 thus ?case by (simp add: avl_insert(1))
1.246 +next
1.247 +  case 7 thus ?case by (simp add: avl_delete(1))
1.248 +qed
1.249 +
1.250 +
1.251  subsection \<open>Height-Size Relation\<close>
1.252
1.253  text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
```