author nipkow Tue Jun 12 07:18:09 2018 +0200 (12 months ago) changeset 68422 0a3a36fa1d63 parent 68415 d74ba11680d4 child 68423 c1db7503dbaa
proved avl for map (finally); tuned
```     1.1 --- a/src/HOL/Data_Structures/AVL_Map.thy	Mon Jun 11 20:45:51 2018 +0200
1.2 +++ b/src/HOL/Data_Structures/AVL_Map.thy	Tue Jun 12 07:18:09 2018 +0200
1.3 @@ -23,7 +23,7 @@
1.4     GT \<Rightarrow> balL l (a,b) (delete x r))"
1.5
1.6
1.7 -subsection \<open>Functional Correctness Proofs\<close>
1.8 +subsection \<open>Functional Correctness\<close>
1.9
1.10  theorem inorder_update:
1.11    "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
1.12 @@ -36,9 +36,153 @@
1.13    (auto simp: del_list_simps inorder_balL inorder_balR
1.14       inorder_del_root inorder_split_maxD split: prod.splits)
1.15
1.16 +
1.17 +subsection \<open>AVL invariants\<close>
1.18 +
1.19 +
1.20 +subsubsection \<open>Insertion maintains AVL balance\<close>
1.21 +
1.22 +theorem avl_update:
1.23 +  assumes "avl t"
1.24 +  shows "avl(update x y t)"
1.25 +        "(height (update x y t) = height t \<or> height (update x y t) = height t + 1)"
1.26 +using assms
1.27 +proof (induction x y t rule: update.induct)
1.28 +  case eq2: (2 x y l a b h r)
1.29 +  case 1
1.30 +  show ?case
1.31 +  proof(cases "x = a")
1.32 +    case True with eq2 1 show ?thesis by simp
1.33 +  next
1.34 +    case False
1.35 +    with eq2 1 show ?thesis
1.36 +    proof(cases "x<a")
1.37 +      case True with eq2 1 show ?thesis by (auto simp add:avl_balL)
1.38 +    next
1.39 +      case False with eq2 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
1.40 +    qed
1.41 +  qed
1.42 +  case 2
1.43 +  show ?case
1.44 +  proof(cases "x = a")
1.45 +    case True with eq2 1 show ?thesis by simp
1.46 +  next
1.47 +    case False
1.48 +    show ?thesis
1.49 +    proof(cases "x<a")
1.50 +      case True
1.51 +      show ?thesis
1.52 +      proof(cases "height (update x y l) = height r + 2")
1.53 +        case False with eq2 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
1.54 +      next
1.55 +        case True
1.56 +        hence "(height (balL (update x y l) (a,b) r) = height r + 2) \<or>
1.57 +          (height (balL (update x y l) (a,b) r) = height r + 3)" (is "?A \<or> ?B")
1.58 +          using eq2 2 \<open>x<a\<close> by (intro height_balL) simp_all
1.59 +        thus ?thesis
1.60 +        proof
1.61 +          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
1.62 +        next
1.63 +          assume ?B with True 1 eq2(2) \<open>x < a\<close> show ?thesis by (simp) arith
1.64 +        qed
1.65 +      qed
1.66 +    next
1.67 +      case False
1.68 +      show ?thesis
1.69 +      proof(cases "height (update x y r) = height l + 2")
1.70 +        case False with eq2 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
1.71 +      next
1.72 +        case True
1.73 +        hence "(height (balR l (a,b) (update x y r)) = height l + 2) \<or>
1.74 +          (height (balR l (a,b) (update x y r)) = height l + 3)"  (is "?A \<or> ?B")
1.75 +          using eq2 2 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by (intro height_balR) simp_all
1.76 +        thus ?thesis
1.77 +        proof
1.78 +          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
1.79 +        next
1.80 +          assume ?B with True 1 eq2(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
1.81 +        qed
1.82 +      qed
1.83 +    qed
1.84 +  qed
1.85 +qed simp_all
1.86 +
1.87 +
1.88 +subsubsection \<open>Deletion maintains AVL balance\<close>
1.89 +
1.90 +theorem avl_delete:
1.91 +  assumes "avl t"
1.92 +  shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
1.93 +using assms
1.94 +proof (induct t)
1.95 +  case (Node l n h r)
1.96 +  obtain a b where [simp]: "n = (a,b)" by fastforce
1.97 +  case 1
1.98 +  show ?case
1.99 +  proof(cases "x = a")
1.100 +    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
1.101 +  next
1.102 +    case False
1.103 +    show ?thesis
1.104 +    proof(cases "x<a")
1.105 +      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
1.106 +    next
1.107 +      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL)
1.108 +    qed
1.109 +  qed
1.110 +  case 2
1.111 +  show ?case
1.112 +  proof(cases "x = a")
1.113 +    case True
1.114 +    with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
1.115 +      \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1"
1.116 +      by (subst height_del_root,simp_all)
1.117 +    with True show ?thesis by simp
1.118 +  next
1.119 +    case False
1.120 +    show ?thesis
1.121 +    proof(cases "x<a")
1.122 +      case True
1.123 +      show ?thesis
1.124 +      proof(cases "height r = height (delete x l) + 2")
1.125 +        case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def)
1.126 +      next
1.127 +        case True
1.128 +        hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
1.129 +          height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
1.130 +          using Node 2 by (intro height_balR) auto
1.131 +        thus ?thesis
1.132 +        proof
1.133 +          assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
1.134 +        next
1.135 +          assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
1.136 +        qed
1.137 +      qed
1.138 +    next
1.139 +      case False
1.140 +      show ?thesis
1.141 +      proof(cases "height l = height (delete x r) + 2")
1.142 +        case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def)
1.143 +      next
1.144 +        case True
1.145 +        hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
1.146 +          height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
1.147 +          using Node 2 by (intro height_balL) auto
1.148 +        thus ?thesis
1.149 +        proof
1.150 +          assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
1.151 +        next
1.152 +          assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
1.153 +        qed
1.154 +      qed
1.155 +    qed
1.156 +  qed
1.157 +qed simp_all
1.158 +
1.159 +
1.160  interpretation Map_by_Ordered
1.161  where empty = Leaf and lookup = lookup and update = update and delete = delete
1.162 -and inorder = inorder and inv = "\<lambda>_. True"
1.163 +and inorder = inorder and inv = avl
1.164  proof (standard, goal_cases)
1.165    case 1 show ?case by simp
1.166  next
1.167 @@ -47,6 +191,12 @@
1.168    case 3 thus ?case by(simp add: inorder_update)
1.169  next
1.170    case 4 thus ?case by(simp add: inorder_delete)
1.171 -qed auto
1.172 +next
1.173 +  case 5 show ?case by simp
1.174 +next
1.175 +  case 6 thus ?case by(simp add: avl_update(1))
1.176 +next
1.177 +  case 7 thus ?case by(simp add: avl_delete(1))
1.178 +qed
1.179
1.180  end
```
```     2.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Mon Jun 11 20:45:51 2018 +0200
2.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Jun 12 07:18:09 2018 +0200
2.3 @@ -121,22 +121,6 @@
2.4      inorder_del_root inorder_split_maxD split: prod.splits)
2.5
2.6
2.7 -subsubsection "Overall functional correctness"
2.8 -
2.9 -interpretation Set_by_Ordered
2.10 -where empty = Leaf and isin = isin and insert = insert and delete = delete
2.11 -and inorder = inorder and inv = "\<lambda>_. True"
2.12 -proof (standard, goal_cases)
2.13 -  case 1 show ?case by simp
2.14 -next
2.15 -  case 2 thus ?case by(simp add: isin_set_inorder)
2.16 -next
2.17 -  case 3 thus ?case by(simp add: inorder_insert)
2.18 -next
2.19 -  case 4 thus ?case by(simp add: inorder_delete)
2.20 -qed (rule TrueI)+
2.21 -
2.22 -
2.23  subsection \<open>AVL invariants\<close>
2.24
2.25  text\<open>Essentially the AFP/AVL proofs\<close>
2.26 @@ -224,7 +208,7 @@
2.27
2.28  text\<open>Insertion maintains the AVL property:\<close>
2.29
2.30 -theorem avl_insert_aux:
2.31 +theorem avl_insert:
2.32    assumes "avl t"
2.33    shows "avl(insert x t)"
2.34          "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
2.35 @@ -232,32 +216,28 @@
2.36  proof (induction t)
2.37    case (Node l a h r)
2.38    case 1
2.39 -  with Node show ?case
2.40 +  show ?case
2.41    proof(cases "x = a")
2.42 -    case True
2.43 -    with Node 1 show ?thesis by simp
2.44 +    case True with Node 1 show ?thesis by simp
2.45    next
2.46      case False
2.47 -    with Node 1 show ?thesis
2.48 +    show ?thesis
2.49      proof(cases "x<a")
2.50 -      case True
2.51 -      with Node 1 show ?thesis by (auto simp add:avl_balL)
2.52 +      case True with Node 1 show ?thesis by (auto simp add:avl_balL)
2.53      next
2.54 -      case False
2.55 -      with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
2.56 +      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
2.57      qed
2.58    qed
2.59    case 2
2.60 -  from 2 Node show ?case
2.61 +  show ?case
2.62    proof(cases "x = a")
2.63 -    case True
2.64 -    with Node 1 show ?thesis by simp
2.65 +    case True with Node 1 show ?thesis by simp
2.66    next
2.67      case False
2.68 -    with Node 1 show ?thesis
2.69 -     proof(cases "x<a")
2.70 +    show ?thesis
2.71 +    proof(cases "x<a")
2.72        case True
2.73 -      with Node 2 show ?thesis
2.74 +      show ?thesis
2.75        proof(cases "height (insert x l) = height r + 2")
2.76          case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
2.77        next
2.78 @@ -267,19 +247,16 @@
2.79            using Node 2 by (intro height_balL) simp_all
2.80          thus ?thesis
2.81          proof
2.82 -          assume ?A
2.83 -          with 2 \<open>x < a\<close> show ?thesis by (auto)
2.84 +          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
2.85          next
2.86 -          assume ?B
2.87 -          with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
2.88 +          assume ?B with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
2.89          qed
2.90        qed
2.91      next
2.92        case False
2.93 -      with Node 2 show ?thesis
2.94 +      show ?thesis
2.95        proof(cases "height (insert x r) = height l + 2")
2.96 -        case False
2.97 -        with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
2.98 +        case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
2.99        next
2.100          case True
2.101          hence "(height (balR l a (insert x r)) = height l + 2) \<or>
2.102 @@ -287,11 +264,9 @@
2.103            using Node 2 by (intro height_balR) simp_all
2.104          thus ?thesis
2.105          proof
2.106 -          assume ?A
2.107 -          with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
2.108 +          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
2.109          next
2.110 -          assume ?B
2.111 -          with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
2.112 +          assume ?B with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
2.113          qed
2.114        qed
2.115      qed
2.116 @@ -310,9 +285,7 @@
2.117    case (Node l a h r)
2.118    case 1
2.119    thus ?case using Node
2.120 -    by (auto simp: height_balL height_balL2 avl_balL
2.121 -      linorder_class.max.absorb1 linorder_class.max.absorb2
2.122 -      split:prod.split)
2.123 +    by (auto simp: height_balL height_balL2 avl_balL split:prod.split)
2.124  next
2.125    case (Node l a h r)
2.126    case 2
2.127 @@ -360,16 +333,15 @@
2.128    have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
2.129    proof(cases "height ?r = height ?l' + 2")
2.130      case False
2.131 -    show ?thesis using l'_height t_height False by (subst  height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
2.132 +    show ?thesis using l'_height t_height False
2.133 +      by (subst height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
2.134    next
2.135      case True
2.136      show ?thesis
2.137      proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (split_max ?l)"]])
2.138 -      case 1
2.139 -      thus ?thesis using l'_height t_height True by arith
2.140 +      case 1 thus ?thesis using l'_height t_height True by arith
2.141      next
2.142 -      case 2
2.143 -      thus ?thesis using l'_height t_height True by arith
2.144 +      case 2 thus ?thesis using l'_height t_height True by arith
2.145      qed
2.146    qed
2.147    thus ?thesis using Node_Node by (auto split:prod.splits)
2.148 @@ -377,30 +349,27 @@
2.149
2.150  text\<open>Deletion maintains the AVL property:\<close>
2.151
2.152 -theorem avl_delete_aux:
2.153 +theorem avl_delete:
2.154    assumes "avl t"
2.155    shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
2.156  using assms
2.157  proof (induct t)
2.158    case (Node l n h r)
2.159    case 1
2.160 -  with Node show ?case
2.161 +  show ?case
2.162    proof(cases "x = n")
2.163 -    case True
2.164 -    with Node 1 show ?thesis by (auto simp:avl_del_root)
2.165 +    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
2.166    next
2.167      case False
2.168 -    with Node 1 show ?thesis
2.169 +    show ?thesis
2.170      proof(cases "x<n")
2.171 -      case True
2.172 -      with Node 1 show ?thesis by (auto simp add:avl_balR)
2.173 +      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
2.174      next
2.175 -      case False
2.176 -      with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
2.177 +      case False with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
2.178      qed
2.179    qed
2.180    case 2
2.181 -  with Node show ?case
2.182 +  show ?case
2.183    proof(cases "x = n")
2.184      case True
2.185      with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
2.186 @@ -409,8 +378,8 @@
2.187      with True show ?thesis by simp
2.188    next
2.189      case False
2.190 -    with Node 1 show ?thesis
2.191 -     proof(cases "x<n")
2.192 +    show ?thesis
2.193 +    proof(cases "x<n")
2.194        case True
2.195        show ?thesis
2.196        proof(cases "height r = height (delete x l) + 2")
2.197 @@ -422,11 +391,9 @@
2.198            using Node 2 by (intro height_balR) auto
2.199          thus ?thesis
2.200          proof
2.201 -          assume ?A
2.202 -          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
2.203 +          assume ?A with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
2.204          next
2.205 -          assume ?B
2.206 -          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
2.207 +          assume ?B with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
2.208          qed
2.209        qed
2.210      next
2.211 @@ -441,11 +408,9 @@
2.212            using Node 2 by (intro height_balL) auto
2.213          thus ?thesis
2.214          proof
2.215 -          assume ?A
2.216 -          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
2.217 +          assume ?A with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
2.218          next
2.219 -          assume ?B
2.220 -          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
2.221 +          assume ?B with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
2.222          qed
2.223        qed
2.224      qed
2.225 @@ -453,6 +418,28 @@
2.226  qed simp_all
2.227
2.228
2.229 +subsection "Overall correctness"
2.230 +
2.231 +interpretation Set_by_Ordered
2.232 +where empty = Leaf and isin = isin and insert = insert and delete = delete
2.233 +and inorder = inorder and inv = avl
2.234 +proof (standard, goal_cases)
2.235 +  case 1 show ?case by simp
2.236 +next
2.237 +  case 2 thus ?case by(simp add: isin_set_inorder)
2.238 +next
2.239 +  case 3 thus ?case by(simp add: inorder_insert)
2.240 +next
2.241 +  case 4 thus ?case by(simp add: inorder_delete)
2.242 +next
2.243 +  case 5 thus ?case by simp
2.244 +next
2.245 +  case 6 thus ?case by (simp add: avl_insert(1))
2.246 +next
2.247 +  case 7 thus ?case by (simp add: avl_delete(1))
2.248 +qed
2.249 +
2.250 +
2.251  subsection \<open>Height-Size Relation\<close>
2.252
2.253  text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
```