[STATEMENT]
lemma it_dfsT_eq_it_dfs:
    assumes [simp, intro!]: "finite reachable"
    shows "it_dfsT = it_dfs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfsT = it_dfs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. it_dfsT = it_dfs
[PROOF STEP]
have "it_dfs \<le> it_dfsT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfs \<le> it_dfsT
[PROOF STEP]
unfolding it_dfs_def it_dfsT_def WHILE_def WHILET_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<bind> WHILE\<^bsup>\<lambda>_. True\<^esup> cond step \<le> init \<bind> WHILE\<^sub>T\<^bsup>\<lambda>_. True\<^esup> cond step
[PROOF STEP]
apply (rule bind_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. init \<le> init
 2. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE\<^bsup>\<lambda>_. True\<^esup> cond step x \<le> WHILE\<^sub>T\<^bsup>\<lambda>_. True\<^esup> cond step x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE\<^bsup>\<lambda>_. True\<^esup> cond step x \<le> WHILE\<^sub>T\<^bsup>\<lambda>_. True\<^esup> cond step x
[PROOF STEP]
apply (rule WHILEI_le_WHILEIT)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
it_dfs \<le> it_dfsT

goal (1 subgoal):
 1. it_dfsT = it_dfs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
it_dfs \<le> it_dfsT

goal (1 subgoal):
 1. it_dfsT = it_dfs
[PROOF STEP]
have "it_dfsT \<le> it_dfs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfsT \<le> it_dfs
[PROOF STEP]
proof (cases "nofail it_dfs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nofail it_dfs \<Longrightarrow> it_dfsT \<le> it_dfs
 2. \<not> nofail it_dfs \<Longrightarrow> it_dfsT \<le> it_dfs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> nofail it_dfs

goal (2 subgoals):
 1. nofail it_dfs \<Longrightarrow> it_dfsT \<le> it_dfs
 2. \<not> nofail it_dfs \<Longrightarrow> it_dfsT \<le> it_dfs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> nofail it_dfs

goal (1 subgoal):
 1. it_dfsT \<le> it_dfs
[PROOF STEP]
by (simp add: not_nofail_iff)
[PROOF STATE]
proof (state)
this:
it_dfsT \<le> it_dfs

goal (1 subgoal):
 1. nofail it_dfs \<Longrightarrow> it_dfsT \<le> it_dfs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nofail it_dfs \<Longrightarrow> it_dfsT \<le> it_dfs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
nofail it_dfs

goal (1 subgoal):
 1. nofail it_dfs \<Longrightarrow> it_dfsT \<le> it_dfs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfsT \<le> it_dfs
[PROOF STEP]
unfolding it_dfsT_def it_dfs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<bind> WHILE\<^sub>T cond step \<le> init \<bind> WHILE cond step
[PROOF STEP]
apply (rule bind_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. init \<le> init
 2. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE\<^sub>T cond step x \<le> WHILE cond step x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE\<^sub>T cond step x \<le> WHILE cond step x
[PROOF STEP]
apply (subst WHILET_eq_WHILE_tproof[
          where I="DFS_invar G param"
          and V="param_dfs_variant"
          ])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. RETURN x \<le> init \<Longrightarrow> wf param_dfs_variant
 2. \<And>x. RETURN x \<le> init \<Longrightarrow> DFS_invar G param x
 3. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>s'. DFS_invar G param s' \<and> (s', s) \<in> param_dfs_variant)
 4. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. RETURN x \<le> init \<Longrightarrow> DFS_invar G param x
 2. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>s'. DFS_invar G param s' \<and> (s', s) \<in> param_dfs_variant)
 3. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
apply (subst rwof_eq_DFS_invar[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. RETURN x \<le> init \<Longrightarrow> rwof init cond step x
 2. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>s'. DFS_invar G param s' \<and> (s', s) \<in> param_dfs_variant)
 3. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
using rwof_init[OF True[unfolded it_dfs_def]]
[PROOF STATE]
proof (prove)
using this:
init \<le> SPEC (rwof init cond step)

goal (3 subgoals):
 1. \<And>x. RETURN x \<le> init \<Longrightarrow> rwof init cond step x
 2. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>s'. DFS_invar G param s' \<and> (s', s) \<in> param_dfs_variant)
 3. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
apply (fastforce dest: order_trans) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>s'. DFS_invar G param s' \<and> (s', s) \<in> param_dfs_variant)
 2. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
apply (rule SPEC_rule_conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (DFS_invar G param)
 2. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>v. (v, s) \<in> param_dfs_variant)
 3. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
apply (rule DFS_invar_step[OF True], assumption+) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>RETURN x \<le> init; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>v. (v, s) \<in> param_dfs_variant)
 2. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
apply (rule param_dfs_variant_step, (assumption|rule True)+) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. RETURN x \<le> init \<Longrightarrow> WHILE cond step x \<le> WHILE cond step x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
it_dfsT \<le> it_dfs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
it_dfsT \<le> it_dfs

goal (1 subgoal):
 1. it_dfsT = it_dfs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
it_dfs = it_dfsT
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
it_dfs = it_dfsT

goal (1 subgoal):
 1. it_dfsT = it_dfs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
it_dfsT = it_dfs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma init_leof_invar: "init \<le>\<^sub>n SPEC (DFS_invar G param)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<le>\<^sub>n SPEC (DFS_invar G param)
[PROOF STEP]
unfolding rwof_eq_DFS_invar[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<le>\<^sub>n SPEC (rwof init cond step)
[PROOF STEP]
by (rule rwof_leof_init)


[STATEMENT]
lemma it_dfs_eq_spec: "it_dfs = SPEC (\<lambda>s. DFS_invar G param s \<and> \<not>cond s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfs = SPEC (\<lambda>s. DFS_invar G param s \<and> \<not> cond s)
[PROOF STEP]
unfolding rwof_eq_DFS_invar[symmetric] it_dfs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<bind> WHILE cond step = SPEC (\<lambda>s. rwof init cond step s \<and> \<not> cond s)
[PROOF STEP]
apply (rule nofail_WHILE_eq_rwof)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (init \<bind> WHILE cond step)
[PROOF STEP]
apply (subst WHILE_eq_I_rwof)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (init \<bind> WHILE\<^bsup>rwof init cond step\<^esup> cond step)
[PROOF STEP]
unfolding rwof_eq_DFS_invar
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (init \<bind> WHILE\<^bsup>DFS_invar G param\<^esup> cond step)
[PROOF STEP]
apply (rule SPEC_nofail[where \<Phi>="\<lambda>_. True"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<bind> WHILE\<^bsup>DFS_invar G param\<^esup> cond step \<le> SPEC (\<lambda>_. True)
[PROOF STEP]
apply (refine_vcg leofD[OF _ init_leof_invar, THEN weaken_SPEC])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. nofail init
 2. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (DFS_invar G param)
 3. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; \<not> cond s\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (simp add: init_def refine_pw_simps nofail_on_init)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (DFS_invar G param)
 2. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; \<not> cond s\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (rule DFS_invar_step')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> nofail (step s)
 2. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> DFS_invar G param s
 3. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> cond s
 4. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; \<not> cond s\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (simp add: step_def refine_pw_simps nofail_on_init do_defs
      get_pending_def get_new_root_def pred_defs
      split: option.split)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> (pending s `` {hd (stack s)} = {} \<longrightarrow> (stack s = [] \<longrightarrow> (\<forall>x. x \<in> V0 \<and> x \<notin> dom (discovered s) \<longrightarrow> nofail (on_new_root param x (new_root x s)))) \<and> (stack s \<noteq> [] \<longrightarrow> nofail (on_finish param (hd (stack s)) (finish (hd (stack s)) s)))) \<and> (pending s `` {hd (stack s)} \<noteq> {} \<longrightarrow> (stack s = [] \<longrightarrow> (\<forall>x. x \<in> V0 \<and> x \<notin> dom (discovered s) \<longrightarrow> nofail (on_new_root param x (new_root x s)))) \<and> (stack s \<noteq> [] \<longrightarrow> (\<forall>x. (x \<in> dom (finished s) \<longrightarrow> (x \<in> dom (discovered s) \<longrightarrow> (hd (stack s), x) \<in> pending s \<longrightarrow> nofail (on_cross_edge param (hd (stack s)) x (cross_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>)))) \<and> (x \<notin> dom (discovered s) \<longrightarrow> (hd (stack s), x) \<in> pending s \<longrightarrow> nofail (on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>))))) \<and> (x \<notin> dom (finished s) \<longrightarrow> (x \<in> dom (discovered s) \<longrightarrow> (hd (stack s), x) \<in> pending s \<longrightarrow> nofail (on_back_edge param (hd (stack s)) x (back_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>)))) \<and> (x \<notin> dom (discovered s) \<longrightarrow> (hd (stack s), x) \<in> pending s \<longrightarrow> nofail (on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>))))))))
 2. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> DFS_invar G param s
 3. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> cond s
 4. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; \<not> cond s\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (intro allI conjI impI nofails)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>x s xa. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s; pending s `` {hd (stack s)} = {}; stack s = []; xa \<in> V0 \<and> xa \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> pre_on_new_root xa (new_root xa s)
 2. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s; pending s `` {hd (stack s)} = {}; stack s \<noteq> []\<rbrakk> \<Longrightarrow> pre_on_finish (hd (stack s)) (finish (hd (stack s)) s)
 3. \<And>x s xa. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s; pending s `` {hd (stack s)} \<noteq> {}; stack s = []; xa \<in> V0 \<and> xa \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> pre_on_new_root xa (new_root xa s)
 4. \<And>x s xa. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s; pending s `` {hd (stack s)} \<noteq> {}; stack s \<noteq> []; xa \<in> dom (finished s); xa \<in> dom (discovered s); (hd (stack s), xa) \<in> pending s\<rbrakk> \<Longrightarrow> pre_on_cross_edge (hd (stack s)) xa (cross_edge (hd (stack s)) xa (s\<lparr>pending := pending s - {(hd (stack s), xa)}\<rparr>))
 5. \<And>x s xa. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s; pending s `` {hd (stack s)} \<noteq> {}; stack s \<noteq> []; xa \<in> dom (finished s); xa \<notin> dom (discovered s); (hd (stack s), xa) \<in> pending s\<rbrakk> \<Longrightarrow> pre_on_discover (hd (stack s)) xa (discover (hd (stack s)) xa (s\<lparr>pending := pending s - {(hd (stack s), xa)}\<rparr>))
 6. \<And>x s xa. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s; pending s `` {hd (stack s)} \<noteq> {}; stack s \<noteq> []; xa \<notin> dom (finished s); xa \<in> dom (discovered s); (hd (stack s), xa) \<in> pending s\<rbrakk> \<Longrightarrow> pre_on_back_edge (hd (stack s)) xa (back_edge (hd (stack s)) xa (s\<lparr>pending := pending s - {(hd (stack s), xa)}\<rparr>))
 7. \<And>x s xa. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s; pending s `` {hd (stack s)} \<noteq> {}; stack s \<noteq> []; xa \<notin> dom (finished s); xa \<notin> dom (discovered s); (hd (stack s), xa) \<in> pending s\<rbrakk> \<Longrightarrow> pre_on_discover (hd (stack s)) xa (discover (hd (stack s)) xa (s\<lparr>pending := pending s - {(hd (stack s), xa)}\<rparr>))
 8. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> DFS_invar G param s
 9. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> cond s
 10. \<And>x s. \<lbrakk>DFS_invar G param x; DFS_invar G param s; \<not> cond s\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (auto simp add: pre_on_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma it_dfs_SPEC:
    assumes "\<And>s. \<lbrakk>DFS_invar G param s; \<not>cond s\<rbrakk> \<Longrightarrow> P s"
    shows "it_dfs \<le> SPEC P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfs \<le> SPEC P
[PROOF STEP]
using weaken_SPEC[OF it_dfs_correct]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. DFS_invar G param x \<and> \<not> cond x \<Longrightarrow> ?\<Psi> x) \<Longrightarrow> it_dfs \<le> SPEC ?\<Psi>

goal (1 subgoal):
 1. it_dfs \<le> SPEC P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<And>x. DFS_invar G param x \<and> \<not> cond x \<Longrightarrow> ?\<Psi> x) \<Longrightarrow> it_dfs \<le> SPEC ?\<Psi>
\<lbrakk>DFS_invar G param ?s4; \<not> cond ?s4\<rbrakk> \<Longrightarrow> P ?s4

goal (1 subgoal):
 1. it_dfs \<le> SPEC P
[PROOF STEP]
by blast


[STATEMENT]
lemma it_dfsT_correct:
    assumes "finite reachable"
    shows "it_dfsT \<le> SPEC (\<lambda>s. DFS_invar G param s \<and> \<not>cond s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfsT \<le> SPEC (\<lambda>s. DFS_invar G param s \<and> \<not> cond s)
[PROOF STEP]
apply (subst it_dfsT_eq_it_dfs[OF assms])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfs \<le> SPEC (\<lambda>s. DFS_invar G param s \<and> \<not> cond s)
[PROOF STEP]
by (rule it_dfs_correct)


[STATEMENT]
lemma it_dfsT_SPEC:
    assumes "finite reachable"
    assumes "\<And>s. \<lbrakk>DFS_invar G param s; \<not>cond s\<rbrakk> \<Longrightarrow> P s"
    shows "it_dfsT \<le> SPEC P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfsT \<le> SPEC P
[PROOF STEP]
apply (subst it_dfsT_eq_it_dfs[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfs \<le> SPEC P
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>DFS_invar G param ?s4; \<not> cond ?s4\<rbrakk> \<Longrightarrow> P ?s4

goal (1 subgoal):
 1. it_dfs \<le> SPEC P
[PROOF STEP]
by (rule it_dfs_SPEC)


[STATEMENT]
lemma surjective_on_implies_card_eq:
  assumes "f ` A = B"
  shows "card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
from \<open>f ` A = B\<close>
[PROOF STATE]
proof (chain)
picking this:
f ` A = B
[PROOF STEP]
have "{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B"
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
from \<open>f ` A = B\<close>
[PROOF STATE]
proof (chain)
picking this:
f ` A = B
[PROOF STEP]
have "inj_on (\<lambda>b. {x \<in> A. f x = b}) B"
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. inj_on (\<lambda>b. {x \<in> A. f x = b}) B
[PROOF STEP]
by (fastforce intro: inj_onI)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>b. {x \<in> A. f x = b}) B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
have "card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B)
[PROOF STEP]
using \<open>{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B\<close>
[PROOF STATE]
proof (prove)
using this:
{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B)

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B)

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
have "\<dots> = card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B) = card B
[PROOF STEP]
using \<open>inj_on (\<lambda>b. {x \<in> A. f x = b}) B\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>b. {x \<in> A. f x = b}) B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B) = card B
[PROOF STEP]
by (rule card_image)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B) = card B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_eq_implies_surjective_on:
  assumes "finite B" "f \<in> A \<rightarrow>\<^sub>E B"
  assumes card_eq: "card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B"
  shows "f ` A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` A \<subseteq> B
 2. B \<subseteq> f ` A
[PROOF STEP]
from \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "f ` A \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f ` A \<subseteq> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` A \<subseteq> B

goal (1 subgoal):
 1. B \<subseteq> f ` A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B \<subseteq> f ` A
[PROOF STEP]
show "B \<subseteq> f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> f ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> B \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> B \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
assume "x \<in> B"
[PROOF STATE]
proof (state)
this:
x \<in> B

goal (1 subgoal):
 1. \<And>x. x \<in> B \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
have "{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
proof (cases "card B \<ge> 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
 2. \<not> 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
assume "\<not> card B \<ge> 1"
[PROOF STATE]
proof (state)
this:
\<not> 1 \<le> card B

goal (2 subgoals):
 1. 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
 2. \<not> 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> 1 \<le> card B
[PROOF STEP]
have "card B = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 1 \<le> card B

goal (1 subgoal):
 1. card B = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card B = 0

goal (2 subgoals):
 1. 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
 2. \<not> 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
from this \<open>finite B\<close>
[PROOF STATE]
proof (chain)
picking this:
card B = 0
finite B
[PROOF STEP]
have "B = {}"
[PROOF STATE]
proof (prove)
using this:
card B = 0
finite B

goal (1 subgoal):
 1. B = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B = {}

goal (2 subgoals):
 1. 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
 2. \<not> 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
B = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
B = {}

goal (1 subgoal):
 1. {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
assume "card B \<ge> 1"
[PROOF STATE]
proof (state)
this:
1 \<le> card B

goal (1 subgoal):
 1. 1 \<le> card B \<Longrightarrow> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
assume "\<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B"
[PROOF STATE]
proof (state)
this:
\<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
have "{} \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B"
[PROOF STATE]
proof (prove)
using this:
\<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. {} \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{} \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{} \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
have "card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B
[PROOF STEP]
using \<open>finite B\<close> card_image_le
[PROOF STATE]
proof (prove)
using this:
finite B
finite ?A \<Longrightarrow> card (?f ` ?A) \<le> card ?A

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B

goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B

goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
have "finite ((\<lambda>b. {x \<in> A. f x = b}) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>b. {x \<in> A. f x = b}) ` B)
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite B

goal (1 subgoal):
 1. finite ((\<lambda>b. {x \<in> A. f x = b}) ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>b. {x \<in> A. f x = b}) ` B)

goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{} \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B
card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B
finite ((\<lambda>b. {x \<in> A. f x = b}) ` B)
[PROOF STEP]
have "card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) \<le> card B - 1"
[PROOF STATE]
proof (prove)
using this:
{} \<in> (\<lambda>b. {x \<in> A. f x = b}) ` B
card ((\<lambda>b. {x \<in> A. f x = b}) ` B) \<le> card B
finite ((\<lambda>b. {x \<in> A. f x = b}) ` B)

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) \<le> card B - 1
[PROOF STEP]
by (auto simp add: card_Diff_singleton)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) \<le> card B - 1

goal (1 subgoal):
 1. \<not> {} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B \<Longrightarrow> False
[PROOF STEP]
from this card_eq \<open>card B \<ge> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) \<le> card B - 1
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
1 \<le> card B
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) \<le> card B - 1
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
1 \<le> card B

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B

goal (1 subgoal):
 1. \<And>x. x \<in> B \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
from this \<open>x \<in> B\<close>
[PROOF STATE]
proof (chain)
picking this:
{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
x \<in> B
[PROOF STEP]
show "x \<in> f ` A"
[PROOF STATE]
proof (prove)
using this:
{} \<notin> (\<lambda>b. {x \<in> A. f x = b}) ` B
x \<in> B

goal (1 subgoal):
 1. x \<in> f ` A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<in> f ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
B \<subseteq> f ` A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_partitions_of:
  assumes "F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
  assumes "univ (\<lambda>f. f ` A = B) F"
  shows "card (partitions_of A B F) = card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
from \<open>F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B"
    and F_eq: "F = range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quotientE
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
\<lbrakk>?X \<in> ?A // ?r; \<And>x. \<lbrakk>?X = ?r `` {x}; x \<in> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
F = range_permutation A B `` {f}

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
from this \<open>univ (\<lambda>f. f ` A = B) F\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
F = range_permutation A B `` {f}
univ (\<lambda>f. f ` A = B) F
[PROOF STEP]
have "f ` A = B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
F = range_permutation A B `` {f}
univ (\<lambda>f. f ` A = B) F

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
using univ_commute'[OF equiv_range_permutation surj_on_respects_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>]
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
F = range_permutation A B `` {f}
univ (\<lambda>f. f ` A = B) F
univ (\<lambda>f. f ` A = B) (range_permutation A B `` {f}) = (f ` A = B)

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ` A = B

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
have "card (partitions_of A B F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (partitions_of A B F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F)
[PROOF STEP]
unfolding partitions_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
card (partitions_of A B F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F)

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (partitions_of A B F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F)

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
have "\<dots> = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}))
[PROOF STEP]
unfolding F_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}))

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) F) = card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}))

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
have "\<dots> = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})
[PROOF STEP]
using equiv_range_permutation domain_partitions_respects_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
equiv (?A \<rightarrow>\<^sub>E ?B) (range_permutation ?A ?B)
(\<lambda>f. (\<lambda>b. {x \<in> ?A. f x = b}) ` ?B - {{}}) respects range_permutation ?A ?B
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})
[PROOF STEP]
by (subst univ_commute') auto
[PROOF STATE]
proof (state)
this:
card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (univ (\<lambda>f. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
from \<open>f ` A = B\<close>
[PROOF STATE]
proof (chain)
picking this:
f ` A = B
[PROOF STEP]
have "\<dots> = card B"
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
using surjective_on_implies_card_eq
[PROOF STATE]
proof (prove)
using this:
f ` A = B
?f ` ?A = ?B \<Longrightarrow> card ((\<lambda>b. {x \<in> ?A. ?f x = b}) ` ?B - {{}}) = card ?B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (partitions_of A B F) = card B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (partitions_of A B F) = card B

goal (1 subgoal):
 1. card (partitions_of A B F) = card B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card (partitions_of A B F) = card B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma functions_of_is_surj_on:
  assumes "finite A" "finite B"
  assumes "partition_on A P" "card P = card B"
  shows "univ (\<lambda>f. f ` A = B) (functions_of P A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
have "functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
using functions_of \<open>finite A\<close> \<open>finite B\<close> \<open>partition_on A P\<close> \<open>card P = card B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B; partition_on ?A ?P; card ?P \<le> card ?B\<rbrakk> \<Longrightarrow> functions_of ?P ?A ?B \<in> (?A \<rightarrow>\<^sub>E ?B) // range_permutation ?A ?B
finite A
finite B
partition_on A P
card P = card B

goal (1 subgoal):
 1. functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
[PROOF STEP]
obtain f where eq_f: "functions_of P A B = range_permutation A B `` {f}" and "f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>functions_of P A B = range_permutation A B `` {f}; f \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quotientE
[PROOF STATE]
proof (prove)
using this:
functions_of P A B \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B
\<lbrakk>?X \<in> ?A // ?r; \<And>x. \<lbrakk>?X = ?r `` {x}; x \<in> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>functions_of P A B = range_permutation A B `` {f}; f \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
functions_of P A B = range_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
from eq_f
[PROOF STATE]
proof (chain)
picking this:
functions_of P A B = range_permutation A B `` {f}
[PROOF STEP]
have "f \<in> functions_of P A B"
[PROOF STATE]
proof (prove)
using this:
functions_of P A B = range_permutation A B `` {f}

goal (1 subgoal):
 1. f \<in> functions_of P A B
[PROOF STEP]
using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> equiv_range_permutation equiv_class_self
[PROOF STATE]
proof (prove)
using this:
functions_of P A B = range_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
equiv (?A \<rightarrow>\<^sub>E ?B) (range_permutation ?A ?B)
\<lbrakk>equiv ?A ?r; ?a \<in> ?A\<rbrakk> \<Longrightarrow> ?a \<in> ?r `` {?a}

goal (1 subgoal):
 1. f \<in> functions_of P A B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f \<in> functions_of P A B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
from \<open>f \<in> functions_of P A B\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> functions_of P A B
[PROOF STEP]
have eq: "(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P"
[PROOF STATE]
proof (prove)
using this:
f \<in> functions_of P A B

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P}

goal (1 subgoal):
 1. (\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
[PROOF STEP]
have "card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
using \<open>card P = card B\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>b. {x \<in> A. f x = b}) ` B - {{}} = P
card P = card B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
from \<open>finite B\<close> \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> this
[PROOF STATE]
proof (chain)
picking this:
finite B
f \<in> A \<rightarrow>\<^sub>E B
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
have "f ` A = B"
[PROOF STATE]
proof (prove)
using this:
finite B
f \<in> A \<rightarrow>\<^sub>E B
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
using card_eq_implies_surjective_on
[PROOF STATE]
proof (prove)
using this:
finite B
f \<in> A \<rightarrow>\<^sub>E B
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
\<lbrakk>finite ?B; ?f \<in> ?A \<rightarrow>\<^sub>E ?B; card ((\<lambda>b. {x \<in> ?A. ?f x = b}) ` ?B - {{}}) = card ?B\<rbrakk> \<Longrightarrow> ?f ` ?A = ?B

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` A = B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f ` A = B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (functions_of P A B)
[PROOF STEP]
unfolding eq_f
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (range_permutation A B `` {f})
[PROOF STEP]
using equiv_range_permutation surj_on_respects_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
f ` A = B
equiv (?A \<rightarrow>\<^sub>E ?B) (range_permutation ?A ?B)
(\<lambda>f. f ` ?A = ?B) respects range_permutation ?A ?B
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (range_permutation A B `` {f})
[PROOF STEP]
by (subst univ_commute') assumption+
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. f ` A = B) (functions_of P A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_partitions_of:
  assumes "finite A" "finite B"
  shows "bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="\<lambda>P. functions_of P A B"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B. functions_of (partitions_of A B a) A B = a
 2. \<forall>a'\<in>{P. partition_on A P \<and> card P = card B}. partitions_of A B (functions_of a' A B) = a'
 3. partitions_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P = card B}
 4. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B
[PROOF STEP]
have quotient_eq: "{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B = {F \<in> ((A \<rightarrow>\<^sub>E B) // range_permutation A B). univ (\<lambda>f. f ` A = B) F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. f ` A = B) F}
[PROOF STEP]
using equiv_range_permutation[of A B] surj_on_respects_range_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
equiv (A \<rightarrow>\<^sub>E B) (range_permutation A B)
(\<lambda>f. f ` A = B) respects range_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. f ` A = B) F}
[PROOF STEP]
by (simp only: univ_preserves_predicate)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. f ` A = B) F}

goal (4 subgoals):
 1. \<forall>a\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B. functions_of (partitions_of A B a) A B = a
 2. \<forall>a'\<in>{P. partition_on A P \<and> card P = card B}. partitions_of A B (functions_of a' A B) = a'
 3. partitions_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P = card B}
 4. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B
