[STATEMENT]
lemma gs: assumes "R\<^sub>b = map ranking P\<^sub>b"
shows "gs n P\<^sub>a R\<^sub>b = (A,BMai) \<longrightarrow> matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs n P\<^sub>a R\<^sub>b = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
unfolding gs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while (\<lambda>(A, B, M, ai). ai < n) (\<lambda>(A, B, M, ai). let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1)) (replicate n 0, replicate n 0, replicate n False, 0) = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
proof(rule while_rule2[where P = "\<lambda>(A,B,M,ai). invar1 A B M ai"
  and r = "measure(\<lambda>(A,B,M,ai). n - ai)"], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. case (replicate n 0, replicate n 0, replicate n False, 0) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; case s of (A, B, M, ai) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
 3. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 4. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. case (replicate n 0, replicate n 0, replicate n False, 0) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; case s of (A, B, M, ai) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
 3. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 4. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (replicate n 0, replicate n 0, replicate n False, 0) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
[PROOF STEP]
by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
[PROOF STATE]
proof (state)
this:
case (replicate n 0, replicate n 0, replicate n False, 0) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; case s of (A, B, M, ai) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; case s of (A, B, M, ai) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
case (2 s)
[PROOF STATE]
proof (state)
this:
case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
case s of (A, B, M, ai) \<Rightarrow> ai < n

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; case s of (A, B, M, ai) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
obtain A B M ai where s: "s =  (A, B, M, ai)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B M ai. s = (A, B, M, ai) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases4
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c d. ?y = (a, b, c, d) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; case s of (A, B, M, ai) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
have 1: "invar2 A B M ai ai"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2 A B M ai ai
[PROOF STEP]
using 2 s
[PROOF STATE]
proof (prove)
using this:
case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
case s of (A, B, M, ai) \<Rightarrow> ai < n
s = (A, B, M, ai)

goal (1 subgoal):
 1. invar2 A B M ai ai
[PROOF STEP]
by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
[PROOF STATE]
proof (state)
this:
invar2 A B M ai ai

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; case s of (A, B, M, ai) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
[PROOF STEP]
using 2 s gs_inner[OF \<open>R\<^sub>b = _ \<close> 1]
[PROOF STATE]
proof (prove)
using this:
case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
case s of (A, B, M, ai) \<Rightarrow> ai < n
s = (A, B, M, ai)
?b = match A ai \<Longrightarrow> gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, ?b) = (?A', ?B', ?a', ?b') \<longrightarrow> invar1 ?A' (?B'[?b' := ?a']) (M[?b' := True]) (ai + 1)

goal (1 subgoal):
 1. (case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)
[PROOF STEP]
by (auto simp: match_def simp del: invar1_def split: prod.split)
[PROOF STATE]
proof (state)
this:
(case case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1) of (A, B, M, ai) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai) \<Rightarrow> let (A, B, a, b) = gs_inner P\<^sub>a R\<^sub>b M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b := a], M[b := True], ai + 1), s) \<in> measure (\<lambda>(A, B, M, ai). n - ai)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 2. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 2. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
case s_ of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
\<not> (case s_ of (A, B, M, ai) \<Rightarrow> ai < n)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai) \<Rightarrow> invar1 A B M ai; \<not> (case s of (A, B, M, ai) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 2. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
case s_ of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
\<not> (case s_ of (A, B, M, ai) \<Rightarrow> ai < n)

goal (1 subgoal):
 1. s_ = (A, BMai) \<longrightarrow> 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:
case s_ of (A, B, M, ai) \<Rightarrow> invar1 A B M ai
\<not> (case s_ of (A, B, M, ai) \<Rightarrow> ai < n)
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}

goal (1 subgoal):
 1. s_ = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s_ = (A, BMai) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A

goal (1 subgoal):
 1. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Wellfounded.wf (measure (\<lambda>(A, B, M, ai). n - ai))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (4 subgoals):
 1. case (replicate n 0, replicate n 0, replicate n False, 0, 0) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; case s of (A, B, M, ai, a) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a), s) \<in> measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a}))
 3. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 4. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (replicate n 0, replicate n 0, replicate n False, 0, 0) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a
[PROOF STEP]
by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
[PROOF STATE]
proof (state)
this:
case (replicate n 0, replicate n 0, replicate n False, 0, 0) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a

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

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

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

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; case s of (A, B, M, ai, a) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a), s) \<in> measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a}))
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
hence 1: "invar2' A B M ai a" "ai < n"
[PROOF STATE]
proof (prove)
using this:
s = (A, B, M, ai, a)

goal (1 subgoal):
 1. invar2' A B M ai a &&& ai < n
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
s = (A, B, M, ai, a)
case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a
case s of (A, B, M, ai, a) \<Rightarrow> ai < n

goal (1 subgoal):
 1. invar2' A B M ai a &&& ai < n
