theory Many_More

lemma MinI:
  assumes fa: "finite A"
  and     ne: "A \<noteq> {}"
  and     xv: "m \<in> A"
  and    min: "\<forall>y \<in> A. m \<le> y"
  shows "Min A = m" using fa ne xv min proof (induct A arbitrary: m rule: finite_ne_induct) case singleton then show ?case by simp next case (insert y F) from insert.prems have yx: "m \<le> y" and fx: "\<forall>y \<in> F. m \<le> y" by auto have "m \<in> insert y F" by fact then show ?case proof assume mv: "m = y" have mlt: "m \<le> Min F" by (rule iffD2 [OF Min_ge_iff [OF insert.hyps(1) insert.hyps(2)] fx]) show ?case apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)]) apply (subst mv [symmetric]) apply (auto simp: min_def mlt) done next assume "m \<in> F" then have mf: "Min F = m" by (rule insert.hyps(4) [OF _ fx]) show ?case apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)]) apply (subst mf) apply (rule iffD2 [OF _ yx]) apply (auto simp: min_def) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Min A = m proof (prove)
using this:
finite A
A \<noteq> {}
m \<in> A
\<forall>y\<in>A. m \<le> y

goal (1 subgoal):
 1. Min A = m proof (state)
goal (2 subgoals):
 1. \<And>x m. \<lbrakk>m \<in> {x}; Ball {x} ((\<le>) m)\<rbrakk> \<Longrightarrow> Min {x} = m
 2. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m proof (state)
this:
m \<in> {x_}
\<forall>a\<in>{x_}. m \<le> a

goal (2 subgoals):
 1. \<And>x m. \<lbrakk>m \<in> {x}; Ball {x} ((\<le>) m)\<rbrakk> \<Longrightarrow> Min {x} = m
 2. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m proof (chain)
picking this:
m \<in> {x_}
\<forall>a\<in>{x_}. m \<le> a proof (prove)
using this:
m \<in> {x_}
\<forall>a\<in>{x_}. m \<le> a

goal (1 subgoal):
 1. Min {x_} = m proof (state)
this:
Min {x_} = m

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m proof (state)
goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m proof (state)
this:
finite F
F \<noteq> {}
y \<notin> F
\<lbrakk>?m \<in> F; \<forall>a\<in>F. ?m \<le> a\<rbrakk> \<Longrightarrow> Min F = ?m
m \<in> insert y F
\<forall>a\<in>insert y F. m \<le> a

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m proof (chain)
picking this:
m \<in> insert y F
\<forall>a\<in>insert y F. m \<le> a proof (prove)
using this:
m \<in> insert y F
\<forall>a\<in>insert y F. m \<le> a

goal (1 subgoal):
 1. m \<le> y &&& \<forall>y\<in>F. m \<le> y proof (state)
this:
m \<le> y
\<forall>y\<in>F. m \<le> y

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m proof (prove)
goal (1 subgoal):
 1. m \<in> insert y F proof (state)
this:
m \<in> insert y F

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m proof (chain)
picking this:
m \<in> insert y F proof (prove)
using this:
m \<in> insert y F

goal (1 subgoal):
 1. Min (insert y F) = m proof (state)
goal (2 subgoals):
 1. m = y \<Longrightarrow> Min (insert y F) = m
 2. m \<in> F \<Longrightarrow> Min (insert y F) = m proof (state)
this:
m = y

goal (2 subgoals):
 1. m = y \<Longrightarrow> Min (insert y F) = m
 2. m \<in> F \<Longrightarrow> Min (insert y F) = m proof (prove)
goal (1 subgoal):
 1. m \<le> Min F proof (state)
this:
m \<le> Min F

goal (2 subgoals):
 1. m = y \<Longrightarrow> Min (insert y F) = m
 2. m \<in> F \<Longrightarrow> Min (insert y F) = m proof (prove)
goal (1 subgoal):
 1. Min (insert y F) = m proof (prove)
goal (1 subgoal):
 1. min y (Min F) = m proof (prove)
goal (1 subgoal):
 1. min m (Min F) = m proof (prove)
goal:
No subgoals! proof (state)
this:
Min (insert y F) = m

goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m proof (state)
goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m proof (state)
this:
m \<in> F

goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m proof (chain)
picking this:
m \<in> F proof (prove)
using this:
m \<in> F

goal (1 subgoal):
 1. Min F = m proof (state)
this:
Min F = m

goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m proof (prove)
goal (1 subgoal):
 1. Min (insert y F) = m proof (prove)
goal (1 subgoal):
 1. min y (Min F) = m proof (prove)
goal (1 subgoal):
 1. min y m = m proof (prove)
goal (1 subgoal):
 1. (min y m = m) = (m \<le> y) proof (prove)
goal:
No subgoals! proof (state)
this:
Min (insert y F) = m

goal:
No subgoals! proof (state)
this:
Min (insert y F) = m

goal:
No subgoals!