moved Imperative_HOL examples to Imperative_HOL/ex
authorhaftmann
Mon Mar 23 19:01:17 2009 +0100 (2009-03-23 ago)
changeset 30689b14b2cc4e25e
parent 30688 2d1d426e00e4
child 30690 55ef8e045931
moved Imperative_HOL examples to Imperative_HOL/ex
src/HOL/Imperative_HOL/ROOT.ML
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Subarray.thy
src/HOL/Imperative_HOL/ex/Sublist.thy
src/HOL/IsaMakefile
src/HOL/ex/ImperativeQuicksort.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Subarray.thy
src/HOL/ex/Sublist.thy
     1.1 --- a/src/HOL/Imperative_HOL/ROOT.ML	Mon Mar 23 19:01:17 2009 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/ROOT.ML	Mon Mar 23 19:01:17 2009 +0100
     1.3 @@ -1,2 +1,2 @@
     1.4  
     1.5 -use_thy "Imperative_HOL";
     1.6 +use_thy "Imperative_HOL_ex";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Mar 23 19:01:17 2009 +0100
     2.3 @@ -0,0 +1,639 @@
     2.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
     2.5 +
     2.6 +theory Imperative_Quicksort
     2.7 +imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
     2.8 +begin
     2.9 +
    2.10 +text {* We prove QuickSort correct in the Relational Calculus. *}
    2.11 +
    2.12 +definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
    2.13 +where
    2.14 +  "swap arr i j = (
    2.15 +     do
    2.16 +       x \<leftarrow> nth arr i;
    2.17 +       y \<leftarrow> nth arr j;
    2.18 +       upd i y arr;
    2.19 +       upd j x arr;
    2.20 +       return ()
    2.21 +     done)"
    2.22 +
    2.23 +lemma swap_permutes:
    2.24 +  assumes "crel (swap a i j) h h' rs"
    2.25 +  shows "multiset_of (get_array a h') 
    2.26 +  = multiset_of (get_array a h)"
    2.27 +  using assms
    2.28 +  unfolding swap_def
    2.29 +  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
    2.30 +
    2.31 +function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    2.32 +where
    2.33 +  "part1 a left right p = (
    2.34 +     if (right \<le> left) then return right
    2.35 +     else (do
    2.36 +       v \<leftarrow> nth a left;
    2.37 +       (if (v \<le> p) then (part1 a (left + 1) right p)
    2.38 +                    else (do swap a left right;
    2.39 +  part1 a left (right - 1) p done))
    2.40 +     done))"
    2.41 +by pat_completeness auto
    2.42 +
    2.43 +termination
    2.44 +by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
    2.45 +
    2.46 +declare part1.simps[simp del]
    2.47 +
    2.48 +lemma part_permutes:
    2.49 +  assumes "crel (part1 a l r p) h h' rs"
    2.50 +  shows "multiset_of (get_array a h') 
    2.51 +  = multiset_of (get_array a h)"
    2.52 +  using assms
    2.53 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    2.54 +  case (1 a l r p h h' rs)
    2.55 +  thus ?case
    2.56 +    unfolding part1.simps [of a l r p]
    2.57 +    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
    2.58 +qed
    2.59 +
    2.60 +lemma part_returns_index_in_bounds:
    2.61 +  assumes "crel (part1 a l r p) h h' rs"
    2.62 +  assumes "l \<le> r"
    2.63 +  shows "l \<le> rs \<and> rs \<le> r"
    2.64 +using assms
    2.65 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    2.66 +  case (1 a l r p h h' rs)
    2.67 +  note cr = `crel (part1 a l r p) h h' rs`
    2.68 +  show ?case
    2.69 +  proof (cases "r \<le> l")
    2.70 +    case True (* Terminating case *)
    2.71 +    with cr `l \<le> r` show ?thesis
    2.72 +      unfolding part1.simps[of a l r p]
    2.73 +      by (elim crelE crel_if crel_return crel_nth) auto
    2.74 +  next
    2.75 +    case False (* recursive case *)
    2.76 +    note rec_condition = this
    2.77 +    let ?v = "get_array a h ! l"
    2.78 +    show ?thesis
    2.79 +    proof (cases "?v \<le> p")
    2.80 +      case True
    2.81 +      with cr False
    2.82 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    2.83 +        unfolding part1.simps[of a l r p]
    2.84 +        by (elim crelE crel_nth crel_if crel_return) auto
    2.85 +      from rec_condition have "l + 1 \<le> r" by arith
    2.86 +      from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    2.87 +      show ?thesis by simp
    2.88 +    next
    2.89 +      case False
    2.90 +      with rec_condition cr
    2.91 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
    2.92 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    2.93 +        unfolding part1.simps[of a l r p]
    2.94 +        by (elim crelE crel_nth crel_if crel_return) auto
    2.95 +      from rec_condition have "l \<le> r - 1" by arith
    2.96 +      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    2.97 +    qed
    2.98 +  qed
    2.99 +qed
   2.100 +
   2.101 +lemma part_length_remains:
   2.102 +  assumes "crel (part1 a l r p) h h' rs"
   2.103 +  shows "Heap.length a h = Heap.length a h'"
   2.104 +using assms
   2.105 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   2.106 +  case (1 a l r p h h' rs)
   2.107 +  note cr = `crel (part1 a l r p) h h' rs`
   2.108 +  
   2.109 +  show ?case
   2.110 +  proof (cases "r \<le> l")
   2.111 +    case True (* Terminating case *)
   2.112 +    with cr show ?thesis
   2.113 +      unfolding part1.simps[of a l r p]
   2.114 +      by (elim crelE crel_if crel_return crel_nth) auto
   2.115 +  next
   2.116 +    case False (* recursive case *)
   2.117 +    with cr 1 show ?thesis
   2.118 +      unfolding part1.simps [of a l r p] swap_def
   2.119 +      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
   2.120 +  qed
   2.121 +qed
   2.122 +
   2.123 +lemma part_outer_remains:
   2.124 +  assumes "crel (part1 a l r p) h h' rs"
   2.125 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   2.126 +  using assms
   2.127 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   2.128 +  case (1 a l r p h h' rs)
   2.129 +  note cr = `crel (part1 a l r p) h h' rs`
   2.130 +  
   2.131 +  show ?case
   2.132 +  proof (cases "r \<le> l")
   2.133 +    case True (* Terminating case *)
   2.134 +    with cr show ?thesis
   2.135 +      unfolding part1.simps[of a l r p]
   2.136 +      by (elim crelE crel_if crel_return crel_nth) auto
   2.137 +  next
   2.138 +    case False (* recursive case *)
   2.139 +    note rec_condition = this
   2.140 +    let ?v = "get_array a h ! l"
   2.141 +    show ?thesis
   2.142 +    proof (cases "?v \<le> p")
   2.143 +      case True
   2.144 +      with cr False
   2.145 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   2.146 +        unfolding part1.simps[of a l r p]
   2.147 +        by (elim crelE crel_nth crel_if crel_return) auto
   2.148 +      from 1(1)[OF rec_condition True rec1]
   2.149 +      show ?thesis by fastsimp
   2.150 +    next
   2.151 +      case False
   2.152 +      with rec_condition cr
   2.153 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   2.154 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   2.155 +        unfolding part1.simps[of a l r p]
   2.156 +        by (elim crelE crel_nth crel_if crel_return) auto
   2.157 +      from swp rec_condition have
   2.158 +        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
   2.159 +	unfolding swap_def
   2.160 +	by (elim crelE crel_nth crel_upd crel_return) auto
   2.161 +      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   2.162 +    qed
   2.163 +  qed
   2.164 +qed
   2.165 +
   2.166 +
   2.167 +lemma part_partitions:
   2.168 +  assumes "crel (part1 a l r p) h h' rs"
   2.169 +  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
   2.170 +  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
   2.171 +  using assms
   2.172 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   2.173 +  case (1 a l r p h h' rs)
   2.174 +  note cr = `crel (part1 a l r p) h h' rs`
   2.175 +  
   2.176 +  show ?case
   2.177 +  proof (cases "r \<le> l")
   2.178 +    case True (* Terminating case *)
   2.179 +    with cr have "rs = r"
   2.180 +      unfolding part1.simps[of a l r p]
   2.181 +      by (elim crelE crel_if crel_return crel_nth) auto
   2.182 +    with True
   2.183 +    show ?thesis by auto
   2.184 +  next
   2.185 +    case False (* recursive case *)
   2.186 +    note lr = this
   2.187 +    let ?v = "get_array a h ! l"
   2.188 +    show ?thesis
   2.189 +    proof (cases "?v \<le> p")
   2.190 +      case True
   2.191 +      with lr cr
   2.192 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   2.193 +        unfolding part1.simps[of a l r p]
   2.194 +        by (elim crelE crel_nth crel_if crel_return) auto
   2.195 +      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
   2.196 +	by fastsimp
   2.197 +      have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
   2.198 +      with 1(1)[OF False True rec1] a_l show ?thesis
   2.199 +	by auto
   2.200 +    next
   2.201 +      case False
   2.202 +      with lr cr
   2.203 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   2.204 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   2.205 +        unfolding part1.simps[of a l r p]
   2.206 +        by (elim crelE crel_nth crel_if crel_return) auto
   2.207 +      from swp False have "get_array a h1 ! r \<ge> p"
   2.208 +	unfolding swap_def
   2.209 +	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
   2.210 +      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
   2.211 +	by fastsimp
   2.212 +      have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   2.213 +      with 1(2)[OF lr False rec2] a_r show ?thesis
   2.214 +	by auto
   2.215 +    qed
   2.216 +  qed
   2.217 +qed
   2.218 +
   2.219 +
   2.220 +fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
   2.221 +where
   2.222 +  "partition a left right = (do
   2.223 +     pivot \<leftarrow> nth a right;
   2.224 +     middle \<leftarrow> part1 a left (right - 1) pivot;
   2.225 +     v \<leftarrow> nth a middle;
   2.226 +     m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
   2.227 +     swap a m right;
   2.228 +     return m
   2.229 +   done)"
   2.230 +
   2.231 +declare partition.simps[simp del]
   2.232 +
   2.233 +lemma partition_permutes:
   2.234 +  assumes "crel (partition a l r) h h' rs"
   2.235 +  shows "multiset_of (get_array a h') 
   2.236 +  = multiset_of (get_array a h)"
   2.237 +proof -
   2.238 +    from assms part_permutes swap_permutes show ?thesis
   2.239 +      unfolding partition.simps
   2.240 +      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   2.241 +qed
   2.242 +
   2.243 +lemma partition_length_remains:
   2.244 +  assumes "crel (partition a l r) h h' rs"
   2.245 +  shows "Heap.length a h = Heap.length a h'"
   2.246 +proof -
   2.247 +  from assms part_length_remains show ?thesis
   2.248 +    unfolding partition.simps swap_def
   2.249 +    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   2.250 +qed
   2.251 +
   2.252 +lemma partition_outer_remains:
   2.253 +  assumes "crel (partition a l r) h h' rs"
   2.254 +  assumes "l < r"
   2.255 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   2.256 +proof -
   2.257 +  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   2.258 +    unfolding partition.simps swap_def
   2.259 +    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
   2.260 +qed
   2.261 +
   2.262 +lemma partition_returns_index_in_bounds:
   2.263 +  assumes crel: "crel (partition a l r) h h' rs"
   2.264 +  assumes "l < r"
   2.265 +  shows "l \<le> rs \<and> rs \<le> r"
   2.266 +proof -
   2.267 +  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   2.268 +    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
   2.269 +         else middle)"
   2.270 +    unfolding partition.simps
   2.271 +    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   2.272 +  from `l < r` have "l \<le> r - 1" by arith
   2.273 +  from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   2.274 +qed
   2.275 +
   2.276 +lemma partition_partitions:
   2.277 +  assumes crel: "crel (partition a l r) h h' rs"
   2.278 +  assumes "l < r"
   2.279 +  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
   2.280 +  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
   2.281 +proof -
   2.282 +  let ?pivot = "get_array a h ! r" 
   2.283 +  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
   2.284 +    and swap: "crel (swap a rs r) h1 h' ()"
   2.285 +    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
   2.286 +         else middle)"
   2.287 +    unfolding partition.simps
   2.288 +    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   2.289 +  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
   2.290 +    (Heap.upd a rs (get_array a h1 ! r) h1)"
   2.291 +    unfolding swap_def
   2.292 +    by (elim crelE crel_return crel_nth crel_upd) simp
   2.293 +  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
   2.294 +    unfolding swap_def
   2.295 +    by (elim crelE crel_return crel_nth crel_upd) simp
   2.296 +  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
   2.297 +    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   2.298 +  from `l < r` have "l \<le> r - 1" by simp 
   2.299 +  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   2.300 +  from part_outer_remains[OF part] `l < r`
   2.301 +  have "get_array a h ! r = get_array a h1 ! r"
   2.302 +    by fastsimp
   2.303 +  with swap
   2.304 +  have right_remains: "get_array a h ! r = get_array a h' ! rs"
   2.305 +    unfolding swap_def
   2.306 +    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   2.307 +  from part_partitions [OF part]
   2.308 +  show ?thesis
   2.309 +  proof (cases "get_array a h1 ! middle \<le> ?pivot")
   2.310 +    case True
   2.311 +    with rs_equals have rs_equals: "rs = middle + 1" by simp
   2.312 +    { 
   2.313 +      fix i
   2.314 +      assume i_is_left: "l \<le> i \<and> i < rs"
   2.315 +      with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
   2.316 +      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   2.317 +      from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
   2.318 +      with part_partitions[OF part] right_remains True
   2.319 +      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   2.320 +      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
   2.321 +	unfolding Heap.upd_def Heap.length_def by simp
   2.322 +    }
   2.323 +    moreover
   2.324 +    {
   2.325 +      fix i
   2.326 +      assume "rs < i \<and> i \<le> r"
   2.327 +
   2.328 +      hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
   2.329 +      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   2.330 +      proof
   2.331 +	assume i_is: "rs < i \<and> i \<le> r - 1"
   2.332 +	with swap_length_remains in_bounds middle_in_bounds rs_equals
   2.333 +	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   2.334 +	from part_partitions[OF part] rs_equals right_remains i_is
   2.335 +	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   2.336 +	  by fastsimp
   2.337 +	with i_props h'_def show ?thesis by fastsimp
   2.338 +      next
   2.339 +	assume i_is: "rs < i \<and> i = r"
   2.340 +	with rs_equals have "Suc middle \<noteq> r" by arith
   2.341 +	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
   2.342 +	with part_partitions[OF part] right_remains 
   2.343 +	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
   2.344 +	  by fastsimp
   2.345 +	with i_is True rs_equals right_remains h'_def
   2.346 +	show ?thesis using in_bounds
   2.347 +	  unfolding Heap.upd_def Heap.length_def
   2.348 +	  by auto
   2.349 +      qed
   2.350 +    }
   2.351 +    ultimately show ?thesis by auto
   2.352 +  next
   2.353 +    case False
   2.354 +    with rs_equals have rs_equals: "middle = rs" by simp
   2.355 +    { 
   2.356 +      fix i
   2.357 +      assume i_is_left: "l \<le> i \<and> i < rs"
   2.358 +      with swap_length_remains in_bounds middle_in_bounds rs_equals
   2.359 +      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   2.360 +      from part_partitions[OF part] rs_equals right_remains i_is_left
   2.361 +      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   2.362 +      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
   2.363 +	unfolding Heap.upd_def by simp
   2.364 +    }
   2.365 +    moreover
   2.366 +    {
   2.367 +      fix i
   2.368 +      assume "rs < i \<and> i \<le> r"
   2.369 +      hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
   2.370 +      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   2.371 +      proof
   2.372 +	assume i_is: "rs < i \<and> i \<le> r - 1"
   2.373 +	with swap_length_remains in_bounds middle_in_bounds rs_equals
   2.374 +	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   2.375 +	from part_partitions[OF part] rs_equals right_remains i_is
   2.376 +	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   2.377 +	  by fastsimp
   2.378 +	with i_props h'_def show ?thesis by fastsimp
   2.379 +      next
   2.380 +	assume i_is: "i = r"
   2.381 +	from i_is False rs_equals right_remains h'_def
   2.382 +	show ?thesis using in_bounds
   2.383 +	  unfolding Heap.upd_def Heap.length_def
   2.384 +	  by auto
   2.385 +      qed
   2.386 +    }
   2.387 +    ultimately
   2.388 +    show ?thesis by auto
   2.389 +  qed
   2.390 +qed
   2.391 +
   2.392 +
   2.393 +function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
   2.394 +where
   2.395 +  "quicksort arr left right =
   2.396 +     (if (right > left)  then
   2.397 +        do
   2.398 +          pivotNewIndex \<leftarrow> partition arr left right;
   2.399 +          pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
   2.400 +          quicksort arr left (pivotNewIndex - 1);
   2.401 +          quicksort arr (pivotNewIndex + 1) right
   2.402 +        done
   2.403 +     else return ())"
   2.404 +by pat_completeness auto
   2.405 +
   2.406 +(* For termination, we must show that the pivotNewIndex is between left and right *) 
   2.407 +termination
   2.408 +by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
   2.409 +
   2.410 +declare quicksort.simps[simp del]
   2.411 +
   2.412 +
   2.413 +lemma quicksort_permutes:
   2.414 +  assumes "crel (quicksort a l r) h h' rs"
   2.415 +  shows "multiset_of (get_array a h') 
   2.416 +  = multiset_of (get_array a h)"
   2.417 +  using assms
   2.418 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   2.419 +  case (1 a l r h h' rs)
   2.420 +  with partition_permutes show ?case
   2.421 +    unfolding quicksort.simps [of a l r]
   2.422 +    by (elim crel_if crelE crel_assert crel_return) auto
   2.423 +qed
   2.424 +
   2.425 +lemma length_remains:
   2.426 +  assumes "crel (quicksort a l r) h h' rs"
   2.427 +  shows "Heap.length a h = Heap.length a h'"
   2.428 +using assms
   2.429 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   2.430 +  case (1 a l r h h' rs)
   2.431 +  with partition_length_remains show ?case
   2.432 +    unfolding quicksort.simps [of a l r]
   2.433 +    by (elim crel_if crelE crel_assert crel_return) auto
   2.434 +qed
   2.435 +
   2.436 +lemma quicksort_outer_remains:
   2.437 +  assumes "crel (quicksort a l r) h h' rs"
   2.438 +   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   2.439 +  using assms
   2.440 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   2.441 +  case (1 a l r h h' rs)
   2.442 +  note cr = `crel (quicksort a l r) h h' rs`
   2.443 +  thus ?case
   2.444 +  proof (cases "r > l")
   2.445 +    case False
   2.446 +    with cr have "h' = h"
   2.447 +      unfolding quicksort.simps [of a l r]
   2.448 +      by (elim crel_if crel_return) auto
   2.449 +    thus ?thesis by simp
   2.450 +  next
   2.451 +  case True
   2.452 +   { 
   2.453 +      fix h1 h2 p ret1 ret2 i
   2.454 +      assume part: "crel (partition a l r) h h1 p"
   2.455 +      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
   2.456 +      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
   2.457 +      assume pivot: "l \<le> p \<and> p \<le> r"
   2.458 +      assume i_outer: "i < l \<or> r < i"
   2.459 +      from  partition_outer_remains [OF part True] i_outer
   2.460 +      have "get_array a h !i = get_array a h1 ! i" by fastsimp
   2.461 +      moreover
   2.462 +      with 1(1) [OF True pivot qs1] pivot i_outer
   2.463 +      have "get_array a h1 ! i = get_array a h2 ! i" by auto
   2.464 +      moreover
   2.465 +      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
   2.466 +      have "get_array a h2 ! i = get_array a h' ! i" by auto
   2.467 +      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
   2.468 +    }
   2.469 +    with cr show ?thesis
   2.470 +      unfolding quicksort.simps [of a l r]
   2.471 +      by (elim crel_if crelE crel_assert crel_return) auto
   2.472 +  qed
   2.473 +qed
   2.474 +
   2.475 +lemma quicksort_is_skip:
   2.476 +  assumes "crel (quicksort a l r) h h' rs"
   2.477 +  shows "r \<le> l \<longrightarrow> h = h'"
   2.478 +  using assms
   2.479 +  unfolding quicksort.simps [of a l r]
   2.480 +  by (elim crel_if crel_return) auto
   2.481 + 
   2.482 +lemma quicksort_sorts:
   2.483 +  assumes "crel (quicksort a l r) h h' rs"
   2.484 +  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
   2.485 +  shows "sorted (subarray l (r + 1) a h')"
   2.486 +  using assms
   2.487 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   2.488 +  case (1 a l r h h' rs)
   2.489 +  note cr = `crel (quicksort a l r) h h' rs`
   2.490 +  thus ?case
   2.491 +  proof (cases "r > l")
   2.492 +    case False
   2.493 +    hence "l \<ge> r + 1 \<or> l = r" by arith 
   2.494 +    with length_remains[OF cr] 1(5) show ?thesis
   2.495 +      by (auto simp add: subarray_Nil subarray_single)
   2.496 +  next
   2.497 +    case True
   2.498 +    { 
   2.499 +      fix h1 h2 p
   2.500 +      assume part: "crel (partition a l r) h h1 p"
   2.501 +      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
   2.502 +      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
   2.503 +      from partition_returns_index_in_bounds [OF part True]
   2.504 +      have pivot: "l\<le> p \<and> p \<le> r" .
   2.505 +     note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
   2.506 +      from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
   2.507 +      have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
   2.508 +        (*-- First of all, by induction hypothesis both sublists are sorted. *)
   2.509 +      from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
   2.510 +      have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
   2.511 +      from quicksort_outer_remains [OF qs2] length_remains
   2.512 +      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
   2.513 +	by (simp add: subarray_eq_samelength_iff)
   2.514 +      with IH1 have IH1': "sorted (subarray l p a h')" by simp
   2.515 +      from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
   2.516 +      have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
   2.517 +        by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
   2.518 +           (* -- Secondly, both sublists remain partitioned. *)
   2.519 +      from partition_partitions[OF part True]
   2.520 +      have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
   2.521 +        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
   2.522 +        by (auto simp add: all_in_set_subarray_conv)
   2.523 +      from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
   2.524 +        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
   2.525 +      have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
   2.526 +	unfolding Heap.length_def subarray_def by (cases p, auto)
   2.527 +      with left_subarray_remains part_conds1 pivot_unchanged
   2.528 +      have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
   2.529 +        by (simp, subst set_of_multiset_of[symmetric], simp)
   2.530 +          (* -- These steps are the analogous for the right sublist \<dots> *)
   2.531 +      from quicksort_outer_remains [OF qs1] length_remains
   2.532 +      have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
   2.533 +	by (auto simp add: subarray_eq_samelength_iff)
   2.534 +      from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
   2.535 +        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
   2.536 +      have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
   2.537 +        unfolding Heap.length_def subarray_def by auto
   2.538 +      with right_subarray_remains part_conds2 pivot_unchanged
   2.539 +      have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
   2.540 +        by (simp, subst set_of_multiset_of[symmetric], simp)
   2.541 +          (* -- Thirdly and finally, we show that the array is sorted
   2.542 +          following from the facts above. *)
   2.543 +      from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [get_array a h' ! p] @ subarray (p + 1) (r + 1) a h'"
   2.544 +	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
   2.545 +      with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
   2.546 +	unfolding subarray_def
   2.547 +	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
   2.548 +	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   2.549 +    }
   2.550 +    with True cr show ?thesis
   2.551 +      unfolding quicksort.simps [of a l r]
   2.552 +      by (elim crel_if crel_return crelE crel_assert) auto
   2.553 +  qed
   2.554 +qed
   2.555 +
   2.556 +
   2.557 +lemma quicksort_is_sort:
   2.558 +  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
   2.559 +  shows "get_array a h' = sort (get_array a h)"
   2.560 +proof (cases "get_array a h = []")
   2.561 +  case True
   2.562 +  with quicksort_is_skip[OF crel] show ?thesis
   2.563 +  unfolding Heap.length_def by simp
   2.564 +next
   2.565 +  case False
   2.566 +  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
   2.567 +    unfolding Heap.length_def subarray_def by auto
   2.568 +  with length_remains[OF crel] have "sorted (get_array a h')"
   2.569 +    unfolding Heap.length_def by simp
   2.570 +  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
   2.571 +qed
   2.572 +
   2.573 +subsection {* No Errors in quicksort *}
   2.574 +text {* We have proved that quicksort sorts (if no exceptions occur).
   2.575 +We will now show that exceptions do not occur. *}
   2.576 +
   2.577 +lemma noError_part1: 
   2.578 +  assumes "l < Heap.length a h" "r < Heap.length a h"
   2.579 +  shows "noError (part1 a l r p) h"
   2.580 +  using assms
   2.581 +proof (induct a l r p arbitrary: h rule: part1.induct)
   2.582 +  case (1 a l r p)
   2.583 +  thus ?case
   2.584 +    unfolding part1.simps [of a l r] swap_def
   2.585 +    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
   2.586 +qed
   2.587 +
   2.588 +lemma noError_partition:
   2.589 +  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
   2.590 +  shows "noError (partition a l r) h"
   2.591 +using assms
   2.592 +unfolding partition.simps swap_def
   2.593 +apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
   2.594 +apply (frule part_length_remains)
   2.595 +apply (frule part_returns_index_in_bounds)
   2.596 +apply auto
   2.597 +apply (frule part_length_remains)
   2.598 +apply (frule part_returns_index_in_bounds)
   2.599 +apply auto
   2.600 +apply (frule part_length_remains)
   2.601 +apply auto
   2.602 +done
   2.603 +
   2.604 +lemma noError_quicksort:
   2.605 +  assumes "l < Heap.length a h" "r < Heap.length a h"
   2.606 +  shows "noError (quicksort a l r) h"
   2.607 +using assms
   2.608 +proof (induct a l r arbitrary: h rule: quicksort.induct)
   2.609 +  case (1 a l ri h)
   2.610 +  thus ?case
   2.611 +    unfolding quicksort.simps [of a l ri]
   2.612 +    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
   2.613 +    apply (frule partition_returns_index_in_bounds)
   2.614 +    apply auto
   2.615 +    apply (frule partition_returns_index_in_bounds)
   2.616 +    apply auto
   2.617 +    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
   2.618 +    apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   2.619 +    apply (erule disjE)
   2.620 +    apply auto
   2.621 +    unfolding quicksort.simps [of a "Suc ri" ri]
   2.622 +    apply (auto intro!: noError_if noError_return)
   2.623 +    done
   2.624 +qed
   2.625 +
   2.626 +
   2.627 +subsection {* Example *}
   2.628 +
   2.629 +definition "qsort a = do
   2.630 +    k \<leftarrow> length a;
   2.631 +    quicksort a 0 (k - 1);
   2.632 +    return a
   2.633 +  done"
   2.634 +
   2.635 +ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
   2.636 +
   2.637 +export_code qsort in SML_imp module_name QSort
   2.638 +export_code qsort in OCaml module_name QSort file -
   2.639 +export_code qsort in OCaml_imp module_name QSort file -
   2.640 +export_code qsort in Haskell module_name QSort file -
   2.641 +
   2.642 +end
   2.643 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Mon Mar 23 19:01:17 2009 +0100
     3.3 @@ -0,0 +1,66 @@
     3.4 +theory Subarray
     3.5 +imports Array Sublist
     3.6 +begin
     3.7 +
     3.8 +definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
     3.9 +where
    3.10 +  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
    3.11 +
    3.12 +lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    3.13 +apply (simp add: subarray_def Heap.upd_def)
    3.14 +apply (simp add: sublist'_update1)
    3.15 +done
    3.16 +
    3.17 +lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    3.18 +apply (simp add: subarray_def Heap.upd_def)
    3.19 +apply (subst sublist'_update2)
    3.20 +apply fastsimp
    3.21 +apply simp
    3.22 +done
    3.23 +
    3.24 +lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
    3.25 +unfolding subarray_def Heap.upd_def
    3.26 +by (simp add: sublist'_update3)
    3.27 +
    3.28 +lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
    3.29 +by (simp add: subarray_def sublist'_Nil')
    3.30 +
    3.31 +lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
    3.32 +by (simp add: subarray_def Heap.length_def sublist'_single)
    3.33 +
    3.34 +lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
    3.35 +by (simp add: subarray_def Heap.length_def length_sublist')
    3.36 +
    3.37 +lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
    3.38 +by (simp add: length_subarray)
    3.39 +
    3.40 +lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
    3.41 +unfolding Heap.length_def subarray_def
    3.42 +by (simp add: sublist'_front)
    3.43 +
    3.44 +lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
    3.45 +unfolding Heap.length_def subarray_def
    3.46 +by (simp add: sublist'_back)
    3.47 +
    3.48 +lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
    3.49 +unfolding subarray_def
    3.50 +by (simp add: sublist'_append)
    3.51 +
    3.52 +lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
    3.53 +unfolding Heap.length_def subarray_def
    3.54 +by (simp add: sublist'_all)
    3.55 +
    3.56 +lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
    3.57 +unfolding Heap.length_def subarray_def
    3.58 +by (simp add: nth_sublist')
    3.59 +
    3.60 +lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
    3.61 +unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    3.62 +
    3.63 +lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
    3.64 +unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
    3.65 +
    3.66 +lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
    3.67 +unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
    3.68 +
    3.69 +end
    3.70 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Mon Mar 23 19:01:17 2009 +0100
     4.3 @@ -0,0 +1,505 @@
     4.4 +(* $Id$ *)
     4.5 +
     4.6 +header {* Slices of lists *}
     4.7 +
     4.8 +theory Sublist
     4.9 +imports Multiset
    4.10 +begin
    4.11 +
    4.12 +
    4.13 +lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    4.14 +apply (induct xs arbitrary: i j k)
    4.15 +apply simp
    4.16 +apply (simp only: sublist_Cons)
    4.17 +apply simp
    4.18 +apply safe
    4.19 +apply simp
    4.20 +apply (erule_tac x="0" in meta_allE)
    4.21 +apply (erule_tac x="j - 1" in meta_allE)
    4.22 +apply (erule_tac x="k - 1" in meta_allE)
    4.23 +apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    4.24 +apply simp
    4.25 +apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
    4.26 +apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
    4.27 +apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
    4.28 +apply simp
    4.29 +apply fastsimp
    4.30 +apply fastsimp
    4.31 +apply fastsimp
    4.32 +apply fastsimp
    4.33 +apply (erule_tac x="i - 1" in meta_allE)
    4.34 +apply (erule_tac x="j - 1" in meta_allE)
    4.35 +apply (erule_tac x="k - 1" in meta_allE)
    4.36 +apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
    4.37 +apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
    4.38 +apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
    4.39 +apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    4.40 +apply simp
    4.41 +apply fastsimp
    4.42 +apply fastsimp
    4.43 +apply fastsimp
    4.44 +apply fastsimp
    4.45 +done
    4.46 +
    4.47 +lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
    4.48 +apply (induct xs arbitrary: i inds)
    4.49 +apply simp
    4.50 +apply (case_tac i)
    4.51 +apply (simp add: sublist_Cons)
    4.52 +apply (simp add: sublist_Cons)
    4.53 +done
    4.54 +
    4.55 +lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
    4.56 +proof (induct xs arbitrary: i inds)
    4.57 +  case Nil thus ?case by simp
    4.58 +next
    4.59 +  case (Cons x xs)
    4.60 +  thus ?case
    4.61 +  proof (cases i)
    4.62 +    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
    4.63 +  next
    4.64 +    case (Suc i')
    4.65 +    with Cons show ?thesis
    4.66 +      apply simp
    4.67 +      apply (simp add: sublist_Cons)
    4.68 +      apply auto
    4.69 +      apply (auto simp add: nat.split)
    4.70 +      apply (simp add: card_less_Suc[symmetric])
    4.71 +      apply (simp add: card_less_Suc2)
    4.72 +      done
    4.73 +  qed
    4.74 +qed
    4.75 +
    4.76 +lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
    4.77 +by (simp add: sublist_update1 sublist_update2)
    4.78 +
    4.79 +lemma sublist_take: "sublist xs {j. j < m} = take m xs"
    4.80 +apply (induct xs arbitrary: m)
    4.81 +apply simp
    4.82 +apply (case_tac m)
    4.83 +apply simp
    4.84 +apply (simp add: sublist_Cons)
    4.85 +done
    4.86 +
    4.87 +lemma sublist_take': "sublist xs {0..<m} = take m xs"
    4.88 +apply (induct xs arbitrary: m)
    4.89 +apply simp
    4.90 +apply (case_tac m)
    4.91 +apply simp
    4.92 +apply (simp add: sublist_Cons sublist_take)
    4.93 +done
    4.94 +
    4.95 +lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
    4.96 +apply (induct xs)
    4.97 +apply simp
    4.98 +apply (simp add: sublist_Cons)
    4.99 +done
   4.100 +
   4.101 +lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
   4.102 +apply (induct xs)
   4.103 +apply simp
   4.104 +apply (simp add: sublist_Cons)
   4.105 +done
   4.106 +
   4.107 +lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
   4.108 +apply (induct xs arbitrary: a)
   4.109 +apply simp
   4.110 +apply(case_tac aa)
   4.111 +apply simp
   4.112 +apply (simp add: sublist_Cons)
   4.113 +apply simp
   4.114 +apply (simp add: sublist_Cons)
   4.115 +done
   4.116 +
   4.117 +lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
   4.118 +apply (induct xs arbitrary: inds)
   4.119 +apply simp
   4.120 +apply (simp add: sublist_Cons)
   4.121 +apply auto
   4.122 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   4.123 +apply auto
   4.124 +done
   4.125 +
   4.126 +lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
   4.127 +apply (induct xs arbitrary: inds)
   4.128 +apply simp
   4.129 +apply (simp add: sublist_Cons)
   4.130 +apply (auto split: if_splits)
   4.131 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   4.132 +apply (case_tac x, auto)
   4.133 +done
   4.134 +
   4.135 +lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
   4.136 +apply (induct xs arbitrary: inds)
   4.137 +apply simp
   4.138 +apply (simp add: sublist_Cons)
   4.139 +apply auto
   4.140 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   4.141 +apply (case_tac x, auto)
   4.142 +done
   4.143 +
   4.144 +lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
   4.145 +apply (induct xs arbitrary: ys inds inds')
   4.146 +apply simp
   4.147 +apply (drule sym, rule sym)
   4.148 +apply (simp add: sublist_Nil, fastsimp)
   4.149 +apply (case_tac ys)
   4.150 +apply (simp add: sublist_Nil, fastsimp)
   4.151 +apply (auto simp add: sublist_Cons)
   4.152 +apply (erule_tac x="list" in meta_allE)
   4.153 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   4.154 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   4.155 +apply fastsimp
   4.156 +apply (erule_tac x="list" in meta_allE)
   4.157 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   4.158 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   4.159 +apply fastsimp
   4.160 +done
   4.161 +
   4.162 +lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
   4.163 +apply (induct xs arbitrary: ys inds)
   4.164 +apply simp
   4.165 +apply (rule sym, simp add: sublist_Nil)
   4.166 +apply (case_tac ys)
   4.167 +apply (simp add: sublist_Nil)
   4.168 +apply (auto simp add: sublist_Cons)
   4.169 +apply (erule_tac x="list" in meta_allE)
   4.170 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   4.171 +apply fastsimp
   4.172 +apply (erule_tac x="list" in meta_allE)
   4.173 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   4.174 +apply fastsimp
   4.175 +done
   4.176 +
   4.177 +lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
   4.178 +by (rule sublist_eq, auto)
   4.179 +
   4.180 +lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
   4.181 +apply (induct xs arbitrary: ys inds)
   4.182 +apply simp
   4.183 +apply (rule sym, simp add: sublist_Nil)
   4.184 +apply (case_tac ys)
   4.185 +apply (simp add: sublist_Nil)
   4.186 +apply (auto simp add: sublist_Cons)
   4.187 +apply (case_tac i)
   4.188 +apply auto
   4.189 +apply (case_tac i)
   4.190 +apply auto
   4.191 +done
   4.192 +
   4.193 +section {* Another sublist function *}
   4.194 +
   4.195 +function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   4.196 +where
   4.197 +  "sublist' n m [] = []"
   4.198 +| "sublist' n 0 xs = []"
   4.199 +| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
   4.200 +| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
   4.201 +by pat_completeness auto
   4.202 +termination by lexicographic_order
   4.203 +
   4.204 +subsection {* Proving equivalence to the other sublist command *}
   4.205 +
   4.206 +lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
   4.207 +apply (induct xs arbitrary: n m)
   4.208 +apply simp
   4.209 +apply (case_tac n)
   4.210 +apply (case_tac m)
   4.211 +apply simp
   4.212 +apply (simp add: sublist_Cons)
   4.213 +apply (case_tac m)
   4.214 +apply simp
   4.215 +apply (simp add: sublist_Cons)
   4.216 +done
   4.217 +
   4.218 +
   4.219 +lemma "sublist' n m xs = sublist xs {n..<m}"
   4.220 +apply (induct xs arbitrary: n m)
   4.221 +apply simp
   4.222 +apply (case_tac n, case_tac m)
   4.223 +apply simp
   4.224 +apply simp
   4.225 +apply (simp add: sublist_take')
   4.226 +apply (case_tac m)
   4.227 +apply simp
   4.228 +apply (simp add: sublist_Cons sublist'_sublist)
   4.229 +done
   4.230 +
   4.231 +
   4.232 +subsection {* Showing equivalence to use of drop and take for definition *}
   4.233 +
   4.234 +lemma "sublist' n m xs = take (m - n) (drop n xs)"
   4.235 +apply (induct xs arbitrary: n m)
   4.236 +apply simp
   4.237 +apply (case_tac m)
   4.238 +apply simp
   4.239 +apply (case_tac n)
   4.240 +apply simp
   4.241 +apply simp
   4.242 +done
   4.243 +
   4.244 +subsection {* General lemma about sublist *}
   4.245 +
   4.246 +lemma sublist'_Nil[simp]: "sublist' i j [] = []"
   4.247 +by simp
   4.248 +
   4.249 +lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow>  sublist' i' j xs)"
   4.250 +by (cases i) auto
   4.251 +
   4.252 +lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
   4.253 +apply (cases j)
   4.254 +apply auto
   4.255 +apply (cases i)
   4.256 +apply auto
   4.257 +done
   4.258 +
   4.259 +lemma sublist_n_0: "sublist' n 0 xs = []"
   4.260 +by (induct xs, auto)
   4.261 +
   4.262 +lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
   4.263 +apply (induct xs arbitrary: n m)
   4.264 +apply simp
   4.265 +apply (case_tac m)
   4.266 +apply simp
   4.267 +apply (case_tac n)
   4.268 +apply simp
   4.269 +apply simp
   4.270 +done
   4.271 +
   4.272 +lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
   4.273 +apply (induct xs arbitrary: n m)
   4.274 +apply simp
   4.275 +apply (case_tac m)
   4.276 +apply simp
   4.277 +apply (case_tac n)
   4.278 +apply simp
   4.279 +apply simp
   4.280 +done
   4.281 +
   4.282 +lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
   4.283 +apply (induct xs arbitrary: n m)
   4.284 +apply simp
   4.285 +apply (case_tac m)
   4.286 +apply simp
   4.287 +apply (case_tac n)
   4.288 +apply simp
   4.289 +apply simp
   4.290 +done
   4.291 +
   4.292 +lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
   4.293 +apply (induct xs arbitrary: n m)
   4.294 +apply simp
   4.295 +apply (case_tac m)
   4.296 +apply simp
   4.297 +apply (case_tac n)
   4.298 +apply simp
   4.299 +apply simp
   4.300 +done
   4.301 +
   4.302 +lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
   4.303 +apply (induct xs arbitrary: n)
   4.304 +apply simp
   4.305 +apply simp
   4.306 +apply (case_tac n)
   4.307 +apply (simp add: sublist_n_0)
   4.308 +apply simp
   4.309 +done
   4.310 +
   4.311 +lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   4.312 +apply (induct xs arbitrary: n m i)
   4.313 +apply simp
   4.314 +apply simp
   4.315 +apply (case_tac i)
   4.316 +apply simp
   4.317 +apply simp
   4.318 +done
   4.319 +
   4.320 +lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   4.321 +apply (induct xs arbitrary: n m i)
   4.322 +apply simp
   4.323 +apply simp
   4.324 +apply (case_tac i)
   4.325 +apply simp
   4.326 +apply simp
   4.327 +done
   4.328 +
   4.329 +lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
   4.330 +proof (induct xs arbitrary: n m i)
   4.331 +  case Nil thus ?case by auto
   4.332 +next
   4.333 +  case (Cons x xs)
   4.334 +  thus ?case
   4.335 +    apply -
   4.336 +    apply auto
   4.337 +    apply (cases i)
   4.338 +    apply auto
   4.339 +    apply (cases i)
   4.340 +    apply auto
   4.341 +    done
   4.342 +qed
   4.343 +
   4.344 +lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
   4.345 +proof (induct xs arbitrary: i j ys n m)
   4.346 +  case Nil
   4.347 +  thus ?case
   4.348 +    apply -
   4.349 +    apply (rule sym, drule sym)
   4.350 +    apply (simp add: sublist'_Nil)
   4.351 +    apply (simp add: sublist'_Nil3)
   4.352 +    apply arith
   4.353 +    done
   4.354 +next
   4.355 +  case (Cons x xs i j ys n m)
   4.356 +  note c = this
   4.357 +  thus ?case
   4.358 +  proof (cases m)
   4.359 +    case 0 thus ?thesis by (simp add: sublist_n_0)
   4.360 +  next
   4.361 +    case (Suc m')
   4.362 +    note a = this
   4.363 +    thus ?thesis
   4.364 +    proof (cases n)
   4.365 +      case 0 note b = this
   4.366 +      show ?thesis
   4.367 +      proof (cases ys)
   4.368 +	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
   4.369 +      next
   4.370 +	case (Cons y ys)
   4.371 +	show ?thesis
   4.372 +	proof (cases j)
   4.373 +	  case 0 with a b Cons.prems show ?thesis by simp
   4.374 +	next
   4.375 +	  case (Suc j') with a b Cons.prems Cons show ?thesis 
   4.376 +	    apply -
   4.377 +	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
   4.378 +	    done
   4.379 +	qed
   4.380 +      qed
   4.381 +    next
   4.382 +      case (Suc n')
   4.383 +      show ?thesis
   4.384 +      proof (cases ys)
   4.385 +	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
   4.386 +      next
   4.387 +	case (Cons y ys) with Suc a Cons.prems show ?thesis
   4.388 +	  apply -
   4.389 +	  apply simp
   4.390 +	  apply (cases j)
   4.391 +	  apply simp
   4.392 +	  apply (cases i)
   4.393 +	  apply simp
   4.394 +	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
   4.395 +	  apply simp
   4.396 +	  apply simp
   4.397 +	  apply simp
   4.398 +	  apply simp
   4.399 +	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
   4.400 +	  apply simp
   4.401 +	  apply simp
   4.402 +	  apply simp
   4.403 +	  done
   4.404 +      qed
   4.405 +    qed
   4.406 +  qed
   4.407 +qed
   4.408 +
   4.409 +lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
   4.410 +by (induct xs arbitrary: i j, auto)
   4.411 +
   4.412 +lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
   4.413 +apply (induct xs arbitrary: a i j)
   4.414 +apply simp
   4.415 +apply (case_tac j)
   4.416 +apply simp
   4.417 +apply (case_tac i)
   4.418 +apply simp
   4.419 +apply simp
   4.420 +done
   4.421 +
   4.422 +lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
   4.423 +apply (induct xs arbitrary: a i j)
   4.424 +apply simp
   4.425 +apply simp
   4.426 +apply (case_tac j)
   4.427 +apply simp
   4.428 +apply auto
   4.429 +apply (case_tac nat)
   4.430 +apply auto
   4.431 +done
   4.432 +
   4.433 +(* suffices that j \<le> length xs and length ys *) 
   4.434 +lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
   4.435 +proof (induct xs arbitrary: ys i j)
   4.436 +  case Nil thus ?case by simp
   4.437 +next
   4.438 +  case (Cons x xs)
   4.439 +  thus ?case
   4.440 +    apply -
   4.441 +    apply (cases ys)
   4.442 +    apply simp
   4.443 +    apply simp
   4.444 +    apply auto
   4.445 +    apply (case_tac i', auto)
   4.446 +    apply (erule_tac x="Suc i'" in allE, auto)
   4.447 +    apply (erule_tac x="i' - 1" in allE, auto)
   4.448 +    apply (case_tac i', auto)
   4.449 +    apply (erule_tac x="Suc i'" in allE, auto)
   4.450 +    done
   4.451 +qed
   4.452 +
   4.453 +lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
   4.454 +by (induct xs, auto)
   4.455 +
   4.456 +lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
   4.457 +by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
   4.458 +
   4.459 +lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
   4.460 +by (induct xs arbitrary: i j k) auto
   4.461 +
   4.462 +lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
   4.463 +apply (induct xs arbitrary: i j k)
   4.464 +apply auto
   4.465 +apply (case_tac k)
   4.466 +apply auto
   4.467 +apply (case_tac i)
   4.468 +apply auto
   4.469 +done
   4.470 +
   4.471 +lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
   4.472 +apply (simp add: sublist'_sublist)
   4.473 +apply (simp add: set_sublist)
   4.474 +apply auto
   4.475 +done
   4.476 +
   4.477 +lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   4.478 +unfolding set_sublist' by blast
   4.479 +
   4.480 +lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   4.481 +unfolding set_sublist' by blast
   4.482 +
   4.483 +
   4.484 +lemma multiset_of_sublist:
   4.485 +assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
   4.486 +assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
   4.487 +assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
   4.488 +assumes multiset: "multiset_of xs = multiset_of ys"
   4.489 +  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
   4.490 +proof -
   4.491 +  from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
   4.492 +    by (simp add: sublist'_append)
   4.493 +  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
   4.494 +  with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
   4.495 +    by (simp add: sublist'_append)
   4.496 +  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
   4.497 +  moreover
   4.498 +  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
   4.499 +    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   4.500 +  moreover
   4.501 +  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
   4.502 +    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   4.503 +  moreover
   4.504 +  ultimately show ?thesis by (simp add: multiset_of_append)
   4.505 +qed
   4.506 +
   4.507 +
   4.508 +end
     5.1 --- a/src/HOL/IsaMakefile	Mon Mar 23 19:01:17 2009 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Mon Mar 23 19:01:17 2009 +0100
     5.3 @@ -649,7 +649,11 @@
     5.4  $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
     5.5    Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
     5.6    Imperative_HOL/Relational.thy \
     5.7 -  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy
     5.8 +  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy \
     5.9 +  Imperative_HOL/Imperative_HOL_ex.thy \
    5.10 +  Imperative_HOL/ex/Imperative_Quicksort.thy \
    5.11 +  Imperative_HOL/ex/Subarray.thy \
    5.12 +  Imperative_HOL/ex/Sublist.thy
    5.13  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
    5.14  
    5.15  
    5.16 @@ -836,7 +840,7 @@
    5.17    ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy			\
    5.18    ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
    5.19    ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
    5.20 -  ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy			\
    5.21 +  ex/Hilbert_Classical.thy			\
    5.22    ex/Induction_Scheme.thy ex/InductiveInvariant.thy			\
    5.23    ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
    5.24    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
    5.25 @@ -845,8 +849,8 @@
    5.26    ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML	\
    5.27    ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
    5.28    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    5.29 -  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy		\
    5.30 -  ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
    5.31 +  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
    5.32 +  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
    5.33    ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
    5.34    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
    5.35    ex/Predicate_Compile.thy ex/predicate_compile.ML
     6.1 --- a/src/HOL/ex/ImperativeQuicksort.thy	Mon Mar 23 19:01:17 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,637 +0,0 @@
     6.4 -theory ImperativeQuicksort
     6.5 -imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
     6.6 -begin
     6.7 -
     6.8 -text {* We prove QuickSort correct in the Relational Calculus. *}
     6.9 -
    6.10 -definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
    6.11 -where
    6.12 -  "swap arr i j = (
    6.13 -     do
    6.14 -       x \<leftarrow> nth arr i;
    6.15 -       y \<leftarrow> nth arr j;
    6.16 -       upd i y arr;
    6.17 -       upd j x arr;
    6.18 -       return ()
    6.19 -     done)"
    6.20 -
    6.21 -lemma swap_permutes:
    6.22 -  assumes "crel (swap a i j) h h' rs"
    6.23 -  shows "multiset_of (get_array a h') 
    6.24 -  = multiset_of (get_array a h)"
    6.25 -  using assms
    6.26 -  unfolding swap_def
    6.27 -  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
    6.28 -
    6.29 -function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    6.30 -where
    6.31 -  "part1 a left right p = (
    6.32 -     if (right \<le> left) then return right
    6.33 -     else (do
    6.34 -       v \<leftarrow> nth a left;
    6.35 -       (if (v \<le> p) then (part1 a (left + 1) right p)
    6.36 -                    else (do swap a left right;
    6.37 -  part1 a left (right - 1) p done))
    6.38 -     done))"
    6.39 -by pat_completeness auto
    6.40 -
    6.41 -termination
    6.42 -by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
    6.43 -
    6.44 -declare part1.simps[simp del]
    6.45 -
    6.46 -lemma part_permutes:
    6.47 -  assumes "crel (part1 a l r p) h h' rs"
    6.48 -  shows "multiset_of (get_array a h') 
    6.49 -  = multiset_of (get_array a h)"
    6.50 -  using assms
    6.51 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    6.52 -  case (1 a l r p h h' rs)
    6.53 -  thus ?case
    6.54 -    unfolding part1.simps [of a l r p]
    6.55 -    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
    6.56 -qed
    6.57 -
    6.58 -lemma part_returns_index_in_bounds:
    6.59 -  assumes "crel (part1 a l r p) h h' rs"
    6.60 -  assumes "l \<le> r"
    6.61 -  shows "l \<le> rs \<and> rs \<le> r"
    6.62 -using assms
    6.63 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    6.64 -  case (1 a l r p h h' rs)
    6.65 -  note cr = `crel (part1 a l r p) h h' rs`
    6.66 -  show ?case
    6.67 -  proof (cases "r \<le> l")
    6.68 -    case True (* Terminating case *)
    6.69 -    with cr `l \<le> r` show ?thesis
    6.70 -      unfolding part1.simps[of a l r p]
    6.71 -      by (elim crelE crel_if crel_return crel_nth) auto
    6.72 -  next
    6.73 -    case False (* recursive case *)
    6.74 -    note rec_condition = this
    6.75 -    let ?v = "get_array a h ! l"
    6.76 -    show ?thesis
    6.77 -    proof (cases "?v \<le> p")
    6.78 -      case True
    6.79 -      with cr False
    6.80 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    6.81 -        unfolding part1.simps[of a l r p]
    6.82 -        by (elim crelE crel_nth crel_if crel_return) auto
    6.83 -      from rec_condition have "l + 1 \<le> r" by arith
    6.84 -      from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    6.85 -      show ?thesis by simp
    6.86 -    next
    6.87 -      case False
    6.88 -      with rec_condition cr
    6.89 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
    6.90 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    6.91 -        unfolding part1.simps[of a l r p]
    6.92 -        by (elim crelE crel_nth crel_if crel_return) auto
    6.93 -      from rec_condition have "l \<le> r - 1" by arith
    6.94 -      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    6.95 -    qed
    6.96 -  qed
    6.97 -qed
    6.98 -
    6.99 -lemma part_length_remains:
   6.100 -  assumes "crel (part1 a l r p) h h' rs"
   6.101 -  shows "Heap.length a h = Heap.length a h'"
   6.102 -using assms
   6.103 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   6.104 -  case (1 a l r p h h' rs)
   6.105 -  note cr = `crel (part1 a l r p) h h' rs`
   6.106 -  
   6.107 -  show ?case
   6.108 -  proof (cases "r \<le> l")
   6.109 -    case True (* Terminating case *)
   6.110 -    with cr show ?thesis
   6.111 -      unfolding part1.simps[of a l r p]
   6.112 -      by (elim crelE crel_if crel_return crel_nth) auto
   6.113 -  next
   6.114 -    case False (* recursive case *)
   6.115 -    with cr 1 show ?thesis
   6.116 -      unfolding part1.simps [of a l r p] swap_def
   6.117 -      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
   6.118 -  qed
   6.119 -qed
   6.120 -
   6.121 -lemma part_outer_remains:
   6.122 -  assumes "crel (part1 a l r p) h h' rs"
   6.123 -  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   6.124 -  using assms
   6.125 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   6.126 -  case (1 a l r p h h' rs)
   6.127 -  note cr = `crel (part1 a l r p) h h' rs`
   6.128 -  
   6.129 -  show ?case
   6.130 -  proof (cases "r \<le> l")
   6.131 -    case True (* Terminating case *)
   6.132 -    with cr show ?thesis
   6.133 -      unfolding part1.simps[of a l r p]
   6.134 -      by (elim crelE crel_if crel_return crel_nth) auto
   6.135 -  next
   6.136 -    case False (* recursive case *)
   6.137 -    note rec_condition = this
   6.138 -    let ?v = "get_array a h ! l"
   6.139 -    show ?thesis
   6.140 -    proof (cases "?v \<le> p")
   6.141 -      case True
   6.142 -      with cr False
   6.143 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   6.144 -        unfolding part1.simps[of a l r p]
   6.145 -        by (elim crelE crel_nth crel_if crel_return) auto
   6.146 -      from 1(1)[OF rec_condition True rec1]
   6.147 -      show ?thesis by fastsimp
   6.148 -    next
   6.149 -      case False
   6.150 -      with rec_condition cr
   6.151 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   6.152 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   6.153 -        unfolding part1.simps[of a l r p]
   6.154 -        by (elim crelE crel_nth crel_if crel_return) auto
   6.155 -      from swp rec_condition have
   6.156 -        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
   6.157 -	unfolding swap_def
   6.158 -	by (elim crelE crel_nth crel_upd crel_return) auto
   6.159 -      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   6.160 -    qed
   6.161 -  qed
   6.162 -qed
   6.163 -
   6.164 -
   6.165 -lemma part_partitions:
   6.166 -  assumes "crel (part1 a l r p) h h' rs"
   6.167 -  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
   6.168 -  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
   6.169 -  using assms
   6.170 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   6.171 -  case (1 a l r p h h' rs)
   6.172 -  note cr = `crel (part1 a l r p) h h' rs`
   6.173 -  
   6.174 -  show ?case
   6.175 -  proof (cases "r \<le> l")
   6.176 -    case True (* Terminating case *)
   6.177 -    with cr have "rs = r"
   6.178 -      unfolding part1.simps[of a l r p]
   6.179 -      by (elim crelE crel_if crel_return crel_nth) auto
   6.180 -    with True
   6.181 -    show ?thesis by auto
   6.182 -  next
   6.183 -    case False (* recursive case *)
   6.184 -    note lr = this
   6.185 -    let ?v = "get_array a h ! l"
   6.186 -    show ?thesis
   6.187 -    proof (cases "?v \<le> p")
   6.188 -      case True
   6.189 -      with lr cr
   6.190 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   6.191 -        unfolding part1.simps[of a l r p]
   6.192 -        by (elim crelE crel_nth crel_if crel_return) auto
   6.193 -      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
   6.194 -	by fastsimp
   6.195 -      have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
   6.196 -      with 1(1)[OF False True rec1] a_l show ?thesis
   6.197 -	by auto
   6.198 -    next
   6.199 -      case False
   6.200 -      with lr cr
   6.201 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   6.202 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   6.203 -        unfolding part1.simps[of a l r p]
   6.204 -        by (elim crelE crel_nth crel_if crel_return) auto
   6.205 -      from swp False have "get_array a h1 ! r \<ge> p"
   6.206 -	unfolding swap_def
   6.207 -	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
   6.208 -      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
   6.209 -	by fastsimp
   6.210 -      have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   6.211 -      with 1(2)[OF lr False rec2] a_r show ?thesis
   6.212 -	by auto
   6.213 -    qed
   6.214 -  qed
   6.215 -qed
   6.216 -
   6.217 -
   6.218 -fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
   6.219 -where
   6.220 -  "partition a left right = (do
   6.221 -     pivot \<leftarrow> nth a right;
   6.222 -     middle \<leftarrow> part1 a left (right - 1) pivot;
   6.223 -     v \<leftarrow> nth a middle;
   6.224 -     m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
   6.225 -     swap a m right;
   6.226 -     return m
   6.227 -   done)"
   6.228 -
   6.229 -declare partition.simps[simp del]
   6.230 -
   6.231 -lemma partition_permutes:
   6.232 -  assumes "crel (partition a l r) h h' rs"
   6.233 -  shows "multiset_of (get_array a h') 
   6.234 -  = multiset_of (get_array a h)"
   6.235 -proof -
   6.236 -    from assms part_permutes swap_permutes show ?thesis
   6.237 -      unfolding partition.simps
   6.238 -      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   6.239 -qed
   6.240 -
   6.241 -lemma partition_length_remains:
   6.242 -  assumes "crel (partition a l r) h h' rs"
   6.243 -  shows "Heap.length a h = Heap.length a h'"
   6.244 -proof -
   6.245 -  from assms part_length_remains show ?thesis
   6.246 -    unfolding partition.simps swap_def
   6.247 -    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   6.248 -qed
   6.249 -
   6.250 -lemma partition_outer_remains:
   6.251 -  assumes "crel (partition a l r) h h' rs"
   6.252 -  assumes "l < r"
   6.253 -  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   6.254 -proof -
   6.255 -  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   6.256 -    unfolding partition.simps swap_def
   6.257 -    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
   6.258 -qed
   6.259 -
   6.260 -lemma partition_returns_index_in_bounds:
   6.261 -  assumes crel: "crel (partition a l r) h h' rs"
   6.262 -  assumes "l < r"
   6.263 -  shows "l \<le> rs \<and> rs \<le> r"
   6.264 -proof -
   6.265 -  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   6.266 -    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
   6.267 -         else middle)"
   6.268 -    unfolding partition.simps
   6.269 -    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   6.270 -  from `l < r` have "l \<le> r - 1" by arith
   6.271 -  from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   6.272 -qed
   6.273 -
   6.274 -lemma partition_partitions:
   6.275 -  assumes crel: "crel (partition a l r) h h' rs"
   6.276 -  assumes "l < r"
   6.277 -  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
   6.278 -  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
   6.279 -proof -
   6.280 -  let ?pivot = "get_array a h ! r" 
   6.281 -  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
   6.282 -    and swap: "crel (swap a rs r) h1 h' ()"
   6.283 -    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
   6.284 -         else middle)"
   6.285 -    unfolding partition.simps
   6.286 -    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   6.287 -  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
   6.288 -    (Heap.upd a rs (get_array a h1 ! r) h1)"
   6.289 -    unfolding swap_def
   6.290 -    by (elim crelE crel_return crel_nth crel_upd) simp
   6.291 -  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
   6.292 -    unfolding swap_def
   6.293 -    by (elim crelE crel_return crel_nth crel_upd) simp
   6.294 -  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
   6.295 -    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   6.296 -  from `l < r` have "l \<le> r - 1" by simp 
   6.297 -  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   6.298 -  from part_outer_remains[OF part] `l < r`
   6.299 -  have "get_array a h ! r = get_array a h1 ! r"
   6.300 -    by fastsimp
   6.301 -  with swap
   6.302 -  have right_remains: "get_array a h ! r = get_array a h' ! rs"
   6.303 -    unfolding swap_def
   6.304 -    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   6.305 -  from part_partitions [OF part]
   6.306 -  show ?thesis
   6.307 -  proof (cases "get_array a h1 ! middle \<le> ?pivot")
   6.308 -    case True
   6.309 -    with rs_equals have rs_equals: "rs = middle + 1" by simp
   6.310 -    { 
   6.311 -      fix i
   6.312 -      assume i_is_left: "l \<le> i \<and> i < rs"
   6.313 -      with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
   6.314 -      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   6.315 -      from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
   6.316 -      with part_partitions[OF part] right_remains True
   6.317 -      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   6.318 -      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
   6.319 -	unfolding Heap.upd_def Heap.length_def by simp
   6.320 -    }
   6.321 -    moreover
   6.322 -    {
   6.323 -      fix i
   6.324 -      assume "rs < i \<and> i \<le> r"
   6.325 -
   6.326 -      hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
   6.327 -      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   6.328 -      proof
   6.329 -	assume i_is: "rs < i \<and> i \<le> r - 1"
   6.330 -	with swap_length_remains in_bounds middle_in_bounds rs_equals
   6.331 -	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   6.332 -	from part_partitions[OF part] rs_equals right_remains i_is
   6.333 -	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   6.334 -	  by fastsimp
   6.335 -	with i_props h'_def show ?thesis by fastsimp
   6.336 -      next
   6.337 -	assume i_is: "rs < i \<and> i = r"
   6.338 -	with rs_equals have "Suc middle \<noteq> r" by arith
   6.339 -	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
   6.340 -	with part_partitions[OF part] right_remains 
   6.341 -	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
   6.342 -	  by fastsimp
   6.343 -	with i_is True rs_equals right_remains h'_def
   6.344 -	show ?thesis using in_bounds
   6.345 -	  unfolding Heap.upd_def Heap.length_def
   6.346 -	  by auto
   6.347 -      qed
   6.348 -    }
   6.349 -    ultimately show ?thesis by auto
   6.350 -  next
   6.351 -    case False
   6.352 -    with rs_equals have rs_equals: "middle = rs" by simp
   6.353 -    { 
   6.354 -      fix i
   6.355 -      assume i_is_left: "l \<le> i \<and> i < rs"
   6.356 -      with swap_length_remains in_bounds middle_in_bounds rs_equals
   6.357 -      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   6.358 -      from part_partitions[OF part] rs_equals right_remains i_is_left
   6.359 -      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   6.360 -      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
   6.361 -	unfolding Heap.upd_def by simp
   6.362 -    }
   6.363 -    moreover
   6.364 -    {
   6.365 -      fix i
   6.366 -      assume "rs < i \<and> i \<le> r"
   6.367 -      hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
   6.368 -      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   6.369 -      proof
   6.370 -	assume i_is: "rs < i \<and> i \<le> r - 1"
   6.371 -	with swap_length_remains in_bounds middle_in_bounds rs_equals
   6.372 -	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   6.373 -	from part_partitions[OF part] rs_equals right_remains i_is
   6.374 -	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   6.375 -	  by fastsimp
   6.376 -	with i_props h'_def show ?thesis by fastsimp
   6.377 -      next
   6.378 -	assume i_is: "i = r"
   6.379 -	from i_is False rs_equals right_remains h'_def
   6.380 -	show ?thesis using in_bounds
   6.381 -	  unfolding Heap.upd_def Heap.length_def
   6.382 -	  by auto
   6.383 -      qed
   6.384 -    }
   6.385 -    ultimately
   6.386 -    show ?thesis by auto
   6.387 -  qed
   6.388 -qed
   6.389 -
   6.390 -
   6.391 -function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
   6.392 -where
   6.393 -  "quicksort arr left right =
   6.394 -     (if (right > left)  then
   6.395 -        do
   6.396 -          pivotNewIndex \<leftarrow> partition arr left right;
   6.397 -          pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
   6.398 -          quicksort arr left (pivotNewIndex - 1);
   6.399 -          quicksort arr (pivotNewIndex + 1) right
   6.400 -        done
   6.401 -     else return ())"
   6.402 -by pat_completeness auto
   6.403 -
   6.404 -(* For termination, we must show that the pivotNewIndex is between left and right *) 
   6.405 -termination
   6.406 -by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
   6.407 -
   6.408 -declare quicksort.simps[simp del]
   6.409 -
   6.410 -
   6.411 -lemma quicksort_permutes:
   6.412 -  assumes "crel (quicksort a l r) h h' rs"
   6.413 -  shows "multiset_of (get_array a h') 
   6.414 -  = multiset_of (get_array a h)"
   6.415 -  using assms
   6.416 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   6.417 -  case (1 a l r h h' rs)
   6.418 -  with partition_permutes show ?case
   6.419 -    unfolding quicksort.simps [of a l r]
   6.420 -    by (elim crel_if crelE crel_assert crel_return) auto
   6.421 -qed
   6.422 -
   6.423 -lemma length_remains:
   6.424 -  assumes "crel (quicksort a l r) h h' rs"
   6.425 -  shows "Heap.length a h = Heap.length a h'"
   6.426 -using assms
   6.427 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   6.428 -  case (1 a l r h h' rs)
   6.429 -  with partition_length_remains show ?case
   6.430 -    unfolding quicksort.simps [of a l r]
   6.431 -    by (elim crel_if crelE crel_assert crel_return) auto
   6.432 -qed
   6.433 -
   6.434 -lemma quicksort_outer_remains:
   6.435 -  assumes "crel (quicksort a l r) h h' rs"
   6.436 -   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   6.437 -  using assms
   6.438 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   6.439 -  case (1 a l r h h' rs)
   6.440 -  note cr = `crel (quicksort a l r) h h' rs`
   6.441 -  thus ?case
   6.442 -  proof (cases "r > l")
   6.443 -    case False
   6.444 -    with cr have "h' = h"
   6.445 -      unfolding quicksort.simps [of a l r]
   6.446 -      by (elim crel_if crel_return) auto
   6.447 -    thus ?thesis by simp
   6.448 -  next
   6.449 -  case True
   6.450 -   { 
   6.451 -      fix h1 h2 p ret1 ret2 i
   6.452 -      assume part: "crel (partition a l r) h h1 p"
   6.453 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
   6.454 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
   6.455 -      assume pivot: "l \<le> p \<and> p \<le> r"
   6.456 -      assume i_outer: "i < l \<or> r < i"
   6.457 -      from  partition_outer_remains [OF part True] i_outer
   6.458 -      have "get_array a h !i = get_array a h1 ! i" by fastsimp
   6.459 -      moreover
   6.460 -      with 1(1) [OF True pivot qs1] pivot i_outer
   6.461 -      have "get_array a h1 ! i = get_array a h2 ! i" by auto
   6.462 -      moreover
   6.463 -      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
   6.464 -      have "get_array a h2 ! i = get_array a h' ! i" by auto
   6.465 -      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
   6.466 -    }
   6.467 -    with cr show ?thesis
   6.468 -      unfolding quicksort.simps [of a l r]
   6.469 -      by (elim crel_if crelE crel_assert crel_return) auto
   6.470 -  qed
   6.471 -qed
   6.472 -
   6.473 -lemma quicksort_is_skip:
   6.474 -  assumes "crel (quicksort a l r) h h' rs"
   6.475 -  shows "r \<le> l \<longrightarrow> h = h'"
   6.476 -  using assms
   6.477 -  unfolding quicksort.simps [of a l r]
   6.478 -  by (elim crel_if crel_return) auto
   6.479 - 
   6.480 -lemma quicksort_sorts:
   6.481 -  assumes "crel (quicksort a l r) h h' rs"
   6.482 -  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
   6.483 -  shows "sorted (subarray l (r + 1) a h')"
   6.484 -  using assms
   6.485 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   6.486 -  case (1 a l r h h' rs)
   6.487 -  note cr = `crel (quicksort a l r) h h' rs`
   6.488 -  thus ?case
   6.489 -  proof (cases "r > l")
   6.490 -    case False
   6.491 -    hence "l \<ge> r + 1 \<or> l = r" by arith 
   6.492 -    with length_remains[OF cr] 1(5) show ?thesis
   6.493 -      by (auto simp add: subarray_Nil subarray_single)
   6.494 -  next
   6.495 -    case True
   6.496 -    { 
   6.497 -      fix h1 h2 p
   6.498 -      assume part: "crel (partition a l r) h h1 p"
   6.499 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
   6.500 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
   6.501 -      from partition_returns_index_in_bounds [OF part True]
   6.502 -      have pivot: "l\<le> p \<and> p \<le> r" .
   6.503 -     note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
   6.504 -      from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
   6.505 -      have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
   6.506 -        (*-- First of all, by induction hypothesis both sublists are sorted. *)
   6.507 -      from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
   6.508 -      have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
   6.509 -      from quicksort_outer_remains [OF qs2] length_remains
   6.510 -      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
   6.511 -	by (simp add: subarray_eq_samelength_iff)
   6.512 -      with IH1 have IH1': "sorted (subarray l p a h')" by simp
   6.513 -      from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
   6.514 -      have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
   6.515 -        by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
   6.516 -           (* -- Secondly, both sublists remain partitioned. *)
   6.517 -      from partition_partitions[OF part True]
   6.518 -      have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
   6.519 -        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
   6.520 -        by (auto simp add: all_in_set_subarray_conv)
   6.521 -      from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
   6.522 -        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
   6.523 -      have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
   6.524 -	unfolding Heap.length_def subarray_def by (cases p, auto)
   6.525 -      with left_subarray_remains part_conds1 pivot_unchanged
   6.526 -      have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
   6.527 -        by (simp, subst set_of_multiset_of[symmetric], simp)
   6.528 -          (* -- These steps are the analogous for the right sublist \<dots> *)
   6.529 -      from quicksort_outer_remains [OF qs1] length_remains
   6.530 -      have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
   6.531 -	by (auto simp add: subarray_eq_samelength_iff)
   6.532 -      from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
   6.533 -        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
   6.534 -      have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
   6.535 -        unfolding Heap.length_def subarray_def by auto
   6.536 -      with right_subarray_remains part_conds2 pivot_unchanged
   6.537 -      have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
   6.538 -        by (simp, subst set_of_multiset_of[symmetric], simp)
   6.539 -          (* -- Thirdly and finally, we show that the array is sorted
   6.540 -          following from the facts above. *)
   6.541 -      from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [get_array a h' ! p] @ subarray (p + 1) (r + 1) a h'"
   6.542 -	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
   6.543 -      with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
   6.544 -	unfolding subarray_def
   6.545 -	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
   6.546 -	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   6.547 -    }
   6.548 -    with True cr show ?thesis
   6.549 -      unfolding quicksort.simps [of a l r]
   6.550 -      by (elim crel_if crel_return crelE crel_assert) auto
   6.551 -  qed
   6.552 -qed
   6.553 -
   6.554 -
   6.555 -lemma quicksort_is_sort:
   6.556 -  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
   6.557 -  shows "get_array a h' = sort (get_array a h)"
   6.558 -proof (cases "get_array a h = []")
   6.559 -  case True
   6.560 -  with quicksort_is_skip[OF crel] show ?thesis
   6.561 -  unfolding Heap.length_def by simp
   6.562 -next
   6.563 -  case False
   6.564 -  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
   6.565 -    unfolding Heap.length_def subarray_def by auto
   6.566 -  with length_remains[OF crel] have "sorted (get_array a h')"
   6.567 -    unfolding Heap.length_def by simp
   6.568 -  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
   6.569 -qed
   6.570 -
   6.571 -subsection {* No Errors in quicksort *}
   6.572 -text {* We have proved that quicksort sorts (if no exceptions occur).
   6.573 -We will now show that exceptions do not occur. *}
   6.574 -
   6.575 -lemma noError_part1: 
   6.576 -  assumes "l < Heap.length a h" "r < Heap.length a h"
   6.577 -  shows "noError (part1 a l r p) h"
   6.578 -  using assms
   6.579 -proof (induct a l r p arbitrary: h rule: part1.induct)
   6.580 -  case (1 a l r p)
   6.581 -  thus ?case
   6.582 -    unfolding part1.simps [of a l r] swap_def
   6.583 -    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
   6.584 -qed
   6.585 -
   6.586 -lemma noError_partition:
   6.587 -  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
   6.588 -  shows "noError (partition a l r) h"
   6.589 -using assms
   6.590 -unfolding partition.simps swap_def
   6.591 -apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
   6.592 -apply (frule part_length_remains)
   6.593 -apply (frule part_returns_index_in_bounds)
   6.594 -apply auto
   6.595 -apply (frule part_length_remains)
   6.596 -apply (frule part_returns_index_in_bounds)
   6.597 -apply auto
   6.598 -apply (frule part_length_remains)
   6.599 -apply auto
   6.600 -done
   6.601 -
   6.602 -lemma noError_quicksort:
   6.603 -  assumes "l < Heap.length a h" "r < Heap.length a h"
   6.604 -  shows "noError (quicksort a l r) h"
   6.605 -using assms
   6.606 -proof (induct a l r arbitrary: h rule: quicksort.induct)
   6.607 -  case (1 a l ri h)
   6.608 -  thus ?case
   6.609 -    unfolding quicksort.simps [of a l ri]
   6.610 -    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
   6.611 -    apply (frule partition_returns_index_in_bounds)
   6.612 -    apply auto
   6.613 -    apply (frule partition_returns_index_in_bounds)
   6.614 -    apply auto
   6.615 -    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
   6.616 -    apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   6.617 -    apply (erule disjE)
   6.618 -    apply auto
   6.619 -    unfolding quicksort.simps [of a "Suc ri" ri]
   6.620 -    apply (auto intro!: noError_if noError_return)
   6.621 -    done
   6.622 -qed
   6.623 -
   6.624 -
   6.625 -subsection {* Example *}
   6.626 -
   6.627 -definition "qsort a = do
   6.628 -    k \<leftarrow> length a;
   6.629 -    quicksort a 0 (k - 1);
   6.630 -    return a
   6.631 -  done"
   6.632 -
   6.633 -ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
   6.634 -
   6.635 -export_code qsort in SML_imp module_name QSort
   6.636 -export_code qsort in OCaml module_name QSort file -
   6.637 -export_code qsort in OCaml_imp module_name QSort file -
   6.638 -export_code qsort in Haskell module_name QSort file -
   6.639 -
   6.640 -end
   6.641 \ No newline at end of file
     7.1 --- a/src/HOL/ex/ROOT.ML	Mon Mar 23 19:01:17 2009 +0100
     7.2 +++ b/src/HOL/ex/ROOT.ML	Mon Mar 23 19:01:17 2009 +0100
     7.3 @@ -21,7 +21,6 @@
     7.4  
     7.5  use_thys [
     7.6    "Numeral",
     7.7 -  "ImperativeQuicksort",
     7.8    "Higher_Order_Logic",
     7.9    "Abstract_NAT",
    7.10    "Guess",
     8.1 --- a/src/HOL/ex/Subarray.thy	Mon Mar 23 19:01:17 2009 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,66 +0,0 @@
     8.4 -theory Subarray
     8.5 -imports Array Sublist
     8.6 -begin
     8.7 -
     8.8 -definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
     8.9 -where
    8.10 -  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
    8.11 -
    8.12 -lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    8.13 -apply (simp add: subarray_def Heap.upd_def)
    8.14 -apply (simp add: sublist'_update1)
    8.15 -done
    8.16 -
    8.17 -lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    8.18 -apply (simp add: subarray_def Heap.upd_def)
    8.19 -apply (subst sublist'_update2)
    8.20 -apply fastsimp
    8.21 -apply simp
    8.22 -done
    8.23 -
    8.24 -lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
    8.25 -unfolding subarray_def Heap.upd_def
    8.26 -by (simp add: sublist'_update3)
    8.27 -
    8.28 -lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
    8.29 -by (simp add: subarray_def sublist'_Nil')
    8.30 -
    8.31 -lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
    8.32 -by (simp add: subarray_def Heap.length_def sublist'_single)
    8.33 -
    8.34 -lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
    8.35 -by (simp add: subarray_def Heap.length_def length_sublist')
    8.36 -
    8.37 -lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
    8.38 -by (simp add: length_subarray)
    8.39 -
    8.40 -lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
    8.41 -unfolding Heap.length_def subarray_def
    8.42 -by (simp add: sublist'_front)
    8.43 -
    8.44 -lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
    8.45 -unfolding Heap.length_def subarray_def
    8.46 -by (simp add: sublist'_back)
    8.47 -
    8.48 -lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
    8.49 -unfolding subarray_def
    8.50 -by (simp add: sublist'_append)
    8.51 -
    8.52 -lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
    8.53 -unfolding Heap.length_def subarray_def
    8.54 -by (simp add: sublist'_all)
    8.55 -
    8.56 -lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
    8.57 -unfolding Heap.length_def subarray_def
    8.58 -by (simp add: nth_sublist')
    8.59 -
    8.60 -lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
    8.61 -unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    8.62 -
    8.63 -lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
    8.64 -unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
    8.65 -
    8.66 -lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
    8.67 -unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
    8.68 -
    8.69 -end
    8.70 \ No newline at end of file
     9.1 --- a/src/HOL/ex/Sublist.thy	Mon Mar 23 19:01:17 2009 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,505 +0,0 @@
     9.4 -(* $Id$ *)
     9.5 -
     9.6 -header {* Slices of lists *}
     9.7 -
     9.8 -theory Sublist
     9.9 -imports Multiset
    9.10 -begin
    9.11 -
    9.12 -
    9.13 -lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    9.14 -apply (induct xs arbitrary: i j k)
    9.15 -apply simp
    9.16 -apply (simp only: sublist_Cons)
    9.17 -apply simp
    9.18 -apply safe
    9.19 -apply simp
    9.20 -apply (erule_tac x="0" in meta_allE)
    9.21 -apply (erule_tac x="j - 1" in meta_allE)
    9.22 -apply (erule_tac x="k - 1" in meta_allE)
    9.23 -apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    9.24 -apply simp
    9.25 -apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
    9.26 -apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
    9.27 -apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
    9.28 -apply simp
    9.29 -apply fastsimp
    9.30 -apply fastsimp
    9.31 -apply fastsimp
    9.32 -apply fastsimp
    9.33 -apply (erule_tac x="i - 1" in meta_allE)
    9.34 -apply (erule_tac x="j - 1" in meta_allE)
    9.35 -apply (erule_tac x="k - 1" in meta_allE)
    9.36 -apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
    9.37 -apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
    9.38 -apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
    9.39 -apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    9.40 -apply simp
    9.41 -apply fastsimp
    9.42 -apply fastsimp
    9.43 -apply fastsimp
    9.44 -apply fastsimp
    9.45 -done
    9.46 -
    9.47 -lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
    9.48 -apply (induct xs arbitrary: i inds)
    9.49 -apply simp
    9.50 -apply (case_tac i)
    9.51 -apply (simp add: sublist_Cons)
    9.52 -apply (simp add: sublist_Cons)
    9.53 -done
    9.54 -
    9.55 -lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
    9.56 -proof (induct xs arbitrary: i inds)
    9.57 -  case Nil thus ?case by simp
    9.58 -next
    9.59 -  case (Cons x xs)
    9.60 -  thus ?case
    9.61 -  proof (cases i)
    9.62 -    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
    9.63 -  next
    9.64 -    case (Suc i')
    9.65 -    with Cons show ?thesis
    9.66 -      apply simp
    9.67 -      apply (simp add: sublist_Cons)
    9.68 -      apply auto
    9.69 -      apply (auto simp add: nat.split)
    9.70 -      apply (simp add: card_less_Suc[symmetric])
    9.71 -      apply (simp add: card_less_Suc2)
    9.72 -      done
    9.73 -  qed
    9.74 -qed
    9.75 -
    9.76 -lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
    9.77 -by (simp add: sublist_update1 sublist_update2)
    9.78 -
    9.79 -lemma sublist_take: "sublist xs {j. j < m} = take m xs"
    9.80 -apply (induct xs arbitrary: m)
    9.81 -apply simp
    9.82 -apply (case_tac m)
    9.83 -apply simp
    9.84 -apply (simp add: sublist_Cons)
    9.85 -done
    9.86 -
    9.87 -lemma sublist_take': "sublist xs {0..<m} = take m xs"
    9.88 -apply (induct xs arbitrary: m)
    9.89 -apply simp
    9.90 -apply (case_tac m)
    9.91 -apply simp
    9.92 -apply (simp add: sublist_Cons sublist_take)
    9.93 -done
    9.94 -
    9.95 -lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
    9.96 -apply (induct xs)
    9.97 -apply simp
    9.98 -apply (simp add: sublist_Cons)
    9.99 -done
   9.100 -
   9.101 -lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
   9.102 -apply (induct xs)
   9.103 -apply simp
   9.104 -apply (simp add: sublist_Cons)
   9.105 -done
   9.106 -
   9.107 -lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
   9.108 -apply (induct xs arbitrary: a)
   9.109 -apply simp
   9.110 -apply(case_tac aa)
   9.111 -apply simp
   9.112 -apply (simp add: sublist_Cons)
   9.113 -apply simp
   9.114 -apply (simp add: sublist_Cons)
   9.115 -done
   9.116 -
   9.117 -lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
   9.118 -apply (induct xs arbitrary: inds)
   9.119 -apply simp
   9.120 -apply (simp add: sublist_Cons)
   9.121 -apply auto
   9.122 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   9.123 -apply auto
   9.124 -done
   9.125 -
   9.126 -lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
   9.127 -apply (induct xs arbitrary: inds)
   9.128 -apply simp
   9.129 -apply (simp add: sublist_Cons)
   9.130 -apply (auto split: if_splits)
   9.131 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   9.132 -apply (case_tac x, auto)
   9.133 -done
   9.134 -
   9.135 -lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
   9.136 -apply (induct xs arbitrary: inds)
   9.137 -apply simp
   9.138 -apply (simp add: sublist_Cons)
   9.139 -apply auto
   9.140 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   9.141 -apply (case_tac x, auto)
   9.142 -done
   9.143 -
   9.144 -lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
   9.145 -apply (induct xs arbitrary: ys inds inds')
   9.146 -apply simp
   9.147 -apply (drule sym, rule sym)
   9.148 -apply (simp add: sublist_Nil, fastsimp)
   9.149 -apply (case_tac ys)
   9.150 -apply (simp add: sublist_Nil, fastsimp)
   9.151 -apply (auto simp add: sublist_Cons)
   9.152 -apply (erule_tac x="list" in meta_allE)
   9.153 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   9.154 -apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   9.155 -apply fastsimp
   9.156 -apply (erule_tac x="list" in meta_allE)
   9.157 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   9.158 -apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   9.159 -apply fastsimp
   9.160 -done
   9.161 -
   9.162 -lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
   9.163 -apply (induct xs arbitrary: ys inds)
   9.164 -apply simp
   9.165 -apply (rule sym, simp add: sublist_Nil)
   9.166 -apply (case_tac ys)
   9.167 -apply (simp add: sublist_Nil)
   9.168 -apply (auto simp add: sublist_Cons)
   9.169 -apply (erule_tac x="list" in meta_allE)
   9.170 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   9.171 -apply fastsimp
   9.172 -apply (erule_tac x="list" in meta_allE)
   9.173 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   9.174 -apply fastsimp
   9.175 -done
   9.176 -
   9.177 -lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
   9.178 -by (rule sublist_eq, auto)
   9.179 -
   9.180 -lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
   9.181 -apply (induct xs arbitrary: ys inds)
   9.182 -apply simp
   9.183 -apply (rule sym, simp add: sublist_Nil)
   9.184 -apply (case_tac ys)
   9.185 -apply (simp add: sublist_Nil)
   9.186 -apply (auto simp add: sublist_Cons)
   9.187 -apply (case_tac i)
   9.188 -apply auto
   9.189 -apply (case_tac i)
   9.190 -apply auto
   9.191 -done
   9.192 -
   9.193 -section {* Another sublist function *}
   9.194 -
   9.195 -function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   9.196 -where
   9.197 -  "sublist' n m [] = []"
   9.198 -| "sublist' n 0 xs = []"
   9.199 -| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
   9.200 -| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
   9.201 -by pat_completeness auto
   9.202 -termination by lexicographic_order
   9.203 -
   9.204 -subsection {* Proving equivalence to the other sublist command *}
   9.205 -
   9.206 -lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
   9.207 -apply (induct xs arbitrary: n m)
   9.208 -apply simp
   9.209 -apply (case_tac n)
   9.210 -apply (case_tac m)
   9.211 -apply simp
   9.212 -apply (simp add: sublist_Cons)
   9.213 -apply (case_tac m)
   9.214 -apply simp
   9.215 -apply (simp add: sublist_Cons)
   9.216 -done
   9.217 -
   9.218 -
   9.219 -lemma "sublist' n m xs = sublist xs {n..<m}"
   9.220 -apply (induct xs arbitrary: n m)
   9.221 -apply simp
   9.222 -apply (case_tac n, case_tac m)
   9.223 -apply simp
   9.224 -apply simp
   9.225 -apply (simp add: sublist_take')
   9.226 -apply (case_tac m)
   9.227 -apply simp
   9.228 -apply (simp add: sublist_Cons sublist'_sublist)
   9.229 -done
   9.230 -
   9.231 -
   9.232 -subsection {* Showing equivalence to use of drop and take for definition *}
   9.233 -
   9.234 -lemma "sublist' n m xs = take (m - n) (drop n xs)"
   9.235 -apply (induct xs arbitrary: n m)
   9.236 -apply simp
   9.237 -apply (case_tac m)
   9.238 -apply simp
   9.239 -apply (case_tac n)
   9.240 -apply simp
   9.241 -apply simp
   9.242 -done
   9.243 -
   9.244 -subsection {* General lemma about sublist *}
   9.245 -
   9.246 -lemma sublist'_Nil[simp]: "sublist' i j [] = []"
   9.247 -by simp
   9.248 -
   9.249 -lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow>  sublist' i' j xs)"
   9.250 -by (cases i) auto
   9.251 -
   9.252 -lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
   9.253 -apply (cases j)
   9.254 -apply auto
   9.255 -apply (cases i)
   9.256 -apply auto
   9.257 -done
   9.258 -
   9.259 -lemma sublist_n_0: "sublist' n 0 xs = []"
   9.260 -by (induct xs, auto)
   9.261 -
   9.262 -lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
   9.263 -apply (induct xs arbitrary: n m)
   9.264 -apply simp
   9.265 -apply (case_tac m)
   9.266 -apply simp
   9.267 -apply (case_tac n)
   9.268 -apply simp
   9.269 -apply simp
   9.270 -done
   9.271 -
   9.272 -lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
   9.273 -apply (induct xs arbitrary: n m)
   9.274 -apply simp
   9.275 -apply (case_tac m)
   9.276 -apply simp
   9.277 -apply (case_tac n)
   9.278 -apply simp
   9.279 -apply simp
   9.280 -done
   9.281 -
   9.282 -lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
   9.283 -apply (induct xs arbitrary: n m)
   9.284 -apply simp
   9.285 -apply (case_tac m)
   9.286 -apply simp
   9.287 -apply (case_tac n)
   9.288 -apply simp
   9.289 -apply simp
   9.290 -done
   9.291 -
   9.292 -lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
   9.293 -apply (induct xs arbitrary: n m)
   9.294 -apply simp
   9.295 -apply (case_tac m)
   9.296 -apply simp
   9.297 -apply (case_tac n)
   9.298 -apply simp
   9.299 -apply simp
   9.300 -done
   9.301 -
   9.302 -lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
   9.303 -apply (induct xs arbitrary: n)
   9.304 -apply simp
   9.305 -apply simp
   9.306 -apply (case_tac n)
   9.307 -apply (simp add: sublist_n_0)
   9.308 -apply simp
   9.309 -done
   9.310 -
   9.311 -lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   9.312 -apply (induct xs arbitrary: n m i)
   9.313 -apply simp
   9.314 -apply simp
   9.315 -apply (case_tac i)
   9.316 -apply simp
   9.317 -apply simp
   9.318 -done
   9.319 -
   9.320 -lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   9.321 -apply (induct xs arbitrary: n m i)
   9.322 -apply simp
   9.323 -apply simp
   9.324 -apply (case_tac i)
   9.325 -apply simp
   9.326 -apply simp
   9.327 -done
   9.328 -
   9.329 -lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
   9.330 -proof (induct xs arbitrary: n m i)
   9.331 -  case Nil thus ?case by auto
   9.332 -next
   9.333 -  case (Cons x xs)
   9.334 -  thus ?case
   9.335 -    apply -
   9.336 -    apply auto
   9.337 -    apply (cases i)
   9.338 -    apply auto
   9.339 -    apply (cases i)
   9.340 -    apply auto
   9.341 -    done
   9.342 -qed
   9.343 -
   9.344 -lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
   9.345 -proof (induct xs arbitrary: i j ys n m)
   9.346 -  case Nil
   9.347 -  thus ?case
   9.348 -    apply -
   9.349 -    apply (rule sym, drule sym)
   9.350 -    apply (simp add: sublist'_Nil)
   9.351 -    apply (simp add: sublist'_Nil3)
   9.352 -    apply arith
   9.353 -    done
   9.354 -next
   9.355 -  case (Cons x xs i j ys n m)
   9.356 -  note c = this
   9.357 -  thus ?case
   9.358 -  proof (cases m)
   9.359 -    case 0 thus ?thesis by (simp add: sublist_n_0)
   9.360 -  next
   9.361 -    case (Suc m')
   9.362 -    note a = this
   9.363 -    thus ?thesis
   9.364 -    proof (cases n)
   9.365 -      case 0 note b = this
   9.366 -      show ?thesis
   9.367 -      proof (cases ys)
   9.368 -	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
   9.369 -      next
   9.370 -	case (Cons y ys)
   9.371 -	show ?thesis
   9.372 -	proof (cases j)
   9.373 -	  case 0 with a b Cons.prems show ?thesis by simp
   9.374 -	next
   9.375 -	  case (Suc j') with a b Cons.prems Cons show ?thesis 
   9.376 -	    apply -
   9.377 -	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
   9.378 -	    done
   9.379 -	qed
   9.380 -      qed
   9.381 -    next
   9.382 -      case (Suc n')
   9.383 -      show ?thesis
   9.384 -      proof (cases ys)
   9.385 -	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
   9.386 -      next
   9.387 -	case (Cons y ys) with Suc a Cons.prems show ?thesis
   9.388 -	  apply -
   9.389 -	  apply simp
   9.390 -	  apply (cases j)
   9.391 -	  apply simp
   9.392 -	  apply (cases i)
   9.393 -	  apply simp
   9.394 -	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
   9.395 -	  apply simp
   9.396 -	  apply simp
   9.397 -	  apply simp
   9.398 -	  apply simp
   9.399 -	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
   9.400 -	  apply simp
   9.401 -	  apply simp
   9.402 -	  apply simp
   9.403 -	  done
   9.404 -      qed
   9.405 -    qed
   9.406 -  qed
   9.407 -qed
   9.408 -
   9.409 -lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
   9.410 -by (induct xs arbitrary: i j, auto)
   9.411 -
   9.412 -lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
   9.413 -apply (induct xs arbitrary: a i j)
   9.414 -apply simp
   9.415 -apply (case_tac j)
   9.416 -apply simp
   9.417 -apply (case_tac i)
   9.418 -apply simp
   9.419 -apply simp
   9.420 -done
   9.421 -
   9.422 -lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
   9.423 -apply (induct xs arbitrary: a i j)
   9.424 -apply simp
   9.425 -apply simp
   9.426 -apply (case_tac j)
   9.427 -apply simp
   9.428 -apply auto
   9.429 -apply (case_tac nat)
   9.430 -apply auto
   9.431 -done
   9.432 -
   9.433 -(* suffices that j \<le> length xs and length ys *) 
   9.434 -lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
   9.435 -proof (induct xs arbitrary: ys i j)
   9.436 -  case Nil thus ?case by simp
   9.437 -next
   9.438 -  case (Cons x xs)
   9.439 -  thus ?case
   9.440 -    apply -
   9.441 -    apply (cases ys)
   9.442 -    apply simp
   9.443 -    apply simp
   9.444 -    apply auto
   9.445 -    apply (case_tac i', auto)
   9.446 -    apply (erule_tac x="Suc i'" in allE, auto)
   9.447 -    apply (erule_tac x="i' - 1" in allE, auto)
   9.448 -    apply (case_tac i', auto)
   9.449 -    apply (erule_tac x="Suc i'" in allE, auto)
   9.450 -    done
   9.451 -qed
   9.452 -
   9.453 -lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
   9.454 -by (induct xs, auto)
   9.455 -
   9.456 -lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
   9.457 -by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
   9.458 -
   9.459 -lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
   9.460 -by (induct xs arbitrary: i j k) auto
   9.461 -
   9.462 -lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
   9.463 -apply (induct xs arbitrary: i j k)
   9.464 -apply auto
   9.465 -apply (case_tac k)
   9.466 -apply auto
   9.467 -apply (case_tac i)
   9.468 -apply auto
   9.469 -done
   9.470 -
   9.471 -lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
   9.472 -apply (simp add: sublist'_sublist)
   9.473 -apply (simp add: set_sublist)
   9.474 -apply auto
   9.475 -done
   9.476 -
   9.477 -lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   9.478 -unfolding set_sublist' by blast
   9.479 -
   9.480 -lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   9.481 -unfolding set_sublist' by blast
   9.482 -
   9.483 -
   9.484 -lemma multiset_of_sublist:
   9.485 -assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
   9.486 -assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
   9.487 -assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
   9.488 -assumes multiset: "multiset_of xs = multiset_of ys"
   9.489 -  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
   9.490 -proof -
   9.491 -  from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
   9.492 -    by (simp add: sublist'_append)
   9.493 -  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
   9.494 -  with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
   9.495 -    by (simp add: sublist'_append)
   9.496 -  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
   9.497 -  moreover
   9.498 -  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
   9.499 -    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   9.500 -  moreover
   9.501 -  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
   9.502 -    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   9.503 -  moreover
   9.504 -  ultimately show ?thesis by (simp add: multiset_of_append)
   9.505 -qed
   9.506 -
   9.507 -
   9.508 -end