1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Nov 22 09:19:34 2010 +0100
1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Nov 22 09:37:39 2010 +0100
1.3 @@ -21,20 +21,20 @@
1.4 return ()
1.5 }"
1.6
1.7 -lemma crel_swapI [crel_intros]:
1.8 +lemma effect_swapI [effect_intros]:
1.9 assumes "i < Array.length h a" "j < Array.length h a"
1.10 "x = Array.get h a ! i" "y = Array.get h a ! j"
1.11 "h' = Array.update a j x (Array.update a i y h)"
1.12 - shows "crel (swap a i j) h h' r"
1.13 - unfolding swap_def using assms by (auto intro!: crel_intros)
1.14 + shows "effect (swap a i j) h h' r"
1.15 + unfolding swap_def using assms by (auto intro!: effect_intros)
1.16
1.17 lemma swap_permutes:
1.18 - assumes "crel (swap a i j) h h' rs"
1.19 + assumes "effect (swap a i j) h h' rs"
1.20 shows "multiset_of (Array.get h' a)
1.21 = multiset_of (Array.get h a)"
1.22 using assms
1.23 unfolding swap_def
1.24 - by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
1.25 + by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
1.26
1.27 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
1.28 where
1.29 @@ -54,7 +54,7 @@
1.30 declare part1.simps[simp del]
1.31
1.32 lemma part_permutes:
1.33 - assumes "crel (part1 a l r p) h h' rs"
1.34 + assumes "effect (part1 a l r p) h h' rs"
1.35 shows "multiset_of (Array.get h' a)
1.36 = multiset_of (Array.get h a)"
1.37 using assms
1.38 @@ -62,23 +62,23 @@
1.39 case (1 a l r p h h' rs)
1.40 thus ?case
1.41 unfolding part1.simps [of a l r p]
1.42 - by (elim crel_bindE crel_ifE crel_returnE crel_nthE) (auto simp add: swap_permutes)
1.43 + by (elim effect_bindE effect_ifE effect_returnE effect_nthE) (auto simp add: swap_permutes)
1.44 qed
1.45
1.46 lemma part_returns_index_in_bounds:
1.47 - assumes "crel (part1 a l r p) h h' rs"
1.48 + assumes "effect (part1 a l r p) h h' rs"
1.49 assumes "l \<le> r"
1.50 shows "l \<le> rs \<and> rs \<le> r"
1.51 using assms
1.52 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.53 case (1 a l r p h h' rs)
1.54 - note cr = `crel (part1 a l r p) h h' rs`
1.55 + note cr = `effect (part1 a l r p) h h' rs`
1.56 show ?case
1.57 proof (cases "r \<le> l")
1.58 case True (* Terminating case *)
1.59 with cr `l \<le> r` show ?thesis
1.60 unfolding part1.simps[of a l r p]
1.61 - by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
1.62 + by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
1.63 next
1.64 case False (* recursive case *)
1.65 note rec_condition = this
1.66 @@ -87,19 +87,19 @@
1.67 proof (cases "?v \<le> p")
1.68 case True
1.69 with cr False
1.70 - have rec1: "crel (part1 a (l + 1) r p) h h' rs"
1.71 + have rec1: "effect (part1 a (l + 1) r p) h h' rs"
1.72 unfolding part1.simps[of a l r p]
1.73 - by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
1.74 + by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
1.75 from rec_condition have "l + 1 \<le> r" by arith
1.76 from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
1.77 show ?thesis by simp
1.78 next
1.79 case False
1.80 with rec_condition cr
1.81 - obtain h1 where swp: "crel (swap a l r) h h1 ()"
1.82 - and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
1.83 + obtain h1 where swp: "effect (swap a l r) h h1 ()"
1.84 + and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
1.85 unfolding part1.simps[of a l r p]
1.86 - by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
1.87 + by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
1.88 from rec_condition have "l \<le> r - 1" by arith
1.89 from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
1.90 qed
1.91 @@ -107,41 +107,41 @@
1.92 qed
1.93
1.94 lemma part_length_remains:
1.95 - assumes "crel (part1 a l r p) h h' rs"
1.96 + assumes "effect (part1 a l r p) h h' rs"
1.97 shows "Array.length h a = Array.length h' a"
1.98 using assms
1.99 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.100 case (1 a l r p h h' rs)
1.101 - note cr = `crel (part1 a l r p) h h' rs`
1.102 + note cr = `effect (part1 a l r p) h h' rs`
1.103
1.104 show ?case
1.105 proof (cases "r \<le> l")
1.106 case True (* Terminating case *)
1.107 with cr show ?thesis
1.108 unfolding part1.simps[of a l r p]
1.109 - by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
1.110 + by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
1.111 next
1.112 case False (* recursive case *)
1.113 with cr 1 show ?thesis
1.114 unfolding part1.simps [of a l r p] swap_def
1.115 - by (auto elim!: crel_bindE crel_ifE crel_nthE crel_returnE crel_updE) fastsimp
1.116 + by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastsimp
1.117 qed
1.118 qed
1.119
1.120 lemma part_outer_remains:
1.121 - assumes "crel (part1 a l r p) h h' rs"
1.122 + assumes "effect (part1 a l r p) h h' rs"
1.123 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
1.124 using assms
1.125 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.126 case (1 a l r p h h' rs)
1.127 - note cr = `crel (part1 a l r p) h h' rs`
1.128 + note cr = `effect (part1 a l r p) h h' rs`
1.129
1.130 show ?case
1.131 proof (cases "r \<le> l")
1.132 case True (* Terminating case *)
1.133 with cr show ?thesis
1.134 unfolding part1.simps[of a l r p]
1.135 - by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
1.136 + by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
1.137 next
1.138 case False (* recursive case *)
1.139 note rec_condition = this
1.140 @@ -150,22 +150,22 @@
1.141 proof (cases "?v \<le> p")
1.142 case True
1.143 with cr False
1.144 - have rec1: "crel (part1 a (l + 1) r p) h h' rs"
1.145 + have rec1: "effect (part1 a (l + 1) r p) h h' rs"
1.146 unfolding part1.simps[of a l r p]
1.147 - by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
1.148 + by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
1.149 from 1(1)[OF rec_condition True rec1]
1.150 show ?thesis by fastsimp
1.151 next
1.152 case False
1.153 with rec_condition cr
1.154 - obtain h1 where swp: "crel (swap a l r) h h1 ()"
1.155 - and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
1.156 + obtain h1 where swp: "effect (swap a l r) h h1 ()"
1.157 + and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
1.158 unfolding part1.simps[of a l r p]
1.159 - by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
1.160 + by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
1.161 from swp rec_condition have
1.162 "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
1.163 unfolding swap_def
1.164 - by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
1.165 + by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
1.166 with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
1.167 qed
1.168 qed
1.169 @@ -173,20 +173,20 @@
1.170
1.171
1.172 lemma part_partitions:
1.173 - assumes "crel (part1 a l r p) h h' rs"
1.174 + assumes "effect (part1 a l r p) h h' rs"
1.175 shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p)
1.176 \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)"
1.177 using assms
1.178 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.179 case (1 a l r p h h' rs)
1.180 - note cr = `crel (part1 a l r p) h h' rs`
1.181 + note cr = `effect (part1 a l r p) h h' rs`
1.182
1.183 show ?case
1.184 proof (cases "r \<le> l")
1.185 case True (* Terminating case *)
1.186 with cr have "rs = r"
1.187 unfolding part1.simps[of a l r p]
1.188 - by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
1.189 + by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
1.190 with True
1.191 show ?thesis by auto
1.192 next
1.193 @@ -197,9 +197,9 @@
1.194 proof (cases "?v \<le> p")
1.195 case True
1.196 with lr cr
1.197 - have rec1: "crel (part1 a (l + 1) r p) h h' rs"
1.198 + have rec1: "effect (part1 a (l + 1) r p) h h' rs"
1.199 unfolding part1.simps[of a l r p]
1.200 - by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
1.201 + by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
1.202 from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
1.203 by fastsimp
1.204 have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
1.205 @@ -208,13 +208,13 @@
1.206 next
1.207 case False
1.208 with lr cr
1.209 - obtain h1 where swp: "crel (swap a l r) h h1 ()"
1.210 - and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
1.211 + obtain h1 where swp: "effect (swap a l r) h h1 ()"
1.212 + and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
1.213 unfolding part1.simps[of a l r p]
1.214 - by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
1.215 + by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
1.216 from swp False have "Array.get h1 a ! r \<ge> p"
1.217 unfolding swap_def
1.218 - by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
1.219 + by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
1.220 with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
1.221 by fastsimp
1.222 have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
1.223 @@ -239,70 +239,70 @@
1.224 declare partition.simps[simp del]
1.225
1.226 lemma partition_permutes:
1.227 - assumes "crel (partition a l r) h h' rs"
1.228 + assumes "effect (partition a l r) h h' rs"
1.229 shows "multiset_of (Array.get h' a)
1.230 = multiset_of (Array.get h a)"
1.231 proof -
1.232 from assms part_permutes swap_permutes show ?thesis
1.233 unfolding partition.simps
1.234 - by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
1.235 + by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
1.236 qed
1.237
1.238 lemma partition_length_remains:
1.239 - assumes "crel (partition a l r) h h' rs"
1.240 + assumes "effect (partition a l r) h h' rs"
1.241 shows "Array.length h a = Array.length h' a"
1.242 proof -
1.243 from assms part_length_remains show ?thesis
1.244 unfolding partition.simps swap_def
1.245 - by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
1.246 + by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
1.247 qed
1.248
1.249 lemma partition_outer_remains:
1.250 - assumes "crel (partition a l r) h h' rs"
1.251 + assumes "effect (partition a l r) h h' rs"
1.252 assumes "l < r"
1.253 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
1.254 proof -
1.255 from assms part_outer_remains part_returns_index_in_bounds show ?thesis
1.256 unfolding partition.simps swap_def
1.257 - by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) fastsimp
1.258 + by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastsimp
1.259 qed
1.260
1.261 lemma partition_returns_index_in_bounds:
1.262 - assumes crel: "crel (partition a l r) h h' rs"
1.263 + assumes effect: "effect (partition a l r) h h' rs"
1.264 assumes "l < r"
1.265 shows "l \<le> rs \<and> rs \<le> r"
1.266 proof -
1.267 - from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
1.268 + from effect obtain middle h'' p where part: "effect (part1 a l (r - 1) p) h h'' middle"
1.269 and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1
1.270 else middle)"
1.271 unfolding partition.simps
1.272 - by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
1.273 + by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp
1.274 from `l < r` have "l \<le> r - 1" by arith
1.275 from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
1.276 qed
1.277
1.278 lemma partition_partitions:
1.279 - assumes crel: "crel (partition a l r) h h' rs"
1.280 + assumes effect: "effect (partition a l r) h h' rs"
1.281 assumes "l < r"
1.282 shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and>
1.283 (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)"
1.284 proof -
1.285 let ?pivot = "Array.get h a ! r"
1.286 - from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
1.287 - and swap: "crel (swap a rs r) h1 h' ()"
1.288 + from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle"
1.289 + and swap: "effect (swap a rs r) h1 h' ()"
1.290 and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1
1.291 else middle)"
1.292 unfolding partition.simps
1.293 - by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
1.294 + by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp
1.295 from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
1.296 (Array.update a rs (Array.get h1 a ! r) h1)"
1.297 unfolding swap_def
1.298 - by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
1.299 + by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
1.300 from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
1.301 unfolding swap_def
1.302 - by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
1.303 + by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
1.304 from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
1.305 - unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
1.306 + unfolding swap_def by (elim effect_bindE effect_returnE effect_nthE effect_updE) auto
1.307 from `l < r` have "l \<le> r - 1" by simp
1.308 note middle_in_bounds = part_returns_index_in_bounds[OF part this]
1.309 from part_outer_remains[OF part] `l < r`
1.310 @@ -311,7 +311,7 @@
1.311 with swap
1.312 have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
1.313 unfolding swap_def
1.314 - by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
1.315 + by (auto simp add: Array.length_def elim!: effect_bindE effect_returnE effect_nthE effect_updE) (cases "r = rs", auto)
1.316 from part_partitions [OF part]
1.317 show ?thesis
1.318 proof (cases "Array.get h1 a ! middle \<le> ?pivot")
1.319 @@ -419,7 +419,7 @@
1.320
1.321
1.322 lemma quicksort_permutes:
1.323 - assumes "crel (quicksort a l r) h h' rs"
1.324 + assumes "effect (quicksort a l r) h h' rs"
1.325 shows "multiset_of (Array.get h' a)
1.326 = multiset_of (Array.get h a)"
1.327 using assms
1.328 @@ -427,41 +427,41 @@
1.329 case (1 a l r h h' rs)
1.330 with partition_permutes show ?case
1.331 unfolding quicksort.simps [of a l r]
1.332 - by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
1.333 + by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
1.334 qed
1.335
1.336 lemma length_remains:
1.337 - assumes "crel (quicksort a l r) h h' rs"
1.338 + assumes "effect (quicksort a l r) h h' rs"
1.339 shows "Array.length h a = Array.length h' a"
1.340 using assms
1.341 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.342 case (1 a l r h h' rs)
1.343 with partition_length_remains show ?case
1.344 unfolding quicksort.simps [of a l r]
1.345 - by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
1.346 + by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
1.347 qed
1.348
1.349 lemma quicksort_outer_remains:
1.350 - assumes "crel (quicksort a l r) h h' rs"
1.351 + assumes "effect (quicksort a l r) h h' rs"
1.352 shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
1.353 using assms
1.354 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.355 case (1 a l r h h' rs)
1.356 - note cr = `crel (quicksort a l r) h h' rs`
1.357 + note cr = `effect (quicksort a l r) h h' rs`
1.358 thus ?case
1.359 proof (cases "r > l")
1.360 case False
1.361 with cr have "h' = h"
1.362 unfolding quicksort.simps [of a l r]
1.363 - by (elim crel_ifE crel_returnE) auto
1.364 + by (elim effect_ifE effect_returnE) auto
1.365 thus ?thesis by simp
1.366 next
1.367 case True
1.368 {
1.369 fix h1 h2 p ret1 ret2 i
1.370 - assume part: "crel (partition a l r) h h1 p"
1.371 - assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
1.372 - assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
1.373 + assume part: "effect (partition a l r) h h1 p"
1.374 + assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ret1"
1.375 + assume qs2: "effect (quicksort a (p + 1) r) h2 h' ret2"
1.376 assume pivot: "l \<le> p \<and> p \<le> r"
1.377 assume i_outer: "i < l \<or> r < i"
1.378 from partition_outer_remains [OF part True] i_outer
1.379 @@ -476,25 +476,25 @@
1.380 }
1.381 with cr show ?thesis
1.382 unfolding quicksort.simps [of a l r]
1.383 - by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
1.384 + by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
1.385 qed
1.386 qed
1.387
1.388 lemma quicksort_is_skip:
1.389 - assumes "crel (quicksort a l r) h h' rs"
1.390 + assumes "effect (quicksort a l r) h h' rs"
1.391 shows "r \<le> l \<longrightarrow> h = h'"
1.392 using assms
1.393 unfolding quicksort.simps [of a l r]
1.394 - by (elim crel_ifE crel_returnE) auto
1.395 + by (elim effect_ifE effect_returnE) auto
1.396
1.397 lemma quicksort_sorts:
1.398 - assumes "crel (quicksort a l r) h h' rs"
1.399 + assumes "effect (quicksort a l r) h h' rs"
1.400 assumes l_r_length: "l < Array.length h a" "r < Array.length h a"
1.401 shows "sorted (subarray l (r + 1) a h')"
1.402 using assms
1.403 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.404 case (1 a l r h h' rs)
1.405 - note cr = `crel (quicksort a l r) h h' rs`
1.406 + note cr = `effect (quicksort a l r) h h' rs`
1.407 thus ?case
1.408 proof (cases "r > l")
1.409 case False
1.410 @@ -505,9 +505,9 @@
1.411 case True
1.412 {
1.413 fix h1 h2 p
1.414 - assume part: "crel (partition a l r) h h1 p"
1.415 - assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
1.416 - assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
1.417 + assume part: "effect (partition a l r) h h1 p"
1.418 + assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ()"
1.419 + assume qs2: "effect (quicksort a (p + 1) r) h2 h' ()"
1.420 from partition_returns_index_in_bounds [OF part True]
1.421 have pivot: "l\<le> p \<and> p \<le> r" .
1.422 note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
1.423 @@ -557,25 +557,25 @@
1.424 }
1.425 with True cr show ?thesis
1.426 unfolding quicksort.simps [of a l r]
1.427 - by (elim crel_ifE crel_returnE crel_bindE crel_assertE) auto
1.428 + by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto
1.429 qed
1.430 qed
1.431
1.432
1.433 lemma quicksort_is_sort:
1.434 - assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
1.435 + assumes effect: "effect (quicksort a 0 (Array.length h a - 1)) h h' rs"
1.436 shows "Array.get h' a = sort (Array.get h a)"
1.437 proof (cases "Array.get h a = []")
1.438 case True
1.439 - with quicksort_is_skip[OF crel] show ?thesis
1.440 + with quicksort_is_skip[OF effect] show ?thesis
1.441 unfolding Array.length_def by simp
1.442 next
1.443 case False
1.444 - from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
1.445 + from quicksort_sorts [OF effect] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
1.446 unfolding Array.length_def subarray_def by auto
1.447 - with length_remains[OF crel] have "sorted (Array.get h' a)"
1.448 + with length_remains[OF effect] have "sorted (Array.get h' a)"
1.449 unfolding Array.length_def by simp
1.450 - with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
1.451 + with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastsimp
1.452 qed
1.453
1.454 subsection {* No Errors in quicksort *}
1.455 @@ -590,26 +590,26 @@
1.456 case (1 a l r p)
1.457 thus ?case unfolding part1.simps [of a l r]
1.458 apply (auto intro!: success_intros del: success_ifI simp add: not_le)
1.459 - apply (auto intro!: crel_intros crel_swapI)
1.460 + apply (auto intro!: effect_intros effect_swapI)
1.461 done
1.462 qed
1.463
1.464 lemma success_bindI' [success_intros]: (*FIXME move*)
1.465 assumes "success f h"
1.466 - assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
1.467 + assumes "\<And>h' r. effect f h h' r \<Longrightarrow> success (g r) h'"
1.468 shows "success (f \<guillemotright>= g) h"
1.469 -using assms(1) proof (rule success_crelE)
1.470 +using assms(1) proof (rule success_effectE)
1.471 fix h' r
1.472 - assume "crel f h h' r"
1.473 + assume "effect f h h' r"
1.474 moreover with assms(2) have "success (g r) h'" .
1.475 - ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_crelI)
1.476 + ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
1.477 qed
1.478
1.479 lemma success_partitionI:
1.480 assumes "l < r" "l < Array.length h a" "r < Array.length h a"
1.481 shows "success (partition a l r) h"
1.482 using assms unfolding partition.simps swap_def
1.483 -apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
1.484 +apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: effect_bindE effect_updE effect_nthE effect_returnE simp add:)
1.485 apply (frule part_length_remains)
1.486 apply (frule part_returns_index_in_bounds)
1.487 apply auto
1.488 @@ -633,7 +633,7 @@
1.489 apply auto
1.490 apply (frule partition_returns_index_in_bounds)
1.491 apply auto
1.492 - apply (auto elim!: crel_assertE dest!: partition_length_remains length_remains)
1.493 + apply (auto elim!: effect_assertE dest!: partition_length_remains length_remains)
1.494 apply (subgoal_tac "Suc r \<le> ri \<or> r = ri")
1.495 apply (erule disjE)
1.496 apply auto