[STATEMENT]
lemma [autoref_itype]:
  "NO_CYC ::\<^sub>i i_blue_wit"
  "(=) ::\<^sub>i i_blue_wit \<rightarrow>\<^sub>i i_blue_wit \<rightarrow>\<^sub>i i_bool"
  "init_wit_blue ::\<^sub>i I \<rightarrow>\<^sub>i i_red_wit I \<rightarrow>\<^sub>i i_blue_wit"
  "init_wit_blue_early ::\<^sub>i I \<rightarrow>\<^sub>i I \<rightarrow>\<^sub>i i_blue_wit"
  "prep_wit_blue ::\<^sub>i I \<rightarrow>\<^sub>i i_blue_wit \<rightarrow>\<^sub>i i_blue_wit"
  "red_init_witness ::\<^sub>i I \<rightarrow>\<^sub>i I \<rightarrow>\<^sub>i i_red_wit I"
  "prep_wit_red ::\<^sub>i I \<rightarrow>\<^sub>i i_red_wit I \<rightarrow>\<^sub>i i_red_wit I"
  "extract_res ::\<^sub>i i_blue_wit \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>I\<rangle>\<^sub>ii_list, \<langle>I\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_option"
  "red_dfs ::\<^sub>i \<langle>I\<rangle>\<^sub>ii_slg \<rightarrow>\<^sub>i \<langle>I\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>I\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i I
    \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>I\<rangle>\<^sub>ii_set, i_red_wit I\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_nres"
  "blue_dfs ::\<^sub>i i_bg i_unit I
    \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>\<langle>I\<rangle>\<^sub>ii_list, \<langle>I\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_option\<rangle>\<^sub>ii_nres"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((NO_CYC ::\<^sub>i i_blue_wit &&& (=) ::\<^sub>i i_blue_wit \<rightarrow>\<^sub>i i_blue_wit \<rightarrow>\<^sub>i i_bool) &&& init_wit_blue ::\<^sub>i I \<rightarrow>\<^sub>i i_red_wit I \<rightarrow>\<^sub>i i_blue_wit &&& init_wit_blue_early ::\<^sub>i I \<rightarrow>\<^sub>i I \<rightarrow>\<^sub>i i_blue_wit &&& prep_wit_blue ::\<^sub>i I \<rightarrow>\<^sub>i i_blue_wit \<rightarrow>\<^sub>i i_blue_wit) &&& (red_init_witness ::\<^sub>i I \<rightarrow>\<^sub>i I \<rightarrow>\<^sub>i i_red_wit I &&& prep_wit_red ::\<^sub>i I \<rightarrow>\<^sub>i i_red_wit I \<rightarrow>\<^sub>i i_red_wit I) &&& extract_res ::\<^sub>i i_blue_wit \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>I\<rangle>\<^sub>ii_list, \<langle>I\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_option &&& red_dfs ::\<^sub>i \<langle>I\<rangle>\<^sub>ii_slg \<rightarrow>\<^sub>i \<langle>I\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>I\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i I \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>I\<rangle>\<^sub>ii_set, i_red_wit I\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_nres &&& blue_dfs ::\<^sub>i i_bg i_unit I \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>\<langle>I\<rangle>\<^sub>ii_list, \<langle>I\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_option\<rangle>\<^sub>ii_nres
[PROOF STEP]
by auto


[STATEMENT]
lemma [autoref_op_pat]: "NO_CYC \<equiv> OP NO_CYC :::\<^sub>i i_blue_wit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NO_CYC \<equiv> OP NO_CYC :::\<^sub>i i_blue_wit
[PROOF STEP]
by simp


[STATEMENT]
lemma autoref_wit[autoref_rules_raw]:
  "(NO_CYC,NO_CYC)\<in>blue_wit_rel"
  "((=), (=)) \<in> blue_wit_rel \<rightarrow> blue_wit_rel \<rightarrow> bool_rel"
  "\<And>R. PREFER_id R
    \<Longrightarrow> (init_wit_blue, init_wit_blue) \<in> R \<rightarrow> red_wit_rel R \<rightarrow> blue_wit_rel"
  "\<And>R. PREFER_id R
    \<Longrightarrow> (init_wit_blue_early, init_wit_blue_early) \<in> R \<rightarrow> R \<rightarrow> blue_wit_rel"
  "\<And>R. PREFER_id R
    \<Longrightarrow> (prep_wit_blue,prep_wit_blue)\<in>R \<rightarrow> blue_wit_rel \<rightarrow> blue_wit_rel"
  "\<And>R. PREFER_id R
    \<Longrightarrow> (red_init_witness, red_init_witness) \<in> R\<rightarrow>R\<rightarrow>red_wit_rel R"
  "\<And>R. PREFER_id R
    \<Longrightarrow> (prep_wit_red,prep_wit_red) \<in> R \<rightarrow> red_wit_rel R \<rightarrow> red_wit_rel R"
  "\<And>R. PREFER_id R
    \<Longrightarrow> (extract_res,extract_res)
        \<in> blue_wit_rel \<rightarrow> \<langle>\<langle>R\<rangle>list_rel\<times>\<^sub>r\<langle>R\<rangle>list_rel\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((NO_CYC, NO_CYC) \<in> blue_wit_rel &&& ((=), (=)) \<in> blue_wit_rel \<rightarrow> blue_wit_rel \<rightarrow> bool_rel) &&& (\<And>R. PREFER_id R \<Longrightarrow> (init_wit_blue, init_wit_blue) \<in> R \<rightarrow> red_wit_rel R \<rightarrow> blue_wit_rel) &&& (\<And>R. PREFER_id R \<Longrightarrow> (init_wit_blue_early, init_wit_blue_early) \<in> R \<rightarrow> R \<rightarrow> blue_wit_rel)) &&& ((\<And>R. PREFER_id R \<Longrightarrow> (prep_wit_blue, prep_wit_blue) \<in> R \<rightarrow> blue_wit_rel \<rightarrow> blue_wit_rel) &&& (\<And>R. PREFER_id R \<Longrightarrow> (red_init_witness, red_init_witness) \<in> R \<rightarrow> R \<rightarrow> red_wit_rel R)) &&& (\<And>R. PREFER_id R \<Longrightarrow> (prep_wit_red, prep_wit_red) \<in> R \<rightarrow> red_wit_rel R \<rightarrow> red_wit_rel R) &&& (\<And>R. PREFER_id R \<Longrightarrow> (extract_res, extract_res) \<in> blue_wit_rel \<rightarrow> \<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>option_rel)
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma impl_red_dfs_autoref[autoref_rules]:
  fixes R :: "('a\<times>'a::linorder) set"
  assumes "PREFER_id R"
  shows "(impl_red_dfs, red_dfs) \<in>
    \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>dflt_rs_rel \<rightarrow> \<langle>R\<rangle>dflt_rs_rel \<rightarrow> R
    \<rightarrow> \<langle>\<langle>R\<rangle>dflt_rs_rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (impl_red_dfs, red_dfs) \<in> \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>dflt_rs_rel \<rightarrow> \<langle>R\<rangle>dflt_rs_rel \<rightarrow> R \<rightarrow> \<langle>\<langle>R\<rangle>dflt_rs_rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel
[PROOF STEP]
using assms impl_red_dfs.refine
[PROOF STATE]
proof (prove)
using this:
PREFER_id R
(impl_red_dfs, red_dfs) \<in> \<langle>Id\<rangle>slg_rel \<rightarrow> \<langle>Id\<rangle>dflt_rs_rel \<rightarrow> \<langle>Id\<rangle>dflt_rs_rel \<rightarrow> Id \<rightarrow> \<langle>\<langle>Id\<rangle>dflt_rs_rel \<times>\<^sub>r red_wit_rel Id\<rangle>nres_rel

goal (1 subgoal):
 1. (impl_red_dfs, red_dfs) \<in> \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>dflt_rs_rel \<rightarrow> \<langle>R\<rangle>dflt_rs_rel \<rightarrow> R \<rightarrow> \<langle>\<langle>R\<rangle>dflt_rs_rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma impl_red_dfs_hash_autoref[autoref_rules]:
  fixes R :: "('a\<times>'a::hashable) set"
  assumes "PREFER_id R"
  shows "(impl_red_dfs_hash, red_dfs) \<in>
    \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>hs.rel \<rightarrow> \<langle>R\<rangle>hs.rel \<rightarrow> R
    \<rightarrow> \<langle>\<langle>R\<rangle>hs.rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (impl_red_dfs_hash, red_dfs) \<in> \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>hs.rel \<rightarrow> \<langle>R\<rangle>hs.rel \<rightarrow> R \<rightarrow> \<langle>\<langle>R\<rangle>hs.rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel
[PROOF STEP]
using assms impl_red_dfs_hash.refine
[PROOF STATE]
proof (prove)
using this:
PREFER_id R
(impl_red_dfs_hash, red_dfs) \<in> \<langle>Id\<rangle>slg_rel \<rightarrow> \<langle>Id\<rangle>hs.rel \<rightarrow> \<langle>Id\<rangle>hs.rel \<rightarrow> Id \<rightarrow> \<langle>\<langle>Id\<rangle>hs.rel \<times>\<^sub>r red_wit_rel Id\<rangle>nres_rel

goal (1 subgoal):
 1. (impl_red_dfs_hash, red_dfs) \<in> \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>hs.rel \<rightarrow> \<langle>R\<rangle>hs.rel \<rightarrow> R \<rightarrow> \<langle>\<langle>R\<rangle>hs.rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma impl_red_dfs_ahs_autoref[autoref_rules]:
  fixes R :: "('a\<times>'a::hashable) set"
  assumes "PREFER_id R"
  shows "(impl_red_dfs_ahs, red_dfs) \<in>
    \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>ahs.rel \<rightarrow> \<langle>R\<rangle>ahs.rel \<rightarrow> R
    \<rightarrow> \<langle>\<langle>R\<rangle>ahs.rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (impl_red_dfs_ahs, red_dfs) \<in> \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>ahs.rel \<rightarrow> \<langle>R\<rangle>ahs.rel \<rightarrow> R \<rightarrow> \<langle>\<langle>R\<rangle>ahs.rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel
[PROOF STEP]
using assms impl_red_dfs_ahs.refine
[PROOF STATE]
proof (prove)
using this:
PREFER_id R
(impl_red_dfs_ahs, red_dfs) \<in> \<langle>Id\<rangle>slg_rel \<rightarrow> \<langle>Id\<rangle>ahs.rel \<rightarrow> \<langle>Id\<rangle>ahs.rel \<rightarrow> Id \<rightarrow> \<langle>\<langle>Id\<rangle>ahs.rel \<times>\<^sub>r red_wit_rel Id\<rangle>nres_rel

goal (1 subgoal):
 1. (impl_red_dfs_ahs, red_dfs) \<in> \<langle>R\<rangle>slg_rel \<rightarrow> \<langle>R\<rangle>ahs.rel \<rightarrow> \<langle>R\<rangle>ahs.rel \<rightarrow> R \<rightarrow> \<langle>\<langle>R\<rangle>ahs.rel \<times>\<^sub>r red_wit_rel R\<rangle>nres_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma impl_blue_dfs_autoref[autoref_rules]:
  fixes R :: "('a \<times> 'a::linorder) set"
  assumes "PREFER_id R"
  shows "(impl_blue_dfs, blue_dfs)
  \<in> bg_impl_rel_ext unit_rel R
   \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>Relators.option_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (impl_blue_dfs, blue_dfs) \<in> bg_impl_rel_ext unit_rel R \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel
[PROOF STEP]
using assms impl_blue_dfs.refine
[PROOF STATE]
proof (prove)
using this:
PREFER_id R
(impl_blue_dfs, blue_dfs) \<in> bg_impl_rel_ext ?R_Iec Id \<rightarrow> \<langle>\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (impl_blue_dfs, blue_dfs) \<in> bg_impl_rel_ext unit_rel R \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma impl_blue_dfs_hash_autoref[autoref_rules]:
  fixes R :: "('a \<times> 'a::hashable) set"
  assumes "PREFER_id R"
  shows "(impl_blue_dfs_hash, blue_dfs) \<in> bg_impl_rel_ext unit_rel R
    \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>Relators.option_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (impl_blue_dfs_hash, blue_dfs) \<in> bg_impl_rel_ext unit_rel R \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel
[PROOF STEP]
using assms impl_blue_dfs_hash.refine
[PROOF STATE]
proof (prove)
using this:
PREFER_id R
(impl_blue_dfs_hash, blue_dfs) \<in> bg_impl_rel_ext ?R_Iec Id \<rightarrow> \<langle>\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (impl_blue_dfs_hash, blue_dfs) \<in> bg_impl_rel_ext unit_rel R \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma impl_blue_dfs_ahs_autoref[autoref_rules]:
  fixes R :: "('a \<times> 'a::hashable) set"
  assumes "MINOR_PRIO_TAG 5"
  assumes "PREFER_id R"
  shows "(impl_blue_dfs_ahs, blue_dfs) \<in> bg_impl_rel_ext unit_rel R
    \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>Relators.option_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (impl_blue_dfs_ahs, blue_dfs) \<in> bg_impl_rel_ext unit_rel R \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel
[PROOF STEP]
using assms impl_blue_dfs_ahs.refine
[PROOF STATE]
proof (prove)
using this:
MINOR_PRIO_TAG 5
PREFER_id R
(impl_blue_dfs_ahs, blue_dfs) \<in> bg_impl_rel_ext ?R_Iec Id \<rightarrow> \<langle>\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (impl_blue_dfs_ahs, blue_dfs) \<in> bg_impl_rel_ext unit_rel R \<rightarrow> \<langle>\<langle>\<langle>R\<rangle>list_rel \<times>\<^sub>r \<langle>R\<rangle>list_rel\<rangle>option_rel\<rangle>nres_rel
[PROOF STEP]
by simp


[STATEMENT]
theorem code_blue_dfs_correct:
  assumes G: "b_graph G" "finite ((g_E G)\<^sup>* `` g_V0 G)"
  assumes REL: "(Gi,G)\<in>bg_impl_rel_ext unit_rel Id"
  shows "RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r.
    case r of None \<Rightarrow> \<forall>prpl. \<not>b_graph.is_lasso_prpl G prpl
  | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note code_blue_dfs.refine
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs ?G) \<le> impl_blue_dfs ?G

goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs ?G) \<le> impl_blue_dfs ?G

goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note impl_blue_dfs.refine[param_fo, OF REL, THEN nres_relD]
[PROOF STATE]
proof (state)
this:
impl_blue_dfs Gi \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (blue_dfs G)

goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
impl_blue_dfs Gi \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (blue_dfs G)

goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note blue_dfs_correct[OF G]
[PROOF STATE]
proof (state)
this:
blue_dfs G \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
RETURN (code_blue_dfs Gi) \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
RETURN (code_blue_dfs Gi) \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L))

goal (1 subgoal):
 1. RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
by (simp cong: option.case_cong)
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem code_blue_dfs_correct':
  assumes G: "b_graph G" "finite ((g_E G)\<^sup>* `` g_V0 G)"
  assumes REL: "(Gi,G)\<in>bg_impl_rel_ext unit_rel Id"
  shows "case code_blue_dfs Gi of
      None \<Rightarrow> \<forall>prpl. \<not>b_graph.is_lasso_prpl G prpl
    | Some L \<Rightarrow> b_graph.is_lasso_prpl G L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case code_blue_dfs Gi of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L
[PROOF STEP]
using code_blue_dfs_correct[OF G REL]
[PROOF STATE]
proof (prove)
using this:
RETURN (code_blue_dfs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal (1 subgoal):
 1. case code_blue_dfs Gi of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L
[PROOF STEP]
by simp


[STATEMENT]
theorem code_blue_dfs_hash_correct:
  assumes G: "b_graph G" "finite ((g_E G)\<^sup>* `` g_V0 G)"
  assumes REL: "(Gi,G)\<in>bg_impl_rel_ext unit_rel Id"
  shows "RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r.
    case r of None \<Rightarrow> \<forall>prpl. \<not>b_graph.is_lasso_prpl G prpl
  | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note code_blue_dfs_hash.refine
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs_hash ?G) \<le> impl_blue_dfs_hash ?G

goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs_hash ?G) \<le> impl_blue_dfs_hash ?G

goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note impl_blue_dfs_hash.refine[param_fo, OF REL, THEN nres_relD]
[PROOF STATE]
proof (state)
this:
impl_blue_dfs_hash Gi \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (blue_dfs G)

goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
impl_blue_dfs_hash Gi \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (blue_dfs G)

goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note blue_dfs_correct[OF G]
[PROOF STATE]
proof (state)
this:
blue_dfs G \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
RETURN (code_blue_dfs_hash Gi) \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
RETURN (code_blue_dfs_hash Gi) \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L))

goal (1 subgoal):
 1. RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
by (simp cong: option.case_cong)
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem code_blue_dfs_hash_correct':
  assumes G: "b_graph G" "finite ((g_E G)\<^sup>* `` g_V0 G)"
  assumes REL: "(Gi,G)\<in>bg_impl_rel_ext unit_rel Id"
  shows "case code_blue_dfs_hash Gi of
      None \<Rightarrow> \<forall>prpl. \<not>b_graph.is_lasso_prpl G prpl
    | Some L \<Rightarrow> b_graph.is_lasso_prpl G L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case code_blue_dfs_hash Gi of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L
[PROOF STEP]
using code_blue_dfs_hash_correct[OF G REL]
[PROOF STATE]
proof (prove)
using this:
RETURN (code_blue_dfs_hash Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal (1 subgoal):
 1. case code_blue_dfs_hash Gi of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L
[PROOF STEP]
by simp


[STATEMENT]
theorem code_blue_dfs_ahs_correct:
  assumes G: "b_graph G" "finite ((g_E G)\<^sup>* `` g_V0 G)"
  assumes REL: "(Gi,G)\<in>bg_impl_rel_ext unit_rel Id"
  shows "RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r.
    case r of None \<Rightarrow> \<forall>prpl. \<not>b_graph.is_lasso_prpl G prpl
  | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note code_blue_dfs_ahs.refine
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs_ahs ?G) \<le> impl_blue_dfs_ahs ?G

goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs_ahs ?G) \<le> impl_blue_dfs_ahs ?G

goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note impl_blue_dfs_ahs.refine[param_fo, OF REL, THEN nres_relD]
[PROOF STATE]
proof (state)
this:
impl_blue_dfs_ahs Gi \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (blue_dfs G)

goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
impl_blue_dfs_ahs Gi \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (blue_dfs G)

goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
note blue_dfs_correct[OF G]
[PROOF STATE]
proof (state)
this:
blue_dfs G \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
RETURN (code_blue_dfs_ahs Gi) \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
RETURN (code_blue_dfs_ahs Gi) \<le> \<Down> (\<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<rangle>option_rel) (SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>L. \<not> b_graph.is_lasso_prpl G L | Some L \<Rightarrow> b_graph.is_lasso_prpl G L))

goal (1 subgoal):
 1. RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)
