Theory Longest_Increasing_Subsequence

(*  Title:      HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
    Author:     Stefan Berghofer
    Copyright:  secunet Security Networks AG
*)

theory Longest_Increasing_Subsequence
imports "HOL-SPARK.SPARK"
begin

text ‹
Set of all increasing subsequences in a prefix of an array
›

definition iseq :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat set set" where
  "iseq xs l = {is. (∀i∈is. i < l) ∧
     (∀i∈is. ∀j∈is. i ≤ j ⟶ xs i ≤ xs j)}"

text ‹
Length of longest increasing subsequence in a prefix of an array
›

definition liseq :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat" where
  "liseq xs i = Max (card ` iseq xs i)"

text ‹
Length of longest increasing subsequence ending at a particular position
›

definition liseq' :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat" where
  "liseq' xs i = Max (card ` (iseq xs (Suc i) ∩ {is. Max is = i}))"

lemma iseq_finite: "finite (iseq xs i)"
  apply (simp add: iseq_def)
  apply (rule finite_subset [OF _
    finite_Collect_subsets [of "{j. j < i}"]])
  apply auto
  done

lemma iseq_finite': "is ∈ iseq xs i ⟹ finite is"
  by (auto simp add: iseq_def bounded_nat_set_is_finite)

lemma iseq_singleton: "i < l ⟹ {i} ∈ iseq xs l"
  by (simp add: iseq_def)

lemma iseq_trivial: "{} ∈ iseq xs i"
  by (simp add: iseq_def)

lemma iseq_nonempty: "iseq xs i ≠ {}"
  by (auto intro: iseq_trivial)

