theory in_range
imports Main Real

begin
type_synonym real_vector = "nat \<Rightarrow> real"

definition in_range ::
  "nat \<Rightarrow> nat \<Rightarrow> bool" where
  "in_range n i \<equiv> 1 \<le> i \<and> i \<le> n"

definition non_negative_real_vector ::
  "nat \<Rightarrow> real_vector \<Rightarrow> bool" where
  "non_negative_real_vector n v \<equiv> \<forall> i::nat . i \<in> {1..n} \<longrightarrow> v i \<ge> 0"

fun maximum ::
  "nat \<Rightarrow> real_vector \<Rightarrow> real" where
  "maximum 0 _ = 0" | (* In our setting with non-negative real numbers it makes sense to define the maximum of the empty set as 0 *)
  "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" (* we don't enforce that y is non-negative, but this computation only makes sense for a non-negative y *)

lemma maximum_sufficient :
  fixes n::nat and y::real_vector and m::real
  assumes non_negative: "non_negative_real_vector n y"
    and non_empty: "n > 0"
    and greater_or_equal: "\<forall> i::nat . i \<in> {1..n} \<longrightarrow> m \<ge> y i"
    and is_component: "\<exists> i::nat . i \<in> {1..n} \<and> m = y i"
  shows "m = maximum n y"
    using assms
proof (induct n)
  case 0
  show ?case sorry
next
  case (Suc n)
  (* removed some steps *)
  have "maximum (Suc n) y = m"
  proof (cases "n = 0")
    case True
    show ?thesis sorry
  next
    case False
    show ?thesis
    proof (cases "y (Suc n) = m")
      case True
      show ?thesis sorry
    next
      case False
      (* The following doesn't work:
      with Suc.prems(4) have pred_is_component: "\<exists>k::nat . k \<in> {1..n} \<and> m = y k" by auto
      Therefore we have to use the auxiliary predicate in_range:
      *)
      from Suc.prems(4) have "\<exists>i::nat . in_range (Suc n) i \<and> m = y i"
        unfolding in_range_def by simp
      with False have "\<exists>k::nat . in_range n k \<and> m = y k"
        unfolding in_range_def by (metis le_antisym not_less_eq_eq)
        (* Sledgehammer fails to prove the former when in_range is defined using i \<in> {1..n}; we need the form 1 \<le> i \<and> i \<le> n *)
      then have pred_is_component: "\<exists>k::nat . k \<in> {1..n} \<and> m = y k"
        unfolding in_range_def by simp
      (* OK, we got what we wanted. *)
      show ?thesis sorry
    qed
  qed
  show ?case sorry
qed

end