[PROOF STEP]
by (simp_all)
[PROOF STATE]
proof (state)
this:
invar2' A B M ai a
ai < n

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; case s of (A, B, M, ai, a) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a), s) \<in> measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a}))
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
have R': "M ! match A a \<Longrightarrow>
    (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) =
     (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
using R_iff_P[OF assms 1]
[PROOF STATE]
proof (prove)
using this:
M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)

goal (1 subgoal):
 1. M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)

goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; case s of (A, B, M, ai, a) \<Rightarrow> ai < n\<rbrakk> \<Longrightarrow> (case case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a), s) \<in> measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a}))
 2. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 3. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a), s) \<in> measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a}))
[PROOF STEP]
using 1 R' pres2'[OF 1]
[PROOF STATE]
proof (prove)
using this:
invar2' A B M ai a
ai < n
M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
\<lbrakk>var A ({<ai + 1} - {a}) = ?v; ?b = match A a; ?a' = B ! ?b; ?A1.0 = A[?a' := A ! ?a' + 1]; ?A2.0 = A[a := A ! a + 1]\<rbrakk> \<Longrightarrow> (\<not> M ! ?b \<longrightarrow> invar2' A (B[?b := a]) (M[?b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < ?v) \<and> (M ! ?b \<longrightarrow> (P\<^sub>b ! match A ?a' \<turnstile> a < ?a' \<longrightarrow> invar2' ?A1.0 (B[?b := a]) M ai ?a' \<and> var ?A1.0 ({<ai + 1} - {?a'}) < ?v) \<and> (\<not> P\<^sub>b ! match A ?a' \<turnstile> a < ?a' \<longrightarrow> invar2' ?A2.0 B M ai a \<and> var ?A2.0 ({<ai + 1} - {a}) < ?v))

goal (1 subgoal):
 1. (case case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a), s) \<in> measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a}))
[PROOF STEP]
apply(simp only: s mem_Collect_eq prod.case Let_def in_measure match_def split: if_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar2' A B M ai a; ai < n; M ! (P\<^sub>a ! a ! (A ! a)) \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! (B ! (P\<^sub>a ! a ! (A ! a)))) = (P\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) \<turnstile> a < B ! (P\<^sub>a ! a ! (A ! a))); \<And>v b a' A1 A2. \<lbrakk>var A ({<ai + 1} - {a}) = v; b = P\<^sub>a ! a ! (A ! a); a' = B ! (P\<^sub>a ! a ! (A ! a)); A1 = A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1]; A2 = A[a := A ! a + 1]\<rbrakk> \<Longrightarrow> (\<not> M ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> invar2' A (B[P\<^sub>a ! a ! (A ! a) := a]) (M[P\<^sub>a ! a ! (A ! a) := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (M ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> (P\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) \<turnstile> a < B ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> invar2' (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1]) (B[P\<^sub>a ! a ! (A ! a) := a]) M ai (B ! (P\<^sub>a ! a ! (A ! a))) \<and> var (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1]) ({<ai + 1} - {B ! (P\<^sub>a ! a ! (A ! a))}) < v) \<and> (\<not> P\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) \<turnstile> a < B ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> invar2' (A[a := A ! a + 1]) B M ai a \<and> var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v))\<rbrakk> \<Longrightarrow> (R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! (B ! (P\<^sub>a ! a ! (A ! a))) \<longrightarrow> (\<not> M ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> invar2' A (B[P\<^sub>a ! a ! (A ! a) := a]) (M[P\<^sub>a ! a ! (A ! a) := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < var A ({<ai + 1} - {a})) \<and> (\<not> \<not> M ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> invar2' (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1]) (B[P\<^sub>a ! a ! (A ! a) := a]) M ai (B ! (P\<^sub>a ! a ! (A ! a))) \<and> var (A[B ! (P\<^sub>a ! a ! (A ! a)) := A ! (B ! (P\<^sub>a ! a ! (A ! a))) + 1]) ({<ai + 1} - {B ! (P\<^sub>a ! a ! (A ! a))}) < var A ({<ai + 1} - {a}))) \<and> (\<not> R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! a < R\<^sub>b ! (P\<^sub>a ! (B ! (P\<^sub>a ! a ! (A ! a))) ! (A ! (B ! (P\<^sub>a ! a ! (A ! a))))) ! (B ! (P\<^sub>a ! a ! (A ! a))) \<longrightarrow> (\<not> M ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> invar2' A (B[P\<^sub>a ! a ! (A ! a) := a]) (M[P\<^sub>a ! a ! (A ! a) := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < var A ({<ai + 1} - {a})) \<and> (\<not> \<not> M ! (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> invar2' (A[a := A ! a + 1]) B M ai a \<and> var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < var A ({<ai + 1} - {a})))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(case case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a) of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, ai, a) \<Rightarrow> let b = P\<^sub>a ! a ! (A ! a) in if \<not> M ! b then (A, B[b := a], M[b := True], ai + 1, ai + 1) else let a' = B ! b; r = R\<^sub>b ! (P\<^sub>a ! a' ! (A ! a')) in if r ! a < r ! a' then (A[a' := A ! a' + 1], B[b := a], M, ai, a') else (A[a := A ! a + 1], B, M, ai, a), s) \<in> measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a}))

goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 2. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 2. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
case (3 s)
[PROOF STATE]
proof (state)
this:
case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a
\<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 2. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
obtain B M ai a where "BMaia =  (B, M, ai, a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B M ai a. BMaia = (B, M, ai, a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases4
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c d. ?y = (a, b, c, d) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (2 subgoals):
 1. \<And>s. \<lbrakk>case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a; \<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)\<rbrakk> \<Longrightarrow> s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
 2. Wellfounded.wf (measure (\<lambda>(A, B, M, ai, a). var A ({<ai + 1} - {a})))
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a
\<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)
BMaia = (B, M, ai, a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a
\<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)
BMaia = (B, M, ai, a)

