Theory Gale_Shapley1
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)
syntax_consts
"_assign_list" ⇌ list_update
translations
"xs[n] := e" ⇀ "xs := CONST list_update xs n e"
abbreviation upt_set :: "nat ⇒ nat set" (‹{<_}›) where
"{<n} ≡ {0..<n}"
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
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›
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
by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def)[]
next
case 2
thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
case (4 z A B ai a)
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
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')
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
by(auto simp: stable_def pref_match_def P_set card_distinct match_def index_nth_id prefers_def optiA_def)[]
next
case 2
thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
case (4 z A B ai a)
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
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')
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
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
thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
case (4 z A B M ai a)
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
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)
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
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
thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
case (4 z A B N ai a)
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
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)
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'] * 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
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
thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
case 3
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
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
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
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
thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
case 3
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
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
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
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
thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
next
case 3
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
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
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
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
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)
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