[PROOF STEP]
by (simp cong: option.case_cong)
[PROOF STATE]
proof (state)
this:
RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem code_blue_dfs_ahs_correct':
  assumes G: "b_graph G" "finite ((g_E G)\<^sup>* `` g_V0 G)"
  assumes REL: "(Gi,G)\<in>bg_impl_rel_ext unit_rel Id"
  shows "case code_blue_dfs_ahs Gi of
      None \<Rightarrow> \<forall>prpl. \<not>b_graph.is_lasso_prpl G prpl
    | Some L \<Rightarrow> b_graph.is_lasso_prpl G L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case code_blue_dfs_ahs Gi of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L
[PROOF STEP]
using code_blue_dfs_ahs_correct[OF G REL]
[PROOF STATE]
proof (prove)
using this:
RETURN (code_blue_dfs_ahs Gi) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L)

goal (1 subgoal):
 1. case code_blue_dfs_ahs Gi of None \<Rightarrow> \<forall>prpl. \<not> b_graph.is_lasso_prpl G prpl | Some L \<Rightarrow> b_graph.is_lasso_prpl G L
[PROOF STEP]
by simp


[STATEMENT]
lemma val_stuck: fixes e::exp assumes val_e: "isval e" shows "stuck e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stuck e
[PROOF STEP]
proof (rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> stuck e \<Longrightarrow> stuck e
[PROOF STEP]
assume "\<not> stuck e"
[PROOF STATE]
proof (state)
this:
\<not> stuck e

goal (1 subgoal):
 1. \<not> stuck e \<Longrightarrow> stuck e
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> stuck e
[PROOF STEP]
obtain e' where red: "e \<longrightarrow> e'"
[PROOF STATE]
proof (prove)
using this:
\<not> stuck e

goal (1 subgoal):
 1. (\<And>e'. e \<longrightarrow> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e \<longrightarrow> e'

goal (1 subgoal):
 1. \<not> stuck e \<Longrightarrow> stuck e
[PROOF STEP]
from val_e red
[PROOF STATE]
proof (chain)
picking this:
isval e
e \<longrightarrow> e'
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
isval e
e \<longrightarrow> e'

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

goal (1 subgoal):
 1. \<not> stuck e \<Longrightarrow> stuck e
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. stuck e
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
stuck e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_fv_aux: assumes fvv: "FV v = {}" shows "FV (subst x v e) \<subseteq> FV e - {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FV (subst x v e) \<subseteq> FV e - {x}
[PROOF STEP]
using fvv
[PROOF STATE]
proof (prove)
using this:
FV v = {}

goal (1 subgoal):
 1. FV (subst x v e) \<subseteq> FV e - {x}
[PROOF STEP]
proof (induction e arbitrary: x v rule: exp.induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x xa v. FV v = {} \<Longrightarrow> FV (subst xa v (EVar x)) \<subseteq> FV (EVar x) - {xa}
 2. \<And>x xa v. FV v = {} \<Longrightarrow> FV (subst xa v (ENat x)) \<subseteq> FV (ENat x) - {xa}
 3. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 4. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 5. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 6. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
case (EVar x)
[PROOF STATE]
proof (state)
this:
FV v = {}

goal (6 subgoals):
 1. \<And>x xa v. FV v = {} \<Longrightarrow> FV (subst xa v (EVar x)) \<subseteq> FV (EVar x) - {xa}
 2. \<And>x xa v. FV v = {} \<Longrightarrow> FV (subst xa v (ENat x)) \<subseteq> FV (ENat x) - {xa}
 3. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 4. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 5. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 6. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FV v = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
FV v = {}

goal (1 subgoal):
 1. FV (subst x v (EVar xa__)) \<subseteq> FV (EVar xa__) - {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FV (subst x v (EVar xa__)) \<subseteq> FV (EVar xa__) - {x}

goal (5 subgoals):
 1. \<And>x xa v. FV v = {} \<Longrightarrow> FV (subst xa v (ENat x)) \<subseteq> FV (ENat x) - {xa}
 2. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 3. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 4. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 5. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x xa v. FV v = {} \<Longrightarrow> FV (subst xa v (ENat x)) \<subseteq> FV (ENat x) - {xa}
 2. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 3. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 4. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 5. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
case (ENat x)
[PROOF STATE]
proof (state)
this:
FV v = {}

goal (5 subgoals):
 1. \<And>x xa v. FV v = {} \<Longrightarrow> FV (subst xa v (ENat x)) \<subseteq> FV (ENat x) - {xa}
 2. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 3. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 4. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 5. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FV v = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
FV v = {}

goal (1 subgoal):
 1. FV (subst x v (ENat xa__)) \<subseteq> FV (ENat xa__) - {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FV (subst x v (ENat xa__)) \<subseteq> FV (ENat xa__) - {x}

goal (4 subgoals):
 1. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 2. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 3. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 4. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 2. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 3. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 4. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
case (ELam y e)
[PROOF STATE]
proof (state)
this:
FV ?v = {} \<Longrightarrow> FV (subst ?x ?v e) \<subseteq> FV e - {?x}
FV v = {}

goal (4 subgoals):
 1. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (ELam x1a x2a)) \<subseteq> FV (ELam x1a x2a) - {x}
 2. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 3. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 4. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FV ?v = {} \<Longrightarrow> FV (subst ?x ?v e) \<subseteq> FV e - {?x}
FV v = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
FV ?v = {} \<Longrightarrow> FV (subst ?x ?v e) \<subseteq> FV e - {?x}
FV v = {}

goal (1 subgoal):
 1. FV (subst x v (ELam y e)) \<subseteq> FV (ELam y e) - {x}
[PROOF STEP]
by (cases "x = y") auto
[PROOF STATE]
proof (state)
this:
FV (subst x v (ELam y e)) \<subseteq> FV (ELam y e) - {x}

goal (3 subgoals):
 1. \<And>x1a x2a x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EApp x1a x2a)) \<subseteq> FV (EApp x1a x2a) - {x}
 2. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EPrim x1a x2a x3)) \<subseteq> FV (EPrim x1a x2a x3) - {x}
 3. \<And>x1a x2a x3 x v. \<lbrakk>\<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x1a) \<subseteq> FV x1a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x2a) \<subseteq> FV x2a - {x}; \<And>x v. FV v = {} \<Longrightarrow> FV (subst x v x3) \<subseteq> FV x3 - {x}; FV v = {}\<rbrakk> \<Longrightarrow> FV (subst x v (EIf x1a x2a x3)) \<subseteq> FV (EIf x1a x2a x3) - {x}
[PROOF STEP]
qed (simp,blast)+


[STATEMENT]
lemma subst_fv:  assumes fv_e: "FV e \<subseteq> {x}" and fv_v: "FV v = {}"
  shows "FV (subst x v e) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FV (subst x v e) = {}
[PROOF STEP]
using fv_e fv_v subst_fv_aux
[PROOF STATE]
proof (prove)
using this:
FV e \<subseteq> {x}
FV v = {}
FV ?v = {} \<Longrightarrow> FV (subst ?x ?v ?e) \<subseteq> FV ?e - {?x}

goal (1 subgoal):
 1. FV (subst x v e) = {}
[PROOF STEP]
by blast


[STATEMENT]
lemma red_pres_fv:  fixes e::exp assumes red: "e \<longrightarrow> e'" and fv: "FV e = {}" shows "FV e' = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FV e' = {}
[PROOF STEP]
using red fv
[PROOF STATE]
proof (prove)
using this:
e \<longrightarrow> e'
FV e = {}

goal (1 subgoal):
 1. FV e' = {}
[PROOF STEP]
proof (induction rule: reduce.induct)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>v x e. \<lbrakk>is_val v; FV (EApp (ELam x e) v) = {}\<rbrakk> \<Longrightarrow> FV (subst x v e) = {}
 2. \<And>e1 e1' e2. \<lbrakk>e1 \<longrightarrow> e1'; FV e1 = {} \<Longrightarrow> FV e1' = {}; FV (EApp e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EApp e1' e2) = {}
 3. \<And>e2 e2' e1. \<lbrakk>e2 \<longrightarrow> e2'; FV e2 = {} \<Longrightarrow> FV e2' = {}; FV (EApp e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EApp e1 e2') = {}
 4. \<And>f n1 n2. FV (EPrim f (ENat n1) (ENat n2)) = {} \<Longrightarrow> FV (ENat (f n1 n2)) = {}
 5. \<And>e1 e1' f e2. \<lbrakk>e1 \<longrightarrow> e1'; FV e1 = {} \<Longrightarrow> FV e1' = {}; FV (EPrim f e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EPrim f e1' e2) = {}
 6. \<And>e2 e2' f e1. \<lbrakk>e2 \<longrightarrow> e2'; FV e2 = {} \<Longrightarrow> FV e2' = {}; FV (EPrim f e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EPrim f e1 e2') = {}
 7. \<And>thn els. FV (EIf (ENat 0) thn els) = {} \<Longrightarrow> FV els = {}
 8. \<And>n thn els. \<lbrakk>n \<noteq> 0; FV (EIf (ENat n) thn els) = {}\<rbrakk> \<Longrightarrow> FV thn = {}
 9. \<And>cond cond' thn els. \<lbrakk>cond \<longrightarrow> cond'; FV cond = {} \<Longrightarrow> FV cond' = {}; FV (EIf cond thn els) = {}\<rbrakk> \<Longrightarrow> FV (EIf cond' thn els) = {}
[PROOF STEP]
case (beta v x e)
[PROOF STATE]
proof (state)
this:
is_val v
FV (EApp (ELam x e) v) = {}