goal (1 subgoal):
 1. s = (A, BMaia) \<longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
using pref_match_stable atLeast0_lessThan_Suc
[PROOF STATE]
proof (prove)
using this:
case s of (A, B, M, ai, a) \<Rightarrow> invar2' A B M ai a
\<not> (case s of (A, B, M, ai, a) \<Rightarrow> ai < n)
BMaia = (B, M, ai, a)
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}
{<Suc ?n} = {?n} \<union> {<?n}

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem gs: "\<lbrakk> Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a \<rbrakk> \<Longrightarrow>
 \<exists>A. Gale_Shapley P\<^sub>a P\<^sub>b = Some(A) \<and> Pref.matching P\<^sub>a A {<n} \<and>
   Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a\<rbrakk> \<Longrightarrow> \<exists>A. Gale_Shapley P\<^sub>a P\<^sub>b = Some A \<and> Pref.matching P\<^sub>a A {<n} \<and> Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A
[PROOF STEP]
unfolding Gale_Shapley_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a\<rbrakk> \<Longrightarrow> \<exists>A. (if Pref P\<^sub>a P\<^sub>b then Some (fst (gs (length P\<^sub>a) P\<^sub>a (map ranking P\<^sub>b))) else None) = Some A \<and> Pref.matching P\<^sub>a A {<n} \<and> Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A
[PROOF STEP]
using Pref.gs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Pref ?P\<^sub>a ?P\<^sub>b; ?R\<^sub>b = map ranking ?P\<^sub>b\<rbrakk> \<Longrightarrow> gs (length ?P\<^sub>a) ?P\<^sub>a ?R\<^sub>b = (?A, ?BMai) \<longrightarrow> Pref.matching ?P\<^sub>a ?A {<length ?P\<^sub>a} \<and> Pref.stable ?P\<^sub>a ?P\<^sub>b ?A {<length ?P\<^sub>a} \<and> Pref.opti\<^sub>a ?P\<^sub>a ?P\<^sub>b ?A

goal (1 subgoal):
 1. \<lbrakk>Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a\<rbrakk> \<Longrightarrow> \<exists>A. (if Pref P\<^sub>a P\<^sub>b then Some (fst (gs (length P\<^sub>a) P\<^sub>a (map ranking P\<^sub>b))) else None) = Some A \<and> Pref.matching P\<^sub>a A {<n} \<and> Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A
[PROOF STEP]
by (metis fst_conv surj_pair)


[STATEMENT]
theorem gs1: "\<lbrakk> Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a \<rbrakk> \<Longrightarrow>
 \<exists>A. Gale_Shapley1 P\<^sub>a P\<^sub>b = Some(A) \<and> Pref.matching P\<^sub>a A {<n} \<and>
   Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a\<rbrakk> \<Longrightarrow> \<exists>A. Gale_Shapley1 P\<^sub>a P\<^sub>b = Some A \<and> Pref.matching P\<^sub>a A {<n} \<and> Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A
[PROOF STEP]
unfolding Gale_Shapley1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a\<rbrakk> \<Longrightarrow> \<exists>A. (if Pref P\<^sub>a P\<^sub>b then Some (fst (gs1 (length P\<^sub>a) P\<^sub>a (map ranking P\<^sub>b))) else None) = Some A \<and> Pref.matching P\<^sub>a A {<n} \<and> Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A
[PROOF STEP]
using Pref.gs1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Pref ?P\<^sub>a ?P\<^sub>b; ?R\<^sub>b = map ranking ?P\<^sub>b\<rbrakk> \<Longrightarrow> gs1 (length ?P\<^sub>a) ?P\<^sub>a ?R\<^sub>b = (?A, ?BMaia) \<longrightarrow> Pref.matching ?P\<^sub>a ?A {<length ?P\<^sub>a} \<and> Pref.stable ?P\<^sub>a ?P\<^sub>b ?A {<length ?P\<^sub>a} \<and> Pref.opti\<^sub>a ?P\<^sub>a ?P\<^sub>b ?A

