theory Even_More_List

lemma Min_eq_length_takeWhile:
  \<open>Min {m. P m} = length (takeWhile (Not \<circ> P) ([0..<n]))\<close>
  if *: \<open>\<And>m. P m \<Longrightarrow> m < n\<close> and \<open>\<exists>m. P m\<close> proof - from \<open>\<exists>m. P m\<close> obtain r where \<open>P r\<close> .. have \<open>Min {m. P m} = q + length (takeWhile (Not \<circ> P) ([q..<n]))\<close>
    if \<open>q \<le> n\<close> \<open>\<And>m. P m \<Longrightarrow> q \<le> m \<and> m < n\<close> for q using that proof (induction rule: inc_induct) case base from base [of r] \<open>P r\<close> show ?case by simp next case (step q) from \<open>q < n\<close> have *: \<open>[q..<n] = q # [Suc q..<n]\<close> by (simp add: upt_rec) show ?case proof (cases \<open>P q\<close>) case False then have \<open>Suc q \<le> m \<and> m < n\<close> if \<open>P m\<close> for m using that step.prems [of m] by (auto simp add: Suc_le_eq less_le) with \<open>\<not> P q\<close> show ?thesis by (simp add: * step.IH) next case True have \<open>{a. P a} \<subseteq> {0..n}\<close> using step.prems by (auto simp add: less_imp_le_nat) moreover have \<open>finite {0..n}\<close> by simp ultimately have \<open>finite {a. P a}\<close> by (rule finite_subset) with \<open>P q\<close> step.prems show ?thesis by (auto intro: Min_eqI simp add: *) qed qed from this [of 0] and that show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Min {m. P m} = length (takeWhile (Not \<circ> P) [0..<n]) proof (state)
goal (1 subgoal):
 1. Min {m. P m} = length (takeWhile (Not \<circ> P) [0..<n]) proof (chain)
picking this:
\<exists>m. P m proof (prove)
using this:
\<exists>m. P m

goal (1 subgoal):
 1. (\<And>r. P r \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
P r

goal (1 subgoal):
 1. Min {m. P m} = length (takeWhile (Not \<circ> P) [0..<n]) proof (prove)
goal (1 subgoal):
 1. Min {m. P m} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (prove)
using this:
q \<le> n
P ?m \<Longrightarrow> q \<le> ?m \<and> ?m < n

goal (1 subgoal):
 1. Min {m. P m} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
goal (2 subgoals):
 1. (\<And>m. P m \<Longrightarrow> n \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = n + length (takeWhile (Not \<circ> P) [n..<n])
 2. \<And>na. \<lbrakk>q \<le> na; na < n; (\<And>m. P m \<Longrightarrow> Suc na \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = Suc na + length (takeWhile (Not \<circ> P) [Suc na..<n]); \<And>m. P m \<Longrightarrow> na \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min (Collect P) = na + length (takeWhile (Not \<circ> P) [na..<n]) proof (state)
this:
P ?m \<Longrightarrow> n \<le> ?m \<and> ?m < n

goal (2 subgoals):
 1. (\<And>m. P m \<Longrightarrow> n \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = n + length (takeWhile (Not \<circ> P) [n..<n])
 2. \<And>na. \<lbrakk>q \<le> na; na < n; (\<And>m. P m \<Longrightarrow> Suc na \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = Suc na + length (takeWhile (Not \<circ> P) [Suc na..<n]); \<And>m. P m \<Longrightarrow> na \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min (Collect P) = na + length (takeWhile (Not \<circ> P) [na..<n]) proof (chain)
picking this:
P r \<Longrightarrow> n \<le> r \<and> r < n
P r proof (prove)
using this:
P r \<Longrightarrow> n \<le> r \<and> r < n
P r

goal (1 subgoal):
 1. Min {a. P a} = n + length (takeWhile (Not \<circ> P) [n..<n]) proof (state)
this:
Min {a. P a} = n + length (takeWhile (Not \<circ> P) [n..<n])

goal (1 subgoal):
 1. \<And>na. \<lbrakk>q \<le> na; na < n; (\<And>m. P m \<Longrightarrow> Suc na \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = Suc na + length (takeWhile (Not \<circ> P) [Suc na..<n]); \<And>m. P m \<Longrightarrow> na \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min (Collect P) = na + length (takeWhile (Not \<circ> P) [na..<n]) proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>q \<le> na; na < n; (\<And>m. P m \<Longrightarrow> Suc na \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = Suc na + length (takeWhile (Not \<circ> P) [Suc na..<n]); \<And>m. P m \<Longrightarrow> na \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min (Collect P) = na + length (takeWhile (Not \<circ> P) [na..<n]) proof (state)
this:
q__ \<le> q
q < n
(\<And>m. P m \<Longrightarrow> Suc q \<le> m \<and> m < n) \<Longrightarrow> Min {a. P a} = Suc q + length (takeWhile (Not \<circ> P) [Suc q..<n])
P ?m \<Longrightarrow> q \<le> ?m \<and> ?m < n

goal (1 subgoal):
 1. \<And>na. \<lbrakk>q__ \<le> na; na < n; (\<And>m. P m \<Longrightarrow> Suc na \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = Suc na + length (takeWhile (Not \<circ> P) [Suc na..<n]); \<And>m. P m \<Longrightarrow> na \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min (Collect P) = na + length (takeWhile (Not \<circ> P) [na..<n]) proof (chain)
picking this:
q < n proof (prove)
using this:
q < n

goal (1 subgoal):
 1. [q..<n] = q # [Suc q..<n] proof (state)
this:
[q..<n] = q # [Suc q..<n]

goal (1 subgoal):
 1. \<And>na. \<lbrakk>q__ \<le> na; na < n; (\<And>m. P m \<Longrightarrow> Suc na \<le> m \<and> m < n) \<Longrightarrow> Min (Collect P) = Suc na + length (takeWhile (Not \<circ> P) [Suc na..<n]); \<And>m. P m \<Longrightarrow> na \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min (Collect P) = na + length (takeWhile (Not \<circ> P) [na..<n]) proof (prove)
goal (1 subgoal):
 1. Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
goal (2 subgoals):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n])
 2. \<not> P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
this:
\<not> P q

goal (2 subgoals):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n])
 2. \<not> P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (chain)
picking this:
\<not> P q proof (prove)
using this:
\<not> P q

goal (1 subgoal):
 1. Suc q \<le> m \<and> m < n proof (prove)
using this:
\<not> P q
P m
P m \<Longrightarrow> q \<le> m \<and> m < n

goal (1 subgoal):
 1. Suc q \<le> m \<and> m < n proof (state)
this:
P ?m \<Longrightarrow> Suc q \<le> ?m \<and> ?m < n

goal (2 subgoals):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n])
 2. \<not> P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (chain)
picking this:
\<not> P q
P ?m \<Longrightarrow> Suc q \<le> ?m \<and> ?m < n proof (prove)
using this:
\<not> P q
P ?m \<Longrightarrow> Suc q \<le> ?m \<and> ?m < n

goal (1 subgoal):
 1. Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
this:
Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n])

