theory BinarnaPretraga
imports Main
begin

(* Implementacija koja koristi liste nije efikasna, jer je indeksni pristup 
   elementima liste linearne slozenosti.
*)
function bp :: "('a::linorder) list \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
  "bp xs x l d = 
    (if l > d then False
     else (
        let s = (l + d) div 2
         in if x < xs ! nat s then bp xs x l (s - 1)
             else if x > xs ! nat s then bp xs x (s + 1) d
             else True
     ))"
  by pat_completeness auto
termination
  by (relation "measure (\<lambda> (xs, x, l, d). nat (d - l + 1))") auto

declare bp.simps[simp del]

definition binarna_pretraga :: "('a::linorder) list \<Rightarrow> 'a \<Rightarrow> bool" where
  "binarna_pretraga xs x = bp xs x 0 (int (length xs) - 1)"

value "binarna_pretraga [2::nat, 3, 5, 7, 8, 10] 1"
value "binarna_pretraga [2::nat, 3, 5, 7, 8, 10] 5"
value "binarna_pretraga [2::nat, 3, 5, 7, 8, 10] 6"
value "binarna_pretraga [2::nat, 3, 5, 7, 8, 10] 7"
value "binarna_pretraga [2::nat, 3, 5, 7, 8, 10] 12"

lemma bp:
  assumes "0 \<le> l" "l \<le> int (length xs)"
  assumes "-1 \<le> d" "d < int (length xs)"
  assumes "sorted xs"
  shows "bp xs x l d \<longleftrightarrow> (\<exists> p. l \<le> p \<and> p \<le> d \<and> xs ! nat p = x)"
  using assms
proof (induction xs x l d rule: bp.induct)
  case (1 xs x l d)
  show ?case
  proof (cases "l > d")
    case True
    then show ?thesis
      by (auto simp add: bp.simps)
  next
    case False
    let ?s = "(l + d) div 2"
    have s: "0 \<le> ?s \<and> ?s < int (length xs)"
      using \<open>0 \<le> l\<close> \<open>\<not> l > d\<close>
      using \<open>l \<le> int (length xs)\<close> \<open>d < int (length xs)\<close>
      by auto

    have sld: "l \<le> ?s \<and> ?s \<le> d"
      using \<open>0 \<le> l\<close> \<open>\<not> l > d\<close>
      by auto

    show ?thesis 
    proof (cases "x < xs ! nat ?s")
      case True

      have desno_veci: "\<forall>p. ?s - 1 < p \<and> p \<le> d \<longrightarrow> x < xs ! nat p"
        using \<open>x < xs ! nat ?s\<close> \<open>sorted xs\<close> s
        by (smt (verit, ccfv_SIG) "1.prems"(4) le_less_trans nat_le_eq_zle nat_less_iff not_le sorted_nth_mono)

      have "bp xs x l d = bp xs x l (?s - 1)"
        using \<open>x < xs ! nat ?s\<close> `\<not> l > d` bp.simps[of xs x l d]
        by auto
      also have "\<dots> = (\<exists> p. l \<le> p \<and> p \<le> ?s - 1 \<and> xs ! nat p = x)"
      proof (rule 1(1))
        show "\<not> d < l" "x < xs ! nat ?s" "0 \<le> l" "l \<le> int (length xs)" "sorted xs"
          by fact+
      next
        show "- 1 \<le> ?s - 1" "?s - 1 < int (length xs)"
          using s
          by auto
      qed simp
      finally
      show ?thesis
        using desno_veci
        by force
    next
      case False
      show ?thesis
      proof (cases "x > xs ! nat ?s")
        case True
        have levo_manji: "\<forall>p. l \<le> p \<and> p < ?s + 1 \<longrightarrow> x > xs ! nat p"
          using \<open>x > xs ! nat ?s\<close> \<open>sorted xs\<close> s
          by (meson le_less_trans nat_le_eq_zle nat_less_iff sorted_nth_mono zle_add1_eq_le)

        have "bp xs x l d = bp xs x (?s + 1) d"
          using \<open>\<not> x < xs ! nat ?s\<close> \<open>x > xs ! nat ?s\<close> `\<not> l > d` bp.simps[of xs x l d]
          by auto
        also have "\<dots> = (\<exists> p. ?s + 1 \<le> p \<and> p \<le> d \<and> xs ! nat p = x)"
        proof (rule 1(2))
          show "\<not> d < l" "\<not> x < xs ! nat ?s" "x > xs ! nat ?s" "-1 \<le> d" "d < int (length xs)" "sorted xs"
            by fact+
        next
          show "0 \<le> ?s + 1" "?s + 1 <= int (length xs)"
            using s
            by auto
        qed simp
        finally
        show ?thesis
          using levo_manji sld
          by (smt (verit) verit_comp_simplify1(1))
      next
        case False
        then have "xs ! nat ?s = x"
          using \<open>\<not> x < xs ! nat ?s\<close>
          by simp
        then show ?thesis
          using \<open>\<not> l > d\<close> `\<not> xs ! nat ?s < x` `\<not> xs ! nat ?s > x` bp.simps[of xs x l d]
          using sld
          by metis
      qed
    qed
  qed
qed

theorem 
  assumes "sorted xs"
  shows "binarna_pretraga xs x \<longleftrightarrow> x \<in> set xs"
  unfolding binarna_pretraga_def
  using bp[of 0 xs "int (length xs) - 1" x]
  by (smt (z3) assms in_set_conv_nth nat_int nat_less_iff negative_zle)


end