goal (1 subgoal):
 1. \<lbrakk>Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a\<rbrakk> \<Longrightarrow> \<exists>A. (if Pref P\<^sub>a P\<^sub>b then Some (fst (gs1 (length P\<^sub>a) P\<^sub>a (map ranking P\<^sub>b))) else None) = Some A \<and> Pref.matching P\<^sub>a A {<n} \<and> Pref.stable P\<^sub>a P\<^sub>b A {<n} \<and> Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A
[PROOF STEP]
by (metis fst_conv surj_pair)


[STATEMENT]
lemma "Gale_Shapley
  [[3,0,1,2], [1,2,0,3], [1,3,2,0], [2,0,3,1]]
  [[3,0,2,1], [0,2,1,3], [0,1,2,3], [3,0,2,1]]
  = Some[0,1,0,1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gale_Shapley [[3, 0, 1, 2], [1, 2, 0, 3], [1, 3, 2, 0], [2, 0, 3, 1]] [[3, 0, 2, 1], [0, 2, 1, 3], [0, 1, 2, 3], [3, 0, 2, 1]] = Some [0, 1, 0, 1]
[PROOF STEP]
by eval


[STATEMENT]
lemma "Gale_Shapley1
  [[4,6,0,1,5,7,3,2], [1,2,6,4,3,0,7,5], [7,4,0,3,5,1,2,6], [2,1,6,3,0,5,7,4],
   [6,1,4,0,2,5,7,3], [0,5,6,4,7,3,1,2], [1,4,6,5,2,3,7,0], [2,7,3,4,6,1,5,0]]
  [[4,2,6,5,0,1,7,3], [7,5,2,4,6,1,0,3], [0,4,5,1,3,7,6,2], [7,6,2,1,3,0,4,5],
   [5,3,6,2,7,0,1,4], [1,7,4,2,3,5,6,0], [6,4,1,0,7,5,3,2], [6,3,0,4,1,2,5,7]]
  = Some [0, 1, 0, 5, 0, 0, 0, 2]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gale_Shapley1 [[4, 6, 0, 1, 5, 7, 3, 2], [1, 2, 6, 4, 3, 0, 7, 5], [7, 4, 0, 3, 5, 1, 2, 6], [2, 1, 6, 3, 0, 5, 7, 4], [6, 1, 4, 0, 2, 5, 7, 3], [0, 5, 6, 4, 7, 3, 1, 2], [1, 4, 6, 5, 2, 3, 7, 0], [2, 7, 3, 4, 6, 1, 5, 0]] [[4, 2, 6, 5, 0, 1, 7, 3], [7, 5, 2, 4, 6, 1, 0, 3], [0, 4, 5, 1, 3, 7, 6, 2], [7, 6, 2, 1, 3, 0, 4, 5], [5, 3, 6, 2, 7, 0, 1, 4], [1, 7, 4, 2, 3, 5, 6, 0], [6, 4, 1, 0, 7, 5, 3, 2], [6, 3, 0, 4, 1, 2, 5, 7]] = Some [0, 1, 0, 5, 0, 0, 0, 2]
[PROOF STEP]
by eval


[STATEMENT]
lemma Collect_iff:
  "a \<in> {x . P x} \<equiv> P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {x. P x} \<equiv> P a
[PROOF STEP]
by auto


[STATEMENT]
lemma diff_diff_eq:
  assumes "C \<subseteq> B"
  shows "(A - C) - (B - C) = A - B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - C - (B - C) = A - B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> B

goal (1 subgoal):
 1. A - C - (B - C) = A - B
[PROOF STEP]
by auto


[STATEMENT]
lemma nth_in_set:
  "\<lbrakk> i < length xs ; xs ! i = x \<rbrakk> \<Longrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; xs ! i = x\<rbrakk> \<Longrightarrow> x \<in> set xs
[PROOF STEP]
by auto


[STATEMENT]
lemma disjI [intro]:
  assumes "\<not> P \<Longrightarrow> Q"
  shows "P \<or> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<or> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> P \<Longrightarrow> Q

goal (1 subgoal):
 1. P \<or> Q
[PROOF STEP]
by auto


[STATEMENT]
lemma empty_eq_Plus_conv:
  "({} = A <+> B) = (A = {} \<and> B = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({} = A <+> B) = (A = {} \<and> B = {})
[PROOF STEP]
by auto


[STATEMENT]
lemma fst3_simp:
  "\<And>a b c. fst3 (a,b,c) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. fst3 (a, b, c) = a
[PROOF STEP]
by (auto simp add: fst3_def)


[STATEMENT]
lemma snd3_simp:
  "\<And>a b c. snd3 (a,b,c) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. snd3 (a, b, c) = b
[PROOF STEP]
by (auto simp add: snd3_def)


[STATEMENT]
lemma thd3_simp:
  "\<And>a b c. thd3 (a,b,c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. thd3 (a, b, c) = c
[PROOF STEP]
by (auto simp add: thd3_def)


[STATEMENT]
lemma tripleI:
  fixes T U
  assumes "fst3 T = fst3 U"
      and "snd3 T = snd3 U"
      and "thd3 T = thd3 U"
  shows "T = U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T = U
[PROOF STEP]
by (metis assms fst3_def snd3_def thd3_def o_def surjective_pairing)


[STATEMENT]
lemma divmultassoc: "a div (b*c) * (b*c) = ((a div (b * c)) * b)*(c::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div (b * c) * (b * c) = a div (b * c) * b * c
[PROOF STEP]
by (rule mult.assoc [symmetric])


[STATEMENT]
lemma delmod: "(a::nat) mod (b*c) mod c = a mod c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) mod c = a mod c
[PROOF STEP]
by (rule mod_mod_cancel [OF dvd_triv_right])


[STATEMENT]
lemma timesmod1: "((x::nat)*((y::nat) mod n)) mod (n::nat) = ((x*y) mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y mod n) mod n = x * y mod n
[PROOF STEP]
by (rule mod_mult_right_eq)


[STATEMENT]
lemma timesmod3: "((a mod (n::nat)) * b) mod n = (a*b) mod n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod n * b mod n = a * b mod n
[PROOF STEP]
by (rule mod_mult_left_eq)


[STATEMENT]
lemma remainderexplemma: "(y mod (a::nat) = z mod a) \<Longrightarrow> (x*y) mod a = (x*z) mod a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y mod a = z mod a \<Longrightarrow> x * y mod a = x * z mod a
[PROOF STEP]
by (rule mod_mult_cong [OF refl])


[STATEMENT]
lemma remainderexp: "((a mod (n::nat))^i) mod n = (a^i) mod n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a mod n) ^ i mod n = a ^ i mod n
[PROOF STEP]
by (rule power_mod)


[STATEMENT]
lemma lotteries_on_subset:
  assumes "A \<subseteq> B"
  shows "lotteries_on A \<subseteq> lotteries_on B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lotteries_on A \<subseteq> lotteries_on B
[PROOF STEP]
by (metis (no_types, lifting) Collect_mono assms gfp.leq_trans lotteries_on_def)


[STATEMENT]
lemma support_in_outcomes:
  "\<forall>oc. \<forall>p \<in> lotteries_on oc. \<forall>a \<in> set_pmf p. a \<in> oc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>oc. \<forall>p\<in>lotteries_on oc. \<forall>a\<in>set_pmf p. a \<in> oc
[PROOF STEP]
by (simp add: lotteries_on_def subsetD)


[STATEMENT]
lemma lotteries_on_nonempty:
  assumes "outcomes \<noteq> {}"
  shows "lotteries_on outcomes \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lotteries_on outcomes \<noteq> {}
[PROOF STEP]
by (auto simp: lotteries_on_def) (metis (full_types) assms
      empty_subsetI ex_in_conv insert_subset set_return_pmf)


[STATEMENT]
lemma finite_support_one_oc:
  assumes "card outcomes = 1"
  shows "\<forall>l \<in> lotteries_on outcomes. finite (set_pmf l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>lotteries_on outcomes. finite (set_pmf l)
[PROOF STEP]
by (metis assms card.infinite finite_subset lotteries_on_def mem_Collect_eq zero_neq_one)


[STATEMENT]
lemma one_outcome_card_support_1:
  assumes "card outcomes = 1"
  shows "\<forall>l \<in> lotteries_on outcomes. card (set_pmf l) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>lotteries_on outcomes. card (set_pmf l) = 1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> lotteries_on outcomes \<Longrightarrow> card (set_pmf l) = 1
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> lotteries_on outcomes \<Longrightarrow> card (set_pmf l) = 1
[PROOF STEP]
assume "l \<in> lotteries_on outcomes"
[PROOF STATE]
proof (state)
this:
l \<in> lotteries_on outcomes

goal (1 subgoal):
 1. \<And>l. l \<in> lotteries_on outcomes \<Longrightarrow> card (set_pmf l) = 1
[PROOF STEP]
have "finite outcomes"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite outcomes
[PROOF STEP]
using assms card.infinite
[PROOF STATE]
proof (prove)
using this:
card outcomes = 1
infinite ?A \<Longrightarrow> card ?A = 0

goal (1 subgoal):
 1. finite outcomes
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite outcomes

goal (1 subgoal):
 1. \<And>l. l \<in> lotteries_on outcomes \<Longrightarrow> card (set_pmf l) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite outcomes
[PROOF STEP]
have "l \<in> lotteries_on outcomes \<longrightarrow> 1 = card (set_pmf l)"
[PROOF STATE]
proof (prove)
using this:
finite outcomes

goal (1 subgoal):
 1. l \<in> lotteries_on outcomes \<longrightarrow> 1 = card (set_pmf l)
[PROOF STEP]
by (metis assms card_eq_0_iff card_mono finite_support_one_oc le_neq_implies_less
        less_one lotteries_on_def mem_Collect_eq set_pmf_not_empty)
[PROOF STATE]
proof (state)
this:
l \<in> lotteries_on outcomes \<longrightarrow> 1 = card (set_pmf l)

goal (1 subgoal):
 1. \<And>l. l \<in> lotteries_on outcomes \<Longrightarrow> card (set_pmf l) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> lotteries_on outcomes \<longrightarrow> 1 = card (set_pmf l)
[PROOF STEP]
show "card (set_pmf l) = 1"
[PROOF STATE]
proof (prove)
using this:
l \<in> lotteries_on outcomes \<longrightarrow> 1 = card (set_pmf l)

goal (1 subgoal):
 1. card (set_pmf l) = 1
[PROOF STEP]
by (simp add: \<open>l \<in> lotteries_on outcomes\<close>)
[PROOF STATE]
proof (state)
this:
card (set_pmf l) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_nempty_ex_degernate_in_lotteries:
  assumes "out \<noteq> {}"
  assumes "finite out"
  shows "\<exists>e \<in> lotteries_on out. \<exists>x \<in> out. pmf e x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1) \<Longrightarrow> False
[PROOF STEP]
assume a: "\<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1)

goal (1 subgoal):
 1. \<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1)
