src/HOL/Data_Structures/AVL_Set.thy
changeset 67406 23307fd33906
parent 66453 cc19f7ca2ed6
child 67964 08cc5ab18c84
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Jan 11 13:48:17 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Jan 12 14:08:53 2018 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  type_synonym 'a avl_tree = "('a,nat) tree"
     1.6  
     1.7 -text {* Invariant: *}
     1.8 +text \<open>Invariant:\<close>
     1.9  
    1.10  fun avl :: "'a avl_tree \<Rightarrow> bool" where
    1.11  "avl Leaf = True" |
    1.12 @@ -80,9 +80,9 @@
    1.13       GT \<Rightarrow> balL l a (delete x r))"
    1.14  
    1.15  
    1.16 -subsection {* Functional Correctness Proofs *}
    1.17 +subsection \<open>Functional Correctness Proofs\<close>
    1.18  
    1.19 -text{* Very different from the AFP/AVL proofs *}
    1.20 +text\<open>Very different from the AFP/AVL proofs\<close>
    1.21  
    1.22  
    1.23  subsubsection "Proofs for insert"
    1.24 @@ -137,12 +137,12 @@
    1.25  qed (rule TrueI)+
    1.26  
    1.27  
    1.28 -subsection {* AVL invariants *}
    1.29 +subsection \<open>AVL invariants\<close>
    1.30  
    1.31 -text{* Essentially the AFP/AVL proofs *}
    1.32 +text\<open>Essentially the AFP/AVL proofs\<close>
    1.33  
    1.34  
    1.35 -subsubsection {* Insertion maintains AVL balance *}
    1.36 +subsubsection \<open>Insertion maintains AVL balance\<close>
    1.37  
    1.38  declare Let_def [simp]
    1.39  
    1.40 @@ -222,7 +222,7 @@
    1.41  
    1.42  (* It appears that these two properties need to be proved simultaneously: *)
    1.43  
    1.44 -text{* Insertion maintains the AVL property: *}
    1.45 +text\<open>Insertion maintains the AVL property:\<close>
    1.46  
    1.47  theorem avl_insert_aux:
    1.48    assumes "avl t"
    1.49 @@ -244,7 +244,7 @@
    1.50        with Node 1 show ?thesis by (auto simp add:avl_balL)
    1.51      next
    1.52        case False
    1.53 -      with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_balR)
    1.54 +      with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
    1.55      qed
    1.56    qed
    1.57    case 2
    1.58 @@ -259,7 +259,7 @@
    1.59        case True
    1.60        with Node 2 show ?thesis
    1.61        proof(cases "height (insert x l) = height r + 2")
    1.62 -        case False with Node 2 `x < a` show ?thesis by (auto simp: height_balL2)
    1.63 +        case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
    1.64        next
    1.65          case True 
    1.66          hence "(height (balL (insert x l) a r) = height r + 2) \<or>
    1.67 @@ -268,10 +268,10 @@
    1.68          thus ?thesis
    1.69          proof
    1.70            assume ?A
    1.71 -          with 2 `x < a` show ?thesis by (auto)
    1.72 +          with 2 \<open>x < a\<close> show ?thesis by (auto)
    1.73          next
    1.74            assume ?B
    1.75 -          with True 1 Node(2) `x < a` show ?thesis by (simp) arith
    1.76 +          with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
    1.77          qed
    1.78        qed
    1.79      next
    1.80 @@ -279,7 +279,7 @@
    1.81        with Node 2 show ?thesis 
    1.82        proof(cases "height (insert x r) = height l + 2")
    1.83          case False
    1.84 -        with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_balR2)
    1.85 +        with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
    1.86        next
    1.87          case True 
    1.88          hence "(height (balR l a (insert x r)) = height l + 2) \<or>
    1.89 @@ -288,10 +288,10 @@
    1.90          thus ?thesis 
    1.91          proof
    1.92            assume ?A
    1.93 -          with 2 `\<not>x < a` show ?thesis by (auto)
    1.94 +          with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
    1.95          next
    1.96            assume ?B
    1.97 -          with True 1 Node(4) `\<not>x < a` show ?thesis by (simp) arith
    1.98 +          with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
    1.99          qed
   1.100        qed
   1.101      qed
   1.102 @@ -299,7 +299,7 @@
   1.103  qed simp_all
   1.104  
   1.105  
   1.106 -subsubsection {* Deletion maintains AVL balance *}
   1.107 +subsubsection \<open>Deletion maintains AVL balance\<close>
   1.108  
   1.109  lemma avl_del_max:
   1.110    assumes "avl x" and "x \<noteq> Leaf"
   1.111 @@ -317,7 +317,7 @@
   1.112    case (Node h l a r)
   1.113    case 2
   1.114    let ?r' = "fst (del_max r)"
   1.115 -  from `avl x` Node 2 have "avl l" and "avl r" by simp_all
   1.116 +  from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all
   1.117    thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a]
   1.118      apply (auto split:prod.splits simp del:avl.simps) by arith+
   1.119  qed auto
   1.120 @@ -331,13 +331,13 @@
   1.121    let ?l = "Node lh ll ln lr"
   1.122    let ?r = "Node rh rl rn rr"
   1.123    let ?l' = "fst (del_max ?l)"
   1.124 -  from `avl t` and Node_Node have "avl ?r" by simp
   1.125 -  from `avl t` and Node_Node have "avl ?l" by simp
   1.126 +  from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
   1.127 +  from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
   1.128    hence "avl(?l')" "height ?l = height(?l') \<or>
   1.129           height ?l = height(?l') + 1" by (rule avl_del_max,simp)+
   1.130 -  with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
   1.131 +  with \<open>avl t\<close> Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
   1.132              \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
   1.133 -  with `avl ?l'` `avl ?r` have "avl(balR ?l' (snd(del_max ?l)) ?r)"
   1.134 +  with \<open>avl ?l'\<close> \<open>avl ?r\<close> have "avl(balR ?l' (snd(del_max ?l)) ?r)"
   1.135      by (rule avl_balR)
   1.136    with Node_Node show ?thesis by (auto split:prod.splits)
   1.137  qed simp_all
   1.138 @@ -352,19 +352,19 @@
   1.139    let ?r = "Node rh rl rn rr"
   1.140    let ?l' = "fst (del_max ?l)"
   1.141    let ?t' = "balR ?l' (snd(del_max ?l)) ?r"
   1.142 -  from `avl t` and Node_Node have "avl ?r" by simp
   1.143 -  from `avl t` and Node_Node have "avl ?l" by simp
   1.144 +  from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
   1.145 +  from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
   1.146    hence "avl(?l')"  by (rule avl_del_max,simp)
   1.147 -  have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_del_max) auto
   1.148 -  have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp
   1.149 -  have "height t = height ?t' \<or> height t = height ?t' + 1" using  `avl t` Node_Node
   1.150 +  have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using \<open>avl ?l\<close> by (intro avl_del_max) auto
   1.151 +  have t_height: "height t = 1 + max (height ?l) (height ?r)" using \<open>avl t\<close> Node_Node by simp
   1.152 +  have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
   1.153    proof(cases "height ?r = height ?l' + 2")
   1.154      case False
   1.155 -    show ?thesis using l'_height t_height False by (subst  height_balR2[OF `avl ?l'` `avl ?r` False])+ arith
   1.156 +    show ?thesis using l'_height t_height False by (subst  height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
   1.157    next
   1.158      case True
   1.159      show ?thesis
   1.160 -    proof(cases rule: disjE[OF height_balR[OF True `avl ?l'` `avl ?r`, of "snd (del_max ?l)"]])
   1.161 +    proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (del_max ?l)"]])
   1.162        case 1
   1.163        thus ?thesis using l'_height t_height True by arith
   1.164      next
   1.165 @@ -375,7 +375,7 @@
   1.166    thus ?thesis using Node_Node by (auto split:prod.splits)
   1.167  qed simp_all
   1.168  
   1.169 -text{* Deletion maintains the AVL property: *}
   1.170 +text\<open>Deletion maintains the AVL property:\<close>
   1.171  
   1.172  theorem avl_delete_aux:
   1.173    assumes "avl t" 
   1.174 @@ -396,7 +396,7 @@
   1.175        with Node 1 show ?thesis by (auto simp add:avl_balR)
   1.176      next
   1.177        case False
   1.178 -      with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_balL)
   1.179 +      with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
   1.180      qed
   1.181    qed
   1.182    case 2
   1.183 @@ -414,7 +414,7 @@
   1.184        case True
   1.185        show ?thesis
   1.186        proof(cases "height r = height (delete x l) + 2")
   1.187 -        case False with Node 1 `x < n` show ?thesis by(auto simp: balR_def)
   1.188 +        case False with Node 1 \<open>x < n\<close> show ?thesis by(auto simp: balR_def)
   1.189        next
   1.190          case True 
   1.191          hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
   1.192 @@ -423,17 +423,17 @@
   1.193          thus ?thesis 
   1.194          proof
   1.195            assume ?A
   1.196 -          with `x < n` Node 2 show ?thesis by(auto simp: balR_def)
   1.197 +          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
   1.198          next
   1.199            assume ?B
   1.200 -          with `x < n` Node 2 show ?thesis by(auto simp: balR_def)
   1.201 +          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
   1.202          qed
   1.203        qed
   1.204      next
   1.205        case False
   1.206        show ?thesis
   1.207        proof(cases "height l = height (delete x r) + 2")
   1.208 -        case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: balL_def)
   1.209 +        case False with Node 1 \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> show ?thesis by(auto simp: balL_def)
   1.210        next
   1.211          case True 
   1.212          hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
   1.213 @@ -442,10 +442,10 @@
   1.214          thus ?thesis 
   1.215          proof
   1.216            assume ?A
   1.217 -          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: balL_def)
   1.218 +          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
   1.219          next
   1.220            assume ?B
   1.221 -          with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: balL_def)
   1.222 +          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
   1.223          qed
   1.224        qed
   1.225      qed