theory Lib

lemma Min_image_distrib:
  assumes minf: "\<And>x y. \<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> min (f x) (f y) = f (min x y)"
  and       fa: "finite A"
  and      ane: "A \<noteq> {}"
  shows "Min (f ` A) = f (Min A)" proof - have rl: "\<And>F. \<lbrakk> F \<subseteq> A; F \<noteq> {} \<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F)" proof - fix F assume fa: "F \<subseteq> A" and fne: "F \<noteq> {}" have "finite F" by (rule finite_subset) fact+ thus "?thesis F" unfolding min_def using fa fne fa proof (induct rule: finite_subset_induct) case empty thus ?case by simp next case (insert x F) thus ?case by (cases "F = {}") (auto dest: Min_in intro: minf) qed qed show ?thesis by (rule rl [OF order_refl]) fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Min (f ` A) = f (Min A) proof (state)
goal (1 subgoal):
 1. Min (f ` A) = f (Min A) proof (prove)
goal (1 subgoal):
 1. \<And>F. \<lbrakk>F \<subseteq> A; F \<noteq> {}\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F) proof (state)
goal (1 subgoal):
 1. \<And>F. \<lbrakk>F \<subseteq> A; F \<noteq> {}\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F) proof (state)
goal (1 subgoal):
 1. \<And>F. \<lbrakk>F \<subseteq> A; F \<noteq> {}\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F) proof (state)
this:
F \<subseteq> A
F \<noteq> {}

goal (1 subgoal):
 1. \<And>F. \<lbrakk>F \<subseteq> A; F \<noteq> {}\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F) proof (prove)
goal (1 subgoal):
 1. finite F proof (state)
this:
finite F

goal (1 subgoal):
 1. \<And>F. \<lbrakk>F \<subseteq> A; F \<noteq> {}\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F) proof (prove)
using this:
finite F

goal (1 subgoal):
 1. Min (f ` F) = f (Min F) proof (prove)
using this:
finite F

goal (1 subgoal):
 1. Min (f ` F) = f (Min F) proof (prove)
using this:
finite F
F \<subseteq> A
F \<noteq> {}
F \<subseteq> A

goal (1 subgoal):
 1. Min (f ` F) = f (Min F) proof (state)
goal (2 subgoals):
 1. \<lbrakk>{} \<noteq> {}; {} \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` {}) = f (Min {})
 2. \<And>a F. \<lbrakk>finite F; a \<in> A; a \<notin> F; \<lbrakk>F \<noteq> {}; F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F); insert a F \<noteq> {}; insert a F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` insert a F) = f (Min (insert a F)) proof (state)
this:
{} \<noteq> {}
{} \<subseteq> A

goal (2 subgoals):
 1. \<lbrakk>{} \<noteq> {}; {} \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` {}) = f (Min {})
 2. \<And>a F. \<lbrakk>finite F; a \<in> A; a \<notin> F; \<lbrakk>F \<noteq> {}; F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F); insert a F \<noteq> {}; insert a F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` insert a F) = f (Min (insert a F)) proof (prove)
using this:
{} \<noteq> {}
{} \<subseteq> A

goal (1 subgoal):
 1. Min (f ` {}) = f (Min {}) proof (state)
this:
Min (f ` {}) = f (Min {})

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> A; a \<notin> F; \<lbrakk>F \<noteq> {}; F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F); insert a F \<noteq> {}; insert a F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` insert a F) = f (Min (insert a F)) proof (state)
goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> A; a \<notin> F; \<lbrakk>F \<noteq> {}; F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F); insert a F \<noteq> {}; insert a F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` insert a F) = f (Min (insert a F)) proof (state)
this:
finite F
x \<in> A
x \<notin> F
\<lbrakk>F \<noteq> {}; F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F)
insert x F \<noteq> {}
insert x F \<subseteq> A

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> A; a \<notin> F; \<lbrakk>F \<noteq> {}; F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F); insert a F \<noteq> {}; insert a F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` insert a F) = f (Min (insert a F)) proof (prove)
using this:
finite F
x \<in> A
x \<notin> F
\<lbrakk>F \<noteq> {}; F \<subseteq> A\<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F)
insert x F \<noteq> {}
insert x F \<subseteq> A

goal (1 subgoal):
 1. Min (f ` insert x F) = f (Min (insert x F)) proof (state)
this:
Min (f ` insert x F) = f (Min (insert x F))

goal:
No subgoals! proof (state)
this:
Min (f ` F) = f (Min F)

goal:
No subgoals! proof (state)
this:
\<lbrakk>?F \<subseteq> A; ?F \<noteq> {}\<rbrakk> \<Longrightarrow> Min (f ` ?F) = f (Min ?F)

goal (1 subgoal):
 1. Min (f ` A) = f (Min A) proof (prove)
goal (1 subgoal):
 1. Min (f ` A) = f (Min A) proof (state)
this:
Min (f ` A) = f (Min A)

goal:
No subgoals!