[STATEMENT]
lemma Gale_Shapley6_1_explicit:
assumes "R\<^sub>b = map ranking P\<^sub>b"
shows "VARS A B M a a' ai b r
 [ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
 WHILE ai < n
 INV { invar2' A B M ai a }
 VAR {var A ({<ai+1} - {a})}
 DO b := match A a;
  IF \<not> M ! b
  THEN B[b] := a; M[b] := True; ai := ai + 1; a := ai
  ELSE a' := B ! b; r := R\<^sub>b ! match A a';
       IF r ! a < r ! a'
       THEN B[b] := a; A[a'] := A!a'+1; a := a'
       ELSE A[a] := A!a+1
       FI
  FI
 OD
 [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
WHILE ai < n INV {invar2' A B M ai a}  VAR {var A ({<ai + 1} - {a})}
DO b := match A a; IF \<not> M ! b THEN B := B[b := a]; M := M[b := True]; ai := ai + 1; a := ai  ELSE a' := B ! b; r := R\<^sub>b ! match A a'; IF r ! a < r ! a' THEN B := B[b := a]; A := A[a' := A ! a' + 1]; a := a'  ELSE A := A[a := A ! a + 1] FI FI 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 (3 subgoals):
 1. \<And>A B M a a' ai b r. ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar2' A B M ai a
 2. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 3. \<And>A B M a a' ai b r. invar2' A B M ai a \<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_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (3 subgoals):
 1. \<And>A B M a a' ai b r. ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar2' A B M ai a
 2. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 3. \<And>A B M a a' ai b r. invar2' A B M ai a \<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_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (1 subgoal):
 1. invar2' A_ B_ M_ ai_ a_
[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:
invar2' A_ B_ M_ ai_ a_

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

goal (2 subgoals):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 2. \<And>A B M a a' ai b r. invar2' A B M ai a \<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:
invar2' A_ B_ M_ ai_ a_ \<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 atLeast0_lessThan_Suc
[PROOF STATE]
proof (prove)
using this:
invar2' A_ B_ M_ ai_ a_ \<and> \<not> ai_ < n
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}
{<Suc ?n} = {?n} \<union> {<?n}

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

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

goal (1 subgoal):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
let ?M = "{<ai+1} - {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < 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 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 2
[PROOF STATE]
proof (prove)
using this:
(invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = 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}) &&& 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. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
note invar = 2[THEN conjunct1,THEN conjunct1]
[PROOF STATE]
proof (state)
this:
invar2' A B M ai a

goal (1 subgoal):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < 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>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < 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>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < 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 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. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
show ?case (is "(?not_matched \<longrightarrow> ?THEN) \<and> (\<not> ?not_matched \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
assume ?not_matched
[PROOF STATE]
proof (state)
this:
\<not> M ! match A a

goal (2 subgoals):
 1. \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> M ! match A a
[PROOF STEP]
have nm: "match A a \<notin> match A ` ?M"
[PROOF STATE]
proof (prove)
using this:
\<not> M ! match A a

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 ! match A a
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 ! match A a
(_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 ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar2' A (B[match A a := a]) (M[match A a := 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[match A a := a]) (M[match A a := 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[match A a := a]) (M[match A a := 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[match A a := a]) (M[match A a := 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 ! match A a
{<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[match A a := a]) (M[match A a := 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[match A a := a]) (M[match A a := 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[match A a := a]) (M[match A a := 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[match A a := a]) (M[match A a := 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[match A a := a]) (M[match A a := 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:
(A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)

goal (1 subgoal):
 1. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
assume matched: "\<not> ?not_matched"
[PROOF STATE]
proof (state)
this:
\<not> \<not> M ! match A a

goal (1 subgoal):
 1. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
let ?a = "B ! match A a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<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
[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}
\<not> \<not> 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. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<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. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<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. \<not> \<not> M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<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. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<Longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. \<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
assume ?pref
[PROOF STATE]
proof (state)
this:
R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)

goal (2 subgoals):
 1. R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<Longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. \<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar2' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a)
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A 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' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a)
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A 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' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a)
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A 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}
\<not> \<not> 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 (2 subgoals):
 1. invar2' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a)
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a}) < v
[PROOF STEP]
have pref: "P\<^sub>b ! match A ?a \<turnstile> a < ?a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a
[PROOF STEP]
using A P\<^sub>b_set \<open>?a < n\<close> \<open>?pref\<close> a assms length_P\<^sub>b
[PROOF STATE]
proof (prove)
using this:
local.wf A
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}
B ! match A a < n
R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)
a < n \<and> a \<notin> {<ai + 1} - {a}
R\<^sub>b = map ranking P\<^sub>b
length P\<^sub>b = n

goal (1 subgoal):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a
[PROOF STEP]
by(auto simp: match_less_n ranking_iff_pref)
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a

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

goal (2 subgoals):
 1. invar2' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a)
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a}) < 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)
[PROOF STEP]
(* changed *)
[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)
[PROOF STEP]
using invAM_swap[OF invAM a a' pref] invAB invAB' a' as
[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 (\<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' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a)
[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 (\<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' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a)
[PROOF STEP]
by (simp add: match_less_n ranking_iff_pref)
[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)

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

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

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

goal (1 subgoal):
 1. \<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
assume "\<not> ?pref"
[PROOF STATE]
proof (state)
this:
\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)

goal (1 subgoal):
 1. \<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar2' (A[a := A ! a + 1]) B M ai a
 2. var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invar2' (A[a := A ! a + 1]) B M ai a
 2. var (A[a := A ! a + 1]) ({<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' (A[a := A ! a + 1]) B M ai a
 2. var (A[a := A ! a + 1]) ({<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' (A[a := A ! a + 1]) B M ai a
[PROOF STEP]
using invAM_next[OF invAM a a'] \<open>\<not> ?pref\<close>  \<open>B ! match A a < n\<close> P\<^sub>b_set 2 assms
[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> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)
B ! match A a < n
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}
(invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = v
R\<^sub>b = map ranking P\<^sub>b

goal (1 subgoal):
 1. invar2' (A[a := A ! a + 1]) B M ai a
[PROOF STEP]
by (simp add: invar2'_def length_P\<^sub>b match_less_n ranking_iff_pref)
[PROOF STATE]
proof (state)
this:
invar2' (A[a := A ! a + 1]) B M ai a

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v
[PROOF STEP]
(* changed *)
[PROOF STATE]
proof (state)
this:
invar2' (A[a := A ! a + 1]) B M ai a

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

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v
[PROOF STEP]
using a v var_next[OF m M _ pref_match1, of a]
[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})

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gs_inner:
assumes "R\<^sub>b = map ranking P\<^sub>b"
assumes "invar2 A B M ai a" "b = match A a"
shows "gs_inner P\<^sub>a R\<^sub>b M (A, B, a, b) = (A',B',a',b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs_inner P\<^sub>a R\<^sub>b M (A, B, a, b) = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
[PROOF STEP]
unfolding gs_inner_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while (\<lambda>(A, B, a, y). M ! y) (\<lambda>(A, B, a, b). let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a))) (A, B, a, b) = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
[PROOF STEP]
proof(rule while_rule2[where P = "\<lambda>(A,B,a,b). invar2 A B M ai a \<and> b = match A a"
 and r = "measure (%(A, B, a, b). Pref.var P\<^sub>a A {<ai})"], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. case (A, B, a, b) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
 2. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; case s of (A, B, a, x) \<Rightarrow> M ! x\<rbrakk> \<Longrightarrow> (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
 3. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 4. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. case (A, B, a, b) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
 2. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; case s of (A, B, a, x) \<Rightarrow> M ! x\<rbrakk> \<Longrightarrow> (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
 3. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 4. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (A, B, a, b) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
R\<^sub>b = map ranking P\<^sub>b
invar2 A B M ai a
b = match A a

goal (1 subgoal):
 1. case (A, B, a, b) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
[PROOF STEP]
unfolding var_def
[PROOF STATE]
proof (prove)
using this:
R\<^sub>b = map ranking P\<^sub>b
invar2 A B M ai a
b = match A a

goal (1 subgoal):
 1. case (A, B, a, b) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
case (A, B, a, b) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; case s of (A, B, a, x) \<Rightarrow> M ! x\<rbrakk> \<Longrightarrow> (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
 2. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 3. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; case s of (A, B, a, x) \<Rightarrow> M ! x\<rbrakk> \<Longrightarrow> (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
 2. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 3. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
case inv: (2 s)
[PROOF STATE]
proof (state)
this:
case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
case s of (A, B, a, x) \<Rightarrow> M ! x

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; case s of (A, B, a, x) \<Rightarrow> M ! x\<rbrakk> \<Longrightarrow> (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
 2. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 3. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
obtain A B a b where s: "s =  (A, B, a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B a b. s = (A, B, a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases4
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c d. ?y = (a, b, c, d) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>A B a b. s = (A, B, a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s = (A, B, a, b)

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; case s of (A, B, a, x) \<Rightarrow> M ! x\<rbrakk> \<Longrightarrow> (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
 2. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 3. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
have R: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
[PROOF STEP]
by (simp add: P\<^sub>b_set \<open>R\<^sub>b = _\<close> length_P\<^sub>b ranking_iff_pref)
[PROOF STATE]
proof (state)
this:
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; case s of (A, B, a, x) \<Rightarrow> M ! x\<rbrakk> \<Longrightarrow> (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
 2. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 3. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
[PROOF STEP]
proof(rule, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
 2. (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
 2. (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
[PROOF STEP]
using inv
[PROOF STATE]
proof (prove)
using this:
case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
case s of (A, B, a, x) \<Rightarrow> M ! x

goal (1 subgoal):
 1. case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
[PROOF STEP]
apply(simp only: s prod.case Let_def split: if_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar2 A B M ai a \<and> b = match A a; M ! match A a\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A 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> P\<^sub>a ! (B ! match A a) ! (A[B ! match A a := A ! (B ! match A a) + 1] ! (B ! match A a)) = match (A[B ! match A a := A ! (B ! match A a) + 1]) (B ! match A a)) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! (B ! match A a) \<longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> P\<^sub>a ! a ! (A[a := A ! a + 1] ! a) = match (A[a := A ! a + 1]) a)
[PROOF STEP]
using inner_pres[OF R _ _ refl refl refl refl refl, of A B M ai a b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>invar2 A B M ai a; M ! b; b = match A a\<rbrakk> \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> invar2 (A[B ! b := A ! (B ! b) + 1]) (B[b := a]) M ai (B ! b) \<and> var (A[B ! b := A ! (B ! b) + 1]) {<ai} < var A {<ai}) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> var (A[a := A ! a + 1]) {<ai} < var A {<ai})

goal (1 subgoal):
 1. \<lbrakk>invar2 A B M ai a \<and> b = match A a; M ! match A a\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A 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> P\<^sub>a ! (B ! match A a) ! (A[B ! match A a := A ! (B ! match A a) + 1] ! (B ! match A a)) = match (A[B ! match A a := A ! (B ! match A a) + 1]) (B ! match A a)) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! (B ! match A a) \<longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> P\<^sub>a ! a ! (A[a := A ! a + 1] ! a) = match (A[a := A ! a + 1]) a)
[PROOF STEP]
unfolding invar2_def match_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>invAM A ({<ai + 1} - {a}) \<and> ((ran (\<alpha> B M) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A ! a) = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n; M ! b; b = P\<^sub>a ! a ! (A ! a)\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! (B ! b) \<longrightarrow> (invAM (A[B ! b := A ! (B ! b) + 1]) ({<ai + 1} - {B ! b}) \<and> ((ran (\<alpha> (B[b := a]) M) = {<ai + 1} - {B ! b} \<and> (\<forall>b a. \<alpha> (B[b := a]) M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A[B ! b := A ! (B ! b) + 1] ! a) = b)) \<and> length (B[b := a]) = n \<and> length M = n) \<and> B ! b \<le> ai \<and> ai < n) \<and> var (A[B ! b := A ! (B ! b) + 1]) {<ai} < var A {<ai}) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! (B ! b) \<longrightarrow> (invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> ((ran (\<alpha> B M) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A[a := A ! a + 1] ! a) = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> var (A[a := A ! a + 1]) {<ai} < var A {<ai})

goal (1 subgoal):
 1. \<lbrakk>(invAM A ({<ai + 1} - {a}) \<and> ((ran (\<alpha> B M) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A ! a) = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> b = P\<^sub>a ! a ! (A ! a); M ! (P\<^sub>a ! a ! (A ! a))\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! (B ! (P\<^sub>a ! a ! (A ! a))) \<longrightarrow> (invAM (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1]) ({<ai + 1} - {B ! (P\<^sub>a ! a ! (A ! a))}) \<and> ((ran (\<alpha> (B[P\<^sub>a ! a ! (A ! a) := a]) M) = {<ai + 1} - {B ! (P\<^sub>a ! a ! (A ! a))} \<and> (\<forall>b a. \<alpha> (B[P\<^sub>a ! a ! (A ! a) := a]) M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1] ! a) = b)) \<and> length (B[P\<^sub>a ! a ! (A ! a) := a]) = n \<and> length M = n) \<and> B ! (P\<^sub>a ! a ! (A ! a)) \<le> ai \<and> ai < n) \<and> P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1] ! (B ! (P\<^sub>a ! a ! (A ! a)))) = P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1] ! (B ! (P\<^sub>a ! a ! (A ! a))))) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! (B ! (P\<^sub>a ! a ! (A ! a))) \<longrightarrow> (invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> ((ran (\<alpha> B M) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A[a := A ! a + 1] ! a) = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> P\<^sub>a ! a ! (A[a := A ! a + 1] ! a) = P\<^sub>a ! a ! (A[a := A ! a + 1] ! a))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a

goal (1 subgoal):
 1. (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
[PROOF STEP]
using inv
[PROOF STATE]
proof (prove)
using this:
case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
case s of (A, B, a, x) \<Rightarrow> M ! x

goal (1 subgoal):
 1. (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})
[PROOF STEP]
apply(simp only: s prod.case Let_def in_measure split: if_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar2 A B M ai a \<and> b = match A a; M ! match A a\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! (B ! match A a) \<longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < var A {<ai}) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! (B ! match A a) \<longrightarrow> var (A[a := A ! a + 1]) {<ai} < var A {<ai})
[PROOF STEP]
using inner_pres[OF R _ _ refl refl refl refl refl, of A B M ai a b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>invar2 A B M ai a; M ! b; b = match A a\<rbrakk> \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> invar2 (A[B ! b := A ! (B ! b) + 1]) (B[b := a]) M ai (B ! b) \<and> var (A[B ! b := A ! (B ! b) + 1]) {<ai} < var A {<ai}) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> invar2 (A[a := A ! a + 1]) B M ai a \<and> var (A[a := A ! a + 1]) {<ai} < var A {<ai})

goal (1 subgoal):
 1. \<lbrakk>invar2 A B M ai a \<and> b = match A a; M ! match A a\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! (B ! match A a) \<longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) {<ai} < var A {<ai}) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! match A a) ! (A ! (B ! match A a))) ! (B ! match A a) \<longrightarrow> var (A[a := A ! a + 1]) {<ai} < var A {<ai})
[PROOF STEP]
unfolding invar2_def match_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>invAM A ({<ai + 1} - {a}) \<and> ((ran (\<alpha> B M) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A ! a) = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n; M ! b; b = P\<^sub>a ! a ! (A ! a)\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! (B ! b) \<longrightarrow> (invAM (A[B ! b := A ! (B ! b) + 1]) ({<ai + 1} - {B ! b}) \<and> ((ran (\<alpha> (B[b := a]) M) = {<ai + 1} - {B ! b} \<and> (\<forall>b a. \<alpha> (B[b := a]) M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A[B ! b := A ! (B ! b) + 1] ! a) = b)) \<and> length (B[b := a]) = n \<and> length M = n) \<and> B ! b \<le> ai \<and> ai < n) \<and> var (A[B ! b := A ! (B ! b) + 1]) {<ai} < var A {<ai}) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! b) ! (A ! (B ! b))) ! (B ! b) \<longrightarrow> (invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> ((ran (\<alpha> B M) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A[a := A ! a + 1] ! a) = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> var (A[a := A ! a + 1]) {<ai} < var A {<ai})

goal (1 subgoal):
 1. \<lbrakk>(invAM A ({<ai + 1} - {a}) \<and> ((ran (\<alpha> B M) = {<ai + 1} - {a} \<and> (\<forall>b a. \<alpha> B M b = Some a \<longrightarrow> P\<^sub>a ! a ! (A ! a) = b)) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n) \<and> b = P\<^sub>a ! a ! (A ! a); M ! (P\<^sub>a ! a ! (A ! a))\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! (B ! (P\<^sub>a ! a ! (A ! a))) \<longrightarrow> var (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1]) {<ai} < var A {<ai}) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! (B ! (P\<^sub>a ! a ! (A ! a))) \<longrightarrow> var (A[a := A ! a + 1]) {<ai} < var A {<ai})
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(case case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)) of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a) \<and> (case s of (A, B, a, b) \<Rightarrow> let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')); (A, B, a) = if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], a') else (A[a := A ! a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)), s) \<in> measure (\<lambda>(A, B, a, b). var A {<ai})

goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 2. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 2. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
case s_ of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a
\<not> (case s_ of (A, B, a, x) \<Rightarrow> M ! x)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, a, b) \<Rightarrow> invar2 A B M ai a \<and> b = match A a; \<not> (case s of (A, B, a, x) \<Rightarrow> M ! x)\<rbrakk> \<Longrightarrow> s = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
 2. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s_ = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
[PROOF STEP]
proof (rule, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s_ = (A', B', a', b') \<Longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
s_ = (A', B', a', b')

goal (1 subgoal):
 1. s_ = (A', B', a', b') \<Longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)
[PROOF STEP]
by(rule inner_to_outer[OF 3[unfolded 1 prod.case]])
[PROOF STATE]
proof (state)
this:
invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s_ = (A', B', a', b') \<longrightarrow> invar1 A' (B'[b' := a']) (M[b' := True]) (ai + 1)

goal (1 subgoal):
 1. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Wellfounded.wf (measure (\<lambda>(A, B, a, b). var A {<ai}))

goal:
No subgoals!
[PROOF STEP]
qed