[STATEMENT]
lemma Main_Entry_valid [simp]:
  "JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M''
  (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter)
[PROOF STEP]
have "valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'')
    ((ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None,
      Enter),
    (\<lambda>s. False)\<^sub>\<surd>,
    (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None,
      Return))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (\<lambda>s. False)\<^sub>\<surd>, ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return)
[PROOF STEP]
by (auto simp: valid_edge_def intro: JVMCFG_reachable.intros)
[PROOF STATE]
proof (state)
this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (\<lambda>s. False)\<^sub>\<surd>, ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return)

goal (1 subgoal):
 1. JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter), (\<lambda>s. False)\<^sub>\<surd>, ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, nodeType.Return)

goal (1 subgoal):
 1. JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter)
[PROOF STEP]
by (fastforce simp: JVMCFG_Interpret.valid_node_def)
[PROOF STATE]
proof (state)
this:
JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma main_0_Enter_reachable [simp]: "(P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter)
[PROOF STEP]
by (rule reachable_step [where n="(ClassMain P, MethodMain P, None, Enter)"])
(fastforce intro: JVMCFG_reachable.intros)+


[STATEMENT]
lemma main_0_Normal_reachable [simp]: "(P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)
[PROOF STEP]
by (rule reachable_step [where n="(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter)"], simp)
(fastforce intro: JVMCFG_reachable.intros)


[STATEMENT]
lemma main_0_Return_reachable [simp]: "(P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Return)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return)
[PROOF STEP]
by (rule reachable_step [where n="(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)"], simp)
(fastforce intro: JVMCFG_reachable.intros)


[STATEMENT]
lemma Exit_reachable [simp]: "(P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, None, Return)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, None, nodeType.Return)
[PROOF STEP]
by (rule reachable_step [where n="(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Return)"], simp)
(fastforce intro: JVMCFG_reachable.intros)


[STATEMENT]
lemma valid_edge_CFG_def: "valid_edge\<^bsub>CFG\<^esub> P = valid_edge (fst\<^bsub>CFG\<^esub> P, fst (snd\<^bsub>CFG\<^esub> P), snd (snd\<^bsub>CFG\<^esub> P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_edge\<^bsub>CFG\<^esub> P = valid_edge (fst\<^bsub>CFG\<^esub> P, fst (snd\<^bsub>CFG\<^esub> P), snd (snd\<^bsub>CFG\<^esub> P))
[PROOF STEP]
by (cases P) (clarsimp simp: Abs_cfg_wf_prog_inverse)


[STATEMENT]
lemma ceq_equality: "ceq = Some eq \<Longrightarrow> equality eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ceq = Some eq \<Longrightarrow> equality eq
[PROOF STEP]
by (drule ceq, rule Equality_Generator.equalityI, simp)


[STATEMENT]
lemma ID_ceq: "ID ceq = Some eq \<Longrightarrow> eq = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ID ceq = Some eq \<Longrightarrow> eq = (=)
[PROOF STEP]
unfolding ID_def id_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ceq = Some eq \<Longrightarrow> eq = (=)
[PROOF STEP]
by(rule ceq)


[STATEMENT]
lemma equality_subst: "c1 = c2 \<Longrightarrow> equality c1 \<Longrightarrow> equality c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c1 = c2; equality c1\<rbrakk> \<Longrightarrow> equality c2
[PROOF STEP]
by blast


[STATEMENT]
lemma [code]: "CEQ(unit) = Some (\<lambda>_ _. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CEQ(unit) = Some (\<lambda>_ _. True)
[PROOF STEP]
unfolding ceq_unit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (=) = Some (\<lambda>_ _. True)
[PROOF STEP]
by (simp, intro ext, auto)


[STATEMENT]
lemma is_ceq_fun [simp]: "\<not> is_ceq TYPE('a \<Rightarrow> 'b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_ceq TYPE('a \<Rightarrow> 'b)
[PROOF STEP]
by(simp add: is_ceq_def ceq_fun_def ID_None)


[STATEMENT]
lemma set_eq_code:
  shows [code]: "set_eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
  and [code_unfold]: "(=) = set_eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_eq A B = (A \<subseteq> B \<and> B \<subseteq> A) &&& (=) = set_eq
[PROOF STEP]
unfolding set_eq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A = B) = (A \<subseteq> B \<and> B \<subseteq> A) &&& (=) = (=)
[PROOF STEP]
by blast+


[STATEMENT]
lemma is_ceq_set [simp, code_post]: "is_ceq TYPE('a set) \<longleftrightarrow> is_ceq TYPE('a :: ceq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ceq TYPE('a set) = is_ceq TYPE('a)
[PROOF STEP]
by(simp add: is_ceq_def ceq_set_def ID_None ID_Some split: option.split)


[STATEMENT]
lemma ID_ceq_set_not_None_iff [simp]: "ID CEQ('a set) \<noteq> None \<longleftrightarrow> ID CEQ('a :: ceq) \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ID CEQ('a set) \<noteq> None) = (ID CEQ('a) \<noteq> None)
[PROOF STEP]
by(simp add: ceq_set_def ID_def split: option.splits)


[STATEMENT]
lemma member_seq_code [code]:
  "member_seq seq.Empty x \<longleftrightarrow> False"
  "member_seq (seq.Insert y P) x \<longleftrightarrow> eq x y \<or> member_pred P x"
  "member_seq (seq.Join Q xq) x \<longleftrightarrow> member_pred Q x \<or> member_seq xq x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.member_seq seq.Empty x = False &&& local.member_seq (seq.Insert y P) x = (eq x y \<or> local.member_pred P x) &&& local.member_seq (seq.Join Q xq) x = (local.member_pred Q x \<or> local.member_seq xq x)
[PROOF STEP]
by(auto simp add: member_seq_def member_pred_def)


[STATEMENT]
lemma member_pred_code [code]:
  "member_pred (Predicate.Seq f) = member_seq (f ())"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.member_pred (Predicate.Seq f) = local.member_seq (f ())
[PROOF STEP]
by(simp add: member_seq_def Seq_def)


[STATEMENT]
lemma leq_seq_code [code]:
  "leq_seq seq.Empty Q \<longleftrightarrow> True"
  "leq_seq (seq.Insert x P) Q \<longleftrightarrow> member_pred Q x \<and> leq_pred P Q"
  "leq_seq (seq.Join P xp) Q \<longleftrightarrow> leq_pred P Q \<and> leq_seq xp Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.leq_seq seq.Empty Q = True &&& local.leq_seq (seq.Insert x P) Q = (local.member_pred Q x \<and> local.leq_pred P Q) &&& local.leq_seq (seq.Join P xp) Q = (local.leq_pred P Q \<and> local.leq_seq xp Q)
[PROOF STEP]
by(auto simp add: leq_seq_def leq_pred_def member_pred_def)


[STATEMENT]
lemma leq_pred_code [code]:
  "leq_pred (Predicate.Seq f) Q \<longleftrightarrow> leq_seq (f ()) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.leq_pred (Predicate.Seq f) Q = local.leq_seq (f ()) Q
[PROOF STEP]
by(simp add: leq_seq_def Seq_def)


[STATEMENT]
lemma member_pred_eq: "member_pred = Predicate.eval"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.member_pred = pred.eval
[PROOF STEP]
unfolding fun_eq_iff member_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. (\<exists>y. eq xa y \<and> pred.eval x y) = pred.eval x xa
[PROOF STEP]
by(simp add: eq)


[STATEMENT]
lemma member_seq_eq: "member_seq = Predicate.member"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.member_seq = Predicate.member
[PROOF STEP]
by(simp add: member_seq_def fun_eq_iff eval_member member_pred_eq)


[STATEMENT]
lemma leq_pred_eq: "leq_pred = (\<le>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.leq_pred = (\<le>)
[PROOF STEP]
unfolding fun_eq_iff leq_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. (\<forall>xb. pred.eval x xb \<longrightarrow> (\<exists>y. eq xb y \<and> pred.eval xa y)) = (x \<le> xa)
[PROOF STEP]
by(auto simp add: eq less_eq_pred_def)


[STATEMENT]
lemma predicate_eq_eq: "predicate_eq = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.predicate_eq = (=)
[PROOF STEP]
unfolding predicate_eq_def fun_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. (local.leq_pred x xa \<and> local.leq_pred xa x) = (x = xa)
[PROOF STEP]
by(auto simp add: leq_pred_eq)


[STATEMENT]
lemma finite_set_fold_singleton[simp]: "Finite_Set.fold f z {x} = f x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
have "fold_graph f z {x} (f x z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_graph f z {x} (f x z)
[PROOF STEP]
by (auto intro: fold_graph.intros)
[PROOF STATE]
proof (state)
this:
fold_graph f z {x} (f x z)

goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fold_graph f z {x} (f x z)

goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
fold_graph f z {x} (f x z)

goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
fix X y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
have "fold_graph f z X y \<Longrightarrow> (X = {} \<longrightarrow> y = z) \<and> (X = {x} \<longrightarrow> y = f x z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_graph f z X y \<Longrightarrow> (X = {} \<longrightarrow> y = z) \<and> (X = {x} \<longrightarrow> y = f x z)
[PROOF STEP]
by (induct rule: fold_graph.induct) auto
[PROOF STATE]
proof (state)
this:
fold_graph f z X y \<Longrightarrow> (X = {} \<longrightarrow> y = z) \<and> (X = {x} \<longrightarrow> y = f x z)

goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold_graph f z ?X2 ?y2 \<Longrightarrow> (?X2 = {} \<longrightarrow> ?y2 = z) \<and> (?X2 = {x} \<longrightarrow> ?y2 = f x z)

goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fold_graph f z {x} (f x z)
fold_graph f z ?X2 ?y2 \<Longrightarrow> (?X2 = {} \<longrightarrow> ?y2 = z) \<and> (?X2 = {x} \<longrightarrow> ?y2 = f x z)
[PROOF STEP]
have "(THE y. fold_graph f z {x} y) = f x z"
[PROOF STATE]
proof (prove)
using this:
fold_graph f z {x} (f x z)
fold_graph f z ?X2 ?y2 \<Longrightarrow> (?X2 = {} \<longrightarrow> ?y2 = z) \<and> (?X2 = {x} \<longrightarrow> ?y2 = f x z)

goal (1 subgoal):
 1. (THE y. fold_graph f z {x} y) = f x z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(THE y. fold_graph f z {x} y) = f x z

goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(THE y. fold_graph f z {x} y) = f x z

goal (1 subgoal):
 1. Finite_Set.fold f z {x} = f x z
[PROOF STEP]
by (simp add: Finite_Set.fold_def)
[PROOF STATE]
proof (state)
this:
Finite_Set.fold f z {x} = f x z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma funpow_lesseq_iter:
  fixes f :: "('a::order) \<Rightarrow> 'a"
  assumes mono: "\<And>k. k \<le> f k" and m_le_n: "m \<le> n"
  shows "(f ^^ m) k \<le> (f ^^ n) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ m) k \<le> (f ^^ n) k
[PROOF STEP]
using m_le_n
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. (f ^^ m) k \<le> (f ^^ n) k
[PROOF STEP]
by (induct n) (fastforce simp: le_Suc_eq intro: mono order_trans)+


[STATEMENT]
lemma funpow_less_iter:
  fixes f :: "('a::order) \<Rightarrow> 'a"
  assumes mono: "\<And>k. k < f k" and m_lt_n: "m < n"
  shows "(f ^^ m) k < (f ^^ n) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ^^ m) k < (f ^^ n) k
[PROOF STEP]
using m_lt_n
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. (f ^^ m) k < (f ^^ n) k
[PROOF STEP]
by (induct n) (auto, blast intro: mono less_trans dest: less_antisym)


[STATEMENT]
lemma Least_eq[simp]: "(LEAST y. y = x) = x" and "(LEAST y. x = y) = x" for x :: "'a::order"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST y. y = x) = x &&& (LEAST y. x = y) = x
[PROOF STEP]
by (blast intro: Least_equality)+


[STATEMENT]
lemma Least_in_nonempty_set_imp_ex:
  fixes f :: "'b \<Rightarrow> ('a::wellorder)"
  assumes
    A_nemp: "A \<noteq> {}" and
    P_least: "P (LEAST y. \<exists>x \<in> A. y = f x)"
  shows "\<exists>x \<in> A. P (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>A. P (f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>A. P (f x)