[PROOF STEP]
have subset: "\<forall>e \<in> lotteries_on out. set_pmf e \<subseteq> out"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1)

goal (1 subgoal):
 1. \<forall>e\<in>lotteries_on out. set_pmf e \<subseteq> out
[PROOF STEP]
using lotteries_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1)
lotteries_on ?Oc = {p. set_pmf p \<subseteq> ?Oc}

goal (1 subgoal):
 1. \<forall>e\<in>lotteries_on out. set_pmf e \<subseteq> out
[PROOF STEP]
by (simp add: lotteries_on_def)
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>lotteries_on out. set_pmf e \<subseteq> out

goal (1 subgoal):
 1. \<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>e\<in>lotteries_on out. set_pmf e \<subseteq> out
[PROOF STEP]
have "\<forall>e. e \<in> lotteries_on out \<longrightarrow> ((\<Sum>i\<in>set_pmf e. pmf e i) = 1)"
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>lotteries_on out. set_pmf e \<subseteq> out

goal (1 subgoal):
 1. \<forall>e. e \<in> lotteries_on out \<longrightarrow> sum (pmf e) (set_pmf e) = 1
[PROOF STEP]
using sum_pmf_eq_1
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>lotteries_on out. set_pmf e \<subseteq> out
\<lbrakk>finite ?A; set_pmf ?p \<subseteq> ?A\<rbrakk> \<Longrightarrow> sum (pmf ?p) ?A = 1