goal (9 subgoals):
 1. \<And>v x e. \<lbrakk>is_val v; FV (EApp (ELam x e) v) = {}\<rbrakk> \<Longrightarrow> FV (subst x v e) = {}
 2. \<And>e1 e1' e2. \<lbrakk>e1 \<longrightarrow> e1'; FV e1 = {} \<Longrightarrow> FV e1' = {}; FV (EApp e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EApp e1' e2) = {}
 3. \<And>e2 e2' e1. \<lbrakk>e2 \<longrightarrow> e2'; FV e2 = {} \<Longrightarrow> FV e2' = {}; FV (EApp e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EApp e1 e2') = {}
 4. \<And>f n1 n2. FV (EPrim f (ENat n1) (ENat n2)) = {} \<Longrightarrow> FV (ENat (f n1 n2)) = {}
 5. \<And>e1 e1' f e2. \<lbrakk>e1 \<longrightarrow> e1'; FV e1 = {} \<Longrightarrow> FV e1' = {}; FV (EPrim f e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EPrim f e1' e2) = {}
 6. \<And>e2 e2' f e1. \<lbrakk>e2 \<longrightarrow> e2'; FV e2 = {} \<Longrightarrow> FV e2' = {}; FV (EPrim f e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EPrim f e1 e2') = {}
 7. \<And>thn els. FV (EIf (ENat 0) thn els) = {} \<Longrightarrow> FV els = {}
 8. \<And>n thn els. \<lbrakk>n \<noteq> 0; FV (EIf (ENat n) thn els) = {}\<rbrakk> \<Longrightarrow> FV thn = {}
 9. \<And>cond cond' thn els. \<lbrakk>cond \<longrightarrow> cond'; FV cond = {} \<Longrightarrow> FV cond' = {}; FV (EIf cond thn els) = {}\<rbrakk> \<Longrightarrow> FV (EIf cond' thn els) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_val v
FV (EApp (ELam x e) v) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_val v
FV (EApp (ELam x e) v) = {}

goal (1 subgoal):
 1. FV (subst x v e) = {}
[PROOF STEP]
using subst_fv
[PROOF STATE]
proof (prove)
using this:
is_val v
FV (EApp (ELam x e) v) = {}
\<lbrakk>FV ?e \<subseteq> {?x}; FV ?v = {}\<rbrakk> \<Longrightarrow> FV (subst ?x ?v ?e) = {}

goal (1 subgoal):
 1. FV (subst x v e) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FV (subst x v e) = {}

goal (8 subgoals):
 1. \<And>e1 e1' e2. \<lbrakk>e1 \<longrightarrow> e1'; FV e1 = {} \<Longrightarrow> FV e1' = {}; FV (EApp e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EApp e1' e2) = {}
 2. \<And>e2 e2' e1. \<lbrakk>e2 \<longrightarrow> e2'; FV e2 = {} \<Longrightarrow> FV e2' = {}; FV (EApp e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EApp e1 e2') = {}
 3. \<And>f n1 n2. FV (EPrim f (ENat n1) (ENat n2)) = {} \<Longrightarrow> FV (ENat (f n1 n2)) = {}
 4. \<And>e1 e1' f e2. \<lbrakk>e1 \<longrightarrow> e1'; FV e1 = {} \<Longrightarrow> FV e1' = {}; FV (EPrim f e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EPrim f e1' e2) = {}
 5. \<And>e2 e2' f e1. \<lbrakk>e2 \<longrightarrow> e2'; FV e2 = {} \<Longrightarrow> FV e2' = {}; FV (EPrim f e1 e2) = {}\<rbrakk> \<Longrightarrow> FV (EPrim f e1 e2') = {}
 6. \<And>thn els. FV (EIf (ENat 0) thn els) = {} \<Longrightarrow> FV els = {}
 7. \<And>n thn els. \<lbrakk>n \<noteq> 0; FV (EIf (ENat n) thn els) = {}\<rbrakk> \<Longrightarrow> FV thn = {}
 8. \<And>cond cond' thn els. \<lbrakk>cond \<longrightarrow> cond'; FV cond = {} \<Longrightarrow> FV cond' = {}; FV (EIf cond thn els) = {}\<rbrakk> \<Longrightarrow> FV (EIf cond' thn els) = {}
[PROOF STEP]
qed fastforce+


[STATEMENT]
lemma reduction_pres_fv: fixes e::exp assumes r: "e \<longrightarrow>* e'" and fv: "FV e = {}" shows "FV e' = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FV e' = {}
[PROOF STEP]
using r fv
[PROOF STATE]
proof (prove)
using this:
e \<longrightarrow>* e'
FV e = {}

goal (1 subgoal):
 1. FV e' = {}
[PROOF STEP]
proof (induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>e. FV e = {} \<Longrightarrow> FV e = {}
 2. \<And>e1 e2 e3. \<lbrakk>e1 \<longrightarrow> e2; e2 \<longrightarrow>* e3; FV e2 = {} \<Longrightarrow> FV e3 = {}; FV e1 = {}\<rbrakk> \<Longrightarrow> FV e3 = {}
[PROOF STEP]
case (ms_nil e)
[PROOF STATE]
proof (state)
this:
FV e = {}

goal (2 subgoals):
 1. \<And>e. FV e = {} \<Longrightarrow> FV e = {}
 2. \<And>e1 e2 e3. \<lbrakk>e1 \<longrightarrow> e2; e2 \<longrightarrow>* e3; FV e2 = {} \<Longrightarrow> FV e3 = {}; FV e1 = {}\<rbrakk> \<Longrightarrow> FV e3 = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FV e = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
FV e = {}

goal (1 subgoal):
 1. FV e = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FV e = {}

goal (1 subgoal):
 1. \<And>e1 e2 e3. \<lbrakk>e1 \<longrightarrow> e2; e2 \<longrightarrow>* e3; FV e2 = {} \<Longrightarrow> FV e3 = {}; FV e1 = {}\<rbrakk> \<Longrightarrow> FV e3 = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e1 e2 e3. \<lbrakk>e1 \<longrightarrow> e2; e2 \<longrightarrow>* e3; FV e2 = {} \<Longrightarrow> FV e3 = {}; FV e1 = {}\<rbrakk> \<Longrightarrow> FV e3 = {}
[PROOF STEP]
case (ms_cons e1 e2 e3)
[PROOF STATE]
proof (state)
this:
e1 \<longrightarrow> e2
e2 \<longrightarrow>* e3
FV e2 = {} \<Longrightarrow> FV e3 = {}
FV e1 = {}

goal (1 subgoal):
 1. \<And>e1 e2 e3. \<lbrakk>e1 \<longrightarrow> e2; e2 \<longrightarrow>* e3; FV e2 = {} \<Longrightarrow> FV e3 = {}; FV e1 = {}\<rbrakk> \<Longrightarrow> FV e3 = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e1 \<longrightarrow> e2
e2 \<longrightarrow>* e3
FV e2 = {} \<Longrightarrow> FV e3 = {}
FV e1 = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
e1 \<longrightarrow> e2
e2 \<longrightarrow>* e3
FV e2 = {} \<Longrightarrow> FV e3 = {}
FV e1 = {}

goal (1 subgoal):
 1. FV e3 = {}
[PROOF STEP]
using red_pres_fv
[PROOF STATE]
proof (prove)
using this:
e1 \<longrightarrow> e2
e2 \<longrightarrow>* e3
FV e2 = {} \<Longrightarrow> FV e3 = {}
FV e1 = {}
\<lbrakk>?e \<longrightarrow> ?e'; FV ?e = {}\<rbrakk> \<Longrightarrow> FV ?e' = {}

goal (1 subgoal):
 1. FV e3 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FV e3 = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lossless_vkey_oracle [simp]:
  "lossless_spmf (vkey_oracle \<eta> \<sigma> x) \<longleftrightarrow> (\<sigma> = None \<longrightarrow> lossless_spmf (key_gen \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (vkey_oracle \<eta> \<sigma> x) = (\<sigma> = None \<longrightarrow> lossless_spmf (key_gen \<eta>))
[PROOF STEP]
by(cases "(\<eta>, \<sigma>, x)" rule: vkey_oracle.cases) auto


[STATEMENT]
lemma lossless_sign_oracle [simp]:
  "\<lbrakk> \<sigma> = None \<Longrightarrow> lossless_spmf (key_gen \<eta>);
    \<And>skey m. valid_message \<eta> m \<Longrightarrow> lossless_spmf (sign \<eta> skey m) \<rbrakk>
  \<Longrightarrow> lossless_spmf (sign_oracle \<eta> \<sigma> m) \<longleftrightarrow> valid_message \<eta> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<sigma> = None \<Longrightarrow> lossless_spmf (key_gen \<eta>); \<And>skey m. valid_message \<eta> m \<Longrightarrow> lossless_spmf (sign \<eta> skey m)\<rbrakk> \<Longrightarrow> lossless_spmf (sign_oracle \<eta> \<sigma> m) = valid_message \<eta> m
[PROOF STEP]
apply(cases "(\<eta>, \<sigma>, m)" rule: sign_oracle.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<eta>' ma. \<lbrakk>\<sigma> = None \<Longrightarrow> lossless_spmf (key_gen \<eta>); \<And>skey m. valid_message \<eta> m \<Longrightarrow> lossless_spmf (sign \<eta> skey m); (\<eta>, \<sigma>, m) = (\<eta>', None, ma)\<rbrakk> \<Longrightarrow> lossless_spmf (sign_oracle \<eta> \<sigma> m) = valid_message \<eta> m
 2. \<And>\<eta>' vkey skey ma log. \<lbrakk>\<sigma> = None \<Longrightarrow> lossless_spmf (key_gen \<eta>); \<And>skey m. valid_message \<eta> m \<Longrightarrow> lossless_spmf (sign \<eta> skey m); (\<eta>, \<sigma>, m) = (\<eta>', Some (vkey, skey, log), ma)\<rbrakk> \<Longrightarrow> lossless_spmf (sign_oracle \<eta> \<sigma> m) = valid_message \<eta> m
