src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
changeset 41561 d1318f3c86ba
child 41588 9546828c0eb3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,665 @@
     1.4 +(*  Title:      HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
     1.5 +    Author:     Stefan Berghofer
     1.6 +    Copyright:  secunet Security Networks AG
     1.7 +*)
     1.8 +
     1.9 +theory Longest_Increasing_Subsequence
    1.10 +imports SPARK
    1.11 +begin
    1.12 +
    1.13 +text {*
    1.14 +Set of all increasing subsequences in a prefix of an array
    1.15 +*}
    1.16 +
    1.17 +definition iseq :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat set set" where
    1.18 +  "iseq xs l = {is. (\<forall>i\<in>is. i < l) \<and>
    1.19 +     (\<forall>i\<in>is. \<forall>j\<in>is. i \<le> j \<longrightarrow> xs i \<le> xs j)}"
    1.20 +
    1.21 +text {*
    1.22 +Length of longest increasing subsequence in a prefix of an array
    1.23 +*}
    1.24 +
    1.25 +definition liseq :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat" where
    1.26 +  "liseq xs i = Max (card ` iseq xs i)"
    1.27 +
    1.28 +text {*
    1.29 +Length of longest increasing subsequence ending at a particular position
    1.30 +*}
    1.31 +
    1.32 +definition liseq' :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat" where
    1.33 +  "liseq' xs i = Max (card ` (iseq xs (Suc i) \<inter> {is. Max is = i}))"  
    1.34 +
    1.35 +lemma iseq_finite: "finite (iseq xs i)"
    1.36 +  apply (simp add: iseq_def)
    1.37 +  apply (rule finite_subset [OF _
    1.38 +    finite_Collect_subsets [of "{j. j < i}"]])
    1.39 +  apply auto
    1.40 +  done
    1.41 +
    1.42 +lemma iseq_finite': "is \<in> iseq xs i \<Longrightarrow> finite is"
    1.43 +  by (auto simp add: iseq_def bounded_nat_set_is_finite)
    1.44 +
    1.45 +lemma iseq_singleton: "i < l \<Longrightarrow> {i} \<in> iseq xs l"
    1.46 +  by (simp add: iseq_def)
    1.47 +
    1.48 +lemma iseq_trivial: "{} \<in> iseq xs i"
    1.49 +  by (simp add: iseq_def)
    1.50 +
    1.51 +lemma iseq_nonempty: "iseq xs i \<noteq> {}"
    1.52 +  by (auto intro: iseq_trivial)
    1.53 +
    1.54 +lemma liseq'_ge1: "1 \<le> liseq' xs x"
    1.55 +  apply (simp add: liseq'_def)
    1.56 +  apply (subgoal_tac "iseq xs (Suc x) \<inter> {is. Max is = x} \<noteq> {}")
    1.57 +  apply (simp add: Max_ge_iff iseq_finite)
    1.58 +  apply (rule_tac x="{x}" in bexI)
    1.59 +  apply (auto intro: iseq_singleton)
    1.60 +  done
    1.61 +
    1.62 +lemma liseq_expand:
    1.63 +  assumes R: "\<And>is. liseq xs i = card is \<Longrightarrow> is \<in> iseq xs i \<Longrightarrow>
    1.64 +    (\<And>js. js \<in> iseq xs i \<Longrightarrow> card js \<le> card is) \<Longrightarrow> P"
    1.65 +  shows "P"
    1.66 +proof -
    1.67 +  have "Max (card ` iseq xs i) \<in> card ` iseq xs i"
    1.68 +    by (rule Max_in) (simp_all add: iseq_finite iseq_nonempty)
    1.69 +  then obtain js where js: "liseq xs i = card js" and "js \<in> iseq xs i"
    1.70 +    by (rule imageE) (simp add: liseq_def)
    1.71 +  moreover {
    1.72 +    fix js'
    1.73 +    assume "js' \<in> iseq xs i"
    1.74 +    then have "card js' \<le> card js"
    1.75 +      by (simp add: js [symmetric] liseq_def iseq_finite iseq_trivial)
    1.76 +  }
    1.77 +  ultimately show ?thesis by (rule R)
    1.78 +qed
    1.79 +
    1.80 +lemma liseq'_expand:
    1.81 +  assumes R: "\<And>is. liseq' xs i = card is \<Longrightarrow> is \<in> iseq xs (Suc i) \<Longrightarrow>
    1.82 +    finite is \<Longrightarrow> Max is = i \<Longrightarrow>
    1.83 +    (\<And>js. js \<in> iseq xs (Suc i) \<Longrightarrow> Max js = i \<Longrightarrow> card js \<le> card is) \<Longrightarrow>
    1.84 +    is \<noteq> {} \<Longrightarrow> P"
    1.85 +  shows "P"
    1.86 +proof -
    1.87 +  have "Max (card ` (iseq xs (Suc i) \<inter> {is. Max is = i})) \<in>
    1.88 +    card ` (iseq xs (Suc i) \<inter> {is. Max is = i})"
    1.89 +    by (auto simp add: iseq_finite intro!: iseq_singleton Max_in)
    1.90 +  then obtain js where js: "liseq' xs i = card js" and "js \<in> iseq xs (Suc i)"
    1.91 +    and "finite js" and "Max js = i"
    1.92 +    by (auto simp add: liseq'_def intro: iseq_finite')
    1.93 +  moreover {
    1.94 +    fix js'
    1.95 +    assume "js' \<in> iseq xs (Suc i)" "Max js' = i"
    1.96 +    then have "card js' \<le> card js"
    1.97 +      by (auto simp add: js [symmetric] liseq'_def iseq_finite intro!: iseq_singleton)
    1.98 +  }
    1.99 +  note max = this
   1.100 +  moreover have "card {i} \<le> card js"
   1.101 +    by (rule max) (simp_all add: iseq_singleton)
   1.102 +  then have "js \<noteq> {}" by auto
   1.103 +  ultimately show ?thesis by (rule R)
   1.104 +qed
   1.105 +
   1.106 +lemma liseq'_ge:
   1.107 +  "j = card js \<Longrightarrow> js \<in> iseq xs (Suc i) \<Longrightarrow> Max js = i \<Longrightarrow>
   1.108 +  js \<noteq> {} \<Longrightarrow> j \<le> liseq' xs i"
   1.109 +  by (simp add: liseq'_def iseq_finite)
   1.110 +
   1.111 +lemma liseq'_eq:
   1.112 +  "j = card js \<Longrightarrow> js \<in> iseq xs (Suc i) \<Longrightarrow> Max js = i \<Longrightarrow>
   1.113 +  js \<noteq> {} \<Longrightarrow> (\<And>js'. js' \<in> iseq xs (Suc i) \<Longrightarrow> Max js' = i \<Longrightarrow> finite js' \<Longrightarrow>
   1.114 +    js' \<noteq> {} \<Longrightarrow> card js' \<le> card js) \<Longrightarrow>
   1.115 +  j = liseq' xs i"
   1.116 +  by (fastsimp simp add: liseq'_def iseq_finite
   1.117 +    intro: Max_eqI [symmetric])
   1.118 +
   1.119 +lemma liseq_ge:
   1.120 +  "j = card js \<Longrightarrow> js \<in> iseq xs i \<Longrightarrow> j \<le> liseq xs i"
   1.121 +  by (auto simp add: liseq_def iseq_finite)
   1.122 +
   1.123 +lemma liseq_eq:
   1.124 +  "j = card js \<Longrightarrow> js \<in> iseq xs i \<Longrightarrow>
   1.125 +  (\<And>js'. js' \<in> iseq xs i \<Longrightarrow> finite js' \<Longrightarrow>
   1.126 +    js' \<noteq> {} \<Longrightarrow> card js' \<le> card js) \<Longrightarrow>
   1.127 +  j = liseq xs i"
   1.128 +  by (fastsimp simp add: liseq_def iseq_finite
   1.129 +    intro: Max_eqI [symmetric])
   1.130 +
   1.131 +lemma max_notin: "finite xs \<Longrightarrow> Max xs < x \<Longrightarrow> x \<notin> xs"
   1.132 +  by (cases "xs = {}") auto
   1.133 +
   1.134 +lemma iseq_insert:
   1.135 +  "xs (Max is) \<le> xs i \<Longrightarrow> is \<in> iseq xs i \<Longrightarrow>
   1.136 +  is \<union> {i} \<in> iseq xs (Suc i)"
   1.137 +  apply (frule iseq_finite')
   1.138 +  apply (cases "is = {}")
   1.139 +  apply (auto simp add: iseq_def)
   1.140 +  apply (rule order_trans [of _ "xs (Max is)"])
   1.141 +  apply auto
   1.142 +  apply (thin_tac "\<forall>a\<in>is. a < i")
   1.143 +  apply (drule_tac x=ia in bspec)
   1.144 +  apply assumption
   1.145 +  apply (drule_tac x="Max is" in bspec)
   1.146 +  apply (auto intro: Max_in)
   1.147 +  done
   1.148 +
   1.149 +lemma iseq_diff: "is \<in> iseq xs (Suc (Max is)) \<Longrightarrow>
   1.150 +  is - {Max is} \<in> iseq xs (Suc (Max (is - {Max is})))"
   1.151 +  apply (frule iseq_finite')
   1.152 +  apply (simp add: iseq_def less_Suc_eq_le)
   1.153 +  done
   1.154 +
   1.155 +lemma iseq_butlast:
   1.156 +  assumes "js \<in> iseq xs (Suc i)" and "js \<noteq> {}"
   1.157 +  and "Max js \<noteq> i"
   1.158 +  shows "js \<in> iseq xs i"
   1.159 +proof -
   1.160 +  from assms have fin: "finite js"
   1.161 +    by (simp add: iseq_finite')
   1.162 +  with assms have "Max js \<in> js"
   1.163 +    by auto
   1.164 +  with assms have "Max js < i"
   1.165 +    by (auto simp add: iseq_def)
   1.166 +  with fin assms have "\<forall>j\<in>js. j < i"
   1.167 +    by (simp add: Max_less_iff)
   1.168 +  with assms show ?thesis
   1.169 +    by (simp add: iseq_def)
   1.170 +qed
   1.171 +
   1.172 +lemma iseq_mono: "is \<in> iseq xs i \<Longrightarrow> i \<le> j \<Longrightarrow> is \<in> iseq xs j"
   1.173 +  by (auto simp add: iseq_def)
   1.174 +
   1.175 +lemma diff_nonempty:
   1.176 +  assumes "1 < card is"
   1.177 +  shows "is - {i} \<noteq> {}"
   1.178 +proof -
   1.179 +  from assms have fin: "finite is" by (auto intro: card_ge_0_finite)
   1.180 +  with assms fin have "card is - 1 \<le> card (is - {i})"
   1.181 +    by (simp add: card_Diff_singleton_if)
   1.182 +  with assms have "0 < card (is - {i})" by simp
   1.183 +  then show ?thesis by (simp add: card_gt_0_iff)
   1.184 +qed
   1.185 +
   1.186 +lemma Max_diff:
   1.187 +  assumes "1 < card is"
   1.188 +  shows "Max (is - {Max is}) < Max is"
   1.189 +proof -
   1.190 +  from assms have "finite is" by (auto intro: card_ge_0_finite)
   1.191 +  moreover from assms have "is - {Max is} \<noteq> {}"
   1.192 +    by (rule diff_nonempty)
   1.193 +  ultimately show ?thesis using assms
   1.194 +    apply (auto simp add: not_less)
   1.195 +    apply (subgoal_tac "a \<le> Max is")
   1.196 +    apply auto
   1.197 +    done
   1.198 +qed
   1.199 +
   1.200 +lemma iseq_nth: "js \<in> iseq xs l \<Longrightarrow> 1 < card js \<Longrightarrow>
   1.201 +  xs (Max (js - {Max js})) \<le> xs (Max js)"
   1.202 +  apply (auto simp add: iseq_def)
   1.203 +  apply (subgoal_tac "Max (js - {Max js}) \<in> js")
   1.204 +  apply (thin_tac "\<forall>i\<in>js. i < l")
   1.205 +  apply (drule_tac x="Max (js - {Max js})" in bspec)
   1.206 +  apply assumption
   1.207 +  apply (drule_tac x="Max js" in bspec)
   1.208 +  using card_gt_0_iff [of js]
   1.209 +  apply simp
   1.210 +  using Max_diff [of js]
   1.211 +  apply simp
   1.212 +  using Max_in [of "js - {Max js}", OF _ diff_nonempty] card_gt_0_iff [of js]
   1.213 +  apply auto
   1.214 +  done
   1.215 +
   1.216 +lemma card_leq1_singleton:
   1.217 +  assumes "finite xs" "xs \<noteq> {}" "card xs \<le> 1"
   1.218 +  obtains x where "xs = {x}"
   1.219 +  using assms
   1.220 +  by induct simp_all
   1.221 +
   1.222 +lemma longest_iseq1:
   1.223 +  "liseq' xs i =
   1.224 +   Max ({0} \<union> {liseq' xs j |j. j < i \<and> xs j \<le> xs i}) + 1"
   1.225 +proof -
   1.226 +  have "Max ({0} \<union> {liseq' xs j |j. j < i \<and> xs j \<le> xs i}) = liseq' xs i - 1"
   1.227 +  proof (rule Max_eqI)
   1.228 +    fix y
   1.229 +    assume "y \<in> {0} \<union> {liseq' xs j |j. j < i \<and> xs j \<le> xs i}"
   1.230 +    then show "y \<le> liseq' xs i - 1"
   1.231 +    proof
   1.232 +      assume "y \<in> {liseq' xs j |j. j < i \<and> xs j \<le> xs i}"
   1.233 +      then obtain j where j: "j < i" "xs j \<le> xs i" "y = liseq' xs j"
   1.234 +        by auto
   1.235 +      have "liseq' xs j + 1 \<le> liseq' xs i"
   1.236 +      proof (rule liseq'_expand)
   1.237 +        fix "is"
   1.238 +        assume H: "liseq' xs j = card is" "is \<in> iseq xs (Suc j)"
   1.239 +          "finite is" "Max is = j" "is \<noteq> {}"
   1.240 +        from H j have "card is + 1 = card (is \<union> {i})"
   1.241 +          by (simp add: card_insert max_notin)
   1.242 +        moreover {
   1.243 +          from H j have "xs (Max is) \<le> xs i" by simp
   1.244 +          moreover from `j < i` have "Suc j \<le> i" by simp
   1.245 +          with `is \<in> iseq xs (Suc j)` have "is \<in> iseq xs i"
   1.246 +            by (rule iseq_mono)
   1.247 +          ultimately have "is \<union> {i} \<in> iseq xs (Suc i)"
   1.248 +          by (rule iseq_insert)
   1.249 +        } moreover from H j have "Max (is \<union> {i}) = i" by simp
   1.250 +        moreover have "is \<union> {i} \<noteq> {}" by simp
   1.251 +        ultimately have "card is + 1 \<le> liseq' xs i"
   1.252 +          by (rule liseq'_ge)
   1.253 +        with H show ?thesis by simp
   1.254 +      qed
   1.255 +      with j show "y \<le> liseq' xs i - 1"
   1.256 +        by simp
   1.257 +    qed simp
   1.258 +  next
   1.259 +    have "liseq' xs i \<le> 1 \<or>
   1.260 +      (\<exists>j. liseq' xs i - 1 = liseq' xs j \<and> j < i \<and> xs j \<le> xs i)"
   1.261 +    proof (rule liseq'_expand)
   1.262 +      fix "is"
   1.263 +      assume H: "liseq' xs i = card is" "is \<in> iseq xs (Suc i)"
   1.264 +        "finite is" "Max is = i" "is \<noteq> {}"
   1.265 +      assume R: "\<And>js. js \<in> iseq xs (Suc i) \<Longrightarrow> Max js = i \<Longrightarrow>
   1.266 +        card js \<le> card is"
   1.267 +      show ?thesis
   1.268 +      proof (cases "card is \<le> 1")
   1.269 +        case True with H show ?thesis by simp
   1.270 +      next
   1.271 +        case False
   1.272 +        then have "1 < card is" by simp
   1.273 +        then have "Max (is - {Max is}) < Max is"
   1.274 +          by (rule Max_diff)
   1.275 +        from `is \<in> iseq xs (Suc i)` `1 < card is`
   1.276 +        have "xs (Max (is - {Max is})) \<le> xs (Max is)"
   1.277 +          by (rule iseq_nth)
   1.278 +        have "card is - 1 = liseq' xs (Max (is - {i}))"
   1.279 +        proof (rule liseq'_eq)
   1.280 +          from `Max is = i` [symmetric] `finite is` `is \<noteq> {}`
   1.281 +          show "card is - 1 = card (is - {i})" by simp
   1.282 +        next
   1.283 +          from `is \<in> iseq xs (Suc i)` `Max is = i` [symmetric]
   1.284 +          show "is - {i} \<in> iseq xs (Suc (Max (is - {i})))"
   1.285 +            by simp (rule iseq_diff)
   1.286 +        next
   1.287 +          from `1 < card is`
   1.288 +          show "is - {i} \<noteq> {}" by (rule diff_nonempty)
   1.289 +        next
   1.290 +          fix js
   1.291 +          assume "js \<in> iseq xs (Suc (Max (is - {i})))"
   1.292 +            "Max js = Max (is - {i})" "finite js" "js \<noteq> {}"
   1.293 +          from `xs (Max (is - {Max is})) \<le> xs (Max is)`
   1.294 +            `Max js = Max (is - {i})` `Max is = i`
   1.295 +          have "xs (Max js) \<le> xs i" by simp
   1.296 +          moreover from `Max is = i` `Max (is - {Max is}) < Max is`
   1.297 +          have "Suc (Max (is - {i})) \<le> i"
   1.298 +            by simp
   1.299 +          with `js \<in> iseq xs (Suc (Max (is - {i})))`
   1.300 +          have "js \<in> iseq xs i"
   1.301 +            by (rule iseq_mono)
   1.302 +          ultimately have "js \<union> {i} \<in> iseq xs (Suc i)"
   1.303 +            by (rule iseq_insert)
   1.304 +          moreover from `js \<noteq> {}` `finite js` `Max js = Max (is - {i})`
   1.305 +            `Max is = i` [symmetric] `Max (is - {Max is}) < Max is`
   1.306 +          have "Max (js \<union> {i}) = i"
   1.307 +            by simp
   1.308 +          ultimately have "card (js \<union> {i}) \<le> card is" by (rule R)
   1.309 +          moreover from `Max is = i` [symmetric] `finite js`
   1.310 +            `Max (is - {Max is}) < Max is` `Max js = Max (is - {i})`
   1.311 +          have "i \<notin> js" by (simp add: max_notin)
   1.312 +          with `finite js`
   1.313 +          have "card (js \<union> {i}) = card ((js \<union> {i}) - {i}) + 1"
   1.314 +            by simp
   1.315 +          ultimately show "card js \<le> card (is - {i})"
   1.316 +            using `i \<notin> js` `Max is = i` [symmetric] `is \<noteq> {}` `finite is`
   1.317 +            by simp
   1.318 +        qed simp
   1.319 +        with H `Max (is - {Max is}) < Max is`
   1.320 +          `xs (Max (is - {Max is})) \<le> xs (Max is)`
   1.321 +        show ?thesis by auto
   1.322 +      qed
   1.323 +    qed
   1.324 +    then show "liseq' xs i - 1 \<in> {0} \<union>
   1.325 +      {liseq' xs j |j. j < i \<and> xs j \<le> xs i}" by simp
   1.326 +  qed simp
   1.327 +  moreover have "1 \<le> liseq' xs i" by (rule liseq'_ge1)
   1.328 +  ultimately show ?thesis by simp
   1.329 +qed
   1.330 +
   1.331 +lemma longest_iseq2': "liseq xs i < liseq' xs i \<Longrightarrow>
   1.332 +  liseq xs (Suc i) = liseq' xs i"
   1.333 +  apply (rule_tac xs=xs and i=i in liseq'_expand)
   1.334 +  apply simp
   1.335 +  apply (rule liseq_eq [symmetric])
   1.336 +  apply (rule refl)
   1.337 +  apply assumption
   1.338 +  apply (case_tac "Max js' = i")
   1.339 +  apply simp
   1.340 +  apply (drule_tac js=js' in iseq_butlast)
   1.341 +  apply assumption+
   1.342 +  apply (drule_tac js=js' in liseq_ge [OF refl])
   1.343 +  apply simp
   1.344 +  done
   1.345 +
   1.346 +lemma longest_iseq2: "liseq xs i < liseq' xs i \<Longrightarrow>
   1.347 +  liseq xs i + 1 = liseq' xs i"
   1.348 +  apply (rule_tac xs=xs and i=i in liseq'_expand)
   1.349 +  apply simp
   1.350 +  apply (rule_tac xs=xs and i=i in liseq_expand)
   1.351 +  apply (drule_tac s="Max is" in sym)
   1.352 +  apply simp
   1.353 +  apply (case_tac "card is \<le> 1")
   1.354 +  apply simp
   1.355 +  apply (drule iseq_diff)
   1.356 +  apply (drule_tac i="Suc (Max (is - {Max is}))" and j="Max is" in iseq_mono)
   1.357 +  apply (simp add: less_eq_Suc_le [symmetric])
   1.358 +  apply (rule Max_diff)
   1.359 +  apply simp
   1.360 +  apply (drule_tac x="is - {Max is}" in meta_spec,
   1.361 +    drule meta_mp, assumption)
   1.362 +  apply simp
   1.363 +  done
   1.364 +
   1.365 +lemma longest_iseq3:
   1.366 +  "liseq xs j = liseq' xs i \<Longrightarrow> xs i \<le> xs j \<Longrightarrow> i < j \<Longrightarrow>
   1.367 +  liseq xs (Suc j) = liseq xs j + 1"
   1.368 +  apply (rule_tac xs=xs and i=j in liseq_expand)
   1.369 +  apply simp
   1.370 +  apply (rule_tac xs=xs and i=i in liseq'_expand)
   1.371 +  apply simp
   1.372 +  apply (rule_tac js="isa \<union> {j}" in liseq_eq [symmetric])
   1.373 +  apply (simp add: card_insert card_Diff_singleton_if max_notin)
   1.374 +  apply (rule iseq_insert)
   1.375 +  apply simp
   1.376 +  apply (erule iseq_mono)
   1.377 +  apply simp
   1.378 +  apply (case_tac "j = Max js'")
   1.379 +  apply simp
   1.380 +  apply (drule iseq_diff)
   1.381 +  apply (drule_tac x="js' - {j}" in meta_spec)
   1.382 +  apply (drule meta_mp)
   1.383 +  apply simp
   1.384 +  apply (case_tac "card js' \<le> 1")
   1.385 +  apply (erule_tac xs=js' in card_leq1_singleton)
   1.386 +  apply assumption+
   1.387 +  apply (simp add: iseq_trivial)
   1.388 +  apply (erule iseq_mono)
   1.389 +  apply (simp add: less_eq_Suc_le [symmetric])
   1.390 +  apply (rule Max_diff)
   1.391 +  apply simp
   1.392 +  apply (rule le_diff_iff [THEN iffD1, of 1])
   1.393 +  apply (simp add: card_0_eq [symmetric] del: card_0_eq)
   1.394 +  apply (simp add: card_insert)
   1.395 +  apply (subgoal_tac "card (js' - {j}) = card js' - 1")
   1.396 +  apply (simp add: card_insert card_Diff_singleton_if max_notin)
   1.397 +  apply (frule_tac A=js' in Max_in)
   1.398 +  apply assumption
   1.399 +  apply (simp add: card_Diff_singleton_if)
   1.400 +  apply (drule_tac js=js' in iseq_butlast)
   1.401 +  apply assumption
   1.402 +  apply (erule not_sym)
   1.403 +  apply (drule_tac x=js' in meta_spec)
   1.404 +  apply (drule meta_mp)
   1.405 +  apply assumption
   1.406 +  apply (simp add: card_insert_disjoint max_notin)
   1.407 +  done
   1.408 +
   1.409 +lemma longest_iseq4:
   1.410 +  "liseq xs j = liseq' xs i \<Longrightarrow> xs i \<le> xs j \<Longrightarrow> i < j \<Longrightarrow>
   1.411 +  liseq' xs j = liseq' xs i + 1"
   1.412 +  apply (rule_tac xs=xs and i=j in liseq_expand)
   1.413 +  apply simp
   1.414 +  apply (rule_tac xs=xs and i=i in liseq'_expand)
   1.415 +  apply simp
   1.416 +  apply (rule_tac js="isa \<union> {j}" in liseq'_eq [symmetric])
   1.417 +  apply (simp add: card_insert card_Diff_singleton_if max_notin)
   1.418 +  apply (rule iseq_insert)
   1.419 +  apply simp
   1.420 +  apply (erule iseq_mono)
   1.421 +  apply simp
   1.422 +  apply simp
   1.423 +  apply simp
   1.424 +  apply (drule_tac s="Max js'" in sym)
   1.425 +  apply simp
   1.426 +  apply (drule iseq_diff)
   1.427 +  apply (drule_tac x="js' - {j}" in meta_spec)
   1.428 +  apply (drule meta_mp)
   1.429 +  apply simp
   1.430 +  apply (case_tac "card js' \<le> 1")
   1.431 +  apply (erule_tac xs=js' in card_leq1_singleton)
   1.432 +  apply assumption+
   1.433 +  apply (simp add: iseq_trivial)
   1.434 +  apply (erule iseq_mono)
   1.435 +  apply (simp add: less_eq_Suc_le [symmetric])
   1.436 +  apply (rule Max_diff)
   1.437 +  apply simp
   1.438 +  apply (rule le_diff_iff [THEN iffD1, of 1])
   1.439 +  apply (simp add: card_0_eq [symmetric] del: card_0_eq)
   1.440 +  apply (simp add: card_insert)
   1.441 +  apply (subgoal_tac "card (js' - {j}) = card js' - 1")
   1.442 +  apply (simp add: card_insert card_Diff_singleton_if max_notin)
   1.443 +  apply (frule_tac A=js' in Max_in)
   1.444 +  apply assumption
   1.445 +  apply (simp add: card_Diff_singleton_if)
   1.446 +  done
   1.447 +
   1.448 +lemma longest_iseq5: "liseq' xs i \<le> liseq xs i \<Longrightarrow>
   1.449 +  liseq xs (Suc i) = liseq xs i"
   1.450 +  apply (rule_tac i=i and xs=xs in liseq'_expand)
   1.451 +  apply simp
   1.452 +  apply (rule_tac xs=xs and i=i in liseq_expand)
   1.453 +  apply simp
   1.454 +  apply (rule liseq_eq [symmetric])
   1.455 +  apply (rule refl)
   1.456 +  apply (erule iseq_mono)
   1.457 +  apply simp
   1.458 +  apply (case_tac "Max js' = i")
   1.459 +  apply (drule_tac x=js' in meta_spec)
   1.460 +  apply simp
   1.461 +  apply (drule iseq_butlast, assumption, assumption)
   1.462 +  apply simp
   1.463 +  done
   1.464 +
   1.465 +lemma liseq_empty: "liseq xs 0 = 0"
   1.466 +  apply (rule_tac js="{}" in liseq_eq [symmetric])
   1.467 +  apply simp
   1.468 +  apply (rule iseq_trivial)
   1.469 +  apply (simp add: iseq_def)
   1.470 +  done
   1.471 +
   1.472 +lemma liseq'_singleton: "liseq' xs 0 = 1"
   1.473 +  by (simp add: longest_iseq1 [of _ 0])
   1.474 +
   1.475 +lemma liseq_singleton: "liseq xs (Suc 0) = Suc 0"
   1.476 +  by (simp add: longest_iseq2' liseq_empty liseq'_singleton)
   1.477 +
   1.478 +lemma liseq'_Suc_unfold:
   1.479 +  "A j \<le> x \<Longrightarrow>
   1.480 +   (insert 0 {liseq' A j' |j'. j' < Suc j \<and> A j' \<le> x}) =
   1.481 +   (insert 0 {liseq' A j' |j'. j' < j \<and> A j' \<le> x}) \<union>
   1.482 +   {liseq' A j}"
   1.483 +  by (auto simp add: less_Suc_eq)
   1.484 +
   1.485 +lemma liseq'_Suc_unfold':
   1.486 +  "\<not> (A j \<le> x) \<Longrightarrow>
   1.487 +   {liseq' A j' |j'. j' < Suc j \<and> A j' \<le> x} =
   1.488 +   {liseq' A j' |j'. j' < j \<and> A j' \<le> x}"
   1.489 +  by (auto simp add: less_Suc_eq)
   1.490 +
   1.491 +lemma iseq_card_limit:
   1.492 +  assumes "is \<in> iseq A i"
   1.493 +  shows "card is \<le> i"
   1.494 +proof -
   1.495 +  from assms have "is \<subseteq> {0..<i}"
   1.496 +    by (auto simp add: iseq_def)
   1.497 +  with finite_atLeastLessThan have "card is \<le> card {0..<i}"
   1.498 +    by (rule card_mono)
   1.499 +  with card_atLeastLessThan show ?thesis by simp
   1.500 +qed
   1.501 +
   1.502 +lemma liseq_limit: "liseq A i \<le> i"
   1.503 +  by (rule_tac xs=A and i=i in liseq_expand)
   1.504 +    (simp add: iseq_card_limit)
   1.505 +
   1.506 +lemma liseq'_limit: "liseq' A i \<le> i + 1"
   1.507 +  by (rule_tac xs=A and i=i in liseq'_expand)
   1.508 +    (simp add: iseq_card_limit)
   1.509 +
   1.510 +definition max_ext :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   1.511 +  "max_ext A i j = Max ({0} \<union> {liseq' A j' |j'. j' < j \<and> A j' \<le> A i})"
   1.512 +
   1.513 +lemma max_ext_limit: "max_ext A i j \<le> j"
   1.514 +  apply (auto simp add: max_ext_def)
   1.515 +  apply (drule Suc_leI)
   1.516 +  apply (cut_tac i=j' and A=A in liseq'_limit)
   1.517 +  apply simp
   1.518 +  done
   1.519 +
   1.520 +
   1.521 +text {* Proof functions *}
   1.522 +
   1.523 +abbreviation (input)
   1.524 +  "arr_conv a \<equiv> (\<lambda>n. a (int n))"
   1.525 +
   1.526 +lemma idx_conv_suc:
   1.527 +  "0 \<le> i \<Longrightarrow> nat (i + 1) = nat i + 1"
   1.528 +  by simp
   1.529 +
   1.530 +abbreviation liseq_ends_at' :: "(int \<Rightarrow> 'a::linorder) \<Rightarrow> int \<Rightarrow> int" where
   1.531 +  "liseq_ends_at' A i \<equiv> int (liseq' (\<lambda>l. A (int l)) (nat i))"
   1.532 +
   1.533 +abbreviation liseq_prfx' :: "(int \<Rightarrow> 'a::linorder) \<Rightarrow> int \<Rightarrow> int" where
   1.534 +  "liseq_prfx' A i \<equiv> int (liseq (\<lambda>l. A (int l)) (nat i))"
   1.535 +
   1.536 +abbreviation max_ext' :: "(int \<Rightarrow> 'a::linorder) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
   1.537 +  "max_ext' A i j \<equiv> int (max_ext (\<lambda>l. A (int l)) (nat i) (nat j))"
   1.538 +
   1.539 +spark_proof_functions
   1.540 +  liseq_ends_at = "liseq_ends_at' :: (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int"
   1.541 +  liseq_prfx = "liseq_prfx' :: (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int"
   1.542 +  max_ext = "max_ext' :: (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int"
   1.543 +
   1.544 +
   1.545 +text {* The verification conditions *}
   1.546 +
   1.547 +spark_open "liseq/liseq_length.siv"
   1.548 +
   1.549 +spark_vc procedure_liseq_length_5
   1.550 +  by (simp_all add: liseq_singleton liseq'_singleton)
   1.551 +
   1.552 +spark_vc procedure_liseq_length_6
   1.553 +proof -
   1.554 +  from H1 H2 H3 H4
   1.555 +  have eq: "liseq (arr_conv a) (nat i) =
   1.556 +    liseq' (arr_conv a) (nat pmax)"
   1.557 +    by simp
   1.558 +  from H14 H3 H4
   1.559 +  have pmax1: "arr_conv a (nat pmax) \<le> arr_conv a (nat i)"
   1.560 +    by simp
   1.561 +  from H3 H4 have pmax2: "nat pmax < nat i"
   1.562 +    by simp
   1.563 +  {
   1.564 +    fix i2
   1.565 +    assume i2: "0 \<le> i2" "i2 \<le> i"
   1.566 +    have "(l(i := l pmax + 1)) i2 =
   1.567 +      int (liseq' (arr_conv a) (nat i2))"
   1.568 +    proof (cases "i2 = i")
   1.569 +      case True
   1.570 +      from eq pmax1 pmax2 have "liseq' (arr_conv a) (nat i) =
   1.571 +        liseq' (arr_conv a) (nat pmax) + 1"
   1.572 +        by (rule longest_iseq4)
   1.573 +      with True H1 H3 H4 show ?thesis
   1.574 +        by simp
   1.575 +    next
   1.576 +      case False
   1.577 +      with H1 i2 show ?thesis
   1.578 +        by simp
   1.579 +    qed
   1.580 +  }
   1.581 +  then show ?C1 by simp
   1.582 +  from eq pmax1 pmax2
   1.583 +  have "liseq (arr_conv a) (Suc (nat i)) =
   1.584 +    liseq (arr_conv a) (nat i) + 1"
   1.585 +    by (rule longest_iseq3)
   1.586 + with H2 H3 H4 show ?C2
   1.587 +    by (simp add: idx_conv_suc)
   1.588 +qed
   1.589 +
   1.590 +spark_vc procedure_liseq_length_7
   1.591 +proof -
   1.592 +  from H1 show ?C1
   1.593 +    by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
   1.594 +  from H6
   1.595 +  have m: "max_ext (arr_conv a) (nat i) (nat i) + 1 =
   1.596 +    liseq' (arr_conv a) (nat i)"
   1.597 +    by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
   1.598 +  with H2 H18
   1.599 +  have gt: "liseq (arr_conv a) (nat i) < liseq' (arr_conv a) (nat i)"
   1.600 +    by simp
   1.601 +  then have "liseq' (arr_conv a) (nat i) = liseq (arr_conv a) (nat i) + 1"
   1.602 +    by (rule longest_iseq2 [symmetric])
   1.603 +  with H2 m show ?C2 by simp
   1.604 +  from gt have "liseq (arr_conv a) (Suc (nat i)) = liseq' (arr_conv a) (nat i)"
   1.605 +    by (rule longest_iseq2')
   1.606 +  with m H6 show ?C3 by (simp add: idx_conv_suc)
   1.607 +qed
   1.608 +
   1.609 +spark_vc procedure_liseq_length_8
   1.610 +proof -
   1.611 +  {
   1.612 +    fix i2
   1.613 +    assume i2: "0 \<le> i2" "i2 \<le> i"
   1.614 +    have "(l(i := max_ext' a i i + 1)) i2 =
   1.615 +      int (liseq' (arr_conv a) (nat i2))"
   1.616 +    proof (cases "i2 = i")
   1.617 +      case True
   1.618 +      with H1 show ?thesis
   1.619 +        by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
   1.620 +    next
   1.621 +      case False
   1.622 +      with H1 i2 show ?thesis by simp
   1.623 +    qed
   1.624 +  }
   1.625 +  then show ?C1 by simp
   1.626 +  from H2 H6 H18
   1.627 +  have "liseq' (arr_conv a) (nat i) \<le> liseq (arr_conv a) (nat i)"
   1.628 +    by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
   1.629 +  then have "liseq (arr_conv a) (Suc (nat i)) = liseq (arr_conv a) (nat i)"
   1.630 +    by (rule longest_iseq5)
   1.631 +  with H2 H6 show ?C2 by (simp add: idx_conv_suc)
   1.632 +qed
   1.633 +
   1.634 +spark_vc procedure_liseq_length_12
   1.635 +  by (simp add: max_ext_def)
   1.636 +
   1.637 +spark_vc procedure_liseq_length_13
   1.638 +  using H1 H6 H13 H21 H22
   1.639 +  by (simp add: max_ext_def
   1.640 +    idx_conv_suc liseq'_Suc_unfold max_def del: Max_less_iff)
   1.641 +
   1.642 +spark_vc procedure_liseq_length_14
   1.643 +  using H1 H6 H13 H21
   1.644 +  by (cases "a j \<le> a i")
   1.645 +    (simp_all add: max_ext_def
   1.646 +      idx_conv_suc liseq'_Suc_unfold liseq'_Suc_unfold')
   1.647 +
   1.648 +spark_vc procedure_liseq_length_19
   1.649 +  using H3 H4 H5 H8 H9
   1.650 +  apply (rule_tac y="int (nat i)" in order_trans)
   1.651 +  apply (cut_tac A="arr_conv a" and i="nat i" and j="nat i" in max_ext_limit)
   1.652 +  apply simp_all
   1.653 +  done
   1.654 +
   1.655 +spark_vc procedure_liseq_length_23
   1.656 +  using H2 H3 H4 H7 H8 H11
   1.657 +  apply (rule_tac y="int (nat i)" in order_trans)
   1.658 +  apply (cut_tac A="arr_conv a" and i="nat i" in liseq_limit)
   1.659 +  apply simp_all
   1.660 +  done
   1.661 +
   1.662 +spark_vc procedure_liseq_length_29
   1.663 +  using H2 H3 H8 H13
   1.664 +  by (simp add: add1_zle_eq [symmetric])
   1.665 +
   1.666 +spark_end
   1.667 +
   1.668 +end