goal (1 subgoal):
 1. \<forall>e. e \<in> lotteries_on out \<longrightarrow> sum (pmf e) (set_pmf e) = 1
[PROOF STEP]
by (metis subset  assms(2) finite_subset order_refl)
[PROOF STATE]
proof (state)
this:
\<forall>e. e \<in> lotteries_on out \<longrightarrow> sum (pmf e) (set_pmf e) = 1

goal (1 subgoal):
 1. \<not> (\<exists>e\<in>lotteries_on out. \<exists>x\<in>out. pmf e x = 1) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>e. e \<in> lotteries_on out \<longrightarrow> sum (pmf e) (set_pmf e) = 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>e. e \<in> lotteries_on out \<longrightarrow> sum (pmf e) (set_pmf e) = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (no_types, lifting) a assms(1) assms(2) card.empty card_gt_0_iff card_seteq
        empty_subsetI finite.emptyI finite_insert insert_subset lotteries_on_def subsetI
        measure_measure_pmf_finite mem_Collect_eq nat_less_le pmf.rep_eq set_pmf_of_set )
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_support_1_probability_1:
  assumes "card (set_pmf p) = 1"
  shows "\<forall>e \<in> set_pmf p. pmf p e = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>set_pmf p. pmf p e = 1
[PROOF STEP]
by(auto) (metis assms card_1_singletonE card_ge_0_finite
      card_subset_eq ex_card le_numeral_extra(4) measure_measure_pmf_finite
      pmf.rep_eq singletonD sum_pmf_eq_1 zero_less_one)


[STATEMENT]
lemma one_outcome_card_lotteries_1:
  assumes "card outcomes = 1"
  shows "card (lotteries_on outcomes) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (lotteries_on outcomes) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (lotteries_on outcomes) = 1
[PROOF STEP]
obtain x :: 'a where
    x: "outcomes = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. outcomes = {x} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms card_1_singletonE