lemma liseq'_ge1: "1 ≤ liseq' xs x"
  apply (simp add: liseq'_def)
  apply (subgoal_tac "iseq xs (Suc x) ∩ {is. Max is = x} ≠ {}")
  apply (simp add: Max_ge_iff iseq_finite)
  apply (rule_tac x="{x}" in bexI)
  apply (auto intro: iseq_singleton)
  done

lemma liseq_expand:
  assumes R: "⋀is. liseq xs i = card is ⟹ is ∈ iseq xs i ⟹
    (⋀js. js ∈ iseq xs i ⟹ card js ≤ card is) ⟹ P"
  shows "P"
proof -
  have "Max (card ` iseq xs i) ∈ card ` iseq xs i"
    by (rule Max_in) (simp_all add: iseq_finite iseq_nonempty)
  then obtain js where js: "liseq xs i = card js" and "js ∈ iseq xs i"
    by (rule imageE) (simp add: liseq_def)
  moreover {
    fix js'
    assume "js' ∈ iseq xs i"
    then have "card js' ≤ card js"
      by (simp add: js [symmetric] liseq_def iseq_finite iseq_trivial)
  }
  ultimately show ?thesis by (rule R)
qed

lemma liseq'_expand:
  assumes R: "⋀is. liseq' xs i = card is ⟹ is ∈ iseq xs (Suc i) ⟹
    finite is ⟹ Max is = i ⟹
    (⋀js. js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹ card js ≤ card is) ⟹
    is ≠ {} ⟹ P"
  shows "P"
proof -
  have "Max (card ` (iseq xs (Suc i) ∩ {is. Max is = i})) ∈
    card ` (iseq xs (Suc i) ∩ {is. Max is = i})"
    by (auto simp add: iseq_finite intro!: iseq_singleton Max_in)
  then obtain js where js: "liseq' xs i = card js" and "js ∈ iseq xs (Suc i)"
    and "finite js" and "Max js = i"
    by (auto simp add: liseq'_def intro: iseq_finite')
  moreover {
    fix js'
    assume "js' ∈ iseq xs (Suc i)" "Max js' = i"
    then have "card js' ≤ card js"
      by (auto simp add: js [symmetric] liseq'_def iseq_finite intro!: iseq_singleton)
  }
  note max = this
  moreover have "card {i} ≤ card js"
    by (rule max) (simp_all add: iseq_singleton)
  then have "js ≠ {}" by auto
  ultimately show ?thesis by (rule R)
qed

lemma liseq'_ge:
  "j = card js ⟹ js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹
  js ≠ {} ⟹ j ≤ liseq' xs i"
  by (simp add: liseq'_def iseq_finite)

lemma liseq'_eq:
  "j = card js ⟹ js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹
  js ≠ {} ⟹ (⋀js'. js' ∈ iseq xs (Suc i) ⟹ Max js' = i ⟹ finite js' ⟹
    js' ≠ {} ⟹ card js' ≤ card js) ⟹
  j = liseq' xs i"
  by (fastforce simp add: liseq'_def iseq_finite
    intro: Max_eqI [symmetric])

lemma liseq_ge:
  "j = card js ⟹ js ∈ iseq xs i ⟹ j ≤ liseq xs i"
  by (auto simp add: liseq_def iseq_finite)

lemma liseq_eq:
  "j = card js ⟹ js ∈ iseq xs i ⟹
  (⋀js'. js' ∈ iseq xs i ⟹ finite js' ⟹
    js' ≠ {} ⟹ card js' ≤ card js) ⟹
  j = liseq xs i"
  by (fastforce simp add: liseq_def iseq_finite
    intro: Max_eqI [symmetric])

lemma max_notin: "finite xs ⟹ Max xs < x ⟹ x ∉ xs"
  by (cases "xs = {}") auto

lemma iseq_insert:
  "xs (Max is) ≤ xs i ⟹ is ∈ iseq xs i ⟹
  is ∪ {i} ∈ iseq xs (Suc i)"
  apply (frule iseq_finite')
  apply (cases "is = {}")
  apply (auto simp add: iseq_def)
  apply (rule order_trans [of _ "xs (Max is)"])
  apply auto
  apply (thin_tac "∀a∈is. a < i")
  apply (drule_tac x=ia in bspec)
  apply assumption
  apply (drule_tac x="Max is" in bspec)
  apply (auto intro: Max_in)
  done

lemma iseq_diff: "is ∈ iseq xs (Suc (Max is)) ⟹
  is - {Max is} ∈ iseq xs (Suc (Max (is - {Max is})))"
  apply (frule iseq_finite')
  apply (simp add: iseq_def less_Suc_eq_le)
  done

lemma iseq_butlast:
  assumes "js ∈ iseq xs (Suc i)" and "js ≠ {}"
  and "Max js ≠ i"
  shows "js ∈ iseq xs i"
proof -
  from assms have fin: "finite js"
    by (simp add: iseq_finite')
  with assms have "Max js ∈ js"
    by auto
  with assms have "Max js < i"
    by (auto simp add: iseq_def)
  with fin assms have "∀j∈js. j < i"
    by simp
  with assms show ?thesis
    by (simp add: iseq_def)
qed

lemma iseq_mono: "is ∈ iseq xs i ⟹ i ≤ j ⟹ is ∈ iseq xs j"
  by (auto simp add: iseq_def)

lemma diff_nonempty:
  assumes "1 < card is"
  shows "is - {i} ≠ {}"
proof -
  from assms have fin: "finite is" by (auto intro: card_ge_0_finite)
  with assms fin have "card is - 1 ≤ card (is - {i})"
    by (simp add: card_Diff_singleton_if)
  with assms have "0 < card (is - {i})" by simp
  then show ?thesis by (simp add: card_gt_0_iff)
qed

lemma Max_diff:
  assumes "1 < card is"
  shows "Max (is - {Max is}) < Max is"
proof -
  from assms have "finite is" by (auto intro: card_ge_0_finite)
  moreover from assms have "is - {Max is} ≠ {}"
    by (rule diff_nonempty)
  ultimately show ?thesis using assms
    apply (auto simp add: not_less)
    apply (subgoal_tac "a ≤ Max is")
    apply auto
    done
qed

lemma iseq_nth: "js ∈ iseq xs l ⟹ 1 < card js ⟹
  xs (Max (js - {Max js})) ≤ xs (Max js)"
  apply (auto simp add: iseq_def)
  apply (subgoal_tac "Max (js - {Max js}) ∈ js")
  apply (thin_tac "∀i∈js. i < l")
  apply (drule_tac x="Max (js - {Max js})" in bspec)
  apply assumption
  apply (drule_tac x="Max js" in bspec)
  using card_gt_0_iff [of js]
  apply simp
  using Max_diff [of js]
  apply simp
  using Max_in [of "js - {Max js}", OF _ diff_nonempty] card_gt_0_iff [of js]
  apply auto
  done

lemma card_leq1_singleton:
  assumes "finite xs" "xs ≠ {}" "card xs ≤ 1"
  obtains x where "xs = {x}"
  using assms
  by induct simp_all

lemma longest_iseq1:
  "liseq' xs i =
   Max ({0} ∪ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}) + 1"
proof -
  have "Max ({0} ∪ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}) = liseq' xs i - 1"
  proof (rule Max_eqI)
    fix y
    assume "y ∈ {0} ∪ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}"
    then show "y ≤ liseq' xs i - 1"
    proof
      assume "y ∈ {liseq' xs j |j. j < i ∧ xs j ≤ xs i}"
      then obtain j where j: "j < i" "xs j ≤ xs i" "y = liseq' xs j"
        by auto
      have "liseq' xs j + 1 ≤ liseq' xs i"
      proof (rule liseq'_expand)
        fix "is"
        assume H: "liseq' xs j = card is" "is ∈ iseq xs (Suc j)"
          "finite is" "Max is = j" "is ≠ {}"
        from H j have "card is + 1 = card (is ∪ {i})"
          by (simp add: card.insert_remove max_notin)
        moreover {
          from H j have "xs (Max is) ≤ xs i" by simp
          moreover from ‹j < i› have "Suc j ≤ i" by simp
          with ‹is ∈ iseq xs (Suc j)› have "is ∈ iseq xs i"
            by (rule iseq_mono)
          ultimately have "is ∪ {i} ∈ iseq xs (Suc i)"
          by (rule iseq_insert)
        } moreover from H j have "Max (is ∪ {i}) = i" by simp
        moreover have "is ∪ {i} ≠ {}" by simp
        ultimately have "card is + 1 ≤ liseq' xs i"
          by (rule liseq'_ge)
        with H show ?thesis by simp
      qed
      with j show "y ≤ liseq' xs i - 1"
        by simp
    qed simp
  next
    have "liseq' xs i ≤ 1 ∨
      (∃j. liseq' xs i - 1 = liseq' xs j ∧ j < i ∧ xs j ≤ xs i)"
    proof (rule liseq'_expand)
      fix "is"
      assume H: "liseq' xs i = card is" "is ∈ iseq xs (Suc i)"
        "finite is" "Max is = i" "is ≠ {}"
      assume R: "⋀js. js ∈ iseq xs (Suc i) ⟹ Max js = i ⟹
        card js ≤ card is"
      show ?thesis
      proof (cases "card is ≤ 1")
        case True with H show ?thesis by simp
      next
        case False
        then have "1 < card is" by simp
        then have "Max (is - {Max is}) < Max is"
          by (rule Max_diff)
        from ‹is ∈ iseq xs (Suc i)› ‹1 < card is›
        have "xs (Max (is - {Max is})) ≤ xs (Max is)"
          by (rule iseq_nth)
        have "card is - 1 = liseq' xs (Max (is - {i}))"
        proof (rule liseq'_eq)
          from ‹Max is = i› [symmetric] ‹finite is› ‹is ≠ {}›
          show "card is - 1 = card (is - {i})" by simp
        next
          from ‹is ∈ iseq xs (Suc i)› ‹Max is = i› [symmetric]
          show "is - {i} ∈ iseq xs (Suc (Max (is - {i})))"
            by simp (rule iseq_diff)
        next
          from ‹1 < card is›
          show "is - {i} ≠ {}" by (rule diff_nonempty)
        next
          fix js
          assume "js ∈ iseq xs (Suc (Max (is - {i})))"
            "Max js = Max (is - {i})" "finite js" "js ≠ {}"
          from ‹xs (Max (is - {Max is})) ≤ xs (Max is)›
            ‹Max js = Max (is - {i})› ‹Max is = i›
          have "xs (Max js) ≤ xs i" by simp
          moreover from ‹Max is = i› ‹Max (is - {Max is}) < Max is›
          have "Suc (Max (is - {i})) ≤ i"
            by simp
          with ‹js ∈ iseq xs (Suc (Max (is - {i})))›
          have "js ∈ iseq xs i"
            by (rule iseq_mono)
          ultimately have "js ∪ {i} ∈ iseq xs (Suc i)"
            by (rule iseq_insert)
          moreover from ‹js ≠ {}› ‹finite js› ‹Max js = Max (is - {i})›
            ‹Max is = i› [symmetric] ‹Max (is - {Max is}) < Max is›
          have "Max (js ∪ {i}) = i"
            by simp
          ultimately have "card (js ∪ {i}) ≤ card is" by (rule R)
          moreover from ‹Max is = i› [symmetric] ‹finite js›
            ‹Max (is - {Max is}) < Max is› ‹Max js = Max (is - {i})›
          have "i ∉ js" by (simp add: max_notin)
          with ‹finite js›
          have "card (js ∪ {i}) = card ((js ∪ {i}) - {i}) + 1"
            by simp
          ultimately show "card js ≤ card (is - {i})"
            using ‹i ∉ js› ‹Max is = i› [symmetric] ‹is ≠ {}› ‹finite is›
            by simp
        qed simp
        with H ‹Max (is - {Max is}) < Max is›
          ‹xs (Max (is - {Max is})) ≤ xs (Max is)›
        show ?thesis by auto
      qed
    qed
    then show "liseq' xs i - 1 ∈ {0} ∪
      {liseq' xs j |j. j < i ∧ xs j ≤ xs i}" by simp
  qed simp
  moreover have "1 ≤ liseq' xs i" by (rule liseq'_ge1)
  ultimately show ?thesis by simp
qed

lemma longest_iseq2': "liseq xs i < liseq' xs i ⟹
  liseq xs (Suc i) = liseq' xs i"
  apply (rule_tac xs=xs and i=i in liseq'_expand)
  apply simp
  apply (rule liseq_eq [symmetric])
  apply (rule refl)
  apply assumption
  apply (case_tac "Max js' = i")
  apply simp
  apply (drule_tac js=js' in iseq_butlast)
  apply assumption+
  apply (drule_tac js=js' in liseq_ge [OF refl])
  apply simp
  done

lemma longest_iseq2: "liseq xs i < liseq' xs i ⟹
  liseq xs i + 1 = liseq' xs i"
  apply (rule_tac xs=xs and i=i in liseq'_expand)
  apply simp
  apply (rule_tac xs=xs and i=i in liseq_expand)
  apply (drule_tac s="Max is" in sym)
  apply simp
  apply (case_tac "card is ≤ 1")
  apply simp
  apply (drule iseq_diff)
  apply (drule_tac i="Suc (Max (is - {Max is}))" and j="Max is" in iseq_mono)
  apply (simp add: less_eq_Suc_le [symmetric])
  apply (rule Max_diff)
  apply simp
  apply (drule_tac x="is - {Max is}" in meta_spec,
    drule meta_mp, assumption)
  apply simp
  done

lemma longest_iseq3:
  "liseq xs j = liseq' xs i ⟹ xs i ≤ xs j ⟹ i < j ⟹
  liseq xs (Suc j) = liseq xs j + 1"
  apply (rule_tac xs=xs and i=j in liseq_expand)
  apply simp
  apply (rule_tac xs=xs and i=i in liseq'_expand)
  apply simp
  apply (rule_tac js="isa ∪ {j}" in liseq_eq [symmetric])
  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
  apply (rule iseq_insert)
  apply simp
  apply (erule iseq_mono)
  apply simp
  apply (case_tac "j = Max js'")
  apply simp
  apply (drule iseq_diff)
  apply (drule_tac x="js' - {j}" in meta_spec)
  apply (drule meta_mp)
  apply simp
  apply (case_tac "card js' ≤ 1")
  apply (erule_tac xs=js' in card_leq1_singleton)
  apply assumption+
  apply (simp add: iseq_trivial)
  apply (erule iseq_mono)
  apply (simp add: less_eq_Suc_le [symmetric])
  apply (rule Max_diff)
  apply simp
  apply (rule le_diff_iff [THEN iffD1, of 1])
  apply (simp add: card_0_eq [symmetric] del: card_0_eq)
  apply (simp add: card.insert_remove)
  apply (subgoal_tac "card (js' - {j}) = card js' - 1")
  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
  apply (frule_tac A=js' in Max_in)
  apply assumption
  apply (simp add: card_Diff_singleton_if)
  apply (drule_tac js=js' in iseq_butlast)
  apply assumption
  apply (erule not_sym)
  apply (drule_tac x=js' in meta_spec)
  apply (drule meta_mp)
  apply assumption
  apply (simp add: card_insert_disjoint max_notin)
  done

lemma longest_iseq4:
  "liseq xs j = liseq' xs i ⟹ xs i ≤ xs j ⟹ i < j ⟹
  liseq' xs j = liseq' xs i + 1"
  apply (rule_tac xs=xs and i=j in liseq_expand)
  apply simp
  apply (rule_tac xs=xs and i=i in liseq'_expand)
  apply simp
  apply (rule_tac js="isa ∪ {j}" in liseq'_eq [symmetric])
  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
  apply (rule iseq_insert)
  apply simp
  apply (erule iseq_mono)
  apply simp
  apply simp
  apply simp
  apply (drule_tac s="Max js'" in sym)
  apply simp
  apply (drule iseq_diff)
  apply (drule_tac x="js' - {j}" in meta_spec)
  apply (drule meta_mp)
  apply simp
  apply (case_tac "card js' ≤ 1")
  apply (erule_tac xs=js' in card_leq1_singleton)
  apply assumption+
  apply (simp add: iseq_trivial)
  apply (erule iseq_mono)
  apply (simp add: less_eq_Suc_le [symmetric])
  apply (rule Max_diff)
  apply simp
  apply (rule le_diff_iff [THEN iffD1, of 1])
  apply (simp add: card_0_eq [symmetric] del: card_0_eq)
  apply (simp add: card.insert_remove)
  apply (subgoal_tac "card (js' - {j}) = card js' - 1")
  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
  apply (frule_tac A=js' in Max_in)
  apply assumption
  apply (simp add: card_Diff_singleton_if)
  done

lemma longest_iseq5: "liseq' xs i ≤ liseq xs i ⟹
  liseq xs (Suc i) = liseq xs i"
  apply (rule_tac i=i and xs=xs in liseq'_expand)
  apply simp
  apply (rule_tac xs=xs and i=i in liseq_expand)
  apply simp
  apply (rule liseq_eq [symmetric])
  apply (rule refl)
  apply (erule iseq_mono)
  apply simp
  apply (case_tac "Max js' = i")
  apply (drule_tac x=js' in meta_spec)
  apply simp
  apply (drule iseq_butlast, assumption, assumption)
  apply simp
  done

lemma liseq_empty: "liseq xs 0 = 0"
  apply (rule_tac js="{}" in liseq_eq [symmetric])
  apply simp
  apply (rule iseq_trivial)
  apply (simp add: iseq_def)
  done

lemma liseq'_singleton: "liseq' xs 0 = 1"
  by (simp add: longest_iseq1 [of _ 0])

lemma liseq_singleton: "liseq xs (Suc 0) = Suc 0"
  by (simp add: longest_iseq2' liseq_empty liseq'_singleton)

lemma liseq'_Suc_unfold:
  "A j ≤ x ⟹
   (insert 0 {liseq' A j' |j'. j' < Suc j ∧ A j' ≤ x}) =
   (insert 0 {liseq' A j' |j'. j' < j ∧ A j' ≤ x}) ∪
   {liseq' A j}"
  by (auto simp add: less_Suc_eq)

lemma liseq'_Suc_unfold':
  "¬ (A j ≤ x) ⟹
   {liseq' A j' |j'. j' < Suc j ∧ A j' ≤ x} =
   {liseq' A j' |j'. j' < j ∧ A j' ≤ x}"
  by (auto simp add: less_Suc_eq)

lemma iseq_card_limit:
  assumes "is ∈ iseq A i"
  shows "card is ≤ i"
proof -
  from assms have "is ⊆ {0..<i}"
    by (auto simp add: iseq_def)
  with finite_atLeastLessThan have "card is ≤ card {0..<i}"
    by (rule card_mono)
  with card_atLeastLessThan show ?thesis by simp
qed

lemma liseq_limit: "liseq A i ≤ i"
  by (rule_tac xs=A and i=i in liseq_expand)
    (simp add: iseq_card_limit)

lemma liseq'_limit: "liseq' A i ≤ i + 1"
  by (rule_tac xs=A and i=i in liseq'_expand)
    (simp add: iseq_card_limit)

definition max_ext :: "(nat ⇒ 'a::linorder) ⇒ nat ⇒ nat ⇒ nat" where
  "max_ext A i j = Max ({0} ∪ {liseq' A j' |j'. j' < j ∧ A j' ≤ A i})"

lemma max_ext_limit: "max_ext A i j ≤ j"
  apply (auto simp add: max_ext_def)
  apply (drule Suc_leI)
  apply (cut_tac i=j' and A=A in liseq'_limit)
  apply simp
  done


text ‹Proof functions›

abbreviation (input)
  "arr_conv a ≡ (λn. a (int n))"

lemma idx_conv_suc:
  "0 ≤ i ⟹ nat (i + 1) = nat i + 1"
  by simp

abbreviation liseq_ends_at' :: "(int ⇒ 'a::linorder) ⇒ int ⇒ int" where
  "liseq_ends_at' A i ≡ int (liseq' (λl. A (int l)) (nat i))"

abbreviation liseq_prfx' :: "(int ⇒ 'a::linorder) ⇒ int ⇒ int" where
  "liseq_prfx' A i ≡ int (liseq (λl. A (int l)) (nat i))"

abbreviation max_ext' :: "(int ⇒ 'a::linorder) ⇒ int ⇒ int ⇒ int" where
  "max_ext' A i j ≡ int (max_ext (λl. A (int l)) (nat i) (nat j))"

spark_proof_functions
  liseq_ends_at = "liseq_ends_at' :: (int ⇒ int) ⇒ int ⇒ int"
  liseq_prfx = "liseq_prfx' :: (int ⇒ int) ⇒ int ⇒ int"
  max_ext = "max_ext' :: (int ⇒ int) ⇒ int ⇒ int ⇒ int"


text ‹The verification conditions›

spark_open ‹liseq/liseq_length›

spark_vc procedure_liseq_length_5
  by (simp_all add: liseq_singleton liseq'_singleton)

spark_vc procedure_liseq_length_6
proof -
  from H1 H2 H3 H4
  have eq: "liseq (arr_conv a) (nat i) =
    liseq' (arr_conv a) (nat pmax)"
    by simp
  from H14 H3 H4
  have pmax1: "arr_conv a (nat pmax) ≤ arr_conv a (nat i)"
    by simp
  from H3 H4 have pmax2: "nat pmax < nat i"
    by simp
  {
    fix i2
    assume i2: "0 ≤ i2" "i2 ≤ i"
    have "(l(i := l pmax + 1)) i2 =
      int (liseq' (arr_conv a) (nat i2))"
    proof (cases "i2 = i")
      case True
      from eq pmax1 pmax2 have "liseq' (arr_conv a) (nat i) =
        liseq' (arr_conv a) (nat pmax) + 1"
        by (rule longest_iseq4)
      with True H1 H3 H4 show ?thesis
        by simp
    next
      case False
      with H1 i2 show ?thesis
        by simp
    qed
  }
  then show ?C1 by simp
  from eq pmax1 pmax2
  have "liseq (arr_conv a) (Suc (nat i)) =
    liseq (arr_conv a) (nat i) + 1"
    by (rule longest_iseq3)
 with H2 H3 H4 show ?C2
    by (simp add: idx_conv_suc)
qed

spark_vc procedure_liseq_length_7
proof -
  from H1 show ?C1
    by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
  from H6
  have m: "max_ext (arr_conv a) (nat i) (nat i) + 1 =
    liseq' (arr_conv a) (nat i)"
    by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
  with H2 H18
  have gt: "liseq (arr_conv a) (nat i) < liseq' (arr_conv a) (nat i)"
    by simp
  then have "liseq' (arr_conv a) (nat i) = liseq (arr_conv a) (nat i) + 1"
    by (rule longest_iseq2 [symmetric])
  with H2 m show ?C2 by simp
  from gt have "liseq (arr_conv a) (Suc (nat i)) = liseq' (arr_conv a) (nat i)"
    by (rule longest_iseq2')
  with m H6 show ?C3 by (simp add: idx_conv_suc)
qed

spark_vc procedure_liseq_length_8
proof -
  {
    fix i2
    assume i2: "0 ≤ i2" "i2 ≤ i"
    have "(l(i := max_ext' a i i + 1)) i2 =
      int (liseq' (arr_conv a) (nat i2))"
    proof (cases "i2 = i")
      case True
      with H1 show ?thesis
        by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
    next
      case False
      with H1 i2 show ?thesis by simp
    qed
  }
  then show ?C1 by simp
  from H2 H6 H18
  have "liseq' (arr_conv a) (nat i) ≤ liseq (arr_conv a) (nat i)"
    by (simp add: max_ext_def longest_iseq1 [of _ "nat i"])
  then have "liseq (arr_conv a) (Suc (nat i)) = liseq (arr_conv a) (nat i)"
    by (rule longest_iseq5)
  with H2 H6 show ?C2 by (simp add: idx_conv_suc)
qed

spark_vc procedure_liseq_length_12
  by (simp add: max_ext_def)

spark_vc procedure_liseq_length_13
  using H1 H6 H13 H21 H22
  by (simp add: max_ext_def
    idx_conv_suc liseq'_Suc_unfold max_def del: Max_less_iff)

spark_vc procedure_liseq_length_14
  using H1 H6 H13 H21
  by (cases "a j ≤ a i")
    (simp_all add: max_ext_def
      idx_conv_suc liseq'_Suc_unfold liseq'_Suc_unfold')

spark_vc procedure_liseq_length_19
  using H3 H4 H5 H8 H9
  apply (rule_tac y="int (nat i)" in order_trans)
  apply (cut_tac A="arr_conv a" and i="nat i" and j="nat i" in max_ext_limit)
  apply simp_all
  done

spark_vc procedure_liseq_length_23
  using H2 H3 H4 H7 H8 H11
  apply (rule_tac y="int (nat i)" in order_trans)
  apply (cut_tac A="arr_conv a" and i="nat i" in liseq_limit)
  apply simp_all
  done

spark_vc procedure_liseq_length_29
  using H2 H3 H8 H13
  by (simp add: add1_zle_eq [symmetric])

spark_end

end