[PROOF STEP]
show "\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B. functions_of (partitions_of A B F) A B = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite B

goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B. functions_of (partitions_of A B F) A B = F
[PROOF STEP]
by (simp add: functions_of_partitions_of quotient_eq)
[PROOF STATE]
proof (state)
this:
\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B. functions_of (partitions_of A B F) A B = F

goal (3 subgoals):
 1. \<forall>a'\<in>{P. partition_on A P \<and> card P = card B}. partitions_of A B (functions_of a' A B) = a'
 2. partitions_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P = card B}
 3. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B
[PROOF STEP]
show "\<forall>P\<in>{P. partition_on A P \<and> card P = card B}. partitions_of A B (functions_of P A B) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>{P. partition_on A P \<and> card P = card B}. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. \<forall>P\<in>{P. partition_on A P \<and> card P = card B}. partitions_of A B (functions_of P A B) = P
[PROOF STEP]
by (auto simp add: partitions_of_functions_of)
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>{P. partition_on A P \<and> card P = card B}. partitions_of A B (functions_of P A B) = P

goal (2 subgoals):
 1. partitions_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P = card B}
 2. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B
[PROOF STEP]
show "partitions_of A B ` ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) \<subseteq> {P. partition_on A P \<and> card P = card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partitions_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P = card B}
[PROOF STEP]
using \<open>finite B\<close> quotient_eq card_partitions_of partitions_of
[PROOF STATE]
proof (prove)
using this:
finite B
{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // range_permutation A B. univ (\<lambda>f. f ` A = B) F}
\<lbrakk>?F \<in> (?A \<rightarrow>\<^sub>E ?B) // range_permutation ?A ?B; univ (\<lambda>f. f ` ?A = ?B) ?F\<rbrakk> \<Longrightarrow> card (partitions_of ?A ?B ?F) = card ?B
\<lbrakk>finite ?B; ?F \<in> (?A \<rightarrow>\<^sub>E ?B) // range_permutation ?A ?B\<rbrakk> \<Longrightarrow> card (partitions_of ?A ?B ?F) \<le> card ?B
\<lbrakk>finite ?B; ?F \<in> (?A \<rightarrow>\<^sub>E ?B) // range_permutation ?A ?B\<rbrakk> \<Longrightarrow> partition_on ?A (partitions_of ?A ?B ?F)

goal (1 subgoal):
 1. partitions_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P = card B}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