[PROOF STEP]
apply(auto simp add: split_beta dest: lossless_spmfD_set_spmf_nonempty)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lossless_sign_oracle_Some: fixes log shows
  "lossless_spmf (sign_oracle \<eta> (Some (vkey, skey, log)) m) \<longleftrightarrow> lossless_spmf (sign \<eta> skey m) \<and> valid_message \<eta> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (sign_oracle \<eta> (Some (vkey, skey, log)) m) = (lossless_spmf (sign \<eta> skey m) \<and> valid_message \<eta> m)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma oracle\<^sub>1_simps [simp]:
  "oracle\<^sub>1 \<eta> s (Inl x) = map_spmf (apfst Inl) (vkey_oracle \<eta> s x)"
  "oracle\<^sub>1 \<eta> s (Inr y) = map_spmf (apfst Inr) (sign_oracle \<eta> s y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oracle\<^sub>1 \<eta> s (Inl x) = map_spmf (apfst Inl) (vkey_oracle \<eta> s x) &&& oracle\<^sub>1 \<eta> s (Inr y) = map_spmf (apfst Inr) (sign_oracle \<eta> s y)
[PROOF STEP]
by(simp_all add: oracle\<^sub>1_def)


[STATEMENT]
lemma advantage\<^sub>1_nonneg: "advantage\<^sub>1 \<A> \<eta> \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> advantage\<^sub>1 \<A> \<eta>
[PROOF STEP]
by(simp add: advantage\<^sub>1_def pmf_nonneg)


[STATEMENT]
lemma oracle\<^sub>n_apply [simp]:
  "oracle\<^sub>n \<eta> s (i, x) = map_spmf (apsnd (fun_upd s i)) (oracle\<^sub>1 \<eta> (s i) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oracle\<^sub>n \<eta> s (i, x) = map_spmf (apsnd (fun_upd s i)) (oracle\<^sub>1 \<eta> (s i) x)
[PROOF STEP]
by(simp add: oracle\<^sub>n_def)


[STATEMENT]
lemma advantage\<^sub>n_nonneg: "advantage\<^sub>n \<A> \<eta> \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> advantage\<^sub>n \<A> \<eta>
[PROOF STEP]
by(simp add: advantage\<^sub>n_def pmf_nonneg)


[STATEMENT]
lemma prefers_asym: "P \<turnstile> x < y \<Longrightarrow> \<not> P \<turnstile> y < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> x < y \<Longrightarrow> \<not> P \<turnstile> y < x
[PROOF STEP]
by(simp add: prefers_def)


[STATEMENT]
lemma prefers_trans: "P \<turnstile> x < y \<Longrightarrow> P \<turnstile> y < z \<Longrightarrow> P \<turnstile> x < z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> x < y; P \<turnstile> y < z\<rbrakk> \<Longrightarrow> P \<turnstile> x < z
[PROOF STEP]
by (meson order_less_trans prefers_def)


[STATEMENT]
lemma length_rk_of_pref[simp]: "length(rk_of_pref v vs P) = length vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rk_of_pref v vs P) = length vs
[PROOF STEP]
by(induction P arbitrary: v)(auto)


[STATEMENT]
lemma nth_rk_of_pref: "\<lbrakk> length P \<le> length rs; i \<in> set P; distinct P; set P \<subseteq> {<length rs} \<rbrakk>
 \<Longrightarrow> rk_of_pref r rs P ! i = index P i + r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length P \<le> length rs; i \<in> set P; distinct P; set P \<subseteq> {<length rs}\<rbrakk> \<Longrightarrow> rk_of_pref r rs P ! i = index P i + r
[PROOF STEP]
by(induction P arbitrary: r i) (auto simp add: nth_list_update)


[STATEMENT]
lemma ranking_index: "\<lbrakk> length P = n; set P = {<n} \<rbrakk> \<Longrightarrow> ranking P = map (index P) [0..<length P]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length P = n; set P = {<n}\<rbrakk> \<Longrightarrow> ranking P = map (index P) [0..<length P]
[PROOF STEP]
by(simp add: list_eq_iff_nth_eq ranking_def card_distinct nth_rk_of_pref)


[STATEMENT]
lemma ranking_iff_pref:  "\<lbrakk> set P = {<length P}; i < length P; j < length P \<rbrakk>
 \<Longrightarrow> ranking P ! i < ranking P ! j \<longleftrightarrow> P \<turnstile> i < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set P = {<length P}; i < length P; j < length P\<rbrakk> \<Longrightarrow> (ranking P ! i < ranking P ! j) = (P \<turnstile> i < j)
[PROOF STEP]
by(simp add: ranking_index prefers_def)


[STATEMENT]
lemma wf_less_n: "\<lbrakk> wf A; a < n \<rbrakk> \<Longrightarrow> A!a < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.wf A; a < n\<rbrakk> \<Longrightarrow> A ! a < n
[PROOF STEP]
by (simp add: subset_eq)


[STATEMENT]
lemma sumA_ub: "wf A \<Longrightarrow> (\<Sum>a<n. A!a) \<le> n*(n-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wf A \<Longrightarrow> sum ((!) A) {..<n} \<le> n * (n - 1)
[PROOF STEP]
using sum_bounded_above[of "{..<n}" "((!) A)" "n-1"] wf_le_n1[of A]
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i \<in> {..<n} \<Longrightarrow> A ! i \<le> n - 1) \<Longrightarrow> sum ((!) A) {..<n} \<le> of_nat (card {..<n}) * (n - 1)
\<lbrakk>local.wf A; ?a < n\<rbrakk> \<Longrightarrow> A ! ?a \<le> n - 1

goal (1 subgoal):
 1. local.wf A \<Longrightarrow> sum ((!) A) {..<n} \<le> n * (n - 1)
[PROOF STEP]
by (simp)


