[STATEMENT]
lemma Gale_Shapley2: "VARS A a a' as
 [as = [0..<n] \<and> A = replicate n 0]
 WHILE as \<noteq> []
 INV { invAM A ({<n} - set as) \<and> invas as}
 VAR {var A ({<n} - set as)}
 DO a := hd as;
  IF match A a \<notin> match A ` ({<n} - set as)
  THEN as := tl as
  ELSE a' := (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A a);
       IF P\<^sub>b ! match A a' \<turnstile> a < a'
       THEN A[a'] := A!a'+1; as := a' # tl as
       ELSE A[a] := A!a+1
       FI
  FI
 OD
 [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [as = [0..<n] \<and> A = replicate n 0]
WHILE as \<noteq> [] INV {invAM A ({<n} - set as) \<and> invas as}  VAR {var A ({<n} - set as)}
DO a := hd as; IF match A a \<notin> match A ` ({<n} - set as) THEN as := tl as  ELSE a' := (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A a); IF P\<^sub>b ! match A a' \<turnstile> a < a' THEN A := A[a' := A ! a' + 1]; as := a' # tl as  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 a a' as. as = [0..<n] \<and> A = replicate n 0 \<Longrightarrow> invAM A ({<n} - set as) \<and> invas as
 2. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
 3. \<And>A a a' as. (invAM A ({<n} - set as) \<and> invas as) \<and> \<not> as \<noteq> [] \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
as_ = [0..<n] \<and> A_ = replicate n 0

goal (3 subgoals):
 1. \<And>A a a' as. as = [0..<n] \<and> A = replicate n 0 \<Longrightarrow> invAM A ({<n} - set as) \<and> invas as
 2. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
 3. \<And>A a a' as. (invAM A ({<n} - set as) \<and> invas as) \<and> \<not> as \<noteq> [] \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
as_ = [0..<n] \<and> A_ = replicate n 0

goal (1 subgoal):
 1. invAM A_ ({<n} - set as_) \<and> invas as_