partitions_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B \<subseteq> {P. partition_on A P \<and> card P = card B}

goal (1 subgoal):
 1. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B
[PROOF STEP]
show "(\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. (\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B
[PROOF STEP]
by (auto simp add: quotient_eq intro: functions_of functions_of_is_surj_on)
[PROOF STATE]
proof (state)
this:
(\<lambda>P. functions_of P A B) ` {P. partition_on A P \<and> card P = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_surjective_functions_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
have "bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}
[PROOF STEP]
by (rule bij_betw_partitions_of)
[PROOF STATE]
proof (state)
this:
bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}
[PROOF STEP]
have "card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = card {P. partition_on A P \<and> card P = card B}"
[PROOF STATE]
proof (prove)
using this:
bij_betw (partitions_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) {P. partition_on A P \<and> card P = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = card {P. partition_on A P \<and> card P = card B}
[PROOF STEP]
by (rule bij_betw_same_card)
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = card {P. partition_on A P \<and> card P = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = card {P. partition_on A P \<and> card P = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
have "card {P. partition_on A P \<and> card P = card B} = Stirling (card A) (card B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P = card B} = Stirling (card A) (card B)
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. card {P. partition_on A P \<and> card P = card B} = Stirling (card A) (card B)
[PROOF STEP]
by (rule card_partition_on)
[PROOF STATE]
proof (state)
this:
card {P. partition_on A P \<and> card P = card B} = Stirling (card A) (card B)

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equiv_defs_P1:
  assumes lossless_D: "\<forall> view. lossless_spmf ((D:: 'view1 adversary_det) view)"
  shows "adv_P1_game m1 m2 D = adv_P1 m1 m2 D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
have return_True_not_False: "spmf (return_spmf (b)) True = spmf (return_spmf (\<not> b)) False"
    for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (return_spmf b) True = spmf (return_spmf (\<not> b)) False
[PROOF STEP]
by(cases b; auto)
[PROOF STATE]
proof (state)
this:
spmf (return_spmf ?b) True = spmf (return_spmf (\<not> ?b)) False

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
have lossless_ideal: "lossless_spmf ((funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))
[PROOF STEP]
by(simp add: lossless_S1 lossless_funct lossless_weight_spmfD split_def lossless_D)
[PROOF STATE]
proof (state)
this:
lossless_spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
have return: "spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S1 m1 o1 \<bind> D)) True
                  = spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S1 m1 o1 \<bind> (\<lambda> view. D view \<bind> (\<lambda> b. return_spmf b)))) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S1 m1 o1 \<bind> D)) True = spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S1 m1 o1 \<bind> (\<lambda>view. D view \<bind> return_spmf))) True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S1 m1 o1 \<bind> D)) True = spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S1 m1 o1 \<bind> (\<lambda>view. D view \<bind> return_spmf))) True

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
have "2*(spmf (P1_game_alt m1 m2 D ) True) - 1 = (spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>(b':: bool). return_spmf (True = b'))))) True
        - (1 - (spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))) True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * spmf (P1_game_alt m1 m2 D) True - 1 = spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)
[PROOF STEP]
by(simp add: spmf_bind integral_spmf_of_set adv_P1_game_def P1_game_alt_def spmf_of_set
          UNIV_bool bind_spmf_const lossless_R1 lossless_S1 lossless_funct lossless_weight_spmfD)
[PROOF STATE]
proof (state)
this:
2 * spmf (P1_game_alt m1 m2 D) True - 1 = spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
hence "adv_P1_game m1 m2 D = \<bar>(spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>(b':: bool). return_spmf (True = b'))))) True
        - (1 - (spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))) True)\<bar>"
[PROOF STATE]
proof (prove)
using this:
2 * spmf (P1_game_alt m1 m2 D) True - 1 = spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = \<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
[PROOF STEP]
using adv_P1_game_def
[PROOF STATE]
proof (prove)
using this:
2 * spmf (P1_game_alt m1 m2 D) True - 1 = spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)
adv_P1_game ?m1.0 ?m2.0 ?D = \<bar>2 * spmf (P1_game_alt ?m1.0 ?m2.0 ?D) True - 1\<bar>

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = \<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adv_P1_game m1 m2 D = \<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
adv_P1_game m1 m2 D = \<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
have "\<bar>(spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>(b':: bool). return_spmf (True = b'))))) True
                      - (1 - (spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview
                            \<bind> (\<lambda>b'. return_spmf (False = b')))))) True)\<bar> = adv_P1 m1 m2 D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P1 m1 m2 D
[PROOF STEP]
apply(simp only: adv_P1_def spmf_False_conv_True[symmetric] lossless_ideal; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1 m1 m2 \<bind> D) True - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (\<not> b'))))) False\<bar> = \<bar>spmf (R1 m1 m2 \<bind> D) True - spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S1 m1 o1 \<bind> D)) True\<bar>
[PROOF STEP]
by(simp only: return)(simp only: split_def spmf_bind return_True_not_False)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P1 m1 m2 D

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
adv_P1_game m1 m2 D = \<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
\<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P1 m1 m2 D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
adv_P1_game m1 m2 D = \<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
\<bar>spmf (R1 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S1 m1 out1 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P1 m1 m2 D

goal (1 subgoal):
 1. adv_P1_game m1 m2 D = adv_P1 m1 m2 D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adv_P1_game m1 m2 D = adv_P1 m1 m2 D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equiv_defs_P2:
  assumes lossless_D: "\<forall> view. lossless_spmf ((D:: 'view2 adversary_det) view)"
  shows "adv_P2_game m1 m2 D = adv_P2 m1 m2 D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
have return_True_not_False: "spmf (return_spmf (b)) True = spmf (return_spmf (\<not> b)) False"
    for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (return_spmf b) True = spmf (return_spmf (\<not> b)) False
[PROOF STEP]
by(cases b; auto)
[PROOF STATE]
proof (state)
this:
spmf (return_spmf ?b) True = spmf (return_spmf (\<not> ?b)) False

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
have lossless_ideal: "lossless_spmf ((funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))
[PROOF STEP]
by(simp add: lossless_S2 lossless_funct lossless_weight_spmfD split_def lossless_D)
[PROOF STATE]
proof (state)
this:
lossless_spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
have return: "spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S2 m2 o2 \<bind> D)) True = spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S2 m2 o2 \<bind> (\<lambda> view. D view \<bind> (\<lambda> b. return_spmf b)))) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S2 m2 o2 \<bind> D)) True = spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S2 m2 o2 \<bind> (\<lambda>view. D view \<bind> return_spmf))) True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S2 m2 o2 \<bind> D)) True = spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S2 m2 o2 \<bind> (\<lambda>view. D view \<bind> return_spmf))) True

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
have
    "2*(spmf (P2_game_alt m1 m2 D ) True) - 1 = (spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>(b':: bool). return_spmf (True = b'))))) True
        - (1 - (spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))) True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * spmf (P2_game_alt m1 m2 D) True - 1 = spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)
[PROOF STEP]
by(simp add: spmf_bind integral_spmf_of_set adv_P1_game_def P2_game_alt_def spmf_of_set
          UNIV_bool bind_spmf_const lossless_R2 lossless_S2 lossless_funct lossless_weight_spmfD)
[PROOF STATE]
proof (state)
this:
2 * spmf (P2_game_alt m1 m2 D) True - 1 = spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
hence "adv_P2_game m1 m2 D = \<bar>(spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>(b':: bool). return_spmf (True = b'))))) True
        - (1 - (spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))) True)\<bar>"
[PROOF STATE]
proof (prove)
using this:
2 * spmf (P2_game_alt m1 m2 D) True - 1 = spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = \<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
[PROOF STEP]
using adv_P2_game_def
[PROOF STATE]
proof (prove)
using this:
2 * spmf (P2_game_alt m1 m2 D) True - 1 = spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)
adv_P2_game ?m1.0 ?m2.0 ?D = \<bar>2 * spmf (P2_game_alt ?m1.0 ?m2.0 ?D) True - 1\<bar>

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = \<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adv_P2_game m1 m2 D = \<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
adv_P2_game m1 m2 D = \<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
have "\<bar>(spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>(b':: bool). return_spmf (True = b'))))) True
        - (1 - (spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b')))))) True)\<bar> = adv_P2 m1 m2 D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P2 m1 m2 D
[PROOF STEP]
apply(simp only: adv_P2_def spmf_False_conv_True[symmetric] lossless_ideal; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R2 m1 m2 \<bind> D) True - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (\<not> b'))))) False\<bar> = \<bar>spmf (R2 m1 m2 \<bind> D) True - spmf (funct m1 m2 \<bind> (\<lambda>(o1, o2). S2 m2 o2 \<bind> D)) True\<bar>
[PROOF STEP]
by(simp only: return)(simp only: split_def spmf_bind return_True_not_False)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P2 m1 m2 D

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
adv_P2_game m1 m2 D = \<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
\<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P2 m1 m2 D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
adv_P2_game m1 m2 D = \<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar>
\<bar>spmf (R2 m1 m2 \<bind> (\<lambda>rview. D rview \<bind> (\<lambda>b'. return_spmf (True = b')))) True - (1 - spmf (funct m1 m2 \<bind> (\<lambda>(out1, out2). S2 m2 out2 \<bind> (\<lambda>sview. D sview \<bind> (\<lambda>b'. return_spmf (False = b'))))) True)\<bar> = adv_P2 m1 m2 D

goal (1 subgoal):
 1. adv_P2_game m1 m2 D = adv_P2 m1 m2 D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adv_P2_game m1 m2 D = adv_P2 m1 m2 D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gtarget_alt_def: "gtarget r v = last (v # r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtarget r v = last (v # r)
[PROOF STEP]
using fold_const
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>x _. x) ?xs ?a = last (?a # ?xs)

goal (1 subgoal):
 1. gtarget r v = last (v # r)
[PROOF STEP]
by this


[STATEMENT]
lemma gstates_alt_def: "gstates r v = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gstates r v = r
[PROOF STEP]
by simp


[STATEMENT]
lemma gtrace_alt_def: "gtrace r v = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtrace r v = r
[PROOF STEP]
by simp


[STATEMENT]
lemma gpath_elim[elim?]:
    assumes "gpath A w V s v"
    obtains r k p
    where "s = [Suc k ..< Suc k + length r] || r" "v = (k, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = [Suc k..<Suc k + length r] || r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = [Suc k..<Suc k + length r] || r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain t r where 1: "s = t || r" "length t = length r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t r. \<lbrakk>s = t || r; length t = length r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using zip_map_fst_snd[of s]
[PROOF STATE]
proof (prove)
using this:
map fst s || map snd s = s

goal (1 subgoal):
 1. (\<And>t r. \<lbrakk>s = t || r; length t = length r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis length_map)
[PROOF STATE]
proof (state)
this:
s = t || r
length t = length r

goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = [Suc k..<Suc k + length r] || r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain k p where 2: "v = (k, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k p. v = (k, p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
v = (k, p)

goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = [Suc k..<Suc k + length r] || r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 3: "t = [Suc k ..< Suc k + length r]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = [Suc k..<Suc k + length r]
[PROOF STEP]
using assms 1 2
[PROOF STATE]
proof (prove)
using this:
gpath A w V s v
s = t || r
length t = length r
v = (k, p)

goal (1 subgoal):
 1. t = [Suc k..<Suc k + length r]
[PROOF STEP]
proof (induct arbitrary: t r k p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p t r k pa. \<lbrakk>[] = t || r; length t = length r; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length r]
 2. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
case (nil v)
[PROOF STATE]
proof (state)
this:
[] = t || r
length t = length r
v = (k, p)

goal (2 subgoals):
 1. \<And>p t r k pa. \<lbrakk>[] = t || r; length t = length r; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length r]
 2. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] = t || r
length t = length r
v = (k, p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] = t || r
length t = length r
v = (k, p)

goal (1 subgoal):
 1. t = [Suc k..<Suc k + length r]
[PROOF STEP]
by (metis add_0_right le_add1 length_0_conv length_zip min.idem upt_conv_Nil)
[PROOF STATE]
proof (state)
this:
t = [Suc k..<Suc k + length r]

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
case (cons u v s)
[PROOF STATE]
proof (state)
this:
case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> u \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V
gpath A w V s u
\<lbrakk>s = ?t || ?r; length ?t = length ?r; u = (?k, ?p)\<rbrakk> \<Longrightarrow> ?t = [Suc ?k..<Suc ?k + length ?r]
u # s = t || r
length t = length r
v = (k, p)

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
have 1: "t || r = (hd t, hd r) # (tl t || tl r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t || r = (hd t, hd r) # (tl t || tl r)
[PROOF STEP]
by (metis cons.prems(1) hd_Cons_tl neq_Nil_conv zip.simps(1) zip_Cons_Cons zip_Nil)
[PROOF STATE]
proof (state)
this:
t || r = (hd t, hd r) # (tl t || tl r)

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
have 2: "s = tl t || tl r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = tl t || tl r
[PROOF STEP]
using cons 1
[PROOF STATE]
proof (prove)
using this:
case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> u \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V
gpath A w V s u
\<lbrakk>s = ?t || ?r; length ?t = length ?r; u = (?k, ?p)\<rbrakk> \<Longrightarrow> ?t = [Suc ?k..<Suc ?k + length ?r]
u # s = t || r
length t = length r
v = (k, p)
t || r = (hd t, hd r) # (tl t || tl r)

goal (1 subgoal):
 1. s = tl t || tl r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s = tl t || tl r

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
have "t = hd t # tl t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = hd t # tl t
[PROOF STEP]
using cons(4)
[PROOF STATE]
proof (prove)
using this:
u # s = t || r

goal (1 subgoal):
 1. t = hd t # tl t
[PROOF STEP]
by (metis hd_Cons_tl list.simps(3) zip_Nil)
[PROOF STATE]
proof (state)
this:
t = hd t # tl t

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t = hd t # tl t

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
have "hd t = Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd t = Suc k
[PROOF STEP]
using "1" cons.hyps(1) cons.prems(1) cons.prems(3)
[PROOF STATE]
proof (prove)
using this:
t || r = (hd t, hd r) # (tl t || tl r)
case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> u \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V
u # s = t || r
v = (k, p)

goal (1 subgoal):
 1. hd t = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd t = Suc k

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hd t = Suc k

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
have "tl t = [Suc (Suc k) ..< Suc (Suc k) + length (tl r)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl t = [Suc (Suc k)..<Suc (Suc k) + length (tl r)]
[PROOF STEP]
using cons(3)[OF 2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length (tl t) = length (tl r); u = (?k, ?p)\<rbrakk> \<Longrightarrow> tl t = [Suc ?k..<Suc ?k + length (tl r)]

goal (1 subgoal):
 1. tl t = [Suc (Suc k)..<Suc (Suc k) + length (tl r)]
[PROOF STEP]
using "1" \<open>hd t = Suc k\<close> cons.prems(1) cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length (tl t) = length (tl r); u = (?k, ?p)\<rbrakk> \<Longrightarrow> tl t = [Suc ?k..<Suc ?k + length (tl r)]
t || r = (hd t, hd r) # (tl t || tl r)
hd t = Suc k
u # s = t || r
length t = length r

goal (1 subgoal):
 1. tl t = [Suc (Suc k)..<Suc (Suc k) + length (tl r)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tl t = [Suc (Suc k)..<Suc (Suc k) + length (tl r)]

goal (1 subgoal):
 1. \<And>a p r t ra k pa. \<lbrakk>case p of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; gpath A w V r a; \<And>t ra k p. \<lbrakk>r = t || ra; length t = length ra; a = (k, p)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]; a # r = t || ra; length t = length ra; p = (k, pa)\<rbrakk> \<Longrightarrow> t = [Suc k..<Suc k + length ra]
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
t = Suc k # [Suc (Suc k)..<Suc (Suc k) + length (tl r)]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
t = Suc k # [Suc (Suc k)..<Suc (Suc k) + length (tl r)]

goal (1 subgoal):
 1. t = [Suc k..<Suc k + length r]
[PROOF STEP]
using cons.prems(2) upt_rec
[PROOF STATE]
proof (prove)
using this:
t = Suc k # [Suc (Suc k)..<Suc (Suc k) + length (tl r)]
length t = length r
[?i..<?j] = (if ?i < ?j then ?i # [Suc ?i..<?j] else [])

goal (1 subgoal):
 1. t = [Suc k..<Suc k + length r]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = [Suc k..<Suc k + length r]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t = [Suc k..<Suc k + length r]

goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = [Suc k..<Suc k + length r] || r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that 1 2 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s = [Suc ?k..<Suc ?k + length ?r] || ?r; v = (?k, ?p)\<rbrakk> \<Longrightarrow> thesis
s = t || r
length t = length r
v = (k, p)
t = [Suc k..<Suc k + length r]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gpath_path[symmetric]: "path A (stake (length r) (sdrop k w) || r) p \<longleftrightarrow>
    gpath A w UNIV ([Suc k ..< Suc k + length r] || r) (k, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)
[PROOF STEP]
proof (induct r arbitrary: k p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k p. path A (stake (length []) (sdrop k w) || []) p = gupath A w ([Suc k..<Suc k + length []] || []) (k, p)
 2. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
case (Nil)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>k p. path A (stake (length []) (sdrop k w) || []) p = gupath A w ([Suc k..<Suc k + length []] || []) (k, p)
 2. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A (stake (length []) (sdrop k w) || []) p = gupath A w ([Suc k..<Suc k + length []] || []) (k, p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A (stake (length []) (sdrop k w) || []) p = gupath A w ([Suc k..<Suc k + length []] || []) (k, p)

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
case (Cons q r)
[PROOF STATE]
proof (state)
this:
path A (stake (length r) (sdrop ?k w) || r) ?p = gupath A w ([Suc ?k..<Suc ?k + length r] || r) (?k, ?p)

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
have 1: "path A (stake (length r) (sdrop (Suc k) w) || r) q \<longleftrightarrow>
      gpath A w UNIV ([Suc (Suc k) ..< Suc k + length (q # r)] || r) (Suc k, q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A (stake (length r) (sdrop (Suc k) w) || r) q = gupath A w ([Suc (Suc k)..<Suc k + length (q # r)] || r) (Suc k, q)
[PROOF STEP]
using Cons[of "Suc k" "q"]
[PROOF STATE]
proof (prove)
using this:
path A (stake (length r) (sdrop (Suc k) w) || r) q = gupath A w ([Suc (Suc k)..<Suc (Suc k) + length r] || r) (Suc k, q)

goal (1 subgoal):
 1. path A (stake (length r) (sdrop (Suc k) w) || r) q = gupath A w ([Suc (Suc k)..<Suc k + length (q # r)] || r) (Suc k, q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
path A (stake (length r) (sdrop (Suc k) w) || r) q = gupath A w ([Suc (Suc k)..<Suc k + length (q # r)] || r) (Suc k, q)

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
have "stake (length (q # r)) (sdrop k w) || q # r =
      (w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake (length (q # r)) (sdrop k w) || q # r = (w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stake (length (q # r)) (sdrop k w) || q # r = (w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stake (length (q # r)) (sdrop k w) || q # r = (w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
have "path A \<dots> p \<longleftrightarrow>
      gpath A w UNIV ((Suc k, q) # ([Suc (Suc k) ..< Suc k + length (q # r)] || r)) (k, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A ((w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)) p = gupath A w ((Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r)) (k, p)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
path A (stake (length r) (sdrop (Suc k) w) || r) q = gupath A w ([Suc (Suc k)..<Suc k + length (q # r)] || r) (Suc k, q)

goal (1 subgoal):
 1. path A ((w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)) p = gupath A w ((Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r)) (k, p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A ((w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)) p = gupath A w ((Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r)) (k, p)

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
path A ((w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)) p = gupath A w ((Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r)) (k, p)

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
have "(Suc k, q) # ([Suc (Suc k) ..< Suc k + length (q # r)] || r) =
      Suc k # [Suc (Suc k) ..< Suc k + length (q # r)] || q # r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r) = Suc k # [Suc (Suc k)..<Suc k + length (q # r)] || q # r
[PROOF STEP]
unfolding zip_Cons_Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r) = (Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
(Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r) = Suc k # [Suc (Suc k)..<Suc k + length (q # r)] || q # r

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Suc k, q) # ([Suc (Suc k)..<Suc k + length (q # r)] || r) = Suc k # [Suc (Suc k)..<Suc k + length (q # r)] || q # r

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
have "Suc k # [Suc (Suc k) ..< Suc k + length (q # r)] = [Suc k ..< Suc k + length (q # r)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k # [Suc (Suc k)..<Suc k + length (q # r)] = [Suc k..<Suc k + length (q # r)]
[PROOF STEP]
by (simp add: upt_rec)
[PROOF STATE]
proof (state)
this:
Suc k # [Suc (Suc k)..<Suc k + length (q # r)] = [Suc k..<Suc k + length (q # r)]

goal (1 subgoal):
 1. \<And>a r k p. (\<And>k p. path A (stake (length r) (sdrop k w) || r) p = gupath A w ([Suc k..<Suc k + length r] || r) (k, p)) \<Longrightarrow> path A (stake (length (a # r)) (sdrop k w) || a # r) p = gupath A w ([Suc k..<Suc k + length (a # r)] || a # r) (k, p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
path A (stake (length (q # r)) (sdrop k w) || q # r) p = gupath A w ([Suc k..<Suc k + length (q # r)] || q # r) (k, p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path A (stake (length (q # r)) (sdrop k w) || q # r) p = gupath A w ([Suc k..<Suc k + length (q # r)] || q # r) (k, p)

goal (1 subgoal):
 1. path A (stake (length (q # r)) (sdrop k w) || q # r) p = gupath A w ([Suc k..<Suc k + length (q # r)] || q # r) (k, p)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
path A (stake (length (q # r)) (sdrop k w) || q # r) p = gupath A w ([Suc k..<Suc k + length (q # r)] || q # r) (k, p)

goal:
No subgoals!
[PROOF STEP]
qed