merged
authorhaftmann
Mon Mar 23 19:01:34 2009 +0100 (2009-03-23 ago)
changeset 3069055ef8e045931
parent 30668 df8a3c2fd5a2
parent 30689 b14b2cc4e25e
child 30691 0047f57f6669
child 30694 4b182a031731
merged
src/HOL/ex/ImperativeQuicksort.thy
src/HOL/ex/Subarray.thy
src/HOL/ex/Sublist.thy
     1.1 --- a/doc-src/HOL/HOL.tex	Mon Mar 23 15:33:35 2009 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon Mar 23 19:01:34 2009 +0100
     1.3 @@ -1427,7 +1427,7 @@
     1.4  provides a decision procedure for \emph{linear arithmetic}: formulae involving
     1.5  addition and subtraction. The simplifier invokes a weak version of this
     1.6  decision procedure automatically. If this is not sufficent, you can invoke the
     1.7 -full procedure \ttindex{arith_tac} explicitly.  It copes with arbitrary
     1.8 +full procedure \ttindex{linear_arith_tac} explicitly.  It copes with arbitrary
     1.9  formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
    1.10    min}, {\tt max} and numerical constants. Other subterms are treated as
    1.11  atomic, while subformulae not involving numerical types are ignored. Quantified
    1.12 @@ -1438,10 +1438,10 @@
    1.13  If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
    1.14  {\tt k dvd} are also supported. The former two are eliminated
    1.15  by case distinctions, again blowing up the running time.
    1.16 -If the formula involves explicit quantifiers, \texttt{arith_tac} may take
    1.17 +If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
    1.18  super-exponential time and space.
    1.19  
    1.20 -If \texttt{arith_tac} fails, try to find relevant arithmetic results in
    1.21 +If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in
    1.22  the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
    1.23  theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
    1.24  Theory \texttt{Divides} contains theorems about \texttt{div} and
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Mar 23 15:33:35 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Mar 23 19:01:34 2009 +0100
     2.3 @@ -1995,6 +1995,8 @@
     2.4    "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     2.5      (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
     2.6  
     2.7 +code_reserved SML oo
     2.8 +
     2.9  ML {* @{code ferrack_test} () *}
    2.10  
    2.11  oracle linr_oracle = {*
     3.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Mon Mar 23 15:33:35 2009 +0100
     3.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon Mar 23 19:01:34 2009 +0100
     3.3 @@ -443,7 +443,7 @@
     3.4  --{* 32 subgoals left *}
     3.5  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
     3.6  
     3.7 -apply(tactic {* TRYALL (simple_arith_tac @{context}) *})
     3.8 +apply(tactic {* TRYALL (linear_arith_tac @{context}) *})
     3.9  --{* 9 subgoals left *}
    3.10  apply (force simp add:less_Suc_eq)
    3.11  apply(drule sym)
     4.1 --- a/src/HOL/Imperative_HOL/ROOT.ML	Mon Mar 23 15:33:35 2009 +0100
     4.2 +++ b/src/HOL/Imperative_HOL/ROOT.ML	Mon Mar 23 19:01:34 2009 +0100
     4.3 @@ -1,2 +1,2 @@
     4.4  
     4.5 -use_thy "Imperative_HOL";
     4.6 +use_thy "Imperative_HOL_ex";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Mar 23 19:01:34 2009 +0100
     5.3 @@ -0,0 +1,639 @@
     5.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
     5.5 +
     5.6 +theory Imperative_Quicksort
     5.7 +imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
     5.8 +begin
     5.9 +
    5.10 +text {* We prove QuickSort correct in the Relational Calculus. *}
    5.11 +
    5.12 +definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
    5.13 +where
    5.14 +  "swap arr i j = (
    5.15 +     do
    5.16 +       x \<leftarrow> nth arr i;
    5.17 +       y \<leftarrow> nth arr j;
    5.18 +       upd i y arr;
    5.19 +       upd j x arr;
    5.20 +       return ()
    5.21 +     done)"
    5.22 +
    5.23 +lemma swap_permutes:
    5.24 +  assumes "crel (swap a i j) h h' rs"
    5.25 +  shows "multiset_of (get_array a h') 
    5.26 +  = multiset_of (get_array a h)"
    5.27 +  using assms
    5.28 +  unfolding swap_def
    5.29 +  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
    5.30 +
    5.31 +function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    5.32 +where
    5.33 +  "part1 a left right p = (
    5.34 +     if (right \<le> left) then return right
    5.35 +     else (do
    5.36 +       v \<leftarrow> nth a left;
    5.37 +       (if (v \<le> p) then (part1 a (left + 1) right p)
    5.38 +                    else (do swap a left right;
    5.39 +  part1 a left (right - 1) p done))
    5.40 +     done))"
    5.41 +by pat_completeness auto
    5.42 +
    5.43 +termination
    5.44 +by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
    5.45 +
    5.46 +declare part1.simps[simp del]
    5.47 +
    5.48 +lemma part_permutes:
    5.49 +  assumes "crel (part1 a l r p) h h' rs"
    5.50 +  shows "multiset_of (get_array a h') 
    5.51 +  = multiset_of (get_array a h)"
    5.52 +  using assms
    5.53 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    5.54 +  case (1 a l r p h h' rs)
    5.55 +  thus ?case
    5.56 +    unfolding part1.simps [of a l r p]
    5.57 +    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
    5.58 +qed
    5.59 +
    5.60 +lemma part_returns_index_in_bounds:
    5.61 +  assumes "crel (part1 a l r p) h h' rs"
    5.62 +  assumes "l \<le> r"
    5.63 +  shows "l \<le> rs \<and> rs \<le> r"
    5.64 +using assms
    5.65 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    5.66 +  case (1 a l r p h h' rs)
    5.67 +  note cr = `crel (part1 a l r p) h h' rs`
    5.68 +  show ?case
    5.69 +  proof (cases "r \<le> l")
    5.70 +    case True (* Terminating case *)
    5.71 +    with cr `l \<le> r` show ?thesis
    5.72 +      unfolding part1.simps[of a l r p]
    5.73 +      by (elim crelE crel_if crel_return crel_nth) auto
    5.74 +  next
    5.75 +    case False (* recursive case *)
    5.76 +    note rec_condition = this
    5.77 +    let ?v = "get_array a h ! l"
    5.78 +    show ?thesis
    5.79 +    proof (cases "?v \<le> p")
    5.80 +      case True
    5.81 +      with cr False
    5.82 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    5.83 +        unfolding part1.simps[of a l r p]
    5.84 +        by (elim crelE crel_nth crel_if crel_return) auto
    5.85 +      from rec_condition have "l + 1 \<le> r" by arith
    5.86 +      from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    5.87 +      show ?thesis by simp
    5.88 +    next
    5.89 +      case False
    5.90 +      with rec_condition cr
    5.91 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
    5.92 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    5.93 +        unfolding part1.simps[of a l r p]
    5.94 +        by (elim crelE crel_nth crel_if crel_return) auto
    5.95 +      from rec_condition have "l \<le> r - 1" by arith
    5.96 +      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    5.97 +    qed
    5.98 +  qed
    5.99 +qed
   5.100 +
   5.101 +lemma part_length_remains:
   5.102 +  assumes "crel (part1 a l r p) h h' rs"
   5.103 +  shows "Heap.length a h = Heap.length a h'"
   5.104 +using assms
   5.105 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   5.106 +  case (1 a l r p h h' rs)
   5.107 +  note cr = `crel (part1 a l r p) h h' rs`
   5.108 +  
   5.109 +  show ?case
   5.110 +  proof (cases "r \<le> l")
   5.111 +    case True (* Terminating case *)
   5.112 +    with cr show ?thesis
   5.113 +      unfolding part1.simps[of a l r p]
   5.114 +      by (elim crelE crel_if crel_return crel_nth) auto
   5.115 +  next
   5.116 +    case False (* recursive case *)
   5.117 +    with cr 1 show ?thesis
   5.118 +      unfolding part1.simps [of a l r p] swap_def
   5.119 +      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
   5.120 +  qed
   5.121 +qed
   5.122 +
   5.123 +lemma part_outer_remains:
   5.124 +  assumes "crel (part1 a l r p) h h' rs"
   5.125 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   5.126 +  using assms
   5.127 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   5.128 +  case (1 a l r p h h' rs)
   5.129 +  note cr = `crel (part1 a l r p) h h' rs`
   5.130 +  
   5.131 +  show ?case
   5.132 +  proof (cases "r \<le> l")
   5.133 +    case True (* Terminating case *)
   5.134 +    with cr show ?thesis
   5.135 +      unfolding part1.simps[of a l r p]
   5.136 +      by (elim crelE crel_if crel_return crel_nth) auto
   5.137 +  next
   5.138 +    case False (* recursive case *)
   5.139 +    note rec_condition = this
   5.140 +    let ?v = "get_array a h ! l"
   5.141 +    show ?thesis
   5.142 +    proof (cases "?v \<le> p")
   5.143 +      case True
   5.144 +      with cr False
   5.145 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   5.146 +        unfolding part1.simps[of a l r p]
   5.147 +        by (elim crelE crel_nth crel_if crel_return) auto
   5.148 +      from 1(1)[OF rec_condition True rec1]
   5.149 +      show ?thesis by fastsimp
   5.150 +    next
   5.151 +      case False
   5.152 +      with rec_condition cr
   5.153 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   5.154 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   5.155 +        unfolding part1.simps[of a l r p]
   5.156 +        by (elim crelE crel_nth crel_if crel_return) auto
   5.157 +      from swp rec_condition have
   5.158 +        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
   5.159 +	unfolding swap_def
   5.160 +	by (elim crelE crel_nth crel_upd crel_return) auto
   5.161 +      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   5.162 +    qed
   5.163 +  qed
   5.164 +qed
   5.165 +
   5.166 +
   5.167 +lemma part_partitions:
   5.168 +  assumes "crel (part1 a l r p) h h' rs"
   5.169 +  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
   5.170 +  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
   5.171 +  using assms
   5.172 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   5.173 +  case (1 a l r p h h' rs)
   5.174 +  note cr = `crel (part1 a l r p) h h' rs`
   5.175 +  
   5.176 +  show ?case
   5.177 +  proof (cases "r \<le> l")
   5.178 +    case True (* Terminating case *)
   5.179 +    with cr have "rs = r"
   5.180 +      unfolding part1.simps[of a l r p]
   5.181 +      by (elim crelE crel_if crel_return crel_nth) auto
   5.182 +    with True
   5.183 +    show ?thesis by auto
   5.184 +  next
   5.185 +    case False (* recursive case *)
   5.186 +    note lr = this
   5.187 +    let ?v = "get_array a h ! l"
   5.188 +    show ?thesis
   5.189 +    proof (cases "?v \<le> p")
   5.190 +      case True
   5.191 +      with lr cr
   5.192 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   5.193 +        unfolding part1.simps[of a l r p]
   5.194 +        by (elim crelE crel_nth crel_if crel_return) auto
   5.195 +      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
   5.196 +	by fastsimp
   5.197 +      have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
   5.198 +      with 1(1)[OF False True rec1] a_l show ?thesis
   5.199 +	by auto
   5.200 +    next
   5.201 +      case False
   5.202 +      with lr cr
   5.203 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   5.204 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   5.205 +        unfolding part1.simps[of a l r p]
   5.206 +        by (elim crelE crel_nth crel_if crel_return) auto
   5.207 +      from swp False have "get_array a h1 ! r \<ge> p"
   5.208 +	unfolding swap_def
   5.209 +	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
   5.210 +      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
   5.211 +	by fastsimp
   5.212 +      have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   5.213 +      with 1(2)[OF lr False rec2] a_r show ?thesis
   5.214 +	by auto
   5.215 +    qed
   5.216 +  qed
   5.217 +qed
   5.218 +
   5.219 +
   5.220 +fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
   5.221 +where
   5.222 +  "partition a left right = (do
   5.223 +     pivot \<leftarrow> nth a right;
   5.224 +     middle \<leftarrow> part1 a left (right - 1) pivot;
   5.225 +     v \<leftarrow> nth a middle;
   5.226 +     m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
   5.227 +     swap a m right;
   5.228 +     return m
   5.229 +   done)"
   5.230 +
   5.231 +declare partition.simps[simp del]
   5.232 +
   5.233 +lemma partition_permutes:
   5.234 +  assumes "crel (partition a l r) h h' rs"
   5.235 +  shows "multiset_of (get_array a h') 
   5.236 +  = multiset_of (get_array a h)"
   5.237 +proof -
   5.238 +    from assms part_permutes swap_permutes show ?thesis
   5.239 +      unfolding partition.simps
   5.240 +      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   5.241 +qed
   5.242 +
   5.243 +lemma partition_length_remains:
   5.244 +  assumes "crel (partition a l r) h h' rs"
   5.245 +  shows "Heap.length a h = Heap.length a h'"
   5.246 +proof -
   5.247 +  from assms part_length_remains show ?thesis
   5.248 +    unfolding partition.simps swap_def
   5.249 +    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   5.250 +qed
   5.251 +
   5.252 +lemma partition_outer_remains:
   5.253 +  assumes "crel (partition a l r) h h' rs"
   5.254 +  assumes "l < r"
   5.255 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   5.256 +proof -
   5.257 +  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   5.258 +    unfolding partition.simps swap_def
   5.259 +    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
   5.260 +qed
   5.261 +
   5.262 +lemma partition_returns_index_in_bounds:
   5.263 +  assumes crel: "crel (partition a l r) h h' rs"
   5.264 +  assumes "l < r"
   5.265 +  shows "l \<le> rs \<and> rs \<le> r"
   5.266 +proof -
   5.267 +  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   5.268 +    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
   5.269 +         else middle)"
   5.270 +    unfolding partition.simps
   5.271 +    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   5.272 +  from `l < r` have "l \<le> r - 1" by arith
   5.273 +  from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   5.274 +qed
   5.275 +
   5.276 +lemma partition_partitions:
   5.277 +  assumes crel: "crel (partition a l r) h h' rs"
   5.278 +  assumes "l < r"
   5.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>
   5.280 +  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
   5.281 +proof -
   5.282 +  let ?pivot = "get_array a h ! r" 
   5.283 +  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
   5.284 +    and swap: "crel (swap a rs r) h1 h' ()"
   5.285 +    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
   5.286 +         else middle)"
   5.287 +    unfolding partition.simps
   5.288 +    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   5.289 +  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
   5.290 +    (Heap.upd a rs (get_array a h1 ! r) h1)"
   5.291 +    unfolding swap_def
   5.292 +    by (elim crelE crel_return crel_nth crel_upd) simp
   5.293 +  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
   5.294 +    unfolding swap_def
   5.295 +    by (elim crelE crel_return crel_nth crel_upd) simp
   5.296 +  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
   5.297 +    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   5.298 +  from `l < r` have "l \<le> r - 1" by simp 
   5.299 +  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   5.300 +  from part_outer_remains[OF part] `l < r`
   5.301 +  have "get_array a h ! r = get_array a h1 ! r"
   5.302 +    by fastsimp
   5.303 +  with swap
   5.304 +  have right_remains: "get_array a h ! r = get_array a h' ! rs"
   5.305 +    unfolding swap_def
   5.306 +    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   5.307 +  from part_partitions [OF part]
   5.308 +  show ?thesis
   5.309 +  proof (cases "get_array a h1 ! middle \<le> ?pivot")
   5.310 +    case True
   5.311 +    with rs_equals have rs_equals: "rs = middle + 1" by simp
   5.312 +    { 
   5.313 +      fix i
   5.314 +      assume i_is_left: "l \<le> i \<and> i < rs"
   5.315 +      with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
   5.316 +      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   5.317 +      from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
   5.318 +      with part_partitions[OF part] right_remains True
   5.319 +      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   5.320 +      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
   5.321 +	unfolding Heap.upd_def Heap.length_def by simp
   5.322 +    }
   5.323 +    moreover
   5.324 +    {
   5.325 +      fix i
   5.326 +      assume "rs < i \<and> i \<le> r"
   5.327 +
   5.328 +      hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
   5.329 +      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   5.330 +      proof
   5.331 +	assume i_is: "rs < i \<and> i \<le> r - 1"
   5.332 +	with swap_length_remains in_bounds middle_in_bounds rs_equals
   5.333 +	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   5.334 +	from part_partitions[OF part] rs_equals right_remains i_is
   5.335 +	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   5.336 +	  by fastsimp
   5.337 +	with i_props h'_def show ?thesis by fastsimp
   5.338 +      next
   5.339 +	assume i_is: "rs < i \<and> i = r"
   5.340 +	with rs_equals have "Suc middle \<noteq> r" by arith
   5.341 +	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
   5.342 +	with part_partitions[OF part] right_remains 
   5.343 +	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
   5.344 +	  by fastsimp
   5.345 +	with i_is True rs_equals right_remains h'_def
   5.346 +	show ?thesis using in_bounds
   5.347 +	  unfolding Heap.upd_def Heap.length_def
   5.348 +	  by auto
   5.349 +      qed
   5.350 +    }
   5.351 +    ultimately show ?thesis by auto
   5.352 +  next
   5.353 +    case False
   5.354 +    with rs_equals have rs_equals: "middle = rs" by simp
   5.355 +    { 
   5.356 +      fix i
   5.357 +      assume i_is_left: "l \<le> i \<and> i < rs"
   5.358 +      with swap_length_remains in_bounds middle_in_bounds rs_equals
   5.359 +      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   5.360 +      from part_partitions[OF part] rs_equals right_remains i_is_left
   5.361 +      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   5.362 +      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
   5.363 +	unfolding Heap.upd_def by simp
   5.364 +    }
   5.365 +    moreover
   5.366 +    {
   5.367 +      fix i
   5.368 +      assume "rs < i \<and> i \<le> r"
   5.369 +      hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
   5.370 +      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   5.371 +      proof
   5.372 +	assume i_is: "rs < i \<and> i \<le> r - 1"
   5.373 +	with swap_length_remains in_bounds middle_in_bounds rs_equals
   5.374 +	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   5.375 +	from part_partitions[OF part] rs_equals right_remains i_is
   5.376 +	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   5.377 +	  by fastsimp
   5.378 +	with i_props h'_def show ?thesis by fastsimp
   5.379 +      next
   5.380 +	assume i_is: "i = r"
   5.381 +	from i_is False rs_equals right_remains h'_def
   5.382 +	show ?thesis using in_bounds
   5.383 +	  unfolding Heap.upd_def Heap.length_def
   5.384 +	  by auto
   5.385 +      qed
   5.386 +    }
   5.387 +    ultimately
   5.388 +    show ?thesis by auto
   5.389 +  qed
   5.390 +qed
   5.391 +
   5.392 +
   5.393 +function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
   5.394 +where
   5.395 +  "quicksort arr left right =
   5.396 +     (if (right > left)  then
   5.397 +        do
   5.398 +          pivotNewIndex \<leftarrow> partition arr left right;
   5.399 +          pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
   5.400 +          quicksort arr left (pivotNewIndex - 1);
   5.401 +          quicksort arr (pivotNewIndex + 1) right
   5.402 +        done
   5.403 +     else return ())"
   5.404 +by pat_completeness auto
   5.405 +
   5.406 +(* For termination, we must show that the pivotNewIndex is between left and right *) 
   5.407 +termination
   5.408 +by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
   5.409 +
   5.410 +declare quicksort.simps[simp del]
   5.411 +
   5.412 +
   5.413 +lemma quicksort_permutes:
   5.414 +  assumes "crel (quicksort a l r) h h' rs"
   5.415 +  shows "multiset_of (get_array a h') 
   5.416 +  = multiset_of (get_array a h)"
   5.417 +  using assms
   5.418 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   5.419 +  case (1 a l r h h' rs)
   5.420 +  with partition_permutes show ?case
   5.421 +    unfolding quicksort.simps [of a l r]
   5.422 +    by (elim crel_if crelE crel_assert crel_return) auto
   5.423 +qed
   5.424 +
   5.425 +lemma length_remains:
   5.426 +  assumes "crel (quicksort a l r) h h' rs"
   5.427 +  shows "Heap.length a h = Heap.length a h'"
   5.428 +using assms
   5.429 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   5.430 +  case (1 a l r h h' rs)
   5.431 +  with partition_length_remains show ?case
   5.432 +    unfolding quicksort.simps [of a l r]
   5.433 +    by (elim crel_if crelE crel_assert crel_return) auto
   5.434 +qed
   5.435 +
   5.436 +lemma quicksort_outer_remains:
   5.437 +  assumes "crel (quicksort a l r) h h' rs"
   5.438 +   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   5.439 +  using assms
   5.440 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   5.441 +  case (1 a l r h h' rs)
   5.442 +  note cr = `crel (quicksort a l r) h h' rs`
   5.443 +  thus ?case
   5.444 +  proof (cases "r > l")
   5.445 +    case False
   5.446 +    with cr have "h' = h"
   5.447 +      unfolding quicksort.simps [of a l r]
   5.448 +      by (elim crel_if crel_return) auto
   5.449 +    thus ?thesis by simp
   5.450 +  next
   5.451 +  case True
   5.452 +   { 
   5.453 +      fix h1 h2 p ret1 ret2 i
   5.454 +      assume part: "crel (partition a l r) h h1 p"
   5.455 +      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
   5.456 +      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
   5.457 +      assume pivot: "l \<le> p \<and> p \<le> r"
   5.458 +      assume i_outer: "i < l \<or> r < i"
   5.459 +      from  partition_outer_remains [OF part True] i_outer
   5.460 +      have "get_array a h !i = get_array a h1 ! i" by fastsimp
   5.461 +      moreover
   5.462 +      with 1(1) [OF True pivot qs1] pivot i_outer
   5.463 +      have "get_array a h1 ! i = get_array a h2 ! i" by auto
   5.464 +      moreover
   5.465 +      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
   5.466 +      have "get_array a h2 ! i = get_array a h' ! i" by auto
   5.467 +      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
   5.468 +    }
   5.469 +    with cr show ?thesis
   5.470 +      unfolding quicksort.simps [of a l r]
   5.471 +      by (elim crel_if crelE crel_assert crel_return) auto
   5.472 +  qed
   5.473 +qed
   5.474 +
   5.475 +lemma quicksort_is_skip:
   5.476 +  assumes "crel (quicksort a l r) h h' rs"
   5.477 +  shows "r \<le> l \<longrightarrow> h = h'"
   5.478 +  using assms
   5.479 +  unfolding quicksort.simps [of a l r]
   5.480 +  by (elim crel_if crel_return) auto
   5.481 + 
   5.482 +lemma quicksort_sorts:
   5.483 +  assumes "crel (quicksort a l r) h h' rs"
   5.484 +  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
   5.485 +  shows "sorted (subarray l (r + 1) a h')"
   5.486 +  using assms
   5.487 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   5.488 +  case (1 a l r h h' rs)
   5.489 +  note cr = `crel (quicksort a l r) h h' rs`
   5.490 +  thus ?case
   5.491 +  proof (cases "r > l")
   5.492 +    case False
   5.493 +    hence "l \<ge> r + 1 \<or> l = r" by arith 
   5.494 +    with length_remains[OF cr] 1(5) show ?thesis
   5.495 +      by (auto simp add: subarray_Nil subarray_single)
   5.496 +  next
   5.497 +    case True
   5.498 +    { 
   5.499 +      fix h1 h2 p
   5.500 +      assume part: "crel (partition a l r) h h1 p"
   5.501 +      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
   5.502 +      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
   5.503 +      from partition_returns_index_in_bounds [OF part True]
   5.504 +      have pivot: "l\<le> p \<and> p \<le> r" .
   5.505 +     note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
   5.506 +      from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
   5.507 +      have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
   5.508 +        (*-- First of all, by induction hypothesis both sublists are sorted. *)
   5.509 +      from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
   5.510 +      have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
   5.511 +      from quicksort_outer_remains [OF qs2] length_remains
   5.512 +      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
   5.513 +	by (simp add: subarray_eq_samelength_iff)
   5.514 +      with IH1 have IH1': "sorted (subarray l p a h')" by simp
   5.515 +      from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
   5.516 +      have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
   5.517 +        by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
   5.518 +           (* -- Secondly, both sublists remain partitioned. *)
   5.519 +      from partition_partitions[OF part True]
   5.520 +      have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
   5.521 +        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
   5.522 +        by (auto simp add: all_in_set_subarray_conv)
   5.523 +      from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
   5.524 +        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
   5.525 +      have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
   5.526 +	unfolding Heap.length_def subarray_def by (cases p, auto)
   5.527 +      with left_subarray_remains part_conds1 pivot_unchanged
   5.528 +      have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
   5.529 +        by (simp, subst set_of_multiset_of[symmetric], simp)
   5.530 +          (* -- These steps are the analogous for the right sublist \<dots> *)
   5.531 +      from quicksort_outer_remains [OF qs1] length_remains
   5.532 +      have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
   5.533 +	by (auto simp add: subarray_eq_samelength_iff)
   5.534 +      from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
   5.535 +        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
   5.536 +      have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
   5.537 +        unfolding Heap.length_def subarray_def by auto
   5.538 +      with right_subarray_remains part_conds2 pivot_unchanged
   5.539 +      have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
   5.540 +        by (simp, subst set_of_multiset_of[symmetric], simp)
   5.541 +          (* -- Thirdly and finally, we show that the array is sorted
   5.542 +          following from the facts above. *)
   5.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'"
   5.544 +	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
   5.545 +      with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
   5.546 +	unfolding subarray_def
   5.547 +	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
   5.548 +	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   5.549 +    }
   5.550 +    with True cr show ?thesis
   5.551 +      unfolding quicksort.simps [of a l r]
   5.552 +      by (elim crel_if crel_return crelE crel_assert) auto
   5.553 +  qed
   5.554 +qed
   5.555 +
   5.556 +
   5.557 +lemma quicksort_is_sort:
   5.558 +  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
   5.559 +  shows "get_array a h' = sort (get_array a h)"
   5.560 +proof (cases "get_array a h = []")
   5.561 +  case True
   5.562 +  with quicksort_is_skip[OF crel] show ?thesis
   5.563 +  unfolding Heap.length_def by simp
   5.564 +next
   5.565 +  case False
   5.566 +  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
   5.567 +    unfolding Heap.length_def subarray_def by auto
   5.568 +  with length_remains[OF crel] have "sorted (get_array a h')"
   5.569 +    unfolding Heap.length_def by simp
   5.570 +  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
   5.571 +qed
   5.572 +
   5.573 +subsection {* No Errors in quicksort *}
   5.574 +text {* We have proved that quicksort sorts (if no exceptions occur).
   5.575 +We will now show that exceptions do not occur. *}
   5.576 +
   5.577 +lemma noError_part1: 
   5.578 +  assumes "l < Heap.length a h" "r < Heap.length a h"
   5.579 +  shows "noError (part1 a l r p) h"
   5.580 +  using assms
   5.581 +proof (induct a l r p arbitrary: h rule: part1.induct)
   5.582 +  case (1 a l r p)
   5.583 +  thus ?case
   5.584 +    unfolding part1.simps [of a l r] swap_def
   5.585 +    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
   5.586 +qed
   5.587 +
   5.588 +lemma noError_partition:
   5.589 +  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
   5.590 +  shows "noError (partition a l r) h"
   5.591 +using assms
   5.592 +unfolding partition.simps swap_def
   5.593 +apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
   5.594 +apply (frule part_length_remains)
   5.595 +apply (frule part_returns_index_in_bounds)
   5.596 +apply auto
   5.597 +apply (frule part_length_remains)
   5.598 +apply (frule part_returns_index_in_bounds)
   5.599 +apply auto
   5.600 +apply (frule part_length_remains)
   5.601 +apply auto
   5.602 +done
   5.603 +
   5.604 +lemma noError_quicksort:
   5.605 +  assumes "l < Heap.length a h" "r < Heap.length a h"
   5.606 +  shows "noError (quicksort a l r) h"
   5.607 +using assms
   5.608 +proof (induct a l r arbitrary: h rule: quicksort.induct)
   5.609 +  case (1 a l ri h)
   5.610 +  thus ?case
   5.611 +    unfolding quicksort.simps [of a l ri]
   5.612 +    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
   5.613 +    apply (frule partition_returns_index_in_bounds)
   5.614 +    apply auto
   5.615 +    apply (frule partition_returns_index_in_bounds)
   5.616 +    apply auto
   5.617 +    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
   5.618 +    apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   5.619 +    apply (erule disjE)
   5.620 +    apply auto
   5.621 +    unfolding quicksort.simps [of a "Suc ri" ri]
   5.622 +    apply (auto intro!: noError_if noError_return)
   5.623 +    done
   5.624 +qed
   5.625 +
   5.626 +
   5.627 +subsection {* Example *}
   5.628 +
   5.629 +definition "qsort a = do
   5.630 +    k \<leftarrow> length a;
   5.631 +    quicksort a 0 (k - 1);
   5.632 +    return a
   5.633 +  done"
   5.634 +
   5.635 +ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
   5.636 +
   5.637 +export_code qsort in SML_imp module_name QSort
   5.638 +export_code qsort in OCaml module_name QSort file -
   5.639 +export_code qsort in OCaml_imp module_name QSort file -
   5.640 +export_code qsort in Haskell module_name QSort file -
   5.641 +
   5.642 +end
   5.643 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Mon Mar 23 19:01:34 2009 +0100
     6.3 @@ -0,0 +1,66 @@
     6.4 +theory Subarray
     6.5 +imports Array Sublist
     6.6 +begin
     6.7 +
     6.8 +definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
     6.9 +where
    6.10 +  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
    6.11 +
    6.12 +lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    6.13 +apply (simp add: subarray_def Heap.upd_def)
    6.14 +apply (simp add: sublist'_update1)
    6.15 +done
    6.16 +
    6.17 +lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
    6.18 +apply (simp add: subarray_def Heap.upd_def)
    6.19 +apply (subst sublist'_update2)
    6.20 +apply fastsimp
    6.21 +apply simp
    6.22 +done
    6.23 +
    6.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]"
    6.25 +unfolding subarray_def Heap.upd_def
    6.26 +by (simp add: sublist'_update3)
    6.27 +
    6.28 +lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
    6.29 +by (simp add: subarray_def sublist'_Nil')
    6.30 +
    6.31 +lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
    6.32 +by (simp add: subarray_def Heap.length_def sublist'_single)
    6.33 +
    6.34 +lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
    6.35 +by (simp add: subarray_def Heap.length_def length_sublist')
    6.36 +
    6.37 +lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
    6.38 +by (simp add: length_subarray)
    6.39 +
    6.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"
    6.41 +unfolding Heap.length_def subarray_def
    6.42 +by (simp add: sublist'_front)
    6.43 +
    6.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)]"
    6.45 +unfolding Heap.length_def subarray_def
    6.46 +by (simp add: sublist'_back)
    6.47 +
    6.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"
    6.49 +unfolding subarray_def
    6.50 +by (simp add: sublist'_append)
    6.51 +
    6.52 +lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
    6.53 +unfolding Heap.length_def subarray_def
    6.54 +by (simp add: sublist'_all)
    6.55 +
    6.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)"
    6.57 +unfolding Heap.length_def subarray_def
    6.58 +by (simp add: nth_sublist')
    6.59 +
    6.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')"
    6.61 +unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    6.62 +
    6.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))"
    6.64 +unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
    6.65 +
    6.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))"
    6.67 +unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
    6.68 +
    6.69 +end
    6.70 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Mon Mar 23 19:01:34 2009 +0100
     7.3 @@ -0,0 +1,505 @@
     7.4 +(* $Id$ *)
     7.5 +
     7.6 +header {* Slices of lists *}
     7.7 +
     7.8 +theory Sublist
     7.9 +imports Multiset
    7.10 +begin
    7.11 +
    7.12 +
    7.13 +lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    7.14 +apply (induct xs arbitrary: i j k)
    7.15 +apply simp
    7.16 +apply (simp only: sublist_Cons)
    7.17 +apply simp
    7.18 +apply safe
    7.19 +apply simp
    7.20 +apply (erule_tac x="0" in meta_allE)
    7.21 +apply (erule_tac x="j - 1" in meta_allE)
    7.22 +apply (erule_tac x="k - 1" in meta_allE)
    7.23 +apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    7.24 +apply simp
    7.25 +apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
    7.26 +apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
    7.27 +apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
    7.28 +apply simp
    7.29 +apply fastsimp
    7.30 +apply fastsimp
    7.31 +apply fastsimp
    7.32 +apply fastsimp
    7.33 +apply (erule_tac x="i - 1" in meta_allE)
    7.34 +apply (erule_tac x="j - 1" in meta_allE)
    7.35 +apply (erule_tac x="k - 1" in meta_allE)
    7.36 +apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
    7.37 +apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
    7.38 +apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
    7.39 +apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    7.40 +apply simp
    7.41 +apply fastsimp
    7.42 +apply fastsimp
    7.43 +apply fastsimp
    7.44 +apply fastsimp
    7.45 +done
    7.46 +
    7.47 +lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
    7.48 +apply (induct xs arbitrary: i inds)
    7.49 +apply simp
    7.50 +apply (case_tac i)
    7.51 +apply (simp add: sublist_Cons)
    7.52 +apply (simp add: sublist_Cons)
    7.53 +done
    7.54 +
    7.55 +lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
    7.56 +proof (induct xs arbitrary: i inds)
    7.57 +  case Nil thus ?case by simp
    7.58 +next
    7.59 +  case (Cons x xs)
    7.60 +  thus ?case
    7.61 +  proof (cases i)
    7.62 +    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
    7.63 +  next
    7.64 +    case (Suc i')
    7.65 +    with Cons show ?thesis
    7.66 +      apply simp
    7.67 +      apply (simp add: sublist_Cons)
    7.68 +      apply auto
    7.69 +      apply (auto simp add: nat.split)
    7.70 +      apply (simp add: card_less_Suc[symmetric])
    7.71 +      apply (simp add: card_less_Suc2)
    7.72 +      done
    7.73 +  qed
    7.74 +qed
    7.75 +
    7.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)"
    7.77 +by (simp add: sublist_update1 sublist_update2)
    7.78 +
    7.79 +lemma sublist_take: "sublist xs {j. j < m} = take m xs"
    7.80 +apply (induct xs arbitrary: m)
    7.81 +apply simp
    7.82 +apply (case_tac m)
    7.83 +apply simp
    7.84 +apply (simp add: sublist_Cons)
    7.85 +done
    7.86 +
    7.87 +lemma sublist_take': "sublist xs {0..<m} = take m xs"
    7.88 +apply (induct xs arbitrary: m)
    7.89 +apply simp
    7.90 +apply (case_tac m)
    7.91 +apply simp
    7.92 +apply (simp add: sublist_Cons sublist_take)
    7.93 +done
    7.94 +
    7.95 +lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
    7.96 +apply (induct xs)
    7.97 +apply simp
    7.98 +apply (simp add: sublist_Cons)
    7.99 +done
   7.100 +
   7.101 +lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
   7.102 +apply (induct xs)
   7.103 +apply simp
   7.104 +apply (simp add: sublist_Cons)
   7.105 +done
   7.106 +
   7.107 +lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
   7.108 +apply (induct xs arbitrary: a)
   7.109 +apply simp
   7.110 +apply(case_tac aa)
   7.111 +apply simp
   7.112 +apply (simp add: sublist_Cons)
   7.113 +apply simp
   7.114 +apply (simp add: sublist_Cons)
   7.115 +done
   7.116 +
   7.117 +lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
   7.118 +apply (induct xs arbitrary: inds)
   7.119 +apply simp
   7.120 +apply (simp add: sublist_Cons)
   7.121 +apply auto
   7.122 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.123 +apply auto
   7.124 +done
   7.125 +
   7.126 +lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
   7.127 +apply (induct xs arbitrary: inds)
   7.128 +apply simp
   7.129 +apply (simp add: sublist_Cons)
   7.130 +apply (auto split: if_splits)
   7.131 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.132 +apply (case_tac x, auto)
   7.133 +done
   7.134 +
   7.135 +lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
   7.136 +apply (induct xs arbitrary: inds)
   7.137 +apply simp
   7.138 +apply (simp add: sublist_Cons)
   7.139 +apply auto
   7.140 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.141 +apply (case_tac x, auto)
   7.142 +done
   7.143 +
   7.144 +lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
   7.145 +apply (induct xs arbitrary: ys inds inds')
   7.146 +apply simp
   7.147 +apply (drule sym, rule sym)
   7.148 +apply (simp add: sublist_Nil, fastsimp)
   7.149 +apply (case_tac ys)
   7.150 +apply (simp add: sublist_Nil, fastsimp)
   7.151 +apply (auto simp add: sublist_Cons)
   7.152 +apply (erule_tac x="list" in meta_allE)
   7.153 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.154 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   7.155 +apply fastsimp
   7.156 +apply (erule_tac x="list" in meta_allE)
   7.157 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.158 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   7.159 +apply fastsimp
   7.160 +done
   7.161 +
   7.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"
   7.163 +apply (induct xs arbitrary: ys inds)
   7.164 +apply simp
   7.165 +apply (rule sym, simp add: sublist_Nil)
   7.166 +apply (case_tac ys)
   7.167 +apply (simp add: sublist_Nil)
   7.168 +apply (auto simp add: sublist_Cons)
   7.169 +apply (erule_tac x="list" in meta_allE)
   7.170 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.171 +apply fastsimp
   7.172 +apply (erule_tac x="list" in meta_allE)
   7.173 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.174 +apply fastsimp
   7.175 +done
   7.176 +
   7.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"
   7.178 +by (rule sublist_eq, auto)
   7.179 +
   7.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)"
   7.181 +apply (induct xs arbitrary: ys inds)
   7.182 +apply simp
   7.183 +apply (rule sym, simp add: sublist_Nil)
   7.184 +apply (case_tac ys)
   7.185 +apply (simp add: sublist_Nil)
   7.186 +apply (auto simp add: sublist_Cons)
   7.187 +apply (case_tac i)
   7.188 +apply auto
   7.189 +apply (case_tac i)
   7.190 +apply auto
   7.191 +done
   7.192 +
   7.193 +section {* Another sublist function *}
   7.194 +
   7.195 +function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   7.196 +where
   7.197 +  "sublist' n m [] = []"
   7.198 +| "sublist' n 0 xs = []"
   7.199 +| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
   7.200 +| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
   7.201 +by pat_completeness auto
   7.202 +termination by lexicographic_order
   7.203 +
   7.204 +subsection {* Proving equivalence to the other sublist command *}
   7.205 +
   7.206 +lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
   7.207 +apply (induct xs arbitrary: n m)
   7.208 +apply simp
   7.209 +apply (case_tac n)
   7.210 +apply (case_tac m)
   7.211 +apply simp
   7.212 +apply (simp add: sublist_Cons)
   7.213 +apply (case_tac m)
   7.214 +apply simp
   7.215 +apply (simp add: sublist_Cons)
   7.216 +done
   7.217 +
   7.218 +
   7.219 +lemma "sublist' n m xs = sublist xs {n..<m}"
   7.220 +apply (induct xs arbitrary: n m)
   7.221 +apply simp
   7.222 +apply (case_tac n, case_tac m)
   7.223 +apply simp
   7.224 +apply simp
   7.225 +apply (simp add: sublist_take')
   7.226 +apply (case_tac m)
   7.227 +apply simp
   7.228 +apply (simp add: sublist_Cons sublist'_sublist)
   7.229 +done
   7.230 +
   7.231 +
   7.232 +subsection {* Showing equivalence to use of drop and take for definition *}
   7.233 +
   7.234 +lemma "sublist' n m xs = take (m - n) (drop n xs)"
   7.235 +apply (induct xs arbitrary: n m)
   7.236 +apply simp
   7.237 +apply (case_tac m)
   7.238 +apply simp
   7.239 +apply (case_tac n)
   7.240 +apply simp
   7.241 +apply simp
   7.242 +done
   7.243 +
   7.244 +subsection {* General lemma about sublist *}
   7.245 +
   7.246 +lemma sublist'_Nil[simp]: "sublist' i j [] = []"
   7.247 +by simp
   7.248 +
   7.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)"
   7.250 +by (cases i) auto
   7.251 +
   7.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))"
   7.253 +apply (cases j)
   7.254 +apply auto
   7.255 +apply (cases i)
   7.256 +apply auto
   7.257 +done
   7.258 +
   7.259 +lemma sublist_n_0: "sublist' n 0 xs = []"
   7.260 +by (induct xs, auto)
   7.261 +
   7.262 +lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
   7.263 +apply (induct xs arbitrary: n m)
   7.264 +apply simp
   7.265 +apply (case_tac m)
   7.266 +apply simp
   7.267 +apply (case_tac n)
   7.268 +apply simp
   7.269 +apply simp
   7.270 +done
   7.271 +
   7.272 +lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
   7.273 +apply (induct xs arbitrary: n m)
   7.274 +apply simp
   7.275 +apply (case_tac m)
   7.276 +apply simp
   7.277 +apply (case_tac n)
   7.278 +apply simp
   7.279 +apply simp
   7.280 +done
   7.281 +
   7.282 +lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
   7.283 +apply (induct xs arbitrary: n m)
   7.284 +apply simp
   7.285 +apply (case_tac m)
   7.286 +apply simp
   7.287 +apply (case_tac n)
   7.288 +apply simp
   7.289 +apply simp
   7.290 +done
   7.291 +
   7.292 +lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
   7.293 +apply (induct xs arbitrary: n m)
   7.294 +apply simp
   7.295 +apply (case_tac m)
   7.296 +apply simp
   7.297 +apply (case_tac n)
   7.298 +apply simp
   7.299 +apply simp
   7.300 +done
   7.301 +
   7.302 +lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
   7.303 +apply (induct xs arbitrary: n)
   7.304 +apply simp
   7.305 +apply simp
   7.306 +apply (case_tac n)
   7.307 +apply (simp add: sublist_n_0)
   7.308 +apply simp
   7.309 +done
   7.310 +
   7.311 +lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   7.312 +apply (induct xs arbitrary: n m i)
   7.313 +apply simp
   7.314 +apply simp
   7.315 +apply (case_tac i)
   7.316 +apply simp
   7.317 +apply simp
   7.318 +done
   7.319 +
   7.320 +lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   7.321 +apply (induct xs arbitrary: n m i)
   7.322 +apply simp
   7.323 +apply simp
   7.324 +apply (case_tac i)
   7.325 +apply simp
   7.326 +apply simp
   7.327 +done
   7.328 +
   7.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]"
   7.330 +proof (induct xs arbitrary: n m i)
   7.331 +  case Nil thus ?case by auto
   7.332 +next
   7.333 +  case (Cons x xs)
   7.334 +  thus ?case
   7.335 +    apply -
   7.336 +    apply auto
   7.337 +    apply (cases i)
   7.338 +    apply auto
   7.339 +    apply (cases i)
   7.340 +    apply auto
   7.341 +    done
   7.342 +qed
   7.343 +
   7.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"
   7.345 +proof (induct xs arbitrary: i j ys n m)
   7.346 +  case Nil
   7.347 +  thus ?case
   7.348 +    apply -
   7.349 +    apply (rule sym, drule sym)
   7.350 +    apply (simp add: sublist'_Nil)
   7.351 +    apply (simp add: sublist'_Nil3)
   7.352 +    apply arith
   7.353 +    done
   7.354 +next
   7.355 +  case (Cons x xs i j ys n m)
   7.356 +  note c = this
   7.357 +  thus ?case
   7.358 +  proof (cases m)
   7.359 +    case 0 thus ?thesis by (simp add: sublist_n_0)
   7.360 +  next
   7.361 +    case (Suc m')
   7.362 +    note a = this
   7.363 +    thus ?thesis
   7.364 +    proof (cases n)
   7.365 +      case 0 note b = this
   7.366 +      show ?thesis
   7.367 +      proof (cases ys)
   7.368 +	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
   7.369 +      next
   7.370 +	case (Cons y ys)
   7.371 +	show ?thesis
   7.372 +	proof (cases j)
   7.373 +	  case 0 with a b Cons.prems show ?thesis by simp
   7.374 +	next
   7.375 +	  case (Suc j') with a b Cons.prems Cons show ?thesis 
   7.376 +	    apply -
   7.377 +	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
   7.378 +	    done
   7.379 +	qed
   7.380 +      qed
   7.381 +    next
   7.382 +      case (Suc n')
   7.383 +      show ?thesis
   7.384 +      proof (cases ys)
   7.385 +	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
   7.386 +      next
   7.387 +	case (Cons y ys) with Suc a Cons.prems show ?thesis
   7.388 +	  apply -
   7.389 +	  apply simp
   7.390 +	  apply (cases j)
   7.391 +	  apply simp
   7.392 +	  apply (cases i)
   7.393 +	  apply simp
   7.394 +	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
   7.395 +	  apply simp
   7.396 +	  apply simp
   7.397 +	  apply simp
   7.398 +	  apply simp
   7.399 +	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
   7.400 +	  apply simp
   7.401 +	  apply simp
   7.402 +	  apply simp
   7.403 +	  done
   7.404 +      qed
   7.405 +    qed
   7.406 +  qed
   7.407 +qed
   7.408 +
   7.409 +lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
   7.410 +by (induct xs arbitrary: i j, auto)
   7.411 +
   7.412 +lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
   7.413 +apply (induct xs arbitrary: a i j)
   7.414 +apply simp
   7.415 +apply (case_tac j)
   7.416 +apply simp
   7.417 +apply (case_tac i)
   7.418 +apply simp
   7.419 +apply simp
   7.420 +done
   7.421 +
   7.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)]"
   7.423 +apply (induct xs arbitrary: a i j)
   7.424 +apply simp
   7.425 +apply simp
   7.426 +apply (case_tac j)
   7.427 +apply simp
   7.428 +apply auto
   7.429 +apply (case_tac nat)
   7.430 +apply auto
   7.431 +done
   7.432 +
   7.433 +(* suffices that j \<le> length xs and length ys *) 
   7.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')"
   7.435 +proof (induct xs arbitrary: ys i j)
   7.436 +  case Nil thus ?case by simp
   7.437 +next
   7.438 +  case (Cons x xs)
   7.439 +  thus ?case
   7.440 +    apply -
   7.441 +    apply (cases ys)
   7.442 +    apply simp
   7.443 +    apply simp
   7.444 +    apply auto
   7.445 +    apply (case_tac i', auto)
   7.446 +    apply (erule_tac x="Suc i'" in allE, auto)
   7.447 +    apply (erule_tac x="i' - 1" in allE, auto)
   7.448 +    apply (case_tac i', auto)
   7.449 +    apply (erule_tac x="Suc i'" in allE, auto)
   7.450 +    done
   7.451 +qed
   7.452 +
   7.453 +lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
   7.454 +by (induct xs, auto)
   7.455 +
   7.456 +lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
   7.457 +by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
   7.458 +
   7.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"
   7.460 +by (induct xs arbitrary: i j k) auto
   7.461 +
   7.462 +lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
   7.463 +apply (induct xs arbitrary: i j k)
   7.464 +apply auto
   7.465 +apply (case_tac k)
   7.466 +apply auto
   7.467 +apply (case_tac i)
   7.468 +apply auto
   7.469 +done
   7.470 +
   7.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}"
   7.472 +apply (simp add: sublist'_sublist)
   7.473 +apply (simp add: set_sublist)
   7.474 +apply auto
   7.475 +done
   7.476 +
   7.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))"
   7.478 +unfolding set_sublist' by blast
   7.479 +
   7.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))"
   7.481 +unfolding set_sublist' by blast
   7.482 +
   7.483 +
   7.484 +lemma multiset_of_sublist:
   7.485 +assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
   7.486 +assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
   7.487 +assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
   7.488 +assumes multiset: "multiset_of xs = multiset_of ys"
   7.489 +  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
   7.490 +proof -
   7.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") 
   7.492 +    by (simp add: sublist'_append)
   7.493 +  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
   7.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") 
   7.495 +    by (simp add: sublist'_append)
   7.496 +  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
   7.497 +  moreover
   7.498 +  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
   7.499 +    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   7.500 +  moreover
   7.501 +  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
   7.502 +    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   7.503 +  moreover
   7.504 +  ultimately show ?thesis by (simp add: multiset_of_append)
   7.505 +qed
   7.506 +
   7.507 +
   7.508 +end
     8.1 --- a/src/HOL/IsaMakefile	Mon Mar 23 15:33:35 2009 +0100
     8.2 +++ b/src/HOL/IsaMakefile	Mon Mar 23 19:01:34 2009 +0100
     8.3 @@ -649,7 +649,11 @@
     8.4  $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
     8.5    Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
     8.6    Imperative_HOL/Relational.thy \
     8.7 -  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy
     8.8 +  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy \
     8.9 +  Imperative_HOL/Imperative_HOL_ex.thy \
    8.10 +  Imperative_HOL/ex/Imperative_Quicksort.thy \
    8.11 +  Imperative_HOL/ex/Subarray.thy \
    8.12 +  Imperative_HOL/ex/Sublist.thy
    8.13  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
    8.14  
    8.15  
    8.16 @@ -836,7 +840,7 @@
    8.17    ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy			\
    8.18    ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
    8.19    ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
    8.20 -  ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy			\
    8.21 +  ex/Hilbert_Classical.thy			\
    8.22    ex/Induction_Scheme.thy ex/InductiveInvariant.thy			\
    8.23    ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
    8.24    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
    8.25 @@ -845,8 +849,8 @@
    8.26    ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML	\
    8.27    ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
    8.28    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    8.29 -  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy		\
    8.30 -  ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
    8.31 +  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
    8.32 +  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
    8.33    ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
    8.34    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
    8.35    ex/Predicate_Compile.thy ex/predicate_compile.ML
     9.1 --- a/src/HOL/NSA/hypreal_arith.ML	Mon Mar 23 15:33:35 2009 +0100
     9.2 +++ b/src/HOL/NSA/hypreal_arith.ML	Mon Mar 23 19:01:34 2009 +0100
     9.3 @@ -30,10 +30,10 @@
     9.4      Simplifier.simproc (the_context ())
     9.5        "fast_hypreal_arith" 
     9.6        ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
     9.7 -    (K LinArith.lin_arith_simproc);
     9.8 +    (K Lin_Arith.lin_arith_simproc);
     9.9  
    9.10  val hypreal_arith_setup =
    9.11 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    9.12 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    9.13     {add_mono_thms = add_mono_thms,
    9.14      mult_mono_thms = mult_mono_thms,
    9.15      inj_thms = real_inj_thms @ inj_thms,
    10.1 --- a/src/HOL/Nat.thy	Mon Mar 23 15:33:35 2009 +0100
    10.2 +++ b/src/HOL/Nat.thy	Mon Mar 23 19:01:34 2009 +0100
    10.3 @@ -63,9 +63,8 @@
    10.4  end
    10.5  
    10.6  lemma Suc_not_Zero: "Suc m \<noteq> 0"
    10.7 -  apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
    10.8 +  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
    10.9      Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
   10.10 -  done
   10.11  
   10.12  lemma Zero_not_Suc: "0 \<noteq> Suc m"
   10.13    by (rule not_sym, rule Suc_not_Zero not_sym)
   10.14 @@ -82,7 +81,7 @@
   10.15    done
   10.16  
   10.17  lemma nat_induct [case_names 0 Suc, induct type: nat]:
   10.18 -  -- {* for backward compatibility -- naming of variables differs *}
   10.19 +  -- {* for backward compatibility -- names of variables differ *}
   10.20    fixes n
   10.21    assumes "P 0"
   10.22      and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   10.23 @@ -1345,19 +1344,13 @@
   10.24    shows "u = s"
   10.25    using 2 1 by (rule trans)
   10.26  
   10.27 +setup Arith_Data.setup
   10.28 +
   10.29  use "Tools/nat_arith.ML"
   10.30  declaration {* K Nat_Arith.setup *}
   10.31  
   10.32 -ML{*
   10.33 -structure ArithFacts =
   10.34 -  NamedThmsFun(val name = "arith"
   10.35 -               val description = "arith facts - only ground formulas");
   10.36 -*}
   10.37 -
   10.38 -setup ArithFacts.setup
   10.39 -
   10.40  use "Tools/lin_arith.ML"
   10.41 -declaration {* K LinArith.setup *}
   10.42 +declaration {* K Lin_Arith.setup *}
   10.43  
   10.44  lemmas [arith_split] = nat_diff_split split_min split_max
   10.45  
    11.1 --- a/src/HOL/NatBin.thy	Mon Mar 23 15:33:35 2009 +0100
    11.2 +++ b/src/HOL/NatBin.thy	Mon Mar 23 19:01:34 2009 +0100
    11.3 @@ -651,7 +651,7 @@
    11.4  val numeral_ss = @{simpset} addsimps @{thms numerals};
    11.5  
    11.6  val nat_bin_arith_setup =
    11.7 - LinArith.map_data
    11.8 + Lin_Arith.map_data
    11.9     (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   11.10       {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   11.11        inj_thms = inj_thms,
    12.1 --- a/src/HOL/Presburger.thy	Mon Mar 23 15:33:35 2009 +0100
    12.2 +++ b/src/HOL/Presburger.thy	Mon Mar 23 19:01:34 2009 +0100
    12.3 @@ -439,12 +439,7 @@
    12.4  
    12.5  use "Tools/Qelim/presburger.ML"
    12.6  
    12.7 -declaration {* fn _ =>
    12.8 -  arith_tactic_add
    12.9 -    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
   12.10 -       (warning "Trying Presburger arithmetic ...";   
   12.11 -    Presburger.cooper_tac true [] [] ctxt i st)))
   12.12 -*}
   12.13 +setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
   12.14  
   12.15  method_setup presburger = {*
   12.16  let
    13.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 23 15:33:35 2009 +0100
    13.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 23 19:01:34 2009 +0100
    13.3 @@ -172,7 +172,7 @@
    13.4  
    13.5      (* Canonical linear form for terms, formulae etc.. *)
    13.6  fun provelin ctxt t = Goal.prove ctxt [] [] t 
    13.7 -  (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
    13.8 +  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
    13.9  fun linear_cmul 0 tm = zero 
   13.10    | linear_cmul n tm = case tm of  
   13.11        Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
    14.1 --- a/src/HOL/Tools/TFL/post.ML	Mon Mar 23 15:33:35 2009 +0100
    14.2 +++ b/src/HOL/Tools/TFL/post.ML	Mon Mar 23 19:01:34 2009 +0100
    14.3 @@ -55,7 +55,7 @@
    14.4    Prim.postprocess strict
    14.5     {wf_tac     = REPEAT (ares_tac wfs 1),
    14.6      terminator = asm_simp_tac ss 1
    14.7 -                 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE
    14.8 +                 THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE
    14.9                             fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
   14.10      simplifier = Rules.simpl_conv ss []};
   14.11  
    15.1 --- a/src/HOL/Tools/arith_data.ML	Mon Mar 23 15:33:35 2009 +0100
    15.2 +++ b/src/HOL/Tools/arith_data.ML	Mon Mar 23 19:01:34 2009 +0100
    15.3 @@ -6,6 +6,11 @@
    15.4  
    15.5  signature ARITH_DATA =
    15.6  sig
    15.7 +  val arith_tac: Proof.context -> int -> tactic
    15.8 +  val verbose_arith_tac: Proof.context -> int -> tactic
    15.9 +  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
   15.10 +  val get_arith_facts: Proof.context -> thm list
   15.11 +
   15.12    val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
   15.13    val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   15.14    val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
   15.15 @@ -14,11 +19,54 @@
   15.16    val trans_tac: thm option -> tactic
   15.17    val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
   15.18      -> simproc
   15.19 +
   15.20 +  val setup: theory -> theory
   15.21  end;
   15.22  
   15.23  structure Arith_Data: ARITH_DATA =
   15.24  struct
   15.25  
   15.26 +(* slots for pluging in arithmetic facts and tactics *)
   15.27 +
   15.28 +structure Arith_Facts = NamedThmsFun(
   15.29 +  val name = "arith"
   15.30 +  val description = "arith facts - only ground formulas"
   15.31 +);
   15.32 +
   15.33 +val get_arith_facts = Arith_Facts.get;
   15.34 +
   15.35 +structure Arith_Tactics = TheoryDataFun
   15.36 +(
   15.37 +  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
   15.38 +  val empty = [];
   15.39 +  val copy = I;
   15.40 +  val extend = I;
   15.41 +  fun merge _ = AList.merge (op =) (K true);
   15.42 +);
   15.43 +
   15.44 +fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
   15.45 +
   15.46 +fun gen_arith_tac verbose ctxt =
   15.47 +  let
   15.48 +    val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
   15.49 +    fun invoke (_, (name, tac)) k st = (if verbose
   15.50 +      then warning ("Trying " ^ name ^ "...") else ();
   15.51 +      tac verbose ctxt k st);
   15.52 +  in FIRST' (map invoke (rev tactics)) end;
   15.53 +
   15.54 +val arith_tac = gen_arith_tac false;
   15.55 +val verbose_arith_tac = gen_arith_tac true;
   15.56 +
   15.57 +val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
   15.58 +  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
   15.59 +    THEN' verbose_arith_tac ctxt)));
   15.60 +
   15.61 +val setup = Arith_Facts.setup
   15.62 +  #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
   15.63 +
   15.64 +
   15.65 +(* various auxiliary and legacy *)
   15.66 +
   15.67  fun prove_conv_nohyps tacs ctxt (t, u) =
   15.68    if t aconv u then NONE
   15.69    else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    16.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 15:33:35 2009 +0100
    16.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 19:01:34 2009 +0100
    16.3 @@ -197,7 +197,7 @@
    16.4                else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
    16.5            in
    16.6              rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
    16.7 -            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
    16.8 +            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
    16.9            end
   16.10  
   16.11          fun steps_tac MAX strict lq lp =
    17.1 --- a/src/HOL/Tools/int_arith.ML	Mon Mar 23 15:33:35 2009 +0100
    17.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Mar 23 19:01:34 2009 +0100
    17.3 @@ -530,7 +530,7 @@
    17.4    :: Int_Numeral_Simprocs.cancel_numerals;
    17.5  
    17.6  val setup =
    17.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    17.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    17.9     {add_mono_thms = add_mono_thms,
   17.10      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
   17.11      inj_thms = nat_inj_thms @ inj_thms,
   17.12 @@ -547,7 +547,7 @@
   17.13    "fast_int_arith" 
   17.14       ["(m::'a::{ordered_idom,number_ring}) < n",
   17.15        "(m::'a::{ordered_idom,number_ring}) <= n",
   17.16 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
   17.17 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
   17.18  
   17.19  end;
   17.20  
    18.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Mon Mar 23 15:33:35 2009 +0100
    18.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Mon Mar 23 19:01:34 2009 +0100
    18.3 @@ -232,7 +232,7 @@
    18.4        val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
    18.5        val pos = less $ zero $ t and neg = less $ t $ zero
    18.6        fun prove p =
    18.7 -        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
    18.8 +        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
    18.9          handle THM _ => NONE
   18.10      in case prove pos of
   18.11           SOME th => SOME(th RS pos_th)
    19.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Mar 23 15:33:35 2009 +0100
    19.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 23 19:01:34 2009 +0100
    19.3 @@ -6,13 +6,9 @@
    19.4  
    19.5  signature BASIC_LIN_ARITH =
    19.6  sig
    19.7 -  type arith_tactic
    19.8 -  val mk_arith_tactic: string -> (Proof.context -> int -> tactic) -> arith_tactic
    19.9 -  val eq_arith_tactic: arith_tactic * arith_tactic -> bool
   19.10    val arith_split_add: attribute
   19.11    val arith_discrete: string -> Context.generic -> Context.generic
   19.12    val arith_inj_const: string * typ -> Context.generic -> Context.generic
   19.13 -  val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic
   19.14    val fast_arith_split_limit: int Config.T
   19.15    val fast_arith_neq_limit: int Config.T
   19.16    val lin_arith_pre_tac: Proof.context -> int -> tactic
   19.17 @@ -21,9 +17,7 @@
   19.18    val trace_arith: bool ref
   19.19    val lin_arith_simproc: simpset -> term -> thm option
   19.20    val fast_nat_arith_simproc: simproc
   19.21 -  val simple_arith_tac: Proof.context -> int -> tactic
   19.22 -  val arith_tac: Proof.context -> int -> tactic
   19.23 -  val silent_arith_tac: Proof.context -> int -> tactic
   19.24 +  val linear_arith_tac: Proof.context -> int -> tactic
   19.25  end;
   19.26  
   19.27  signature LIN_ARITH =
   19.28 @@ -39,7 +33,7 @@
   19.29    val setup: Context.generic -> Context.generic
   19.30  end;
   19.31  
   19.32 -structure LinArith: LIN_ARITH =
   19.33 +structure Lin_Arith: LIN_ARITH =
   19.34  struct
   19.35  
   19.36  (* Parameters data for general linear arithmetic functor *)
   19.37 @@ -72,7 +66,7 @@
   19.38    let val _ $ t = Thm.prop_of thm
   19.39    in t = Const("False",HOLogic.boolT) end;
   19.40  
   19.41 -fun is_nat(t) = fastype_of1 t = HOLogic.natT;
   19.42 +fun is_nat t = (fastype_of1 t = HOLogic.natT);
   19.43  
   19.44  fun mk_nat_thm sg t =
   19.45    let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   19.46 @@ -83,49 +77,35 @@
   19.47  
   19.48  (* arith context data *)
   19.49  
   19.50 -datatype arith_tactic =
   19.51 -  ArithTactic of {name: string, tactic: Proof.context -> int -> tactic, id: stamp};
   19.52 -
   19.53 -fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()};
   19.54 -
   19.55 -fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
   19.56 -
   19.57  structure ArithContextData = GenericDataFun
   19.58  (
   19.59    type T = {splits: thm list,
   19.60              inj_consts: (string * typ) list,
   19.61 -            discrete: string list,
   19.62 -            tactics: arith_tactic list};
   19.63 -  val empty = {splits = [], inj_consts = [], discrete = [], tactics = []};
   19.64 +            discrete: string list};
   19.65 +  val empty = {splits = [], inj_consts = [], discrete = []};
   19.66    val extend = I;
   19.67    fun merge _
   19.68 -   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
   19.69 -    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T =
   19.70 +   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
   19.71 +    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
   19.72     {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
   19.73      inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
   19.74 -    discrete = Library.merge (op =) (discrete1, discrete2),
   19.75 -    tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
   19.76 +    discrete = Library.merge (op =) (discrete1, discrete2)};
   19.77  );
   19.78  
   19.79  val get_arith_data = ArithContextData.get o Context.Proof;
   19.80  
   19.81  val arith_split_add = Thm.declaration_attribute (fn thm =>
   19.82 -  ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
   19.83 +  ArithContextData.map (fn {splits, inj_consts, discrete} =>
   19.84      {splits = update Thm.eq_thm_prop thm splits,
   19.85 -     inj_consts = inj_consts, discrete = discrete, tactics = tactics}));
   19.86 -
   19.87 -fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
   19.88 -  {splits = splits, inj_consts = inj_consts,
   19.89 -   discrete = update (op =) d discrete, tactics = tactics});
   19.90 +     inj_consts = inj_consts, discrete = discrete}));
   19.91  
   19.92 -fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
   19.93 -  {splits = splits, inj_consts = update (op =) c inj_consts,
   19.94 -   discrete = discrete, tactics= tactics});
   19.95 +fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
   19.96 +  {splits = splits, inj_consts = inj_consts,
   19.97 +   discrete = update (op =) d discrete});
   19.98  
   19.99 -fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
  19.100 -  {splits = splits, inj_consts = inj_consts, discrete = discrete,
  19.101 -   tactics = update eq_arith_tactic tac tactics});
  19.102 -
  19.103 +fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
  19.104 +  {splits = splits, inj_consts = update (op =) c inj_consts,
  19.105 +   discrete = discrete});
  19.106  
  19.107  val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
  19.108  val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
  19.109 @@ -794,7 +774,7 @@
  19.110     Most of the work is done by the cancel tactics. *)
  19.111  
  19.112  val init_arith_data =
  19.113 - Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
  19.114 + map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
  19.115     {add_mono_thms = add_mono_thms @
  19.116      @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
  19.117      mult_mono_thms = mult_mono_thms,
  19.118 @@ -815,7 +795,7 @@
  19.119    arith_discrete "nat";
  19.120  
  19.121  fun add_arith_facts ss =
  19.122 -  add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;
  19.123 +  add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
  19.124  
  19.125  val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
  19.126  
  19.127 @@ -895,27 +875,16 @@
  19.128      (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
  19.129      (fast_ex_arith_tac ctxt ex);
  19.130  
  19.131 -fun more_arith_tacs ctxt =
  19.132 -  let val tactics = #tactics (get_arith_data ctxt)
  19.133 -  in FIRST' (map (fn ArithTactic {tactic, ...} => tactic ctxt) tactics) end;
  19.134 -
  19.135  in
  19.136  
  19.137 -fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
  19.138 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true];
  19.139 -
  19.140 -fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
  19.141 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true,
  19.142 -  more_arith_tacs ctxt];
  19.143 +fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
  19.144 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
  19.145  
  19.146 -fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
  19.147 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false,
  19.148 -  more_arith_tacs ctxt];
  19.149 +val linear_arith_tac = gen_linear_arith_tac true;
  19.150  
  19.151 -val arith_method = Args.bang_facts >>
  19.152 -  (fn prems => fn ctxt => METHOD (fn facts =>
  19.153 -      HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
  19.154 -      THEN' arith_tac ctxt)));
  19.155 +val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
  19.156 +  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
  19.157 +    THEN' linear_arith_tac ctxt)));
  19.158  
  19.159  end;
  19.160  
  19.161 @@ -929,11 +898,12 @@
  19.162        (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
  19.163    Context.mapping
  19.164     (setup_options #>
  19.165 -    Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
  19.166 +    Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
  19.167 +    Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
  19.168      Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
  19.169        "declaration of split rules for arithmetic procedure") I;
  19.170  
  19.171  end;
  19.172  
  19.173 -structure BasicLinArith: BASIC_LIN_ARITH = LinArith;
  19.174 -open BasicLinArith;
  19.175 +structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
  19.176 +open Basic_Lin_Arith;
    20.1 --- a/src/HOL/Tools/nat_simprocs.ML	Mon Mar 23 15:33:35 2009 +0100
    20.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Mon Mar 23 19:01:34 2009 +0100
    20.3 @@ -565,7 +565,7 @@
    20.4  in
    20.5  
    20.6  val nat_simprocs_setup =
    20.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    20.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    20.9     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   20.10      inj_thms = inj_thms, lessD = lessD, neqE = neqE,
   20.11      simpset = simpset addsimps add_rules
    21.1 --- a/src/HOL/Tools/rat_arith.ML	Mon Mar 23 15:33:35 2009 +0100
    21.2 +++ b/src/HOL/Tools/rat_arith.ML	Mon Mar 23 19:01:34 2009 +0100
    21.3 @@ -35,7 +35,7 @@
    21.4  in
    21.5  
    21.6  val rat_arith_setup =
    21.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    21.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    21.9     {add_mono_thms = add_mono_thms,
   21.10      mult_mono_thms = mult_mono_thms,
   21.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    22.1 --- a/src/HOL/Tools/real_arith.ML	Mon Mar 23 15:33:35 2009 +0100
    22.2 +++ b/src/HOL/Tools/real_arith.ML	Mon Mar 23 19:01:34 2009 +0100
    22.3 @@ -29,7 +29,7 @@
    22.4  in
    22.5  
    22.6  val real_arith_setup =
    22.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    22.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    22.9     {add_mono_thms = add_mono_thms,
   22.10      mult_mono_thms = mult_mono_thms,
   22.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    23.1 --- a/src/HOL/Word/WordArith.thy	Mon Mar 23 15:33:35 2009 +0100
    23.2 +++ b/src/HOL/Word/WordArith.thy	Mon Mar 23 19:01:34 2009 +0100
    23.3 @@ -512,7 +512,7 @@
    23.4  
    23.5  fun uint_arith_tacs ctxt = 
    23.6    let
    23.7 -    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
    23.8 +    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
    23.9      val cs = local_claset_of ctxt;
   23.10      val ss = local_simpset_of ctxt;
   23.11    in 
   23.12 @@ -1075,7 +1075,7 @@
   23.13  
   23.14  fun unat_arith_tacs ctxt =   
   23.15    let
   23.16 -    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
   23.17 +    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
   23.18      val cs = local_claset_of ctxt;
   23.19      val ss = local_simpset_of ctxt;
   23.20    in 
    24.1 --- a/src/HOL/ex/Arith_Examples.thy	Mon Mar 23 15:33:35 2009 +0100
    24.2 +++ b/src/HOL/ex/Arith_Examples.thy	Mon Mar 23 19:01:34 2009 +0100
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:  HOL/ex/Arith_Examples.thy
    24.5 -    ID:     $Id$
    24.6      Author: Tjark Weber
    24.7  *)
    24.8  
    24.9 @@ -14,13 +13,13 @@
   24.10  
   24.11    @{ML fast_arith_tac} is a very basic version of the tactic.  It performs no
   24.12    meta-to-object-logic conversion, and only some splitting of operators.
   24.13 -  @{ML simple_arith_tac} performs meta-to-object-logic conversion, full
   24.14 +  @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
   24.15    splitting of operators, and NNF normalization of the goal.  The @{text arith}
   24.16    method combines them both, and tries other methods (e.g.~@{text presburger})
   24.17    as well.  This is the one that you should use in your proofs!
   24.18  
   24.19    An @{text arith}-based simproc is available as well (see @{ML
   24.20 -  LinArith.lin_arith_simproc}), which---for performance
   24.21 +  Lin_Arith.lin_arith_simproc}), which---for performance
   24.22    reasons---however does even less splitting than @{ML fast_arith_tac}
   24.23    at the moment (namely inequalities only).  (On the other hand, it
   24.24    does take apart conjunctions, which @{ML fast_arith_tac} currently
   24.25 @@ -83,7 +82,7 @@
   24.26    by (tactic {* fast_arith_tac @{context} 1 *})
   24.27  
   24.28  lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
   24.29 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.30 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.31  
   24.32  lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
   24.33    by (tactic {* fast_arith_tac @{context} 1 *})
   24.34 @@ -140,34 +139,34 @@
   24.35  subsection {* Meta-Logic *}
   24.36  
   24.37  lemma "x < Suc y == x <= y"
   24.38 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.39 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.40  
   24.41  lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
   24.42 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.43 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.44  
   24.45  
   24.46  subsection {* Various Other Examples *}
   24.47  
   24.48  lemma "(x < Suc y) = (x <= y)"
   24.49 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.50 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.51  
   24.52  lemma "[| (x::nat) < y; y < z |] ==> x < z"
   24.53    by (tactic {* fast_arith_tac @{context} 1 *})
   24.54  
   24.55  lemma "(x::nat) < y & y < z ==> x < z"
   24.56 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.57 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.58  
   24.59  text {* This example involves no arithmetic at all, but is solved by
   24.60    preprocessing (i.e. NNF normalization) alone. *}
   24.61  
   24.62  lemma "(P::bool) = Q ==> Q = P"
   24.63 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.64 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.65  
   24.66  lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
   24.67 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.68 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.69  
   24.70  lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
   24.71 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.72 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.73  
   24.74  lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
   24.75    by (tactic {* fast_arith_tac @{context} 1 *})
   24.76 @@ -185,7 +184,7 @@
   24.77    by (tactic {* fast_arith_tac @{context} 1 *})
   24.78  
   24.79  lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
   24.80 -  by (tactic {* simple_arith_tac @{context} 1 *})
   24.81 +  by (tactic {* linear_arith_tac @{context} 1 *})
   24.82  
   24.83  lemma "(x - y) - (x::nat) = (x - x) - y"
   24.84    by (tactic {* fast_arith_tac @{context} 1 *})
   24.85 @@ -207,7 +206,7 @@
   24.86  (*        preprocessing negates the goal and tries to compute its negation *)
   24.87  (*        normal form, which creates lots of separate cases for this       *)
   24.88  (*        disjunction of conjunctions                                      *)
   24.89 -(* by (tactic {* simple_arith_tac 1 *}) *)
   24.90 +(* by (tactic {* linear_arith_tac 1 *}) *)
   24.91  oops
   24.92  
   24.93  lemma "2 * (x::nat) ~= 1"
    25.1 --- a/src/HOL/ex/ImperativeQuicksort.thy	Mon Mar 23 15:33:35 2009 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,637 +0,0 @@
    25.4 -theory ImperativeQuicksort
    25.5 -imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
    25.6 -begin
    25.7 -
    25.8 -text {* We prove QuickSort correct in the Relational Calculus. *}
    25.9 -
   25.10 -definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
   25.11 -where
   25.12 -  "swap arr i j = (
   25.13 -     do
   25.14 -       x \<leftarrow> nth arr i;
   25.15 -       y \<leftarrow> nth arr j;
   25.16 -       upd i y arr;
   25.17 -       upd j x arr;
   25.18 -       return ()
   25.19 -     done)"
   25.20 -
   25.21 -lemma swap_permutes:
   25.22 -  assumes "crel (swap a i j) h h' rs"
   25.23 -  shows "multiset_of (get_array a h') 
   25.24 -  = multiset_of (get_array a h)"
   25.25 -  using assms
   25.26 -  unfolding swap_def
   25.27 -  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
   25.28 -
   25.29 -function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
   25.30 -where
   25.31 -  "part1 a left right p = (
   25.32 -     if (right \<le> left) then return right
   25.33 -     else (do
   25.34 -       v \<leftarrow> nth a left;
   25.35 -       (if (v \<le> p) then (part1 a (left + 1) right p)
   25.36 -                    else (do swap a left right;
   25.37 -  part1 a left (right - 1) p done))
   25.38 -     done))"
   25.39 -by pat_completeness auto
   25.40 -
   25.41 -termination
   25.42 -by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
   25.43 -
   25.44 -declare part1.simps[simp del]
   25.45 -
   25.46 -lemma part_permutes:
   25.47 -  assumes "crel (part1 a l r p) h h' rs"
   25.48 -  shows "multiset_of (get_array a h') 
   25.49 -  = multiset_of (get_array a h)"
   25.50 -  using assms
   25.51 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   25.52 -  case (1 a l r p h h' rs)
   25.53 -  thus ?case
   25.54 -    unfolding part1.simps [of a l r p]
   25.55 -    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
   25.56 -qed
   25.57 -
   25.58 -lemma part_returns_index_in_bounds:
   25.59 -  assumes "crel (part1 a l r p) h h' rs"
   25.60 -  assumes "l \<le> r"
   25.61 -  shows "l \<le> rs \<and> rs \<le> r"
   25.62 -using assms
   25.63 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   25.64 -  case (1 a l r p h h' rs)
   25.65 -  note cr = `crel (part1 a l r p) h h' rs`
   25.66 -  show ?case
   25.67 -  proof (cases "r \<le> l")
   25.68 -    case True (* Terminating case *)
   25.69 -    with cr `l \<le> r` show ?thesis
   25.70 -      unfolding part1.simps[of a l r p]
   25.71 -      by (elim crelE crel_if crel_return crel_nth) auto
   25.72 -  next
   25.73 -    case False (* recursive case *)
   25.74 -    note rec_condition = this
   25.75 -    let ?v = "get_array a h ! l"
   25.76 -    show ?thesis
   25.77 -    proof (cases "?v \<le> p")
   25.78 -      case True
   25.79 -      with cr False
   25.80 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   25.81 -        unfolding part1.simps[of a l r p]
   25.82 -        by (elim crelE crel_nth crel_if crel_return) auto
   25.83 -      from rec_condition have "l + 1 \<le> r" by arith
   25.84 -      from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
   25.85 -      show ?thesis by simp
   25.86 -    next
   25.87 -      case False
   25.88 -      with rec_condition cr
   25.89 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   25.90 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   25.91 -        unfolding part1.simps[of a l r p]
   25.92 -        by (elim crelE crel_nth crel_if crel_return) auto
   25.93 -      from rec_condition have "l \<le> r - 1" by arith
   25.94 -      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
   25.95 -    qed
   25.96 -  qed
   25.97 -qed
   25.98 -
   25.99 -lemma part_length_remains:
  25.100 -  assumes "crel (part1 a l r p) h h' rs"
  25.101 -  shows "Heap.length a h = Heap.length a h'"
  25.102 -using assms
  25.103 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  25.104 -  case (1 a l r p h h' rs)
  25.105 -  note cr = `crel (part1 a l r p) h h' rs`
  25.106 -  
  25.107 -  show ?case
  25.108 -  proof (cases "r \<le> l")
  25.109 -    case True (* Terminating case *)
  25.110 -    with cr show ?thesis
  25.111 -      unfolding part1.simps[of a l r p]
  25.112 -      by (elim crelE crel_if crel_return crel_nth) auto
  25.113 -  next
  25.114 -    case False (* recursive case *)
  25.115 -    with cr 1 show ?thesis
  25.116 -      unfolding part1.simps [of a l r p] swap_def
  25.117 -      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
  25.118 -  qed
  25.119 -qed
  25.120 -
  25.121 -lemma part_outer_remains:
  25.122 -  assumes "crel (part1 a l r p) h h' rs"
  25.123 -  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
  25.124 -  using assms
  25.125 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  25.126 -  case (1 a l r p h h' rs)
  25.127 -  note cr = `crel (part1 a l r p) h h' rs`
  25.128 -  
  25.129 -  show ?case
  25.130 -  proof (cases "r \<le> l")
  25.131 -    case True (* Terminating case *)
  25.132 -    with cr show ?thesis
  25.133 -      unfolding part1.simps[of a l r p]
  25.134 -      by (elim crelE crel_if crel_return crel_nth) auto
  25.135 -  next
  25.136 -    case False (* recursive case *)
  25.137 -    note rec_condition = this
  25.138 -    let ?v = "get_array a h ! l"
  25.139 -    show ?thesis
  25.140 -    proof (cases "?v \<le> p")
  25.141 -      case True
  25.142 -      with cr False
  25.143 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
  25.144 -        unfolding part1.simps[of a l r p]
  25.145 -        by (elim crelE crel_nth crel_if crel_return) auto
  25.146 -      from 1(1)[OF rec_condition True rec1]
  25.147 -      show ?thesis by fastsimp
  25.148 -    next
  25.149 -      case False
  25.150 -      with rec_condition cr
  25.151 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
  25.152 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
  25.153 -        unfolding part1.simps[of a l r p]
  25.154 -        by (elim crelE crel_nth crel_if crel_return) auto
  25.155 -      from swp rec_condition have
  25.156 -        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
  25.157 -	unfolding swap_def
  25.158 -	by (elim crelE crel_nth crel_upd crel_return) auto
  25.159 -      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
  25.160 -    qed
  25.161 -  qed
  25.162 -qed
  25.163 -
  25.164 -
  25.165 -lemma part_partitions:
  25.166 -  assumes "crel (part1 a l r p) h h' rs"
  25.167 -  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
  25.168 -  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
  25.169 -  using assms
  25.170 -proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
  25.171 -  case (1 a l r p h h' rs)
  25.172 -  note cr = `crel (part1 a l r p) h h' rs`
  25.173 -  
  25.174 -  show ?case
  25.175 -  proof (cases "r \<le> l")
  25.176 -    case True (* Terminating case *)
  25.177 -    with cr have "rs = r"
  25.178 -      unfolding part1.simps[of a l r p]
  25.179 -      by (elim crelE crel_if crel_return crel_nth) auto
  25.180 -    with True
  25.181 -    show ?thesis by auto
  25.182 -  next
  25.183 -    case False (* recursive case *)
  25.184 -    note lr = this
  25.185 -    let ?v = "get_array a h ! l"
  25.186 -    show ?thesis
  25.187 -    proof (cases "?v \<le> p")
  25.188 -      case True
  25.189 -      with lr cr
  25.190 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
  25.191 -        unfolding part1.simps[of a l r p]
  25.192 -        by (elim crelE crel_nth crel_if crel_return) auto
  25.193 -      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
  25.194 -	by fastsimp
  25.195 -      have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
  25.196 -      with 1(1)[OF False True rec1] a_l show ?thesis
  25.197 -	by auto
  25.198 -    next
  25.199 -      case False
  25.200 -      with lr cr
  25.201 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
  25.202 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
  25.203 -        unfolding part1.simps[of a l r p]
  25.204 -        by (elim crelE crel_nth crel_if crel_return) auto
  25.205 -      from swp False have "get_array a h1 ! r \<ge> p"
  25.206 -	unfolding swap_def
  25.207 -	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
  25.208 -      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
  25.209 -	by fastsimp
  25.210 -      have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
  25.211 -      with 1(2)[OF lr False rec2] a_r show ?thesis
  25.212 -	by auto
  25.213 -    qed
  25.214 -  qed
  25.215 -qed
  25.216 -
  25.217 -
  25.218 -fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
  25.219 -where
  25.220 -  "partition a left right = (do
  25.221 -     pivot \<leftarrow> nth a right;
  25.222 -     middle \<leftarrow> part1 a left (right - 1) pivot;
  25.223 -     v \<leftarrow> nth a middle;
  25.224 -     m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
  25.225 -     swap a m right;
  25.226 -     return m
  25.227 -   done)"
  25.228 -
  25.229 -declare partition.simps[simp del]
  25.230 -
  25.231 -lemma partition_permutes:
  25.232 -  assumes "crel (partition a l r) h h' rs"
  25.233 -  shows "multiset_of (get_array a h') 
  25.234 -  = multiset_of (get_array a h)"
  25.235 -proof -
  25.236 -    from assms part_permutes swap_permutes show ?thesis
  25.237 -      unfolding partition.simps
  25.238 -      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
  25.239 -qed
  25.240 -
  25.241 -lemma partition_length_remains:
  25.242 -  assumes "crel (partition a l r) h h' rs"
  25.243 -  shows "Heap.length a h = Heap.length a h'"
  25.244 -proof -
  25.245 -  from assms part_length_remains show ?thesis
  25.246 -    unfolding partition.simps swap_def
  25.247 -    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
  25.248 -qed
  25.249 -
  25.250 -lemma partition_outer_remains:
  25.251 -  assumes "crel (partition a l r) h h' rs"
  25.252 -  assumes "l < r"
  25.253 -  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
  25.254 -proof -
  25.255 -  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
  25.256 -    unfolding partition.simps swap_def
  25.257 -    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
  25.258 -qed
  25.259 -
  25.260 -lemma partition_returns_index_in_bounds:
  25.261 -  assumes crel: "crel (partition a l r) h h' rs"
  25.262 -  assumes "l < r"
  25.263 -  shows "l \<le> rs \<and> rs \<le> r"
  25.264 -proof -
  25.265 -  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
  25.266 -    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
  25.267 -         else middle)"
  25.268 -    unfolding partition.simps
  25.269 -    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
  25.270 -  from `l < r` have "l \<le> r - 1" by arith
  25.271 -  from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
  25.272 -qed
  25.273 -
  25.274 -lemma partition_partitions:
  25.275 -  assumes crel: "crel (partition a l r) h h' rs"
  25.276 -  assumes "l < r"
  25.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>
  25.278 -  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
  25.279 -proof -
  25.280 -  let ?pivot = "get_array a h ! r" 
  25.281 -  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
  25.282 -    and swap: "crel (swap a rs r) h1 h' ()"
  25.283 -    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
  25.284 -         else middle)"
  25.285 -    unfolding partition.simps
  25.286 -    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
  25.287 -  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
  25.288 -    (Heap.upd a rs (get_array a h1 ! r) h1)"
  25.289 -    unfolding swap_def
  25.290 -    by (elim crelE crel_return crel_nth crel_upd) simp
  25.291 -  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
  25.292 -    unfolding swap_def
  25.293 -    by (elim crelE crel_return crel_nth crel_upd) simp
  25.294 -  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
  25.295 -    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
  25.296 -  from `l < r` have "l \<le> r - 1" by simp 
  25.297 -  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
  25.298 -  from part_outer_remains[OF part] `l < r`
  25.299 -  have "get_array a h ! r = get_array a h1 ! r"
  25.300 -    by fastsimp
  25.301 -  with swap
  25.302 -  have right_remains: "get_array a h ! r = get_array a h' ! rs"
  25.303 -    unfolding swap_def
  25.304 -    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
  25.305 -  from part_partitions [OF part]
  25.306 -  show ?thesis
  25.307 -  proof (cases "get_array a h1 ! middle \<le> ?pivot")
  25.308 -    case True
  25.309 -    with rs_equals have rs_equals: "rs = middle + 1" by simp
  25.310 -    { 
  25.311 -      fix i
  25.312 -      assume i_is_left: "l \<le> i \<and> i < rs"
  25.313 -      with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
  25.314 -      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
  25.315 -      from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
  25.316 -      with part_partitions[OF part] right_remains True
  25.317 -      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
  25.318 -      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
  25.319 -	unfolding Heap.upd_def Heap.length_def by simp
  25.320 -    }
  25.321 -    moreover
  25.322 -    {
  25.323 -      fix i
  25.324 -      assume "rs < i \<and> i \<le> r"
  25.325 -
  25.326 -      hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
  25.327 -      hence "get_array a h' ! rs \<le> get_array a h' ! i"
  25.328 -      proof
  25.329 -	assume i_is: "rs < i \<and> i \<le> r - 1"
  25.330 -	with swap_length_remains in_bounds middle_in_bounds rs_equals
  25.331 -	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
  25.332 -	from part_partitions[OF part] rs_equals right_remains i_is
  25.333 -	have "get_array a h' ! rs \<le> get_array a h1 ! i"
  25.334 -	  by fastsimp
  25.335 -	with i_props h'_def show ?thesis by fastsimp
  25.336 -      next
  25.337 -	assume i_is: "rs < i \<and> i = r"
  25.338 -	with rs_equals have "Suc middle \<noteq> r" by arith
  25.339 -	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
  25.340 -	with part_partitions[OF part] right_remains 
  25.341 -	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
  25.342 -	  by fastsimp
  25.343 -	with i_is True rs_equals right_remains h'_def
  25.344 -	show ?thesis using in_bounds
  25.345 -	  unfolding Heap.upd_def Heap.length_def
  25.346 -	  by auto
  25.347 -      qed
  25.348 -    }
  25.349 -    ultimately show ?thesis by auto
  25.350 -  next
  25.351 -    case False
  25.352 -    with rs_equals have rs_equals: "middle = rs" by simp
  25.353 -    { 
  25.354 -      fix i
  25.355 -      assume i_is_left: "l \<le> i \<and> i < rs"
  25.356 -      with swap_length_remains in_bounds middle_in_bounds rs_equals
  25.357 -      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
  25.358 -      from part_partitions[OF part] rs_equals right_remains i_is_left
  25.359 -      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
  25.360 -      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
  25.361 -	unfolding Heap.upd_def by simp
  25.362 -    }
  25.363 -    moreover
  25.364 -    {
  25.365 -      fix i
  25.366 -      assume "rs < i \<and> i \<le> r"
  25.367 -      hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
  25.368 -      hence "get_array a h' ! rs \<le> get_array a h' ! i"
  25.369 -      proof
  25.370 -	assume i_is: "rs < i \<and> i \<le> r - 1"
  25.371 -	with swap_length_remains in_bounds middle_in_bounds rs_equals
  25.372 -	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
  25.373 -	from part_partitions[OF part] rs_equals right_remains i_is
  25.374 -	have "get_array a h' ! rs \<le> get_array a h1 ! i"
  25.375 -	  by fastsimp
  25.376 -	with i_props h'_def show ?thesis by fastsimp
  25.377 -      next
  25.378 -	assume i_is: "i = r"
  25.379 -	from i_is False rs_equals right_remains h'_def
  25.380 -	show ?thesis using in_bounds
  25.381 -	  unfolding Heap.upd_def Heap.length_def
  25.382 -	  by auto
  25.383 -      qed
  25.384 -    }
  25.385 -    ultimately
  25.386 -    show ?thesis by auto
  25.387 -  qed
  25.388 -qed
  25.389 -
  25.390 -
  25.391 -function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
  25.392 -where
  25.393 -  "quicksort arr left right =
  25.394 -     (if (right > left)  then
  25.395 -        do
  25.396 -          pivotNewIndex \<leftarrow> partition arr left right;
  25.397 -          pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
  25.398 -          quicksort arr left (pivotNewIndex - 1);
  25.399 -          quicksort arr (pivotNewIndex + 1) right
  25.400 -        done
  25.401 -     else return ())"
  25.402 -by pat_completeness auto
  25.403 -
  25.404 -(* For termination, we must show that the pivotNewIndex is between left and right *) 
  25.405 -termination
  25.406 -by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
  25.407 -
  25.408 -declare quicksort.simps[simp del]
  25.409 -
  25.410 -
  25.411 -lemma quicksort_permutes:
  25.412 -  assumes "crel (quicksort a l r) h h' rs"
  25.413 -  shows "multiset_of (get_array a h') 
  25.414 -  = multiset_of (get_array a h)"
  25.415 -  using assms
  25.416 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  25.417 -  case (1 a l r h h' rs)
  25.418 -  with partition_permutes show ?case
  25.419 -    unfolding quicksort.simps [of a l r]
  25.420 -    by (elim crel_if crelE crel_assert crel_return) auto
  25.421 -qed
  25.422 -
  25.423 -lemma length_remains:
  25.424 -  assumes "crel (quicksort a l r) h h' rs"
  25.425 -  shows "Heap.length a h = Heap.length a h'"
  25.426 -using assms
  25.427 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  25.428 -  case (1 a l r h h' rs)
  25.429 -  with partition_length_remains show ?case
  25.430 -    unfolding quicksort.simps [of a l r]
  25.431 -    by (elim crel_if crelE crel_assert crel_return) auto
  25.432 -qed
  25.433 -
  25.434 -lemma quicksort_outer_remains:
  25.435 -  assumes "crel (quicksort a l r) h h' rs"
  25.436 -   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
  25.437 -  using assms
  25.438 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  25.439 -  case (1 a l r h h' rs)
  25.440 -  note cr = `crel (quicksort a l r) h h' rs`
  25.441 -  thus ?case
  25.442 -  proof (cases "r > l")
  25.443 -    case False
  25.444 -    with cr have "h' = h"
  25.445 -      unfolding quicksort.simps [of a l r]
  25.446 -      by (elim crel_if crel_return) auto
  25.447 -    thus ?thesis by simp
  25.448 -  next
  25.449 -  case True
  25.450 -   { 
  25.451 -      fix h1 h2 p ret1 ret2 i
  25.452 -      assume part: "crel (partition a l r) h h1 p"
  25.453 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
  25.454 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
  25.455 -      assume pivot: "l \<le> p \<and> p \<le> r"
  25.456 -      assume i_outer: "i < l \<or> r < i"
  25.457 -      from  partition_outer_remains [OF part True] i_outer
  25.458 -      have "get_array a h !i = get_array a h1 ! i" by fastsimp
  25.459 -      moreover
  25.460 -      with 1(1) [OF True pivot qs1] pivot i_outer
  25.461 -      have "get_array a h1 ! i = get_array a h2 ! i" by auto
  25.462 -      moreover
  25.463 -      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
  25.464 -      have "get_array a h2 ! i = get_array a h' ! i" by auto
  25.465 -      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
  25.466 -    }
  25.467 -    with cr show ?thesis
  25.468 -      unfolding quicksort.simps [of a l r]
  25.469 -      by (elim crel_if crelE crel_assert crel_return) auto
  25.470 -  qed
  25.471 -qed
  25.472 -
  25.473 -lemma quicksort_is_skip:
  25.474 -  assumes "crel (quicksort a l r) h h' rs"
  25.475 -  shows "r \<le> l \<longrightarrow> h = h'"
  25.476 -  using assms
  25.477 -  unfolding quicksort.simps [of a l r]
  25.478 -  by (elim crel_if crel_return) auto
  25.479 - 
  25.480 -lemma quicksort_sorts:
  25.481 -  assumes "crel (quicksort a l r) h h' rs"
  25.482 -  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
  25.483 -  shows "sorted (subarray l (r + 1) a h')"
  25.484 -  using assms
  25.485 -proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
  25.486 -  case (1 a l r h h' rs)
  25.487 -  note cr = `crel (quicksort a l r) h h' rs`
  25.488 -  thus ?case
  25.489 -  proof (cases "r > l")
  25.490 -    case False
  25.491 -    hence "l \<ge> r + 1 \<or> l = r" by arith 
  25.492 -    with length_remains[OF cr] 1(5) show ?thesis
  25.493 -      by (auto simp add: subarray_Nil subarray_single)
  25.494 -  next
  25.495 -    case True
  25.496 -    { 
  25.497 -      fix h1 h2 p
  25.498 -      assume part: "crel (partition a l r) h h1 p"
  25.499 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
  25.500 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
  25.501 -      from partition_returns_index_in_bounds [OF part True]
  25.502 -      have pivot: "l\<le> p \<and> p \<le> r" .
  25.503 -     note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
  25.504 -      from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
  25.505 -      have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
  25.506 -        (*-- First of all, by induction hypothesis both sublists are sorted. *)
  25.507 -      from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
  25.508 -      have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
  25.509 -      from quicksort_outer_remains [OF qs2] length_remains
  25.510 -      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
  25.511 -	by (simp add: subarray_eq_samelength_iff)
  25.512 -      with IH1 have IH1': "sorted (subarray l p a h')" by simp
  25.513 -      from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
  25.514 -      have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
  25.515 -        by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
  25.516 -           (* -- Secondly, both sublists remain partitioned. *)
  25.517 -      from partition_partitions[OF part True]
  25.518 -      have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
  25.519 -        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
  25.520 -        by (auto simp add: all_in_set_subarray_conv)
  25.521 -      from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
  25.522 -        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
  25.523 -      have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
  25.524 -	unfolding Heap.length_def subarray_def by (cases p, auto)
  25.525 -      with left_subarray_remains part_conds1 pivot_unchanged
  25.526 -      have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
  25.527 -        by (simp, subst set_of_multiset_of[symmetric], simp)
  25.528 -          (* -- These steps are the analogous for the right sublist \<dots> *)
  25.529 -      from quicksort_outer_remains [OF qs1] length_remains
  25.530 -      have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
  25.531 -	by (auto simp add: subarray_eq_samelength_iff)
  25.532 -      from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
  25.533 -        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
  25.534 -      have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
  25.535 -        unfolding Heap.length_def subarray_def by auto
  25.536 -      with right_subarray_remains part_conds2 pivot_unchanged
  25.537 -      have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
  25.538 -        by (simp, subst set_of_multiset_of[symmetric], simp)
  25.539 -          (* -- Thirdly and finally, we show that the array is sorted
  25.540 -          following from the facts above. *)
  25.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'"
  25.542 -	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
  25.543 -      with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
  25.544 -	unfolding subarray_def
  25.545 -	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
  25.546 -	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
  25.547 -    }
  25.548 -    with True cr show ?thesis
  25.549 -      unfolding quicksort.simps [of a l r]
  25.550 -      by (elim crel_if crel_return crelE crel_assert) auto
  25.551 -  qed
  25.552 -qed
  25.553 -
  25.554 -
  25.555 -lemma quicksort_is_sort:
  25.556 -  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
  25.557 -  shows "get_array a h' = sort (get_array a h)"
  25.558 -proof (cases "get_array a h = []")
  25.559 -  case True
  25.560 -  with quicksort_is_skip[OF crel] show ?thesis
  25.561 -  unfolding Heap.length_def by simp
  25.562 -next
  25.563 -  case False
  25.564 -  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
  25.565 -    unfolding Heap.length_def subarray_def by auto
  25.566 -  with length_remains[OF crel] have "sorted (get_array a h')"
  25.567 -    unfolding Heap.length_def by simp
  25.568 -  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
  25.569 -qed
  25.570 -
  25.571 -subsection {* No Errors in quicksort *}
  25.572 -text {* We have proved that quicksort sorts (if no exceptions occur).
  25.573 -We will now show that exceptions do not occur. *}
  25.574 -
  25.575 -lemma noError_part1: 
  25.576 -  assumes "l < Heap.length a h" "r < Heap.length a h"
  25.577 -  shows "noError (part1 a l r p) h"
  25.578 -  using assms
  25.579 -proof (induct a l r p arbitrary: h rule: part1.induct)
  25.580 -  case (1 a l r p)
  25.581 -  thus ?case
  25.582 -    unfolding part1.simps [of a l r] swap_def
  25.583 -    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
  25.584 -qed
  25.585 -
  25.586 -lemma noError_partition:
  25.587 -  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
  25.588 -  shows "noError (partition a l r) h"
  25.589 -using assms
  25.590 -unfolding partition.simps swap_def
  25.591 -apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
  25.592 -apply (frule part_length_remains)
  25.593 -apply (frule part_returns_index_in_bounds)
  25.594 -apply auto
  25.595 -apply (frule part_length_remains)
  25.596 -apply (frule part_returns_index_in_bounds)
  25.597 -apply auto
  25.598 -apply (frule part_length_remains)
  25.599 -apply auto
  25.600 -done
  25.601 -
  25.602 -lemma noError_quicksort:
  25.603 -  assumes "l < Heap.length a h" "r < Heap.length a h"
  25.604 -  shows "noError (quicksort a l r) h"
  25.605 -using assms
  25.606 -proof (induct a l r arbitrary: h rule: quicksort.induct)
  25.607 -  case (1 a l ri h)
  25.608 -  thus ?case
  25.609 -    unfolding quicksort.simps [of a l ri]
  25.610 -    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
  25.611 -    apply (frule partition_returns_index_in_bounds)
  25.612 -    apply auto
  25.613 -    apply (frule partition_returns_index_in_bounds)
  25.614 -    apply auto
  25.615 -    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
  25.616 -    apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
  25.617 -    apply (erule disjE)
  25.618 -    apply auto
  25.619 -    unfolding quicksort.simps [of a "Suc ri" ri]
  25.620 -    apply (auto intro!: noError_if noError_return)
  25.621 -    done
  25.622 -qed
  25.623 -
  25.624 -
  25.625 -subsection {* Example *}
  25.626 -
  25.627 -definition "qsort a = do
  25.628 -    k \<leftarrow> length a;
  25.629 -    quicksort a 0 (k - 1);
  25.630 -    return a
  25.631 -  done"
  25.632 -
  25.633 -ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
  25.634 -
  25.635 -export_code qsort in SML_imp module_name QSort
  25.636 -export_code qsort in OCaml module_name QSort file -
  25.637 -export_code qsort in OCaml_imp module_name QSort file -
  25.638 -export_code qsort in Haskell module_name QSort file -
  25.639 -
  25.640 -end
  25.641 \ No newline at end of file
    26.1 --- a/src/HOL/ex/ROOT.ML	Mon Mar 23 15:33:35 2009 +0100
    26.2 +++ b/src/HOL/ex/ROOT.ML	Mon Mar 23 19:01:34 2009 +0100
    26.3 @@ -21,7 +21,6 @@
    26.4  
    26.5  use_thys [
    26.6    "Numeral",
    26.7 -  "ImperativeQuicksort",
    26.8    "Higher_Order_Logic",
    26.9    "Abstract_NAT",
   26.10    "Guess",
    27.1 --- a/src/HOL/ex/Subarray.thy	Mon Mar 23 15:33:35 2009 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,66 +0,0 @@
    27.4 -theory Subarray
    27.5 -imports Array Sublist
    27.6 -begin
    27.7 -
    27.8 -definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
    27.9 -where
   27.10 -  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
   27.11 -
   27.12 -lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
   27.13 -apply (simp add: subarray_def Heap.upd_def)
   27.14 -apply (simp add: sublist'_update1)
   27.15 -done
   27.16 -
   27.17 -lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
   27.18 -apply (simp add: subarray_def Heap.upd_def)
   27.19 -apply (subst sublist'_update2)
   27.20 -apply fastsimp
   27.21 -apply simp
   27.22 -done
   27.23 -
   27.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]"
   27.25 -unfolding subarray_def Heap.upd_def
   27.26 -by (simp add: sublist'_update3)
   27.27 -
   27.28 -lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
   27.29 -by (simp add: subarray_def sublist'_Nil')
   27.30 -
   27.31 -lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
   27.32 -by (simp add: subarray_def Heap.length_def sublist'_single)
   27.33 -
   27.34 -lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
   27.35 -by (simp add: subarray_def Heap.length_def length_sublist')
   27.36 -
   27.37 -lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
   27.38 -by (simp add: length_subarray)
   27.39 -
   27.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"
   27.41 -unfolding Heap.length_def subarray_def
   27.42 -by (simp add: sublist'_front)
   27.43 -
   27.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)]"
   27.45 -unfolding Heap.length_def subarray_def
   27.46 -by (simp add: sublist'_back)
   27.47 -
   27.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"
   27.49 -unfolding subarray_def
   27.50 -by (simp add: sublist'_append)
   27.51 -
   27.52 -lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
   27.53 -unfolding Heap.length_def subarray_def
   27.54 -by (simp add: sublist'_all)
   27.55 -
   27.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)"
   27.57 -unfolding Heap.length_def subarray_def
   27.58 -by (simp add: nth_sublist')
   27.59 -
   27.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')"
   27.61 -unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
   27.62 -
   27.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))"
   27.64 -unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
   27.65 -
   27.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))"
   27.67 -unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
   27.68 -
   27.69 -end
   27.70 \ No newline at end of file
    28.1 --- a/src/HOL/ex/Sublist.thy	Mon Mar 23 15:33:35 2009 +0100
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,505 +0,0 @@
    28.4 -(* $Id$ *)
    28.5 -
    28.6 -header {* Slices of lists *}
    28.7 -
    28.8 -theory Sublist
    28.9 -imports Multiset
   28.10 -begin
   28.11 -
   28.12 -
   28.13 -lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
   28.14 -apply (induct xs arbitrary: i j k)
   28.15 -apply simp
   28.16 -apply (simp only: sublist_Cons)
   28.17 -apply simp
   28.18 -apply safe
   28.19 -apply simp
   28.20 -apply (erule_tac x="0" in meta_allE)
   28.21 -apply (erule_tac x="j - 1" in meta_allE)
   28.22 -apply (erule_tac x="k - 1" in meta_allE)
   28.23 -apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
   28.24 -apply simp
   28.25 -apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
   28.26 -apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
   28.27 -apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
   28.28 -apply simp
   28.29 -apply fastsimp
   28.30 -apply fastsimp
   28.31 -apply fastsimp
   28.32 -apply fastsimp
   28.33 -apply (erule_tac x="i - 1" in meta_allE)
   28.34 -apply (erule_tac x="j - 1" in meta_allE)
   28.35 -apply (erule_tac x="k - 1" in meta_allE)
   28.36 -apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
   28.37 -apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
   28.38 -apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
   28.39 -apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
   28.40 -apply simp
   28.41 -apply fastsimp
   28.42 -apply fastsimp
   28.43 -apply fastsimp
   28.44 -apply fastsimp
   28.45 -done
   28.46 -
   28.47 -lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
   28.48 -apply (induct xs arbitrary: i inds)
   28.49 -apply simp
   28.50 -apply (case_tac i)
   28.51 -apply (simp add: sublist_Cons)
   28.52 -apply (simp add: sublist_Cons)
   28.53 -done
   28.54 -
   28.55 -lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
   28.56 -proof (induct xs arbitrary: i inds)
   28.57 -  case Nil thus ?case by simp
   28.58 -next
   28.59 -  case (Cons x xs)
   28.60 -  thus ?case
   28.61 -  proof (cases i)
   28.62 -    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
   28.63 -  next
   28.64 -    case (Suc i')
   28.65 -    with Cons show ?thesis
   28.66 -      apply simp
   28.67 -      apply (simp add: sublist_Cons)
   28.68 -      apply auto
   28.69 -      apply (auto simp add: nat.split)
   28.70 -      apply (simp add: card_less_Suc[symmetric])
   28.71 -      apply (simp add: card_less_Suc2)
   28.72 -      done
   28.73 -  qed
   28.74 -qed
   28.75 -
   28.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)"
   28.77 -by (simp add: sublist_update1 sublist_update2)
   28.78 -
   28.79 -lemma sublist_take: "sublist xs {j. j < m} = take m xs"
   28.80 -apply (induct xs arbitrary: m)
   28.81 -apply simp
   28.82 -apply (case_tac m)
   28.83 -apply simp
   28.84 -apply (simp add: sublist_Cons)
   28.85 -done
   28.86 -
   28.87 -lemma sublist_take': "sublist xs {0..<m} = take m xs"
   28.88 -apply (induct xs arbitrary: m)
   28.89 -apply simp
   28.90 -apply (case_tac m)
   28.91 -apply simp
   28.92 -apply (simp add: sublist_Cons sublist_take)
   28.93 -done
   28.94 -
   28.95 -lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
   28.96 -apply (induct xs)
   28.97 -apply simp
   28.98 -apply (simp add: sublist_Cons)
   28.99 -done
  28.100 -
  28.101 -lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
  28.102 -apply (induct xs)
  28.103 -apply simp
  28.104 -apply (simp add: sublist_Cons)
  28.105 -done
  28.106 -
  28.107 -lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
  28.108 -apply (induct xs arbitrary: a)
  28.109 -apply simp
  28.110 -apply(case_tac aa)
  28.111 -apply simp
  28.112 -apply (simp add: sublist_Cons)
  28.113 -apply simp
  28.114 -apply (simp add: sublist_Cons)
  28.115 -done
  28.116 -
  28.117 -lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
  28.118 -apply (induct xs arbitrary: inds)
  28.119 -apply simp
  28.120 -apply (simp add: sublist_Cons)
  28.121 -apply auto
  28.122 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
  28.123 -apply auto
  28.124 -done
  28.125 -
  28.126 -lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
  28.127 -apply (induct xs arbitrary: inds)
  28.128 -apply simp
  28.129 -apply (simp add: sublist_Cons)
  28.130 -apply (auto split: if_splits)
  28.131 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
  28.132 -apply (case_tac x, auto)
  28.133 -done
  28.134 -
  28.135 -lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
  28.136 -apply (induct xs arbitrary: inds)
  28.137 -apply simp
  28.138 -apply (simp add: sublist_Cons)
  28.139 -apply auto
  28.140 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
  28.141 -apply (case_tac x, auto)
  28.142 -done
  28.143 -
  28.144 -lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
  28.145 -apply (induct xs arbitrary: ys inds inds')
  28.146 -apply simp
  28.147 -apply (drule sym, rule sym)
  28.148 -apply (simp add: sublist_Nil, fastsimp)
  28.149 -apply (case_tac ys)
  28.150 -apply (simp add: sublist_Nil, fastsimp)
  28.151 -apply (auto simp add: sublist_Cons)
  28.152 -apply (erule_tac x="list" in meta_allE)
  28.153 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
  28.154 -apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
  28.155 -apply fastsimp
  28.156 -apply (erule_tac x="list" in meta_allE)
  28.157 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
  28.158 -apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
  28.159 -apply fastsimp
  28.160 -done
  28.161 -
  28.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"
  28.163 -apply (induct xs arbitrary: ys inds)
  28.164 -apply simp
  28.165 -apply (rule sym, simp add: sublist_Nil)
  28.166 -apply (case_tac ys)
  28.167 -apply (simp add: sublist_Nil)
  28.168 -apply (auto simp add: sublist_Cons)
  28.169 -apply (erule_tac x="list" in meta_allE)
  28.170 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
  28.171 -apply fastsimp
  28.172 -apply (erule_tac x="list" in meta_allE)
  28.173 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
  28.174 -apply fastsimp
  28.175 -done
  28.176 -
  28.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"
  28.178 -by (rule sublist_eq, auto)
  28.179 -
  28.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)"
  28.181 -apply (induct xs arbitrary: ys inds)
  28.182 -apply simp
  28.183 -apply (rule sym, simp add: sublist_Nil)
  28.184 -apply (case_tac ys)
  28.185 -apply (simp add: sublist_Nil)
  28.186 -apply (auto simp add: sublist_Cons)
  28.187 -apply (case_tac i)
  28.188 -apply auto
  28.189 -apply (case_tac i)
  28.190 -apply auto
  28.191 -done
  28.192 -
  28.193 -section {* Another sublist function *}
  28.194 -
  28.195 -function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
  28.196 -where
  28.197 -  "sublist' n m [] = []"
  28.198 -| "sublist' n 0 xs = []"
  28.199 -| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
  28.200 -| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
  28.201 -by pat_completeness auto
  28.202 -termination by lexicographic_order
  28.203 -
  28.204 -subsection {* Proving equivalence to the other sublist command *}
  28.205 -
  28.206 -lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
  28.207 -apply (induct xs arbitrary: n m)
  28.208 -apply simp
  28.209 -apply (case_tac n)
  28.210 -apply (case_tac m)
  28.211 -apply simp
  28.212 -apply (simp add: sublist_Cons)
  28.213 -apply (case_tac m)
  28.214 -apply simp
  28.215 -apply (simp add: sublist_Cons)
  28.216 -done
  28.217 -
  28.218 -
  28.219 -lemma "sublist' n m xs = sublist xs {n..<m}"
  28.220 -apply (induct xs arbitrary: n m)
  28.221 -apply simp
  28.222 -apply (case_tac n, case_tac m)
  28.223 -apply simp
  28.224 -apply simp
  28.225 -apply (simp add: sublist_take')
  28.226 -apply (case_tac m)
  28.227 -apply simp
  28.228 -apply (simp add: sublist_Cons sublist'_sublist)
  28.229 -done
  28.230 -
  28.231 -
  28.232 -subsection {* Showing equivalence to use of drop and take for definition *}
  28.233 -
  28.234 -lemma "sublist' n m xs = take (m - n) (drop n xs)"
  28.235 -apply (induct xs arbitrary: n m)
  28.236 -apply simp
  28.237 -apply (case_tac m)
  28.238 -apply simp
  28.239 -apply (case_tac n)
  28.240 -apply simp
  28.241 -apply simp
  28.242 -done
  28.243 -
  28.244 -subsection {* General lemma about sublist *}
  28.245 -
  28.246 -lemma sublist'_Nil[simp]: "sublist' i j [] = []"
  28.247 -by simp
  28.248 -
  28.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)"
  28.250 -by (cases i) auto
  28.251 -
  28.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))"
  28.253 -apply (cases j)
  28.254 -apply auto
  28.255 -apply (cases i)
  28.256 -apply auto
  28.257 -done
  28.258 -
  28.259 -lemma sublist_n_0: "sublist' n 0 xs = []"
  28.260 -by (induct xs, auto)
  28.261 -
  28.262 -lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
  28.263 -apply (induct xs arbitrary: n m)
  28.264 -apply simp
  28.265 -apply (case_tac m)
  28.266 -apply simp
  28.267 -apply (case_tac n)
  28.268 -apply simp
  28.269 -apply simp
  28.270 -done
  28.271 -
  28.272 -lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
  28.273 -apply (induct xs arbitrary: n m)
  28.274 -apply simp
  28.275 -apply (case_tac m)
  28.276 -apply simp
  28.277 -apply (case_tac n)
  28.278 -apply simp
  28.279 -apply simp
  28.280 -done
  28.281 -
  28.282 -lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
  28.283 -apply (induct xs arbitrary: n m)
  28.284 -apply simp
  28.285 -apply (case_tac m)
  28.286 -apply simp
  28.287 -apply (case_tac n)
  28.288 -apply simp
  28.289 -apply simp
  28.290 -done
  28.291 -
  28.292 -lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
  28.293 -apply (induct xs arbitrary: n m)
  28.294 -apply simp
  28.295 -apply (case_tac m)
  28.296 -apply simp
  28.297 -apply (case_tac n)
  28.298 -apply simp
  28.299 -apply simp
  28.300 -done
  28.301 -
  28.302 -lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
  28.303 -apply (induct xs arbitrary: n)
  28.304 -apply simp
  28.305 -apply simp
  28.306 -apply (case_tac n)
  28.307 -apply (simp add: sublist_n_0)
  28.308 -apply simp
  28.309 -done
  28.310 -
  28.311 -lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
  28.312 -apply (induct xs arbitrary: n m i)
  28.313 -apply simp
  28.314 -apply simp
  28.315 -apply (case_tac i)
  28.316 -apply simp
  28.317 -apply simp
  28.318 -done
  28.319 -
  28.320 -lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
  28.321 -apply (induct xs arbitrary: n m i)
  28.322 -apply simp
  28.323 -apply simp
  28.324 -apply (case_tac i)
  28.325 -apply simp
  28.326 -apply simp
  28.327 -done
  28.328 -
  28.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]"
  28.330 -proof (induct xs arbitrary: n m i)
  28.331 -  case Nil thus ?case by auto
  28.332 -next
  28.333 -  case (Cons x xs)
  28.334 -  thus ?case
  28.335 -    apply -
  28.336 -    apply auto
  28.337 -    apply (cases i)
  28.338 -    apply auto
  28.339 -    apply (cases i)
  28.340 -    apply auto
  28.341 -    done
  28.342 -qed
  28.343 -
  28.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"
  28.345 -proof (induct xs arbitrary: i j ys n m)
  28.346 -  case Nil
  28.347 -  thus ?case
  28.348 -    apply -
  28.349 -    apply (rule sym, drule sym)
  28.350 -    apply (simp add: sublist'_Nil)
  28.351 -    apply (simp add: sublist'_Nil3)
  28.352 -    apply arith
  28.353 -    done
  28.354 -next
  28.355 -  case (Cons x xs i j ys n m)
  28.356 -  note c = this
  28.357 -  thus ?case
  28.358 -  proof (cases m)
  28.359 -    case 0 thus ?thesis by (simp add: sublist_n_0)
  28.360 -  next
  28.361 -    case (Suc m')
  28.362 -    note a = this
  28.363 -    thus ?thesis
  28.364 -    proof (cases n)
  28.365 -      case 0 note b = this
  28.366 -      show ?thesis
  28.367 -      proof (cases ys)
  28.368 -	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
  28.369 -      next
  28.370 -	case (Cons y ys)
  28.371 -	show ?thesis
  28.372 -	proof (cases j)
  28.373 -	  case 0 with a b Cons.prems show ?thesis by simp
  28.374 -	next
  28.375 -	  case (Suc j') with a b Cons.prems Cons show ?thesis 
  28.376 -	    apply -
  28.377 -	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
  28.378 -	    done
  28.379 -	qed
  28.380 -      qed
  28.381 -    next
  28.382 -      case (Suc n')
  28.383 -      show ?thesis
  28.384 -      proof (cases ys)
  28.385 -	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
  28.386 -      next
  28.387 -	case (Cons y ys) with Suc a Cons.prems show ?thesis
  28.388 -	  apply -
  28.389 -	  apply simp
  28.390 -	  apply (cases j)
  28.391 -	  apply simp
  28.392 -	  apply (cases i)
  28.393 -	  apply simp
  28.394 -	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
  28.395 -	  apply simp
  28.396 -	  apply simp
  28.397 -	  apply simp
  28.398 -	  apply simp
  28.399 -	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
  28.400 -	  apply simp
  28.401 -	  apply simp
  28.402 -	  apply simp
  28.403 -	  done
  28.404 -      qed
  28.405 -    qed
  28.406 -  qed
  28.407 -qed
  28.408 -
  28.409 -lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
  28.410 -by (induct xs arbitrary: i j, auto)
  28.411 -
  28.412 -lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
  28.413 -apply (induct xs arbitrary: a i j)
  28.414 -apply simp
  28.415 -apply (case_tac j)
  28.416 -apply simp
  28.417 -apply (case_tac i)
  28.418 -apply simp
  28.419 -apply simp
  28.420 -done
  28.421 -
  28.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)]"
  28.423 -apply (induct xs arbitrary: a i j)
  28.424 -apply simp
  28.425 -apply simp
  28.426 -apply (case_tac j)
  28.427 -apply simp
  28.428 -apply auto
  28.429 -apply (case_tac nat)
  28.430 -apply auto
  28.431 -done
  28.432 -
  28.433 -(* suffices that j \<le> length xs and length ys *) 
  28.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')"
  28.435 -proof (induct xs arbitrary: ys i j)
  28.436 -  case Nil thus ?case by simp
  28.437 -next
  28.438 -  case (Cons x xs)
  28.439 -  thus ?case
  28.440 -    apply -
  28.441 -    apply (cases ys)
  28.442 -    apply simp
  28.443 -    apply simp
  28.444 -    apply auto
  28.445 -    apply (case_tac i', auto)
  28.446 -    apply (erule_tac x="Suc i'" in allE, auto)
  28.447 -    apply (erule_tac x="i' - 1" in allE, auto)
  28.448 -    apply (case_tac i', auto)
  28.449 -    apply (erule_tac x="Suc i'" in allE, auto)
  28.450 -    done
  28.451 -qed
  28.452 -
  28.453 -lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
  28.454 -by (induct xs, auto)
  28.455 -
  28.456 -lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
  28.457 -by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
  28.458 -
  28.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"
  28.460 -by (induct xs arbitrary: i j k) auto
  28.461 -
  28.462 -lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
  28.463 -apply (induct xs arbitrary: i j k)
  28.464 -apply auto
  28.465 -apply (case_tac k)
  28.466 -apply auto
  28.467 -apply (case_tac i)
  28.468 -apply auto
  28.469 -done
  28.470 -
  28.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}"
  28.472 -apply (simp add: sublist'_sublist)
  28.473 -apply (simp add: set_sublist)
  28.474 -apply auto
  28.475 -done
  28.476 -
  28.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))"
  28.478 -unfolding set_sublist' by blast
  28.479 -
  28.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))"
  28.481 -unfolding set_sublist' by blast
  28.482 -
  28.483 -
  28.484 -lemma multiset_of_sublist:
  28.485 -assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
  28.486 -assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
  28.487 -assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
  28.488 -assumes multiset: "multiset_of xs = multiset_of ys"
  28.489 -  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
  28.490 -proof -
  28.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") 
  28.492 -    by (simp add: sublist'_append)
  28.493 -  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
  28.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") 
  28.495 -    by (simp add: sublist'_append)
  28.496 -  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
  28.497 -  moreover
  28.498 -  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
  28.499 -    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
  28.500 -  moreover
  28.501 -  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
  28.502 -    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
  28.503 -  moreover
  28.504 -  ultimately show ?thesis by (simp add: multiset_of_append)
  28.505 -qed
  28.506 -
  28.507 -
  28.508 -end
    29.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 23 15:33:35 2009 +0100
    29.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 23 19:01:34 2009 +0100
    29.3 @@ -466,7 +466,7 @@
    29.4                       NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
    29.5                                 handle Option =>
    29.6                                 (trace_thm "" thm1; trace_thm "" thm2;
    29.7 -                                sys_error "Lin.arith. failed to add thms")
    29.8 +                                sys_error "Linear arithmetic: failed to add thms")
    29.9                               )
   29.10                     | SOME thm => thm)
   29.11          | SOME thm => thm;
   29.12 @@ -588,8 +588,8 @@
   29.13            handle NoEx => NONE
   29.14        in
   29.15          case ex of
   29.16 -          SOME s => (warning "arith failed - see trace for a counterexample"; tracing s)
   29.17 -        | NONE => warning "arith failed"
   29.18 +          SOME s => (warning "Linear arithmetic failed - see trace for a counterexample."; tracing s)
   29.19 +        | NONE => warning "Linear arithmetic failed"
   29.20        end;
   29.21  
   29.22  (* ------------------------------------------------------------------------- *)
    30.1 --- a/src/Pure/Isar/code_unit.ML	Mon Mar 23 15:33:35 2009 +0100
    30.2 +++ b/src/Pure/Isar/code_unit.ML	Mon Mar 23 19:01:34 2009 +0100
    30.3 @@ -218,7 +218,7 @@
    30.4      |> burrow_thms (canonical_tvars thy purify_tvar)
    30.5      |> map (canonical_vars thy purify_var)
    30.6      |> map (canonical_absvars purify_var)
    30.7 -    |> map Drule.zero_var_indexes
    30.8 +    |> Drule.zero_var_indexes_list
    30.9    end;
   30.10  
   30.11