Theory Gale_Shapley1

(*
Stepwise refinement of the Gale-Shapley algorithm down to executable functional code.

Author: Tobias Nipkow
*)

section "Part 1: Refinement down to lists"

theory Gale_Shapley1
imports
  "HOL-Hoare.Hoare_Logic"
  "List-Index.List_Index"
  "HOL-Library.While_Combinator"
  "HOL-Library.LaTeXsugar"
begin

subsection ‹Misc›

lemmas conj12 = conjunct1 conjunct2

syntax
  "_assign_list" :: "idt ⇒ nat ⇒ 'b ⇒ 'com"  ("(2_[_] :=/ _)" [70, 0, 65] 61)

translations
  "xs[n] := e" ⇀ "xs := CONST list_update xs n e"

abbreviation upt_set :: "nat ⇒ nat set" ("{<_}") where
"{<n} ≡ {0..<n}"

(* Maybe also require y : set P? *)
definition prefers :: "'a list ⇒ 'a ⇒ 'a ⇒ bool" where
"prefers P x y = (index P x < index P y)"

abbreviation prefa :: "'a list ⇒ 'a ⇒ 'a ⇒ bool" ("(_ ⊢/ _ < _)" [50,50,50] 50) where
"P ⊢ x < y ≡ prefers P x y"

lemma prefers_asym: "P ⊢ x < y ⟹ ¬ P ⊢ y < x"
by(simp add: prefers_def)

lemma prefers_trans: "P ⊢ x < y ⟹ P ⊢ y < z ⟹ P ⊢ x < z"
by (meson order_less_trans prefers_def)

fun rk_of_pref :: "nat ⇒ nat list ⇒ nat list ⇒ nat list" where
"rk_of_pref r rs (n#ns) = (rk_of_pref (r+1) rs ns)[n := r]" |
"rk_of_pref r rs [] = rs"

definition ranking :: "nat list ⇒ nat list" where
"ranking P = rk_of_pref 0 (replicate (length P) 0) P"

lemma length_rk_of_pref[simp]: "length(rk_of_pref v vs P) = length vs"
by(induction P arbitrary: v)(auto)

lemma nth_rk_of_pref: "⟦ length P ≤ length rs; i ∈ set P; distinct P; set P ⊆ {<length rs} ⟧
 ⟹ rk_of_pref r rs P ! i = index P i + r"
by(induction P arbitrary: r i) (auto simp add: nth_list_update)

lemma ranking_index: "⟦ length P = n; set P = {<n} ⟧ ⟹ ranking P = map (index P) [0..<length P]"
by(simp add: list_eq_iff_nth_eq ranking_def card_distinct nth_rk_of_pref)

lemma ranking_iff_pref:  "⟦ set P = {<length P}; i < length P; j < length P ⟧
 ⟹ ranking P ! i < ranking P ! j ⟷ P ⊢ i < j"
by(simp add: ranking_index prefers_def)


subsection ‹Fixing the preference lists›
 
type_synonym prefs = "nat list list"

locale Pref =
fixes n
fixes P :: prefs
fixes Q :: prefs
defines "n ≡ length P"
assumes length_Q: "length Q = n"
assumes P_set: "a < n  ⟹ length(P!a) = n ∧ set(P!a) = {<n}"
assumes Q_set: "b < n ⟹ length(Q!b) = n ∧ set(Q!b) = {<n}"
begin


abbreviation wf :: "nat list ⇒ bool" where
"wf xs ≡ length xs = n ∧ set xs ⊆ {<n}"

lemma wf_less_n: "⟦ wf A; a < n ⟧ ⟹ A!a < n"
by (simp add: subset_eq)

corollary wf_le_n1: "⟦ wf A; a < n ⟧ ⟹ A!a ≤ n-1"
using wf_less_n by fastforce

lemma sumA_ub: "wf A ⟹ (∑a<n. A!a) ≤ n*(n-1)"
using sum_bounded_above[of "{..<n}" "((!) A)" "n-1"] wf_le_n1[of A] by (simp)


subsection ‹The (termination) variant(s)›

text ‹Basic idea: either some ‹A!a› is incremented or size of ‹M› is incremented, but this cannot
go on forever because in the worst case all ‹A!a = n-1› and ‹M = n›. Because ‹n*(n-1) + n = n^2›,
this leads to the following simple variant:›

definition var0 :: "nat list ⇒ nat set ⇒ nat" where
[simp]: "var0 A M = (n^2 - ((∑a<n. A!a) + card M))"

lemma var0_match:
assumes "wf A" "M ⊆ {<n}" "a < n ∧ a ∉ M"
shows "var0 A (M ∪ {a}) < var0 A M"
proof -
  have 2: "M ⊂ {<n}" using assms(2-3) by auto
  have 3: "card M < n" using psubset_card_mono[OF _ 2] by simp
  then show ?thesis
    using sumA_ub[OF assms(1)] assms(3) finite_subset[OF assms(2)]
    by (simp add: power2_eq_square algebra_simps le_diff_conv2)
qed