goal (1 subgoal):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
goal (1 subgoal):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
this:
P q

goal (1 subgoal):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (prove)
goal (1 subgoal):
 1. {a. P a} \<subseteq> {0..n} proof (prove)
using this:
P ?m \<Longrightarrow> q \<le> ?m \<and> ?m < n

goal (1 subgoal):
 1. {a. P a} \<subseteq> {0..n} proof (state)
this:
{a. P a} \<subseteq> {0..n}

goal (1 subgoal):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
this:
{a. P a} \<subseteq> {0..n}

goal (1 subgoal):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (prove)
goal (1 subgoal):
 1. finite {0..n} proof (state)
this:
finite {0..n}

goal (1 subgoal):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (chain)
picking this:
{a. P a} \<subseteq> {0..n}
finite {0..n} proof (prove)
using this:
{a. P a} \<subseteq> {0..n}
finite {0..n}

goal (1 subgoal):
 1. finite {a. P a} proof (state)
this:
finite {a. P a}

goal (1 subgoal):
 1. P q \<Longrightarrow> Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (chain)
picking this:
P q
P ?m \<Longrightarrow> q \<le> ?m \<and> ?m < n
finite {a. P a} proof (prove)
using this:
P q
P ?m \<Longrightarrow> q \<le> ?m \<and> ?m < n
finite {a. P a}

goal (1 subgoal):
 1. Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n]) proof (state)
this:
Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n])

goal:
No subgoals! proof (state)
this:
Min {a. P a} = q + length (takeWhile (Not \<circ> P) [q..<n])

goal:
No subgoals! proof (state)
this:
\<lbrakk>?q \<le> n; \<And>m. P m \<Longrightarrow> ?q \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min {m. P m} = ?q + length (takeWhile (Not \<circ> P) [?q..<n])

goal (1 subgoal):
 1. Min {m. P m} = length (takeWhile (Not \<circ> P) [0..<n]) proof (chain)
picking this:
\<lbrakk>0 \<le> n; \<And>m. P m \<Longrightarrow> 0 \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min {m. P m} = 0 + length (takeWhile (Not \<circ> P) [0..<n])
P ?m \<Longrightarrow> ?m < n
\<exists>m. P m proof (prove)
using this:
\<lbrakk>0 \<le> n; \<And>m. P m \<Longrightarrow> 0 \<le> m \<and> m < n\<rbrakk> \<Longrightarrow> Min {m. P m} = 0 + length (takeWhile (Not \<circ> P) [0..<n])
P ?m \<Longrightarrow> ?m < n
\<exists>m. P m

goal (1 subgoal):
 1. Min {m. P m} = length (takeWhile (Not \<circ> P) [0..<n]) proof (state)
this:
Min {m. P m} = length (takeWhile (Not \<circ> P) [0..<n])

goal:
No subgoals!