[PROOF STEP]
obtain a where a: "a \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A_nemp
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. (\<And>a. a \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. \<exists>x\<in>A. P (f x)
[PROOF STEP]
have "\<exists>x. x \<in> A \<and> (LEAST y. \<exists>x. x \<in> A \<and> y = f x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> A \<and> (LEAST y. \<exists>x. x \<in> A \<and> y = f x) = f x
[PROOF STEP]
by (rule LeastI[of _ "f a"]) (fast intro: a)
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> A \<and> (LEAST y. \<exists>x. x \<in> A \<and> y = f x) = f x

goal (1 subgoal):
 1. \<exists>x\<in>A. P (f x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> A \<and> (LEAST y. \<exists>x. x \<in> A \<and> y = f x) = f x

goal (1 subgoal):
 1. \<exists>x\<in>A. P (f x)
[PROOF STEP]
by (metis P_least)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>A. P (f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Least_eq_0_enat: "P 0 \<Longrightarrow> (LEAST x :: enat. P x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0 \<Longrightarrow> (LEAST x. P x) = 0
[PROOF STEP]
by (simp add: Least_equality)


[STATEMENT]
lemma irrefl_trans_imp_antisym: "irrefl r \<Longrightarrow> trans r \<Longrightarrow> antisym r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irrefl r; trans r\<rbrakk> \<Longrightarrow> antisym r
[PROOF STEP]
unfolding irrefl_def trans_def antisym_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. (a, a) \<notin> r; \<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r\<rbrakk> \<Longrightarrow> \<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y
[PROOF STEP]
by fast


[STATEMENT]
lemma irreflp_transp_imp_antisymP: "irreflp p \<Longrightarrow> transp p \<Longrightarrow> antisymp p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irreflp p; transp p\<rbrakk> \<Longrightarrow> antisymp p
[PROOF STEP]
by (fact irrefl_trans_imp_antisym [to_pred])


[STATEMENT]
lemma finite_nonempty_ex_succ_imp_cyclic:
  assumes
    fin: "finite A" and
    nemp: "A \<noteq> {}" and
    ex_y: "\<forall>x \<in> A. \<exists>y \<in> A. (y, x) \<in> r"
  shows "\<not> acyclic r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
let ?R = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
have R_sub_r: "?R \<subseteq> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r} \<subseteq> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r} \<subseteq> r

goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
have "?R \<subseteq> A \<times> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r} \<subseteq> A \<times> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r} \<subseteq> A \<times> A

goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
hence fin_R: "finite ?R"
[PROOF STATE]
proof (prove)
using this:
{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r} \<subseteq> A \<times> A

goal (1 subgoal):
 1. finite {(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}
[PROOF STEP]
by (auto intro: fin dest!: infinite_super)
[PROOF STATE]
proof (state)
this:
finite {(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}

goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
have "\<not> acyclic ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> acyclicP (\<lambda>x y. x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r)
[PROOF STEP]
by (rule notI, drule finite_acyclic_wf[OF fin_R], unfold wf_eq_minimal, drule spec[of _ A],
      use ex_y nemp in blast)
[PROOF STATE]
proof (state)
this:
\<not> acyclicP (\<lambda>x y. x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r)

goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> acyclicP (\<lambda>x y. x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r)

goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
using R_sub_r acyclic_subset
[PROOF STATE]
proof (prove)
using this:
\<not> acyclicP (\<lambda>x y. x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r)
{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r} \<subseteq> r
\<lbrakk>acyclic ?s; ?r \<subseteq> ?s\<rbrakk> \<Longrightarrow> acyclic ?r

goal (1 subgoal):
 1. \<not> acyclic r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> acyclic r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relcomp_subset_left_imp_relcomp_trancl_subset_left:
  assumes sub: "R O S \<subseteq> R"
  shows "R O S\<^sup>* \<subseteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R O S\<^sup>* \<subseteq> R
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> R O S\<^sup>* \<Longrightarrow> x \<in> R
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> R O S\<^sup>* \<Longrightarrow> x \<in> R
[PROOF STEP]
assume "x \<in> R O S\<^sup>*"
[PROOF STATE]
proof (state)
this:
x \<in> R O S\<^sup>*

goal (1 subgoal):
 1. \<And>x. x \<in> R O S\<^sup>* \<Longrightarrow> x \<in> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> R O S\<^sup>*
[PROOF STEP]
obtain n where "x \<in> R O S ^^ n"
[PROOF STATE]
proof (prove)
using this:
x \<in> R O S\<^sup>*

goal (1 subgoal):
 1. (\<And>n. x \<in> R O S ^^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rtrancl_imp_relpow
[PROOF STATE]
proof (prove)
using this:
x \<in> R O S\<^sup>*
?p \<in> ?R\<^sup>* \<Longrightarrow> \<exists>n. ?p \<in> ?R ^^ n

goal (1 subgoal):
 1. (\<And>n. x \<in> R O S ^^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> R O S ^^ n

goal (1 subgoal):
 1. \<And>x. x \<in> R O S\<^sup>* \<Longrightarrow> x \<in> R
[PROOF STEP]
thus "x \<in> R"
[PROOF STATE]
proof (prove)
using this:
x \<in> R O S ^^ n

goal (1 subgoal):
 1. x \<in> R
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> R O S ^^ 0 \<Longrightarrow> x \<in> R
 2. \<And>n. \<lbrakk>x \<in> R O S ^^ n \<Longrightarrow> x \<in> R; x \<in> R O S ^^ Suc n\<rbrakk> \<Longrightarrow> x \<in> R
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
x \<in> R O S ^^ m \<Longrightarrow> x \<in> R
x \<in> R O S ^^ Suc m

goal (2 subgoals):
 1. x \<in> R O S ^^ 0 \<Longrightarrow> x \<in> R
 2. \<And>n. \<lbrakk>x \<in> R O S ^^ n \<Longrightarrow> x \<in> R; x \<in> R O S ^^ Suc n\<rbrakk> \<Longrightarrow> x \<in> R
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> R O S ^^ m \<Longrightarrow> x \<in> R
x \<in> R O S ^^ Suc m

goal (1 subgoal):
 1. x \<in> R
[PROOF STEP]
by (metis (no_types) O_assoc inf_sup_ord(3) le_iff_sup relcomp_distrib2 relpow.simps(2)
        relpow_commute sub subsetCE)
[PROOF STATE]
proof (state)
this:
x \<in> R

goal (1 subgoal):
 1. x \<in> R O S ^^ 0 \<Longrightarrow> x \<in> R
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
x \<in> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_chain_in_rtrancl:
  assumes m_le_n: "m \<le> n" and f_chain: "\<forall>i \<in> {m..<n}. (f i, f (Suc i)) \<in> R"
  shows "(f m, f n) \<in> R\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f m, f n) \<in> R\<^sup>*
[PROOF STEP]
proof (rule relpow_imp_rtrancl, rule relpow_fun_conv[THEN iffD2], intro exI conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?f5 0 = f m
 2. ?f5 ?n = f n
 3. \<forall>i<?n. (?f5 i, ?f5 (Suc i)) \<in> R
[PROOF STEP]
let ?g = "\<lambda>i. f (m + i)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?f5 0 = f m
 2. ?f5 ?n = f n
 3. \<forall>i<?n. (?f5 i, ?f5 (Suc i)) \<in> R
[PROOF STEP]
let ?k = "n - m"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?f5 0 = f m
 2. ?f5 ?n = f n
 3. \<forall>i<?n. (?f5 i, ?f5 (Suc i)) \<in> R
[PROOF STEP]
show "?g 0 = f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (m + 0) = f m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (m + 0) = f m

goal (2 subgoals):
 1. f (m + ?n) = f n
 2. \<forall>i<?n. (f (m + i), f (m + Suc i)) \<in> R
[PROOF STEP]
show "?g ?k = f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (m + (n - m)) = f n
[PROOF STEP]
using m_le_n
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. f (m + (n - m)) = f n
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f (m + (n - m)) = f n

goal (1 subgoal):
 1. \<forall>i<n - m. (f (m + i), f (m + Suc i)) \<in> R
[PROOF STEP]
show "(\<forall>i < ?k. (?g i, ?g (Suc i)) \<in> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n - m. (f (m + i), f (m + Suc i)) \<in> R
[PROOF STEP]
by (simp add: f_chain)
[PROOF STATE]
proof (state)
this:
\<forall>i<n - m. (f (m + i), f (m + Suc i)) \<in> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_rev_chain_in_rtrancl:
  assumes m_le_n: "m \<le> n" and f_chain: "\<forall>i \<in> {m..<n}. (f (Suc i), f i) \<in> R"
  shows "(f n, f m) \<in> R\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f n, f m) \<in> R\<^sup>*
[PROOF STEP]
by (rule f_chain_in_rtrancl[OF m_le_n, of "\<lambda>i. f (n + m - i)", simplified])
    (metis f_chain le_add_diff Suc_diff_Suc Suc_leI atLeastLessThan_iff diff_Suc_diff_eq1 diff_less
      le_add1 less_le_trans zero_less_Suc)


[STATEMENT]
lemma wf_app: "wf r \<Longrightarrow> wf {(x, y). (f x, f y) \<in> r}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf r \<Longrightarrow> wf {(x, y). (f x, f y) \<in> r}
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q) \<Longrightarrow> \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> {(x, y). (f x, f y) \<in> r} \<longrightarrow> y \<notin> Q)
[PROOF STEP]
by (intro allI, drule spec[of _ "f ` Q" for Q]) fast


[STATEMENT]
lemma wfP_app: "wfP p \<Longrightarrow> wfP (\<lambda>x y. p (f x) (f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wfP p \<Longrightarrow> wfP (\<lambda>x y. p (f x) (f y))
[PROOF STEP]
unfolding wfP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(x, y). p x y} \<Longrightarrow> wf {(x, y). p (f x) (f y)}
[PROOF STEP]
by (rule wf_app[of "{(x, y). p x y}" f, simplified])


[STATEMENT]
lemma wf_exists_minimal:
  assumes wf: "wf r" and Q: "Q x"
  shows "\<exists>x. Q x \<and> (\<forall>y. (f y, f x) \<in> r \<longrightarrow> \<not> Q y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. Q x \<and> (\<forall>y. (f y, f x) \<in> r \<longrightarrow> \<not> Q y)
[PROOF STEP]
using wf_eq_minimal[THEN iffD1, OF wf_app[OF wf], rule_format, of _ "{x. Q x}", simplified, OF Q]
[PROOF STATE]
proof (prove)
using this:
\<exists>z. Q z \<and> (\<forall>y. (?f y, ?f z) \<in> r \<longrightarrow> \<not> Q y)

goal (1 subgoal):
 1. \<exists>x. Q x \<and> (\<forall>y. (f y, f x) \<in> r \<longrightarrow> \<not> Q y)
[PROOF STEP]
by blast


[STATEMENT]
lemma wfP_exists_minimal:
  assumes wf: "wfP p" and Q: "Q x"
  shows "\<exists>x. Q x \<and> (\<forall>y. p (f y) (f x) \<longrightarrow> \<not> Q y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. Q x \<and> (\<forall>y. p (f y) (f x) \<longrightarrow> \<not> Q y)
[PROOF STEP]
by (rule wf_exists_minimal[of "{(x, y). p x y}" Q x, OF wf[unfolded wfP_def] Q, simplified])


[STATEMENT]
lemma finite_irrefl_trans_imp_wf: "finite r \<Longrightarrow> irrefl r \<Longrightarrow> trans r \<Longrightarrow> wf r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite r; irrefl r; trans r\<rbrakk> \<Longrightarrow> wf r
[PROOF STEP]
by (erule finite_acyclic_wf) (simp add: acyclic_irrefl)


[STATEMENT]
lemma finite_irreflp_transp_imp_wfp:
  "finite {(x, y). p x y} \<Longrightarrow> irreflp p \<Longrightarrow> transp p \<Longrightarrow> wfP p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {(x, y). p x y}; irreflp p; transp p\<rbrakk> \<Longrightarrow> wfP p
[PROOF STEP]
using finite_irrefl_trans_imp_wf[of "{(x, y). p x y}"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {(x, y). p x y}; irrefl {(x, y). p x y}; trans {(x, y). p x y}\<rbrakk> \<Longrightarrow> wf {(x, y). p x y}

goal (1 subgoal):
 1. \<lbrakk>finite {(x, y). p x y}; irreflp p; transp p\<rbrakk> \<Longrightarrow> wfP p
[PROOF STEP]
unfolding wfP_def transp_def irreflp_def trans_def irrefl_def mem_Collect_eq prod.case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {(x, y). p x y}; \<forall>a. \<not> p a a; \<forall>x y z. p x y \<longrightarrow> p y z \<longrightarrow> p x z\<rbrakk> \<Longrightarrow> wf {(x, y). p x y}

goal (1 subgoal):
 1. \<lbrakk>finite {(x, y). p x y}; \<forall>a. \<not> p a a; \<forall>x y z. p x y \<longrightarrow> p y z \<longrightarrow> p x z\<rbrakk> \<Longrightarrow> wf {(x, y). p x y}
[PROOF STEP]
by assumption


[STATEMENT]
lemma wf_infinite_down_chain_compatible:
  assumes
    wf_R: "wf R" and
    inf_chain_RS: "\<forall>i. (f (Suc i), f i) \<in> R \<union> S" and
    O_subset: "R O S \<subseteq> R"
  shows "\<exists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
assume "\<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S"
[PROOF STATE]
proof (state)
this:
\<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>k. \<exists>i. (f (Suc (i + k)), f (i + k)) \<notin> S"
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S

goal (1 subgoal):
 1. \<forall>k. \<exists>i. (f (Suc (i + k)), f (i + k)) \<notin> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>k. \<exists>i. (f (Suc (i + k)), f (i + k)) \<notin> S

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>k. \<exists>i > k. (f (Suc i), f i) \<notin> S"
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<exists>i. (f (Suc (i + k)), f (i + k)) \<notin> S

goal (1 subgoal):
 1. \<forall>k. \<exists>i>k. (f (Suc i), f i) \<notin> S
[PROOF STEP]
by (metis add.commute add_Suc less_add_Suc1)
[PROOF STATE]
proof (state)
this:
\<forall>k. \<exists>i>k. (f (Suc i), f i) \<notin> S

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>k. \<exists>i > k. (f (Suc i), f i) \<in> R"
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<exists>i>k. (f (Suc i), f i) \<notin> S

goal (1 subgoal):
 1. \<forall>k. \<exists>i>k. (f (Suc i), f i) \<in> R
[PROOF STEP]
using inf_chain_RS
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<exists>i>k. (f (Suc i), f i) \<notin> S
\<forall>i. (f (Suc i), f i) \<in> R \<union> S

goal (1 subgoal):
 1. \<forall>k. \<exists>i>k. (f (Suc i), f i) \<in> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>k. \<exists>i>k. (f (Suc i), f i) \<in> R

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
hence "\<exists>i > k. (f (Suc i), f i) \<in> R \<and> (\<forall>j > k. (f (Suc j), f j) \<in> R \<longrightarrow> j \<ge> i)" for k
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<exists>i>k. (f (Suc i), f i) \<in> R

goal (1 subgoal):
 1. \<exists>i>k. (f (Suc i), f i) \<in> R \<and> (\<forall>j>k. (f (Suc j), f j) \<in> R \<longrightarrow> i \<le> j)
[PROOF STEP]
using wf_eq_minimal[THEN iffD1, OF wf_less, rule_format,
      of _ "{i. i > k \<and> (f (Suc i), f i) \<in> R}", simplified]
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<exists>i>k. (f (Suc i), f i) \<in> R
k < ?x \<and> (f (Suc ?x), f ?x) \<in> R \<Longrightarrow> \<exists>z>k. (f (Suc z), f z) \<in> R \<and> (\<forall>y<z. k < y \<longrightarrow> (f (Suc y), f y) \<notin> R)

goal (1 subgoal):
 1. \<exists>i>k. (f (Suc i), f i) \<in> R \<and> (\<forall>j>k. (f (Suc j), f j) \<in> R \<longrightarrow> i \<le> j)
[PROOF STEP]
by (meson not_less)
[PROOF STATE]
proof (state)
this:
\<exists>i>?k. (f (Suc i), f i) \<in> R \<and> (\<forall>j>?k. (f (Suc j), f j) \<in> R \<longrightarrow> i \<le> j)

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i>?k. (f (Suc i), f i) \<in> R \<and> (\<forall>j>?k. (f (Suc j), f j) \<in> R \<longrightarrow> i \<le> j)
[PROOF STEP]
obtain j_of where
    j_of_gt: "\<And>k. j_of k > k" and
    j_of_in_R: "\<And>k. (f (Suc (j_of k)), f (j_of k)) \<in> R" and
    j_of_min: "\<And>k. \<forall>j > k. (f (Suc j), f j) \<in> R \<longrightarrow> j \<ge> j_of k"
[PROOF STATE]
proof (prove)
using this:
\<exists>i>?k. (f (Suc i), f i) \<in> R \<and> (\<forall>j>?k. (f (Suc j), f j) \<in> R \<longrightarrow> i \<le> j)

goal (1 subgoal):
 1. (\<And>j_of. \<lbrakk>\<And>k. k < j_of k; \<And>k. (f (Suc (j_of k)), f (j_of k)) \<in> R; \<And>k. \<forall>j>k. (f (Suc j), f j) \<in> R \<longrightarrow> j_of k \<le> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
?k < j_of ?k
(f (Suc (j_of ?k)), f (j_of ?k)) \<in> R
\<forall>j>?k. (f (Suc j), f j) \<in> R \<longrightarrow> j_of ?k \<le> j

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
have j_of_min_s: "\<And>k j. j > k \<Longrightarrow> j < j_of k \<Longrightarrow> (f (Suc j), f j) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k j. \<lbrakk>k < j; j < j_of k\<rbrakk> \<Longrightarrow> (f (Suc j), f j) \<in> S
[PROOF STEP]
using j_of_min inf_chain_RS
[PROOF STATE]
proof (prove)
using this:
\<forall>j>?k. (f (Suc j), f j) \<in> R \<longrightarrow> j_of ?k \<le> j
\<forall>i. (f (Suc i), f i) \<in> R \<union> S

goal (1 subgoal):
 1. \<And>k j. \<lbrakk>k < j; j < j_of k\<rbrakk> \<Longrightarrow> (f (Suc j), f j) \<in> S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?k < ?j; ?j < j_of ?k\<rbrakk> \<Longrightarrow> (f (Suc ?j), f ?j) \<in> S

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
define g :: "nat \<Rightarrow> 'a" where "\<And>k. g k = f (Suc ((j_of ^^ k) 0))"
[PROOF STATE]
proof (state)
this:
g ?k = f (Suc ((j_of ^^ ?k) 0))

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
have between_g[simplified]: "(f ((j_of ^^ (Suc i)) 0), f (Suc ((j_of ^^ i) 0))) \<in> S\<^sup>*" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f ((j_of ^^ Suc i) 0), f (Suc ((j_of ^^ i) 0))) \<in> S\<^sup>*
[PROOF STEP]
proof (rule f_rev_chain_in_rtrancl; clarify?)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc ((j_of ^^ i) 0) \<le> (j_of ^^ Suc i) 0
 2. \<And>ia. ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0} \<Longrightarrow> (f (Suc ia), f ia) \<in> S
[PROOF STEP]
show "Suc ((j_of ^^ i) 0) \<le> (j_of ^^ Suc i) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ((j_of ^^ i) 0) \<le> (j_of ^^ Suc i) 0
[PROOF STEP]
using j_of_gt
[PROOF STATE]
proof (prove)
using this:
?k < j_of ?k

goal (1 subgoal):
 1. Suc ((j_of ^^ i) 0) \<le> (j_of ^^ Suc i) 0
[PROOF STEP]
by (simp add: Suc_leI)
[PROOF STATE]
proof (state)
this:
Suc ((j_of ^^ i) 0) \<le> (j_of ^^ Suc i) 0

goal (1 subgoal):
 1. \<And>ia. ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0} \<Longrightarrow> (f (Suc ia), f ia) \<in> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0} \<Longrightarrow> (f (Suc ia), f ia) \<in> S
[PROOF STEP]
fix ia
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia. ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0} \<Longrightarrow> (f (Suc ia), f ia) \<in> S
[PROOF STEP]
assume ia: "ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0}"
[PROOF STATE]
proof (state)
this:
ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0}

goal (1 subgoal):
 1. \<And>ia. ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0} \<Longrightarrow> (f (Suc ia), f ia) \<in> S
