theory Lib

lemma set_has_max:
  fixes ls :: "('a :: linorder) list"
  assumes ls: "ls \<noteq> []"
  shows "\<exists>max \<in> set ls. \<forall>z \<in> set ls. z \<le> max" using ls proof (induct ls) case Nil thus ?case by simp next case (Cons l ls) show ?case proof (cases "ls = []") case True thus ?thesis by simp next case False then obtain max where mv: "max \<in> set ls" and mm: "\<forall>z \<in> set ls. z \<le> max" using Cons.hyps by auto show ?thesis proof (cases "max \<le> l") case True have "l \<in> set (l # ls)" by simp thus ?thesis proof from mm show "\<forall>z \<in> set (l # ls). z \<le> l" using True by auto qed next case False from mv have "max \<in> set (l # ls)" by simp thus ?thesis proof from mm show "\<forall>z \<in> set (l # ls). z \<le> max" using False by auto qed qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max proof (prove)
using this:
ls \<noteq> []

goal (1 subgoal):
 1. \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max proof (state)
goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> \<exists>max\<in>set []. \<forall>z\<in>set []. z \<le> max
 2. \<And>a ls. \<lbrakk>ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max; a # ls \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>max\<in>set (a # ls). \<forall>z\<in>set (a # ls). z \<le> max proof (state)
this:
[] \<noteq> []

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> \<exists>max\<in>set []. \<forall>z\<in>set []. z \<le> max
 2. \<And>a ls. \<lbrakk>ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max; a # ls \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>max\<in>set (a # ls). \<forall>z\<in>set (a # ls). z \<le> max proof (prove)
using this:
[] \<noteq> []

goal (1 subgoal):
 1. \<exists>max\<in>set []. \<forall>z\<in>set []. z \<le> max proof (state)
this:
\<exists>max\<in>set []. \<forall>z\<in>set []. z \<le> max

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max; a # ls \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>max\<in>set (a # ls). \<forall>z\<in>set (a # ls). z \<le> max proof (state)
goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max; a # ls \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>max\<in>set (a # ls). \<forall>z\<in>set (a # ls). z \<le> max proof (state)
this:
ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max
l # ls \<noteq> []

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max; a # ls \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>max\<in>set (a # ls). \<forall>z\<in>set (a # ls). z \<le> max proof (prove)
goal (1 subgoal):
 1. \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
goal (2 subgoals):
 1. ls = [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max
 2. ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
this:
ls = []

goal (2 subgoals):
 1. ls = [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max
 2. ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (prove)
using this:
ls = []

goal (1 subgoal):
 1. \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
this:
\<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max

goal (1 subgoal):
 1. ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
goal (1 subgoal):
 1. ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
this:
ls \<noteq> []

goal (1 subgoal):
 1. ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (chain)
picking this:
ls \<noteq> [] proof (prove)
using this:
ls \<noteq> []

goal (1 subgoal):
 1. (\<And>max. \<lbrakk>max \<in> set ls; \<forall>z\<in>set ls. z \<le> max\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
ls \<noteq> []
ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set ls. \<forall>z\<in>set ls. z \<le> max

goal (1 subgoal):
 1. (\<And>max. \<lbrakk>max \<in> set ls; \<forall>z\<in>set ls. z \<le> max\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
max \<in> set ls
\<forall>z\<in>set ls. z \<le> max

goal (1 subgoal):
 1. ls \<noteq> [] \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (prove)
goal (1 subgoal):
 1. \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
goal (2 subgoals):
 1. max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max
 2. \<not> max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
this:
max \<le> l

goal (2 subgoals):
 1. max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max
 2. \<not> max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (prove)
goal (1 subgoal):
 1. l \<in> set (l # ls) proof (state)
this:
l \<in> set (l # ls)

goal (2 subgoals):
 1. max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max
 2. \<not> max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (prove)
using this:
l \<in> set (l # ls)

goal (1 subgoal):
 1. \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
goal (1 subgoal):
 1. \<forall>z\<in>set (l # ls). z \<le> l proof (chain)
picking this:
\<forall>z\<in>set ls. z \<le> max proof (prove)
using this:
\<forall>z\<in>set ls. z \<le> max

goal (1 subgoal):
 1. \<forall>z\<in>set (l # ls). z \<le> l proof (prove)
using this:
\<forall>z\<in>set ls. z \<le> max
max \<le> l

goal (1 subgoal):
 1. \<forall>z\<in>set (l # ls). z \<le> l proof (state)
this:
\<forall>z\<in>set (l # ls). z \<le> l

goal:
No subgoals! proof (state)
this:
\<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max

goal (1 subgoal):
 1. \<not> max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
goal (1 subgoal):
 1. \<not> max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
this:
\<not> max \<le> l

goal (1 subgoal):
 1. \<not> max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (chain)
picking this:
max \<in> set ls proof (prove)
using this:
max \<in> set ls

goal (1 subgoal):
 1. max \<in> set (l # ls) proof (state)
this:
max \<in> set (l # ls)

goal (1 subgoal):
 1. \<not> max \<le> l \<Longrightarrow> \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (prove)
using this:
max \<in> set (l # ls)

goal (1 subgoal):
 1. \<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max proof (state)
goal (1 subgoal):
 1. \<forall>z\<in>set (l # ls). z \<le> max proof (chain)
picking this:
\<forall>z\<in>set ls. z \<le> max proof (prove)
using this:
\<forall>z\<in>set ls. z \<le> max

goal (1 subgoal):
 1. \<forall>z\<in>set (l # ls). z \<le> max proof (prove)
using this:
\<forall>z\<in>set ls. z \<le> max
\<not> max \<le> l

goal (1 subgoal):
 1. \<forall>z\<in>set (l # ls). z \<le> max proof (state)
this:
\<forall>z\<in>set (l # ls). z \<le> max

goal:
No subgoals! proof (state)
this:
\<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max

goal:
No subgoals! proof (state)
this:
\<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max

goal:
No subgoals! proof (state)
this:
\<exists>max\<in>set (l # ls). \<forall>z\<in>set (l # ls). z \<le> max

goal:
No subgoals!