theory Verification imports
 Notraits
begin


fun height_of_node :: "AVLNode option \<Rightarrow> nat" where
  "height_of_node None = 0"
| "height_of_node (Some (mkAVLNode _ l r)) =
     max (height_of_node l) (height_of_node r) + 1"

  

fun is_ok :: "'a result \<Rightarrow> bool" where
  "is_ok (Ok _) = True"
| "is_ok _ = False"


lemma[simp]: "is_ok (cmp a b)"
  by simp


(* nicer induction rule for type AVLNode option *)
lemma AVLNode_option_induct: 
  assumes "\<And>v l r. (\<And>x. x \<in> set_option l \<Longrightarrow> P (Some x))
  \<Longrightarrow> (\<And>x. x \<in> set_option r \<Longrightarrow> P (Some x))
  \<Longrightarrow> P (Some (mkAVLNode v l r))"
  and "P None"
  shows "P AVLNodeOption"
proof (cases AVLNodeOption)
  case None
  then show ?thesis using assms by simp
next
  case (Some a)
  then show ?thesis 
    apply (induction a arbitrary: AVLNodeOption)
    using Some assms(1) by blast
qed


lemma right_is_smaller: "height_of_node r < height_of_node (Some (mkAVLNode v l r))"
  by (cases l) auto
  
lemma left_is_smaller: "height_of_node l < height_of_node (Some (mkAVLNode v l r))"
  by (cases r) auto
  

(* the loop in find always terminates (important for using \<open>obtain\<close> further down *)
termination aVLTreeSet_find_loop
proof (relation "measure (\<lambda>(v, t). height_of_node t)")
  show "wf (measure (\<lambda>(v, t). height_of_node t))" by simp
next
  fix value1 current_tree and x2 :: "AVLNode"
  assume "current_tree = Some x2"
  then show "((value1, right x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)"
  using right_is_smaller in_measure 
  by (metis AVLNode.collapse case_prod_conv)
next
  fix value1 current_tree and x2 :: "AVLNode"
  assume "current_tree = Some x2"
  then show "((value1, left x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)"
  using left_is_smaller in_measure 
  by (metis AVLNode.collapse case_prod_conv)
qed


value "cmp (u32 1) (u32 1)"

value "left (mkAVLNode (u32 0) None (Some (mkAVLNode (u32 0) None None)))"

lemma find_loop_ok: "is_ok (aVLTreeSet_find_loop v n)"
proof (induction n arbitrary: v rule: AVLNode_option_induct)
  case (1 u l r)
  obtain ordering where order: "Ok ordering = cmp u v"
    by force
  then show ?case 
  proof (cases ordering)
    case Ordering_Less
    hence "is_ok (aVLTreeSet_find_loop v r)" 
      using 1 by (simp add: option.split_sel_asm)
    then obtain b r' where a: "Ok (b, r') = aVLTreeSet_find_loop v r"
       by (auto elim: is_ok.elims)
    hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) =
               Ok (b, Some (mkAVLNode u l r'))"
      using Ordering_Less order apply simp
      by (smt (verit) AVLNode.expand AVLNode.record_simps(12) AVLNode.record_simps(13) AVLNode.record_simps(14) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4))
    then show ?thesis by simp
  next
    case Ordering_Equal
    hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) = Ok (True, Some (mkAVLNode u l r))"
      using 1 order by simp
    then show ?thesis by simp
  next
    case Ordering_Greater
    hence "is_ok (aVLTreeSet_find_loop v l)" 
      using 1 by (simp add: option.split_sel_asm)
    then obtain b l' where a: "Ok (b, l') = aVLTreeSet_find_loop v l"
       by (auto elim: is_ok.elims)
    hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) =
               Ok (b, Some (mkAVLNode u l' r))"
      using Ordering_Greater order apply simp
      by (smt (verit, ccfv_threshold) AVLNode.expand AVLNode.record_simps(6) AVLNode.record_simps(7) AVLNode.record_simps(8) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4))
    then show ?thesis by simp
  qed
next
  case 2
  then show ?case by simp
qed

(* find never produces an error *)
lemma find_ok: "\<exists>res. aVLTreeSet_find t v = Ok res"
proof -
  obtain b as where "Ok (b, as) = aVLTreeSet_find_loop v (root t)"
    using find_loop_ok by (metis is_ok.elims(2) old.prod.exhaust)
  then have "aVLTreeSet_find t v = Ok (b, \<lparr> root = as \<rparr>)" 
    apply simp unfolding bind_def
    by (metis old.prod.case result.simps(4))
  thus ?thesis 
    by simp
qed


end