[PROOF STEP]
have ia_gt: "ia > (j_of ^^ i) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (j_of ^^ i) 0 < ia
[PROOF STEP]
using ia
[PROOF STATE]
proof (prove)
using this:
ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0}

goal (1 subgoal):
 1. (j_of ^^ i) 0 < ia
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(j_of ^^ i) 0 < ia

goal (1 subgoal):
 1. \<And>ia. ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0} \<Longrightarrow> (f (Suc ia), f ia) \<in> S
[PROOF STEP]
have ia_lt: "ia < j_of ((j_of ^^ i) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia < j_of ((j_of ^^ i) 0)
[PROOF STEP]
using ia
[PROOF STATE]
proof (prove)
using this:
ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0}

goal (1 subgoal):
 1. ia < j_of ((j_of ^^ i) 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ia < j_of ((j_of ^^ i) 0)

goal (1 subgoal):
 1. \<And>ia. ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0} \<Longrightarrow> (f (Suc ia), f ia) \<in> S
[PROOF STEP]
show "(f (Suc ia), f ia) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f (Suc ia), f ia) \<in> S
[PROOF STEP]
by (rule j_of_min_s[OF ia_gt ia_lt])
[PROOF STATE]
proof (state)
this:
(f (Suc ia), f ia) \<in> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f (j_of ((j_of ^^ ?i) 0)), f (Suc ((j_of ^^ ?i) 0))) \<in> S\<^sup>*

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
have "\<And>i. (g (Suc i), g i) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (g (Suc i), g i) \<in> R
[PROOF STEP]
unfolding g_def funpow.simps comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (f (Suc (j_of ((j_of ^^ i) 0))), f (Suc ((j_of ^^ i) 0))) \<in> R
[PROOF STEP]
by (rule subsetD[OF relcomp_subset_left_imp_relcomp_trancl_subset_left[OF O_subset]])
      (rule relcompI[OF j_of_in_R between_g])
[PROOF STATE]
proof (state)
this:
(g (Suc ?i), g ?i) \<in> R

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(g (Suc ?i), g ?i) \<in> R

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
have "\<forall>f. \<exists>i. (f (Suc i), f i) \<notin> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. \<exists>i. (f (Suc i), f i) \<notin> R
[PROOF STEP]
using wf_R[unfolded wf_iff_no_infinite_down_chain]
[PROOF STATE]
proof (prove)
using this:
\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> R

goal (1 subgoal):
 1. \<forall>f. \<exists>i. (f (Suc i), f i) \<notin> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>f. \<exists>i. (f (Suc i), f i) \<notin> R

goal (1 subgoal):
 1. \<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(g (Suc ?i), g ?i) \<in> R
\<forall>f. \<exists>i. (f (Suc i), f i) \<notin> R
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(g (Suc ?i), g ?i) \<in> R
\<forall>f. \<exists>i. (f (Suc i), f i) \<notin> R

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in wellorder) exists_minimal:
  fixes x :: 'a
  assumes "P x"
  shows "\<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<ge> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P x

goal (1 subgoal):
 1. \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y)
[PROOF STEP]
by (auto intro: LeastI Least_le)


[STATEMENT]
lemma rev_induct2[consumes 1, case_names Nil snoc]:
  "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
   (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (xs @ [x]) (ys @ [y])) \<Longrightarrow> P xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P xs ys
[PROOF STEP]
proof (induct xs arbitrary: ys rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>length [] = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P [] ys
 2. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>length xs = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P xs ys; length (xs @ [x]) = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P (xs @ [x]) ys
[PROOF STEP]
case (snoc x xs ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length xs = length ?ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P xs ?ys
length (xs @ [x]) = length ys
P [] []
\<lbrakk>length ?xs = length ?ys; P ?xs ?ys\<rbrakk> \<Longrightarrow> P (?xs @ [?x]) (?ys @ [?y])

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>length [] = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P [] ys
 2. \<And>x xs ys. \<lbrakk>\<And>ys. \<lbrakk>length xs = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P xs ys; length (xs @ [x]) = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P (xs @ [x]) ys
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs = length ?ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P xs ?ys
length (xs @ [x]) = length ys
P [] []
\<lbrakk>length ?xs = length ?ys; P ?xs ?ys\<rbrakk> \<Longrightarrow> P (?xs @ [?x]) (?ys @ [?y])

goal (1 subgoal):
 1. P (xs @ [x]) ys
[PROOF STEP]
by (induct ys rule: rev_induct) simp_all
[PROOF STATE]
proof (state)
this:
P (xs @ [x]) ys

goal (1 subgoal):
 1. \<And>ys. \<lbrakk>length [] = length ys; P [] []; \<And>x xs y ys. \<lbrakk>length xs = length ys; P xs ys\<rbrakk> \<Longrightarrow> P (xs @ [x]) (ys @ [y])\<rbrakk> \<Longrightarrow> P [] ys
[PROOF STEP]
qed auto


[STATEMENT]
lemma in_lists_iff_set: "xs \<in> lists A \<longleftrightarrow> set xs \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> lists A) = (set xs \<subseteq> A)
[PROOF STEP]
by fast


[STATEMENT]
lemma butlast_append_Cons[simp]: "butlast (xs @ y # ys) = xs @ butlast (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast (xs @ y # ys) = xs @ butlast (y # ys)
[PROOF STEP]
using butlast_append[of xs "y # ys", simplified]
[PROOF STATE]
proof (prove)
using this:
butlast (xs @ y # ys) = xs @ (if ys = [] then [] else y # butlast ys)

goal (1 subgoal):
 1. butlast (xs @ y # ys) = xs @ butlast (y # ys)
[PROOF STEP]
by simp


[STATEMENT]
lemma rev_in_lists[simp]: "rev xs \<in> lists A \<longleftrightarrow> xs \<in> lists A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rev xs \<in> lists A) = (xs \<in> lists A)
[PROOF STEP]
by auto


[STATEMENT]
lemma hd_le_sum_list:
  fixes xs :: "'a::ordered_ab_semigroup_monoid_add_imp_le list"
  assumes "xs \<noteq> []" and "\<forall>i < length xs. xs ! i \<ge> 0"
  shows "hd xs \<le> sum_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd xs \<le> sum_list xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
\<forall>i<length xs. (0::'a) \<le> xs ! i

goal (1 subgoal):
 1. hd xs \<le> sum_list xs
[PROOF STEP]
by (induct xs rule: rev_induct, simp_all,
    metis add_cancel_right_left add_increasing2 hd_append2 lessI less_SucI list.sel(1) nth_append
      nth_append_length order_refl self_append_conv2 sum_list.Nil)


[STATEMENT]
lemma sum_list_ge_length_times:
  fixes a :: "'a::{ordered_ab_semigroup_add,semiring_1}"
  assumes "\<forall>i < length xs. xs ! i \<ge> a"
  shows "sum_list xs \<ge> of_nat (length xs) * a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (length xs) * a \<le> sum_list xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length xs. a \<le> xs ! i

goal (1 subgoal):
 1. of_nat (length xs) * a \<le> sum_list xs
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>i<length []. a \<le> [] ! i \<Longrightarrow> of_nat (length []) * a \<le> sum_list []
 2. \<And>aa xs. \<lbrakk>\<forall>i<length xs. a \<le> xs ! i \<Longrightarrow> of_nat (length xs) * a \<le> sum_list xs; \<forall>i<length (aa # xs). a \<le> (aa # xs) ! i\<rbrakk> \<Longrightarrow> of_nat (length (aa # xs)) * a \<le> sum_list (aa # xs)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. a \<le> xs ! i \<Longrightarrow> of_nat (length xs) * a \<le> sum_list xs
\<forall>i<length (x # xs). a \<le> (x # xs) ! i

goal (2 subgoals):
 1. \<forall>i<length []. a \<le> [] ! i \<Longrightarrow> of_nat (length []) * a \<le> sum_list []
 2. \<And>aa xs. \<lbrakk>\<forall>i<length xs. a \<le> xs ! i \<Longrightarrow> of_nat (length xs) * a \<le> sum_list xs; \<forall>i<length (aa # xs). a \<le> (aa # xs) ! i\<rbrakk> \<Longrightarrow> of_nat (length (aa # xs)) * a \<le> sum_list (aa # xs)
[PROOF STEP]
note ih = this(1) and xxs_i_ge_a = this(2)
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. a \<le> xs ! i \<Longrightarrow> of_nat (length xs) * a \<le> sum_list xs
\<forall>i<length (x # xs). a \<le> (x # xs) ! i

goal (2 subgoals):
 1. \<forall>i<length []. a \<le> [] ! i \<Longrightarrow> of_nat (length []) * a \<le> sum_list []
 2. \<And>aa xs. \<lbrakk>\<forall>i<length xs. a \<le> xs ! i \<Longrightarrow> of_nat (length xs) * a \<le> sum_list xs; \<forall>i<length (aa # xs). a \<le> (aa # xs) ! i\<rbrakk> \<Longrightarrow> of_nat (length (aa # xs)) * a \<le> sum_list (aa # xs)
[PROOF STEP]
have xs_i_ge_a: "\<forall>i < length xs. xs ! i \<ge> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length xs. a \<le> xs ! i
[PROOF STEP]
using xxs_i_ge_a
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length (x # xs). a \<le> (x # xs) ! i

goal (1 subgoal):
 1. \<forall>i<length xs. a \<le> xs ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length xs. a \<le> xs ! i

goal (2 subgoals):
 1. \<forall>i<length []. a \<le> [] ! i \<Longrightarrow> of_nat (length []) * a \<le> sum_list []
 2. \<And>aa xs. \<lbrakk>\<forall>i<length xs. a \<le> xs ! i \<Longrightarrow> of_nat (length xs) * a \<le> sum_list xs; \<forall>i<length (aa # xs). a \<le> (aa # xs) ! i\<rbrakk> \<Longrightarrow> of_nat (length (aa # xs)) * a \<le> sum_list (aa # xs)
[PROOF STEP]
have "x \<ge> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> x
[PROOF STEP]
using xxs_i_ge_a
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length (x # xs). a \<le> (x # xs) ! i

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

goal (2 subgoals):
 1. \<forall>i<length []. a \<le> [] ! i \<Longrightarrow> of_nat (length []) * a \<le> sum_list []
 2. \<And>aa xs. \<lbrakk>\<forall>i<length xs. a \<le> xs ! i \<Longrightarrow> of_nat (length xs) * a \<le> sum_list xs; \<forall>i<length (aa # xs). a \<le> (aa # xs) ! i\<rbrakk> \<Longrightarrow> of_nat (length (aa # xs)) * a \<le> sum_list (aa # xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a \<le> x

goal (1 subgoal):
 1. of_nat (length (x # xs)) * a \<le> sum_list (x # xs)
[PROOF STEP]
using ih[OF xs_i_ge_a]
[PROOF STATE]
proof (prove)
using this:
a \<le> x
of_nat (length xs) * a \<le> sum_list xs

goal (1 subgoal):
 1. of_nat (length (x # xs)) * a \<le> sum_list (x # xs)
[PROOF STEP]
by (simp add: ring_distribs ordered_ab_semigroup_add_class.add_mono)
[PROOF STATE]
proof (state)
this:
of_nat (length (x # xs)) * a \<le> sum_list (x # xs)

goal (1 subgoal):
 1. \<forall>i<length []. a \<le> [] ! i \<Longrightarrow> of_nat (length []) * a \<le> sum_list []
[PROOF STEP]
qed auto


[STATEMENT]
lemma prod_list_nonneg:
  fixes xs :: "('a :: {ordered_semiring_0,linordered_nonzero_semiring}) list"
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0"
  shows "prod_list xs \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> prod_list xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> (0::'a) \<le> ?x

goal (1 subgoal):
 1. (0::'a) \<le> prod_list xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma zip_append_0_upt:
  "zip (xs @ ys) [0..<length xs + length ys] =
   zip xs [0..<length xs] @ zip ys [length xs..<length xs + length ys]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip (xs @ ys) [0..<length xs + length ys] = zip xs [0..<length xs] @ zip ys [length xs..<length xs + length ys]
[PROOF STEP]
proof (induct ys arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. zip (xs @ []) [0..<length xs + length []] = zip xs [0..<length xs] @ zip [] [length xs..<length xs + length []]
 2. \<And>a ys xs. (\<And>xs. zip (xs @ ys) [0..<length xs + length ys] = zip xs [0..<length xs] @ zip ys [length xs..<length xs + length ys]) \<Longrightarrow> zip (xs @ a # ys) [0..<length xs + length (a # ys)] = zip xs [0..<length xs] @ zip (a # ys) [length xs..<length xs + length (a # ys)]
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
zip (?xs @ ys) [0..<length ?xs + length ys] = zip ?xs [0..<length ?xs] @ zip ys [length ?xs..<length ?xs + length ys]

goal (2 subgoals):
 1. \<And>xs. zip (xs @ []) [0..<length xs + length []] = zip xs [0..<length xs] @ zip [] [length xs..<length xs + length []]
 2. \<And>a ys xs. (\<And>xs. zip (xs @ ys) [0..<length xs + length ys] = zip xs [0..<length xs] @ zip ys [length xs..<length xs + length ys]) \<Longrightarrow> zip (xs @ a # ys) [0..<length xs + length (a # ys)] = zip xs [0..<length xs] @ zip (a # ys) [length xs..<length xs + length (a # ys)]
[PROOF STEP]
note ih = this
[PROOF STATE]
proof (state)
this:
zip (?xs @ ys) [0..<length ?xs + length ys] = zip ?xs [0..<length ?xs] @ zip ys [length ?xs..<length ?xs + length ys]

goal (2 subgoals):
 1. \<And>xs. zip (xs @ []) [0..<length xs + length []] = zip xs [0..<length xs] @ zip [] [length xs..<length xs + length []]
 2. \<And>a ys xs. (\<And>xs. zip (xs @ ys) [0..<length xs + length ys] = zip xs [0..<length xs] @ zip ys [length xs..<length xs + length ys]) \<Longrightarrow> zip (xs @ a # ys) [0..<length xs + length (a # ys)] = zip xs [0..<length xs] @ zip (a # ys) [length xs..<length xs + length (a # ys)]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip (xs @ y # ys) [0..<length xs + length (y # ys)] = zip xs [0..<length xs] @ zip (y # ys) [length xs..<length xs + length (y # ys)]
[PROOF STEP]
using ih[of "xs @ [y]"]
[PROOF STATE]
proof (prove)
using this:
zip ((xs @ [y]) @ ys) [0..<length (xs @ [y]) + length ys] = zip (xs @ [y]) [0..<length (xs @ [y])] @ zip ys [length (xs @ [y])..<length (xs @ [y]) + length ys]

goal (1 subgoal):
 1. zip (xs @ y # ys) [0..<length xs + length (y # ys)] = zip xs [0..<length xs] @ zip (y # ys) [length xs..<length xs + length (y # ys)]
[PROOF STEP]
by (simp, cases ys, simp, simp add: upt_rec)
[PROOF STATE]
proof (state)
this:
zip (xs @ y # ys) [0..<length xs + length (y # ys)] = zip xs [0..<length xs] @ zip (y # ys) [length xs..<length xs + length (y # ys)]

goal (1 subgoal):
 1. \<And>xs. zip (xs @ []) [0..<length xs + length []] = zip xs [0..<length xs] @ zip [] [length xs..<length xs + length []]
[PROOF STEP]
qed auto


[STATEMENT]
lemma zip_eq_butlast_last:
  assumes len_gt0: "length xs > 0" and len_eq: "length xs = length ys"
  shows "zip xs ys = zip (butlast xs) (butlast ys) @ [(last xs, last ys)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip xs ys = zip (butlast xs) (butlast ys) @ [(last xs, last ys)]
[PROOF STEP]
using len_eq len_gt0
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
0 < length xs

goal (1 subgoal):
 1. zip xs ys = zip (butlast xs) (butlast ys) @ [(last xs, last ys)]
[PROOF STEP]
by (induct rule: list_induct2) auto


[STATEMENT]
lemma the_enat_0[simp]: "the_enat 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat 0 = 0
[PROOF STEP]
by (simp add: zero_enat_def)


[STATEMENT]
lemma the_enat_1[simp]: "the_enat 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_enat 1 = 1
[PROOF STEP]
by (simp add: one_enat_def)


[STATEMENT]
lemma enat_le_minus_1_imp_lt: "m \<le> n - 1 \<Longrightarrow> n \<noteq> \<infinity> \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m < n" for m n :: enat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n - 1; n \<noteq> \<infinity>; n \<noteq> 0\<rbrakk> \<Longrightarrow> m < n
[PROOF STEP]
by (cases m; cases n; simp add: zero_enat_def one_enat_def)


[STATEMENT]
lemma enat_diff_diff_eq: "k - m - n = k - (m + n)" for k m n :: enat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k - m - n = k - (m + n)
[PROOF STEP]
by (cases k; cases m; cases n) auto


[STATEMENT]
lemma enat_the_enat_iden[simp]: "n \<noteq> \<infinity> \<Longrightarrow> enat (the_enat n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> \<infinity> \<Longrightarrow> enat (the_enat n) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma the_enat_minus_nat: "m \<noteq> \<infinity> \<Longrightarrow> the_enat (m - enat n) = the_enat m - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<noteq> \<infinity> \<Longrightarrow> the_enat (m - enat n) = the_enat m - n
[PROOF STEP]
by auto


[STATEMENT]
lemma enat_the_enat_le: "enat (the_enat x) \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (the_enat x) \<le> x
[PROOF STEP]
by (cases x; simp)


[STATEMENT]
lemma enat_the_enat_minus_le: "enat (the_enat (x - y)) \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (the_enat (x - y)) \<le> x
[PROOF STEP]
by (cases x; cases y; simp)


[STATEMENT]
lemma enat_le_imp_minus_le: "k \<le> m \<Longrightarrow> k - n \<le> m" for k m n :: enat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> m \<Longrightarrow> k - n \<le> m
[PROOF STEP]
by (metis Groups.add_ac(2) enat_diff_diff_eq enat_ord_simps(3) enat_sub_add_same
    enat_the_enat_iden enat_the_enat_minus_le idiff_0_right idiff_infinity idiff_infinity_right
    order_trans_rules(23) plus_enat_simps(3))


[STATEMENT]
lemma add_diff_assoc2_enat: "m \<ge> n \<Longrightarrow> m - n + p = m + p - n" for m n p :: enat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> m - n + p = m + p - n
[PROOF STEP]
by (cases m; cases n; cases p; auto)


[STATEMENT]
lemma enat_mult_minus_distrib: "enat x * (y - z) = enat x * y - enat x * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat x * (y - z) = enat x * y - enat x * z
[PROOF STEP]
by (cases y; cases z; auto simp: enat_0 right_diff_distrib')


[STATEMENT]
lemma add_mset_lt_left_lt: "a < b \<Longrightarrow> add_mset a A < add_mset b A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b \<Longrightarrow> add_mset a A < add_mset b A
[PROOF STEP]
unfolding less_multiset\<^sub>H\<^sub>O
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b \<Longrightarrow> add_mset a A \<noteq> add_mset b A \<and> (\<forall>y. count (add_mset b A) y < count (add_mset a A) y \<longrightarrow> (\<exists>x>y. count (add_mset a A) x < count (add_mset b A) x))
[PROOF STEP]
by auto


[STATEMENT]
lemma add_mset_le_left_le: "a \<le> b \<Longrightarrow> add_mset a A \<le> add_mset b A" for a :: "'a :: linorder"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> add_mset a A \<le> add_mset b A
[PROOF STEP]
unfolding less_multiset\<^sub>H\<^sub>O
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> add_mset a A \<le> add_mset b A
[PROOF STEP]
by auto


[STATEMENT]
lemma add_mset_lt_right_lt: "A < B \<Longrightarrow> add_mset a A < add_mset a B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A < B \<Longrightarrow> add_mset a A < add_mset a B
[PROOF STEP]
unfolding less_multiset\<^sub>H\<^sub>O
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> B \<and> (\<forall>y. count B y < count A y \<longrightarrow> (\<exists>x>y. count A x < count B x)) \<Longrightarrow> add_mset a A \<noteq> add_mset a B \<and> (\<forall>y. count (add_mset a B) y < count (add_mset a A) y \<longrightarrow> (\<exists>x>y. count (add_mset a A) x < count (add_mset a B) x))
[PROOF STEP]
by auto


[STATEMENT]
lemma add_mset_le_right_le: "A \<le> B \<Longrightarrow> add_mset a A \<le> add_mset a B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> add_mset a A \<le> add_mset a B
[PROOF STEP]
unfolding less_multiset\<^sub>H\<^sub>O
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> add_mset a A \<le> add_mset a B
[PROOF STEP]
by auto


[STATEMENT]
lemma add_mset_lt_lt_lt:
  assumes a_lt_b: "a < b" and A_le_B: "A < B"
  shows "add_mset a A < add_mset b B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset a A < add_mset b B
[PROOF STEP]
by (rule less_trans[OF add_mset_lt_left_lt[OF a_lt_b] add_mset_lt_right_lt[OF A_le_B]])


[STATEMENT]
lemma add_mset_lt_lt_le: "a < b \<Longrightarrow> A \<le> B \<Longrightarrow> add_mset a A < add_mset b B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; A \<le> B\<rbrakk> \<Longrightarrow> add_mset a A < add_mset b B
[PROOF STEP]
using add_mset_lt_lt_lt le_neq_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < ?b; ?A < ?B\<rbrakk> \<Longrightarrow> add_mset ?a ?A < add_mset ?b ?B
\<lbrakk>?a \<le> ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. \<lbrakk>a < b; A \<le> B\<rbrakk> \<Longrightarrow> add_mset a A < add_mset b B
[PROOF STEP]
by fastforce


[STATEMENT]
lemma add_mset_le_le_le:
  fixes a :: "'a :: linorder"
  assumes a_le_b: "a \<le> b" and A_le_B: "A \<le> B"
  shows "add_mset a A \<le> add_mset b B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset a A \<le> add_mset b B
[PROOF STEP]
by (rule order.trans[OF add_mset_le_left_le[OF a_le_b] add_mset_le_right_le[OF A_le_B]])


[STATEMENT]
lemma nonempty_subseteq_mset_eq_singleton: "M \<noteq> {#} \<Longrightarrow> M \<subseteq># {#x#} \<Longrightarrow> M = {#x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M \<noteq> {#}; M \<subseteq># {#x#}\<rbrakk> \<Longrightarrow> M = {#x#}
[PROOF STEP]
by (cases M) (auto dest: subset_mset.diff_add)


[STATEMENT]
lemma nonempty_subseteq_mset_iff_singleton: "(M \<noteq> {#} \<and> M \<subseteq># {#x#} \<and> P) \<longleftrightarrow> M = {#x#} \<and> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M \<noteq> {#} \<and> M \<subseteq># {#x#} \<and> P) = (M = {#x#} \<and> P)
[PROOF STEP]
by (cases M) (auto dest: subset_mset.diff_add)


[STATEMENT]
lemma count_gt_imp_in_mset[intro]: "count M x > n \<Longrightarrow> x \<in># M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < count M x \<Longrightarrow> x \<in># M
[PROOF STEP]
using count_greater_zero_iff
[PROOF STATE]
proof (prove)
using this:
(0 < count ?M ?x) = (?x \<in># ?M)

goal (1 subgoal):
 1. n < count M x \<Longrightarrow> x \<in># M
[PROOF STEP]
by fastforce


[STATEMENT]
lemma size_lt_imp_ex_count_lt: "size M < size N \<Longrightarrow> \<exists>x \<in># N. count M x < count N x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size M < size N \<Longrightarrow> \<exists>x\<in>#N. count M x < count N x
[PROOF STEP]
by (metis count_eq_zero_iff leD not_le_imp_less not_less_zero size_mset_mono subseteq_mset_def)


[STATEMENT]
lemma filter_filter_mset[simp]: "{#x \<in># {#x \<in># M. Q x#}. P x#} = {#x \<in># M. P x \<and> Q x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_mset P (filter_mset Q M) = {#x \<in># M. P x \<and> Q x#}
[PROOF STEP]
by (induct M) auto


[STATEMENT]
lemma size_filter_unsat_elem:
  assumes "x \<in># M" and "\<not> P x"
  shows "size {#x \<in># M. P x#} < size M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (filter_mset P M) < size M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. size (filter_mset P M) < size M
[PROOF STEP]
have "size (filter_mset P M) \<noteq> size M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (filter_mset P M) \<noteq> size M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in># M
\<not> P x

goal (1 subgoal):
 1. size (filter_mset P M) \<noteq> size M
[PROOF STEP]
by (metis add.right_neutral add_diff_cancel_left' count_filter_mset mem_Collect_eq
      multiset_partition nonempty_has_size set_mset_def size_union)
[PROOF STATE]
proof (state)
this:
size (filter_mset P M) \<noteq> size M

goal (1 subgoal):
 1. size (filter_mset P M) < size M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size (filter_mset P M) \<noteq> size M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
size (filter_mset P M) \<noteq> size M

goal (1 subgoal):
 1. size (filter_mset P M) < size M
[PROOF STEP]
by (meson leD nat_neq_iff size_filter_mset_lesseq)
[PROOF STATE]
proof (state)
this:
size (filter_mset P M) < size M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_filter_ne_elem: "x \<in># M \<Longrightarrow> size {#y \<in># M. y \<noteq> x#} < size M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in># M \<Longrightarrow> size {#y \<in># M. y \<noteq> x#} < size M
[PROOF STEP]
by (simp add: size_filter_unsat_elem[of x M "\<lambda>y. y \<noteq> x"])


[STATEMENT]
lemma size_eq_ex_count_lt:
  assumes
    sz_m_eq_n: "size M = size N" and
    m_eq_n: "M \<noteq> N"
  shows "\<exists>x. count M x < count N x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
obtain x where "count M x \<noteq> count N x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. count M x \<noteq> count N x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using m_eq_n
[PROOF STATE]
proof (prove)
using this:
M \<noteq> N

goal (1 subgoal):
 1. (\<And>x. count M x \<noteq> count N x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson multiset_eqI)
[PROOF STATE]
proof (state)
this:
count M x \<noteq> count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
count M x \<noteq> count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
count M x \<noteq> count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
assume "count M x < count N x"
[PROOF STATE]
proof (state)
this:
count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
count M x < count N x \<Longrightarrow> \<exists>x. count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
count M x < count N x \<Longrightarrow> \<exists>x. count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
count M x < count N x \<Longrightarrow> \<exists>x. count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
assume cnt_x: "count M x > count N x"
[PROOF STATE]
proof (state)
this:
count N x < count M x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
have "size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} =
      size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} = size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
using sz_m_eq_n multiset_partition
[PROOF STATE]
proof (prove)
using this:
size M = size N
?M = filter_mset ?P ?M + {#x \<in># ?M. \<not> ?P x#}

goal (1 subgoal):
 1. size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} = size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
by (metis size_union)
[PROOF STATE]
proof (state)
this:
size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} = size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
hence sz_m_minus_x: "size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}"
[PROOF STATE]
proof (prove)
using this:
size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} = size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}

goal (1 subgoal):
 1. size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
using cnt_x
[PROOF STATE]
proof (prove)
using this:
size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} = size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}
count N x < count M x

goal (1 subgoal):
 1. size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
obtain y where "count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y"
[PROOF STATE]
proof (prove)
using this:
size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}

goal (1 subgoal):
 1. (\<And>y. count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using size_lt_imp_ex_count_lt[OF sz_m_minus_x]
[PROOF STATE]
proof (prove)
using this:
size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}
\<exists>xa\<in>#{#y \<in># N. y \<noteq> x#}. count {#y \<in># M. y \<noteq> x#} xa < count {#y \<in># N. y \<noteq> x#} xa

goal (1 subgoal):
 1. (\<And>y. count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
hence "count M y < count N y"
[PROOF STATE]
proof (prove)
using this:
count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y

goal (1 subgoal):
 1. count M y < count N y
[PROOF STEP]
by (metis count_filter_mset less_asym)
[PROOF STATE]
proof (state)
this:
count M y < count N y

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
count M y < count N y

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
count N x < count M x \<Longrightarrow> \<exists>x. count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
count M x \<noteq> count N x
count M x < count N x \<Longrightarrow> \<exists>x. count M x < count N x
count N x < count M x \<Longrightarrow> \<exists>x. count M x < count N x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count M x \<noteq> count N x
count M x < count N x \<Longrightarrow> \<exists>x. count M x < count N x
count N x < count M x \<Longrightarrow> \<exists>x. count M x < count N x

goal (1 subgoal):
 1. \<exists>x. count M x < count N x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>x. count M x < count N x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_image_mset_lt_imp_lt_raw:
  assumes
    "finite A" and
    "A = set_mset M \<union> set_mset N" and
    "count (image_mset f M) b < count (image_mset f N) b"
  shows "\<exists>x. f x = b \<and> count M x < count N x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
A = set_mset M \<union> set_mset N
count (image_mset f M) b < count (image_mset f N) b

goal (1 subgoal):
 1. \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
proof (induct A arbitrary: M N b rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>F = set_mset ?M \<union> set_mset ?N; count (image_mset f ?M) ?b < count (image_mset f ?N) ?b\<rbrakk> \<Longrightarrow> \<exists>x. f x = ?b \<and> count ?M x < count ?N x
insert x F = set_mset M \<union> set_mset N
count (image_mset f M) b < count (image_mset f N) b

goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
    cnt_b = this(5)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>F = set_mset ?M \<union> set_mset ?N; count (image_mset f ?M) ?b < count (image_mset f ?N) ?b\<rbrakk> \<Longrightarrow> \<exists>x. f x = ?b \<and> count ?M x < count ?N x
insert x F = set_mset M \<union> set_mset N
count (image_mset f M) b < count (image_mset f N) b

goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
let ?Ma = "{#y \<in># M. y \<noteq> x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
let ?Mb = "{#y \<in># M. y = x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
let ?Na = "{#y \<in># N. y \<noteq> x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
let ?Nb = "{#y \<in># N. y = x#}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M = {#y \<in># M. y = x#} + {#y \<in># M. y \<noteq> x#} &&& N = {#y \<in># N. y = x#} + {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
using multiset_partition
[PROOF STATE]
proof (prove)
using this:
?M = filter_mset ?P ?M + {#x \<in># ?M. \<not> ?P x#}

goal (1 subgoal):
 1. M = {#y \<in># M. y = x#} + {#y \<in># M. y \<noteq> x#} &&& N = {#y \<in># N. y = x#} + {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
M = {#y \<in># M. y = x#} + {#y \<in># M. y \<noteq> x#}
N = {#y \<in># N. y = x#} + {#y \<in># N. y \<noteq> x#}

goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = set_mset {#y \<in># M. y \<noteq> x#} \<union> set_mset {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
using x_f_eq_m_n x_ni_f
[PROOF STATE]
proof (prove)
using this:
insert x F = set_mset M \<union> set_mset N
x \<notin> F

goal (1 subgoal):
 1. F = set_mset {#y \<in># M. y \<noteq> x#} \<union> set_mset {#y \<in># N. y \<noteq> x#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = set_mset {#y \<in># M. y \<noteq> x#} \<union> set_mset {#y \<in># N. y \<noteq> x#}

goal (2 subgoals):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<And>x F M N b. \<lbrakk>finite F; x \<notin> F; \<And>M N b. \<lbrakk>F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x; insert x F = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
proof (cases "count (image_mset f ?Ma) b < count (image_mset f ?Na) b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
case cnt_ba: True
[PROOF STATE]
proof (state)
this:
count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b

goal (2 subgoals):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
obtain xa where "f xa = b" and "count ?Ma xa < count ?Na xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xa. \<lbrakk>f xa = b; count {#y \<in># M. y \<noteq> x#} xa < count {#y \<in># N. y \<noteq> x#} xa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ih[OF f_eq_ma_na cnt_ba]
[PROOF STATE]
proof (prove)
using this:
\<exists>xa. f xa = b \<and> count {#y \<in># M. y \<noteq> x#} xa < count {#y \<in># N. y \<noteq> x#} xa

goal (1 subgoal):
 1. (\<And>xa. \<lbrakk>f xa = b; count {#y \<in># M. y \<noteq> x#} xa < count {#y \<in># N. y \<noteq> x#} xa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f xa = b
count {#y \<in># M. y \<noteq> x#} xa < count {#y \<in># N. y \<noteq> x#} xa

goal (2 subgoals):
 1. count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
 2. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f xa = b
count {#y \<in># M. y \<noteq> x#} xa < count {#y \<in># N. y \<noteq> x#} xa

goal (1 subgoal):
 1. \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
by (metis count_filter_mset not_less0)
[PROOF STATE]
proof (state)
this:
\<exists>x. f x = b \<and> count M x < count N x

goal (1 subgoal):
 1. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
case cnt_ba: False
[PROOF STATE]
proof (state)
this:
\<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b

goal (1 subgoal):
 1. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
have fx_eq_b: "f x = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = b
[PROOF STEP]
using cnt_b cnt_ba
[PROOF STATE]
proof (prove)
using this:
count (image_mset f M) b < count (image_mset f N) b
\<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b

goal (1 subgoal):
 1. f x = b
[PROOF STEP]
by (subst (asm) m_part, subst (asm) n_part, auto, presburger)
[PROOF STATE]
proof (state)
this:
f x = b

goal (1 subgoal):
 1. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f x = b

goal (1 subgoal):
 1. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
have "count M x < count N x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count M x < count N x
[PROOF STEP]
using cnt_b cnt_ba
[PROOF STATE]
proof (prove)
using this:
count (image_mset f M) b < count (image_mset f N) b
\<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b

goal (1 subgoal):
 1. count M x < count N x
[PROOF STEP]
by (subst (asm) m_part, subst (asm) n_part, auto simp: fx_eq_b)
[PROOF STATE]
proof (state)
this:
count M x < count N x

goal (1 subgoal):
 1. \<not> count (image_mset f {#y \<in># M. y \<noteq> x#}) b < count (image_mset f {#y \<in># N. y \<noteq> x#}) b \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f x = b
count M x < count N x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f x = b
count M x < count N x

goal (1 subgoal):
 1. \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. f x = b \<and> count M x < count N x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. f x = b \<and> count M x < count N x

goal (1 subgoal):
 1. \<And>M N b. \<lbrakk>{} = set_mset M \<union> set_mset N; count (image_mset f M) b < count (image_mset f N) b\<rbrakk> \<Longrightarrow> \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
qed auto


[STATEMENT]
lemma count_image_mset_lt_imp_lt:
  assumes cnt_b: "count (image_mset f M) b < count (image_mset f N) b"
  shows "\<exists>x. f x = b \<and> count M x < count N x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. f x = b \<and> count M x < count N x
[PROOF STEP]
by (rule count_image_mset_lt_imp_lt_raw[of "set_mset M \<union> set_mset N", OF _ refl cnt_b]) auto