[STATEMENT]
lemma Gale_Shapley4_1: "VARS A B a a' ai b
 [ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> B = (\<lambda>_. None)]
 WHILE ai < n
 INV { invAM A ({<ai+1} - {a}) \<and> invAB A B ({<ai+1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai=n \<longrightarrow> a=ai)}
 VAR {var A ({<ai+1} - {a})}
 DO b := match A a;
  IF B b = None
  THEN B := B(b := Some a); ai := ai + 1; a := ai
  ELSE a' := the(B b);
       IF P\<^sub>b ! match A a' \<turnstile> a < a'
       THEN B := B(b := Some a); A[a'] := A!a'+1; a := a'
       ELSE A[a] := A!a+1
       FI
  FI
 OD
 [matching A {<n} \<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> B = Map.empty]
WHILE ai < n INV {invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)}  VAR {var A ({<ai + 1} - {a})}
DO b := match A a; IF B b = None THEN B := B(b \<mapsto> a); ai := ai + 1; a := ai  ELSE a' := the (B b); IF P\<^sub>b ! match A a' \<turnstile> a < a' THEN B := B(b \<mapsto> 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 a a' ai b. ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> B = Map.empty \<Longrightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)
 2. \<And>na A B a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 3. \<And>A B a a' ai b. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
ai_ = 0 \<and> a_ = 0 \<and> A_ = replicate n 0 \<and> B_ = Map.empty

goal (3 subgoals):
 1. \<And>A B a a' ai b. ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> B = Map.empty \<Longrightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)
 2. \<And>na A B a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 3. \<And>A B a a' ai b. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ai_ = 0 \<and> a_ = 0 \<and> A_ = replicate n 0 \<and> B_ = Map.empty

goal (1 subgoal):
 1. invAM A_ ({<ai_ + 1} - {a_}) \<and> invAB A_ B_ ({<ai_ + 1} - {a_}) \<and> (a_ \<le> ai_ \<and> ai_ \<le> n) \<and> (ai_ = n \<longrightarrow> a_ = ai_)
[PROOF STEP]
by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def)
[PROOF STATE]
proof (state)
this:
invAM A_ ({<ai_ + 1} - {a_}) \<and> invAB A_ B_ ({<ai_ + 1} - {a_}) \<and> (a_ \<le> ai_ \<and> ai_ \<le> n) \<and> (ai_ = n \<longrightarrow> a_ = ai_)

goal (2 subgoals):
 1. \<And>na A B a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 2. \<And>A B a a' ai b. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>na A B a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 2. \<And>A B a a' ai b. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<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:
(invAM A_ ({<ai_ + 1} - {a_}) \<and> invAB A_ B_ ({<ai_ + 1} - {a_}) \<and> (a_ \<le> ai_ \<and> ai_ \<le> n) \<and> (ai_ = n \<longrightarrow> a_ = ai_)) \<and> \<not> ai_ < n

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

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

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
using atLeast0_lessThan_Suc
[PROOF STATE]
proof (prove)
using this:
(invAM A_ ({<ai_ + 1} - {a_}) \<and> invAB A_ B_ ({<ai_ + 1} - {a_}) \<and> (a_ \<le> ai_ \<and> ai_ \<le> n) \<and> (ai_ = n \<longrightarrow> a_ = ai_)) \<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 a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na A B a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
case (2 v A B a a' ai b)
[PROOF STATE]
proof (state)
this:
((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = v

goal (1 subgoal):
 1. \<And>na A B a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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 a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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 "a \<le> ai"
    and v: "var A ?M = v" and as: "a \<le> ai \<and> ai < n" and invAB: "invAB A B ?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}) &&& a \<le> ai) &&& var A ({<ai + 1} - {a}) = v &&& a \<le> ai \<and> ai < n &&& invAB A B ({<ai + 1} - {a})
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<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}) &&& a \<le> ai) &&& var A ({<ai + 1} - {a}) = v &&& a \<le> ai \<and> ai < n &&& invAB A B ({<ai + 1} - {a})
[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})
a \<le> ai
var A ({<ai + 1} - {a}) = v
a \<le> ai \<and> ai < n
invAB A B ({<ai + 1} - {a})

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

goal (1 subgoal):
 1. \<And>na A B a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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 a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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 a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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 a a' ai b. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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. (B (match A a) = None \<longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (B (match A a) \<noteq> None \<longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. B (match A a) = None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
assume ?not_matched
[PROOF STATE]
proof (state)
this:
B (match A a) = None