lemma var0_next:
assumes "wf A" "M ⊆ {<n}" "M ≠ {<n}" "a' < n"
shows "var0 (A[a' := A ! a' + 1]) M < var0 A M"
proof -
  have 0: "card M < n" using assms(2,3)
    by (metis atLeast0LessThan card_lessThan card_subset_eq finite_lessThan lessThan_iff nat_less_le
              subset_eq_atLeast0_lessThan_card)
  have *: "1 + (∑a<n. A!a) + card M ≤ n*n"
    using sumA_ub[OF assms(1)] 0 by (simp add: algebra_simps le_diff_conv2)
  have "var0 (A[a' := A ! a' + 1]) M = n*n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M)"
    using assms by(simp add: power2_eq_square nth_list_update sum.If_cases lessThan_atLeast0 flip:Diff_eq)
  also have "… = n^2 - (1 + (∑a<n. A!a) + card M)"
    using sum.insert_remove[of "{<n}" "nth A" a',simplified,symmetric] assms(4)
    by (simp add:insert_absorb lessThan_atLeast0 power2_eq_square)
  also have "… < n^2 - ((∑a<n. A!a) + card M)" unfolding power2_eq_square using * by linarith
  finally show ?thesis unfolding var0_def .
qed

definition var :: "nat list ⇒ nat set ⇒ nat" where
[simp]: "var A M = (n^2 - n + 1 - ((∑a<n. A!a) + card M))"

lemma sumA_ub2:
assumes "a' < n" "A!a' ≤ n-1" "∀a < n. a ≠ a' ⟶ A!a ≤ n-2"
shows "(∑a<n. A!a) ≤ (n-1)*(n-1)"
proof -
  have "(∑a<n. A!a) = (∑a ∈ ({<n}-{a'}) ∪ {a'}. A!a)"
    by (simp add: assms(1) atLeast0LessThan insert_absorb)
  also have "… =(∑a ∈ {<n}-{a'}. A!a) + A!a'"
    by (simp add: sum.insert_remove)
  also have "… ≤ (∑a ∈ {<n}-{a'}. A!a) + (n-1)" using assms(2) by linarith
  also have "… ≤ (n-1)*(n-2) + (n-1)"
    using sum_bounded_above[of "{..<n}-{a'}" "((!) A)" "n-2"] assms(1,3)
    by (simp add: atLeast0LessThan)
  also have "… = (n-1)*(n-1)"
    by (metis Suc_diff_Suc Suc_eq_plus1 add.commute diff_is_0_eq' linorder_not_le mult_Suc_right mult_cancel_left nat_1_add_1)
  finally show ?thesis .
qed

definition "match A a = P ! a ! (A ! a)"

lemma match_less_n: "⟦ wf A; a < n ⟧ ⟹ match A a < n"
by (metis P_set atLeastLessThan_iff match_def nth_mem subset_eq)

lemma match_upd_neq: "⟦ wf A; a < n; a ≠ a' ⟧ ⟹ match (A[a := b]) a' = match A a'"
by (simp add: match_def)

definition stable :: "nat list ⇒ nat set ⇒ bool" where
"stable A M = (¬(∃a∈M. ∃a'∈M. P ! a ⊢ match A a' < match A a ∧ Q ! match A a' ⊢ a < a'))"

text ‹The set of Bs that an A would prefer to its current match,
i.e. all Bs above its current match ‹A!a›.›
abbreviation preferred where
"preferred A a == nth (P!a) ` {<A!a}"

definition matching where [simp]:
"matching A M = (wf A ∧ inj_on (match A) M)"


text ‹If ‹a'› is unmatched and final then all other ‹a› are matched:›

lemma final_last:
assumes M: "M ⊆ {<n}" and inj: "inj_on (match A) M" and pref_match': "preferred A a ⊆ match A ` M"
and a: "a < n ∧ a ∉ M" and final: "A ! a + 1 = n"
shows "insert a M = {<n}"
proof -
  let ?B = "preferred A a"
  have "(!) (P ! a) ` {<n} = {<n}" by (metis P_set a map_nth set_map set_upt)
  hence "inj_on ((!) (P ! a)) {<n}" by(simp add: eq_card_imp_inj_on)
  hence "inj_on ((!) (P ! a)) {<A!a}" using final by(simp add: subset_inj_on)
  hence 1: "Suc(card ?B) = n" using final by (simp add: card_image)
  have 2: "card ?B ≤ card M"
    by(rule surj_card_le[OF subset_eq_atLeast0_lessThan_finite[OF M] pref_match'])
  have 3: "card M < n" using M a
    by (metis atLeast0LessThan card_seteq order.refl finite_atLeastLessThan le_neq_implies_less lessThan_iff subset_eq_atLeast0_lessThan_card)
  have "Suc (card M) = n" using 1 2 3 by simp
  thus ?thesis using M a by (simp add: card_subset_eq finite_subset)
qed

lemma more_choices:
assumes A: "wf A" and M: "M ⊆ {<n}" "M ≠ {<n}"
and pref_match': "preferred A a ⊆ match A ` M"
and "a < n" and matched: "match A a ∈ match A ` M"
shows "A ! a + 1 < n"
proof (rule ccontr)
  assume "¬ A ! a + 1 < n"
  hence "A ! a + 1 = n" using A ‹a < n› unfolding matching_def
    by (metis add.commute wf_less_n linorder_neqE_nat not_less_eq plus_1_eq_Suc)
  hence *: "nth (P ! a) ` {<n} ⊆ match A ` M"
    using pref_match' matched less_Suc_eq match_def by fastforce
  have "nth (P!a) ` {<n} = {<n}"
    using P_set[OF  ‹a < n›] by (metis map_nth set_map set_upt)
  hence "{<n} ⊆ match A ` M" using * by metis
  hence "card {<n} ≤ card M"
    using finite_subset[OF ‹M ⊆ {<n}› finite_atLeastLessThan] by (metis surj_card_le)
  then show False using M card_seteq by blast
qed

corollary more_choices_matched:
assumes "wf A" "M ⊆ {<n}" "M ≠ {<n}"
and "preferred A a ⊆ match A ` M" and "a ∈ M"
shows "A ! a + 1 < n"
using more_choices[OF assms(1-4)] ‹a ∈ M› ‹M ⊆ {<n}› atLeastLessThan_iff by blast

lemma atmost1_final: assumes M: "M ⊆ {<n}" and inj: "inj_on (match A) M"
and "∀a<n. preferred A a ⊆ match A ` M"
shows "∃⇩≤⇩1 a. a < n ∧ a ∉ M ∧ A ! a + 1 = n"
apply rule
subgoal for x y
using final_last[OF M inj, of x] final_last[OF M inj, of y] assms(3) by blast
done

lemma sumA_UB:
assumes "matching A M" "M ⊆ {<n}" "M ≠ {<n}" "∀a<n. preferred A a ⊆ match A ` M"
shows "(∑a<n. A!a) ≤ (n-1)^2"
proof -
  have "wf A" using assms(1) by(simp)
  have M: "∀a∈M. A!a + 1 < n" using more_choices_matched[OF ‹wf A› assms(2-3)] assms(4)
    ‹M ⊆ {<n}› atLeastLessThan_iff by blast
  note Ainj = conj12[OF assms(1)[unfolded matching_def]]
  show ?thesis
  proof (cases "∃a'<n. a' ∉ M ∧ A!a' + 1 = n")
    case True
    then obtain a' where a': "a'<n" "a' ∉ M" "A!a' + 1 = n" using ‹M ⊆ {<n}› ‹M ≠ {<n}› by blast
    hence "∀a<n. a ≠ a' ⟶ A!a ≤ n-2"
      using Uniq_D[OF atmost1_final[OF assms(2) Ainj(2) assms(4)], of a'] M wf_le_n1[OF Ainj(1)]
      by (metis Suc_1 Suc_eq_plus1 add_diff_cancel_right' add_le_imp_le_diff diff_diff_left less_eq_Suc_le order_less_le)
    from sumA_ub2[OF a'(1) _ this] a'(3) show ?thesis unfolding power2_eq_square by linarith
  next
    case False
    hence "∀a'<n. a' ∉ M ⟶ A ! a' + 1 < n"
      by (metis Suc_eq_plus1 Suc_lessI wf_less_n[OF Ainj(1)])
    with M have "∀a<n. A ! a + 1 < n" by blast
    hence "(∑a<n. A!a) ≤ n*(n-2)" using sum_bounded_above[of "{..<n}" "((!) A)" "n-2"] by fastforce
    also have "… ≤ (n-1)*(n-1)" by(simp add: algebra_simps)
    finally show ?thesis unfolding power2_eq_square .
  qed
qed

lemma var_ub:
assumes "matching A M" "M ⊆ {<n}" "M ≠ {<n}" "∀a<n. preferred A a ⊆ match A ` M"
shows "(∑a<n. A!a) + card M  < n^2 - n + 1"
proof -
  have 1: "M ⊂ {<n}" using assms(2,3) by auto
  have 2: "card M < n" using psubset_card_mono[OF _ 1] by simp
  have 3: "sum ((!) A) {..<n} ≤ n^2 + 1 - 2*n"
    using sumA_UB[OF assms(1-4)]  by (simp add: power2_eq_square algebra_simps)
  have 4: "2*n ≤ Suc (n^2)" using le_square[of n] unfolding power2_eq_square
    by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_SucI mult_2 mult_le_mono1 not_less_eq_eq plus_1_eq_Suc)
  show "(∑a<n. A!a) + card M  < n^2 - n + 1" using 2 3 4 by linarith
qed

lemma var_match:
assumes "matching A M" "M ⊆ {<n}" "M ≠ {<n}" "∀a<n. preferred A a ⊆ match A ` M" "a ∉ M"
shows "var A (M ∪ {a}) < var A M"
proof -
  have 2: "M ⊂ {<n}" using assms(2,3) by auto
  have 3: "card M < n" using psubset_card_mono[OF _ 2] by simp
  have 4: "sum ((!) A) {..<n} ≤ n^2 + 1 - 2*n"
    using sumA_UB[OF assms(1-4)]  by (simp add: power2_eq_square algebra_simps)
  have 5: "2*n ≤ Suc (n^2)" using le_square[of n] unfolding power2_eq_square
    by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_SucI mult_2 mult_le_mono1 not_less_eq_eq plus_1_eq_Suc)
  have 6: "(∑a<n. A!a) + card M  < n^2 + 1 - n" using 3 4 5 by linarith
  from var_ub[OF assms(1-4)] show ?thesis using ‹a ∉ M› finite_subset[OF assms(2)] by(simp)
qed

lemma var_next:
assumes"matching A M" "M ⊆ {<n}" "M ≠ {<n}" "∀a<n. preferred A a ⊆ match A ` M"
 "a < n"
shows "var (A[a := A ! a + 1]) M < var A M"
proof -
  have "var (A[a := A ! a + 1]) M = n*n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M)"
    using assms(1,5) by(simp add: power2_eq_square nth_list_update sum.If_cases lessThan_atLeast0 flip:Diff_eq)
  also have "… = n^2 - n + 1 - (1 + (∑a<n. A!a) + card M)"
    using sum.insert_remove[of "{<n}" "nth A" a,simplified,symmetric] assms(5)
    by (simp add:insert_absorb lessThan_atLeast0 power2_eq_square)
  also have "… < n^2 - n + 1 - ((∑a<n. A!a) + card M)" using var_ub[OF assms(1-4)] unfolding power2_eq_square
    by linarith
  finally show ?thesis unfolding var_def .
qed


subsection ‹Auxiliary Predicates›

text ‹The following two predicates express the same property:
if ‹a› prefers ‹b› over ‹a›'s current match,
then ‹b› is matched with an ‹a'› that ‹b› prefers to ‹a›.›

definition pref_match where
"pref_match A M = (∀a<n. ∀b<n. P!a ⊢ b < match A a ⟶ (∃a'∈M. b = match A a' ∧ Q ! b ⊢ a' < a))"

definition pref_match' where
"pref_match' A M = (∀a<n. ∀b ∈ preferred A a. ∃a'∈M. b = match A a' ∧ Q ! b ⊢ a' < a)"

lemma pref_match'_iff: "wf A ⟹ pref_match' A M = pref_match A M"
apply (auto simp add: pref_match'_def pref_match_def imp_ex prefers_def match_def)
  apply (smt (verit) P_set atLeast0LessThan order.strict_trans index_first lessThan_iff linorder_neqE_nat nth_index)
  by (smt (verit, best) P_set atLeast0LessThan card_atLeastLessThan card_distinct diff_zero in_mono index_nth_id lessThan_iff less_trans nth_mem)

definition optiA where
"optiA A = (∄A'. matching A' {<n} ∧ stable A' {<n} ∧
                (∃a<n. P ! a ⊢ match A' a < match A a))"

definition pessiB where
"pessiB A = (∄A'. matching A' {<n} ∧ stable A' {<n} ∧
                 (∃a<n. ∃a'<n. match A a = match A' a' ∧ Q ! match A a ⊢ a < a'))"

lemma optiA_pessiB: assumes "optiA A" shows "pessiB A"
unfolding pessiB_def
proof (safe, goal_cases)
  case (1 A' a a')
  have "¬ P!a ⊢  match A a <  match A' a" using 1
    by (metis atLeast0LessThan lessThan_iff stable_def)
  with 1 ‹optiA A› show ?case using P_set match_less_n optiA_def prefers_def unfolding matching_def
    by (metis (no_types) atLeast0LessThan inj_on_contraD lessThan_iff less_not_refl linorder_neqE_nat nth_index)
qed

lemma optiA_inv:
assumes A: "wf A" and a: "a < n" and a': "a' < n" and same_match: "match A a' = match A a"
and pref: "Q ! match A a' ⊢ a' < a" and "optiA A"
shows "optiA (A[a := A ! a + 1])"
proof (unfold optiA_def matching_def, rule notI, elim exE conjE)
  note optiA = ‹optiA A›[unfolded optiA_def matching_def]
  let ?A = "A[a := A ! a + 1]"
  fix A' a''
  assume "a'' < n" and A': "length A' = n" "set A' ⊆ {<n}" "stable A' {<n}" "inj_on (match A') {<n}"
  and pref_a'': "P ! a'' ⊢ match A' a'' < match ?A a''"
  show False
  proof cases
    assume [simp]: "a'' = a"
    have "A!a < n" using A a by(simp add: subset_eq)
    with A A' a pref_a'' have "P ! a ⊢ match A' a < match A a ∨ match A' a = match A a"
      apply(auto simp: prefers_def match_def)
      by (smt (verit) P_set wf_less_n card_atLeastLessThan card_distinct diff_zero index_nth_id
              not_less_eq not_less_less_Suc_eq)
    thus False
    proof
      assume "P ! a ⊢ match A' a < match A a " thus False using optiA A' ‹a < n› by(fastforce) 
    next
      assume "match A' a = match A a"
      have "a ≠ a'" using pref a' by(auto simp: prefers_def)
      hence "P ! a' ⊢ match A' a < match A' a' ∧ Q ! match A' a ⊢ a' < a" using optiA pref A' same_match ‹match A' a = match A a› a a'
        by (metis P_set atLeast0LessThan match_less_n inj_onD lessThan_iff linorder_neqE_nat nth_index prefers_def)
      thus False using a a' ‹a ≠ a'› A'(3) by (metis stable_def atLeastLessThan_iff zero_le)
    qed
  next
    assume "a'' ≠ a" thus False using optiA A' pref_a'' ‹a'' < n› by(metis match_def nth_list_update_neq)
  qed
qed

lemma pref_match_stable:
  "⟦ matching A {<n}; pref_match A {<n} ⟧ ⟹ stable A {<n}"
unfolding pref_match_def stable_def matching_def
by (metis atLeast0LessThan match_less_n inj_onD lessThan_iff prefers_asym)


subsection ‹Algorithm 1›

definition invAM where
[simp]: "invAM A M = (matching A M ∧ M ⊆ {<n} ∧ pref_match A M ∧ optiA A)"

lemma invAM_match:
  "⟦ invAM A M;  a < n ∧ a ∉ M;  match A a ∉ match A ` M ⟧ ⟹ invAM A (M ∪ {a})"
by(simp add: pref_match_def)

lemma invAM_swap:
assumes "invAM A M"
assumes a: "a < n ∧ a ∉ M" and a': "a' ∈ M ∧ match A a' = match A a" and pref: "Q ! match A a' ⊢ a < a'"
shows "invAM (A[a' := A!a'+1]) (M - {a'} ∪ {a})"
proof -
  have A: "wf A" and M : "M ⊆ {<n}" and inj: "inj_on (match A) M" and pref_match: "pref_match A M"
  and "optiA A" by(insert ‹invAM A M›) (auto)
  have "M ≠ {<n}" "a' < n" "a ≠ a'" using a' a M by auto
  have pref_match': "pref_match' A M" using pref_match pref_match'_iff[OF A] by blast
  let ?A = "A[a' := A!a'+1]" let ?M = "M - {a'} ∪ {a}"
  have neq_a': "∀x. x ∈ ?M ⟶ a' ≠ x" using ‹a ≠ a'› by blast
  have ‹set ?A ⊆ {<n}›
    apply(rule set_update_subsetI[OF A[THEN conjunct2]])
    using more_choices[OF _ M ‹M ≠ {<n}›] A inj pref_match' a' subsetD[OF M, of a']
    by(fastforce simp: pref_match'_def)
  hence "wf ?A" using A by(simp)
  moreover have "inj_on (match ?A) ?M" using a a' inj
    by(simp add: match_def inj_on_def)(metis Diff_iff insert_iff nth_list_update_neq)
  moreover have "pref_match' ?A ?M" using a a' pref_match' A pref ‹a' < n›
    apply(simp add: pref_match'_def match_upd_neq neq_a' Ball_def Bex_def image_iff imp_ex nth_list_update less_Suc_eq
            flip: match_def)
    by (metis prefers_trans)
  moreover have "optiA ?A" using optiA_inv[OF A ‹a' < n› _ _ _ ‹optiA A›] a a'[THEN conjunct2] pref by auto
  ultimately show ?thesis using a a' M pref_match'_iff by auto
qed

(* TODO: could also be used in invAM_next *)
lemma preferred_subset_match_if_invAM:
assumes "invAM A M"
shows "∀a<n. preferred A a ⊆ match A ` M" (is ?P)
proof -
  have A: "wf A" and pref_match: "pref_match A M" using assms(1) by auto
  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
  thus pref_match1: "∀a<n. preferred A a ⊆ match A ` M" unfolding pref_match'_def by blast
qed

lemma invAM_next:
assumes "invAM A M"
assumes a: "a < n ∧ a ∉ M" and a': "a' ∈ M ∧ match A a' = match A a" and pref: "¬ Q ! match A a' ⊢ a < a'"
shows "invAM (A[a := A!a + 1]) M"
proof -
  have A: "wf A" and M : "M ⊆ {<n}" and inj: "inj_on (match A) M" and pref_match: "pref_match A M"
  and optiA: "optiA A" and "a' < n"
    by(insert ‹invAM A M› a') (auto)
  hence pref': "Q ! match A a' ⊢ a' < a"
    using pref a a' Q_set unfolding prefers_def
    by (metis match_def match_less_n index_eq_index_conv linorder_less_linear subsetD)
  have "M ≠ {<n}" using a by fastforce
  have neq_a: "∀x. x∈ M ⟶ a ≠ x" using a by blast
  have pref_match': "pref_match' A M" using pref_match pref_match'_iff[OF A,of M] by blast
  hence "∀a<n. preferred A a ⊆ match A ` M" unfolding pref_match'_def by blast
  hence "A!a + 1 < n"
    using more_choices[OF _ M ‹M ≠ {<n}›] A inj a a' unfolding matching_def by (metis (no_types, lifting) imageI)
  let ?A = "A[a := A!a+1]"
  have "wf ?A" using A ‹A!a + 1 < n› by(simp add: set_update_subsetI)
  moreover have "inj_on (match ?A) M" using a inj
    by(simp add: match_def inj_on_def) (metis nth_list_update_neq)
  moreover have "pref_match' ?A M" using a pref_match' pref' A a' neq_a
    by(auto simp: match_upd_neq pref_match'_def Ball_def Bex_def image_iff nth_list_update imp_ex less_Suc_eq
            simp flip: match_def)
  moreover have  "optiA ?A" using optiA_inv[OF A conjunct1[OF a] ‹a' < n› conjunct2[OF a'] pref' optiA] .
  ultimately show ?thesis using M by (simp add: pref_match'_iff)
qed


lemma Gale_Shapley1: "VARS M A a a' b
 [M = {} ∧ A = replicate n 0]
 WHILE M ≠ {<n}
 INV { invAM A M }
 VAR {var A M}
 DO a := (SOME a. a < n ∧ a ∉ M); b := match A a;
  IF b ∉ match A ` M
  THEN M := M ∪ {a}
  ELSE a' := (SOME a'. a' ∈ M ∧ match A a' = b);
       IF Q ! match A a' ⊢ a < a'
       THEN A[a'] := A!a'+1; M := M - {a'} ∪ {a}
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
   by(auto simp: stable_def optiA_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def)
next
  case 3 thus ?case using pref_match_stable by auto
next
  case (2 v M A a)
  hence invAM: "invAM A M" and m: "matching A M" and M: "M ⊆ {<n}" "M ≠ {<n}" and "optiA A"
    and v: "var A M = v" by auto
  note Ainj = conj12[OF m[unfolded matching_def]]
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  define a where "a = (SOME a. a < n ∧ a ∉ M)"
  have a: "a < n ∧ a ∉ M" unfolding a_def using M
    by (metis (no_types, lifting) atLeastLessThan_iff someI_ex subsetI subset_antisym)
  show ?case (is "?P((SOME a. a < n ∧ a ∉ M))") unfolding a_def[symmetric]
  proof -
    show "?P a" (is "(?not_matched ⟶ ?THEN) ∧ (¬ ?not_matched ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?not_matched
      show ?THEN
      proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases)
        case 1 show ?case using invAM_match[OF invAM a ‹?not_matched›] .

        case 2 show ?case
          using var_match[OF m M pref_match1] var0_match[OF Ainj(1) M(1)] a unfolding v by blast
      qed
    next
      assume matched: "¬ ?not_matched"
      define a' where "a' = (SOME a'.  a' ∈ M ∧ match A a' = match A a)"
      have a': "a' ∈ M ∧ match A a' = match A a" unfolding a'_def using matched
        by (smt (verit) image_iff someI_ex)
      hence "a' < n" "a ≠ a'" using a M atLeast0LessThan by auto
      show ?ELSE (is "?P((SOME a'. a' ∈ M ∧ match A a' = match A a))") unfolding a'_def[symmetric]
      proof -
        show "?P a'" (is "(?pref ⟶ ?THEN) ∧ (¬ ?pref ⟶ ?ELSE)")
        proof (rule; rule)
          assume ?pref
          show ?THEN
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            case 1 show ?case by(rule invAM_swap[OF invAM a a' ‹?pref›])

            case 2
            have "card(M - {a'} ∪ {a}) = card M"
              using a a' card.remove subset_eq_atLeast0_lessThan_finite[OF M(1)] by fastforce
            thus ?case using v var_next[OF m M pref_match1 ‹a' < n›] var0_next[OF Ainj(1) M ‹a' < n›]
              by simp
          qed
        next
          assume "¬ ?pref"
          show ?ELSE
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            case 1 show ?case using invAM_next[OF invAM a a' ‹¬ ?pref›] .

            case 2
            show ?case using a v var_next[OF m M pref_match1, of a] var0_next[OF Ainj(1) M, of a]
              by simp
          qed
        qed
      qed
    qed
  qed
qed

text ‹Proof also works for @{const var0} instead of @{const var}.›


subsection ‹Algorithm 2: List of unmatched As›

abbreviation invas where
"invas as == (set as ⊆ {<n} ∧ distinct as)"

lemma Gale_Shapley2: "VARS A a a' as b
 [as = [0..<n] ∧ A = replicate n 0]
 WHILE as ≠ []
 INV { invAM A ({<n} - set as) ∧ invas as}
 VAR {var A ({<n} - set as)}
 DO a := hd as; b := match A a;
  IF b ∉ match A ` ({<n} - set as)
  THEN as := tl as
  ELSE a' := (SOME a'. a' ∈ {<n} - set as ∧ match A a' = b);
       IF Q ! match A a' ⊢ a < a'
       THEN A[a'] := A!a'+1; as := a' # tl as
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
   by(auto simp: stable_def optiA_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def)
next
  case 3 thus ?case using pref_match_stable by auto
next
  case (2 v A _ a' as)
  let ?M = "{<n} - set as"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and "as ≠ []" and as: "invas as" and v: "var A ?M = v" using 2 by auto
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  from ‹as ≠ []› obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv)
  have set_as: "?M ∪ {a} = {<n} - set as'" using as aseq by force
  have a: "a < n ∧ a ∉ ?M" using as unfolding aseq by (simp)
  show ?case
  proof (simp only: aseq list.sel, goal_cases)
    case 1 show ?case (is "(?not_matched ⟶ ?THEN) ∧ (¬ ?not_matched ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?not_matched
      then have nm: "match A a ∉ match A ` ?M" unfolding aseq .
      show ?THEN
      proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases)
        case 1 show ?case using invAM_match[OF invAM a nm] as unfolding set_as by (simp add: aseq)
        case 2 show ?case
          using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan
          unfolding set_as v by blast 
      qed
    next
      assume matched: "¬ ?not_matched"
      define a' where "a' = (SOME a'.  a' ∈ ?M ∧ match A a' = match A a)"
      have a': "a' ∈ ?M ∧ match A a' = match A a" unfolding a'_def aseq using matched
        by (smt (verit) image_iff someI_ex)
      hence "a' < n" "a ≠ a'" using a M atLeast0LessThan by auto
      show ?ELSE unfolding aseq[symmetric] a'_def[symmetric]
      proof (goal_cases)
        case 1
        show ?case (is "(?pref ⟶ ?THEN) ∧ (¬ ?pref ⟶ ?ELSE)")
        proof (rule; rule)
          assume ?pref
          show ?THEN
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            have *: "{<n} - set as - {a'} ∪ {a} = {<n} - set (a' # as')" using a a' as aseq by auto
            case 1 show ?case using invAM_swap[OF invAM a a' ‹?pref›] unfolding *
              using a' as aseq by force
            case 2
            have "card({<n} - set as) = card({<n} - set (a' # as'))" using a a' as aseq by auto
            thus ?case using v var_next[OF m M _ pref_match1, of a'] ‹a' < n› a atLeast0LessThan
              by (metis Suc_eq_plus1 lessThan_iff var_def)
          qed
        next
          assume "¬ ?pref"
          show ?ELSE
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            case 1 show ?case using invAM_next[OF ‹invAM A ?M› a a' ‹¬ ?pref›] as by blast

            case 2
            show ?case using a v var_next[OF m M _ pref_match1, of a]
              by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) 
          qed
        qed
      qed
    qed
  qed
qed


subsection ‹Algorithm 3: Record matching of Bs to As›

abbreviation invAB :: "nat list ⇒ (nat ⇒ nat option) ⇒ nat set ⇒ bool" where
"invAB A B M == (ran B = M ∧ (∀b a. B b = Some a ⟶ match A a = b))"

lemma invAB_swap:
assumes invAB: "invAB A B M"
assumes a: "a < n ∧ a ∉ M" and a': "a' ∈ M ∧ match A a' = match A a"
  and "inj_on B (dom B)" "B(match A a) = Some a'"
shows "invAB (A[a' := A!a'+1]) (B(match A a := Some a)) (M - {a'} ∪ {a})"
proof -
  have "∀b x. b ≠ match A a ⟶ B b = Some x ⟶ a'≠ x" using invAB a' by blast
  moreover have "a ≠ a'" using a a' by auto 
  ultimately show ?thesis using assms by(simp add: ran_map_upd_Some match_def)
qed


lemma Gale_Shapley3: "VARS A B a a' as b
 [as = [0..<n] ∧ A = replicate n 0 ∧ B = (λ_. None)]
 WHILE as ≠ []
 INV { invAM A ({<n} - set as) ∧ invAB A B ({<n} - set as) ∧ invas as}
 VAR {var A ({<n} - set as)}
 DO a := hd as; b := match A a;
  IF B b = None
  THEN B := B(b := Some a); as := tl as
  ELSE a' := the(B b);
       IF Q ! match A a' ⊢ a < a'
       THEN B := B(b := Some a); A[a'] := A!a'+1; as := a' # tl as
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
    by(auto simp: stable_def optiA_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def)
next
  case 3 thus ?case using pref_match_stable by auto
next
  case (2 v A B _ a' as)
  let ?M = "{<n} - set as"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and "as ≠ []" and as: "invas as" and invAB: "invAB A B ?M" and v: "var A ?M = v"
    using 2 by auto
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  from ‹as ≠ []› obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv)
  have set_as: "?M ∪ {a} = {<n} - set as'" using as aseq by force
  have a: "a < n ∧ a ∉ ?M" using as unfolding aseq by (simp)
  show ?case
  proof (simp only: aseq list.sel, goal_cases)
    case 1 show ?case (is "(?not_matched ⟶ ?THEN) ∧ (¬ ?not_matched ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?not_matched
      then have nm: "match A a ∉ match A ` ?M" using invAB unfolding aseq ran_def
        apply (clarsimp simp: set_eq_iff) using not_None_eq by blast
      show ?THEN
      proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases)
        have invAM': "invAM A ({<n} - set as')"
          using invAM_match[OF invAM a nm] unfolding set_as[symmetric] by simp
        have invAB': "invAB A (B(match A a := Some a)) ({<n} - set as')"
          using invAB ‹?not_matched› set_as by (simp)
        case 1 show ?case using invAM' as invAB' unfolding set_as aseq
          by (metis distinct.simps(2) insert_subset list.simps(15))
        case 2 show ?case
          using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan
          unfolding set_as v by blast 
      qed
    next
      assume matched: "¬ ?not_matched"
      then obtain a' where a'eq: "B(match A a) = Some a'" by auto
      have a': "a' ∈ ?M ∧ match A a' = match A a" unfolding aseq using a'eq invAB
        by (metis ranI aseq)
      hence "a' < n" "a ≠ a'" using a M atLeast0LessThan by auto
      show ?ELSE unfolding aseq[symmetric] a'eq option.sel
      proof (goal_cases)
        have inj_dom: "inj_on B (dom B)" by (metis (mono_tags) domD inj_onI invAB)
        case 1
        show ?case (is "(?pref ⟶ ?THEN) ∧ (¬ ?pref ⟶ ?ELSE)")
        proof (rule; rule)
          assume ?pref
          show ?THEN
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            have *: "{<n} - set as - {a'} ∪ {a} = {<n} - set (a' # as')" using a a' as aseq by auto
            have a'neq: "∀b x. b ≠ match A a ⟶ B b = Some x ⟶ a'≠ x"
              using invAB a' by blast
            have invAB': "invAB (A[a' := A ! a' + 1]) (B(match A a := Some a)) ({<n} - insert a' (set as'))"
              using invAB_swap[OF invAB a a' inj_dom a'eq] * by simp
            case 1 show ?case using invAM_swap[OF invAM a a' ‹?pref›] invAB' unfolding *
              using a' as aseq by simp
            case 2
            have "card({<n} - set as) = card({<n} - set (a' # as'))" using a a' as aseq by auto
            thus ?case using v var_next[OF m M _ pref_match1, of a'] ‹a' < n› a atLeast0LessThan
              by (metis Suc_eq_plus1 lessThan_iff var_def)
          qed
        next
          assume "¬ ?pref"
          show ?ELSE
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            case 1
            have "invAB (A[a := A ! a + 1]) B ?M" using invAB a
              by (metis match_def nth_list_update_neq ranI)
            thus ?case using invAM_next[OF invAM a a' ‹¬ ?pref›] as by blast
            case 2
            show ?case using a v var_next[OF m M _ pref_match1, of a]
              by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) 
          qed
        qed
      qed
    qed
  qed
qed


subsection ‹Unused data refinement step›

(* begin unused: directly implement function B via lists B and M (data refinement);
   also done in Alg. 4 in a more principled manner *)

abbreviation invAB' :: "nat list ⇒ nat list ⇒ bool list ⇒ nat set ⇒ bool" where
"invAB' A B M M' == (length B = n ∧ length M = n ∧ M' = nth B ` {b. b < n ∧ M!b}
 ∧ (∀b<n. M!b ⟶ B!b < n ∧ match A (B!b) = b))"

lemma Gale_Shapley4_unused: "VARS A B M a a' as b
 [as = [0..<n] ∧ A = replicate n 0 ∧ B = replicate n 0 ∧ M = replicate n False]
 WHILE as ≠ []
 INV { invAM A ({<n} - set as) ∧ invAB' A B M ({<n} - set as) ∧ invas as}
 VAR {var A ({<n} - set as)}
 DO a := hd as; b := match A a;
  IF ¬ (M ! b)
  THEN M[b] := True; B[b] := a; as := tl as
  ELSE a' := B ! b;
       IF Q ! match A a' ⊢ a < a'
       THEN B[b] := a; A[a'] := A!a'+1; as := a' # tl as
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [wf A ∧ inj_on (match A) {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
   by(auto simp: stable_def optiA_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def)
next
  case 3 thus ?case using pref_match_stable by auto
next
  case (2 v A B M _ a' as)
  let ?M = "{<n} - set as"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and notall: "as ≠ []" and as: "invas as" and invAB: "invAB' A B M ?M" and v: "var A ?M = v"
    using 2 by auto
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  from notall obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv)
  have set_as: "?M ∪ {a} = {<n} - set as'" using as aseq by force
  have a: "a < n ∧ a ∉ ?M" using as unfolding aseq by (simp)
  show ?case
  proof (simp only: aseq list.sel, goal_cases)
    case 1 show ?case (is "(?not_matched ⟶ ?THEN) ∧ (¬ ?not_matched ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?not_matched
      then have nm: "match A a ∉ match A ` ?M" using invAB set_as unfolding aseq by force
      show ?THEN
      proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases)
        have invAM': "invAM A ({<n} - set as')"
          using invAM_match[OF invAM a nm] unfolding set_as[symmetric] by simp
        then have invAB': "invAB' A (B[match A a := a]) (M[match A a := True]) ({<n} - set as')"
          using invAB ‹?not_matched› set_as match_less_n[OF A] a
          by (auto simp add: image_def nth_list_update)
        case 1 show ?case using invAM' invAB as invAB' unfolding set_as aseq
          by (metis distinct.simps(2) insert_subset list.simps(15))
        case 2 show ?case
          using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan
          unfolding set_as v by blast 
      qed
    next
      assume matched: "¬ ?not_matched"
      hence "match A a ∈ match A ` ({<n} - insert a (set as'))" using  match_less_n[OF A] a invAB
        apply(auto) by (metis (lifting) image_eqI list.simps(15) mem_Collect_eq aseq)
      hence "Suc(A!a) < n" using more_choices[OF A M, of a] a pref_match1
        using aseq atLeast0LessThan by auto
      let ?a = "B ! match A a"
      have a': "?a ∈ ?M ∧ match A ?a = match A a"
        using invAB match_less_n[OF A] matched a by blast
      hence "?a < n" "a ≠ ?a" using a by auto
      show ?ELSE unfolding aseq option.sel
      proof (goal_cases)
        case 1
        show ?case (is "(?pref ⟶ ?THEN) ∧ (¬ ?pref ⟶ ?ELSE)")
        proof (rule; rule)
          assume ?pref
          show ?THEN
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            have *: "{<n} - set as - {?a} ∪ {a} = {<n} - set (?a # as')" using a a' as aseq by auto
            have a'neq: "∀b<n. b ≠ match A a ⟶ M!b ⟶ ?a ≠ B!b"
              using invAB a' by metis
            have invAB': "invAB' (A[?a := A ! ?a + 1]) (B[match A a := a]) M ({<n} - set (?a#as'))"
              using invAB aseq * ‹a ≠ ?a› a' match_less_n[OF A, of a] a
              apply (simp add: nth_list_update)
              apply rule
               apply(auto simp add:  image_def)[]
              apply (clarsimp simp add: match_def)
              apply (metis (opaque_lifting) nth_list_update_neq)
              done
            case 1 show ?case using invAM_swap[OF invAM a a' ‹?pref›] invAB' unfolding *
              using a' as aseq by (auto)
            case 2
            have "card({<n} - set as) = card({<n} - set (?a # as'))" using a a' as aseq by simp
            thus ?case using v var_next[OF m M _ pref_match1, of ?a] ‹?a < n› a atLeast0LessThan
              by (metis Suc_eq_plus1 lessThan_iff var_def)
          qed
        next
          assume "¬ ?pref"
          show ?ELSE
          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
            case 1
            have "invAB' (A[a := A ! a + 1]) B M ({<n} - set as)" using invAB a ‹a ≠ ?a›
              by (metis match_def nth_list_update_neq)
            thus ?case using invAM_next[OF invAM a a' ‹¬ ?pref›] as aseq by fastforce
            case 2
            show ?case using a v var_next[OF m M _ pref_match1, of a] aseq
              by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) 
          qed
        qed
      qed
    qed
  qed
qed


subsection ‹Algorithm 4: remove list of unmatched As›

subsubsection ‹An initial version›

text ‹The inner variant appears intuitive but complicates the derivation of an overall complexity bound
because the inner variant also depends on a variable that is modified by the outer loop.›

lemma Gale_Shapley4:
"VARS A B ai a a'
 [ai = 0 ∧ A = replicate n 0 ∧ B = (λ_. None)]
 WHILE ai < n
 INV { invAM A {<ai} ∧ invAB A B {<ai} ∧ ai ≤ n }
 VAR {z = n - ai}
 DO a := ai;
  WHILE B (match A a) ≠ None
  INV { invAM A ({<ai+1} - {a}) ∧ invAB A B ({<ai+1} - {a}) ∧ (a ≤ ai ∧ ai < n) ∧ z = n-ai }
  VAR {var A {<ai}}
  DO a' := the(B (match A a));
     IF Q ! match A a' ⊢ a < a'
     THEN B := B(match A a := Some a); A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI
  OD;
  B := B(match A a := Some a); ai := ai+1
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case  (* outer invar holds initially *)
   by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def)[]
next
  case 2 (* outer invar and b implies inner invar *)
  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
  case (4 z A B ai a) (* inner invar' and not b implies outer invar *)
  note inv = 4[THEN conjunct1]
  note invAM = inv[THEN conjunct1]
  note aai = inv[THEN conjunct2,THEN conjunct2]
  show ?case
  proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
    case 1
    have *: "{<Suc ai} = insert a ({<Suc ai} - {a})" using aai by (simp add: insert_absorb)
    have **: "inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) ∧ match A a ∉ match A ` ({<Suc ai} - {a}))"
      by (metis "*" Diff_idemp inj_on_insert)
    have nm: "match A a ∉ match A ` ({<Suc ai} - {a})" using 4 unfolding ran_def
        apply (clarsimp simp: set_eq_iff) by (metis not_None_eq)
    have invAM': "invAM A {<ai+1}"
      using invAM_match[OF invAM, of a] aai nm by (simp add: ** insert_absorb)
    show ?case using 4 invAM' by (simp add: insert_absorb)
  next
    case 2 thus ?case using 4 by auto
  qed
next
  case 5 (* outer invar and not b implies post *)
  thus ?case using pref_match_stable unfolding invAM_def by (metis le_neq_implies_less)
next
  case (3 z v A B ai a a') (* preservation of inner invar *)
  let ?M = "{<ai+1} - {a}"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and matched: "B(match A a) ≠ None" and as: "a ≤ ai ∧ ai < n" and invAB: "invAB A B ?M"
    and v: "var A ?M = v" using 3 by auto
  note invar = 3[THEN conjunct1,THEN conjunct1]
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  from matched obtain a' where a'eq: "B(match A a) = Some a'" by auto
  have a': "a' ∈ ?M ∧ match A a' = match A a" using a'eq invAB by (metis ranI)
  have a: "a < n ∧ a ∉ ?M" using invar by auto
  have "?M ≠ {<n}" and "a' < n" using M a a' atLeast0LessThan by auto
  have card: "card {<ai} = card ?M" using as by simp
  show ?case unfolding a'eq option.sel
  proof (goal_cases)
    case 1
    show ?case (is "(?unstab ⟶ ?THEN) ∧ (¬ ?unstab ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?unstab
      have *: "{<ai + 1} - {a} - {a'} ∪ {a} = {<ai + 1} - {a'}" using invar a' by auto
      show ?THEN
      proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
        have inj_dom: "inj_on B (dom B)" by (metis (mono_tags) domD inj_onI invAB)
        have invAB': "invAB (A[a' := A ! a' + 1]) (B(match A a ↦ a)) ({<ai + 1} - {a'})"
          using invAB_swap[OF invAB a a' inj_dom a'eq] * by simp
        case 1 show ?case
          using invAM_swap[OF invAM a a' ‹?unstab›] invAB' invar a' unfolding * by (simp)
      next
        case 2
        show ?case using v var_next[OF m M ‹?M ≠ {<n}› pref_match1 ‹a' < n›] card
          by (metis var_def Suc_eq_plus1 psubset_eq)
      qed
    next
      assume "¬ ?unstab"
      show ?ELSE
      proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
        have *: "∀b a'. B b = Some a' ⟶ a ≠ a'" by (metis invAB ranI a) 
        case 1 show ?case using invAM_next[OF invAM a a' ‹¬ ?unstab›] invar * by (simp add: match_def)
      next
        case 2
        show ?case using v var_next[OF m M ‹?M ≠ {<n}› pref_match1, of a] a card
          by (metis Suc_eq_plus1 var_def)
      qed
    qed
  qed
qed

subsubsection ‹A better inner variant›

text ‹This is the definitive version of Algorithm 4.
The inner variant is changed to support the easy derivation of the precise upper bound
of the number of executed actions.
This variant shows that the algorithm can at most execute @{term "n^2 - n + 1"}
basic actions (match, swap, next).›

definition var2 :: "nat list ⇒ nat" where
[simp]: "var2 A = (n-1)^2 - (∑a<n. A!a)"

text ‹Because ‹A› is not changed by the outer loop, the initial value of @{term "var2 A"},
which is @{term "(n-1)^2"}, is an upper bound of the number of iterations of the inner loop.
To this we need to add ‹n› because the outer loop executes additional ‹n› match actions
at the end of the loop body.
Thus at most @{prop "(n-1)^2 + n = n^2 - n + 1"} actions are executed, exactly as in the earlier algorithms.›

lemma var2_next:
assumes "invAM (A[a := A!a + 1]) M" "M ≠ {<n}" "a < n"
shows "var2 (A[a := A!a + 1]) < var2 A"
proof -
  let ?A = "A[a := A!a + 1]"
  have "wf ?A" using assms(1) by auto
  have 1: "(∑a<n. ?A!a) = (∑a<n. A!a) + 1"
  proof -
    have "(∑a<n. ?A!a) = 1 + (A ! a + sum ((!) A) ({<n} - {a}))"
      using ‹wf ?A› ‹a < n› by(simp add: nth_list_update sum.If_cases lessThan_atLeast0 flip:Diff_eq)
    also have "… = (∑a<n. A!a) + 1"
      using ‹a < n› member_le_sum[of a "{<n}" "nth A"] by(simp add: sum_diff1_nat lessThan_atLeast0)
    finally show ?thesis .
  qed
  have "(∑a<n. ?A!a) ≤ (n-1)^2"
    using sumA_UB[of ?A M] assms(1,2) by (meson invAM_def preferred_subset_match_if_invAM)
  with 1 show ?thesis unfolding var2_def by auto
qed

lemma Gale_Shapley4_var2:
"VARS A B ai a a'
 [ai = 0 ∧ A = replicate n 0 ∧ B = (λ_. None)]
 WHILE ai < n
 INV { invAM A {<ai} ∧ invAB A B {<ai} ∧ ai ≤ n }
 VAR {z = n - ai}
 DO a := ai;
  WHILE B (match A a) ≠ None
  INV { invAM A ({<ai+1} - {a}) ∧ invAB A B ({<ai+1} - {a}) ∧ (a ≤ ai ∧ ai < n) ∧ z = n-ai }
  VAR {var2 A}
  DO a' := the(B (match A a));
     IF Q ! match A a' ⊢ a < a'
     THEN B := B(match A a := Some a); A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI
  OD;
  B := B(match A a := Some a); ai := ai+1
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case  (* outer invar holds initially *)
   by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def)[]
next
  case 2 (* outer invar and b implies inner invar *)
  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
  case (4 z A B ai a) (* inner invar' and not b implies outer invar *)
  note inv = 4[THEN conjunct1]
  note invAM = inv[THEN conjunct1]
  note aai = inv[THEN conjunct2,THEN conjunct2]
  show ?case
  proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
    case 1
    have *: "{<Suc ai} = insert a ({<Suc ai} - {a})" using aai by (simp add: insert_absorb)
    have **: "inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) ∧ match A a ∉ match A ` ({<Suc ai} - {a}))"
      by (metis "*" Diff_idemp inj_on_insert)
    have nm: "match A a ∉ match A ` ({<Suc ai} - {a})" using 4 unfolding ran_def
        apply (clarsimp simp: set_eq_iff) by (metis not_None_eq)
    have invAM': "invAM A {<ai+1}"
      using invAM_match[OF invAM, of a] aai nm by (simp add: ** insert_absorb)
    show ?case using 4 invAM' by (simp add: insert_absorb)
  next
    case 2 thus ?case using 4 by auto
  qed
next
  case 5 (* outer invar and not b implies post *)
  thus ?case using pref_match_stable unfolding invAM_def by (metis le_neq_implies_less)
next
  case (3 z v A B ai a a') (* preservation of inner invar *)
  let ?M = "{<ai+1} - {a}"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and matched: "B(match A a) ≠ None" and as: "a ≤ ai ∧ ai < n" and invAB: "invAB A B ?M"
    and v: "var2 A = v" using 3 by auto
  note invar = 3[THEN conjunct1,THEN conjunct1]
  from matched obtain a' where a'eq: "B(match A a) = Some a'" by auto
  have a': "a' ∈ ?M ∧ match A a' = match A a" using a'eq invAB by (metis ranI)
  have a: "a < n ∧ a ∉ ?M" using invar by auto
  have "?M ≠ {<n}" and "a' < n" using M a a' atLeast0LessThan by auto
  show ?case unfolding a'eq option.sel
  proof (goal_cases)
    case 1
    show ?case (is "(?unstab ⟶ ?THEN) ∧ (¬ ?unstab ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?unstab
      have *: "{<ai + 1} - {a} - {a'} ∪ {a} = {<ai + 1} - {a'}" using invar a' by auto
      show ?THEN
      proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
        note invAM' = invAM_swap[OF invAM a a' ‹?unstab›]
        have inj_dom: "inj_on B (dom B)" by (metis (mono_tags) domD inj_onI invAB)
        have invAB': "invAB (A[a' := A ! a' + 1]) (B(match A a ↦ a)) ({<ai + 1} - {a'})"
          using invAB_swap[OF invAB a a' inj_dom a'eq] * by simp
        case 1 show ?case using invAM' invAB' invar a' unfolding * by (simp)
        case 2 show ?case using v var2_next[OF invAM'] ‹a' < n› * atLeast0LessThan by auto
      qed
    next
      assume "¬ ?unstab"
      show ?ELSE
      proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
        note invAM' = invAM_next[OF invAM a a' ‹¬ ?unstab›]
        have *: "∀b a'. B b = Some a' ⟶ a ≠ a'" by (metis invAB ranI a) 
        case 1 show ?case using invAM' invar * by (simp add: match_def)
        case 2 show ?case using v var2_next[OF invAM'] a ‹?M ≠ {<n}› by blast
      qed
    qed
  qed
qed


subsubsection ‹Algorithm 4.1: single-loop variant›

text ‹A bit of a relic because it is an instance of a general program transformation for
merging nested loops by an additional test inside the single loop.›

lemma Gale_Shapley4_1: "VARS A B a a' ai b
 [ai = 0 ∧ a = 0 ∧ A = replicate n 0 ∧ B = (λ_. None)]
 WHILE ai < n
 INV { invAM A ({<ai+1} - {a}) ∧ invAB A B ({<ai+1} - {a}) ∧ (a ≤ ai ∧ ai ≤ n) ∧ (ai=n ⟶ a=ai)}
 VAR {var A ({<ai+1} - {a})}
 DO b := match A a;
  IF B b = None
  THEN B := B(b := Some a); ai := ai + 1; a := ai
  ELSE a' := the(B b);
       IF Q ! match A a' ⊢ a < a'
       THEN B := B(b := Some a); A[a'] := A!a'+1; a := a'
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
    by(auto simp: stable_def optiA_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def)
next
  case 3 thus ?case using pref_match_stable
    using atLeast0_lessThan_Suc by force
next
  case (2 v A B a a' ai b)
  let ?M = "{<ai+1} - {a}"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and as: "a ≤ ai ∧ ai < n" and invAB: "invAB A B ?M" and v: "var A ?M = v" using 2 by auto
  note invar = 2[THEN conjunct1,THEN conjunct1]
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  have a: "a < n ∧ a ∉ ?M" using as by (simp)
  show ?case (is "(?not_matched ⟶ ?THEN) ∧ (¬ ?not_matched ⟶ ?ELSE)")
  proof (rule; rule)
    assume ?not_matched
    then have nm: "match A a ∉ match A ` ?M" using invAB unfolding ran_def
      apply (clarsimp simp: set_eq_iff) using not_None_eq by blast
    show ?THEN
    proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases)
      have *: "{<ai + 1 + 1} - {ai + 1} = {<ai + 1}" by auto
      have **: "{<ai + 1} - {a} ∪ {a} = {<ai + 1}" using as by auto
      hence invAM': "invAM A {<ai+1}"using invAM_match[OF invAM a nm] by simp
      have invAB': "invAB A (B(match A a := Some a)) {<ai+1}"
        using invAB ‹?not_matched› ** by (simp)
      case 1 show ?case using invAM' as invAB' * by presburger
      case 2 show ?case
        using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan * **
        unfolding v by (metis lessThan_iff)
    qed
  next
    assume matched: "¬ ?not_matched"
    then obtain a' where a'eq: "B(match A a) = Some a'" by auto
    have a': "a' ∈ ?M ∧ match A a' = match A a" using a'eq invAB by (metis ranI)
    hence "a' < n" "a ≠ a'" using a M atLeast0LessThan by auto
    show ?ELSE unfolding a'eq option.sel
    proof (goal_cases)
      have inj_dom: "inj_on B (dom B)" by (metis (mono_tags) domD inj_onI invAB)
      case 1
      show ?case (is "(?pref ⟶ ?THEN) ∧ (¬ ?pref ⟶ ?ELSE)")
      proof (rule; rule)
        assume ?pref
        show ?THEN
        proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
          have *: "{<ai + 1} - {a} - {a'} ∪ {a} = {<ai + 1} - {a'}" using a a' as by auto
          have a'neq: "∀b x. b ≠ match A a ⟶ B b = Some x ⟶ a'≠ x"
            using invAB a' by blast
          have invAB': "invAB (A[a' := A ! a' + 1]) (B(match A a := Some a)) ({<ai + 1} - {a'})"
            using invAB_swap[OF invAB a a' inj_dom a'eq] * by simp
          case 1 show ?case using invAM_swap[OF invAM a a' ‹?pref›] invAB' unfolding *
            using a' as by simp
          case 2
          have "card({<ai + 1} - {a'}) = card({<ai + 1} - {a})" using a a' as by auto
          thus ?case using v var_next[OF m M _ pref_match1, of a'] ‹a' < n› a atLeast0LessThan
            by (metis Suc_eq_plus1 lessThan_iff var_def)
        qed
      next
        assume "¬ ?pref"
        show ?ELSE
        proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
          case 1
          have "invAB (A[a := A ! a + 1]) B ?M" using invAB a
            by (metis match_def nth_list_update_neq ranI)
          thus ?case using invAM_next[OF invAM a a' ‹¬ ?pref›] using "2" by presburger
          case 2
          show ?case using a v var_next[OF m M _ pref_match1, of a]
            by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) 
        qed
      qed
    qed
  qed
qed


subsection ‹Algorithm 5: Data refinement of ‹B››

definition "α B N = (λb. if b < n ∧ N!b then Some(B!b) else None)"

lemma α_Some[simp]: "α B N b = Some a ⟷ b < n ∧ N!b ∧ a = B!b"
by(auto simp add: α_def)

lemma αupdate1: "⟦ ¬ N ! b; b < length B; b < length N; n = length N ⟧
 ⟹ ran(α (B[b := a]) (N[b := True])) = ran(α B N) ∪ {a}"
by(force simp add: α_def ran_def nth_list_update)

lemma αupdate2: "⟦ N!b; b < length B; b < length N; length N = n ⟧
 ⟹ α (B[b := a]) N = (α B N)(b := Some a)"
by(force simp add: α_def nth_list_update)


abbreviation invAB2 :: "nat list ⇒ nat list ⇒ bool list ⇒ nat set ⇒ bool" where
"invAB2 A B N M == (invAB A (α B N) M ∧ (length B = n ∧ length N = n))"

definition invar1 where
[simp]: "invar1 A B N ai = (invAM A {<ai} ∧ invAB2 A B N {<ai} ∧ ai ≤ n)"

definition invar2 where
[simp]: "invar2 A B N ai a ≡ (invAM A ({<ai+1} - {a}) ∧ invAB2 A B N ({<ai+1} - {a}) ∧ a ≤ ai ∧ ai < n)"

text ‹First, the `old' version with the more complicated inner variant:›

lemma Gale_Shapley5:
"VARS A B N ai a a'
 [ai = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar1 A B N ai }
 VAR { z = n - ai}
 DO a := ai;
  WHILE N ! match A a
  INV { invar2 A B N ai a ∧ z = n-ai }
  VAR {var A {<ai}}
  DO a' := B ! match A a;
     IF Q ! match A a' ⊢ a < a'
     THEN B[match A a] := a; A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI
  OD;
  B[match A a] := a; N[match A a] := True; ai := ai+1
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case  (* outer invar holds initially *)
   by(auto simp: pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 2 (* outer invar and b implies inner invar *)
  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
  case (4 z A B M ai a) (* inner invar' and not b implies outer invar *)
  note inv = 4[THEN conjunct1, unfolded invar2_def]
  note invAM = inv[THEN conjunct1,THEN conjunct1]
  note aai = inv[THEN conjunct1, THEN conjunct2, THEN conjunct2]
  show ?case
  proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
    case 1
    have *: "{<Suc ai} = insert a ({<Suc ai} - {a})" using aai by (simp add: insert_absorb)
    have **: "inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) ∧ match A a ∉ match A ` ({<Suc ai} - {a}))"
      by (metis "*" Diff_idemp inj_on_insert)
    have nm: "match A a ∉ match A ` ({<Suc ai} - {a})" using 4 unfolding invar2_def ran_def
        apply (clarsimp simp: set_eq_iff) by (metis)
    have invAM': "invAM A {<ai+1}"
      using invAM_match[OF invAM, of a] aai nm by (simp add: ** insert_absorb)
    show ?case using 4 invAM' by (simp add: αupdate1 match_less_n insert_absorb nth_list_update)
  next
    case 2 thus ?case using 4 by auto
  qed
next
  case 5 (* outer invar and not b implies post *)
  thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less)
next
  case (3 z v A B N ai a) (* preservation of inner invar *)
  let ?M = "{<ai+1} - {a}"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and matched: "N ! match A a" and as: "a ≤ ai ∧ ai < n" and invAB: "invAB2 A B N ?M"
    and v: "var A {<ai} = v" using 3 by auto
  note invar = 3[THEN conjunct1, THEN conjunct1, unfolded invar2_def]
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  let ?a = "B ! match A a"
  have a: "a < n ∧ a ∉ ?M" using invar by auto
  have a': "?a ∈ ?M ∧ match A ?a = match A a"
    using invAB match_less_n[OF A] a matched by (metis α_Some ranI)
  have "?M ≠ {<n}" and "?a < n" using M a a' atLeast0LessThan by auto
  have card: "card {<ai} = card ?M" using as by simp
  have *: "{<ai + 1} - {a} - {?a} ∪ {a} = {<ai + 1} - {?a}" using invar a' by auto
  show ?case
  proof (simp only: mem_Collect_eq prod.case, goal_cases)
    case 1
    show ?case
    proof ((rule;rule;rule), goal_cases)
      case unstab: 1
      have inj_dom: "inj_on (α B N) (dom (α B N))" by (metis (mono_tags) domD inj_onI invAB)
      have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (α (B[match A a := a]) N) ({<ai + 1} - {?a})"
        using invAB_swap[OF invAB[THEN conjunct1] a a' inj_dom] * match_less_n[OF A] a matched invAB
        by(simp add:αupdate2)
      show ?case using invAM_swap[OF invAM a a' unstab] invAB' invar a'
        unfolding * by (simp add: insert_absorb αupdate2)

      case 2
      show ?case using v var_next[OF m M ‹?M ≠ {<n}› pref_match1 ‹?a < n›] card
        by (metis var_def Suc_eq_plus1)
    next
      case stab: 3
      have *: "∀b. b < n ∧ N!b ⟶ a ≠ B!b" by (metis invAB ranI α_Some a) 
      show ?case using invAM_next[OF invAM a a' stab] invar * by (simp add: match_def)

      case 4
      show ?case using v var_next[OF m M ‹?M ≠ {<n}› pref_match1, of a] a card
        by (metis Suc_eq_plus1 var_def)
    qed
  qed
qed

text ‹The definitive version with variant @{const var2}:›

lemma Gale_Shapley5_var2:
"VARS A B N ai a a'
 [ai = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar1 A B N ai }
 VAR { z = n - ai}
 DO a := ai;
  WHILE N ! match A a
  INV { invar2 A B N ai a ∧ z = n-ai }
  VAR {var2 A}
  DO a' := B ! match A a;
     IF Q ! match A a' ⊢ a < a'
     THEN B[match A a] := a; A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI
  OD;
  B[match A a] := a; N[match A a] := True; ai := ai+1
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case  (* outer invar holds initially *)
   by(auto simp: pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 2 (* outer invar and b implies inner invar *)
  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
  case (4 z A B N ai a) (* inner invar' and not b implies outer invar *)
  note inv = 4[THEN conjunct1, unfolded invar2_def]
  note invAM = inv[THEN conjunct1,THEN conjunct1]
  note aai = inv[THEN conjunct1, THEN conjunct2, THEN conjunct2]
  show ?case
  proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
    case 1
    have *: "{<Suc ai} = insert a ({<Suc ai} - {a})" using aai by (simp add: insert_absorb)
    have **: "inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) ∧ match A a ∉ match A ` ({<Suc ai} - {a}))"
      by (metis "*" Diff_idemp inj_on_insert)
    have nm: "match A a ∉ match A ` ({<Suc ai} - {a})" using 4 unfolding invar2_def ran_def
        apply (clarsimp simp: set_eq_iff) by (metis)
    have invAM': "invAM A {<ai+1}"
      using invAM_match[OF invAM, of a] aai nm by (simp add: ** insert_absorb)
    show ?case using 4 invAM' by (simp add: αupdate1 match_less_n insert_absorb nth_list_update)
  next
    case 2 thus ?case using 4 by auto
  qed
next
  case 5 (* outer invar and not b implies post *)
  thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less)
next
  case (3 z v A B N ai a) (* preservation of inner invar *)
  let ?M = "{<ai+1} - {a}"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and matched: "N ! match A a" and as: "a ≤ ai ∧ ai < n" and invAB: "invAB2 A B N ?M"
    and v: "var2 A = v" using 3 by auto
  note invar = 3[THEN conjunct1, THEN conjunct1, unfolded invar2_def]
  let ?a = "B ! match A a"
  have a: "a < n ∧ a ∉ ?M" using invar by auto
  have a': "?a ∈ ?M ∧ match A ?a = match A a"
    using invAB match_less_n[OF A] a matched by (metis α_Some ranI)
  have "?M ≠ {<n}" and "?a < n" using M a a' atLeast0LessThan by auto
  have card: "card {<ai} = card ?M" using as by simp
  have *: "{<ai + 1} - {a} - {?a} ∪ {a} = {<ai + 1} - {?a}" using invar a' by auto
  show ?case
  proof (simp only: mem_Collect_eq prod.case, goal_cases)
    case 1
    show ?case
    proof ((rule;rule;rule), goal_cases)
      case unstab: 1
      note invAM' = invAM_swap[OF invAM a a' unstab]
      have inj_dom: "inj_on (α B N) (dom (α B N))" by (metis (mono_tags) domD inj_onI invAB)
      have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (α (B[match A a := a]) N) ({<ai + 1} - {?a})"
        using invAB_swap[OF invAB[THEN conjunct1] a a' inj_dom] * match_less_n[OF A] a matched invAB
        by(simp add:αupdate2)
      show ?case using invAM' invAB' invar a' unfolding * by (simp add: insert_absorb αupdate2)
       (* case 2 show ?case using v var2_next[OF invAM'] ‹a' < n› * atLeast0LessThan by auto*)

      case 2
      show ?case using v var2_next[OF invAM'] * M ‹?a < n› a' by (metis subset_Diff_insert)
    next
      case stab: 3
      note invAM' = invAM_next[OF invAM a a' stab]
      have "∀b. b < n ∧ N!b ⟶ a ≠ B!b" by (metis invAB ranI α_Some a) 
      thus ?case using invAM' invar by (simp add: match_def)

      case 4
      show ?case using v var2_next[OF invAM'] a ‹?M ≠ {<n}› by blast
    qed
  qed
qed


subsubsection ‹Algorithm 5.1: single-loop variant›

definition invar2' where
[simp]: "invar2' A B N ai a ≡ (invAM A ({<ai+1} - {a}) ∧ invAB2 A B N ({<ai+1} - {a}) ∧ a ≤ ai ∧ ai ≤ n)"

lemma pres2':
assumes "invar2' A B N ai a" "ai < n" "var A ({<ai + 1} - {a}) = v"
and after[simp]: "b = match A a" "a' = B ! b" "A1 = A[a' := A ! a' + 1]" "A2 = A[a := A ! a + 1]"
shows
  "(¬ N ! b ⟶
    invar2' A (B[b := a]) (N[b := True]) (ai + 1) (ai + 1) ∧ var A ({<ai + 1 + 1} - {ai + 1}) < v) ∧
   (N ! b ⟶
    (Q ! match A a' ⊢ a < a' ⟶ invar2' A1 (B[b := a]) N ai a' ∧ var A1 ({<ai + 1} - {a'}) < v) ∧
    (¬ Q ! match A a' ⊢ a < a' ⟶ invar2' A2 B N ai a ∧ var A2 ({<ai + 1} - {a}) < v))"
proof -
  let ?M = "{<ai+1} - {a}"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and v: "var A ?M = v" and as: "a ≤ ai ∧ ai < n" and invAB: "invAB2 A B N ?M"
    using assms by auto
  note invar = assms(1)
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  have a: "a < n ∧ a ∉ ?M" using as by (simp)
  show ?thesis (is "(¬ ?matched ⟶ ?THEN) ∧ (?matched ⟶ ?ELSE)")
  proof (rule; rule)
    assume "¬ ?matched"
    then have nm: "match A a ∉ match A ` ?M" using invAB unfolding ran_def
      apply (clarsimp simp: set_eq_iff) by metis
    show ?THEN
    proof(rule conjI, goal_cases)
      have *: "{<ai + 1 + 1} - {ai + 1} = {<ai + 1}" by auto
      have **: "{<ai + 1} - {a} ∪ {a} = {<ai + 1}" using as by auto
      hence invAM': "invAM A {<ai+1}" using invAM_match[OF invAM a nm] by simp
      have invAB': "invAB2 A (B[match A a := a]) (N[match A a := True]) {<ai+1}"
        using invAB ‹¬ ?matched› **
        by (simp add: A a αupdate1 match_less_n nth_list_update)
      case 1 show ?case using invAM' as invAB' *
        by (simp add: Suc_le_eq plus_1_eq_Suc)
      case 2 show ?case
        using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan * **
        unfolding v by (metis lessThan_iff)
    qed
  next
    assume matched: "?matched"
    let ?a = "B ! match A a"
    have a': "?a ∈ ?M ∧ match A ?a = match A a"
      using invAB match_less_n[OF A] a matched after by (metis α_Some ranI)
    hence "?a < n" "a ≠ ?a" using a M atLeast0LessThan by auto
    have inj_dom: "inj_on (α B N) (dom (α B N))" by (metis (mono_tags) domD inj_onI invAB)
    show ?ELSE (is "(?pref ⟶ ?THEN) ∧ (¬ ?pref ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?pref
      show ?THEN
      proof (rule conjI, goal_cases)
        have *: "{<ai + 1} - {a} - {?a} ∪ {a} = {<ai + 1} - {?a}" using a a' as by auto
        have a'neq: "∀b<n. b ≠ match A a ⟶ N!b ⟶ ?a ≠ B!b"
          using invAB a' by force
        have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (α (B[match A a := a]) N) ({<ai + 1} - {?a})"
          using invAB_swap[OF invAB[THEN conjunct1] a a' inj_dom] * match_less_n[OF A] a matched invAB
          by(simp add:αupdate2)
        case 1 show ?case using invAM_swap[OF invAM a a'] ‹?pref› invAB invAB' unfolding *
          using a' as by simp
        case 2
        have "card({<ai + 1} - {?a}) = card({<ai + 1} - {a})" using a a' as by auto
        thus ?case using v var_next[OF m M _ pref_match1, of ?a] ‹?a < n› a atLeast0LessThan
          by (metis Suc_eq_plus1 lessThan_iff var_def after)
      qed
    next
      assume "¬ ?pref"
      show ?ELSE
      proof (rule conjI, goal_cases)
        case 1
        have "invAB2 (A[a := A ! a + 1]) B N ?M" using invAB a
          by (metis match_def nth_list_update_neq ranI)
        thus ?case using invAM_next[OF invAM a a'] ‹¬ ?pref› invar after
          by (meson invar2'_def)
        case 2
        show ?case using a v var_next[OF m M _ pref_match1, of a] after
          by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) 
      qed
    qed
  qed
qed

lemma Gale_Shapley5_1: "VARS A B N a a' ai b
 [ai = 0 ∧ a = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar2' A B N ai a }
 VAR {var A ({<ai+1} - {a})}
 DO b := match A a;
  IF ¬ N ! b
  THEN B[b] := a; N[b] := True; ai := ai + 1; a := ai
  ELSE a' := B ! b;
       IF Q ! match A a' ⊢ a < a'
       THEN B[b] := a; A[a'] := A!a'+1; a := a'
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
   by(auto simp: pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 3 thus ?case using pref_match_stable
    using atLeast0_lessThan_Suc by force
next
  case (2 v A B N a a' ai b)
  thus ?case using pres2'
    by (simp only:mem_Collect_eq prod.case) blast
qed


subsection ‹Algorithm 6: replace ‹Q› by ranking ‹R››

lemma inner_to_outer:
assumes inv: "invar2 A B N ai a ∧ b = match A a" and not_b: "¬ N ! b"
shows "invar1 A (B[b := a]) (N[b := True]) (ai+1)"
proof -
  note invAM = inv[unfolded invar2_def, THEN conjunct1,THEN conjunct1]
  have *: "{<Suc ai} = insert a ({<Suc ai} - {a})" using inv by (simp add: insert_absorb)
  have **: "inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) ∧ match A a ∉ match A ` ({<Suc ai} - {a}))"
    by (metis "*" Diff_idemp inj_on_insert)
  have nm: "match A a ∉ match A ` ({<Suc ai} - {a})" using inv not_b unfolding invar2_def ran_def
      apply (clarsimp simp: set_eq_iff) by (metis)
  have invAM': "invAM A {<ai+1}"
    using invAM_match[OF invAM, of a] inv nm by (simp add: ** insert_absorb)
  show ?thesis using inv not_b invAM' match_less_n by (clarsimp simp: αupdate1 insert_absorb nth_list_update)
qed

lemma inner_pres:
assumes R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2" and
  inv: "invar2 A B N ai a" and m: "N ! b" and v: "var A {<ai} = v"
  and after: "A1 = A[a' := A ! a' + 1]" "A2 = A[a := A ! a + 1]"
    "a' = B!b" "r = R ! match A a'" "b = match A a"
shows "(r ! a < r ! a' ⟶ invar2 A1 (B[b:=a]) N ai a' ∧ var A1 {<ai} < v) ∧
  (¬ r ! a < r ! a' ⟶ invar2 A2 B N ai a ∧ var A2 {<ai} < v)"
proof -
  let ?M = "{<ai+1} - {a}"
  note [simp] = after
  note inv' = inv[unfolded invar2_def]
  have A: "wf A" and M: "?M ⊆ {<n}" and invAM: "invAM A ?M" and invAB: "invAB A (α B N) ?M"
    and mat: "matching A ?M" and as: "a ≤ ai ∧ ai < n" using inv' by auto
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  let ?a = "B ! match A a"
  have a: "a < n ∧ a ∉ ?M" using inv by auto
  have a': "?a ∈ ?M ∧ match A ?a = match A a"
    using invAB match_less_n[OF A] a m inv by (metis α_Some ranI ‹b = _›)
  have "?M ≠ {<n}" and "?a < n" using M a a' atLeast0LessThan by auto
  have card: "card {<ai} = card ?M" using as by simp
  show ?thesis
  proof ((rule;rule;rule), goal_cases)
    have *: "{<ai + 1} - {a} - {?a} ∪ {a} = {<ai + 1} - {?a}" using inv a' by auto
    case 1
    hence unstab: "Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q R by (simp)
    have inj_dom: "inj_on (α B N) (dom (α B N))" by (metis (mono_tags) domD inj_onI invAB)
    have invAB': "invAB A1 (α (B[match A a := a]) N) ({<ai + 1} - {?a})"
      using invAB_swap[OF invAB a a' inj_dom] * match_less_n[OF A] a m
      by (simp add: αupdate2 inv')
    show ?case using invAM_swap[OF invAM a a'] unstab invAB' inv a'
      unfolding * by (simp)
  next
    case 2
      show ?case using v var_next[OF mat M ‹?M ≠ {<n}› pref_match1 ‹?a < n›] card assms(5,7,9)
        by (metis Suc_eq_plus1 var_def)
  next
    have *: "∀b. b < n ∧ N!b ⟶ a ≠ B!b" by (metis invAB ranI α_Some a)
    case 3
    hence unstab: "¬ Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q
      by (simp add: ranking_iff_pref)
    then show ?case using invAM_next[OF invAM a a'] 3 inv * by (simp add: match_def)
  next
    case 4
      show ?case using v var_next[OF mat M ‹?M ≠ {<n}› pref_match1, of a] a card assms(6)
        by (metis Suc_eq_plus1 var_def)
  qed
qed

text ‹First, the `old' version with the more complicated inner variant:›

lemma Gale_Shapley6:
assumes "R = map ranking Q"
shows
"VARS A B N ai a a' b r
 [ai = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar1 A B N ai }
 VAR {z = n - ai}
 DO a := ai; b := match A a;
  WHILE N ! b
  INV { invar2 A B N ai a ∧ b = match A a ∧ z = n-ai }
  VAR {var A {<ai}}
  DO a' := B ! b; r := R ! match A a';
     IF r ! a < r ! a'
     THEN B[b] := a; A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI;
     b := match A a
  OD;
  B[b] := a; N[b] := True; ai := ai+1
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case  (* outer invar holds initially *)
   by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 2 (* outer invar and b implies inner invar *)
  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
  case 3 (* preservation of inner invar *)
  have R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2"
    by (simp add: Q_set ‹R = _› length_Q ranking_iff_pref)
  show ?case
  proof (simp only: mem_Collect_eq prod.case, goal_cases)
    case 1 show ?case using inner_pres[OF R _ _ refl refl refl] 3 by blast
  qed
next
  case 4 (* inner invar' and not b implies outer invar *)
  show ?case
  proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
    case 1 show ?case using 4 inner_to_outer by blast
  next
    case 2 thus ?case using 4 by auto
  qed
next
  case 5 (* outer invar and not b implies post *)
  thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less)
qed

lemma inner_pres_var2:
assumes R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2" and
  inv: "invar2 A B N ai a" and m: "N ! b" and v: "var2 A = v"
  and after: "A1 = A[a' := A ! a' + 1]" "A2 = A[a := A ! a + 1]"
    "a' = B!b" "r = R ! match A a'" "b = match A a"
shows "(r ! a < r ! a' ⟶ invar2 A1 (B[b:=a]) N ai a' ∧ var2 A1 < v) ∧
  (¬ r ! a < r ! a' ⟶ invar2 A2 B N ai a ∧ var2 A2 < v)"
proof -
  let ?M = "{<ai+1} - {a}"
  note [simp] = after
  note inv' = inv[unfolded invar2_def]
  have A: "wf A" and M: "?M ⊆ {<n}" and invAM: "invAM A ?M" and invAB: "invAB A (α B N) ?M"
    and mat: "matching A ?M" and as: "a ≤ ai ∧ ai < n" using inv' by auto
  let ?a = "B ! match A a"
  have a: "a < n ∧ a ∉ ?M" using inv by auto
  have a': "?a ∈ ?M ∧ match A ?a = match A a"
    using invAB match_less_n[OF A] a m inv by (metis α_Some ranI ‹b = _›)
  have "?M ≠ {<n}" and "?a < n" using M a a' atLeast0LessThan by auto
  have card: "card {<ai} = card ?M" using as by simp
  show ?thesis
  proof ((rule;rule;rule), goal_cases)
    have *: "{<ai + 1} - {a} - {?a} ∪ {a} = {<ai + 1} - {?a}" using inv a' by auto
    note invAM' =  invAM_swap[OF invAM a a']
    case 1
    hence unstab: "Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q R by (simp)
    have inj_dom: "inj_on (α B N) (dom (α B N))" by (metis (mono_tags) domD inj_onI invAB)
    have invAB': "invAB A1 (α (B[match A a := a]) N) ({<ai + 1} - {?a})"
      using invAB_swap[OF invAB a a' inj_dom] * match_less_n[OF A] a m
      by (simp add: αupdate2 inv')
    show ?case using invAM' unstab invAB' inv a' unfolding * by (simp)

    case 2
      show ?case using v var2_next[OF invAM'] assms(5,7,9) * M ‹?a < n› a'
        by (metis subset_Diff_insert unstab)
  next
    have *: "∀b. b < n ∧ N!b ⟶ a ≠ B!b" by (metis invAB ranI α_Some a)
    note invAM' = invAM_next[OF invAM a a']
    case 3
    hence unstab: "¬ Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q
      by (simp add: ranking_iff_pref)
    then show ?case using invAM' 3 inv * by (simp add: match_def)

    case 4
      show ?case using v var2_next[OF invAM'] a assms(6,7,9) ‹?M ≠ {<n}› unstab by fastforce
  qed
qed

text ‹The definitive version with variant @{const var2}:›

lemma Gale_Shapley6_var2:
assumes "R = map ranking Q"
shows
"VARS A B N ai a a' b r
 [ai = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar1 A B N ai }
 VAR {z = n - ai}
 DO a := ai; b := match A a;
  WHILE N ! b
  INV { invar2 A B N ai a ∧ b = match A a ∧ z = n-ai }
  VAR {var2 A}
  DO a' := B ! b; r := R ! match A a';
     IF r ! a < r ! a'
     THEN B[b] := a; A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI;
     b := match A a
  OD;
  B[b] := a; N[b] := True; ai := ai+1
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case  (* outer invar holds initially *)
   by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 2 (* outer invar and b implies inner invar *)
  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
  case 3 (* preservation of inner invar *)
  have R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2"
    by (simp add: Q_set ‹R = _› length_Q ranking_iff_pref)
  show ?case
  proof (simp only: mem_Collect_eq prod.case, goal_cases)
    case 1 show ?case using inner_pres_var2[OF R _ _ refl refl refl] 3 by blast
  qed
next
  case 4 (* inner invar' and not b implies outer invar *)
  show ?case
  proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
    case 1 show ?case using 4 inner_to_outer by blast
  next
    case 2 thus ?case using 4 by auto
  qed
next
  case 5 (* outer invar and not b implies post *)
  thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less)
qed

text ‹A less precise version where the inner variant does not depend on variables changed in the outer loop.
Thus the inner variant is an upper bound on the number of executions of the inner loop test/body.
Superseded by the @{const var2} version.›

lemma var0_next2:
assumes "wf (A[a' := A ! a' + 1])" "a' < n"
shows "var0 (A[a' := A ! a' + 1]) {<n} < var0 A {<n}"
proof -
  let ?A = "A[a' := A ! a' + 1]"
  have 0: "card {<n} = n" by simp
  have *: "(∑a<n. ?A!a) + card {<n} ≤ n^2"
    using sumA_ub[OF assms(1)] 0 by (simp add: power2_eq_square algebra_simps le_diff_conv2)
  have "(∑a<n. A!a) < (∑a<n. ?A!a) "
    using assms sum.remove[of "{<n}" a' "(!) A"]
    by(simp add: nth_list_update sum.If_cases lessThan_atLeast0 Diff_eq)
  thus ?thesis using * unfolding var0_def by linarith
qed


lemma inner_pres2:
assumes R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2" and
  inv: "invar2 A B N ai a" and m: "N ! b" and v: "var0 A {<n} = v"
  and after: "A1 = A[a' := A ! a' + 1]" "A2 = A[a := A ! a + 1]"
    "a' = B!b" "r = R ! match A a'" "b = match A a"
shows "(r ! a < r ! a' ⟶ invar2 A1 (B[b:=a]) N ai a' ∧ var0 A1 {<n} < v) ∧
  (¬ r ! a < r ! a' ⟶ invar2 A2 B N ai a ∧ var0 A2 {<n} < v)"
proof -
  let ?M = "{<ai+1} - {a}"
  note [simp] = after
  note inv' = inv[unfolded invar2_def]
  have A: "wf A" and M: "?M ⊆ {<n}" and invAM: "invAM A ?M" and invAB: "invAB A (α B N) ?M"
    and mat: "matching A ?M"
    and as: "a ≤ ai ∧ ai < n" using inv' by auto
  note pref_match1 = preferred_subset_match_if_invAM[OF invAM]
  let ?a = "B ! match A a"
  have a: "a < n ∧ a ∉ ?M" using inv by auto
  have a': "?a ∈ ?M ∧ match A ?a = match A a"
    using invAB match_less_n[OF A] a m inv by (metis α_Some ranI ‹b = _›)
  have "?M ≠ {<n}" and "?a < n" using M a a' atLeast0LessThan by auto
  have card: "card {<ai} = card ?M" using as by simp
  show ?thesis
  proof ((rule;rule;rule), goal_cases)
    have *: "{<ai + 1} - {a} - {?a} ∪ {a} = {<ai + 1} - {?a}" using inv a' by auto
    case 1
    hence unstab: "Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q R by (simp)
    have inj_dom: "inj_on (α B N) (dom (α B N))" by (metis (mono_tags) domD inj_onI invAB)
    have invAB': "invAB A1 (α (B[match A a := a]) N) ({<ai + 1} - {?a})"
      using invAB_swap[OF invAB a a' inj_dom] * match_less_n[OF A] a m
      by (simp add: αupdate2 inv')
    show ?case using invAM_swap[OF invAM a a'] unstab invAB' inv a'
      unfolding * by (simp add: insert_absorb αupdate2)
  next
    case 2
    hence unstab: "Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q R by (simp)
    from invAM_swap[OF invAM a a'] unstab have wf: "wf (A[a' := A ! a' + 1])" by auto
    show ?case using v var0_next2[OF wf] using ‹B ! match A a < n› assms(5,7,9) by blast
  next
    have *: "∀b. b < n ∧ N!b ⟶ a ≠ B!b" by (metis invAB ranI α_Some a)
    case 3
    hence unstab: "¬ Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q
      by (simp add: ranking_iff_pref)
    then show ?case using invAM_next[OF invAM a a'] 3 inv * by (simp add: match_def)
  next
    case 4
    hence unstab: "¬ Q ! match A a' ⊢ a < a'"
      using R a a' as Q_set P_set match_less_n[OF A] n_def length_Q
      by (simp add: ranking_iff_pref)
    from invAM_next[OF invAM a a'] unstab have wf: "wf (A[a := A ! a + 1])" by auto
    show ?case using v var0_next2[OF wf] a using assms(6) by presburger
  qed
qed

lemma Gale_Shapley6':
assumes "R = map ranking Q"
shows
"VARS A B N ai a a' b r
 [ai = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar1 A B N ai }
 VAR {z = n - ai}
 DO a := ai; b := match A a;
  WHILE N ! b
  INV { invar2 A B N ai a ∧ b = match A a ∧ z = n-ai }
  VAR {var0 A {<n}}
  DO a' := B ! b; r := R ! match A a';
     IF r ! a < r ! a'
     THEN B[b] := a; A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI;
     b := match A a
  OD;
  B[b] := a; N[b] := True; ai := ai+1
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case  (* outer invar holds initially *)
   by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 2 (* outer invar and b implies inner invar *)
  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
  case 3 (* preservation of inner invar *)
  have R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2"
    by (simp add: Q_set ‹R = _› length_Q ranking_iff_pref)
  show ?case
  proof (simp only: mem_Collect_eq prod.case, goal_cases)
    case 1 show ?case using inner_pres2[OF R _ _ refl refl refl] 3 by blast
  qed
next
  case 4 (* inner invar' and not b implies outer invar *)
  show ?case
  proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
    case 1 show ?case using 4 inner_to_outer by blast
  next
    case 2 thus ?case using 4 by auto
  qed
next
  case 5 (* outer invar and not b implies post *)
  thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less)
qed


subsubsection ‹Algorithm 6.1: single-loop variant›

lemma R_iff_P:
assumes "R = map ranking Q" "invar2' A B N ai a" "ai < n" "N ! match A a"
shows "(R ! match A (B ! match A a) ! a < R ! match A (B ! match A a) ! (B ! match A a)) =
  (Q ! match A (B ! match A a) ⊢ a < B ! match A a)"
proof -
  have R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2"
    by (simp add: Q_set ‹R = _› length_Q ranking_iff_pref)
  let ?M = "{<ai+1} - {a}"
  have A: "wf A" and M: "?M ⊆ {<n}" and as: "a < n" and invAB: "invAB2 A B N ?M"
      using assms(2,3) by auto
  have a': "B ! match A a ∈ ?M"
    using invAB match_less_n[OF A] as ‹N!match A a› by (metis α_Some ranI)
  hence "B ! match A a < n" using M by auto
  thus ?thesis using assms R match_less_n by auto
qed


lemma Gale_Shapley6_1:
assumes "R = map ranking Q"
shows "VARS A B N a a' ai b r
 [ai = 0 ∧ a = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar2' A B N ai a }
 VAR {var A ({<ai+1} - {a})}
 DO b := match A a;
  IF ¬ N ! b
  THEN B[b] := a; N[b] := True; ai := ai + 1; a := ai
  ELSE a' := B ! b; r := R ! match A a';
       IF r ! a < r ! a'
       THEN B[b] := a; A[a'] := A!a'+1; a := a'
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
   by(auto simp: pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 3 thus ?case using pref_match_stable atLeast0_lessThan_Suc by force
next
  case (2 v A B N a a' ai)
  have R': "N ! match A a ⟹
    (R ! match A (B ! match A a) ! a < R ! match A (B ! match A a) ! (B ! match A a)) =
     (Q ! match A (B ! match A a) ⊢ a < B ! match A a)"
    using R_iff_P 2 assms by blast
  show ?case
    apply(simp only:mem_Collect_eq prod.case)
    using 2 R' pres2'[of A B N ai a] by presburger
qed

(* TODO: rm? *)
lemma Gale_Shapley6_1_explicit:
assumes "R = map ranking Q"
shows "VARS A B N a a' ai b r
 [ai = 0 ∧ a = 0 ∧ A = replicate n 0 ∧ length B = n ∧ N = replicate n False]
 WHILE ai < n
 INV { invar2' A B N ai a }
 VAR {var A ({<ai+1} - {a})}
 DO b := match A a;
  IF ¬ N ! b
  THEN B[b] := a; N[b] := True; ai := ai + 1; a := ai
  ELSE a' := B ! b; r := R ! match A a';
       IF r ! a < r ! a'
       THEN B[b] := a; A[a'] := A!a'+1; a := a'
       ELSE A[a] := A!a+1
       FI
  FI 
 OD
 [matching A {<n} ∧ stable A {<n} ∧ optiA A]"
proof (vcg_tc, goal_cases)
  case 1 thus ?case
   by(auto simp: pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case 3 thus ?case using pref_match_stable atLeast0_lessThan_Suc by force
next
  case (2 v A B N a a' ai b)
  let ?M = "{<ai+1} - {a}"
  have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M ⊆ {<n}"
    and pref_match: "pref_match A ?M"
    and v: "var A ?M = v" and as: "a ≤ ai ∧ ai < n" and invAB: "invAB2 A B N ?M"
    using 2 by auto
  note invar = 2[THEN conjunct1,THEN conjunct1]
  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
  hence pref_match1: "∀a<n. preferred A a ⊆ match A ` ?M" unfolding pref_match'_def by blast
  have a: "a < n ∧ a ∉ ?M" using as by (simp)
  show ?case (is "(?not_matched ⟶ ?THEN) ∧ (¬ ?not_matched ⟶ ?ELSE)")
  proof (rule; rule)
    assume ?not_matched
    then have nm: "match A a ∉ match A ` ?M" using invAB unfolding ran_def
      apply (clarsimp simp: set_eq_iff) by metis
    show ?THEN
    proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases)
      have *: "{<ai + 1 + 1} - {ai + 1} = {<ai + 1}" by auto
      have **: "{<ai + 1} - {a} ∪ {a} = {<ai + 1}" using as by auto
      hence invAM': "invAM A {<ai+1}" using invAM_match[OF invAM a nm] by simp
      have invAB': "invAB2 A (B[match A a := a]) (N[match A a := True]) {<ai+1}"
        using invAB ‹?not_matched› **
        by (simp add: A a αupdate1 match_less_n nth_list_update)
      case 1 show ?case using invAM' as invAB' *
        by (simp add: Suc_le_eq plus_1_eq_Suc)
      case 2 show ?case
        using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan * **
        unfolding v by (metis lessThan_iff)
    qed
  next
    assume matched: "¬ ?not_matched"
    let ?a = "B ! match A a"
    have a': "?a ∈ ?M ∧ match A ?a = match A a"
      using invAB match_less_n[OF A] a matched by (metis α_Some ranI)
    hence "?a < n" "a ≠ ?a" using a M atLeast0LessThan by auto
    have inj_dom: "inj_on (α B N) (dom (α B N))" by (metis (mono_tags) domD inj_onI invAB)
    show ?ELSE (is "(?pref ⟶ ?THEN) ∧ (¬ ?pref ⟶ ?ELSE)")
    proof (rule; rule)
      assume ?pref
      show ?THEN
      proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
        have *: "{<ai + 1} - {a} - {?a} ∪ {a} = {<ai + 1} - {?a}" using a a' as by auto
        have a'neq: "∀b<n. b ≠ match A a ⟶ N!b ⟶ ?a ≠ B!b"
          using invAB a' by force
        have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (α (B[match A a := a]) N) ({<ai + 1} - {?a})"
          using invAB_swap[OF invAB[THEN conjunct1] a a' inj_dom] * match_less_n[OF A] a matched invAB
          by(simp add:αupdate2)
        have pref: "Q ! match A ?a ⊢ a < ?a" using A Q_set ‹?a < n› ‹?pref› a assms length_Q
          by(auto simp: match_less_n ranking_iff_pref)
        case 1 show ?case (* changed *)
          using invAM_swap[OF invAM a a' pref] invAB invAB' a' as unfolding *
          by (simp add: match_less_n ranking_iff_pref)
        case 2
        have "card({<ai + 1} - {?a}) = card({<ai + 1} - {a})" using a a' as by auto
        thus ?case using v var_next[OF m M _ pref_match1, of ?a] ‹?a < n› a atLeast0LessThan
          by (metis Suc_eq_plus1 lessThan_iff var_def)
      qed
    next
      assume "¬ ?pref"
      show ?ELSE
      proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
        case 1
        have "invAB2 (A[a := A ! a + 1]) B N ?M" using invAB a
          by (metis match_def nth_list_update_neq ranI)
        thus ?case using invAM_next[OF invAM a a'] ‹¬ ?pref›  ‹B ! match A a < n› Q_set 2 assms
          by (simp add: invar2'_def length_Q match_less_n ranking_iff_pref) (* changed *)
        case 2
        show ?case using a v var_next[OF m M _ pref_match1, of a]
          by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) 
      qed
    qed
  qed
qed

end


subsection ‹Functional implementation›

definition
"gs_inner P R N =
  while (λ(A,B,a,b). N!b)
    (λ(A,B,a,b).
      let a' = B ! b;
          r = R ! (P ! a' ! (A ! a')) in
      let (A, B, a) =
        if r ! a < r ! a'
        then (A[a' := A!a' + 1], B[b := a], a')
        else (A[a := A!a + 1], B, a)
      in (A, B, a, P ! a ! (A ! a)))"

definition
"gs n P R =
  while (λ(A,B,N,ai). ai < n)
   (λ(A,B,N,ai).
     let (A,B,a,b) = gs_inner P R N (A, B, ai, P ! ai ! (A ! ai))
     in (A, B[b:=a], N[b:=True], ai+1))
  (replicate n 0, replicate n 0, replicate n False,0)"

definition
"gs1 n P R =
  while (λ(A,B,N,ai,a). ai < n)
   (λ(A,B,N,ai,a).
     let b = P ! a ! (A ! a) in
     if ¬ N ! b
     then (A, B[b := a], N[b := True], ai+1, ai+1)
     else let a' = B ! b; r = R ! (P ! a' ! (A ! a')) in
       if r ! a < r ! a'
       then (A[a' := A!a'+1], B[b := a], N, ai, a')
       else (A[a := A!a+1], B, N, ai, a))
  (replicate n 0, replicate n 0, replicate n False, 0, 0)"

context Pref
begin

lemma gs_inner:
assumes "R = map ranking Q"
assumes "invar2 A B N ai a" "b = match A a"
shows "gs_inner P R N (A, B, a, b) = (A',B',a',b') ⟶ invar1 A' (B'[b' := a']) (N[b' := True]) (ai+1)"
unfolding gs_inner_def
proof(rule while_rule2[where P = "λ(A,B,a,b). invar2 A B N ai a ∧ b = match A a"
 and r = "measure (%(A, B, a, b). Pref.var P A {<ai})"], goal_cases)
  case 1
  show ?case using assms unfolding var_def by simp
next
  case inv: (2 s)
  obtain A B a b where s: "s =  (A, B, a, b)"
    using prod_cases4 by blast
  have R: "∀b<n. ∀a1<n. ∀a2<n. R ! b ! a1 < R ! b ! a2 ⟷ Q ! b ⊢ a1 < a2"
    by (simp add: Q_set ‹R = _› length_Q ranking_iff_pref)
  show ?case
  proof(rule, goal_cases)
    case 1 show ?case
    using inv apply(simp only: s prod.case Let_def split: if_split)
    using inner_pres[OF R _ _ refl refl refl refl refl, of A B N ai a b]
    unfolding invar2_def match_def by presburger
    case 2 show ?case
    using inv apply(simp only: s prod.case Let_def in_measure split: if_split)
    using inner_pres[OF R _ _ refl refl refl refl refl, of A B N ai a b]
    unfolding invar2_def match_def by presburger
  qed
next
  case 3
  show ?case
  proof (rule, goal_cases)
    case 1 show ?case by(rule inner_to_outer[OF 3[unfolded 1 prod.case]])
  qed
next
  case 4
  show ?case by simp
qed

lemma gs: assumes "R = map ranking Q"
shows "gs n P R = (A,BNai) ⟶ matching A {<n} ∧ stable A {<n} ∧ optiA A"
unfolding gs_def
proof(rule while_rule2[where P = "λ(A,B,N,ai). invar1 A B N ai"
  and r = "measure(λ(A,B,N,ai). n - ai)"], goal_cases)
  case 1 show ?case
   by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case (2 s)
  obtain A B N ai where s: "s =  (A, B, N, ai)"
    using prod_cases4 by blast
  have 1: "invar2 A B N ai ai" using 2 s
    by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
  show ?case using 2 s gs_inner[OF ‹R = _ › 1] by (auto simp: match_def simp del: invar1_def split: prod.split)
next
  case 3
  thus ?case using pref_match_stable by auto
next
  case 4
  show ?case by simp
qed


lemma gs1: assumes "R = map ranking Q"
shows "gs1 n P R = (A,BNaia) ⟶ matching A {<n} ∧ stable A {<n} ∧ optiA A"
unfolding gs1_def
proof(rule while_rule2[where P = "λ(A,B,N,ai,a). invar2' A B N ai a"
  and r = "measure (%(A, B, N, ai, a). Pref.var P A ({<ai+1} - {a}))"], goal_cases)
  case 1 show ?case
    by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def α_def cong: conj_cong)
next
  case (2 s)
  obtain A B N ai a where s: "s =  (A, B, N, ai, a)"
    using prod_cases5 by blast
  hence 1: "invar2' A B N ai a" "ai < n" using 2 by (simp_all)
  have R': "N ! match A a ⟹
    (R ! match A (B ! match A a) ! a < R ! match A (B ! match A a) ! (B ! match A a)) =
     (Q ! match A (B ! match A a) ⊢ a < B ! match A a)"
    using R_iff_P[OF assms 1] by linarith
  show ?case 
    using 1 R' pres2'[OF 1]
    apply(simp only: s mem_Collect_eq prod.case Let_def in_measure match_def split: if_split)
    by blast
next
  case (3 s)
  obtain B N ai a where "BNaia =  (B, N, ai, a)"
    using prod_cases4 by blast
  with 3 show ?case
    using pref_match_stable atLeast0_lessThan_Suc by force
next
  case 4
  show ?case by simp
qed


end


subsection ‹Executable functional Code›

definition
"Gale_Shapley P Q = (if Pref P Q then Some (fst (gs (length P) P (map ranking Q))) else None)"

theorem gs: "⟦ Pref P Q; n = length P ⟧ ⟹
 ∃A. Gale_Shapley P Q = Some(A) ∧ Pref.matching P A {<n} ∧
   Pref.stable P Q A {<n} ∧ Pref.optiA P Q A"
unfolding Gale_Shapley_def using Pref.gs
by (metis fst_conv surj_pair)

declare Pref_def [code]

definition
"Gale_Shapley1 P Q = (if Pref P Q then Some (fst (gs1 (length P) P (map ranking Q))) else None)"

theorem gs1: "⟦ Pref P Q; n = length P ⟧ ⟹
 ∃A. Gale_Shapley1 P Q = Some(A) ∧ Pref.matching P A {<n} ∧
   Pref.stable P Q A {<n} ∧ Pref.optiA P Q A"
unfolding Gale_Shapley1_def using Pref.gs1
by (metis fst_conv surj_pair)

declare Pref_def [code]

text ‹Two examples from Gusfield and Irving:›

lemma "Gale_Shapley
  [[3,0,1,2], [1,2,0,3], [1,3,2,0], [2,0,3,1]]
  [[3,0,2,1], [0,2,1,3], [0,1,2,3], [3,0,2,1]]
  = Some[0,1,0,1]"
by eval

lemma "Gale_Shapley1
  [[4,6,0,1,5,7,3,2], [1,2,6,4,3,0,7,5], [7,4,0,3,5,1,2,6], [2,1,6,3,0,5,7,4],
   [6,1,4,0,2,5,7,3], [0,5,6,4,7,3,1,2], [1,4,6,5,2,3,7,0], [2,7,3,4,6,1,5,0]]
  [[4,2,6,5,0,1,7,3], [7,5,2,4,6,1,0,3], [0,4,5,1,3,7,6,2], [7,6,2,1,3,0,4,5],
   [5,3,6,2,7,0,1,4], [1,7,4,2,3,5,6,0], [6,4,1,0,7,5,3,2], [6,3,0,4,1,2,5,7]]
  = Some [0, 1, 0, 5, 0, 0, 0, 2]"
by eval

end