[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. [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 := B[match A a := a]; A := A[a' := A ! a' + 1]; a := a'  ELSE A := A[a := A ! a + 1] FI OD; B := B[match A a := a]; M := M[match A a := True]; ai := ai + 1 OD
[matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A]
[PROOF STEP]
proof (vcg_tc, goal_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>A B M ai a a'. ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar1 A B M ai
 2. \<And>z A B M ai a a'. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> z = n - ai
 3. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 4. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 5. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
ai_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (5 subgoals):
 1. \<And>A B M ai a a'. ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar1 A B M ai
 2. \<And>z A B M ai a a'. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> z = n - ai
 3. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 4. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 5. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ai_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (1 subgoal):
 1. invar1 A_ B_ M_ ai_
[PROOF STEP]
(* outer invar holds initially *)
[PROOF STATE]
proof (prove)
using this:
ai_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (1 subgoal):
 1. invar1 A_ B_ M_ ai_
[PROOF STEP]
by(auto simp: 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)
[PROOF STATE]
proof (state)
this:
invar1 A_ B_ M_ ai_

goal (4 subgoals):
 1. \<And>z A B M ai a a'. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> z = n - ai
 2. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>z A B M ai a a'. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> z = n - ai
 2. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(invar1 A_ B_ M_ ai_ \<and> ai_ < n) \<and> n - ai_ = z_

goal (4 subgoals):
 1. \<And>z A B M ai a a'. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> z = n - ai
 2. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
(* outer invar and b ibplies inner invar *)
[PROOF STATE]
proof (state)
this:
(invar1 A_ B_ M_ ai_ \<and> ai_ < n) \<and> n - ai_ = z_

goal (4 subgoals):
 1. \<And>z A B M ai a a'. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> z = n - ai
 2. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(invar1 A_ B_ M_ ai_ \<and> ai_ < n) \<and> n - ai_ = z_

goal (1 subgoal):
 1. invar2 A_ B_ M_ ai_ ai_ \<and> z_ = n - ai_
[PROOF STEP]
by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
[PROOF STATE]
proof (state)
this:
invar2 A_ B_ M_ ai_ ai_ \<and> z_ = n - ai_

goal (3 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case (4 z A B M ai a)
[PROOF STATE]
proof (state)
this:
(invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a

goal (3 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
(* inner invar' and not b ibplies outer invar *)
[PROOF STATE]
proof (state)
this:
(invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a

goal (3 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
note inv = 4[THEN conjunct1, unfolded invar2_def]
[PROOF STATE]
proof (state)
this:
(invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (3 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
note invAM = inv[THEN conjunct1,THEN conjunct1]
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1} - {a})

goal (3 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
note aai = inv[THEN conjunct1, THEN conjunct2, THEN conjunct2]
[PROOF STATE]
proof (state)
this:
a \<le> ai \<and> ai < n

goal (3 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B M ai a a'. (invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a, a') \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B[match A a := a], M[match A a := True], ai + 1, a, a'_) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
 2. n - (ai + 1) < z
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
 2. n - (ai + 1) < z
[PROOF STEP]
have *: "{<Suc ai} = insert a ({<Suc ai} - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<Suc ai} = {a} \<union> ({<Suc ai} - {a})
[PROOF STEP]
using aai
[PROOF STATE]
proof (prove)
using this:
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. {<Suc ai} = {a} \<union> ({<Suc ai} - {a})
[PROOF STEP]
by (simp add: insert_absorb)
[PROOF STATE]
proof (state)
this:
{<Suc ai} = {a} \<union> ({<Suc ai} - {a})

goal (2 subgoals):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
 2. n - (ai + 1) < z
[PROOF STEP]
have **: "inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))
[PROOF STEP]
by (metis "*" Diff_idemp inj_on_insert)
[PROOF STATE]
proof (state)
this:
inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))

goal (2 subgoals):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
 2. n - (ai + 1) < z
[PROOF STEP]
have nm: "match A a \<notin> match A ` ({<Suc ai} - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match A a \<notin> match A ` ({<Suc ai} - {a})
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
(invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<Suc ai} - {a})
[PROOF STEP]
unfolding invar2_def ran_def
[PROOF STATE]
proof (prove)
using this:
((invAM A ({<ai + 1} - {a}) \<and> ((_Collect b (\<exists>a. \<alpha> B M a = Some b) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> match A a = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> M ! match A a

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<Suc ai} - {a})
[PROOF STEP]
apply (clarsimp simp: set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n = length A; set A \<subseteq> {<length A}; inj_on (match A) ({<Suc ai} - {a}); {<Suc ai} - {a} \<subseteq> {<length A}; pref_match A ({<Suc ai} - {a}); opti\<^sub>a A; \<forall>x. (\<exists>a<length A. M ! a \<and> x = B ! a) = (x < Suc ai \<and> x \<noteq> a); \<forall>b. b < length A \<and> M ! b \<longrightarrow> match A (B ! b) = b; length B = length A; length M = length A; a \<le> ai; ai < length A; z = length A - ai; \<not> M ! match A x; match A a = match A x; x < Suc ai\<rbrakk> \<Longrightarrow> x = a
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
match A a \<notin> match A ` ({<Suc ai} - {a})

goal (2 subgoals):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
 2. n - (ai + 1) < z
[PROOF STEP]
have invAM': "invAM A {<ai+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM A {<ai + 1}
[PROOF STEP]
using invAM_match[OF invAM, of a] aai nm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < n \<and> a \<notin> {<ai + 1} - {a}; match A a \<notin> match A ` ({<ai + 1} - {a})\<rbrakk> \<Longrightarrow> invAM A ({<ai + 1} - {a} \<union> {a})
a \<le> ai \<and> ai < n
match A a \<notin> match A ` ({<Suc ai} - {a})

goal (1 subgoal):
 1. invAM A {<ai + 1}
[PROOF STEP]
by (simp add: ** insert_absorb)
[PROOF STATE]
proof (state)
this:
invAM A {<ai + 1}

goal (2 subgoals):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
 2. n - (ai + 1) < z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
[PROOF STEP]
using 4 invAM'
[PROOF STATE]
proof (prove)
using this:
(invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a
invAM A {<ai + 1}

goal (1 subgoal):
 1. invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)
[PROOF STEP]
by (simp add: \<alpha>update1 match_less_n insert_absorb nth_list_update)
[PROOF STATE]
proof (state)
this:
invar1 A (B[match A a := a]) (M[match A a := True]) (ai + 1)

goal (1 subgoal):
 1. n - (ai + 1) < z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n - (ai + 1) < z
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. n - (ai + 1) < z
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - (ai + 1) < z
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
(invar2 A B M ai a \<and> z = n - ai) \<and> \<not> M ! match A a

goal (1 subgoal):
 1. n - (ai + 1) < z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - (ai + 1) < z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A, B[match A a := a], M[match A a := True], ai + 1, a, a'_) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> n - ai) < z)

goal (2 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 5
[PROOF STATE]
proof (state)
this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n

goal (2 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
(* outer invar and not b ibplies post *)
[PROOF STATE]
proof (state)
this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n

goal (2 subgoals):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B M ai a a'. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
using pref_match_stable
[PROOF STATE]
proof (prove)
using this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
unfolding invAM_def invar1_def
[PROOF STATE]
proof (prove)
using this:
((matching A_ {<ai_} \<and> {<ai_} \<subseteq> {<n} \<and> pref_match A_ {<ai_} \<and> opti\<^sub>a A_) \<and> (invAB A_ (\<alpha> B_ M_) {<ai_} \<and> length B_ = n \<and> length M_ = n) \<and> ai_ \<le> n) \<and> \<not> ai_ < n
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
by(metis le_neq_implies_less)
[PROOF STATE]
proof (state)
this:
matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
case (3 z v A B M ai a)
[PROOF STATE]
proof (state)
this:
((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = v

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
(* preservation of inner invar *)
[PROOF STATE]
proof (state)
this:
((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = v

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
let ?M = "{<ai+1} - {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((invAM A ({<ai + 1} - {a}) &&& matching A ({<ai + 1} - {a})) &&& local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n}) &&& (pref_match A ({<ai + 1} - {a}) &&& M ! match A a) &&& var A {<ai} = v &&& a \<le> ai \<and> ai < n &&& invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = v

goal (1 subgoal):
 1. ((invAM A ({<ai + 1} - {a}) &&& matching A ({<ai + 1} - {a})) &&& local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n}) &&& (pref_match A ({<ai + 1} - {a}) &&& M ! match A a) &&& var A {<ai} = v &&& a \<le> ai \<and> ai < n &&& invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1} - {a})
matching A ({<ai + 1} - {a})
local.wf A
{<ai + 1} - {a} \<subseteq> {<n}
pref_match A ({<ai + 1} - {a})
M ! match A a
var A {<ai} = v
a \<le> ai \<and> ai < n
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
note invar = 3[THEN conjunct1, THEN conjunct1, unfolded invar2_def]
[PROOF STATE]
proof (state)
this:
(invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
[PROOF STATE]
proof (state)
this:
pref_match' A ({<ai + 1} - {a})

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M"
[PROOF STATE]
proof (prove)
using this:
pref_match' A ({<ai + 1} - {a})

goal (1 subgoal):
 1. \<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})
[PROOF STEP]
unfolding pref_match'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>aa<n. \<forall>b\<in>preferred A aa. \<exists>a'\<in>{<ai + 1} - {a}. b = match A a' \<and> P\<^sub>b ! b \<turnstile> a' < aa

goal (1 subgoal):
 1. \<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
let ?a = "B ! match A a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have a: "a < n \<and> a \<notin> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < n \<and> a \<notin> {<ai + 1} - {a}
[PROOF STEP]
using invar
[PROOF STATE]
proof (prove)
using this:
(invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (1 subgoal):
 1. a < n \<and> a \<notin> {<ai + 1} - {a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a < n \<and> a \<notin> {<ai + 1} - {a}

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have a': "?a \<in> ?M \<and> match A ?a = match A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
[PROOF STEP]
using invAB match_less_n[OF A] a matched
[PROOF STATE]
proof (prove)
using this:
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<ai + 1} - {a}
M ! match A a

goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
[PROOF STEP]
by (metis \<alpha>_Some ranI)
[PROOF STATE]
proof (state)
this:
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have "?M \<noteq> {<n}" and "?a < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} \<noteq> {<n} &&& B ! match A a < n
[PROOF STEP]
using M a a' atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
{<ai + 1} - {a} \<subseteq> {<n}
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
{<?n} = {..<?n}

goal (1 subgoal):
 1. {<ai + 1} - {a} \<noteq> {<n} &&& B ! match A a < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{<ai + 1} - {a} \<noteq> {<n}
B ! match A a < n

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have card: "card {<ai} = card ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {<ai} = card ({<ai + 1} - {a})
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. card {<ai} = card ({<ai + 1} - {a})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {<ai} = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have *: "{<ai + 1} - {a} - {?a} \<union> {a} = {<ai + 1} - {?a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
[PROOF STEP]
using invar a'
[PROOF STATE]
proof (prove)
using this:
(invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. {<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}

goal (1 subgoal):
 1. \<And>z na A B M ai a a'. ((invar2 A B M ai a \<and> z = n - ai) \<and> M ! match A a) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < v))
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai) \<and> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai) \<and> var (A[a := A ! a + 1]) {<ai} < v)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai) \<and> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai) \<and> var (A[a := A ! a + 1]) {<ai} < v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai) \<and> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai) \<and> var (A[a := A ! a + 1]) {<ai} < v)
[PROOF STEP]
proof ((rule;rule;rule), goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai
 2. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
 3. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 4. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
case unstab: 1
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a

goal (4 subgoals):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai
 2. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
 3. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 4. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
have inj_dom: "inj_on (\<alpha> B M) (dom (\<alpha> B M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<alpha> B M) (dom (\<alpha> B M))
[PROOF STEP]
by (metis (mono_tags) domD inj_onI invAB)
[PROOF STATE]
proof (state)
this:
inj_on (\<alpha> B M) (dom (\<alpha> B M))

goal (4 subgoals):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai
 2. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
 3. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 4. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {?a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
[PROOF STEP]
using invAB_swap[OF invAB[THEN conjunct1] a a' inj_dom] * match_less_n[OF A] a matched invAB
[PROOF STATE]
proof (prove)
using this:
\<alpha> B M (match A a) = Some (B ! match A a) \<Longrightarrow> invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> B M(match A a \<mapsto> a)) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
{<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<ai + 1} - {a}
M ! match A a
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
[PROOF STEP]
by(simp add:\<alpha>update2)
[PROOF STATE]
proof (state)
this:
invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})

goal (4 subgoals):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai
 2. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
 3. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 4. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai
[PROOF STEP]
using invAM_swap[OF invAM a a' unstab] invAB' invar a'
[PROOF STATE]
proof (prove)
using this:
invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
(invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a})
invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
(invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai
[PROOF STEP]
by (simp add: insert_absorb \<alpha>update2)
[PROOF STATE]
proof (state)
this:
invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai

goal (3 subgoals):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
 2. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 3. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a

goal (3 subgoals):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
 2. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 3. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
[PROOF STEP]
using v var_next[OF m M \<open>?M \<noteq> {<n}\<close> pref_match1 \<open>?a < n\<close>] card
[PROOF STATE]
proof (prove)
using this:
var A {<ai} = v
var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {a}) < var A ({<ai + 1} - {a})
card {<ai} = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v
[PROOF STEP]
by (metis var_def Suc_eq_plus1)
[PROOF STATE]
proof (state)
this:
var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v

goal (2 subgoals):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 2. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 2. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
case stab: 3
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a

goal (2 subgoals):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 2. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
have *: "\<forall>b. b < n \<and> M!b \<longrightarrow> a \<noteq> B!b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b. b < n \<and> M ! b \<longrightarrow> a \<noteq> B ! b
[PROOF STEP]
by (metis invAB ranI \<alpha>_Some a)
[PROOF STATE]
proof (state)
this:
\<forall>b. b < n \<and> M ! b \<longrightarrow> a \<noteq> B ! b

goal (2 subgoals):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
 2. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
[PROOF STEP]
using invAM_next[OF invAM a a' stab] invar *
[PROOF STATE]
proof (prove)
using this:
invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})
(invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> z = n - ai
\<forall>b. b < n \<and> M ! b \<longrightarrow> a \<noteq> B ! b

goal (1 subgoal):
 1. invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai
[PROOF STEP]
by (simp add: match_def)
[PROOF STATE]
proof (state)
this:
invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
using v var_next[OF m M \<open>?M \<noteq> {<n}\<close> pref_match1, of a] a card
[PROOF STATE]
proof (prove)
using this:
var A {<ai} = v
a < n \<Longrightarrow> var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < var A ({<ai + 1} - {a})
a < n \<and> a \<notin> {<ai + 1} - {a}
card {<ai} = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
by (metis Suc_eq_plus1 var_def)
[PROOF STATE]
proof (state)
this:
var (A[a := A ! a + 1]) {<ai} < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> z = n - ai) \<and> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < v) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (invar2 (A[a := A ! a + 1]) B M ai a \<and> z = n - ai) \<and> var (A[a := A ! a + 1]) {<ai} < v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, ai, B ! match A a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! match A a) \<in> _Collect s ((case s of (A, B, M, ai, a, a') \<Rightarrow> invar2 A B M ai a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a') \<Rightarrow> var A {<ai}) < v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pres2':
assumes "invar2' A B M 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
  "(\<not> M ! b \<longrightarrow>
    invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and>
   (M ! b \<longrightarrow>
    (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and>
    (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
let ?M = "{<ai+1} - {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
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 v: "var A ?M = v" and as: "a \<le> ai \<and> ai < n" and invAB: "invAB2 A B M ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((invAM A ({<ai + 1} - {a}) &&& matching A ({<ai + 1} - {a})) &&& local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n}) &&& (pref_match A ({<ai + 1} - {a}) &&& var A ({<ai + 1} - {a}) = v) &&& a \<le> ai \<and> ai < n &&& invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
invar2' A B M ai a
ai < n
var A ({<ai + 1} - {a}) = v
b = match A a
a' = B ! b
A1 = A[a' := A ! a' + 1]
A2 = A[a := A ! a + 1]

goal (1 subgoal):
 1. ((invAM A ({<ai + 1} - {a}) &&& matching A ({<ai + 1} - {a})) &&& local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n}) &&& (pref_match A ({<ai + 1} - {a}) &&& var A ({<ai + 1} - {a}) = v) &&& a \<le> ai \<and> ai < n &&& invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1} - {a})
matching A ({<ai + 1} - {a})
local.wf A
{<ai + 1} - {a} \<subseteq> {<n}
pref_match A ({<ai + 1} - {a})
var A ({<ai + 1} - {a}) = v
a \<le> ai \<and> ai < n
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
note invar = assms(1)
[PROOF STATE]
proof (state)
this:
invar2' A B M ai a

goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
[PROOF STATE]
proof (state)
this:
pref_match' A ({<ai + 1} - {a})

goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M"
[PROOF STATE]
proof (prove)
using this:
pref_match' A ({<ai + 1} - {a})

goal (1 subgoal):
 1. \<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})
[PROOF STEP]
unfolding pref_match'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>aa<n. \<forall>b\<in>preferred A aa. \<exists>a'\<in>{<ai + 1} - {a}. b = match A a' \<and> P\<^sub>b ! b \<turnstile> a' < aa

goal (1 subgoal):
 1. \<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})

goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
have a: "a < n \<and> a \<notin> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < n \<and> a \<notin> {<ai + 1} - {a}
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. a < n \<and> a \<notin> {<ai + 1} - {a}
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
a < n \<and> a \<notin> {<ai + 1} - {a}

goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
show ?thesis (is "(\<not> ?matched \<longrightarrow> ?THEN) \<and> (?matched \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> M ! b \<Longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v
 2. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
assume "\<not> ?matched"
[PROOF STATE]
proof (state)
this:
\<not> M ! b

goal (2 subgoals):
 1. \<not> M ! b \<Longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v
 2. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> M ! b
[PROOF STEP]
have nm: "match A a \<notin> match A ` ?M"
[PROOF STATE]
proof (prove)
using this:
\<not> M ! b

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<ai + 1} - {a})
[PROOF STEP]
using invAB
[PROOF STATE]
proof (prove)
using this:
\<not> M ! b
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<ai + 1} - {a})
[PROOF STEP]
unfolding ran_def
[PROOF STATE]
proof (prove)
using this:
\<not> M ! b
(_Collect b (\<exists>a. \<alpha> B M a = Some b) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> match A a = b)) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<ai + 1} - {a})
[PROOF STEP]
apply (clarsimp simp: set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> M ! match A x; \<forall>x. (\<exists>a<length B. M ! a \<and> x = B ! a) = (x < Suc ai \<and> x \<noteq> a); \<forall>b. b < length B \<and> M ! b \<longrightarrow> match A (B ! b) = b; length M = length B; n = length B; match A a = match A x; x < Suc ai\<rbrakk> \<Longrightarrow> x = a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
match A a \<notin> match A ` ({<ai + 1} - {a})

goal (2 subgoals):
 1. \<not> M ! b \<Longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v
 2. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
proof(rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
 2. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
have *: "{<ai + 1 + 1} - {ai + 1} = {<ai + 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1 + 1} - {ai + 1} = {<ai + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{<ai + 1 + 1} - {ai + 1} = {<ai + 1}

goal (2 subgoals):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
 2. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
have **: "{<ai + 1} - {a} \<union> {a} = {<ai + 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} \<union> {a} = {<ai + 1}
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. {<ai + 1} - {a} \<union> {a} = {<ai + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{<ai + 1} - {a} \<union> {a} = {<ai + 1}

goal (2 subgoals):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
 2. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
hence invAM': "invAM A {<ai+1}"
[PROOF STATE]
proof (prove)
using this:
{<ai + 1} - {a} \<union> {a} = {<ai + 1}

goal (1 subgoal):
 1. invAM A {<ai + 1}
[PROOF STEP]
using invAM_match[OF invAM a nm]
[PROOF STATE]
proof (prove)
using this:
{<ai + 1} - {a} \<union> {a} = {<ai + 1}
invAM A ({<ai + 1} - {a} \<union> {a})

goal (1 subgoal):
 1. invAM A {<ai + 1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invAM A {<ai + 1}

goal (2 subgoals):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
 2. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
have invAB': "invAB2 A (B[match A a := a]) (M[match A a := True]) {<ai+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB A (\<alpha> (B[match A a := a]) (M[match A a := True])) {<ai + 1} \<and> length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n
[PROOF STEP]
using invAB \<open>\<not> ?matched\<close> **
[PROOF STATE]
proof (prove)
using this:
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
\<not> M ! b
{<ai + 1} - {a} \<union> {a} = {<ai + 1}

goal (1 subgoal):
 1. invAB A (\<alpha> (B[match A a := a]) (M[match A a := True])) {<ai + 1} \<and> length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n
[PROOF STEP]
by (simp add: A a \<alpha>update1 match_less_n nth_list_update)
[PROOF STATE]
proof (state)
this:
invAB A (\<alpha> (B[match A a := a]) (M[match A a := True])) {<ai + 1} \<and> length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n

goal (2 subgoals):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
 2. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
 2. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
[PROOF STEP]
using invAM' as invAB' *
[PROOF STATE]
proof (prove)
using this:
invAM A {<ai + 1}
a \<le> ai \<and> ai < n
invAB A (\<alpha> (B[match A a := a]) (M[match A a := True])) {<ai + 1} \<and> length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n
{<ai + 1 + 1} - {ai + 1} = {<ai + 1}

goal (1 subgoal):
 1. invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)
[PROOF STEP]
by (simp add: Suc_le_eq plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1)

goal (1 subgoal):
 1. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan * **
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{<ai + 1} - {a} \<noteq> {<n}; a \<notin> {<ai + 1} - {a}\<rbrakk> \<Longrightarrow> var A ({<ai + 1} - {a} \<union> {a}) < var A ({<ai + 1} - {a})
a < n \<and> a \<notin> {<ai + 1} - {a}
{<?n} = {..<?n}
{<ai + 1 + 1} - {ai + 1} = {<ai + 1}
{<ai + 1} - {a} \<union> {a} = {<ai + 1}

goal (1 subgoal):
 1. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
unfolding v
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{<ai + 1} - {a} \<noteq> {<n}; a \<notin> {<ai + 1} - {a}\<rbrakk> \<Longrightarrow> var A ({<ai + 1} - {a} \<union> {a}) < v
a < n \<and> a \<notin> {<ai + 1} - {a}
{<?n} = {..<?n}
{<ai + 1 + 1} - {ai + 1} = {<ai + 1}
{<ai + 1} - {a} \<union> {a} = {<ai + 1}

goal (1 subgoal):
 1. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
by (metis lessThan_iff)
[PROOF STATE]
proof (state)
this:
var A ({<ai + 1 + 1} - {ai + 1}) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v

goal (1 subgoal):
 1. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
assume matched: "?matched"
[PROOF STATE]
proof (state)
this:
M ! b

goal (1 subgoal):
 1. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
let ?a = "B ! match A a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
have a': "?a \<in> ?M \<and> match A ?a = match A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
[PROOF STEP]
using invAB match_less_n[OF A] a matched after
[PROOF STATE]
proof (prove)
using this:
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<ai + 1} - {a}
M ! b
b = match A a
a' = B ! b
A1 = A[a' := A ! a' + 1]
A2 = A[a := A ! a + 1]

goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
[PROOF STEP]
by (metis \<alpha>_Some ranI)
[PROOF STATE]
proof (state)
this:
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
hence "?a < n" "a \<noteq> ?a"
[PROOF STATE]
proof (prove)
using this:
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. B ! match A a < n &&& a \<noteq> B ! match A a
[PROOF STEP]
using a M atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a < n \<and> a \<notin> {<ai + 1} - {a}
{<ai + 1} - {a} \<subseteq> {<n}
{<?n} = {..<?n}

goal (1 subgoal):
 1. B ! match A a < n &&& a \<noteq> B ! match A a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B ! match A a < n
a \<noteq> B ! match A a

goal (1 subgoal):
 1. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
have inj_dom: "inj_on (\<alpha> B M) (dom (\<alpha> B M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<alpha> B M) (dom (\<alpha> B M))
[PROOF STEP]
by (metis (mono_tags) domD inj_onI invAB)
[PROOF STATE]
proof (state)
this:
inj_on (\<alpha> B M) (dom (\<alpha> B M))

goal (1 subgoal):
 1. M ! b \<Longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
show ?ELSE (is "(?pref \<longrightarrow> ?THEN) \<and> (\<not> ?pref \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
assume ?pref
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A a' \<turnstile> a < a'

goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
proof (rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar2' A1 (B[b := a]) M ai a'
 2. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
have *: "{<ai + 1} - {a} - {?a} \<union> {a} = {<ai + 1} - {?a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
[PROOF STEP]
using a a' as
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. {<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}

goal (2 subgoals):
 1. invar2' A1 (B[b := a]) M ai a'
 2. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
have a'neq: "\<forall>b<n. b \<noteq> match A a \<longrightarrow> M!b \<longrightarrow> ?a \<noteq> B!b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b<n. b \<noteq> match A a \<longrightarrow> M ! b \<longrightarrow> B ! match A a \<noteq> B ! b
[PROOF STEP]
using invAB a'
[PROOF STATE]
proof (prove)
using this:
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. \<forall>b<n. b \<noteq> match A a \<longrightarrow> M ! b \<longrightarrow> B ! match A a \<noteq> B ! b
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>b<n. b \<noteq> match A a \<longrightarrow> M ! b \<longrightarrow> B ! match A a \<noteq> B ! b

goal (2 subgoals):
 1. invar2' A1 (B[b := a]) M ai a'
 2. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {?a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
[PROOF STEP]
using invAB_swap[OF invAB[THEN conjunct1] a a' inj_dom] * match_less_n[OF A] a matched invAB
[PROOF STATE]
proof (prove)
using this:
\<alpha> B M (match A a) = Some (B ! match A a) \<Longrightarrow> invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> B M(match A a \<mapsto> a)) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
{<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<ai + 1} - {a}
M ! b
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
[PROOF STEP]
by(simp add:\<alpha>update2)
[PROOF STATE]
proof (state)
this:
invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})

goal (2 subgoals):
 1. invar2' A1 (B[b := a]) M ai a'
 2. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invar2' A1 (B[b := a]) M ai a'
 2. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2' A1 (B[b := a]) M ai a'
[PROOF STEP]
using invAM_swap[OF invAM a a'] \<open>?pref\<close> invAB invAB'
[PROOF STATE]
proof (prove)
using this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
P\<^sub>b ! match A a' \<turnstile> a < a'
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})

goal (1 subgoal):
 1. invar2' A1 (B[b := a]) M ai a'
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a})
P\<^sub>b ! match A a' \<turnstile> a < a'
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})

goal (1 subgoal):
 1. invar2' A1 (B[b := a]) M ai a'
[PROOF STEP]
using a' as
[PROOF STATE]
proof (prove)
using this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a})
P\<^sub>b ! match A a' \<turnstile> a < a'
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. invar2' A1 (B[b := a]) M ai a'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invar2' A1 (B[b := a]) M ai a'

goal (1 subgoal):
 1. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
have "card({<ai + 1} - {?a}) = card({<ai + 1} - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({<ai + 1} - {B ! match A a}) = card ({<ai + 1} - {a})
[PROOF STEP]
using a a' as
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. card ({<ai + 1} - {B ! match A a}) = card ({<ai + 1} - {a})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({<ai + 1} - {B ! match A a}) = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
card ({<ai + 1} - {B ! match A a}) = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
using v var_next[OF m M _ pref_match1, of ?a] \<open>?a < n\<close> a atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
card ({<ai + 1} - {B ! match A a}) = card ({<ai + 1} - {a})
var A ({<ai + 1} - {a}) = v
\<lbrakk>{<ai + 1} - {a} \<noteq> {<n}; B ! match A a < n\<rbrakk> \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {a}) < var A ({<ai + 1} - {a})
B ! match A a < n
a < n \<and> a \<notin> {<ai + 1} - {a}
{<?n} = {..<?n}

goal (1 subgoal):
 1. var A1 ({<ai + 1} - {a'}) < v
[PROOF STEP]
by (metis Suc_eq_plus1 lessThan_iff var_def after)
[PROOF STATE]
proof (state)
this:
var A1 ({<ai + 1} - {a'}) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
assume "\<not> ?pref"
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
proof (rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar2' A2 B M ai a
 2. var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invar2' A2 B M ai a
 2. var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
have "invAB2 (A[a := A ! a + 1]) B M ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB (A[a := A ! a + 1]) (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
using invAB a
[PROOF STATE]
proof (prove)
using this:
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
a < n \<and> a \<notin> {<ai + 1} - {a}

goal (1 subgoal):
 1. invAB (A[a := A ! a + 1]) (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
by (metis match_def nth_list_update_neq ranI)
[PROOF STATE]
proof (state)
this:
invAB (A[a := A ! a + 1]) (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (2 subgoals):
 1. invar2' A2 B M ai a
 2. var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
invAB (A[a := A ! a + 1]) (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. invar2' A2 B M ai a
[PROOF STEP]
using invAM_next[OF invAM a a'] \<open>\<not> ?pref\<close> invar after
[PROOF STATE]
proof (prove)
using this:
invAB (A[a := A ! a + 1]) (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'
invar2' A B M ai a
b = match A a
a' = B ! b
A1 = A[a' := A ! a' + 1]
A2 = A[a := A ! a + 1]

goal (1 subgoal):
 1. invar2' A2 B M ai a
[PROOF STEP]
by (meson invar2'_def)
[PROOF STATE]
proof (state)
this:
invar2' A2 B M ai a

goal (1 subgoal):
 1. var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
using a v var_next[OF m M _ pref_match1, of a] after
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<ai + 1} - {a}
var A ({<ai + 1} - {a}) = v
\<lbrakk>{<ai + 1} - {a} \<noteq> {<n}; a < n\<rbrakk> \<Longrightarrow> var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < var A ({<ai + 1} - {a})
b = match A a
a' = B ! b
A1 = A[a' := A ! a' + 1]
A2 = A[a := A ! a + 1]

goal (1 subgoal):
 1. var A2 ({<ai + 1} - {a}) < v
[PROOF STEP]
by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff)
[PROOF STATE]
proof (state)
this:
var A2 ({<ai + 1} - {a}) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<not> M ! b \<longrightarrow> invar2' A (B[b := a]) (M[b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! b \<longrightarrow> (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A1 (B[b := a]) M ai a' \<and> var A1 ({<ai + 1} - {a'}) < v) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> invar2' A2 B M ai a \<and> var A2 ({<ai + 1} - {a}) < v))

goal:
No subgoals!
[PROOF STEP]
qed