[PROOF STATE]
proof (prove)
using this:
card outcomes = 1
\<lbrakk>card ?A = 1; \<And>x. ?A = {x} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x. outcomes = {x} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
outcomes = {x}

goal (1 subgoal):
 1. card (lotteries_on outcomes) = 1
[PROOF STEP]
have exl: "\<exists>l \<in> lotteries_on outcomes. pmf l x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l\<in>lotteries_on outcomes. pmf l x = 1
[PROOF STEP]
by (metis x assms card.infinite empty_iff
        finite_nempty_ex_degernate_in_lotteries insert_iff zero_neq_one)
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>lotteries_on outcomes. pmf l x = 1

goal (1 subgoal):
 1. card (lotteries_on outcomes) = 1
[PROOF STEP]
have pmfs: "\<forall>l \<in> lotteries_on outcomes. set_pmf l = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>lotteries_on outcomes. set_pmf l = {x}
[PROOF STEP]
by (simp add: lotteries_on_def set_pmf_subset_singleton x)
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>lotteries_on outcomes. set_pmf l = {x}

goal (1 subgoal):
 1. card (lotteries_on outcomes) = 1
[PROOF STEP]
have "\<forall>l \<in> lotteries_on outcomes. pmf l x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>lotteries_on outcomes. pmf l x = 1
[PROOF STEP]
by (simp add: lotteries_on_def set_pmf_subset_singleton x)
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>lotteries_on outcomes. pmf l x = 1

goal (1 subgoal):
 1. card (lotteries_on outcomes) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>lotteries_on outcomes. pmf l x = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>lotteries_on outcomes. pmf l x = 1

goal (1 subgoal):
 1. card (lotteries_on outcomes) = 1
[PROOF STEP]
by (metis exl empty_iff is_singletonI' is_singleton_altdef
        order_refl pmfs set_pmf_subset_singleton)
[PROOF STATE]
proof (state)
this:
card (lotteries_on outcomes) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mix_pmf_in_lotteries:
  assumes "p \<in> lotteries_on A"
    and "q \<in> lotteries_on A"
    and "a \<in> {0<..<1}"
  shows "(mix_pmf a p q) \<in> lotteries_on A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf a p q \<in> lotteries_on A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mix_pmf a p q \<in> lotteries_on A
[PROOF STEP]
have "set_pmf (mix_pmf a p q) = set_pmf p \<union> set_pmf q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) = set_pmf p \<union> set_pmf q
[PROOF STEP]
by (meson assms(3) set_pmf_mix)
[PROOF STATE]
proof (state)
this:
set_pmf (mix_pmf a p q) = set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. mix_pmf a p q \<in> lotteries_on A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set_pmf (mix_pmf a p q) = set_pmf p \<union> set_pmf q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_pmf (mix_pmf a p q) = set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. mix_pmf a p q \<in> lotteries_on A
[PROOF STEP]
by (metis Un_subset_iff assms(1) assms(2) lotteries_on_def mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
mix_pmf a p q \<in> lotteries_on A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_degen_lotteries_equals_outcomes:
  shows "card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
consider (empty) "out = {}" | (not_empty) "out \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>out = {} \<Longrightarrow> thesis; out \<noteq> {} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>out = {} \<Longrightarrow> ?thesis; out \<noteq> {} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>out = {} \<Longrightarrow> ?thesis; out \<noteq> {} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>out = {} \<Longrightarrow> ?thesis; out \<noteq> {} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
case not_empty
[PROOF STATE]
proof (state)
this:
out \<noteq> {}

goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
define DG where
      DG: "DG = {x \<in> lotteries_on out. card (set_pmf x) = 1}"
[PROOF STATE]
proof (state)
this:
DG = {x \<in> lotteries_on out. card (set_pmf x) = 1}

goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
define AP where
      AP: "AP = {return_pmf x |x. x \<in> out}"
[PROOF STATE]
proof (state)
this:
AP = {return_pmf x |x. x \<in> out}

goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
have **: "card AP = card out"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card AP = card out
[PROOF STEP]
using AP return_pmf_card_equals_set
[PROOF STATE]
proof (prove)
using this:
AP = {return_pmf x |x. x \<in> out}
card {return_pmf x |x. x \<in> ?S} = card ?S

goal (1 subgoal):
 1. card AP = card out
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card AP = card out

goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
have *: "\<forall>d \<in> DG. d \<in> AP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d\<in>DG. d \<in> AP
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. d \<in> DG \<Longrightarrow> d \<in> AP
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. d \<in> DG \<Longrightarrow> d \<in> AP
[PROOF STEP]
assume "l \<in> DG"
[PROOF STATE]
proof (state)
this:
l \<in> DG

goal (1 subgoal):
 1. \<And>d. d \<in> DG \<Longrightarrow> d \<in> AP
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> DG
[PROOF STEP]
have "l \<in> lotteries_on out \<and> 1 = card (set_pmf l)"
[PROOF STATE]
proof (prove)
using this:
l \<in> DG

goal (1 subgoal):
 1. l \<in> lotteries_on out \<and> 1 = card (set_pmf l)
[PROOF STEP]
using DG
[PROOF STATE]
proof (prove)
using this:
l \<in> DG
DG = {x \<in> lotteries_on out. card (set_pmf x) = 1}

goal (1 subgoal):
 1. l \<in> lotteries_on out \<and> 1 = card (set_pmf l)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
l \<in> lotteries_on out \<and> 1 = card (set_pmf l)

goal (1 subgoal):
 1. \<And>d. d \<in> DG \<Longrightarrow> d \<in> AP
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> lotteries_on out \<and> 1 = card (set_pmf l)
[PROOF STEP]
obtain x where
        x: "x \<in> out" "set_pmf l = {x}"
[PROOF STATE]
proof (prove)
using this:
l \<in> lotteries_on out \<and> 1 = card (set_pmf l)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> out; set_pmf l = {x}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types) card_1_singletonE singletonI support_in_outcomes)
[PROOF STATE]
proof (state)
this:
x \<in> out
set_pmf l = {x}

