diff --git a/thys/Gale_Shapley/Gale_Shapley1.thy b/thys/Gale_Shapley/Gale_Shapley1.thy
new file mode 100644
--- /dev/null
+++ b/thys/Gale_Shapley/Gale_Shapley1.thy
@@ -0,0 +1,1298 @@
+(*
+Stepwise refinement of the Gale-Shapley algorithm down to executable functional code.
+
+Part 1: Refinement down to lists.
+
+Author: Tobias Nipkow
+*)
+
+theory Gale_Shapley1
+imports Main
+  "HOL-Hoare.Hoare_Logic"
+  "List-Index.List_Index"
+  "HOL-Library.While_Combinator"
+  "HOL-Library.LaTeXsugar"
+begin
+
+lemmas conj12 = conjunct1 conjunct2
+
+(* TODO: mv *)
+theorem while_rule2:
+  "[| P s;
+      !!s. [| P s; b s  |] ==> P (c s) \<and> (c s, s) \<in> r;
+      !!s. [| P s; \<not> b s  |] ==> Q s;
+      wf r |] ==>
+   Q (while b c s)"
+using while_rule[of P] by metis
+
+(* by now in Map *)
+lemma ran_map_upd_Some:
+  "\<lbrakk> m x = Some y; inj_on m (dom m); z \<notin> ran m \<rbrakk> \<Longrightarrow> ran(m(x := Some z)) = ran m - {y} \<union> {z}"
+by(force simp add: ran_def domI inj_onD)
+
+syntax
+  "_assign_list" :: "idt \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'com"  ("(2_[_] :=/ _)" [70, 0, 65] 61)
+
+translations
+  "xs[n] := e" \<rightharpoonup> "xs := CONST list_update xs n e"
+
+abbreviation upt_set :: "nat \<Rightarrow> nat set" ("{<_}") where
+"{<n} \<equiv> {0..<n}"
+
+(* Maybe also require y : set P? *)
+definition prefers :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
+"prefers P x y = (index P x < index P y)"
+
+abbreviation prefa :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_ \<turnstile>/ _ < _)" [50,50,50] 50) where
+"P \<turnstile> x < y \<equiv> prefers P x y"
+
+lemma prefers_asym: "P \<turnstile> x < y \<Longrightarrow> \<not> P \<turnstile> y < x"
+by(simp add: prefers_def)
+
+lemma prefers_trans: "P \<turnstile> x < y \<Longrightarrow> P \<turnstile> y < z \<Longrightarrow> P \<turnstile> x < z"
+by (meson order_less_trans prefers_def)
+
+fun rk_of_pref :: "nat \<Rightarrow> nat list \<Rightarrow> nat list \<Rightarrow> 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 \<Rightarrow> 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: "\<lbrakk> length P \<le> length rs; i \<in> set P; distinct P; set P \<subseteq> {<length rs} \<rbrakk>
+ \<Longrightarrow> 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_iff_pref:  "\<lbrakk> set P = {<length P}; i < length P; j < length P \<rbrakk>
+ \<Longrightarrow> ranking P ! i < ranking P ! j \<longleftrightarrow> P \<turnstile> i < j"
+by(simp add: ranking_def prefers_def nth_rk_of_pref card_distinct)
+
+
+subsection \<open>Fixing the preference lists\<close>
+ 
+type_synonym prefs = "nat list list"
+
+locale Pref =
+fixes n
+fixes P\<^sub>a :: prefs
+fixes P\<^sub>b :: prefs
+defines "n \<equiv> length P\<^sub>a"
+assumes length_P\<^sub>b: "length P\<^sub>b = n"
+assumes P\<^sub>a_set: "a < n  \<Longrightarrow> length(P\<^sub>a!a) = n \<and> set(P\<^sub>a!a) = {<n}"
+assumes P\<^sub>b_set: "b < n \<Longrightarrow> length(P\<^sub>b!b) = n \<and> set(P\<^sub>b!b) = {<n}"
+begin
+
+
+abbreviation wf :: "nat list \<Rightarrow> bool" where
+"wf xs \<equiv> length xs = n \<and> set xs \<subseteq> {<n}"
+
+lemma wf_less_n: "\<lbrakk> wf A; a < n \<rbrakk> \<Longrightarrow> A!a < n"
+by (simp add: subset_eq)
+
+corollary wf_le_n1: "\<lbrakk> wf A; a < n \<rbrakk> \<Longrightarrow> A!a \<le> n-1"
+using wf_less_n by fastforce
+
+lemma sumA_ub: "wf A \<Longrightarrow> (\<Sum>a<n. A!a) \<le> n*(n-1)"
+using sum_bounded_above[of "{..<n}" "((!) A)" "n-1"] wf_le_n1[of A] by (simp)
+
+
+subsubsection \<open>The (termination) variant(s)\<close>
+
+text \<open>Basic idea: either some \<open>A!a\<close> is incremented or size of \<open>M\<close> is incremented, but this cannot
+go on forever because in the worst case all \<open>A!a = n-1\<close> and \<open>M = n\<close>. Because \<open>n*(n-1) + n = n^2\<close>,
+this leads to the following simple variant:\<close>
+
+definition var0 :: "nat list \<Rightarrow> nat set \<Rightarrow> nat" where
+[simp]: "var0 A M = (n^2 - ((\<Sum>a<n. A!a) + card M))"
+
+lemma var0_match:
+assumes "wf A" "M \<subseteq> {<n}" "a < n \<and> a \<notin> M"
+shows "var0 A (M \<union> {a}) < var0 A M"
+proof -
+  have 2: "M \<subset> {<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 \<subseteq> {<n}" "M \<noteq> {<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 + (\<Sum>a<n. A!a) + card M \<le> 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 "\<dots> = n^2 - (1 + (\<Sum>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 "\<dots> < n^2 - ((\<Sum>a<n. A!a) + card M)" unfolding power2_eq_square using * by linarith
+  finally show ?thesis unfolding var0_def .
+qed
+
+definition var :: "nat list \<Rightarrow> nat set \<Rightarrow> nat" where
+[simp]: "var A M = (n^2 - n + 1 - ((\<Sum>a<n. A!a) + card M))"
+
+lemma sumA_ub2:
+assumes "a' < n" "A!a' \<le> n-1" "\<forall>a < n. a \<noteq> a' \<longrightarrow> A!a \<le> n-2"
+shows "(\<Sum>a<n. A!a) \<le> (n-1)*(n-1)"
+proof -
+  have "(\<Sum>a<n. A!a) = (\<Sum>a \<in> ({<n}-{a'}) \<union> {a'}. A!a)"
+    by (simp add: assms(1) atLeast0LessThan insert_absorb)
+  also have "\<dots> =(\<Sum>a \<in> {<n}-{a'}. A!a) + A!a'"
+    by (simp add: sum.insert_remove)
+  also have "\<dots> \<le> (\<Sum>a \<in> {<n}-{a'}. A!a) + (n-1)" using assms(2) by linarith
+  also have "\<dots> \<le> (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 "\<dots> = (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\<^sub>a ! a ! (A ! a)"
+
+lemma match_less_n: "\<lbrakk> wf A; a < n \<rbrakk> \<Longrightarrow> match A a < n"
+by (metis P\<^sub>a_set atLeastLessThan_iff match_def nth_mem subset_eq)
+
+lemma match_upd_neq: "\<lbrakk> wf A; a < n; a \<noteq> a' \<rbrakk> \<Longrightarrow> match (A[a := b]) a' = match A a'"
+by (simp add: match_def)
+
+definition blocks :: "nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+"blocks A a a' = (P\<^sub>a ! a \<turnstile> match A a' < match A a \<and> P\<^sub>b ! match A a' \<turnstile> a < a')"
+
+definition stable :: "nat list \<Rightarrow> nat set \<Rightarrow> bool" where
+"stable A M = (\<not>(\<exists>a\<in>M. \<exists>a'\<in>M. a \<noteq> a' \<and> blocks A a a'))"
+
+text \<open>The set of Bs that an A would prefer to its current match,
+i.e. all Bs above its current match \<open>A!a\<close>.\<close>
+abbreviation preferred where
+"preferred A a == nth (P\<^sub>a!a) ` {<A!a}"
+
+definition matching where [simp]:
+"matching A M = (wf A \<and> inj_on (match A) M)"
+
+
+text \<open>If \<open>a'\<close> is unmatched and final then all other \<open>a\<close> are matched:\<close>
+
+lemma final_last:
+assumes M: "M \<subseteq> {<n}" and inj: "inj_on (match A) M" and pref_match': "preferred A a \<subseteq> match A ` M"
+and a: "a < n \<and> a \<notin> M" and final: "A ! a + 1 = n"
+shows "insert a M = {<n}"
+proof -
+  let ?B = "preferred A a"
+  have "(!) (P\<^sub>a ! a) ` {<n} = {<n}" by (metis P\<^sub>a_set a map_nth set_map set_upt)
+  hence "inj_on ((!) (P\<^sub>a ! a)) {<n}" by(simp add: eq_card_imp_inj_on)
+  hence "inj_on ((!) (P\<^sub>a ! a)) {<A!a}" using final by(simp add: subset_inj_on)
+  hence 1: "Suc(card ?B) = n" using P\<^sub>a_set a final by (simp add: card_image)
+  have 2: "card ?B \<le> 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: "matching A M" and M: "M \<subseteq> {<n}" "M \<noteq> {<n}"
+and pref_match': "preferred A a \<subseteq> match A ` M"
+and "a < n" and matched: "match A a \<in> match A ` M"
+shows "A ! a + 1 < n"
+proof (rule ccontr)
+  have match: "match A ` M \<subseteq> {<n}" using A M P\<^sub>a_set unfolding matching_def
+    by (smt (verit, best) atLeastLessThan_iff match_def image_subsetI in_mono nth_mem)
+  have "card M < n" using M
+    by (metis card_atLeastLessThan card_seteq diff_zero finite_atLeastLessThan not_less)
+  assume "\<not> A ! a + 1 < n"
+  hence "A ! a + 1 = n" using A \<open>a < n\<close> unfolding matching_def
+    by (metis add.commute wf_less_n linorder_neqE_nat not_less_eq plus_1_eq_Suc)
+  hence *: "nth (P\<^sub>a ! a) ` {<n} \<subseteq> match A ` M"
+    using pref_match' matched less_Suc_eq match_def by fastforce
+  have "nth (P\<^sub>a!a) ` {<n} = {<n}"
+    by (metis \<open>a < n\<close> map_nth P\<^sub>a_set set_map set_upt)
+  hence "match A ` M = {<n}"
+    by (metis * match set_eq_subset)
+  then show False using A M \<open>card M < n\<close> unfolding matching_def
+    by (metis atLeast0LessThan card_image card_lessThan nat_neq_iff)
+qed
+
+corollary more_choices_matched:
+assumes "matching A M" "M \<subseteq> {<n}" "M \<noteq> {<n}"
+and "preferred A a \<subseteq> match A ` M" and "a \<in> M"
+shows "A ! a + 1 < n"
+using more_choices[OF assms(1-4)] \<open>a \<in> M\<close> \<open>M \<subseteq> {<n}\<close> atLeastLessThan_iff by blast
+
+lemma atmost1_final: assumes M: "M \<subseteq> {<n}" and inj: "inj_on (match A) M"
+and "\<forall>a<n. preferred A a \<subseteq> match A ` M"
+shows "\<exists>\<^sub>\<le>\<^sub>1 a. a < n \<and> a \<notin> M \<and> 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 \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> match A ` M"
+shows "(\<Sum>a<n. A!a) \<le> (n-1)^2"
+proof -
+  have M: "\<forall>a\<in>M. A!a + 1 < n" using more_choices_matched[OF assms(1-3)] assms(4)
+    \<open>M \<subseteq> {<n}\<close> atLeastLessThan_iff by blast
+  note Ainj = conj12[OF assms(1)[unfolded matching_def]]
+  show ?thesis
+  proof (cases "\<exists>a'<n. a' \<notin> M \<and> A!a' + 1 = n")
+    case True
+    then obtain a' where a': "a'<n" "a' \<notin> M" "A!a' + 1 = n" using \<open>M \<subseteq> {<n}\<close> \<open>M \<noteq> {<n}\<close> by blast
+    hence "\<forall>a<n. a \<noteq> a' \<longrightarrow> A!a \<le> 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 "\<forall>a'<n. a' \<notin> M \<longrightarrow> A ! a' + 1 < n"
+      by (metis Suc_eq_plus1 Suc_lessI wf_less_n[OF Ainj(1)])
+    with M have "\<forall>a<n. A ! a + 1 < n" by blast
+    hence "(\<Sum>a<n. A!a) \<le> n*(n-2)" using sum_bounded_above[of "{..<n}" "((!) A)" "n-2"] by fastforce
+    also have "\<dots> \<le> (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 \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> match A ` M"
+shows "(\<Sum>a<n. A!a) + card M  < n^2 - n + 1"
+proof -
+  have 1: "M \<subset> {<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} \<le> n^2 + 1 - 2*n"
+    using sumA_UB[OF assms(1-4)]  by (simp add: power2_eq_square algebra_simps)
+  have 4: "2*n \<le> 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 "(\<Sum>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 \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> match A ` M" "a \<notin> M"
+shows "var A (M \<union> {a}) < var A M"
+proof -
+  have 2: "M \<subset> {<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} \<le> n^2 + 1 - 2*n"
+    using sumA_UB[OF assms(1-4)]  by (simp add: power2_eq_square algebra_simps)
+  have 5: "2*n \<le> 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: "(\<Sum>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 \<open>a \<notin> M\<close> finite_subset[OF assms(2)] by(simp)
+qed
+
+lemma var_next:
+assumes"matching A M" "M \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> 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 "\<dots> = n^2 - n + 1 - (1 + (\<Sum>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 "\<dots> < n^2 - n + 1 - ((\<Sum>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
+
+
+text \<open>The following two predicates express the same property:
+if \<open>a\<close> prefers \<open>b\<close> over \<open>a\<close>'s current match,
+then \<open>b\<close> is matched with an \<open>a'\<close> that \<open>b\<close> prefers to \<open>a\<close>.\<close>
+
+definition pref_match where
+"pref_match A M = (\<forall>a<n. \<forall>b<n. P\<^sub>a!a \<turnstile> b < match A a \<longrightarrow> (\<exists>a'\<in>M. b = match A a' \<and> P\<^sub>b ! b \<turnstile> a' < a))"
+
+definition pref_match' where
+"pref_match' A M = (\<forall>a<n. \<forall>b \<in> preferred A a. \<exists>a'\<in>M. b = match A a' \<and> P\<^sub>b ! b \<turnstile> a' < a)"
+
+lemma pref_match'_iff: "wf A \<Longrightarrow> 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\<^sub>a_set atLeast0LessThan order.strict_trans index_first lessThan_iff linorder_neqE_nat nth_index)
+  by (smt (verit, best) P\<^sub>a_set atLeast0LessThan card_atLeastLessThan card_distinct diff_zero in_mono index_nth_id lessThan_iff less_trans nth_mem)
+
+definition opti\<^sub>a where
+"opti\<^sub>a A = (\<nexists>A'. matching A' {<n} \<and> stable A' {<n} \<and>
+                (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match A a))"
+
+definition pessi\<^sub>b where
+"pessi\<^sub>b A = (\<nexists>A'. matching A' {<n} \<and> stable A' {<n} \<and>
+                 (\<exists>a<n. \<exists>a'<n. match A a = match A' a' \<and> P\<^sub>b ! match A a \<turnstile> a < a'))"
+
+lemma opti\<^sub>a_pessi\<^sub>b: assumes "opti\<^sub>a A" shows "pessi\<^sub>b A"
+unfolding pessi\<^sub>b_def
+proof (safe, goal_cases)
+  case (1 A' a a')
+  have "\<not> P\<^sub>a!a \<turnstile>  match A a <  match A' a" using 1
+    by (metis atLeast0LessThan blocks_def lessThan_iff prefers_asym stable_def)
+  with 1 \<open>opti\<^sub>a A\<close> show ?case using P\<^sub>a_set match_less_n opti\<^sub>a_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 opti\<^sub>a_inv:
+assumes A: "wf A" and a: "a < n" and a': "a' < n" and same_match: "match A a' = match A a"
+and pref: "P\<^sub>b ! match A a' \<turnstile> a' < a" and "opti\<^sub>a A"
+shows "opti\<^sub>a (A[a := A ! a + 1])"
+proof (unfold opti\<^sub>a_def matching_def, rule notI, elim exE conjE)
+  note opti\<^sub>a = \<open>opti\<^sub>a A\<close>[unfolded opti\<^sub>a_def matching_def]
+  let ?A = "A[a := A ! a + 1]"
+  fix A' a''
+  assume "a'' < n" and A': "length A' = n" "set A' \<subseteq> {<n}" "stable A' {<n}" "inj_on (match A') {<n}"
+  and pref_a'': "P\<^sub>a ! a'' \<turnstile> 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\<^sub>a ! a \<turnstile> match A' a < match A a \<or> match A' a = match A a"
+      apply(auto simp: prefers_def match_def)
+      by (smt (verit) P\<^sub>a_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\<^sub>a ! a \<turnstile> match A' a < match A a " thus False using opti\<^sub>a A' \<open>a < n\<close> by(fastforce) 
+    next
+      assume "match A' a = match A a"
+      have "a \<noteq> a'" using pref a' by(auto simp: prefers_def)
+      hence "blocks A' a' a" using opti\<^sub>a pref A' same_match \<open>match A' a = match A a\<close> a a'
+        unfolding blocks_def
+        by (metis P\<^sub>a_set atLeast0LessThan match_less_n inj_onD lessThan_iff linorder_neqE_nat nth_index prefers_def)
+      thus False using a a' \<open>a \<noteq> a'\<close> A'(3) by (metis stable_def atLeastLessThan_iff zero_le)
+    qed
+  next
+    assume "a'' \<noteq> a" thus False using opti\<^sub>a A' pref_a'' \<open>a'' < n\<close> by(metis match_def nth_list_update_neq)
+  qed
+qed
+
+lemma pref_match_stable:
+  "\<lbrakk> matching A {<n}; pref_match A {<n} \<rbrakk> \<Longrightarrow> stable A {<n}"
+unfolding pref_match_def stable_def blocks_def matching_def
+by (metis atLeast0LessThan match_less_n inj_onD lessThan_iff prefers_asym)
+
+definition invAM where
+[simp]: "invAM A M = (matching A M \<and> M \<subseteq> {<n} \<and> pref_match A M \<and> opti\<^sub>a A)"
+
+lemma invAM_match:
+  "\<lbrakk> invAM A M;  a < n \<and> a \<notin> M;  match A a \<notin> match A ` M \<rbrakk> \<Longrightarrow> invAM A (M \<union> {a})"
+by(simp add: pref_match_def)
+
+lemma invAM_swap:
+assumes "invAM A M"
+assumes a: "a < n \<and> a \<notin> M" and a': "a' \<in> M \<and> match A a' = match A a" and pref: "P\<^sub>b ! match A a' \<turnstile> a < a'"
+shows "invAM (A[a' := A!a'+1]) (M - {a'} \<union> {a})"
+proof -
+  have A: "wf A" and M : "M \<subseteq> {<n}" and inj: "inj_on (match A) M" and pref_match: "pref_match A M"
+  and "opti\<^sub>a A" by(insert \<open>invAM A M\<close>) (auto)
+  have "M \<noteq> {<n}" "a' < n" "a \<noteq> 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'} \<union> {a}"
+  have neq_a': "\<forall>x. x \<in> ?M \<longrightarrow> a' \<noteq> x" using \<open>a \<noteq> a'\<close> by blast
+  have \<open>set ?A \<subseteq> {<n}\<close>
+    apply(rule set_update_subsetI[OF A[THEN conjunct2]])
+    using more_choices[OF _ M \<open>M \<noteq> {<n}\<close>] 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 \<open>a' < n\<close>
+    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 "opti\<^sub>a ?A" using opti\<^sub>a_inv[OF A \<open>a' < n\<close> _ _ _ \<open>opti\<^sub>a A\<close>] a a'[THEN conjunct2] pref by auto
+  ultimately show ?thesis using a a' M pref_match'_iff by auto
+qed
+
+lemma invAM_next:
+assumes "invAM A M"
+assumes a: "a < n \<and> a \<notin> M" and a': "a' \<in> M \<and> match A a' = match A a" and pref: "\<not> P\<^sub>b ! match A a' \<turnstile> a < a'"
+shows "invAM (A[a := A!a + 1]) M"
+proof -
+  have A: "wf A" and M : "M \<subseteq> {<n}" and inj: "inj_on (match A) M" and pref_match: "pref_match A M"
+  and opti\<^sub>a: "opti\<^sub>a A" and "a' < n"
+    by(insert \<open>invAM A M\<close> a') (auto)
+  hence pref': "P\<^sub>b ! match A a' \<turnstile> a' < a"
+    using pref a a' P\<^sub>b_set unfolding prefers_def
+    by (metis match_def match_less_n index_eq_index_conv linorder_less_linear subsetD)
+  have "M \<noteq> {<n}" using a by fastforce
+  have neq_a: "\<forall>x. x\<in> M \<longrightarrow> a \<noteq> 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 "\<forall>a<n. preferred A a \<subseteq> match A ` M" unfolding pref_match'_def by blast
+  hence "A!a + 1 < n"
+    using more_choices[OF _ M \<open>M \<noteq> {<n}\<close>] 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 \<open>A!a + 1 < n\<close> 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  "opti\<^sub>a ?A" using opti\<^sub>a_inv[OF A conjunct1[OF a] \<open>a' < n\<close> conjunct2[OF a'] pref' opti\<^sub>a] .
+  ultimately show ?thesis using M by (simp add: pref_match'_iff)
+qed
+
+
+subsection \<open>Algorithm 1\<close>
+
+lemma Gale_Shapley1: "VARS M A a a'
+ [M = {} \<and> A = replicate n 0]
+ WHILE M \<noteq> {<n}
+ INV { invAM A M }
+ VAR {var A M}
+ DO a := (SOME a. a < n \<and> a \<notin> M);
+  IF match A a \<notin> match A ` M
+  THEN M := M \<union> {a}
+  ELSE a' := (SOME a'. a' \<in> M \<and> match A a' = match A a);
+       IF P\<^sub>b ! match A a' \<turnstile> a < a'
+       THEN A[a'] := A!a'+1; M := M - {a'} \<union> {a}
+       ELSE A[a] := A!a+1
+       FI
+  FI 
+ OD
+ [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case
+   by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_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 \<subseteq> {<n}" "M \<noteq> {<n}"
+    and pref_match: "pref_match A M" and "opti\<^sub>a A" and v: "var A M = v" by auto
+  note Ainj = conj12[OF m[unfolded matching_def]]
+  note pref_match' = pref_match[THEN pref_match'_iff[OF Ainj(1), THEN iffD2]]
+  hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` M" unfolding pref_match'_def by blast
+  define a where "a = (SOME a. a < n \<and> a \<notin> M)"
+  have a: "a < n \<and> a \<notin> 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 \<and> a \<notin> M))") unfolding a_def[symmetric]
+  proof -
+    show "?P a" (is "(?not_matched \<longrightarrow> ?THEN) \<and> (\<not> ?not_matched \<longrightarrow> ?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 \<open>?not_matched\<close>] .
+
+        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> ?not_matched"
+      define a' where "a' = (SOME a'.  a' \<in> M \<and> match A a' = match A a)"
+      have a': "a' \<in> M \<and> match A a' = match A a" unfolding a'_def using matched
+        by (smt (verit) image_iff someI_ex)
+      hence "a' < n" "a \<noteq> a'" using a M atLeast0LessThan by auto
+      show ?ELSE (is "?P((SOME a'. a' \<in> M \<and> match A a' = match A a))") unfolding a'_def[symmetric]
+      proof -
+        show "?P a'" (is "(?pref \<longrightarrow> ?THEN) \<and> (\<not> ?pref \<longrightarrow> ?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' \<open>?pref\<close>])
+
+            case 2
+            have "card(M - {a'} \<union> {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 \<open>a' < n\<close>] var0_next[OF Ainj(1) M \<open>a' < n\<close>]
+              by simp
+          qed
+        next
+          assume "\<not> ?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' \<open>\<not> ?pref\<close>] .
+
+            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 \<open>Proof also works for @{const var0} instead of @{const var}.\<close>
+
+
+subsection \<open>Algorithm 2: List of unmatched As\<close>
+
+abbreviation invas where
+"invas as == (set as \<subseteq> {<n} \<and> distinct as)"
+
+lemma Gale_Shapley2: "VARS A a a' as
+ [as = [0..<n] \<and> A = replicate n 0]
+ WHILE as \<noteq> []
+ INV { invAM A ({<n} - set as) \<and> invas as}
+ VAR {var A ({<n} - set as)}
+ DO a := hd as;
+  IF match A a \<notin> match A ` ({<n} - set as)
+  THEN as := tl as
+  ELSE a' := (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A a);
+       IF P\<^sub>b ! match A a' \<turnstile> a < a'
+       THEN A[a'] := A!a'+1; as := a' # tl as
+       ELSE A[a] := A!a+1
+       FI
+  FI 
+ OD
+ [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case
+   by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_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 A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M \<subseteq> {<n}"
+    and pref_match: "pref_match A ?M" and "opti\<^sub>a A" and "as \<noteq> []" and v: "var A ?M = v"
+    and as: "invas as" using 2 by auto
+  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
+  hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M" unfolding pref_match'_def by blast
+  from \<open>as \<noteq> []\<close> obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv)
+  have set_as: "?M \<union> {a} = {<n} - set as'" using as aseq by force
+  have a: "a < n \<and> a \<notin> ?M" using as unfolding aseq by (simp)
+  show ?case
+  proof (simp only: aseq list.sel, goal_cases)
+    case 1 show ?case (is "(?not_matched \<longrightarrow> ?THEN) \<and> (\<not> ?not_matched \<longrightarrow> ?ELSE)")
+    proof (rule; rule)
+      assume ?not_matched
+      then have nm: "match A a \<notin> 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 \<open>invAM A ?M\<close> 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> ?not_matched"
+      define a' where "a' = (SOME a'.  a' \<in> ?M \<and> match A a' = match A a)"
+      have a': "a' \<in> ?M \<and> match A a' = match A a" unfolding a'_def aseq using matched
+        by (smt (verit) image_iff someI_ex)
+      hence "a' < n" "a \<noteq> a'" using a M atLeast0LessThan by auto
+      show ?ELSE unfolding aseq[symmetric] a'_def[symmetric]
+      proof (goal_cases)
+        case 1
+        show ?case (is "(?pref \<longrightarrow> ?THEN) \<and> (\<not> ?pref \<longrightarrow> ?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'} \<union> {a} = {<n} - set (a' # as')" using a a' as aseq by auto
+            case 1 show ?case using invAM_swap[OF \<open>invAM A ?M\<close> a a' \<open>?pref\<close>] 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'] \<open>a' < n\<close> a atLeast0LessThan
+              by (metis Suc_eq_plus1 lessThan_iff var_def)
+          qed
+        next
+          assume "\<not> ?pref"
+          show ?ELSE
+          proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
+            case 1 show ?case using invAM_next[OF \<open>invAM A ?M\<close> a a' \<open>\<not> ?pref\<close>] 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
+
+
+abbreviation invAB :: "nat list \<Rightarrow> (nat \<Rightarrow> nat option) \<Rightarrow> nat set \<Rightarrow> bool" where
+"invAB A B M == (ran B = M \<and> (\<forall>b a. B b = Some a \<longrightarrow> match A a = b))"
+
+lemma invAB_swap:
+assumes invAB: "invAB A B M"
+assumes a: "a < n \<and> a \<notin> M" and a': "a' \<in> M \<and> 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'} \<union> {a})"
+proof -
+  have "\<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a'\<noteq> x" using invAB a' by blast
+  moreover have "a \<noteq> a'" using a a' by auto 
+  ultimately show ?thesis using assms by(simp add: ran_map_upd_Some match_def)
+qed
+
+
+subsection \<open>Algorithm 3: Record matching of Bs to As\<close>
+
+lemma Gale_Shapley3: "VARS A B a a' as b
+ [as = [0..<n] \<and> A = replicate n 0 \<and> B = (\<lambda>_. None)]
+ WHILE as \<noteq> []
+ INV { invAM A ({<n} - set as) \<and> invAB A B ({<n} - set as) \<and> 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 P\<^sub>b ! match A a' \<turnstile> 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} \<and> stable A {<n} \<and> opti\<^sub>a A]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case
+    by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_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 \<subseteq> {<n}"
+    and pref_match: "pref_match A ?M" and "opti\<^sub>a A" and "as \<noteq> []" and v: "var A ?M = v"
+    and as: "invas as" and invAB: "invAB A B ?M" using 2 by auto
+  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
+  hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M" unfolding pref_match'_def by blast
+  from \<open>as \<noteq> []\<close> obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv)
+  have set_as: "?M \<union> {a} = {<n} - set as'" using as aseq by force
+  have a: "a < n \<and> a \<notin> ?M" using as unfolding aseq by (simp)
+  show ?case
+  proof (simp only: aseq list.sel, goal_cases)
+    case 1 show ?case (is "(?not_matched \<longrightarrow> ?THEN) \<and> (\<not> ?not_matched \<longrightarrow> ?ELSE)")
+    proof (rule; rule)
+      assume ?not_matched
+      then have nm: "match A a \<notin> 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 \<open>?not_matched\<close> 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> ?not_matched"
+      then obtain a' where a'eq: "B(match A a) = Some a'" by auto
+      have a': "a' \<in> ?M \<and> match A a' = match A a" unfolding aseq using a'eq invAB
+        by (metis ranI aseq)
+      hence "a' < n" "a \<noteq> 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 \<longrightarrow> ?THEN) \<and> (\<not> ?pref \<longrightarrow> ?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'} \<union> {a} = {<n} - set (a' # as')" using a a' as aseq by auto
+            have a'neq: "\<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a'\<noteq> 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' \<open>?pref\<close>] 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'] \<open>a' < n\<close> a atLeast0LessThan
+              by (metis Suc_eq_plus1 lessThan_iff var_def)
+          qed
+        next
+          assume "\<not> ?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' \<open>\<not> ?pref\<close>] 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
+
+(* 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 \<Rightarrow> nat list \<Rightarrow> bool list \<Rightarrow> nat set \<Rightarrow> bool" where
+"invAB' A B M M' == (length B = n \<and> length M = n \<and> M' = nth B ` {b. b < n \<and> M!b}
+ \<and> (\<forall>b<n. M!b \<longrightarrow> B!b < n \<and> match A (B!b) = b))"
+
+lemma Gale_Shapley4': "VARS A B M a a' as b
+ [as = [0..<n] \<and> A = replicate n 0 \<and> B = replicate n 0 \<and> M = replicate n False]
+ WHILE as \<noteq> []
+ INV { invAM A ({<n} - set as) \<and> invAB' A B M ({<n} - set as) \<and> invas as}
+ VAR {var A ({<n} - set as)}
+ DO a := hd as; b := match A a;
+  IF \<not> (M ! b)
+  THEN M[b] := True; B[b] := a; as := tl as
+  ELSE a' := B ! b;
+       IF P\<^sub>b ! match A a' \<turnstile> 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 \<and> inj_on (match A) {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case
+   by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_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 \<subseteq> {<n}"
+    and pref_match: "pref_match A ?M" and "opti\<^sub>a A" and notall: "as \<noteq> []" and v: "var A ?M = v"
+    and as: "invas as" and invAB: "invAB' A B M ?M" using 2 by auto
+  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
+  hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M" unfolding pref_match'_def by blast
+  from notall obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv)
+  have set_as: "?M \<union> {a} = {<n} - set as'" using as aseq by force
+  have a: "a < n \<and> a \<notin> ?M" using as unfolding aseq by (simp)
+  show ?case
+  proof (simp only: aseq list.sel, goal_cases)
+    case 1 show ?case (is "(?not_matched \<longrightarrow> ?THEN) \<and> (\<not> ?not_matched \<longrightarrow> ?ELSE)")
+    proof (rule; rule)
+      assume ?not_matched
+      then have nm: "match A a \<notin> 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 \<open>?not_matched\<close> 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> ?not_matched"
+      hence "match A a \<in> 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 m M, of a] a pref_match1
+        using aseq atLeast0LessThan by auto
+      let ?a = "B ! match A a"
+      have a': "?a \<in> ?M \<and> match A ?a = match A a"
+        using invAB match_less_n[OF A] matched a by blast
+      hence "?a < n" "a \<noteq> ?a" using a by auto
+      show ?ELSE unfolding aseq option.sel
+      proof (goal_cases)
+        case 1
+        show ?case (is "(?pref \<longrightarrow> ?THEN) \<and> (\<not> ?pref \<longrightarrow> ?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} \<union> {a} = {<n} - set (?a # as')" using a a' as aseq by auto
+            have a'neq: "\<forall>b<n. b \<noteq> match A a \<longrightarrow> M!b \<longrightarrow> ?a \<noteq> 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 * \<open>a \<noteq> ?a\<close> 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' \<open>?pref\<close>] 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] \<open>?a < n\<close> a atLeast0LessThan
+              by (metis Suc_eq_plus1 lessThan_iff var_def)
+          qed
+        next
+          assume "\<not> ?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 \<open>a \<noteq> ?a\<close>
+              by (metis match_def nth_list_update_neq)
+            thus ?case using invAM_next[OF invAM a a' \<open>\<not> ?pref\<close>] 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
+
+(* end unused *)
+
+
+subsection \<open>Algorithm 4: remove list of unmatched As\<close>
+
+lemma Gale_Shapley4:
+"VARS A B ai a a'
+ [ai = 0 \<and> A = replicate n 0 \<and> B = (\<lambda>_. None)]
+ WHILE ai < n
+ INV { invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n }
+ VAR {z = n - ai}
+ DO a := ai;
+  WHILE B (match A a) \<noteq> None
+  INV { invAM A ({<ai+1} - {a}) \<and> invAB A B ({<ai+1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n-ai }
+  VAR {var A {<ai}}
+  DO a' := the(B (match A a));
+     IF P\<^sub>b ! match A a' \<turnstile> 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} \<and> stable A {<n} \<and> opti\<^sub>a A]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case  (* outer invar holds initially *)
+   by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def)[]
+next
+  case 2 (* outer invar and b ibplies 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 ibplies 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}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))"
+      by (metis "*" Diff_idemp inj_on_insert)
+    have nm: "match A a \<notin> 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 \<subseteq> {<n}"
+    and pref_match: "pref_match A ?M" and matched: "B(match A a) \<noteq> None" and "a \<le> ai"
+    and v: "var A ?M = v" and as: "a \<le> ai \<and> ai < n" and invAB: "invAB A B ?M" using 3 by auto
+  note invar = 3[THEN conjunct1,THEN conjunct1]
+  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
+  hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M" unfolding pref_match'_def by blast
+  from matched obtain a' where a'eq: "B(match A a) = Some a'" by auto
+  have a': "a' \<in> ?M \<and> match A a' = match A a" using a'eq invAB by (metis ranI)
+  have a: "a < n \<and> a \<notin> ?M" using invar by auto
+  have "?M \<noteq> {<n}" and "a' < n" using M a a' atLeast0LessThan by auto
+  have card: "card {<ai} = card ?M" using \<open>a \<le> ai\<close> by simp
+  show ?case unfolding a'eq option.sel
+  proof (goal_cases)
+    case 1
+    show ?case (is "(?unstab \<longrightarrow> ?THEN) \<and> (\<not> ?unstab \<longrightarrow> ?ELSE)")
+    proof (rule; rule)
+      assume ?unstab
+      have *: "{<ai + 1} - {a} - {a'} \<union> {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 \<mapsto> 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' \<open>?unstab\<close>] invAB' invar a' unfolding * by (simp)
+      next
+        case 2
+        show ?case using v var_next[OF m M \<open>?M \<noteq> {<n}\<close> pref_match1 \<open>a' < n\<close>] card
+          by (metis var_def Suc_eq_plus1 psubset_eq)
+      qed
+    next
+      assume "\<not> ?unstab"
+      show ?ELSE
+      proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
+        have *: "\<forall>b a'. B b = Some a' \<longrightarrow> a \<noteq> a'" by (metis invAB ranI a) 
+        case 1 show ?case using invAM_next[OF invAM a a' \<open>\<not> ?unstab\<close>] invar * by (simp add: match_def)
+      next
+        case 2
+        show ?case using v var_next[OF m M \<open>?M \<noteq> {<n}\<close> pref_match1, of a] a card
+          by (metis Suc_eq_plus1 var_def)
+      qed
+    qed
+  qed
+qed
+
+definition "\<alpha> B M = (\<lambda>b. if b < n \<and> M!b then Some(B!b) else None)"
+
+lemma \<alpha>_Some[simp]: "\<alpha> B M b = Some a \<longleftrightarrow> b < n \<and> M!b \<and> a = B!b"
+by(auto simp add: \<alpha>_def)
+
+lemma \<alpha>update1: "\<lbrakk> \<not> M ! b; b < length B; b < length M; n = length M \<rbrakk>
+ \<Longrightarrow> ran(\<alpha> (B[b := a]) (M[b := True])) = ran(\<alpha> B M) \<union> {a}"
+by(force simp add: \<alpha>_def ran_def nth_list_update)
+
+lemma \<alpha>update2: "\<lbrakk> M!b; b < length B; b < length M; length M = n \<rbrakk>
+ \<Longrightarrow> \<alpha> (B[b := a]) M = (\<alpha> B M)(b := Some a)"
+by(force simp add: \<alpha>_def nth_list_update)
+
+ 
+abbreviation invAB2 :: "nat list \<Rightarrow> nat list \<Rightarrow> bool list \<Rightarrow> nat set \<Rightarrow> bool" where
+"invAB2 A B M M' == (invAB A (\<alpha> B M) M' \<and> (length B = n \<and> length M = n))"
+
+definition invar1 where
+[simp]: "invar1 A B M ai = (invAM A {<ai} \<and> invAB2 A B M {<ai} \<and> ai \<le> n)"
+
+definition invar2 where
+[simp]: "invar2 A B M ai a \<equiv> (invAM A ({<ai+1} - {a}) \<and> invAB2 A B M ({<ai+1} - {a}) \<and> a \<le> ai \<and> ai < n)"
+
+
+subsection \<open>Algorithm 5: Data refinement of \<open>B\<close>\<close>
+
+lemma Gale_Shapley5:
+"VARS A B M ai a a'
+ [ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
+ WHILE ai < n
+ INV { invar1 A B M ai }
+ VAR { z = n - ai}
+ DO a := ai;
+  WHILE M ! match A a
+  INV { invar2 A B M ai a \<and> z = n-ai }
+  VAR {var A {<ai}}
+  DO a' := B ! match A a;
+     IF P\<^sub>b ! match A a' \<turnstile> 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; M[match A a] := True; ai := ai+1
+ OD
+ [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case  (* outer invar holds initially *)
+   by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
+next
+  case 2 (* outer invar and b ibplies 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 ibplies 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}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))"
+      by (metis "*" Diff_idemp inj_on_insert)
+    have nm: "match A a \<notin> 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: \<alpha>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 ibplies 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 M 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 \<subseteq> {<n}"
+    and pref_match: "pref_match A ?M" and matched: "M ! match A a"
+    and v: "var A {<ai} = v" and as: "a \<le> ai \<and> ai < n" and invAB: "invAB2 A B M ?M"
+    using 3 by auto
+  note invar = 3[THEN conjunct1, THEN conjunct1, unfolded invar2_def]
+  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
+  hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M" unfolding pref_match'_def by blast
+  let ?a = "B ! match A a"
+  have a: "a < n \<and> a \<notin> ?M" using invar by auto
+  have a': "?a \<in> ?M \<and> match A ?a = match A a"
+    using invAB match_less_n[OF A] a matched by (metis \<alpha>_Some ranI)
+  have "?M \<noteq> {<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} \<union> {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 (\<alpha> B M) (dom (\<alpha> B M))" by (metis (mono_tags) domD inj_onI invAB)
+      have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (\<alpha> (B[match A a := a]) M) ({<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:\<alpha>update2)
+      show ?case using invAM_swap[OF invAM a a' unstab] invAB' invar a'
+        unfolding * by (simp add: insert_absorb \<alpha>update2)
+
+      case 2
+      show ?case using v var_next[OF m M \<open>?M \<noteq> {<n}\<close> pref_match1 \<open>?a < n\<close>] card
+        by (metis var_def Suc_eq_plus1)
+    next
+      case stab: 3
+      have *: "\<forall>b. b < n \<and> M!b \<longrightarrow> a \<noteq> B!b" by (metis invAB ranI \<alpha>_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 \<open>?M \<noteq> {<n}\<close> pref_match1, of a] a card
+        by (metis Suc_eq_plus1 var_def)
+    qed
+  qed
+qed
+
+lemma inner_to_outer:
+assumes inv: "invar2 A B M ai a \<and> b = match A a" and not_b: "\<not> M ! b"
+shows "invar1 A (B[b := a]) (M[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}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))"
+    by (metis "*" Diff_idemp inj_on_insert)
+  have nm: "match A a \<notin> 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: \<alpha>update1 insert_absorb nth_list_update)
+qed
+
+lemma inner_pres:
+assumes R: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R ! b ! a1 < R ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2" and
+  inv: "invar2 A B M ai a" and m: "M ! b" and v: "var A {<ai} = v"
+  and after: "A1 = A[B ! b := A ! (B ! b) + 1]" "A2 = A[a := A ! a + 1]"
+    "a' = B!b" "r = R ! match A a'" "b = match A a"
+shows "(r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b:=a]) M ai a' \<and> var A1 {<ai} < v) \<and>
+  (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> 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 \<subseteq> {<n}" and invAM: "invAM A ?M" and invAB: "invAB A (\<alpha> B M) ?M"
+    and mat: "matching A ?M" and pref_match: "pref_match A ?M"
+    and as: "a \<le> ai \<and> ai < n" using inv' by auto
+  note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
+  hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M" unfolding pref_match'_def by blast
+  let ?a = "B ! match A a"
+  have a: "a < n \<and> a \<notin> ?M" using inv by auto
+  have a': "?a \<in> ?M \<and> match A ?a = match A a"
+    using invAB match_less_n[OF A] a m inv by (metis \<alpha>_Some ranI \<open>b = _\<close>)
+  have "?M \<noteq> {<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} \<union> {a} = {<ai + 1} - {?a}" using inv a' by auto
+    case 1
+    hence unstab: "P\<^sub>b ! match A a' \<turnstile> a < a'"
+      using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b R by (simp)
+    have inj_dom: "inj_on (\<alpha> B M) (dom (\<alpha> B M))" by (metis (mono_tags) domD inj_onI invAB)
+    have invAB': "invAB A1 (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {?a})"
+      using invAB_swap[OF invAB a a' inj_dom] * match_less_n[OF A] a m
+      by (simp add: \<alpha>update2 inv')
+    show ?case using invAM_swap[OF invAM a a'] unstab invAB' inv a'
+      unfolding * by (simp add: insert_absorb \<alpha>update2)
+  next
+    case 2
+      show ?case using v var_next[OF mat M \<open>?M \<noteq> {<n}\<close> pref_match1 \<open>?a < n\<close>] card assms(5,9)
+        by (metis Suc_eq_plus1 var_def)
+  next
+    have *: "\<forall>b. b < n \<and> M!b \<longrightarrow> a \<noteq> B!b" by (metis invAB ranI \<alpha>_Some a)
+    case 3
+    hence unstab: "\<not> P\<^sub>b ! match A a' \<turnstile> a < a'"
+      using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b
+      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 \<open>?M \<noteq> {<n}\<close> pref_match1, of a] a card assms(6)
+        by (metis Suc_eq_plus1 var_def)
+  qed
+qed
+
+
+subsection \<open>Algorithm 6: replace \<open>P\<^sub>b\<close> by ranking \<open>R\<close>\<close>
+
+lemma Gale_Shapley6:
+assumes "R = map ranking P\<^sub>b"
+shows
+"VARS A B M ai a a' b r
+ [ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
+ WHILE ai < n
+ INV { invar1 A B M ai }
+ VAR {z = n - ai}
+ DO a := ai; b := match A a;
+  WHILE M ! b
+  INV { invar2 A B M ai a \<and> b = match A a \<and> 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; M[b] := True; ai := ai+1
+ OD
+ [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case  (* outer invar holds initially *)
+   by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
+next
+  case 2 (* outer invar and b ibplies inner invar *)
+  thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
+next
+  case 3 (* preservation of inner invar *)
+  have R: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R ! b ! a1 < R ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2"
+    by (simp add: P\<^sub>b_set \<open>R = _\<close> length_P\<^sub>b 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 ibplies 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 ibplies post *)
+  thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less)
+qed
+
+end
+
+
+subsection \<open>Functional implementation\<close>
+
+definition
+"gs_inner P\<^sub>a R M =
+  while (\<lambda>(A,B,a,b). M!b)
+    (\<lambda>(A,B,a,b).
+      let a' = B ! b;
+          r = R ! (P\<^sub>a ! 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\<^sub>a ! a ! (A ! a)))"
+
+definition
+"gs n P\<^sub>a R =
+  while (\<lambda>(A,B,M,ai). ai < n)
+   (\<lambda>(A,B,M,ai).
+     let (A,B,a,b) = gs_inner P\<^sub>a R M (A, B, ai, P\<^sub>a ! ai ! (A ! ai))
+     in (A, B[b:=a], M[b:=True], ai+1))
+  (replicate n 0, replicate n 0, replicate n False,0)"
+
+context Pref
+begin
+
+lemma gs_inner:
+assumes "R = map ranking P\<^sub>b"
+assumes "invar2 A B M ai a" "b = match A a"
+shows "gs_inner P\<^sub>a R M (A, B, a, b) = (A',B',a',b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai+1)"
+unfolding gs_inner_def
+proof(rule while_rule2[where P = "\<lambda>(A,B,a,b). invar2 A B M ai a \<and> b = match A a"
+ and r = "measure (%(A, B, a, b). Pref.var P\<^sub>a 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: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R ! b ! a1 < R ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2"
+    by (simp add: P\<^sub>b_set \<open>R = _\<close> length_P\<^sub>b 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 M 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 M 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 P\<^sub>b"
+shows "gs n P\<^sub>a R = (A,BMai) \<longrightarrow> matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A"
+unfolding gs_def
+proof(rule while_rule2[where P = "\<lambda>(A,B,M,ai). invar1 A B M ai"
+  and r = "measure(\<lambda>(A,B,M,ai). n - ai)"], goal_cases)
+  case 1 show ?case
+   by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
+next
+  case (2 s)
+  obtain A B M ai where s: "s =  (A, B, M, ai)"
+    using prod_cases4 by blast
+  have 1: "invar2 A B M ai ai" using 2 s
+    by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
+  show ?case using 2 s gs_inner[OF \<open>R = _ \<close> 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
+
+end
+
+
+subsection \<open>Executable functional Code\<close>
+
+definition
+"Gale_Shapley P\<^sub>a P\<^sub>b = (if Pref P\<^sub>a P\<^sub>b then Some (fst (gs (length P\<^sub>a) P\<^sub>a (map ranking P\<^sub>b))) else None)"
+
+theorem gs: "\<lbrakk> Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a \<rbrakk> \<Longrightarrow>
+ \<exists>A. Gale_Shapley P\<^sub>a P\<^sub>b = Some(A) \<and> Pref.matching P\<^sub>a A {<n} \<and>
+   Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A"
+unfolding Gale_Shapley_def using Pref.gs
+by (metis fst_conv surj_pair)
+
+declare Pref_def [code]
+
+text \<open>Two examples from Gusfield and Irving:\<close>
+
+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_Shapley
+  [[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
\ No newline at end of file
diff --git a/thys/Gale_Shapley/Gale_Shapley2.thy b/thys/Gale_Shapley/Gale_Shapley2.thy
new file mode 100644
--- /dev/null
+++ b/thys/Gale_Shapley/Gale_Shapley2.thy
@@ -0,0 +1,253 @@
+(*
+Stepwise refinement of the Gale-Shapley algorithm down to executable code.
+
+Part 2: Refinement from lists to arrays,
+        resulting in a linear (in the input size, which is n^2) time algorithm
+
+Author: Tobias Nipkow
+*)
+
+theory Gale_Shapley2
+imports Gale_Shapley1 "Collections.Diff_Array"
+begin
+
+abbreviation "array \<equiv> new_array"
+notation array_get (infixl "!!" 100)
+notation array_set ("_[_ ::= _]" [1000,0,0] 900)
+abbreviation "list \<equiv> list_of_array"
+
+lemma list_array: "list (array x n) = replicate n x"
+by (simp add: new_array_def)
+
+lemma array_get: "a !! i = list a ! i"
+by (cases a) simp
+
+context Pref
+begin
+
+subsection \<open>Algorithm 7: Arrays\<close>
+
+definition "match_array A a = P\<^sub>a ! a ! (A !! a)"
+
+lemma match_array: "match_array A a = match (list A) a"
+by(cases A) (simp add: match_array_def match_def)
+
+lemmas array_abs = match_array array_list_of_set array_get
+
+lemma Gale_Shapley7:
+assumes "R = map ranking P\<^sub>b"
+shows
+"VARS A B M ai a a' b r
+ [ai = 0 \<and> A = array 0 n \<and> B = array 0 n \<and> M = array False n]
+ WHILE ai < n
+ INV { invar1 (list A) (list B) (list M) ai }
+ VAR {z = n - ai}
+ DO a := ai; b := match_array A a;
+  WHILE M !! b
+  INV { invar2 (list A) (list B) (list M) ai a \<and> b = match_array A a \<and> z = n-ai }
+  VAR {var (list A) {<ai}}
+  DO a' := B !! b; r := R ! match_array A a';
+     IF r ! a < r ! a'
+     THEN B := B[b ::= a]; A := A[a' ::= A !! a' + 1]; a := a'
+     ELSE A := A[a ::= A !! a + 1]
+     FI;
+     b := match_array A a
+  OD;
+  B := B[b ::= a]; M := M[b ::= True]; ai := ai+1
+ OD
+ [matching (list A) {<n} \<and> stable (list A) {<n} \<and> opti\<^sub>a (list A)]"
+proof (vcg_tc, goal_cases)
+  case 1 thus ?case  (* outer invar holds initially *)
+   by(auto simp:  pref_match_def P\<^sub>a_set card_distinct match_def list_array index_nth_id prefers_def opti\<^sub>a_def \<alpha>_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: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R ! b ! a1 < R ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2"
+    by (simp add: P\<^sub>b_set \<open>R = _\<close> length_P\<^sub>b 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
+      unfolding array_abs 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 unfolding array_abs by blast
+  next
+    case 2 thus ?case using 4 by auto
+  qed
+next
+  case 5 (* outer invar and not b ibplies post *)
+  thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less)
+qed
+
+end
+
+
+subsection \<open>Executable functional Code\<close>
+
+definition gs_inner where
+"gs_inner P\<^sub>a R M =
+  while (\<lambda>(A,B,a,b). M !! b)
+    (\<lambda>(A,B,a,b).
+      let a' = B !! b;
+          r = R !! (P\<^sub>a !! 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\<^sub>a !! a !! (A !! a)))"
+
+definition gs where
+"gs n P\<^sub>a R =
+  while (\<lambda>(A,B,M,ai). ai < n)
+   (\<lambda>(A,B,M,ai).
+     let (A,B,a,b) = gs_inner P\<^sub>a R M (A, B, ai, P\<^sub>a !! ai !! (A !! ai))
+     in (A, B[b ::= a], M[b::=True], ai+1))
+  (array 0 n, array 0 n, array False n, 0)"
+
+
+definition "pref_array = array_of_list o map array_of_list"
+
+lemma list_list_pref_array: "i < length Pa \<Longrightarrow> list (list (pref_array Pa) ! i) = Pa ! i"
+by(simp add: pref_array_def)
+
+fun rk_of_pref :: "nat \<Rightarrow> nat array \<Rightarrow> nat list \<Rightarrow> nat array" where
+"rk_of_pref r rs (n#ns) = (rk_of_pref (r+1) rs ns)[n ::= r]" |
+"rk_of_pref r rs [] = rs"
+
+definition rank_array1 :: "nat list \<Rightarrow> nat array" where
+"rank_array1 P = rk_of_pref 0 (array 0 (length P)) P"
+
+definition rank_array :: "nat list list \<Rightarrow> nat array array" where
+"rank_array = array_of_list o map rank_array1"
+
+lemma length_rk_of_pref[simp]: "array_length(rk_of_pref v vs P) = array_length vs"
+by(induction P arbitrary: v)(auto)
+
+lemma nth_rk_of_pref:
+ "\<lbrakk> length P \<le> array_length rs; i \<in> set P; distinct P; set P \<subseteq> {<array_length rs} \<rbrakk>
+ \<Longrightarrow> rk_of_pref r rs P !! i = index P i + r"
+by(induction P arbitrary: r i) (auto simp add: array_get_array_set_other)
+
+lemma rank_array1_iff_pref:  "\<lbrakk> set P = {<length P}; i < length P; j < length P \<rbrakk>
+ \<Longrightarrow> rank_array1 P !! i < rank_array1 P !! j \<longleftrightarrow> P \<turnstile> i < j"
+by(simp add: rank_array1_def prefers_def nth_rk_of_pref card_distinct)
+
+definition Gale_Shapley where
+"Gale_Shapley P\<^sub>a P\<^sub>b =
+  (if Pref P\<^sub>a P\<^sub>b
+   then Some (fst (gs (length P\<^sub>a) (pref_array P\<^sub>a) (rank_array P\<^sub>b)))
+   else None)"
+
+(*export_code Gale_Shapley_array in SML*)
+
+context Pref
+begin
+
+lemma gs_inner:
+assumes "R = rank_array P\<^sub>b"
+assumes "invar2 (list A) (list B) (list M) ai a" "b = match_array A a"
+shows "gs_inner (pref_array P\<^sub>a) R M (A, B, a, b) = (A',B',a',b')
+  \<longrightarrow> invar1 (list A') ((list B')[b' := a']) ((list M)[b' := True]) (ai+1)"
+unfolding gs_inner_def
+proof(rule while_rule2[where
+     P = "\<lambda>(A,B,a,b). invar2 (list A) (list B) (list M) ai a \<and> b = match_array A a"
+ and r = "measure (\<lambda>(A, B, a, b). Pref.var P\<^sub>a (list 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
+  show ?case
+  proof(rule, goal_cases)
+    case 1
+    have *: "a < n" using s inv(1)[unfolded invar2_def] by (auto)
+    hence 2: "list A ! a < n" using s inv(1)[unfolded invar2_def]
+      apply simp using "*" wf_less_n by presburger
+    hence "match (list A) a < n"
+      by (metis "*" P\<^sub>a_set atLeast0LessThan lessThan_iff match_def nth_mem)
+    from this have **: "list B ! match (list A) a < n" using s inv[unfolded invar2_def]
+      apply (simp add: array_abs ran_def) using atLeast0LessThan by blast
+    have R: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. map list (list R) ! b ! a1 < map list (list R) ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2"
+    using rank_array1_iff_pref by(simp add: \<open>R = _\<close> length_P\<^sub>b array_get P\<^sub>b_set rank_array_def)
+    have ***: "match (list A) (list B ! b) < length (list R)"  using s inv(1)[unfolded invar2_def]
+      using ** by(simp add: \<open>R = _\<close> rank_array_def match_array match_less_n length_P\<^sub>b)
+    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 "list A" "list B" "list M" ai a b]
+    unfolding invar2_def array_abs
+      list_list_pref_array[OF **[unfolded n_def]] list_list_pref_array[OF *[unfolded n_def]] nth_map[OF ***]
+    unfolding 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 "list A" "list B" "list M" ai a b]
+    unfolding invar2_def array_abs
+      list_list_pref_array[OF **[unfolded n_def]] list_list_pref_array[OF *[unfolded n_def]] nth_map[OF ***]
+    unfolding 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 array_abs]])
+  qed
+next
+  case 4
+  show ?case by simp
+qed
+
+lemma gs: assumes "R = rank_array P\<^sub>b"
+shows "gs n (pref_array P\<^sub>a) R = (A,B,M,ai) \<longrightarrow> matching (list A) {<n} \<and> stable (list A) {<n} \<and> opti\<^sub>a (list A)"
+unfolding gs_def
+proof(rule while_rule2[where P = "\<lambda>(A,B,M,ai). invar1 (list A) (list B) (list M) ai"
+  and r = "measure(\<lambda>(A,B,M,ai). n - ai)"], goal_cases)
+  case 1 show ?case
+   by(auto simp: pref_match_def P\<^sub>a_set card_distinct match_def list_array index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
+next
+  case (2 s)
+  obtain A B M ai where s: "s =  (A, B, M, ai)"
+    using prod_cases4 by blast
+  have 1: "invar2 (list A) (list B) (list M) ai ai" using 2 s
+    by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
+  hence "ai < n" by(simp)
+  show ?case using 2 s gs_inner[OF \<open>R = _ \<close> 1]
+    by (auto simp: array_abs match_def list_list_pref_array[OF \<open>ai < n\<close>[unfolded n_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
+
+end
+
+theorem gs: "\<lbrakk> Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a \<rbrakk> \<Longrightarrow>
+ \<exists>A. Gale_Shapley P\<^sub>a P\<^sub>b = Some A
+   \<and> Pref.matching P\<^sub>a (list A) {<n} \<and> Pref.stable P\<^sub>a P\<^sub>b (list A) {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b (list A)"
+unfolding Gale_Shapley_def using Pref.gs
+by (metis fst_conv surj_pair)
+
+
+text \<open>Two examples from Gusfield and Irving:\<close>
+
+lemma "list_of_array (the (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]]))
+  = [0,1,0,1]"
+by eval
+
+lemma "list_of_array (the (Gale_Shapley
+  [[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]]))
+  = [0, 1, 0, 5, 0, 0, 0, 2]"
+by eval
+
+end
\ No newline at end of file
diff --git a/thys/Gale_Shapley/ROOT b/thys/Gale_Shapley/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Gale_Shapley/ROOT
@@ -0,0 +1,13 @@
+chapter AFP
+
+session Gale_Shapley (AFP) = HOL +
+  sessions
+    "HOL-Library"
+    "HOL-Hoare"
+    "List-Index"
+    Collections
+  theories [timeout = 600]
+    "Gale_Shapley2"
+  document_files
+    "root.tex"
+    "root.bib"
diff --git a/thys/Gale_Shapley/document/root.bib b/thys/Gale_Shapley/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Gale_Shapley/document/root.bib
@@ -0,0 +1,57 @@
+@article{Baker91,
+author = {Baker, Henry G.},
+title = {Shallow Binding Makes Functional Arrays Fast},
+year = {1991},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {26},
+number = {8},
+url = {https://doi.org/10.1145/122598.122614},
+journal = {SIGPLAN Not.},
+month = {aug},
+pages = {145-147},
+}
+
+@inproceedings{ConchonF07,
+  author    = {Sylvain Conchon and
+               Jean{-}Christophe Filli{\^{a}}tre},
+  editor    = {Claudio V. Russo and
+               Derek Dreyer},
+  title     = {A persistent union-find data structure},
+  booktitle = {Proceedings of the {ACM} Workshop on ML, 2007, Freiburg, Germany,
+               October 5, 2007},
+  pages     = {37--46},
+  publisher = {{ACM}},
+  year      = {2007},
+  url       = {https://doi.org/10.1145/1292535.1292541},
+}
+
+@article{GaleS62,
+  author    = {D. Gale and
+               L. S. Shapley},
+  title     = {College Admissions and the Stability of Marriage},
+  journal   = {Am. Math. Mon.},
+  volume    = {69},
+  number    = {1},
+  pages     = {9--15},
+  year      = {1962},
+}
+
+@book{GusfieldI89,
+  author    = {Dan Gusfield and
+               Robert W. Irving},
+  title     = {The Stable marriage problem - structure and algorithms},
+  series    = {Foundations of computing series},
+  publisher = {{MIT} Press},
+  year      = {1989}
+}
+
+@article{Collections-AFP,
+  author  = {Peter Lammich},
+  title   = {Collections Framework},
+  journal = {Archive of Formal Proofs},
+  month   = nov,
+  year    = 2009,
+  note    = {\url{https://isa-afp.org/entries/Collections.html},
+            Formal proof development},
+}
diff --git a/thys/Gale_Shapley/document/root.tex b/thys/Gale_Shapley/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Gale_Shapley/document/root.tex
@@ -0,0 +1,59 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+\usepackage{amssymb}
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Gale-Shapley Algorithm}
+\author{Tobias Nipkow}
+\maketitle
+
+\begin{abstract}
+  This is a stepwise refinement and proof of the Gale-Shapley stable
+  matching (or marriage) algorithm down to executable code. Both a
+  purely functional implementation based on lists and a
+  functional implementation based on efficient arrays (provided
+  by the Collections entry in the AFP) are developed.  The latter
+  implementation runs in time $O(n^2)$ where $n$ is the cardinality of
+  the two sets to be matched.
+\end{abstract}
+
+\section{Introduction}
+
+The Gale-Shapley algorithm \cite{GaleS62,GusfieldI89} for stable
+matchings (or marriages) matches two sets of the same cardinality $n$,
+where each element has a complete list of preferences (a linear order)
+of the elements of the other set.
+
+The refinement process is carried out largely on the level of a simple
+imperative language. In every refinement step the whole algorithm is
+stated and proved. Most of the proof is abstrtacted into general
+lemmas that are used in multiple proofs. Except for one bigger step,
+each algorithm proof is obtained from the previous one by incremental changes.
+In the end, two executable functional algorithms are obtained:
+a purely functional one based on lists and a functional one based on a
+persistent imperative implementation of arrays (provided by the AFP entry
+Collections Framework \cite{Collections-AFP} based on \cite{Baker91}
+(see also \cite{ConchonF07})).
+The latter algorithm has linear complexity, i.e. $O(n^2)$.
+
+We prove that each of the algorithm computes a stable matching that is
+optimal for one of the two sets.
+
+\newpage
+
+% include generated text of all theories
+\input{session}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,649 +1,650 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 CoSMed
 CoSMeDis
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
+Gale_Shapley
 GaleStewart_Games
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szpilrajn
 Szemeredi_Regularity
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weighted_Path_Order
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL