[STATEMENT]
lemma mono_on_subset: "\<lbrakk> mono_on f A ; B \<subseteq> A \<rbrakk> \<Longrightarrow> mono_on f B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SetInterval2.mono_on f A; B \<subseteq> A\<rbrakk> \<Longrightarrow> SetInterval2.mono_on f B
[PROOF STEP]
unfolding mono_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; B \<subseteq> A\<rbrakk> \<Longrightarrow> \<forall>a\<in>B. \<forall>b\<in>B. a \<le> b \<longrightarrow> f a \<le> f b
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_mono_on_subset: "\<lbrakk> strict_mono_on f A ; B \<subseteq> A \<rbrakk> \<Longrightarrow> strict_mono_on f B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SetInterval2.strict_mono_on f A; B \<subseteq> A\<rbrakk> \<Longrightarrow> SetInterval2.strict_mono_on f B
[PROOF STEP]
unfolding strict_mono_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a < b \<longrightarrow> f a < f b; B \<subseteq> A\<rbrakk> \<Longrightarrow> \<forall>a\<in>B. \<forall>b\<in>B. a < b \<longrightarrow> f a < f b
[PROOF STEP]
by blast


[STATEMENT]
lemma mono_on_UNIV_mono_conv: "mono_on f UNIV = mono f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetInterval2.mono_on f UNIV = mono f
[PROOF STEP]
unfolding mono_on_def mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a\<in>UNIV. \<forall>b\<in>UNIV. a \<le> b \<longrightarrow> f a \<le> f b) = (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_mono_on_UNIV_strict_mono_conv: "
  strict_mono_on f UNIV = strict_mono f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetInterval2.strict_mono_on f UNIV = strict_mono f
[PROOF STEP]
unfolding strict_mono_on_def strict_mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>a\<in>UNIV. \<forall>b\<in>UNIV. a < b \<longrightarrow> f a < f b) = (\<forall>x y. x < y \<longrightarrow> f x < f y)
[PROOF STEP]
by blast


[STATEMENT]
lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono f \<Longrightarrow> SetInterval2.mono_on f A
[PROOF STEP]
unfolding mono_on_def mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_mono_imp_strict_mono_on: "strict_mono f \<Longrightarrow> strict_mono_on f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono f \<Longrightarrow> SetInterval2.strict_mono_on f A
[PROOF STEP]
unfolding strict_mono_on_def strict_mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x < y \<longrightarrow> f x < f y \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>A. a < b \<longrightarrow> f a < f b
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_mono_on_imp_mono_on: "strict_mono_on f A \<Longrightarrow> mono_on f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetInterval2.strict_mono_on f A \<Longrightarrow> SetInterval2.mono_on f A
[PROOF STEP]
apply (unfold strict_mono_on_def mono_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>A. \<forall>b\<in>A. a < b \<longrightarrow> f a < f b \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b
[PROOF STEP]
apply (fastforce simp: order_le_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inj_imp_inj_on: "inj f \<Longrightarrow> inj_on f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f \<Longrightarrow> inj_on f A
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. \<forall>y\<in>UNIV. f x = f y \<longrightarrow> x = y \<Longrightarrow> \<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_mono_on_imp_inj_on: "
  strict_mono_on f (A::'a::linorder set) \<Longrightarrow> inj_on f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetInterval2.strict_mono_on f A \<Longrightarrow> inj_on f A
[PROOF STEP]
apply (unfold strict_mono_on_def inj_on_def, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a < b \<longrightarrow> f a < f b; x \<in> A; y \<in> A; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a < b \<longrightarrow> f a < f b; x \<in> A; y \<in> A; f x = f y; x \<noteq> y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (fastforce simp add: linorder_neq_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strict_mono_imp_inj: "strict_mono (f::('a::linorder \<Rightarrow> 'b::order)) \<Longrightarrow> inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono f \<Longrightarrow> inj f
[PROOF STEP]
by (rule strict_mono_imp_inj_on)


[STATEMENT]
lemma strict_mono_on_mono_on_conv: "
  strict_mono_on f (A::'a::linorder set) = (mono_on f A \<and> inj_on f A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetInterval2.strict_mono_on f A = (SetInterval2.mono_on f A \<and> inj_on f A)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. SetInterval2.strict_mono_on f A \<Longrightarrow> SetInterval2.mono_on f A \<and> inj_on f A
 2. SetInterval2.mono_on f A \<and> inj_on f A \<Longrightarrow> SetInterval2.strict_mono_on f A
[PROOF STEP]
apply (frule strict_mono_on_imp_mono_on)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>SetInterval2.strict_mono_on f A; SetInterval2.mono_on f A\<rbrakk> \<Longrightarrow> SetInterval2.mono_on f A \<and> inj_on f A
 2. SetInterval2.mono_on f A \<and> inj_on f A \<Longrightarrow> SetInterval2.strict_mono_on f A
[PROOF STEP]
apply (frule strict_mono_on_imp_inj_on)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>SetInterval2.strict_mono_on f A; SetInterval2.mono_on f A; inj_on f A\<rbrakk> \<Longrightarrow> SetInterval2.mono_on f A \<and> inj_on f A
 2. SetInterval2.mono_on f A \<and> inj_on f A \<Longrightarrow> SetInterval2.strict_mono_on f A
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SetInterval2.mono_on f A \<and> inj_on f A \<Longrightarrow> SetInterval2.strict_mono_on f A
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SetInterval2.mono_on f A; inj_on f A\<rbrakk> \<Longrightarrow> SetInterval2.strict_mono_on f A
[PROOF STEP]
apply (unfold inj_on_def mono_on_def strict_mono_on_def, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y; a \<in> A; b \<in> A; a < b\<rbrakk> \<Longrightarrow> f a < f b
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inj_on_image_mem_iff: "
  \<lbrakk> inj_on f A; B \<subseteq> A; a \<in> A \<rbrakk> \<Longrightarrow> (f a \<in> f ` B) = (a \<in> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; B \<subseteq> A; a \<in> A\<rbrakk> \<Longrightarrow> (f a \<in> f ` B) = (a \<in> B)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y; B \<subseteq> A; a \<in> A\<rbrakk> \<Longrightarrow> (f a \<in> f ` B) = (a \<in> B)
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_conv: "(surj_on f A B) = (\<forall>b\<in>B. \<exists>a\<in>A. b = f a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f A B = (\<forall>b\<in>B. \<exists>a\<in>A. b = f a)
[PROOF STEP]
unfolding surj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>b\<in>B. \<exists>a\<in>A. b = f a) = (\<forall>b\<in>B. \<exists>a\<in>A. b = f a)
[PROOF STEP]
..


[STATEMENT]
lemma surj_on_id: "surj_on id A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on id A A
[PROOF STEP]
unfolding id_def surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>A. \<exists>a\<in>A. b = a
[PROOF STEP]
by blast


[STATEMENT]
lemma comp_surj_on: "
  \<lbrakk> surj_on f A B; surj_on g B C \<rbrakk> \<Longrightarrow> surj_on (g \<circ> f) A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>surj_on f A B; surj_on g B C\<rbrakk> \<Longrightarrow> surj_on (g \<circ> f) A C
[PROOF STEP]
unfolding comp_def surj_on_image_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B \<subseteq> f ` A; C \<subseteq> g ` B\<rbrakk> \<Longrightarrow> C \<subseteq> (\<lambda>x. g (f x)) ` A
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_Un_right: "surj_on f A (B1 \<union> B2) = (surj_on f A B1 \<and> surj_on f A B2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f A (B1 \<union> B2) = (surj_on f A B1 \<and> surj_on f A B2)
[PROOF STEP]
unfolding surj_on_image_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B1 \<union> B2 \<subseteq> f ` A) = (B1 \<subseteq> f ` A \<and> B2 \<subseteq> f ` A)
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_Un_left: "
  surj_on f (A1 \<union> A2) B =
  (\<exists>B1. \<exists>B2. B \<subseteq> B1 \<union> B2 \<and> surj_on f A1 B1 \<and> surj_on f A2 B2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f (A1 \<union> A2) B = (\<exists>B1 B2. B \<subseteq> B1 \<union> B2 \<and> surj_on f A1 B1 \<and> surj_on f A2 B2)
[PROOF STEP]
unfolding surj_on_image_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B \<subseteq> f ` (A1 \<union> A2)) = (\<exists>B1 B2. B \<subseteq> B1 \<union> B2 \<and> B1 \<subseteq> f ` A1 \<and> B2 \<subseteq> f ` A2)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. B \<subseteq> f ` (A1 \<union> A2) \<Longrightarrow> \<exists>B1 B2. B \<subseteq> B1 \<union> B2 \<and> B1 \<subseteq> f ` A1 \<and> B2 \<subseteq> f ` A2
 2. \<exists>B1 B2. B \<subseteq> B1 \<union> B2 \<and> B1 \<subseteq> f ` A1 \<and> B2 \<subseteq> f ` A2 \<Longrightarrow> B \<subseteq> f ` (A1 \<union> A2)
[PROOF STEP]
apply (rule_tac x="f ` A1" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. B \<subseteq> f ` (A1 \<union> A2) \<Longrightarrow> \<exists>B2. B \<subseteq> f ` A1 \<union> B2 \<and> f ` A1 \<subseteq> f ` A1 \<and> B2 \<subseteq> f ` A2
 2. \<exists>B1 B2. B \<subseteq> B1 \<union> B2 \<and> B1 \<subseteq> f ` A1 \<and> B2 \<subseteq> f ` A2 \<Longrightarrow> B \<subseteq> f ` (A1 \<union> A2)
[PROOF STEP]
apply (rule_tac x="f ` A2" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. B \<subseteq> f ` (A1 \<union> A2) \<Longrightarrow> B \<subseteq> f ` A1 \<union> f ` A2 \<and> f ` A1 \<subseteq> f ` A1 \<and> f ` A2 \<subseteq> f ` A2
 2. \<exists>B1 B2. B \<subseteq> B1 \<union> B2 \<and> B1 \<subseteq> f ` A1 \<and> B2 \<subseteq> f ` A2 \<Longrightarrow> B \<subseteq> f ` (A1 \<union> A2)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B1 B2. B \<subseteq> B1 \<union> B2 \<and> B1 \<subseteq> f ` A1 \<and> B2 \<subseteq> f ` A2 \<Longrightarrow> B \<subseteq> f ` (A1 \<union> A2)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma surj_on_diff_right: "surj_on f A B \<Longrightarrow> surj_on f A (B - B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f A B \<Longrightarrow> surj_on f A (B - B')
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>a\<in>A. b = f a \<Longrightarrow> \<forall>b\<in>B - B'. \<exists>a\<in>A. b = f a
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_empty_left: "surj_on f {} B = (B = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f {} B = (B = {})
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>b\<in>B. \<exists>a\<in>{}. b = f a) = (B = {})
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_imageI: "surj_on (g \<circ> f) A B \<Longrightarrow> surj_on g (f ` A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on (g \<circ> f) A B \<Longrightarrow> surj_on g (f ` A) B
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>B. \<exists>a\<in>A. b = (g \<circ> f) a \<Longrightarrow> \<forall>b\<in>B. \<exists>a\<in>f ` A. b = g a
[PROOF STEP]
by fastforce


[STATEMENT]
lemma surj_on_insert_right: "surj_on f A (insert b B) = (surj_on f A B \<and> surj_on f A {b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f A (insert b B) = (surj_on f A B \<and> surj_on f A {b})
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>b\<in>insert b B. \<exists>a\<in>A. b = f a) = ((\<forall>b\<in>B. \<exists>a\<in>A. b = f a) \<and> (\<forall>b\<in>{b}. \<exists>a\<in>A. b = f a))
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_insert_left: "surj_on f (insert a A) B = (surj_on f A (B - {f a}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj_on f (insert a A) B = surj_on f A (B - {f a})
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>b\<in>B. \<exists>a\<in>insert a A. b = f a) = (\<forall>b\<in>B - {f a}. \<exists>a\<in>A. b = f a)
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_subset_right: "\<lbrakk> surj_on f A B; B' \<subseteq> B \<rbrakk> \<Longrightarrow> surj_on f A B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>surj_on f A B; B' \<subseteq> B\<rbrakk> \<Longrightarrow> surj_on f A B'
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>b\<in>B. \<exists>a\<in>A. b = f a; B' \<subseteq> B\<rbrakk> \<Longrightarrow> \<forall>b\<in>B'. \<exists>a\<in>A. b = f a
[PROOF STEP]
by blast


[STATEMENT]
lemma surj_on_subset_left: "\<lbrakk> surj_on f A B; A \<subseteq> A' \<rbrakk> \<Longrightarrow> surj_on f A' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>surj_on f A B; A \<subseteq> A'\<rbrakk> \<Longrightarrow> surj_on f A' B
[PROOF STEP]
unfolding surj_on_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>b\<in>B. \<exists>a\<in>A. b = f a; A \<subseteq> A'\<rbrakk> \<Longrightarrow> \<forall>b\<in>B. \<exists>a\<in>A'. b = f a
[PROOF STEP]
by blast


[STATEMENT]
lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B \<Longrightarrow> surj_on f A B
[PROOF STEP]
unfolding bij_betw_def surj_on_image_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A \<and> f ` A = B \<Longrightarrow> B \<subseteq> f ` A
[PROOF STEP]
by simp


[STATEMENT]
lemma bij_betw_inj_on_surj_on_conv: "
  bij_betw f A B = (inj_on f A \<and> surj_on f A B \<and> f ` A \<subseteq> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A B = (inj_on f A \<and> surj_on f A B \<and> f ` A \<subseteq> B)
[PROOF STEP]
unfolding bij_betw_def surj_on_image_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inj_on f A \<and> f ` A = B) = (inj_on f A \<and> B \<subseteq> f ` A \<and> f ` A \<subseteq> B)
[PROOF STEP]
by blast


[STATEMENT]
lemma image_nat_induct: "
  \<lbrakk> P (f 0); \<And>n. P (f n) \<Longrightarrow> P (f (Suc n)); surj_on f UNIV I; a \<in> I \<rbrakk> \<Longrightarrow> P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (f 0); \<And>n. P (f n) \<Longrightarrow> P (f (Suc n)); surj_on f UNIV I; a \<in> I\<rbrakk> \<Longrightarrow> P a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>P (f 0); \<And>n. P (f n) \<Longrightarrow> P (f (Suc n)); surj_on f UNIV I; a \<in> I\<rbrakk> \<Longrightarrow> P a
[PROOF STEP]
assume as_P0: "P (f 0)"
    and  as_IA: "\<And>n. P (f n) \<Longrightarrow> P (f (Suc n))"
    and  as_surj_f: "surj_on f UNIV I"
    and  as_a: "a \<in> I"
[PROOF STATE]
proof (state)
this:
P (f 0)
P (f ?n) \<Longrightarrow> P (f (Suc ?n))
surj_on f UNIV I
a \<in> I

goal (1 subgoal):
 1. \<lbrakk>P (f 0); \<And>n. P (f n) \<Longrightarrow> P (f (Suc n)); surj_on f UNIV I; a \<in> I\<rbrakk> \<Longrightarrow> P a
[PROOF STEP]
have P_n:"\<And>n. P (f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. P (f n)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. P (f 0)
 2. \<And>n na. P (f na) \<Longrightarrow> P (f (Suc na))
[PROOF STEP]
apply (simp only: as_P0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. P (f na) \<Longrightarrow> P (f (Suc na))
[PROOF STEP]
apply (simp only: as_IA)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
P (f ?n)

goal (1 subgoal):
 1. \<lbrakk>P (f 0); \<And>n. P (f n) \<Longrightarrow> P (f (Suc n)); surj_on f UNIV I; a \<in> I\<rbrakk> \<Longrightarrow> P a
[PROOF STEP]
have "\<forall>x\<in>I. \<exists>n. x = f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>I. \<exists>n. x = f n
[PROOF STEP]
using as_surj_f
[PROOF STATE]
proof (prove)
using this:
surj_on f UNIV I

goal (1 subgoal):
 1. \<forall>x\<in>I. \<exists>n. x = f n
[PROOF STEP]
by (unfold surj_on_conv, blast)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>I. \<exists>n. x = f n

goal (1 subgoal):
 1. \<lbrakk>P (f 0); \<And>n. P (f n) \<Longrightarrow> P (f (Suc n)); surj_on f UNIV I; a \<in> I\<rbrakk> \<Longrightarrow> P a
[PROOF STEP]
hence "\<exists>n. a = f n"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>I. \<exists>n. x = f n

goal (1 subgoal):
 1. \<exists>n. a = f n
[PROOF STEP]
using as_a
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>I. \<exists>n. x = f n
a \<in> I

goal (1 subgoal):
 1. \<exists>n. a = f n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. a = f n

goal (1 subgoal):
 1. \<lbrakk>P (f 0); \<And>n. P (f n) \<Longrightarrow> P (f (Suc n)); surj_on f UNIV I; a \<in> I\<rbrakk> \<Longrightarrow> P a
[PROOF STEP]
thus "P a"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. a = f n

goal (1 subgoal):
 1. P a
[PROOF STEP]
using P_n
[PROOF STATE]
proof (prove)
using this:
\<exists>n. a = f n
P (f ?n)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_induct'[rule_format]: "
  \<lbrakk> P n0; \<And>n. \<lbrakk> n0 \<le> n;  P n \<rbrakk> \<Longrightarrow> P (Suc n); n0 \<le> n \<rbrakk> \<Longrightarrow> P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P n0; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (Suc n); n0 \<le> n\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
by (insert nat_induct[where n="n-n0" and P="\<lambda>n. P (n0+n)"], simp)


[STATEMENT]
lemma enat_induct: "
  \<lbrakk> P 0; P \<infinity>; \<And>n. P n \<Longrightarrow> P (eSuc n)\<rbrakk> \<Longrightarrow> P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P 0; P \<infinity>; \<And>n. P n \<Longrightarrow> P (eSuc n)\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply (case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>P 0; P \<infinity>; \<And>n. P n \<Longrightarrow> P (eSuc n); n = enat nat\<rbrakk> \<Longrightarrow> P n
 2. \<lbrakk>P 0; P \<infinity>; \<And>n. P n \<Longrightarrow> P (eSuc n); n = \<infinity>\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P 0; P \<infinity>; \<And>n. P n \<Longrightarrow> P (eSuc n); n = \<infinity>\<rbrakk> \<Longrightarrow> P n
 2. \<And>nat. \<lbrakk>P 0; P \<infinity>; \<And>n. P n \<Longrightarrow> P (eSuc n); n = enat nat\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>P 0; P \<infinity>; \<And>n. P n \<Longrightarrow> P (eSuc n); n = enat nat\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply (simp only: enat_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>P (enat 0); P \<infinity>; \<And>n. P n \<Longrightarrow> P (case n of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>); n = enat nat\<rbrakk> \<Longrightarrow> P (enat nat)
[PROOF STEP]
apply (rename_tac n1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n1. \<lbrakk>P (enat 0); P \<infinity>; \<And>n. P n \<Longrightarrow> P (case n of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>); n = enat n1\<rbrakk> \<Longrightarrow> P (enat n1)
[PROOF STEP]
apply (induct_tac n1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n1. \<lbrakk>P (enat 0); P \<infinity>; \<And>n. P n \<Longrightarrow> P (case n of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>); n = enat n1\<rbrakk> \<Longrightarrow> P (enat 0)
 2. \<And>n1 na. \<lbrakk>P (enat 0); P \<infinity>; \<And>n. P n \<Longrightarrow> P (case n of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>); n = enat n1; P (enat na)\<rbrakk> \<Longrightarrow> P (enat (Suc na))
[PROOF STEP]
apply (simp add: enat.splits)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eSuc_imp_Suc_aux_0:
  "\<lbrakk> \<And>n. P n \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. P n \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))
[PROOF STEP]
by (simp only: enat_defs enat.splits)


[STATEMENT]
lemma eSuc_imp_Suc_aux_n0:
  "\<lbrakk> \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))
[PROOF STEP]
assume IA: "\<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n)"
    and n0_n: "n0' \<le> n'"
    and Pn: "P (enat n')"
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat n0' \<le> ?n; P ?n\<rbrakk> \<Longrightarrow> P (eSuc ?n)
n0' \<le> n'
P (enat n')

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))
[PROOF STEP]
from n0_n
[PROOF STATE]
proof (chain)
picking this:
n0' \<le> n'
[PROOF STEP]
have "(enat n0' \<le> enat n')"
[PROOF STATE]
proof (prove)
using this:
n0' \<le> n'

goal (1 subgoal):
 1. enat n0' \<le> enat n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat n0' \<le> enat n'

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))
[PROOF STEP]
with Pn IA
[PROOF STATE]
proof (chain)
picking this:
P (enat n')
\<lbrakk>enat n0' \<le> ?n; P ?n\<rbrakk> \<Longrightarrow> P (eSuc ?n)
enat n0' \<le> enat n'
[PROOF STEP]
have "P (eSuc (enat n'))"
[PROOF STATE]
proof (prove)
using this:
P (enat n')
\<lbrakk>enat n0' \<le> ?n; P ?n\<rbrakk> \<Longrightarrow> P (eSuc ?n)
enat n0' \<le> enat n'

goal (1 subgoal):
 1. P (eSuc (enat n'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P (eSuc (enat n'))

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; P (enat n')\<rbrakk> \<Longrightarrow> P (enat (Suc n'))
[PROOF STEP]
thus "P (enat (Suc n'))"
[PROOF STATE]
proof (prove)
using this:
P (eSuc (enat n'))

goal (1 subgoal):
 1. P (enat (Suc n'))
[PROOF STEP]
by (simp only: eSuc_enat)
[PROOF STATE]
proof (state)
this:
P (enat (Suc n'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enat_induct': "
  \<lbrakk> P (n0::enat); P \<infinity>; \<And>n. \<lbrakk> n0 \<le> n;  P n \<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n \<rbrakk> \<Longrightarrow> P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply (case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat\<rbrakk> \<Longrightarrow> P n
 2. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = \<infinity>\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = \<infinity>\<rbrakk> \<Longrightarrow> P n
 2. \<And>nat. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply (case_tac n0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat nata. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat; n0 = enat nata\<rbrakk> \<Longrightarrow> P n
 2. \<And>nat. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat; n0 = \<infinity>\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat; n0 = \<infinity>\<rbrakk> \<Longrightarrow> P n
 2. \<And>nat nata. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat; n0 = enat nata\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat nata. \<lbrakk>P n0; P \<infinity>; \<And>n. \<lbrakk>n0 \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0 \<le> n; n = enat nat; n0 = enat nata\<rbrakk> \<Longrightarrow> P n
[PROOF STEP]
apply (rename_tac n' n0', simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n' n0'. \<lbrakk>P (enat n0'); P \<infinity>; \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; n = enat n'; n0 = enat n0'\<rbrakk> \<Longrightarrow> P (enat n')
[PROOF STEP]
apply (rule_tac ?n0.0="n0'" and n=n' and P="\<lambda>n. P (enat n)" in nat_induct')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n' n0'. \<lbrakk>P (enat n0'); P \<infinity>; \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; n = enat n'; n0 = enat n0'\<rbrakk> \<Longrightarrow> P (enat n0')
 2. \<And>n' n0' na. \<lbrakk>P (enat n0'); P \<infinity>; \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; n = enat n'; n0 = enat n0'; n0' \<le> na; P (enat na)\<rbrakk> \<Longrightarrow> P (enat (Suc na))
 3. \<And>n' n0'. \<lbrakk>P (enat n0'); P \<infinity>; \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; n = enat n'; n0 = enat n0'\<rbrakk> \<Longrightarrow> n0' \<le> n'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n' n0' na. \<lbrakk>P (enat n0'); P \<infinity>; \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; n = enat n'; n0 = enat n0'; n0' \<le> na; P (enat na)\<rbrakk> \<Longrightarrow> P (enat (Suc na))
 2. \<And>n' n0'. \<lbrakk>P (enat n0'); P \<infinity>; \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; n = enat n'; n0 = enat n0'\<rbrakk> \<Longrightarrow> n0' \<le> n'
[PROOF STEP]
apply (simp add: eSuc_enat[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n' n0'. \<lbrakk>P (enat n0'); P \<infinity>; \<And>n. \<lbrakk>enat n0' \<le> n; P n\<rbrakk> \<Longrightarrow> P (eSuc n); n0' \<le> n'; n = enat n'; n0 = enat n0'\<rbrakk> \<Longrightarrow> n0' \<le> n'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_less_interval:"
  wf { (x,y). x \<in> (I::nat set) \<and> y \<in> I \<and> x < y }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(x, y). x \<in> I \<and> y \<in> I \<and> x < y}
[PROOF STEP]
apply (rule wf_subset[where
  p="{ (x,y). x \<in> I \<and> y \<in> I \<and> x < y }" and
  r="{(x,y). x < y}"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf {(x, y). x < y}
 2. {(x, y). x \<in> I \<and> y \<in> I \<and> x < y} \<subseteq> {(x, y). x < y}
[PROOF STEP]
apply (rule wf_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> I \<and> y \<in> I \<and> x < y} \<subseteq> {(x, y). x < y}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma interval_induct: "
  \<lbrakk> \<And>x. \<forall>y. (x\<in>(I::nat set) \<and> y \<in> I \<and> y < x \<longrightarrow> P y) \<Longrightarrow> P x \<rbrakk>
  \<Longrightarrow> P a"
  (is "\<lbrakk> \<And>x. \<forall>y. ?IA x y \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> P a")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<forall>y. x \<in> I \<and> y \<in> I \<and> y < x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a
[PROOF STEP]
apply (rule_tac r="{ (x,y). x \<in> I \<and> y \<in> I \<and> x < y }" in wf_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>x. \<forall>y. x \<in> I \<and> y \<in> I \<and> y < x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> wf {(x, y). x \<in> I \<and> y \<in> I \<and> x < y}
 2. \<And>x. \<lbrakk>\<And>x. \<forall>y. x \<in> I \<and> y \<in> I \<and> y < x \<longrightarrow> P y \<Longrightarrow> P x; \<forall>y. (y, x) \<in> {(x, y). x \<in> I \<and> y \<in> I \<and> x < y} \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply (rule wf_less_interval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. \<forall>y. x \<in> I \<and> y \<in> I \<and> y < x \<longrightarrow> P y \<Longrightarrow> P x; \<forall>y. (y, x) \<in> {(x, y). x \<in> I \<and> y \<in> I \<and> x < y} \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_left_inj: "inj (\<lambda>x. n + (x::'a::cancel_ab_semigroup_add))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj ((+) n)
[PROOF STEP]
by (simp add: inj_on_def)


[STATEMENT]
lemma add_right_inj: "inj (\<lambda>x. x + (n::'a::cancel_ab_semigroup_add))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>x. x + n)
[PROOF STEP]
by (simp add: inj_on_def)


[STATEMENT]
lemma mult_left_inj: "0 < n \<Longrightarrow> inj (\<lambda>x. (n::nat) * x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> inj ((*) n)
[PROOF STEP]
by (simp add: inj_on_def)


[STATEMENT]
lemma mult_right_inj: "0 < n \<Longrightarrow> inj (\<lambda>x. x * (n::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> inj (\<lambda>x. x * n)
[PROOF STEP]
by (simp add: inj_on_def)


[STATEMENT]
lemma sub_left_inj_on: "inj_on (\<lambda>x. (x::nat) - k) {k..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. x - k) {k..}
[PROOF STEP]
by (rule inj_onI, simp)


[STATEMENT]
lemma sub_right_inj_on: "inj_on (\<lambda>x. k - (x::nat)) {..k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ((-) k) {..k}
[PROOF STEP]
by (rule inj_onI, simp)


[STATEMENT]
lemma add_left_strict_mono: "strict_mono (\<lambda>x. n + (x::'a::ordered_cancel_ab_semigroup_add))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono ((+) n)
[PROOF STEP]
by (unfold strict_mono_def, clarify, rule add_strict_left_mono)


[STATEMENT]
lemma add_right_strict_mono: "strict_mono (\<lambda>x. x + (n::'a::ordered_cancel_ab_semigroup_add))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono (\<lambda>x. x + n)
[PROOF STEP]
by (unfold strict_mono_def, clarify, rule add_strict_right_mono)


[STATEMENT]
lemma mult_left_strict_mono: "0 < n \<Longrightarrow> strict_mono (\<lambda>x. n * (x::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> strict_mono ((*) n)
[PROOF STEP]
by (unfold strict_mono_def, clarify, simp)


[STATEMENT]
lemma mult_right_strict_mono: "0 < n \<Longrightarrow> strict_mono (\<lambda>x. x * (n::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> strict_mono (\<lambda>x. x * n)
[PROOF STEP]
by (unfold strict_mono_def, clarify, simp)


[STATEMENT]
lemma div_right_strict_mono_on: "
  \<lbrakk> 0 < (k::nat); \<forall>x\<in>I. \<forall>y\<in>I. x < y \<longrightarrow> x + k \<le> y \<rbrakk> \<Longrightarrow>
  strict_mono_on (\<lambda>x. x div k) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; \<forall>x\<in>I. \<forall>y\<in>I. x < y \<longrightarrow> x + k \<le> y\<rbrakk> \<Longrightarrow> SetInterval2.strict_mono_on (\<lambda>x. x div k) I
[PROOF STEP]
apply (unfold strict_mono_on_def, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>0 < k; \<forall>x\<in>I. \<forall>y\<in>I. x < y \<longrightarrow> x + k \<le> y; a \<in> I; b \<in> I; a < b\<rbrakk> \<Longrightarrow> a div k < b div k
[PROOF STEP]
apply (fastforce dest: div_le_mono[of _ _ k])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mod_eq_div_right_strict_mono_on: "
  \<lbrakk> 0 < (k::nat); \<forall>x\<in>I. \<forall>y\<in>I. x mod k = y mod k \<rbrakk> \<Longrightarrow>
  strict_mono_on (\<lambda>x. x div k) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; \<forall>x\<in>I. \<forall>y\<in>I. x mod k = y mod k\<rbrakk> \<Longrightarrow> SetInterval2.strict_mono_on (\<lambda>x. x div k) I
[PROOF STEP]
apply (rule div_right_strict_mono_on, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; \<forall>x\<in>I. \<forall>y\<in>I. x mod k = y mod k\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. \<forall>y\<in>I. x < y \<longrightarrow> x + k \<le> y
[PROOF STEP]
apply (blast intro: less_mod_eq_imp_add_divisor_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMinI: "k \<in> I \<Longrightarrow> iMin I \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> I \<Longrightarrow> iMin I \<in> I
[PROOF STEP]
unfolding iMin_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> I \<Longrightarrow> (LEAST x. x \<in> I) \<in> I
[PROOF STEP]
by (rule_tac k=k in LeastI)


[STATEMENT]
lemma iMinI_ex: "\<exists>x. x \<in> I \<Longrightarrow> iMin I \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> I \<Longrightarrow> iMin I \<in> I
[PROOF STEP]
by (blast intro: iMinI)


[STATEMENT]
lemma iMinI2: "\<lbrakk> k \<in> I; \<And>x. x \<in> I \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> P (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; \<And>x. x \<in> I \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P (iMin I)
[PROOF STEP]
by (blast intro: iMinI)


[STATEMENT]
lemma iMinI2_ex: "\<lbrakk> \<exists>x. x \<in> I; \<And>x. x \<in> I \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> P (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. x \<in> I; \<And>x. x \<in> I \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P (iMin I)
[PROOF STEP]
by (blast intro: iMinI_ex)


[STATEMENT]
lemma iMinI2_ex2: "\<lbrakk> I \<noteq> {} ; \<And>x. x \<in> I \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> P (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<And>x. x \<in> I \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P (iMin I)
[PROOF STEP]
by (blast intro: iMinI_ex2)


[STATEMENT]
lemma iMin_le[dest]: "k \<in> I \<Longrightarrow> iMin I \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> I \<Longrightarrow> iMin I \<le> k
[PROOF STEP]
by (simp only: iMin_def Least_le)


[STATEMENT]
lemma iMin_neq_imp_greater[dest]: "\<lbrakk> k \<in> I; k \<noteq> iMin I \<rbrakk> \<Longrightarrow> iMin I < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; k \<noteq> iMin I\<rbrakk> \<Longrightarrow> iMin I < k
[PROOF STEP]
by (rule order_neq_le_trans[OF not_sym iMin_le])


[STATEMENT]
lemma iMin_mono: "
  \<lbrakk> mono f; \<exists>x. x \<in> I \<rbrakk> \<Longrightarrow> iMin (f ` I) = f (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono f; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> iMin (f ` I) = f (iMin I)
[PROOF STEP]
apply (unfold iMin_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono f; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> (LEAST x. x \<in> f ` I) = f (LEAST x. x \<in> I)
[PROOF STEP]
apply (rule Least_mono[of f I], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono f; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. \<forall>xa\<in>I. x \<le> xa
[PROOF STEP]
apply (rule_tac x="iMin I" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mono f; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. iMin I \<le> x
 2. \<lbrakk>mono f; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> iMin I \<in> I
[PROOF STEP]
apply (simp add: iMin_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono f; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> iMin I \<in> I
[PROOF STEP]
apply (simp add: iMinI_ex)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_less_iMin: "k < iMin I \<Longrightarrow> k \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < iMin I \<Longrightarrow> k \<notin> I
[PROOF STEP]
unfolding iMin_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < (LEAST x. x \<in> I) \<Longrightarrow> k \<notin> I
[PROOF STEP]
by (rule not_less_Least)


[STATEMENT]
lemma Collect_not_less_iMin: "k < iMin {x. P x} \<Longrightarrow> \<not> P k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < iMin {x. P x} \<Longrightarrow> \<not> P k
[PROOF STEP]
by (drule not_less_iMin, blast)


[STATEMENT]
lemma Collect_iMin_le: "P k \<Longrightarrow> iMin {x. P x} \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P k \<Longrightarrow> iMin {x. P x} \<le> k
[PROOF STEP]
by (rule iMin_le, blast)


[STATEMENT]
lemma Collect_minI: "\<lbrakk> k \<in> I; P (k::('a::wellorder)) \<rbrakk> \<Longrightarrow> \<exists>x\<in>I. P x \<and> (\<forall>y\<in>I. y < x \<longrightarrow> \<not> P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> \<exists>x\<in>I. P x \<and> (\<forall>y\<in>I. y < x \<longrightarrow> \<not> P y)
[PROOF STEP]
apply (rule_tac x="iMin {y \<in> I. P y}" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> P (iMin {y \<in> I. P y}) \<and> (\<forall>y\<in>I. y < iMin {y \<in> I. P y} \<longrightarrow> \<not> P y)
 2. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> iMin {y \<in> I. P y} \<in> I
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> iMin {y \<in> I. P y} \<in> I
 2. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> P (iMin {y \<in> I. P y}) \<and> (\<forall>y\<in>I. y < iMin {y \<in> I. P y} \<longrightarrow> \<not> P y)
[PROOF STEP]
apply (rule subsetD[OF _ iMinI, OF Collect_is_subset], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> P (iMin {y \<in> I. P y}) \<and> (\<forall>y\<in>I. y < iMin {y \<in> I. P y} \<longrightarrow> \<not> P y)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> P (iMin {y \<in> I. P y})
 2. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> \<forall>y\<in>I. y < iMin {y \<in> I. P y} \<longrightarrow> \<not> P y
[PROOF STEP]
apply (blast intro: iMinI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; P k\<rbrakk> \<Longrightarrow> \<forall>y\<in>I. y < iMin {y \<in> I. P y} \<longrightarrow> \<not> P y
[PROOF STEP]
apply (blast dest: not_less_iMin)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMin_the:  "iMin I = (THE x. x \<in> I \<and> (\<forall>y. y \<in> I \<longrightarrow> x \<le> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMin I = (THE x. x \<in> I \<and> (\<forall>y. y \<in> I \<longrightarrow> x \<le> y))
[PROOF STEP]
by (simp add: iMin_def Least_def)


[STATEMENT]
lemma iMin_the2: "iMin I = (THE x. x \<in> I \<and> (\<forall>y\<in>I. x \<le> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMin I = (THE x. x \<in> I \<and> (\<forall>y\<in>I. x \<le> y))
[PROOF STEP]
apply (simp add: iMin_the)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE x. x \<in> I \<and> (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)) = (THE x. x \<in> I \<and> (\<forall>y\<in>I. x \<le> y))
[PROOF STEP]
apply (subgoal_tac "\<And>x. (\<forall>y \<in> I. x \<le> y) = (\<forall>y. y \<in> I \<longrightarrow> x \<le> y) ")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>x. (\<forall>y\<in>I. x \<le> y) = (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)) \<Longrightarrow> (THE x. x \<in> I \<and> (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)) = (THE x. x \<in> I \<and> (\<forall>y\<in>I. x \<le> y))
 2. \<And>x. (\<forall>y\<in>I. x \<le> y) = (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<forall>y\<in>I. x \<le> y) = (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)
 2. (\<And>x. (\<forall>y\<in>I. x \<le> y) = (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)) \<Longrightarrow> (THE x. x \<in> I \<and> (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)) = (THE x. x \<in> I \<and> (\<forall>y\<in>I. x \<le> y))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (\<forall>y\<in>I. x \<le> y) = (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)) \<Longrightarrow> (THE x. x \<in> I \<and> (\<forall>y. y \<in> I \<longrightarrow> x \<le> y)) = (THE x. x \<in> I \<and> (\<forall>y\<in>I. x \<le> y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMin_equality: "
  \<lbrakk> k \<in> I; \<And>x. x \<in> I \<Longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> iMin I = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; \<And>x. x \<in> I \<Longrightarrow> k \<le> x\<rbrakk> \<Longrightarrow> iMin I = k
[PROOF STEP]
unfolding iMin_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; \<And>x. x \<in> I \<Longrightarrow> k \<le> x\<rbrakk> \<Longrightarrow> (LEAST x. x \<in> I) = k
[PROOF STEP]
by (blast intro: Least_equality)


[STATEMENT]
lemma iMin_mono_on: "
  \<lbrakk> mono_on f I; \<exists>x. x \<in> I \<rbrakk> \<Longrightarrow> iMin (f ` I) = f (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SetInterval2.mono_on f I; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> iMin (f ` I) = f (iMin I)
[PROOF STEP]
apply (unfold mono_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>I. \<forall>b\<in>I. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> iMin (f ` I) = f (iMin I)
[PROOF STEP]
apply (rule iMin_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a\<in>I. \<forall>b\<in>I. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> I\<rbrakk> \<Longrightarrow> f (iMin I) \<in> f ` I
 2. \<And>x. \<lbrakk>\<forall>a\<in>I. \<forall>b\<in>I. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> I; x \<in> f ` I\<rbrakk> \<Longrightarrow> f (iMin I) \<le> x
[PROOF STEP]
apply (blast intro: iMinI_ex)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMin_mono_on2: "
  \<lbrakk> mono_on f I; I \<noteq> {} \<rbrakk> \<Longrightarrow> iMin (f ` I) = f (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SetInterval2.mono_on f I; I \<noteq> {}\<rbrakk> \<Longrightarrow> iMin (f ` I) = f (iMin I)
[PROOF STEP]
by (rule iMin_mono_on, blast+)


[STATEMENT]
lemma iMinI2_order:"
  \<lbrakk> k \<in> I; \<And>y. y \<in> I \<Longrightarrow> k \<le> y;
    \<And>x. \<lbrakk> x \<in> I; \<forall>y\<in>I. x \<le> y \<rbrakk> \<Longrightarrow> P x \<rbrakk> \<Longrightarrow>
  P (iMin I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> I; \<And>y. y \<in> I \<Longrightarrow> k \<le> y; \<And>x. \<lbrakk>x \<in> I; \<forall>y\<in>I. x \<le> y\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P (iMin I)
[PROOF STEP]
by (simp add: iMin_def LeastI2_order)


[STATEMENT]
lemma wellorder_iMin_lemma: "
  k \<in> I \<Longrightarrow> iMin I \<in> I \<and> iMin I \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> I \<Longrightarrow> iMin I \<in> I \<and> iMin I \<le> k
[PROOF STEP]
by (blast intro: iMinI iMin_le)


[STATEMENT]
lemma iMin_Min_conv: "
  \<lbrakk> finite I; I \<noteq> {} \<rbrakk> \<Longrightarrow> iMin I = Min I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; I \<noteq> {}\<rbrakk> \<Longrightarrow> iMin I = Min I
[PROOF STEP]
apply (rule order_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite I; I \<noteq> {}\<rbrakk> \<Longrightarrow> iMin I \<le> Min I
 2. \<lbrakk>finite I; I \<noteq> {}\<rbrakk> \<Longrightarrow> Min I \<le> iMin I
[PROOF STEP]
apply (rule Min_ge_iff[THEN iffD2], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite I; I \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>a\<in>I. iMin I \<le> a
 2. \<lbrakk>finite I; I \<noteq> {}\<rbrakk> \<Longrightarrow> Min I \<le> iMin I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; I \<noteq> {}\<rbrakk> \<Longrightarrow> Min I \<le> iMin I
[PROOF STEP]
apply (rule Min_le_iff[THEN iffD2], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; I \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>a\<in>I. a \<le> iMin I
[PROOF STEP]
apply (blast intro: iMinI_ex2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Min_neq_imp_greater[dest]: "\<lbrakk> finite I; k \<in> I; k \<noteq> Min I \<rbrakk> \<Longrightarrow> Min I < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; k \<in> I; k \<noteq> Min I\<rbrakk> \<Longrightarrow> Min I < k
[PROOF STEP]
by (rule order_neq_le_trans[OF not_sym Min_le])


[STATEMENT]
lemma Max_neq_imp_less[dest]: "\<lbrakk> finite I; k \<in> I; k \<noteq> Max I \<rbrakk> \<Longrightarrow> k < Max I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; k \<in> I; k \<noteq> Max I\<rbrakk> \<Longrightarrow> k < Max I
[PROOF STEP]
by (rule order_neq_le_trans[OF _ Max_ge])


[STATEMENT]
lemma nat_Least_mono: "
  \<lbrakk> A \<noteq> {}; mono (f::(nat\<Rightarrow>nat)) \<rbrakk> \<Longrightarrow>
  (LEAST x. x \<in> f ` A) = f (LEAST x. x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; incseq f\<rbrakk> \<Longrightarrow> (LEAST x. x \<in> f ` A) = f (LEAST x. x \<in> A)
[PROOF STEP]
unfolding iMin_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; incseq f\<rbrakk> \<Longrightarrow> iMin (f ` A) = f (iMin A)
[PROOF STEP]
by (blast intro: iMin_mono2)


[STATEMENT]
lemma Least_disj: "
  \<lbrakk> \<exists>x. P x; \<exists>x. Q x \<rbrakk> \<Longrightarrow>
  (LEAST (x::'a::wellorder). (P x \<or> Q x)) = min (LEAST x. P x) (LEAST x. Q x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<exists>x. Q x\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (elim exE, rename_tac x1 x2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>P x1; Q x2\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (subgoal_tac "\<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
 2. \<And>x1 x2 x1a x2a Pa Qa. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa\<rbrakk> \<Longrightarrow> (LEAST x. Pa x \<or> Qa x) = Least Pa
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a Pa Qa. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa\<rbrakk> \<Longrightarrow> (LEAST x. Pa x \<or> Qa x) = Least Pa
 2. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (rule Least_equality)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x1a x2a Pa Qa. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa\<rbrakk> \<Longrightarrow> Pa (Least Pa) \<or> Qa (Least Pa)
 2. \<And>x1 x2 x1a x2a Pa Qa y. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa; Pa y \<or> Qa y\<rbrakk> \<Longrightarrow> Least Pa \<le> y
 3. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (blast intro: LeastI Least_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a Pa Qa y. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa; Pa y \<or> Qa y\<rbrakk> \<Longrightarrow> Least Pa \<le> y
 2. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x1a x2a Pa Qa y. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa; Pa y\<rbrakk> \<Longrightarrow> Least Pa \<le> y
 2. \<And>x1 x2 x1a x2a Pa Qa y. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa; Qa y\<rbrakk> \<Longrightarrow> Least Pa \<le> y
 3. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (rule Least_le, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a Pa Qa y. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa; Qa y\<rbrakk> \<Longrightarrow> Least Pa \<le> y
 2. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (rule order_trans, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a Pa Qa y. \<lbrakk>P x1; Q x2; Pa x1a; Qa x2a; Least Pa \<le> Least Qa; Qa y\<rbrakk> \<Longrightarrow> Least Qa \<le> y
 2. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (rule Least_le, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = min (LEAST x. P x) (LEAST x. Q x)
[PROOF STEP]
apply (unfold min_def, split if_split, safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P
 2. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P; \<not> Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least Q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P; \<not> Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least Q
[PROOF STEP]
apply (subst disj_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>P x1; Q x2; \<And>x1 x2 P Q. \<lbrakk>P x1; Q x2; Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = Least P; \<not> Least P \<le> Least Q\<rbrakk> \<Longrightarrow> (LEAST x. Q x \<or> P x) = Least Q
[PROOF STEP]
apply (fastforce simp: linorder_not_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Least_imp_le: "
  \<lbrakk> \<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow>
  (LEAST (x::'a::wellorder). Q x) \<le> (LEAST x. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> (LEAST x. Q x) \<le> (LEAST x. P x)
[PROOF STEP]
by (blast intro: Least_le LeastI2_ex)


[STATEMENT]
lemma Least_imp_disj_eq: "
  \<lbrakk> \<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow>
  (LEAST (x::'a::wellorder). P x \<or> Q x) = (LEAST x. Q x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = (LEAST x. Q x)
[PROOF STEP]
apply (subst Least_disj, assumption, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> min (Least P) (Least Q) = Least Q
[PROOF STEP]
apply (subst min.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> min (Least Q) (Least P) = Least Q
[PROOF STEP]
apply (rule min.absorb_iff1[THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Least Q \<le> Least P
[PROOF STEP]
apply (rule Least_imp_le, assumption, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Least_le_imp_le: "
  \<lbrakk> \<exists>x. P x; \<exists>x. Q x; \<And>x y. \<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> x \<le> y \<rbrakk> \<Longrightarrow>
  (LEAST (x::'a::wellorder). P x) \<le> (LEAST (x::'a::wellorder). Q x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<exists>x. Q x; \<And>x y. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> (LEAST x. P x) \<le> (LEAST x. Q x)
[PROOF STEP]
by (blast intro: LeastI)


[STATEMENT]
lemma Least_le_imp_le_disj: "
  \<lbrakk> \<exists>x. P x; \<And>x y. \<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> x \<le> y \<rbrakk> \<Longrightarrow>
  (LEAST (x::'a::wellorder). P x \<or> Q x) = (LEAST (x::'a::wellorder). P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x y. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = (LEAST x. P x)
[PROOF STEP]
apply (case_tac "\<exists>x. Q x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<exists>x. P x; \<And>x y. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> x \<le> y; \<exists>x. Q x\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = (LEAST x. P x)
 2. \<lbrakk>\<exists>x. P x; \<And>x y. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> x \<le> y; \<nexists>x. Q x\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = (LEAST x. P x)
[PROOF STEP]
apply (simp only: Least_disj min.absorb_iff1[THEN iffD1, OF Least_le_imp_le])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. P x; \<And>x y. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> x \<le> y; \<nexists>x. Q x\<rbrakk> \<Longrightarrow> (LEAST x. P x \<or> Q x) = (LEAST x. P x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Max_equality: "\<lbrakk> (k::'a::linorder) \<in> A; finite A; \<And>x. x \<in> A \<Longrightarrow> x \<le> k \<rbrakk> \<Longrightarrow>
  Max A = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> A; finite A; \<And>x. x \<in> A \<Longrightarrow> x \<le> k\<rbrakk> \<Longrightarrow> Max A = k
[PROOF STEP]
by (rule Max_eqI)


[STATEMENT]
lemma not_greater_Max: "\<lbrakk> finite A; Max A < k \<rbrakk>  \<Longrightarrow> k \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < k\<rbrakk> \<Longrightarrow> k \<notin> A
[PROOF STEP]
apply (rule ccontr, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < k; k \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule Max_ge[of A k], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < k; k \<in> A; k \<le> Max A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule order_le_less_trans[of _ _ k], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < k; k \<in> A; k \<le> Max A; k < k\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Collect_not_greater_Max: "\<lbrakk> finite {x. P x}; Max {x. P x} < k \<rbrakk> \<Longrightarrow> \<not> P k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {x. P x}; Max {x. P x} < k\<rbrakk> \<Longrightarrow> \<not> P k
[PROOF STEP]
by (drule not_greater_Max, assumption, drule Collect_not_in_imp_not)


[STATEMENT]
lemma Collect_Max_ge: "\<lbrakk> finite {x. P x}; P k \<rbrakk> \<Longrightarrow> k \<le> Max {x. P x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {x. P x}; P k\<rbrakk> \<Longrightarrow> k \<le> Max {x. P x}
[PROOF STEP]
by (rule Max_ge, assumption, rule CollectI)


[STATEMENT]
lemma MaxI: "\<lbrakk> k \<in> A; finite A \<rbrakk> \<Longrightarrow> Max A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> A; finite A\<rbrakk> \<Longrightarrow> Max A \<in> A
[PROOF STEP]
by (case_tac "A = {}", simp_all)


[STATEMENT]
lemma MaxI_ex: "\<lbrakk> \<exists>x. x \<in> A; finite A \<rbrakk> \<Longrightarrow> Max A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> Max A \<in> A
[PROOF STEP]
by (blast intro: MaxI)


[STATEMENT]
lemma MaxI_ex2: "\<lbrakk> A \<noteq> {}; finite A \<rbrakk> \<Longrightarrow> Max A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> Max A \<in> A
[PROOF STEP]
by (blast intro: MaxI)


[STATEMENT]
lemma MaxI2_ex:"\<lbrakk> \<exists>x. x \<in> A; \<And>x. x \<in> A \<Longrightarrow> P x; finite A \<rbrakk> \<Longrightarrow> P (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x. x \<in> A; \<And>x. x \<in> A \<Longrightarrow> P x; finite A\<rbrakk> \<Longrightarrow> P (Max A)
[PROOF STEP]
by (blast intro: MaxI2)


[STATEMENT]
lemma MaxI2_ex2:"\<lbrakk> A \<noteq> {}; \<And>x. x \<in> A \<Longrightarrow> P x; finite A \<rbrakk> \<Longrightarrow> P (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; \<And>x. x \<in> A \<Longrightarrow> P x; finite A\<rbrakk> \<Longrightarrow> P (Max A)
[PROOF STEP]
by (blast intro: MaxI2)


[STATEMENT]
lemma Max_mono: "\<lbrakk> mono f; \<exists>x. x \<in> A; finite A \<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono f; \<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
apply (unfold mono_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y; \<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y; finite A; x \<in> A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
apply (frule Max_in, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y; finite A; x \<in> A; Max A \<in> A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
apply (rule Max_equality, clarsimp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Max_mono2:"\<lbrakk> mono f; A \<noteq> {}; finite A \<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono f; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
by (blast intro: Max_mono)


[STATEMENT]
lemma Max_mono_on: "\<lbrakk> mono_on f A; \<exists>x. x \<in> A; finite A \<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SetInterval2.mono_on f A; \<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
apply (unfold mono_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
apply (rule Max_equality)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> f (Max A) \<in> f ` A
 2. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> finite (f ` A)
 3. \<And>x. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> A; finite A; x \<in> f ` A\<rbrakk> \<Longrightarrow> x \<le> f (Max A)
[PROOF STEP]
apply (blast intro: Max_in)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> A; finite A\<rbrakk> \<Longrightarrow> finite (f ` A)
 2. \<And>x. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> A; finite A; x \<in> f ` A\<rbrakk> \<Longrightarrow> x \<le> f (Max A)
[PROOF STEP]
apply (rule finite_imageI, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>a\<in>A. \<forall>b\<in>A. a \<le> b \<longrightarrow> f a \<le> f b; \<exists>x. x \<in> A; finite A; x \<in> f ` A\<rbrakk> \<Longrightarrow> x \<le> f (Max A)
[PROOF STEP]
apply (blast intro: Max_in Max_ge)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Max_mono_on2: "
  \<lbrakk> mono_on f A; A \<noteq> {}; finite A \<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SetInterval2.mono_on f A; A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> Max (f ` A) = f (Max A)
[PROOF STEP]
by (rule Max_mono_on, blast+)


[STATEMENT]
lemma Max_the: "
  \<lbrakk> A \<noteq> {}; finite A \<rbrakk> \<Longrightarrow>
  Max A = (THE x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> Max A = (THE x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x))
[PROOF STEP]
apply (rule iffD1[OF eq_commute])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> (THE x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)) = Max A
[PROOF STEP]
apply (rule the_equality, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>A \<noteq> {}; finite A; x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)\<rbrakk> \<Longrightarrow> x = Max A
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>A \<noteq> {}; finite A; x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)\<rbrakk> \<Longrightarrow> Max A = x
[PROOF STEP]
apply (rule Max_equality)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>A \<noteq> {}; finite A; x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)\<rbrakk> \<Longrightarrow> x \<in> A
 2. \<And>x. \<lbrakk>A \<noteq> {}; finite A; x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)\<rbrakk> \<Longrightarrow> finite A
 3. \<And>x xa. \<lbrakk>A \<noteq> {}; finite A; x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x); xa \<in> A\<rbrakk> \<Longrightarrow> xa \<le> x
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Max_the2: "\<lbrakk> A \<noteq> {}; finite A \<rbrakk> \<Longrightarrow>
  Max A = (THE x. x \<in> A \<and> (\<forall>y\<in>A. y \<le> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> Max A = (THE x. x \<in> A \<and> (\<forall>y\<in>A. y \<le> x))
[PROOF STEP]
apply (simp add: Max_the)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> (THE x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)) = (THE x. x \<in> A \<and> (\<forall>y\<in>A. y \<le> x))
[PROOF STEP]
apply (subgoal_tac "\<And>x. (\<forall>y\<in>A. y \<le> x) = (\<forall>y. y \<in> A \<longrightarrow> y \<le> x) ")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; finite A; \<And>x. (\<forall>y\<in>A. y \<le> x) = (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)\<rbrakk> \<Longrightarrow> (THE x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)) = (THE x. x \<in> A \<and> (\<forall>y\<in>A. y \<le> x))
 2. \<And>x. \<lbrakk>A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> (\<forall>y\<in>A. y \<le> x) = (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>A \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> (\<forall>y\<in>A. y \<le> x) = (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)
 2. \<lbrakk>A \<noteq> {}; finite A; \<And>x. (\<forall>y\<in>A. y \<le> x) = (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)\<rbrakk> \<Longrightarrow> (THE x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)) = (THE x. x \<in> A \<and> (\<forall>y\<in>A. y \<le> x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; finite A; \<And>x. (\<forall>y\<in>A. y \<le> x) = (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)\<rbrakk> \<Longrightarrow> (THE x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> y \<le> x)) = (THE x. x \<in> A \<and> (\<forall>y\<in>A. y \<le> x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wellorder_Max_lemma: "\<lbrakk> k \<in> A; finite A \<rbrakk> \<Longrightarrow> Max A \<in> A \<and> k \<le> Max A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> A; finite A\<rbrakk> \<Longrightarrow> Max A \<in> A \<and> k \<le> Max A
[PROOF STEP]
by (case_tac "A = {}", simp_all)


[STATEMENT]
lemma MaxI2_order: "\<lbrakk> k \<in> A; finite A; \<And>y. y \<in> A \<Longrightarrow> y \<le> k;
  \<And>x. \<lbrakk> x \<in> A; \<forall>y\<in>A. y \<le> x \<rbrakk> \<Longrightarrow> P x \<rbrakk>
  \<Longrightarrow> P (Max A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<in> A; finite A; \<And>y. y \<in> A \<Longrightarrow> y \<le> k; \<And>x. \<lbrakk>x \<in> A; \<forall>y\<in>A. y \<le> x\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P (Max A)
[PROOF STEP]
by (simp add: Max_equality)


[STATEMENT]
lemma Min_le_Max: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> Min A \<le> Max A
[PROOF STEP]
by (rule Max_ge[OF _ Min_in])


[STATEMENT]
lemma iMin_le_Max: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> iMin A \<le> Max A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> iMin A \<le> Max A
[PROOF STEP]
by (rule ssubst[OF iMin_Min_conv], assumption+, rule Min_le_Max)


[STATEMENT]
lemma iMax_finite_conv: "finite I = (iMax I \<noteq> \<infinity>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite I = (iMax I \<noteq> \<infinity>)
[PROOF STEP]
by (simp add: iMax_def)


[STATEMENT]
lemma iMax_infinite_conv: "infinite I = (iMax I = \<infinity>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite I = (iMax I = \<infinity>)
[PROOF STEP]
by (simp add: iMax_def)


[STATEMENT]
lemma "class.distrib_lattice (min::('a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)) (\<le>) (<) max"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (subgoal_tac "class.order (\<le>) (<)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
 2. class.order (\<le>) (<)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.order (\<le>) (<)
 2. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule class.order.intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. class.preorder (\<le>) (<)
 2. class.order_axioms (\<le>)
 3. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule class.preorder.intro)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y. (x < y) = (x \<le> y \<and> \<not> y \<le> x)
 2. \<And>x. x \<le> x
 3. \<And>x y z. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z
 4. class.order_axioms (\<le>)
 5. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule less_le_not_le)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<le> x
 2. \<And>x y z. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z
 3. class.order_axioms (\<le>)
 4. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule order_refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z
 2. class.order_axioms (\<le>)
 3. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule order_trans, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.order_axioms (\<le>)
 2. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule class.order_axioms.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y
 2. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule order_antisym, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.order (\<le>) (<) \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (subgoal_tac "class.linorder (\<le>) (<)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
 2. class.order (\<le>) (<) \<Longrightarrow> class.linorder (\<le>) (<)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.order (\<le>) (<) \<Longrightarrow> class.linorder (\<le>) (<)
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule class.linorder.intro, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. class.order (\<le>) (<) \<Longrightarrow> class.linorder_axioms (\<le>)
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule class.linorder_axioms.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. class.order (\<le>) (<) \<Longrightarrow> x \<le> y \<or> y \<le> x
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule linorder_class.linear)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice min (\<le>) (<) max
[PROOF STEP]
apply (rule class.distrib_lattice.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.lattice min (\<le>) (<) max
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule class.lattice.intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_inf min (\<le>) (<)
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_sup max (\<le>) (<)
 3. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule class.semilattice_inf.intro, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_inf_axioms min (\<le>)
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_sup max (\<le>) (<)
 3. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule class.semilattice_inf_axioms.intro)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> min x y \<le> x
 2. \<And>x y. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> min x y \<le> y
 3. \<And>x y z. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<); x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> min y z
 4. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_sup max (\<le>) (<)
 5. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule le_minI1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> min x y \<le> y
 2. \<And>x y z. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<); x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> min y z
 3. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_sup max (\<le>) (<)
 4. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule le_minI2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<); x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> min y z
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_sup max (\<le>) (<)
 3. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule conj_le_imp_min, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_sup max (\<le>) (<)
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule class.semilattice_sup.intro, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.semilattice_sup_axioms max (\<le>)
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule class.semilattice_sup_axioms.intro)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> x \<le> max x y
 2. \<And>y x. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> y \<le> max x y
 3. \<And>y x z. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<); y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> max y z \<le> x
 4. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule max.cobounded1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y x. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> y \<le> max x y
 2. \<And>y x z. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<); y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> max y z \<le> x
 3. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule max.cobounded2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y x z. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<); y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> max y z \<le> x
 2. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule conj_le_imp_max, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> class.distrib_lattice_axioms min max
[PROOF STEP]
apply (rule class.distrib_lattice_axioms.intro)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>class.order (\<le>) (<); class.linorder (\<le>) (<)\<rbrakk> \<Longrightarrow> max x (min y z) = min (max x y) (max x z)
[PROOF STEP]
apply (rule max_min_distrib2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma max_Min_eq_Min_max[rule_format]: "
  finite A \<Longrightarrow>
  A \<noteq> {} \<longrightarrow>
  max x (Min A) = Min {max x a |a. a \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> A \<noteq> {} \<longrightarrow> max x (Min A) = Min {max x a |a. a \<in> A}
[PROOF STEP]
apply (rule finite.induct[of A], simp_all del: insert_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Aa a. \<lbrakk>finite A; finite Aa; Aa \<noteq> {} \<longrightarrow> max x (Min Aa) = Min {max x a |a. a \<in> Aa}\<rbrakk> \<Longrightarrow> max x (Min (insert a Aa)) = Min {max x aa |aa. aa \<in> insert a Aa}
[PROOF STEP]
apply (rename_tac A1 a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; A1 \<noteq> {} \<longrightarrow> max x (Min A1) = Min {max x a |a. a \<in> A1}\<rbrakk> \<Longrightarrow> max x (Min (insert a A1)) = Min {max x aa |aa. aa \<in> insert a A1}
[PROOF STEP]
apply (case_tac "A1 = {}", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; A1 \<noteq> {} \<longrightarrow> max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}\<rbrakk> \<Longrightarrow> max x (Min (insert a A1)) = Min {max x aa |aa. aa \<in> insert a A1}
[PROOF STEP]
apply (rule_tac
  t="{max x b |b. b \<in> insert a A1}" and
  s="insert (max x a) {max x b |b. b \<in> A1}"
  in subst)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; A1 \<noteq> {} \<longrightarrow> max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}\<rbrakk> \<Longrightarrow> insert (max x a) {max x b |b. b \<in> A1} = {max x b |b. b \<in> insert a A1}
 2. \<And>A1 a. \<lbrakk>finite A; finite A1; A1 \<noteq> {} \<longrightarrow> max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}\<rbrakk> \<Longrightarrow> max x (Min (insert a A1)) = Min (insert (max x a) {max x b |b. b \<in> A1})
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; A1 \<noteq> {} \<longrightarrow> max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}\<rbrakk> \<Longrightarrow> max x (Min (insert a A1)) = Min (insert (max x a) {max x b |b. b \<in> A1})
[PROOF STEP]
apply (subst Min_insert, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
[PROOF STEP]
apply (case_tac "a \<le> Min A1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}; a \<le> Min A1\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
 2. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}; \<not> a \<le> Min A1\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
[PROOF STEP]
apply (frule max_le_monoR[where x=x])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}; a \<le> Min A1; max x a \<le> max x (Min A1)\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
 2. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}; \<not> a \<le> Min A1\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
[PROOF STEP]
apply (simp only: min_eqL)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}; \<not> a \<le> Min A1\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
[PROOF STEP]
apply (simp only: linorder_not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}; Min A1 < a\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
[PROOF STEP]
apply (frule max_le_monoR[where x=x, OF less_imp_le])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A1 a. \<lbrakk>finite A; finite A1; max x (Min A1) = Min {max x a |a. a \<in> A1}; A1 \<noteq> {}; Min A1 < a; max x (Min A1) \<le> max x a\<rbrakk> \<Longrightarrow> max x (min a (Min A1)) = min (max x a) (Min {max x b |b. b \<in> A1})
[PROOF STEP]
apply (simp only: min_eqR)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma max_iMin_eq_iMin_max: "
  \<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow>
  max x (iMin A) = iMin {max x a |a. a \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> max x (iMin A) = iMin {max x a |a. a \<in> A}
[PROOF STEP]
apply (simp add: iMin_Min_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> max x (Min A) = Min {max x a |a. a \<in> A}
[PROOF STEP]
apply (insert iMin_Min_conv[of "{max x a |a. a \<in> A}"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; iMin {max x a |a. a \<in> A} = Min {max x a |a. a \<in> A}\<rbrakk> \<Longrightarrow> max x (Min A) = Min {max x a |a. a \<in> A}
[PROOF STEP]
apply (subgoal_tac "finite {max x a |a. a \<in> A}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite A; A \<noteq> {}; iMin {max x a |a. a \<in> A} = Min {max x a |a. a \<in> A}; finite {max x a |a. a \<in> A}\<rbrakk> \<Longrightarrow> max x (Min A) = Min {max x a |a. a \<in> A}
 2. \<lbrakk>finite A; A \<noteq> {}; iMin {max x a |a. a \<in> A} = Min {max x a |a. a \<in> A}\<rbrakk> \<Longrightarrow> finite {max x a |a. a \<in> A}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite A; A \<noteq> {}; iMin {max x a |a. a \<in> A} = Min {max x a |a. a \<in> A}\<rbrakk> \<Longrightarrow> finite {max x a |a. a \<in> A}
 2. \<lbrakk>finite A; A \<noteq> {}; iMin {max x a |a. a \<in> A} = Min {max x a |a. a \<in> A}; finite {max x a |a. a \<in> A}\<rbrakk> \<Longrightarrow> max x (Min A) = Min {max x a |a. a \<in> A}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; iMin {max x a |a. a \<in> A} = Min {max x a |a. a \<in> A}; finite {max x a |a. a \<in> A}\<rbrakk> \<Longrightarrow> max x (Min A) = Min {max x a |a. a \<in> A}
[PROOF STEP]
apply (simp add: max_Min_eq_Min_max)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "\<lbrakk> finite A; A \<noteq>{} \<rbrakk> \<Longrightarrow> \<forall>x\<in>A. x \<le> Max A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>A. x \<le> Max A
[PROOF STEP]
by simp


[STATEMENT]
lemma iMin_subset: "\<lbrakk> A \<noteq> {}; A \<subseteq> B \<rbrakk> \<Longrightarrow> iMin B \<le> iMin A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; A \<subseteq> B\<rbrakk> \<Longrightarrow> iMin B \<le> iMin A
[PROOF STEP]
by (blast intro: iMin_le iMinI_ex2)


[STATEMENT]
lemma Max_subset: "\<lbrakk> A \<noteq> {}; A \<subseteq> B; finite B \<rbrakk> \<Longrightarrow> Max A \<le> Max B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> Max A \<le> Max B
[PROOF STEP]
by (rule linorder_class.Max_mono)


[STATEMENT]
lemma Min_subset: "\<lbrakk> A \<noteq> {}; A \<subseteq> B; finite B \<rbrakk> \<Longrightarrow> Min B \<le> Min A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> Min B \<le> Min A
[PROOF STEP]
by (rule linorder_class.Min_antimono)


[STATEMENT]
lemma iMin_Int_ge1: "(A \<inter> B) \<noteq> {} \<Longrightarrow> iMin A \<le> iMin (A \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> iMin A \<le> iMin (A \<inter> B)
[PROOF STEP]
by (rule iMin_subset[OF _ Int_lower1])


[STATEMENT]
lemma iMin_Int_ge2: "(A \<inter> B) \<noteq> {} \<Longrightarrow> iMin B \<le> iMin (A \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> iMin B \<le> iMin (A \<inter> B)
[PROOF STEP]
by (rule iMin_subset[OF _ Int_lower2])


[STATEMENT]
lemma iMin_Int_ge: "(A \<inter> B) \<noteq> {} \<Longrightarrow> max (iMin A) (iMin B) \<le> iMin (A \<inter> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> max (iMin A) (iMin B) \<le> iMin (A \<inter> B)
[PROOF STEP]
apply (rule conj_le_imp_max)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> iMin A \<le> iMin (A \<inter> B)
 2. A \<inter> B \<noteq> {} \<Longrightarrow> iMin B \<le> iMin (A \<inter> B)
[PROOF STEP]
apply (rule iMin_Int_ge1, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> iMin B \<le> iMin (A \<inter> B)
[PROOF STEP]
apply (rule iMin_Int_ge2, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Max_Int_le1: "\<lbrakk> (A \<inter> B) \<noteq> {}; finite A \<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> Max A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B \<noteq> {}; finite A\<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> Max A
[PROOF STEP]
by (rule Max_subset[OF _ Int_lower1])


[STATEMENT]
lemma Max_Int_le2: "\<lbrakk> (A \<inter> B) \<noteq> {}; finite B \<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> Max B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B \<noteq> {}; finite B\<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> Max B
[PROOF STEP]
by (rule Max_subset[OF _ Int_lower2])


[STATEMENT]
lemma Max_Int_le: "\<lbrakk> (A \<inter> B) \<noteq> {}; finite A; finite B \<rbrakk> \<Longrightarrow>
  Max (A \<inter> B) \<le> min (Max A) (Max B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B \<noteq> {}; finite A; finite B\<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> min (Max A) (Max B)
[PROOF STEP]
apply (rule conj_le_imp_min)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<inter> B \<noteq> {}; finite A; finite B\<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> Max A
 2. \<lbrakk>A \<inter> B \<noteq> {}; finite A; finite B\<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> Max B
[PROOF STEP]
apply (rule Max_Int_le1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B \<noteq> {}; finite A; finite B\<rbrakk> \<Longrightarrow> Max (A \<inter> B) \<le> Max B
[PROOF STEP]
apply (rule Max_Int_le2, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMin_Un[rule_format]: "
  \<lbrakk> A \<noteq> {}; B \<noteq> {} \<rbrakk> \<Longrightarrow>
  iMin (A \<union> B) = min (iMin A) (iMin B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> iMin (A \<union> B) = min (iMin A) (iMin B)
[PROOF STEP]
apply (rule order_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> iMin (A \<union> B) \<le> min (iMin A) (iMin B)
 2. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> min (iMin A) (iMin B) \<le> iMin (A \<union> B)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> iMin (A \<union> B) \<le> iMin A \<and> iMin (A \<union> B) \<le> iMin B
 2. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> min (iMin A) (iMin B) \<le> iMin (A \<union> B)
[PROOF STEP]
apply (blast intro: iMin_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> min (iMin A) (iMin B) \<le> iMin (A \<union> B)
[PROOF STEP]
apply (simp add: min_le_iff_disj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> iMin A \<le> iMin (A \<union> B) \<or> iMin B \<le> iMin (A \<union> B)
[PROOF STEP]
apply (insert iMinI_ex2[of "A\<union>B"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<noteq> {}; B \<noteq> {}; A \<union> B \<noteq> {} \<Longrightarrow> iMin (A \<union> B) \<in> A \<union> B\<rbrakk> \<Longrightarrow> iMin A \<le> iMin (A \<union> B) \<or> iMin B \<le> iMin (A \<union> B)
[PROOF STEP]
apply (blast intro: iMin_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMin_singleton[simp]: "iMin {a} = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMin {a} = a
[PROOF STEP]
by (rule singletonI[THEN iMinI, THEN singletonD])


[STATEMENT]
lemma iMax_singleton[simp]: "iMax {a} = enat a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMax {a} = enat a
[PROOF STEP]
by (simp add: iMax_def)


[STATEMENT]
lemma Max_le_Min_imp_singleton: "
  \<lbrakk> finite A; A \<noteq> {}; Max A \<le> Min A \<rbrakk> \<Longrightarrow> A = {Min A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A\<rbrakk> \<Longrightarrow> A = {Min A}
[PROOF STEP]
apply (frule Max_le_iff[THEN iffD1, of _ "Min A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A; \<forall>a\<in>A. a \<le> Min A\<rbrakk> \<Longrightarrow> A = {Min A}
[PROOF STEP]
apply (frule Min_ge_iff[THEN iffD1, of _ "Min A"], assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A; \<forall>a\<in>A. a \<le> Min A; \<forall>a\<in>A. Min A \<le> a\<rbrakk> \<Longrightarrow> A = {Min A}
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A; \<forall>a\<in>A. a \<le> Min A; \<forall>a\<in>A. Min A \<le> a\<rbrakk> \<Longrightarrow> (x \<in> A) = (x \<in> {Min A})
[PROOF STEP]
apply (unfold Ball_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A; \<forall>x. x \<in> A \<longrightarrow> x \<le> Min A; \<forall>x. x \<in> A \<longrightarrow> Min A \<le> x\<rbrakk> \<Longrightarrow> (x \<in> A) = (x \<in> {Min A})
[PROOF STEP]
apply (erule_tac x=x in allE, erule_tac x=x in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A; x \<in> A \<longrightarrow> x \<le> Min A; x \<in> A \<longrightarrow> Min A \<le> x\<rbrakk> \<Longrightarrow> (x \<in> A) = (x \<in> {Min A})
[PROOF STEP]
apply (blast intro: order_antisym Min_in)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Max_le_Min_conv_singleton: "
  \<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> Min A) = (\<exists>x. A = {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> (Max A \<le> Min A) = (\<exists>x. A = {x})
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A\<rbrakk> \<Longrightarrow> \<exists>x. A = {x}
 2. \<lbrakk>finite A; A \<noteq> {}; \<exists>x. A = {x}\<rbrakk> \<Longrightarrow> Max A \<le> Min A
[PROOF STEP]
apply (rule_tac x="Min A" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite A; A \<noteq> {}; Max A \<le> Min A\<rbrakk> \<Longrightarrow> A = {Min A}
 2. \<lbrakk>finite A; A \<noteq> {}; \<exists>x. A = {x}\<rbrakk> \<Longrightarrow> Max A \<le> Min A
[PROOF STEP]
apply (rule Max_le_Min_imp_singleton, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; \<exists>x. A = {x}\<rbrakk> \<Longrightarrow> Max A \<le> Min A
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Max_le_iMin_imp_le: "
  \<lbrakk> finite A; Max A \<le> iMin B; a \<in> A; b \<in> B \<rbrakk> \<Longrightarrow> a \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A \<le> iMin B; a \<in> A; b \<in> B\<rbrakk> \<Longrightarrow> a \<le> b
[PROOF STEP]
by (blast dest: Max_ge intro: order_trans)


[STATEMENT]
lemma le_imp_Max_le_iMin: "
  \<lbrakk> finite A; A \<noteq> {}; B \<noteq> {}; \<forall>a\<in>A. \<forall>b\<in>B. a \<le> b \<rbrakk> \<Longrightarrow> Max A \<le> iMin B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; B \<noteq> {}; \<forall>a\<in>A. \<forall>b\<in>B. a \<le> b\<rbrakk> \<Longrightarrow> Max A \<le> iMin B
[PROOF STEP]
by (blast intro: Max_in iMinI_ex2)


[STATEMENT]
lemma Max_le_iMin_conv_le: "
  \<lbrakk> finite A; A \<noteq> {}; B \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> iMin B) = (\<forall>a\<in>A. \<forall>b\<in>B. a \<le> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> (Max A \<le> iMin B) = (\<forall>a\<in>A. \<forall>b\<in>B. a \<le> b)
[PROOF STEP]
by (blast intro: Max_le_iMin_imp_le le_imp_Max_le_iMin)


[STATEMENT]
lemma Max_less_iMin_imp_less: "
  \<lbrakk> finite A; Max A < iMin B; a \<in> A; b \<in> B \<rbrakk> \<Longrightarrow> a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < iMin B; a \<in> A; b \<in> B\<rbrakk> \<Longrightarrow> a < b
[PROOF STEP]
by (blast dest: Max_less_iff intro: order_less_le_trans iMin_le)


[STATEMENT]
lemma less_imp_Max_less_iMin: "
  \<lbrakk> finite A; A \<noteq> {}; B \<noteq> {}; \<forall>a\<in>A. \<forall>b\<in>B. a < b \<rbrakk> \<Longrightarrow> Max A < iMin B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}; B \<noteq> {}; \<forall>a\<in>A. \<forall>b\<in>B. a < b\<rbrakk> \<Longrightarrow> Max A < iMin B
[PROOF STEP]
by (blast intro: Max_in iMinI_ex2)