goal (1 subgoal):
 1. \<And>d. d \<in> DG \<Longrightarrow> d \<in> AP
[PROOF STEP]
have "return_pmf x = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_pmf x = l
[PROOF STEP]
using set_pmf_subset_singleton x(2)
[PROOF STATE]
proof (prove)
using this:
(set_pmf ?p \<subseteq> {?x}) = (?p = return_pmf ?x)
set_pmf l = {x}

goal (1 subgoal):
 1. return_pmf x = l
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
return_pmf x = l

goal (1 subgoal):
 1. \<And>d. d \<in> DG \<Longrightarrow> d \<in> AP
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
return_pmf x = l
[PROOF STEP]
show "l \<in> AP"
[PROOF STATE]
proof (prove)
using this:
return_pmf x = l

goal (1 subgoal):
 1. l \<in> AP
[PROOF STEP]
using AP x(1)
[PROOF STATE]
proof (prove)
using this:
return_pmf x = l
AP = {return_pmf x |x. x \<in> out}
x \<in> out

goal (1 subgoal):
 1. l \<in> AP
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> AP

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>d\<in>DG. d \<in> AP

goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>d\<in>DG. d \<in> AP

goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
have "AP = DG"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AP = DG
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AP \<subseteq> DG
 2. DG \<subseteq> AP
[PROOF STEP]
have "\<forall>e \<in> AP. e \<in> lotteries_on out"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>AP. e \<in> lotteries_on out
[PROOF STEP]
by(auto simp: lotteries_on_def AP)
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>AP. e \<in> lotteries_on out

goal (2 subgoals):
 1. AP \<subseteq> DG
 2. DG \<subseteq> AP
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>e\<in>AP. e \<in> lotteries_on out
[PROOF STEP]
show "AP \<subseteq> DG"
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>AP. e \<in> lotteries_on out

goal (1 subgoal):
 1. AP \<subseteq> DG
[PROOF STEP]
using DG AP
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>AP. e \<in> lotteries_on out
DG = {x \<in> lotteries_on out. card (set_pmf x) = 1}
AP = {return_pmf x |x. x \<in> out}

goal (1 subgoal):
 1. AP \<subseteq> DG
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
AP \<subseteq> DG

goal (1 subgoal):
 1. DG \<subseteq> AP
[PROOF STEP]
qed (auto simp: *)
[PROOF STATE]
proof (state)
this:
AP = DG

goal (2 subgoals):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
 2. out \<noteq> {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>d\<in>DG. d \<in> AP
AP = DG
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>DG. d \<in> AP
AP = DG

goal (1 subgoal):
 1. card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
using DG **
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>DG. d \<in> AP
AP = DG
DG = {x \<in> lotteries_on out. card (set_pmf x) = 1}
card AP = card out

goal (1 subgoal):
 1. card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out

goal (1 subgoal):
 1. out = {} \<Longrightarrow> card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out
[PROOF STEP]
qed (simp add: lotteries_on_def set_pmf_not_empty)
[PROOF STATE]
proof (state)
this:
card {x \<in> lotteries_on out. card (set_pmf x) = 1} = card out

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZeroHeightReachableElimAux[rule_format]:
  "(M, l, s, k, r) \<in> Reachable \<Longrightarrow> 0=k \<longrightarrow> r=s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, r) \<in> Reachable \<Longrightarrow> 0 = k \<longrightarrow> r = s
[PROOF STEP]
by (erule Reachable.induct, simp_all)


[STATEMENT]
lemma ZeroHeightReachableElim: "(M,l,s,0,r) \<in> Reachable \<Longrightarrow> r=s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, r) \<in> Reachable \<Longrightarrow> r = s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, r) \<in> Reachable \<Longrightarrow> r = s
[PROOF STEP]
by (erule ZeroHeightReachableElimAux, simp)