[STATEMENT]
lemma var0_match:
assumes "wf A" "M \<subseteq> {<n}" "a < n \<and> a \<notin> M"
shows "var0 A (M \<union> {a}) < var0 A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var0 A (M \<union> {a}) < var0 A M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var0 A (M \<union> {a}) < var0 A M
[PROOF STEP]
have 2: "M \<subset> {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<subset> {<n}
[PROOF STEP]
using assms(2-3)
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> {<n}
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. M \<subset> {<n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<subset> {<n}

goal (1 subgoal):
 1. var0 A (M \<union> {a}) < var0 A M
[PROOF STEP]
have 3: "card M < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card M < n
[PROOF STEP]
using psubset_card_mono[OF _ 2]
[PROOF STATE]
proof (prove)
using this:
finite {<n} \<Longrightarrow> card M < card {<n}

goal (1 subgoal):
 1. card M < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card M < n

goal (1 subgoal):
 1. var0 A (M \<union> {a}) < var0 A M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card M < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card M < n

goal (1 subgoal):
 1. var0 A (M \<union> {a}) < var0 A M
[PROOF STEP]
using sumA_ub[OF assms(1)] assms(3) finite_subset[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
card M < n
sum ((!) A) {..<n} \<le> n * (n - 1)
a < n \<and> a \<notin> M
finite {<n} \<Longrightarrow> finite M

goal (1 subgoal):
 1. var0 A (M \<union> {a}) < var0 A M
[PROOF STEP]
by (simp add: power2_eq_square algebra_simps le_diff_conv2)
[PROOF STATE]
proof (state)
this:
var0 A (M \<union> {a}) < var0 A M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var0_next:
assumes "wf A" "M \<subseteq> {<n}" "M \<noteq> {<n}" "a' < n"
shows "var0 (A[a' := A ! a' + 1]) M < var0 A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
have 0: "card M < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card M < n
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> {<n}
M \<noteq> {<n}

goal (1 subgoal):
 1. card M < n
[PROOF STEP]
by (metis atLeast0LessThan card_lessThan card_subset_eq finite_lessThan lessThan_iff nat_less_le
              subset_eq_atLeast0_lessThan_card)
[PROOF STATE]
proof (state)
this:
card M < n

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
have *: "1 + (\<Sum>a<n. A!a) + card M \<le> n*n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + sum ((!) A) {..<n} + card M \<le> n * n
[PROOF STEP]
using sumA_ub[OF assms(1)] 0
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} \<le> n * (n - 1)
card M < n

goal (1 subgoal):
 1. 1 + sum ((!) A) {..<n} + card M \<le> n * n
[PROOF STEP]
by (simp add: algebra_simps le_diff_conv2)
[PROOF STATE]
proof (state)
this:
1 + sum ((!) A) {..<n} + card M \<le> n * n

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
have "var0 (A[a' := A ! a' + 1]) M = n*n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M = n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
local.wf A
M \<subseteq> {<n}
M \<noteq> {<n}
a' < n

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M = n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M)
[PROOF STEP]
by(simp add: power2_eq_square nth_list_update sum.If_cases lessThan_atLeast0 flip:Diff_eq)
[PROOF STATE]
proof (state)
this:
var0 (A[a' := A ! a' + 1]) M = n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M)

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
var0 (A[a' := A ! a' + 1]) M = n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M)

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
have "\<dots> = n^2 - (1 + (\<Sum>a<n. A!a) + card M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M) = n\<^sup>2 - (1 + sum ((!) A) {..<n} + card M)
[PROOF STEP]
using sum.insert_remove[of "{<n}" "nth A" a',simplified,symmetric] assms(4)
[PROOF STATE]
proof (prove)
using this:
A ! a' + sum ((!) A) ({<n} - {a'}) = sum ((!) A) ({a'} \<union> {<n})
a' < n

goal (1 subgoal):
 1. n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M) = n\<^sup>2 - (1 + sum ((!) A) {..<n} + card M)
[PROOF STEP]
by (simp add:insert_absorb lessThan_atLeast0 power2_eq_square)
[PROOF STATE]
proof (state)
this:
n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M) = n\<^sup>2 - (1 + sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n * n - (1 + (A ! a' + sum ((!) A) ({<n} - {a'})) + card M) = n\<^sup>2 - (1 + sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
have "\<dots> < n^2 - ((\<Sum>a<n. A!a) + card M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n\<^sup>2 - (1 + sum ((!) A) {..<n} + card M) < n\<^sup>2 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n * n - (1 + sum ((!) A) {..<n} + card M) < n * n - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
1 + sum ((!) A) {..<n} + card M \<le> n * n

goal (1 subgoal):
 1. n * n - (1 + sum ((!) A) {..<n} + card M) < n * n - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
n\<^sup>2 - (1 + sum ((!) A) {..<n} + card M) < n\<^sup>2 - (sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
var0 (A[a' := A ! a' + 1]) M < n\<^sup>2 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
var0 (A[a' := A ! a' + 1]) M < n\<^sup>2 - (sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var0 (A[a' := A ! a' + 1]) M < var0 A M
[PROOF STEP]
unfolding var0_def
[PROOF STATE]
proof (prove)
using this:
n\<^sup>2 - (sum ((!) (A[a' := A ! a' + 1])) {..<n} + card M) < n\<^sup>2 - (sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. n\<^sup>2 - (sum ((!) (A[a' := A ! a' + 1])) {..<n} + card M) < n\<^sup>2 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
var0 (A[a' := A ! a' + 1]) M < var0 A M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumA_ub2:
assumes "a' < n" "A!a' \<le> n-1" "\<forall>a < n. a \<noteq> a' \<longrightarrow> A!a \<le> n-2"
shows "(\<Sum>a<n. A!a) \<le> (n-1)*(n-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
have "(\<Sum>a<n. A!a) = (\<Sum>a \<in> ({<n}-{a'}) \<union> {a'}. A!a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} = sum ((!) A) ({<n} - {a'} \<union> {a'})
[PROOF STEP]
by (simp add: assms(1) atLeast0LessThan insert_absorb)
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} = sum ((!) A) ({<n} - {a'} \<union> {a'})

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} = sum ((!) A) ({<n} - {a'} \<union> {a'})

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
have "\<dots> =(\<Sum>a \<in> {<n}-{a'}. A!a) + A!a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) ({<n} - {a'} \<union> {a'}) = sum ((!) A) ({<n} - {a'}) + A ! a'
[PROOF STEP]
by (simp add: sum.insert_remove)
[PROOF STATE]
proof (state)
this:
sum ((!) A) ({<n} - {a'} \<union> {a'}) = sum ((!) A) ({<n} - {a'}) + A ! a'

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((!) A) ({<n} - {a'} \<union> {a'}) = sum ((!) A) ({<n} - {a'}) + A ! a'

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
have "\<dots> \<le> (\<Sum>a \<in> {<n}-{a'}. A!a) + (n-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) ({<n} - {a'}) + A ! a' \<le> sum ((!) A) ({<n} - {a'}) + (n - 1)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
A ! a' \<le> n - 1

goal (1 subgoal):
 1. sum ((!) A) ({<n} - {a'}) + A ! a' \<le> sum ((!) A) ({<n} - {a'}) + (n - 1)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
sum ((!) A) ({<n} - {a'}) + A ! a' \<le> sum ((!) A) ({<n} - {a'}) + (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((!) A) ({<n} - {a'}) + A ! a' \<le> sum ((!) A) ({<n} - {a'}) + (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
have "\<dots> \<le> (n-1)*(n-2) + (n-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) ({<n} - {a'}) + (n - 1) \<le> (n - 1) * (n - 2) + (n - 1)
[PROOF STEP]
using sum_bounded_above[of "{..<n}-{a'}" "((!) A)" "n-2"] assms(1,3)
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i \<in> {..<n} - {a'} \<Longrightarrow> A ! i \<le> n - 2) \<Longrightarrow> sum ((!) A) ({..<n} - {a'}) \<le> of_nat (card ({..<n} - {a'})) * (n - 2)
a' < n
\<forall>a<n. a \<noteq> a' \<longrightarrow> A ! a \<le> n - 2

goal (1 subgoal):
 1. sum ((!) A) ({<n} - {a'}) + (n - 1) \<le> (n - 1) * (n - 2) + (n - 1)
[PROOF STEP]
by (simp add: atLeast0LessThan)
[PROOF STATE]
proof (state)
this:
sum ((!) A) ({<n} - {a'}) + (n - 1) \<le> (n - 1) * (n - 2) + (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((!) A) ({<n} - {a'}) + (n - 1) \<le> (n - 1) * (n - 2) + (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
have "\<dots> = (n-1)*(n-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n - 1) * (n - 2) + (n - 1) = (n - 1) * (n - 1)
[PROOF STEP]
by (metis Suc_diff_Suc Suc_eq_plus1 add.commute diff_is_0_eq' linorder_not_le mult_Suc_right mult_cancel_left nat_1_add_1)
[PROOF STATE]
proof (state)
this:
(n - 1) * (n - 2) + (n - 1) = (n - 1) * (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma match_less_n: "\<lbrakk> wf A; a < n \<rbrakk> \<Longrightarrow> match A a < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.wf A; a < n\<rbrakk> \<Longrightarrow> match A a < n
[PROOF STEP]
by (metis P\<^sub>a_set atLeastLessThan_iff match_def nth_mem subset_eq)


[STATEMENT]
lemma match_upd_neq: "\<lbrakk> wf A; a < n; a \<noteq> a' \<rbrakk> \<Longrightarrow> match (A[a := b]) a' = match A a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.wf A; a < n; a \<noteq> a'\<rbrakk> \<Longrightarrow> match (A[a := b]) a' = match A a'
[PROOF STEP]
by (simp add: match_def)


[STATEMENT]
lemma final_last:
assumes M: "M \<subseteq> {<n}" and inj: "inj_on (match A) M" and pref_match': "preferred A a \<subseteq> match A ` M"
and a: "a < n \<and> a \<notin> M" and final: "A ! a + 1 = n"
shows "insert a M = {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
let ?B = "preferred A a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
have "(!) (P\<^sub>a ! a) ` {<n} = {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!) (P\<^sub>a ! a) ` {<n} = {<n}
[PROOF STEP]
by (metis P\<^sub>a_set a map_nth set_map set_upt)
[PROOF STATE]
proof (state)
this:
(!) (P\<^sub>a ! a) ` {<n} = {<n}

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
hence "inj_on ((!) (P\<^sub>a ! a)) {<n}"
[PROOF STATE]
proof (prove)
using this:
(!) (P\<^sub>a ! a) ` {<n} = {<n}

goal (1 subgoal):
 1. inj_on ((!) (P\<^sub>a ! a)) {<n}
[PROOF STEP]
by(simp add: eq_card_imp_inj_on)
[PROOF STATE]
proof (state)
this:
inj_on ((!) (P\<^sub>a ! a)) {<n}

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
hence "inj_on ((!) (P\<^sub>a ! a)) {<A!a}"
[PROOF STATE]
proof (prove)
using this:
inj_on ((!) (P\<^sub>a ! a)) {<n}

goal (1 subgoal):
 1. inj_on ((!) (P\<^sub>a ! a)) {<A ! a}
[PROOF STEP]
using final
[PROOF STATE]
proof (prove)
using this:
inj_on ((!) (P\<^sub>a ! a)) {<n}
A ! a + 1 = n

goal (1 subgoal):
 1. inj_on ((!) (P\<^sub>a ! a)) {<A ! a}
[PROOF STEP]
by(simp add: subset_inj_on)
[PROOF STATE]
proof (state)
this:
inj_on ((!) (P\<^sub>a ! a)) {<A ! a}

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
hence 1: "Suc(card ?B) = n"
[PROOF STATE]
proof (prove)
using this:
inj_on ((!) (P\<^sub>a ! a)) {<A ! a}

goal (1 subgoal):
 1. Suc (card (preferred A a)) = n
[PROOF STEP]
using final
[PROOF STATE]
proof (prove)
using this:
inj_on ((!) (P\<^sub>a ! a)) {<A ! a}
A ! a + 1 = n

goal (1 subgoal):
 1. Suc (card (preferred A a)) = n
[PROOF STEP]
by (simp add: card_image)
[PROOF STATE]
proof (state)
this:
Suc (card (preferred A a)) = n

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
have 2: "card ?B \<le> card M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (preferred A a) \<le> card M
[PROOF STEP]
by(rule surj_card_le[OF subset_eq_atLeast0_lessThan_finite[OF M] pref_match'])
[PROOF STATE]
proof (state)
this:
card (preferred A a) \<le> card M

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
have 3: "card M < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card M < n
[PROOF STEP]
using M a
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> {<n}
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. card M < n
[PROOF STEP]
by (metis atLeast0LessThan card_seteq order.refl finite_atLeastLessThan le_neq_implies_less lessThan_iff subset_eq_atLeast0_lessThan_card)
[PROOF STATE]
proof (state)
this:
card M < n

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
have "Suc (card M) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card M) = n
[PROOF STEP]
using 1 2 3
[PROOF STATE]
proof (prove)
using this:
Suc (card (preferred A a)) = n
card (preferred A a) \<le> card M
card M < n

goal (1 subgoal):
 1. Suc (card M) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (card M) = n

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc (card M) = n

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
using M a
[PROOF STATE]
proof (prove)
using this:
Suc (card M) = n
M \<subseteq> {<n}
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. {a} \<union> M = {<n}
[PROOF STEP]
by (simp add: card_subset_eq finite_subset)
[PROOF STATE]
proof (state)
this:
{a} \<union> M = {<n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma more_choices:
assumes A: "matching A M" and M: "M \<subseteq> {<n}" "M \<noteq> {<n}"
and pref_match': "preferred A a \<subseteq> match A ` M"
and "a < n" and matched: "match A a \<in> match A ` M"
shows "A ! a + 1 < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ! a + 1 < n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
have match: "match A ` M \<subseteq> {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match A ` M \<subseteq> {<n}
[PROOF STEP]
using A M P\<^sub>a_set
[PROOF STATE]
proof (prove)
using this:
matching A M
M \<subseteq> {<n}
M \<noteq> {<n}
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}

goal (1 subgoal):
 1. match A ` M \<subseteq> {<n}
[PROOF STEP]
unfolding matching_def
[PROOF STATE]
proof (prove)
using this:
local.wf A \<and> inj_on (match A) M
M \<subseteq> {<n}
M \<noteq> {<n}
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}

goal (1 subgoal):
 1. match A ` M \<subseteq> {<n}
[PROOF STEP]
by (smt (verit, best) atLeastLessThan_iff match_def image_subsetI in_mono nth_mem)
[PROOF STATE]
proof (state)
this:
match A ` M \<subseteq> {<n}

goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
have "card M < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card M < n
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> {<n}
M \<noteq> {<n}

goal (1 subgoal):
 1. card M < n
[PROOF STEP]
by (metis card_atLeastLessThan card_seteq diff_zero finite_atLeastLessThan not_less)
[PROOF STATE]
proof (state)
this:
card M < n

goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
assume "\<not> A ! a + 1 < n"
[PROOF STATE]
proof (state)
this:
\<not> A ! a + 1 < n

goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
hence "A ! a + 1 = n"
[PROOF STATE]
proof (prove)
using this:
\<not> A ! a + 1 < n

goal (1 subgoal):
 1. A ! a + 1 = n
[PROOF STEP]
using A \<open>a < n\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> A ! a + 1 < n
matching A M
a < n

goal (1 subgoal):
 1. A ! a + 1 = n
[PROOF STEP]
unfolding matching_def
[PROOF STATE]
proof (prove)
using this:
\<not> A ! a + 1 < n
local.wf A \<and> inj_on (match A) M
a < n

goal (1 subgoal):
 1. A ! a + 1 = n
[PROOF STEP]
by (metis add.commute wf_less_n linorder_neqE_nat not_less_eq plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
A ! a + 1 = n

goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
hence *: "nth (P\<^sub>a ! a) ` {<n} \<subseteq> match A ` M"
[PROOF STATE]
proof (prove)
using this:
A ! a + 1 = n

goal (1 subgoal):
 1. (!) (P\<^sub>a ! a) ` {<n} \<subseteq> match A ` M
[PROOF STEP]
using pref_match' matched less_Suc_eq match_def
[PROOF STATE]
proof (prove)
using this:
A ! a + 1 = n
preferred A a \<subseteq> match A ` M
match A a \<in> match A ` M
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)
match ?A ?a = P\<^sub>a ! ?a ! (?A ! ?a)

goal (1 subgoal):
 1. (!) (P\<^sub>a ! a) ` {<n} \<subseteq> match A ` M
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(!) (P\<^sub>a ! a) ` {<n} \<subseteq> match A ` M

goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
have "nth (P\<^sub>a!a) ` {<n} = {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!) (P\<^sub>a ! a) ` {<n} = {<n}
[PROOF STEP]
by (metis \<open>a < n\<close> map_nth P\<^sub>a_set set_map set_upt)
[PROOF STATE]
proof (state)
this:
(!) (P\<^sub>a ! a) ` {<n} = {<n}

goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
hence "match A ` M = {<n}"
[PROOF STATE]
proof (prove)
using this:
(!) (P\<^sub>a ! a) ` {<n} = {<n}

goal (1 subgoal):
 1. match A ` M = {<n}
[PROOF STEP]
by (metis * match set_eq_subset)
[PROOF STATE]
proof (state)
this:
match A ` M = {<n}

goal (1 subgoal):
 1. \<not> A ! a + 1 < n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
match A ` M = {<n}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
match A ` M = {<n}

goal (1 subgoal):
 1. False
[PROOF STEP]
using A M \<open>card M < n\<close>
[PROOF STATE]
proof (prove)
using this:
match A ` M = {<n}
matching A M
M \<subseteq> {<n}
M \<noteq> {<n}
card M < n

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding matching_def
[PROOF STATE]
proof (prove)
using this:
match A ` M = {<n}
local.wf A \<and> inj_on (match A) M
M \<subseteq> {<n}
M \<noteq> {<n}
card M < n

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis atLeast0LessThan card_image card_lessThan nat_neq_iff)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atmost1_final: assumes M: "M \<subseteq> {<n}" and inj: "inj_on (match A) M"
and "\<forall>a<n. preferred A a \<subseteq> match A ` M"
shows "\<exists>\<^sub>\<le>\<^sub>1 a. a < n \<and> a \<notin> M \<and> A ! a + 1 = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<^sub>\<le>\<^sub>1 a. a < n \<and> a \<notin> M \<and> A ! a + 1 = n
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x < n \<and> x \<notin> M \<and> A ! x + 1 = n; y < n \<and> y \<notin> M \<and> A ! y + 1 = n\<rbrakk> \<Longrightarrow> y = x
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < n \<and> x \<notin> M \<and> A ! x + 1 = n; y < n \<and> y \<notin> M \<and> A ! y + 1 = n\<rbrakk> \<Longrightarrow> y = x
[PROOF STEP]
using final_last[OF M inj, of x] final_last[OF M inj, of y] assms(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>preferred A x \<subseteq> match A ` M; x < n \<and> x \<notin> M; A ! x + 1 = n\<rbrakk> \<Longrightarrow> {x} \<union> M = {<n}
\<lbrakk>preferred A y \<subseteq> match A ` M; y < n \<and> y \<notin> M; A ! y + 1 = n\<rbrakk> \<Longrightarrow> {y} \<union> M = {<n}
\<forall>a<n. preferred A a \<subseteq> match A ` M

goal (1 subgoal):
 1. \<lbrakk>x < n \<and> x \<notin> M \<and> A ! x + 1 = n; y < n \<and> y \<notin> M \<and> A ! y + 1 = n\<rbrakk> \<Longrightarrow> y = x
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sumA_UB:
assumes "matching A M" "M \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> match A ` M"
shows "(\<Sum>a<n. A!a) \<le> (n-1)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
have M: "\<forall>a\<in>M. A!a + 1 < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>M. A ! a + 1 < n
[PROOF STEP]
using more_choices_matched[OF assms(1-3)] assms(4)
    \<open>M \<subseteq> {<n}\<close> atLeastLessThan_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>preferred A ?a \<subseteq> match A ` M; ?a \<in> M\<rbrakk> \<Longrightarrow> A ! ?a + 1 < n
\<forall>a<n. preferred A a \<subseteq> match A ` M
M \<subseteq> {<n}
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)

goal (1 subgoal):
 1. \<forall>a\<in>M. A ! a + 1 < n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>M. A ! a + 1 < n

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
note Ainj = conj12[OF assms(1)[unfolded matching_def]]
[PROOF STATE]
proof (state)
this:
local.wf A
inj_on (match A) M

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
proof (cases "\<exists>a'<n. a' \<notin> M \<and> A!a' + 1 = n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
 2. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n

goal (2 subgoals):
 1. \<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
 2. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n
[PROOF STEP]
obtain a' where a': "a'<n" "a' \<notin> M" "A!a' + 1 = n"
[PROOF STATE]
proof (prove)
using this:
\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>a' < n; a' \<notin> M; A ! a' + 1 = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>M \<subseteq> {<n}\<close> \<open>M \<noteq> {<n}\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n
M \<subseteq> {<n}
M \<noteq> {<n}

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>a' < n; a' \<notin> M; A ! a' + 1 = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a' < n
a' \<notin> M
A ! a' + 1 = n

goal (2 subgoals):
 1. \<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
 2. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
hence "\<forall>a<n. a \<noteq> a' \<longrightarrow> A!a \<le> n-2"
[PROOF STATE]
proof (prove)
using this:
a' < n
a' \<notin> M
A ! a' + 1 = n

goal (1 subgoal):
 1. \<forall>a<n. a \<noteq> a' \<longrightarrow> A ! a \<le> n - 2
[PROOF STEP]
using Uniq_D[OF atmost1_final[OF assms(2) Ainj(2) assms(4)], of a'] M wf_le_n1[OF Ainj(1)]
[PROOF STATE]
proof (prove)
using this:
a' < n
a' \<notin> M
A ! a' + 1 = n
\<lbrakk>a' < n \<and> a' \<notin> M \<and> A ! a' + 1 = n; ?b < n \<and> ?b \<notin> M \<and> A ! ?b + 1 = n\<rbrakk> \<Longrightarrow> a' = ?b
\<forall>a\<in>M. A ! a + 1 < n
?a < n \<Longrightarrow> A ! ?a \<le> n - 1

goal (1 subgoal):
 1. \<forall>a<n. a \<noteq> a' \<longrightarrow> A ! a \<le> n - 2
[PROOF STEP]
by (metis Suc_1 Suc_eq_plus1 add_diff_cancel_right' add_le_imp_le_diff diff_diff_left less_eq_Suc_le order_less_le)
[PROOF STATE]
proof (state)
this:
\<forall>a<n. a \<noteq> a' \<longrightarrow> A ! a \<le> n - 2

goal (2 subgoals):
 1. \<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
 2. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
from sumA_ub2[OF a'(1) _ this] a'(3)
[PROOF STATE]
proof (chain)
picking this:
A ! a' \<le> n - 1 \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
A ! a' + 1 = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A ! a' \<le> n - 1 \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
A ! a' + 1 = n

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
A ! a' \<le> n - 1 \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
A ! a' + 1 = n

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2

goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n)

goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
hence "\<forall>a'<n. a' \<notin> M \<longrightarrow> A ! a' + 1 < n"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n)

goal (1 subgoal):
 1. \<forall>a'<n. a' \<notin> M \<longrightarrow> A ! a' + 1 < n
[PROOF STEP]
by (metis Suc_eq_plus1 Suc_lessI wf_less_n[OF Ainj(1)])
[PROOF STATE]
proof (state)
this:
\<forall>a'<n. a' \<notin> M \<longrightarrow> A ! a' + 1 < n

goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
with M
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>M. A ! a + 1 < n
\<forall>a'<n. a' \<notin> M \<longrightarrow> A ! a' + 1 < n
[PROOF STEP]
have "\<forall>a<n. A ! a + 1 < n"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>M. A ! a + 1 < n
\<forall>a'<n. a' \<notin> M \<longrightarrow> A ! a' + 1 < n

goal (1 subgoal):
 1. \<forall>a<n. A ! a + 1 < n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>a<n. A ! a + 1 < n

goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
hence "(\<Sum>a<n. A!a) \<le> n*(n-2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>a<n. A ! a + 1 < n

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> n * (n - 2)
[PROOF STEP]
using sum_bounded_above[of "{..<n}" "((!) A)" "n-2"]
[PROOF STATE]
proof (prove)
using this:
\<forall>a<n. A ! a + 1 < n
(\<And>i. i \<in> {..<n} \<Longrightarrow> A ! i \<le> n - 2) \<Longrightarrow> sum ((!) A) {..<n} \<le> of_nat (card {..<n}) * (n - 2)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> n * (n - 2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> n * (n - 2)

goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> n * (n - 2)

goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
have "\<dots> \<le> (n-1)*(n-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n * (n - 2) \<le> (n - 1) * (n - 1)
[PROOF STEP]
by(simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
n * (n - 2) \<le> (n - 1) * (n - 1)

goal (1 subgoal):
 1. \<not> (\<exists>a'<n. a' \<notin> M \<and> A ! a' + 1 = n) \<Longrightarrow> sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> (n - 1) * (n - 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_ub:
assumes "matching A M" "M \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> match A ` M"
shows "(\<Sum>a<n. A!a) + card M  < n^2 - n + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
have 1: "M \<subset> {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<subset> {<n}
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> {<n}
M \<noteq> {<n}

goal (1 subgoal):
 1. M \<subset> {<n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<subset> {<n}

goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
have 2: "card M < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card M < n
[PROOF STEP]
using psubset_card_mono[OF _ 1]
[PROOF STATE]
proof (prove)
using this:
finite {<n} \<Longrightarrow> card M < card {<n}

goal (1 subgoal):
 1. card M < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card M < n

goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
have 3: "sum ((!) A) {..<n} \<le> n^2 + 1 - 2*n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n
[PROOF STEP]
using sumA_UB[OF assms(1-4)]
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n
[PROOF STEP]
by (simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n

goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
have 4: "2*n \<le> Suc (n^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * n \<le> Suc (n\<^sup>2)
[PROOF STEP]
using le_square[of n]
[PROOF STATE]
proof (prove)
using this:
n \<le> n * n

goal (1 subgoal):
 1. 2 * n \<le> Suc (n\<^sup>2)
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
n \<le> n * n

goal (1 subgoal):
 1. 2 * n \<le> Suc (n * n)
[PROOF STEP]
by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_SucI mult_2 mult_le_mono1 not_less_eq_eq plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
2 * n \<le> Suc (n\<^sup>2)

goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
show "(\<Sum>a<n. A!a) + card M  < n^2 - n + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
using 2 3 4
[PROOF STATE]
proof (prove)
using this:
card M < n
sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n
2 * n \<le> Suc (n\<^sup>2)

goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_match:
assumes "matching A M" "M \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> match A ` M" "a \<notin> M"
shows "var A (M \<union> {a}) < var A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
have 2: "M \<subset> {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<subset> {<n}
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> {<n}
M \<noteq> {<n}

goal (1 subgoal):
 1. M \<subset> {<n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<subset> {<n}

goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
have 3: "card M < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card M < n
[PROOF STEP]
using psubset_card_mono[OF _ 2]
[PROOF STATE]
proof (prove)
using this:
finite {<n} \<Longrightarrow> card M < card {<n}

goal (1 subgoal):
 1. card M < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card M < n

goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
have 4: "sum ((!) A) {..<n} \<le> n^2 + 1 - 2*n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n
[PROOF STEP]
using sumA_UB[OF assms(1-4)]
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} \<le> (n - 1)\<^sup>2

goal (1 subgoal):
 1. sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n
[PROOF STEP]
by (simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n

goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
have 5: "2*n \<le> Suc (n^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * n \<le> Suc (n\<^sup>2)
[PROOF STEP]
using le_square[of n]
[PROOF STATE]
proof (prove)
using this:
n \<le> n * n

goal (1 subgoal):
 1. 2 * n \<le> Suc (n\<^sup>2)
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
n \<le> n * n

goal (1 subgoal):
 1. 2 * n \<le> Suc (n * n)
[PROOF STEP]
by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_SucI mult_2 mult_le_mono1 not_less_eq_eq plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
2 * n \<le> Suc (n\<^sup>2)

goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
have 6: "(\<Sum>a<n. A!a) + card M  < n^2 + 1 - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 + 1 - n
[PROOF STEP]
using 3 4 5
[PROOF STATE]
proof (prove)
using this:
card M < n
sum ((!) A) {..<n} \<le> n\<^sup>2 + 1 - 2 * n
2 * n \<le> Suc (n\<^sup>2)

goal (1 subgoal):
 1. sum ((!) A) {..<n} + card M < n\<^sup>2 + 1 - n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
sum ((!) A) {..<n} + card M < n\<^sup>2 + 1 - n

goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
from var_ub[OF assms(1-4)]
[PROOF STATE]
proof (chain)
picking this:
sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1

goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
using \<open>a \<notin> M\<close> finite_subset[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1
a \<notin> M
finite {<n} \<Longrightarrow> finite M

goal (1 subgoal):
 1. var A (M \<union> {a}) < var A M
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
var A (M \<union> {a}) < var A M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_next:
assumes"matching A M" "M \<subseteq> {<n}" "M \<noteq> {<n}" "\<forall>a<n. preferred A a \<subseteq> match A ` M"
 "a < n"
shows "var (A[a := A ! a + 1]) M < var A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
have "var (A[a := A ! a + 1]) M = n*n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M = n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M)
[PROOF STEP]
using assms(1,5)
[PROOF STATE]
proof (prove)
using this:
matching A M
a < n

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M = n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M)
[PROOF STEP]
by(simp add: power2_eq_square nth_list_update sum.If_cases lessThan_atLeast0 flip:Diff_eq)
[PROOF STATE]
proof (state)
this:
var (A[a := A ! a + 1]) M = n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M)

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
var (A[a := A ! a + 1]) M = n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M)

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
have "\<dots> = n^2 - n + 1 - (1 + (\<Sum>a<n. A!a) + card M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M) = n\<^sup>2 - n + 1 - (1 + sum ((!) A) {..<n} + card M)
[PROOF STEP]
using sum.insert_remove[of "{<n}" "nth A" a,simplified,symmetric] assms(5)
[PROOF STATE]
proof (prove)
using this:
A ! a + sum ((!) A) ({<n} - {a}) = sum ((!) A) ({a} \<union> {<n})
a < n

goal (1 subgoal):
 1. n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M) = n\<^sup>2 - n + 1 - (1 + sum ((!) A) {..<n} + card M)
[PROOF STEP]
by (simp add:insert_absorb lessThan_atLeast0 power2_eq_square)
[PROOF STATE]
proof (state)
this:
n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M) = n\<^sup>2 - n + 1 - (1 + sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n * n - n + 1 - (1 + (A ! a + sum ((!) A) ({<n} - {a})) + card M) = n\<^sup>2 - n + 1 - (1 + sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
have "\<dots> < n^2 - n + 1 - ((\<Sum>a<n. A!a) + card M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n\<^sup>2 - n + 1 - (1 + sum ((!) A) {..<n} + card M) < n\<^sup>2 - n + 1 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
using var_ub[OF assms(1-4)]
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} + card M < n\<^sup>2 - n + 1

goal (1 subgoal):
 1. n\<^sup>2 - n + 1 - (1 + sum ((!) A) {..<n} + card M) < n\<^sup>2 - n + 1 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
sum ((!) A) {..<n} + card M < n * n - n + 1

goal (1 subgoal):
 1. n * n - n + 1 - (1 + sum ((!) A) {..<n} + card M) < n * n - n + 1 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
n\<^sup>2 - n + 1 - (1 + sum ((!) A) {..<n} + card M) < n\<^sup>2 - n + 1 - (sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
var (A[a := A ! a + 1]) M < n\<^sup>2 - n + 1 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
var (A[a := A ! a + 1]) M < n\<^sup>2 - n + 1 - (sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < var A M
[PROOF STEP]
unfolding var_def
[PROOF STATE]
proof (prove)
using this:
n\<^sup>2 - n + 1 - (sum ((!) (A[a := A ! a + 1])) {..<n} + card M) < n\<^sup>2 - n + 1 - (sum ((!) A) {..<n} + card M)

goal (1 subgoal):
 1. n\<^sup>2 - n + 1 - (sum ((!) (A[a := A ! a + 1])) {..<n} + card M) < n\<^sup>2 - n + 1 - (sum ((!) A) {..<n} + card M)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
var (A[a := A ! a + 1]) M < var A M

goal:
No subgoals!
[PROOF STEP]
qed