[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_ ({<n} - set as_) \<and> invas as_

goal (2 subgoals):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
 2. \<And>A a a' as. (invAM A ({<n} - set as) \<and> invas as) \<and> \<not> as \<noteq> [] \<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 a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
 2. \<And>A a a' as. (invAM A ({<n} - set as) \<and> invas as) \<and> \<not> as \<noteq> [] \<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_ ({<n} - set as_) \<and> invas as_) \<and> \<not> as_ \<noteq> []

goal (2 subgoals):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
 2. \<And>A a a' as. (invAM A ({<n} - set as) \<and> invas as) \<and> \<not> as \<noteq> [] \<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_ ({<n} - set as_) \<and> invas as_) \<and> \<not> as_ \<noteq> []

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_ ({<n} - set as_) \<and> invas as_) \<and> \<not> as_ \<noteq> []
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
by auto
[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 a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
case (2 v A _ a' as)
[PROOF STATE]
proof (state)
this:
((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = v

goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
let ?M = "{<n} - set as"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
have "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M \<subseteq> {<n}"
    and pref_match: "pref_match A ?M" and "opti\<^sub>a A" and "as \<noteq> []" and v: "var A ?M = v"
    and as: "invas as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((invAM A ({<n} - set as) &&& matching A ({<n} - set as)) &&& local.wf A &&& {<n} - set as \<subseteq> {<n}) &&& (pref_match A ({<n} - set as) &&& opti\<^sub>a A) &&& as \<noteq> [] &&& var A ({<n} - set as) = v &&& invas as
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = v

goal (1 subgoal):
 1. ((invAM A ({<n} - set as) &&& matching A ({<n} - set as)) &&& local.wf A &&& {<n} - set as \<subseteq> {<n}) &&& (pref_match A ({<n} - set as) &&& opti\<^sub>a A) &&& as \<noteq> [] &&& var A ({<n} - set as) = v &&& invas as
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invAM A ({<n} - set as)
matching A ({<n} - set as)
local.wf A
{<n} - set as \<subseteq> {<n}
pref_match A ({<n} - set as)
opti\<^sub>a A
as \<noteq> []
var A ({<n} - set as) = v
invas as

goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
[PROOF STATE]
proof (state)
this:
pref_match' A ({<n} - set as)

goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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 ({<n} - set as)

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

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

goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
from \<open>as \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
[PROOF STEP]
obtain a as' where aseq: "as = a # as'"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []

goal (1 subgoal):
 1. (\<And>a as'. as = a # as' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
as = a # as'

goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
have set_as: "?M \<union> {a} = {<n} - set as'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<n} - set as \<union> {a} = {<n} - set as'
[PROOF STEP]
using as aseq
[PROOF STATE]
proof (prove)
using this:
invas as
as = a # as'

goal (1 subgoal):
 1. {<n} - set as \<union> {a} = {<n} - set as'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{<n} - set as \<union> {a} = {<n} - set as'

goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
have a: "a < n \<and> a \<notin> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < n \<and> a \<notin> {<n} - set as
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
invas as

goal (1 subgoal):
 1. a < n \<and> a \<notin> {<n} - set as
[PROOF STEP]
unfolding aseq
[PROOF STATE]
proof (prove)
using this:
invas (a # as')

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

goal (1 subgoal):
 1. \<And>na A a a' as. ((invAM A ({<n} - set as) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)))
[PROOF STEP]
proof (simp only: aseq list.sel, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (match A a \<notin> match A ` ({<n} - set (a # as')) \<longrightarrow> (A, a, a', as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

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

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

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<n} - set as)
[PROOF STEP]
unfolding aseq
[PROOF STATE]
proof (prove)
using this:
match A a \<notin> match A ` ({<n} - set (a # as'))

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<n} - set (a # as'))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
match A a \<notin> match A ` ({<n} - set as)

goal (2 subgoals):
 1. match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (A, a, a', as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)
 2. \<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, a, a', as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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 ({<n} - set as') \<and> invas as'
 2. var A ({<n} - set as') < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM A ({<n} - set as') \<and> invas as'
 2. var A ({<n} - set as') < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM A ({<n} - set as') \<and> invas as'
[PROOF STEP]
using invAM_match[OF \<open>invAM A ?M\<close> a nm] as
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as \<union> {a})
invas as

goal (1 subgoal):
 1. invAM A ({<n} - set as') \<and> invas as'
[PROOF STEP]
unfolding set_as
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as')
invas as

goal (1 subgoal):
 1. invAM A ({<n} - set as') \<and> invas as'
[PROOF STEP]
by (simp add: aseq)
[PROOF STATE]
proof (state)
this:
invAM A ({<n} - set as') \<and> invas as'

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

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

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

goal (1 subgoal):
 1. var A ({<n} - set as') < v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
var A ({<n} - set as') < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A, a, a', as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
assume matched: "\<not> ?not_matched"
[PROOF STATE]
proof (state)
this:
\<not> match A a \<notin> match A ` ({<n} - set (a # as'))

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
define a' where "a' = (SOME a'.  a' \<in> ?M \<and> match A a' = match A a)"
[PROOF STATE]
proof (state)
this:
a' = (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A a)

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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> {<n} - set as \<and> match A a' = match A a
[PROOF STEP]
unfolding a'_def aseq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<in> {<n} - set (a # as') \<and> match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) = match A a
[PROOF STEP]
using matched
[PROOF STATE]
proof (prove)
using this:
\<not> match A a \<notin> match A ` ({<n} - set (a # as'))

goal (1 subgoal):
 1. (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<in> {<n} - set (a # as') \<and> match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) = match A a
[PROOF STEP]
by (smt (verit) image_iff someI_ex)
[PROOF STATE]
proof (state)
this:
a' \<in> {<n} - set as \<and> match A a' = match A a

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
hence "a' < n" "a \<noteq> a'"
[PROOF STATE]
proof (prove)
using this:
a' \<in> {<n} - set as \<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> {<n} - set as \<and> match A a' = match A a
a < n \<and> a \<notin> {<n} - set as
{<n} - set as \<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. \<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
unfolding aseq[symmetric] a'_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[a' := A ! a' + 1], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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]) ({<n} - set (a' # as')) \<and> invas (a' # as')
 2. var (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) < v
[PROOF STEP]
have *: "{<n} - set as - {a'} \<union> {a} = {<n} - set (a' # as')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<n} - set as - {a'} \<union> {a} = {<n} - set (a' # as')
[PROOF STEP]
using a a' as aseq
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<n} - set as
a' \<in> {<n} - set as \<and> match A a' = match A a
invas as
as = a # as'

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

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) \<and> invas (a' # as')
 2. var (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) \<and> invas (a' # as')
 2. var (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) \<and> invas (a' # as')
[PROOF STEP]
using invAM_swap[OF \<open>invAM A ?M\<close> a a' \<open>?pref\<close>]
[PROOF STATE]
proof (prove)
using this:
invAM (A[a' := A ! a' + 1]) ({<n} - set as - {a'} \<union> {a})

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) \<and> invas (a' # as')
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as'))

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) \<and> invas (a' # as')
[PROOF STEP]
using a' as aseq
[PROOF STATE]
proof (prove)
using this:
invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as'))
a' \<in> {<n} - set as \<and> match A a' = match A a
invas as
as = a # as'

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) \<and> invas (a' # as')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
invAM (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) \<and> invas (a' # as')

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

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

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

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

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) < 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 ({<n} - set as) = card ({<n} - set (a' # as'))
var A ({<n} - set as) = v
\<lbrakk>{<n} - set as \<noteq> {<n}; a' < n\<rbrakk> \<Longrightarrow> var (A[a' := A ! a' + 1]) ({<n} - set as) < var A ({<n} - set as)
a' < n
a < n \<and> a \<notin> {<n} - set as
{<?n} = {..<?n}

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) < v
[PROOF STEP]
by (metis Suc_eq_plus1 lessThan_iff var_def)
[PROOF STATE]
proof (state)
this:
var (A[a' := A ! a' + 1]) ({<n} - set (a' # as')) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A[a' := A ! a' + 1], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)

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

goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) ({<n} - set as) \<and> invas as
 2. var (A[a := A ! a + 1]) ({<n} - set as) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<n} - set as) \<and> invas as
[PROOF STEP]
using invAM_next[OF \<open>invAM A ?M\<close> a a' \<open>\<not> ?pref\<close>] as
[PROOF STATE]
proof (prove)
using this:
invAM (A[a := A ! a + 1]) ({<n} - set as)
invas as

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<n} - set as) \<and> invas as
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invAM (A[a := A ! a + 1]) ({<n} - set as) \<and> invas as

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

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<n} - set as) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<n} - set as) < 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> {<n} - set as
var A ({<n} - set as) = v
\<lbrakk>{<n} - set as \<noteq> {<n}; a < n\<rbrakk> \<Longrightarrow> var (A[a := A ! a + 1]) ({<n} - set as) < var A ({<n} - set as)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < 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], a, a', a' # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], a, a', as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(match A a \<notin> match A ` ({<n} - set (a # as')) \<longrightarrow> (A, a, a', as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> match A a \<notin> match A ` ({<n} - set (a # as')) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a := A ! (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a) \<longrightarrow> (A[a := A ! a + 1], a, SOME a'. a' \<in> {<n} - set (a # as') \<and> match A a' = match A a, a # as') \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (A, hd as, a', tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> match A (hd as) \<notin> match A ` ({<n} - set as) \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as) := A ! (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) # tl as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<turnstile> hd as < (SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as)) \<longrightarrow> (A[hd as := A ! hd as + 1], hd as, SOME a'. a' \<in> {<n} - set as \<and> match A a' = match A (hd as), as) \<in> _Collect s ((case s of (A, a, a', as) \<Rightarrow> invAM A ({<n} - set as) \<and> invas as) \<and> (case s of (A, a, a', as) \<Rightarrow> var A ({<n} - set as)) < v)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invAB_swap:
assumes invAB: "invAB A B M"
assumes a: "a < n \<and> a \<notin> M" and a': "a' \<in> M \<and> match A a' = match A a"
  and "inj_on B (dom B)" "B(match A a) = Some a'"
shows "invAB (A[a' := A!a'+1]) (B(match A a := Some a)) (M - {a'} \<union> {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) (M - {a'} \<union> {a})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) (M - {a'} \<union> {a})
[PROOF STEP]
have "\<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 M
a' \<in> M \<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 (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) (M - {a'} \<union> {a})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a' \<noteq> x

goal (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) (M - {a'} \<union> {a})
[PROOF STEP]
have "a \<noteq> a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> a'
[PROOF STEP]
using a a'
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a

goal (1 subgoal):
 1. a \<noteq> a'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<noteq> a'

goal (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) (M - {a'} \<union> {a})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a' \<noteq> x
a \<noteq> a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a' \<noteq> x
a \<noteq> a'

goal (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) (M - {a'} \<union> {a})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>b x. b \<noteq> match A a \<longrightarrow> B b = Some x \<longrightarrow> a' \<noteq> x
a \<noteq> a'
invAB A B M
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a
inj_on B (dom B)
B (match A a) = Some a'

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

goal:
No subgoals!
[PROOF STEP]
qed