Isabelle simplifier unpredictability

AssocTree.thy

theory AssocTree
imports Main
begin

(* Binary lookup in a sorted list *)
(* this seems silly because the list operations are linear, but if we can specialise this definition
  for a particular statically-known list then we'd end up with an efficient implementation *)
fun lookup_tree :: "(('a :: linorder) × 'b) list ⇒ 'b ⇒ 'a ⇒ 'b" where
    "lookup_tree [] def _ = def"
  | "lookup_tree [(k',v)] def k = (if k = k' then v else def)"
  | "lookup_tree xs def k =
     (let n = length xs div 2
      in let hs = take n xs
      in let ts = drop n xs
      in let (tk, tv) = hd ts
      in if k = tk
         then tv
         else if k < tk
         then lookup_tree hs def k
         else lookup_tree (tl ts) def k
      )"


(* Test case for lookup_tree *)
definition lookup_test :: "nat ⇒ nat ⇒ nat" where
 "lookup_test = lookup_tree [(1,10), (2,20), (3,30), (4,40), (5,50)]"

(* I just want to see what happens when we simplify lookup_test:
   wrap it in a free function 'SPEC' so we can't prove anything  *)
lemma "SPEC (lookup_test default_value key)"
  apply (unfold lookup_test_def)
  (* SPEC (lookup_tree [(1, 10), (2, 20), (3, 30), (4, 40), (5, 50)] default_value key) *)
  apply (simp split del: if_split cong: if_cong)
  (* SPEC
     (if key = 3 then 30
      else if key < 3 then if key = 2 then 20 else if key = Suc 0 then 10 else default_value
           else if key = 5 then 50 else if key < 5 then 40 else default_value)
  *)
  oops

lemma "SPEC (lookup_test default_value key)" unfolding lookup_test_def
  apply (simp split del: if_split cong: if_cong)
  (* SPEC
     (if key = 3 then 30
      else if key < 3 then if key = 2 then 20 else if key = Suc 0 then 10 else default_value
           else if key = 5 then 50 else if key < 5 then 40 else default_value)
  *)
  (* This is same as above *)
  oops


(* This is the exact same thing, just with lookup_test unfolded *)
(* but it simplifies to a different thing ! ! ! *)
lemma "SPEC (lookup_tree [(1, 10), (2, 20), (3, 30), (4, 40), (5, 50)] default_value key)"
  apply (simp split del: if_split cong: if_cong)
  (* SPEC
     (if key = 3 then 30
      else if key < 3 then if key = 2 then 20 else if key < 2 then if key = 1 then 10 else default_value else default_value
           else if key = 5 then 50 else if key < 5 then if key = 4 then 40 else default_value else default_value)
  *)
  (* This is different from above - we have the "if key = 4" that's simplified away from previous versions *)
  oops