goal (2 subgoals):
 1. B (match A a) = None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B (match A a) = None
[PROOF STEP]
have nm: "match A a \<notin> match A ` ?M"
[PROOF STATE]
proof (prove)
using this:
B (match A a) = None

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<ai + 1} - {a})
[PROOF STEP]
using invAB
[PROOF STATE]
proof (prove)
using this:
B (match A a) = None
invAB A B ({<ai + 1} - {a})

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

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>B (match A x) = None; \<forall>x. (\<exists>a. B a = Some x) = (x < Suc ai \<and> x \<noteq> a); \<forall>b a. B b = Some a \<longrightarrow> match A a = b; match A a = match A x; x < Suc ai\<rbrakk> \<Longrightarrow> x = a
[PROOF STEP]
using not_None_eq
[PROOF STATE]
proof (prove)
using this:
(?x \<noteq> None) = (\<exists>y. ?x = Some y)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>B (match A x) = None; \<forall>x. (\<exists>a. B a = Some x) = (x < Suc ai \<and> x \<noteq> a); \<forall>b a. B b = Some a \<longrightarrow> match A a = b; match A a = match A x; x < Suc ai\<rbrakk> \<Longrightarrow> x = a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
match A a \<notin> match A ` ({<ai + 1} - {a})

goal (2 subgoals):
 1. B (match A a) = None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B(match A a \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> 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. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> 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 \<open>a \<le> ai\<close>
[PROOF STATE]
proof (prove)
using this:
a \<le> ai

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. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> 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. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> ai + 1 = ai + 1)
 2. var A ({<ai + 1 + 1} - {ai + 1}) < v
[PROOF STEP]
have invAB': "invAB A (B(match A a := Some a)) {<ai+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB A (B(match A a \<mapsto> a)) {<ai + 1}
[PROOF STEP]
using invAB \<open>?not_matched\<close> **
[PROOF STATE]
proof (prove)
using this:
invAB A B ({<ai + 1} - {a})
B (match A a) = None
{<ai + 1} - {a} \<union> {a} = {<ai + 1}

goal (1 subgoal):
 1. invAB A (B(match A a \<mapsto> a)) {<ai + 1}
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
invAB A (B(match A a \<mapsto> a)) {<ai + 1}

goal (2 subgoals):
 1. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> 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. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> 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. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> 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 (B(match A a \<mapsto> a)) {<ai + 1}
{<ai + 1 + 1} - {ai + 1} = {<ai + 1}

goal (1 subgoal):
 1. invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> ai + 1 = ai + 1)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1 + 1} - {ai + 1}) \<and> invAB A (B(match A a \<mapsto> a)) ({<ai + 1 + 1} - {ai + 1}) \<and> (ai + 1 \<le> ai + 1 \<and> ai + 1 \<le> n) \<and> (ai + 1 = n \<longrightarrow> 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 \<mapsto> a), ai + 1, a', ai + 1, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)

goal (1 subgoal):
 1. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
assume matched: "\<not> ?not_matched"
[PROOF STATE]
proof (state)
this:
B (match A a) \<noteq> None

goal (1 subgoal):
 1. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B (match A a) \<noteq> None
[PROOF STEP]
obtain a' where a'eq: "B(match A a) = Some a'"
[PROOF STATE]
proof (prove)
using this:
B (match A a) \<noteq> None

goal (1 subgoal):
 1. (\<And>a'. B (match A a) = Some a' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B (match A a) = Some a'

goal (1 subgoal):
 1. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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. a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a
[PROOF STEP]
using a'eq invAB
[PROOF STATE]
proof (prove)
using this:
B (match A a) = Some a'
invAB A B ({<ai + 1} - {a})

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

goal (1 subgoal):
 1. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
hence "a' < n" "a \<noteq> a'"
[PROOF STATE]
proof (prove)
using this:
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a

goal (1 subgoal):
 1. a' < n &&& a \<noteq> a'
[PROOF STEP]
using a M atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
a' \<in> {<ai + 1} - {a} \<and> 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. a' < n &&& a \<noteq> a'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a' < n
a \<noteq> a'

goal (1 subgoal):
 1. B (match A a) \<noteq> None \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), the (B (match A a)), the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, a, the (B (match A a)), ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
unfolding a'eq option.sel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
have inj_dom: "inj_on B (dom B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on B (dom B)
[PROOF STEP]
by (metis (mono_tags) domD inj_onI invAB)
[PROOF STATE]
proof (state)
this:
inj_on B (dom B)

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

goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
show ?case (is "(?pref \<longrightarrow> ?THEN) \<and> (\<not> ?pref \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
assume ?pref
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A a' \<turnstile> a < a'

goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[a' := A ! a' + 1], B(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)
 2. var (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) < v
[PROOF STEP]
have *: "{<ai + 1} - {a} - {a'} \<union> {a} = {<ai + 1} - {a'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} - {a'} \<union> {a} = {<ai + 1} - {a'}
[PROOF STEP]
using a a' as
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<ai + 1} - {a}
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a
a \<le> ai \<and> ai < n

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

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

goal (1 subgoal):
 1. \<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a' \<noteq> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a' \<noteq> x

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)
 2. var (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) < v
[PROOF STEP]
have invAB': "invAB (A[a' := A ! a' + 1]) (B(match A a := Some a)) ({<ai + 1} - {a'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'})
[PROOF STEP]
using invAB_swap[OF invAB a a' inj_dom a'eq] *
[PROOF STATE]
proof (prove)
using this:
invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a} - {a'} \<union> {a})
{<ai + 1} - {a} - {a'} \<union> {a} = {<ai + 1} - {a'}

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

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)
 2. var (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)
 2. var (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)
[PROOF STEP]
using invAM_swap[OF invAM a a' \<open>?pref\<close>] invAB'
[PROOF STATE]
proof (prove)
using this:
invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a} - {a'} \<union> {a})
invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'})

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

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)
[PROOF STEP]
using a' as
[PROOF STATE]
proof (prove)
using this:
invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'})
invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'})
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a' = ai)

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]
have "card({<ai + 1} - {a'}) = card({<ai + 1} - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({<ai + 1} - {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}
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a
a \<le> ai \<and> ai < n

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

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

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) < v
[PROOF STEP]
using v var_next[OF m M _ pref_match1, of a'] \<open>a' < n\<close> a atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
card ({<ai + 1} - {a'}) = card ({<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})
a' < n
a < n \<and> a \<notin> {<ai + 1} - {a}
{<?n} = {..<?n}

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) < v
[PROOF STEP]
by (metis Suc_eq_plus1 lessThan_iff var_def)
[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(match A a \<mapsto> a), a', a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)

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

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<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. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)
 2. var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

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

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

goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)
 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]) B ({<ai + 1} - {a})

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)
[PROOF STEP]
using invAM_next[OF invAM a a' \<open>\<not> ?pref\<close>]
[PROOF STATE]
proof (prove)
using this:
invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a})
invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)
[PROOF STEP]
using "2"
[PROOF STATE]
proof (prove)
using this:
invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a})
invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})
((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = v

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)

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, a, a', ai, match A a) \<in> _Collect s ((case s of (A, B, a, a', ai, b) \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai \<le> n) \<and> (ai = n \<longrightarrow> a = ai)) \<and> (case s of (A, B, a, a', ai, b) \<Rightarrow> var A ({<ai + 1} - {a})) < v)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<alpha>_Some[simp]: "\<alpha> B M b = Some a \<longleftrightarrow> b < n \<and> M!b \<and> a = B!b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<alpha> B M b = Some a) = (b < n \<and> M ! b \<and> a = B ! b)
[PROOF STEP]
by(auto simp add: \<alpha>_def)


[STATEMENT]
lemma \<alpha>update1: "\<lbrakk> \<not> M ! b; b < length B; b < length M; n = length M \<rbrakk>
 \<Longrightarrow> ran(\<alpha> (B[b := a]) (M[b := True])) = ran(\<alpha> B M) \<union> {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> M ! b; b < length B; b < length M; n = length M\<rbrakk> \<Longrightarrow> ran (\<alpha> (B[b := a]) (M[b := True])) = ran (\<alpha> B M) \<union> {a}
[PROOF STEP]
by(force simp add: \<alpha>_def ran_def nth_list_update)


[STATEMENT]
lemma \<alpha>update2: "\<lbrakk> M!b; b < length B; b < length M; length M = n \<rbrakk>
 \<Longrightarrow> \<alpha> (B[b := a]) M = (\<alpha> B M)(b := Some a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M ! b; b < length B; b < length M; length M = n\<rbrakk> \<Longrightarrow> \<alpha> (B[b := a]) M = \<alpha> B M(b \<mapsto> a)
[PROOF STEP]
by(force simp add: \<alpha>_def nth_list_update)