src/HOL/Data_Structures/AVL_Set.thy
changeset 61232 c46faf9762f7
child 61428 5e1938107371
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Wed Sep 23 09:47:04 2015 +0200
     1.3 @@ -0,0 +1,457 @@
     1.4 +(*
     1.5 +Author:     Tobias Nipkow
     1.6 +Derived from AFP entry AVL.
     1.7 +*)
     1.8 +
     1.9 +section "AVL Tree Implementation of Sets"
    1.10 +
    1.11 +theory AVL_Set
    1.12 +imports Isin2
    1.13 +begin
    1.14 +
    1.15 +type_synonym 'a avl_tree = "('a,nat) tree"
    1.16 +
    1.17 +text {* Invariant: *}
    1.18 +
    1.19 +fun avl :: "'a avl_tree \<Rightarrow> bool" where
    1.20 +"avl Leaf = True" |
    1.21 +"avl (Node h l a r) =
    1.22 + ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> 
    1.23 +  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
    1.24 +
    1.25 +fun ht :: "'a avl_tree \<Rightarrow> nat" where
    1.26 +"ht Leaf = 0" |
    1.27 +"ht (Node h l a r) = h"
    1.28 +
    1.29 +definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.30 +"node l a r = Node (max (ht l) (ht r) + 1) l a r"
    1.31 +
    1.32 +definition node_bal_l :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.33 +"node_bal_l l a r = (
    1.34 +  if ht l = ht r + 2 then (case l of 
    1.35 +    Node _ bl b br \<Rightarrow> (if ht bl < ht br
    1.36 +    then case br of
    1.37 +      Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
    1.38 +    else node bl b (node br a r)))
    1.39 +  else node l a r)"
    1.40 +
    1.41 +definition node_bal_r :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.42 +"node_bal_r l a r = (
    1.43 +  if ht r = ht l + 2 then (case r of
    1.44 +    Node _ bl b br \<Rightarrow> (if ht bl > ht br
    1.45 +    then case bl of
    1.46 +      Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
    1.47 +    else node (node l a bl) b br))
    1.48 +  else node l a r)"
    1.49 +
    1.50 +fun insert :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.51 +"insert x Leaf = Node 1 Leaf x Leaf" |
    1.52 +"insert x (Node h l a r) = 
    1.53 +   (if x=a then Node h l a r
    1.54 +    else if x<a
    1.55 +      then node_bal_l (insert x l) a r
    1.56 +      else node_bal_r l a (insert x r))"
    1.57 +
    1.58 +fun delete_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
    1.59 +"delete_max (Node _ l a Leaf) = (l,a)" |
    1.60 +"delete_max (Node _ l a r) = (
    1.61 +  let (r',a') = delete_max r in
    1.62 +  (node_bal_l l a r', a'))"
    1.63 +
    1.64 +lemmas delete_max_induct = delete_max.induct[case_names Leaf Node]
    1.65 +
    1.66 +fun delete_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.67 +"delete_root (Node h Leaf a r) = r" |
    1.68 +"delete_root (Node h l a Leaf) = l" |
    1.69 +"delete_root (Node h l a r) =
    1.70 +  (let (l', a') = delete_max l in node_bal_r l' a' r)"
    1.71 +
    1.72 +lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node]
    1.73 +
    1.74 +fun delete :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.75 +"delete _ Leaf = Leaf" |
    1.76 +"delete x (Node h l a r) = (
    1.77 +   if x = a then delete_root (Node h l a r)
    1.78 +   else if x < a then node_bal_r (delete x l) a r
    1.79 +   else node_bal_l l a (delete x r))"
    1.80 +
    1.81 +
    1.82 +subsection {* Functional Correctness Proofs *}
    1.83 +
    1.84 +text{* Very different from the AFP/AVL proofs *}
    1.85 +
    1.86 +
    1.87 +subsubsection "Proofs for insert"
    1.88 +
    1.89 +lemma inorder_node_bal_l:
    1.90 +  "inorder (node_bal_l l a r) = inorder l @ a # inorder r"
    1.91 +by (auto simp: node_def node_bal_l_def split:tree.splits)
    1.92 +
    1.93 +lemma inorder_node_bal_r:
    1.94 +  "inorder (node_bal_r l a r) = inorder l @ a # inorder r"
    1.95 +by (auto simp: node_def node_bal_r_def split:tree.splits)
    1.96 +
    1.97 +theorem inorder_insert:
    1.98 +  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    1.99 +by (induct t) 
   1.100 +   (auto simp: ins_list_simps inorder_node_bal_l inorder_node_bal_r)
   1.101 +
   1.102 +
   1.103 +subsubsection "Proofs for delete"
   1.104 +
   1.105 +lemma inorder_delete_maxD:
   1.106 +  "\<lbrakk> delete_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
   1.107 +   inorder t' @ [a] = inorder t"
   1.108 +by(induction t arbitrary: t' rule: delete_max.induct)
   1.109 +  (auto simp: inorder_node_bal_l split: prod.splits tree.split)
   1.110 +
   1.111 +lemma inorder_delete_root:
   1.112 +  "inorder (delete_root (Node h l a r)) = inorder l @ inorder r"
   1.113 +by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct)
   1.114 +  (auto simp: inorder_node_bal_r inorder_delete_maxD split: prod.splits)
   1.115 +
   1.116 +theorem inorder_delete:
   1.117 +  "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
   1.118 +by(induction t)
   1.119 +  (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r
   1.120 +    inorder_delete_root inorder_delete_maxD split: prod.splits)
   1.121 +
   1.122 +
   1.123 +subsubsection "Overall functional correctness"
   1.124 +
   1.125 +interpretation Set_by_Ordered
   1.126 +where empty = Leaf and isin = isin and insert = insert and delete = delete
   1.127 +and inorder = inorder and wf = "\<lambda>_. True"
   1.128 +proof (standard, goal_cases)
   1.129 +  case 1 show ?case by simp
   1.130 +next
   1.131 +  case 2 thus ?case by(simp add: isin_set)
   1.132 +next
   1.133 +  case 3 thus ?case by(simp add: inorder_insert)
   1.134 +next
   1.135 +  case 4 thus ?case by(simp add: inorder_delete)
   1.136 +next
   1.137 +  case 5 thus ?case ..
   1.138 +qed
   1.139 +
   1.140 +
   1.141 +subsection {* AVL invariants *}
   1.142 +
   1.143 +text{* Essentially the AFP/AVL proofs *}
   1.144 +
   1.145 +
   1.146 +subsubsection {* Insertion maintains AVL balance *}
   1.147 +
   1.148 +declare Let_def [simp]
   1.149 +
   1.150 +lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
   1.151 +by (induct t) simp_all
   1.152 +
   1.153 +lemma height_node_bal_l:
   1.154 +  "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   1.155 +   height (node_bal_l l a r) = height r + 2 \<or>
   1.156 +   height (node_bal_l l a r) = height r + 3"
   1.157 +by (cases l) (auto simp:node_def node_bal_l_def split:tree.split)
   1.158 +       
   1.159 +lemma height_node_bal_r:
   1.160 +  "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
   1.161 +   height (node_bal_r l a r) = height l + 2 \<or>
   1.162 +   height (node_bal_r l a r) = height l + 3"
   1.163 +by (cases r) (auto simp add:node_def node_bal_r_def split:tree.split)
   1.164 +
   1.165 +lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
   1.166 +by (simp add: node_def)
   1.167 +
   1.168 +lemma avl_node:
   1.169 +  "\<lbrakk> avl l; avl r;
   1.170 +     height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
   1.171 +   \<rbrakk> \<Longrightarrow> avl(node l a r)"
   1.172 +by (auto simp add:max_def node_def)
   1.173 +
   1.174 +lemma height_node_bal_l2:
   1.175 +  "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
   1.176 +   height (node_bal_l l a r) = (1 + max (height l) (height r))"
   1.177 +by (cases l, cases r) (simp_all add: node_bal_l_def)
   1.178 +
   1.179 +lemma height_node_bal_r2:
   1.180 +  "\<lbrakk> avl l;  avl r;  height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
   1.181 +   height (node_bal_r l a r) = (1 + max (height l) (height r))"
   1.182 +by (cases l, cases r) (simp_all add: node_bal_r_def)
   1.183 +
   1.184 +lemma avl_node_bal_l: 
   1.185 +  assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
   1.186 +    \<or> height r = height l + 1 \<or> height l = height r + 2" 
   1.187 +  shows "avl(node_bal_l l a r)"
   1.188 +proof(cases l)
   1.189 +  case Leaf
   1.190 +  with assms show ?thesis by (simp add: node_def node_bal_l_def)
   1.191 +next
   1.192 +  case (Node ln ll lr lh)
   1.193 +  with assms show ?thesis
   1.194 +  proof(cases "height l = height r + 2")
   1.195 +    case True
   1.196 +    from True Node assms show ?thesis
   1.197 +      by (auto simp: node_bal_l_def intro!: avl_node split: tree.split) arith+
   1.198 +  next
   1.199 +    case False
   1.200 +    with assms show ?thesis by (simp add: avl_node node_bal_l_def)
   1.201 +  qed
   1.202 +qed
   1.203 +
   1.204 +lemma avl_node_bal_r: 
   1.205 +  assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
   1.206 +    \<or> height r = height l + 1 \<or> height r = height l + 2" 
   1.207 +  shows "avl(node_bal_r l a r)"
   1.208 +proof(cases r)
   1.209 +  case Leaf
   1.210 +  with assms show ?thesis by (simp add: node_def node_bal_r_def)
   1.211 +next
   1.212 +  case (Node rn rl rr rh)
   1.213 +  with assms show ?thesis
   1.214 +  proof(cases "height r = height l + 2")
   1.215 +    case True
   1.216 +      from True Node assms show ?thesis
   1.217 +        by (auto simp: node_bal_r_def intro!: avl_node split: tree.split) arith+
   1.218 +  next
   1.219 +    case False
   1.220 +    with assms show ?thesis by (simp add: node_bal_r_def avl_node)
   1.221 +  qed
   1.222 +qed
   1.223 +
   1.224 +(* It appears that these two properties need to be proved simultaneously: *)
   1.225 +
   1.226 +text{* Insertion maintains the AVL property: *}
   1.227 +
   1.228 +theorem avl_insert_aux:
   1.229 +  assumes "avl t"
   1.230 +  shows "avl(insert x t)"
   1.231 +        "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
   1.232 +using assms
   1.233 +proof (induction t)
   1.234 +  case (Node h l a r)
   1.235 +  case 1
   1.236 +  with Node show ?case
   1.237 +  proof(cases "x = a")
   1.238 +    case True
   1.239 +    with Node 1 show ?thesis by simp
   1.240 +  next
   1.241 +    case False
   1.242 +    with Node 1 show ?thesis 
   1.243 +    proof(cases "x<a")
   1.244 +      case True
   1.245 +      with Node 1 show ?thesis by (auto simp add:avl_node_bal_l)
   1.246 +    next
   1.247 +      case False
   1.248 +      with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_node_bal_r)
   1.249 +    qed
   1.250 +  qed
   1.251 +  case 2
   1.252 +  from 2 Node show ?case
   1.253 +  proof(cases "x = a")
   1.254 +    case True
   1.255 +    with Node 1 show ?thesis by simp
   1.256 +  next
   1.257 +    case False
   1.258 +    with Node 1 show ?thesis 
   1.259 +     proof(cases "x<a")
   1.260 +      case True
   1.261 +      with Node 2 show ?thesis
   1.262 +      proof(cases "height (insert x l) = height r + 2")
   1.263 +        case False with Node 2 `x < a` show ?thesis by (auto simp: height_node_bal_l2)
   1.264 +      next
   1.265 +        case True 
   1.266 +        hence "(height (node_bal_l (insert x l) a r) = height r + 2) \<or>
   1.267 +          (height (node_bal_l (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
   1.268 +          using Node 2 by (intro height_node_bal_l) simp_all
   1.269 +        thus ?thesis
   1.270 +        proof
   1.271 +          assume ?A
   1.272 +          with 2 `x < a` show ?thesis by (auto)
   1.273 +        next
   1.274 +          assume ?B
   1.275 +          with True 1 Node(2) `x < a` show ?thesis by (simp) arith
   1.276 +        qed
   1.277 +      qed
   1.278 +    next
   1.279 +      case False
   1.280 +      with Node 2 show ?thesis 
   1.281 +      proof(cases "height (insert x r) = height l + 2")
   1.282 +        case False
   1.283 +        with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_node_bal_r2)
   1.284 +      next
   1.285 +        case True 
   1.286 +        hence "(height (node_bal_r l a (insert x r)) = height l + 2) \<or>
   1.287 +          (height (node_bal_r l a (insert x r)) = height l + 3)"  (is "?A \<or> ?B")
   1.288 +          using Node 2 by (intro height_node_bal_r) simp_all
   1.289 +        thus ?thesis 
   1.290 +        proof
   1.291 +          assume ?A
   1.292 +          with 2 `\<not>x < a` show ?thesis by (auto)
   1.293 +        next
   1.294 +          assume ?B
   1.295 +          with True 1 Node(4) `\<not>x < a` show ?thesis by (simp) arith
   1.296 +        qed
   1.297 +      qed
   1.298 +    qed
   1.299 +  qed
   1.300 +qed simp_all
   1.301 +
   1.302 +
   1.303 +subsubsection {* Deletion maintains AVL balance *}
   1.304 +
   1.305 +lemma avl_delete_max:
   1.306 +  assumes "avl x" and "x \<noteq> Leaf"
   1.307 +  shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \<or>
   1.308 +         height x = height(fst (delete_max x)) + 1"
   1.309 +using assms
   1.310 +proof (induct x rule: delete_max_induct)
   1.311 +  case (Node h l a rh rl b rr)
   1.312 +  case 1
   1.313 +  with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto
   1.314 +  with 1 Node have "avl (node_bal_l l a (fst (delete_max (Node rh rl b rr))))"
   1.315 +    by (intro avl_node_bal_l) fastforce+
   1.316 +  thus ?case 
   1.317 +    by (auto simp: height_node_bal_l height_node_bal_l2
   1.318 +      linorder_class.max.absorb1 linorder_class.max.absorb2
   1.319 +      split:prod.split)
   1.320 +next
   1.321 +  case (Node h l a rh rl b rr)
   1.322 +  case 2
   1.323 +  let ?r = "Node rh rl b rr"
   1.324 +  let ?r' = "fst (delete_max ?r)"
   1.325 +  from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all
   1.326 +  thus ?case using Node 2 height_node_bal_l[of l ?r' a] height_node_bal_l2[of l ?r' a]
   1.327 +    apply (auto split:prod.splits simp del:avl.simps) by arith+
   1.328 +qed auto
   1.329 +
   1.330 +lemma avl_delete_root:
   1.331 +  assumes "avl t" and "t \<noteq> Leaf"
   1.332 +  shows "avl(delete_root t)" 
   1.333 +using assms
   1.334 +proof (cases t rule:delete_root_cases)
   1.335 +  case (Node_Node h lh ll ln lr n rh rl rn rr)
   1.336 +  let ?l = "Node lh ll ln lr"
   1.337 +  let ?r = "Node rh rl rn rr"
   1.338 +  let ?l' = "fst (delete_max ?l)"
   1.339 +  from `avl t` and Node_Node have "avl ?r" by simp
   1.340 +  from `avl t` and Node_Node have "avl ?l" by simp
   1.341 +  hence "avl(?l')" "height ?l = height(?l') \<or>
   1.342 +         height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+
   1.343 +  with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
   1.344 +            \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
   1.345 +  with `avl ?l'` `avl ?r` have "avl(node_bal_r ?l' (snd(delete_max ?l)) ?r)"
   1.346 +    by (rule avl_node_bal_r)
   1.347 +  with Node_Node show ?thesis by (auto split:prod.splits)
   1.348 +qed simp_all
   1.349 +
   1.350 +lemma height_delete_root:
   1.351 +  assumes "avl t" and "t \<noteq> Leaf" 
   1.352 +  shows "height t = height(delete_root t) \<or> height t = height(delete_root t) + 1"
   1.353 +using assms
   1.354 +proof (cases t rule: delete_root_cases)
   1.355 +  case (Node_Node h lh ll ln lr n rh rl rn rr)
   1.356 +  let ?l = "Node lh ll ln lr"
   1.357 +  let ?r = "Node rh rl rn rr"
   1.358 +  let ?l' = "fst (delete_max ?l)"
   1.359 +  let ?t' = "node_bal_r ?l' (snd(delete_max ?l)) ?r"
   1.360 +  from `avl t` and Node_Node have "avl ?r" by simp
   1.361 +  from `avl t` and Node_Node have "avl ?l" by simp
   1.362 +  hence "avl(?l')"  by (rule avl_delete_max,simp)
   1.363 +  have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto
   1.364 +  have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp
   1.365 +  have "height t = height ?t' \<or> height t = height ?t' + 1" using  `avl t` Node_Node
   1.366 +  proof(cases "height ?r = height ?l' + 2")
   1.367 +    case False
   1.368 +    show ?thesis using l'_height t_height False by (subst  height_node_bal_r2[OF `avl ?l'` `avl ?r` False])+ arith
   1.369 +  next
   1.370 +    case True
   1.371 +    show ?thesis
   1.372 +    proof(cases rule: disjE[OF height_node_bal_r[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]])
   1.373 +      case 1
   1.374 +      thus ?thesis using l'_height t_height True by arith
   1.375 +    next
   1.376 +      case 2
   1.377 +      thus ?thesis using l'_height t_height True by arith
   1.378 +    qed
   1.379 +  qed
   1.380 +  thus ?thesis using Node_Node by (auto split:prod.splits)
   1.381 +qed simp_all
   1.382 +
   1.383 +text{* Deletion maintains the AVL property: *}
   1.384 +
   1.385 +theorem avl_delete_aux:
   1.386 +  assumes "avl t" 
   1.387 +  shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
   1.388 +using assms
   1.389 +proof (induct t)
   1.390 +  case (Node h l n r)
   1.391 +  case 1
   1.392 +  with Node show ?case
   1.393 +  proof(cases "x = n")
   1.394 +    case True
   1.395 +    with Node 1 show ?thesis by (auto simp:avl_delete_root)
   1.396 +  next
   1.397 +    case False
   1.398 +    with Node 1 show ?thesis 
   1.399 +    proof(cases "x<n")
   1.400 +      case True
   1.401 +      with Node 1 show ?thesis by (auto simp add:avl_node_bal_r)
   1.402 +    next
   1.403 +      case False
   1.404 +      with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_node_bal_l)
   1.405 +    qed
   1.406 +  qed
   1.407 +  case 2
   1.408 +  with Node show ?case
   1.409 +  proof(cases "x = n")
   1.410 +    case True
   1.411 +    with 1 have "height (Node h l n r) = height(delete_root (Node h l n r))
   1.412 +      \<or> height (Node h l n r) = height(delete_root (Node h l n r)) + 1"
   1.413 +      by (subst height_delete_root,simp_all)
   1.414 +    with True show ?thesis by simp
   1.415 +  next
   1.416 +    case False
   1.417 +    with Node 1 show ?thesis 
   1.418 +     proof(cases "x<n")
   1.419 +      case True
   1.420 +      show ?thesis
   1.421 +      proof(cases "height r = height (delete x l) + 2")
   1.422 +        case False with Node 1 `x < n` show ?thesis by(auto simp: node_bal_r_def)
   1.423 +      next
   1.424 +        case True 
   1.425 +        hence "(height (node_bal_r (delete x l) n r) = height (delete x l) + 2) \<or>
   1.426 +          height (node_bal_r (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
   1.427 +          using Node 2 by (intro height_node_bal_r) auto
   1.428 +        thus ?thesis 
   1.429 +        proof
   1.430 +          assume ?A
   1.431 +          with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
   1.432 +        next
   1.433 +          assume ?B
   1.434 +          with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
   1.435 +        qed
   1.436 +      qed
   1.437 +    next
   1.438 +      case False
   1.439 +      show ?thesis
   1.440 +      proof(cases "height l = height (delete x r) + 2")
   1.441 +        case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: node_bal_l_def)
   1.442 +      next
   1.443 +        case True 
   1.444 +        hence "(height (node_bal_l l n (delete x r)) = height (delete x r) + 2) \<or>
   1.445 +          height (node_bal_l l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
   1.446 +          using Node 2 by (intro height_node_bal_l) auto
   1.447 +        thus ?thesis 
   1.448 +        proof
   1.449 +          assume ?A
   1.450 +          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
   1.451 +        next
   1.452 +          assume ?B
   1.453 +          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
   1.454 +        qed
   1.455 +      qed
   1.456 +    qed
   1.457 +  qed
   1.458 +qed simp_all
   1.459 +
   1.460 +end