theory More_Word_Operations

lemma word_log2_unfold:
  \<open>word_log2 w = (if w = 0 then 0 else Max {n. bit w n})\<close>
  for w :: \<open>'a::len word\<close> proof (cases \<open>w = 0\<close>) case True then show ?thesis by simp next case False then obtain r where \<open>bit w r\<close> by (auto simp add: bit_eq_iff) then have \<open>Max {m. bit w m} = LENGTH('a) - Suc (length
    (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))\<close> by (subst Max_eq_length_takeWhile [of _ \<open>LENGTH('a)\<close>])
      (auto simp add: bit_imp_le_length) then have \<open>word_log2 w = Max {x. bit w x}\<close> by (simp add: word_log2_def word_clz_def word_size to_bl_unfold rev_map takeWhile_map) with \<open>w \<noteq> 0\<close> show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (state)
goal (2 subgoals):
 1. w = 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
 2. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (state)
this:
w = 0

goal (2 subgoals):
 1. w = 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
 2. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (chain)
picking this:
w = 0 proof (prove)
using this:
w = 0

goal (1 subgoal):
 1. word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (state)
this:
word_log2 w = (if w = 0 then 0 else Max {n. bit w n})

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (state)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (state)
this:
w \<noteq> 0

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (chain)
picking this:
w \<noteq> 0 proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. (\<And>r. bit w r \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
bit w r

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (chain)
picking this:
bit w r proof (prove)
using this:
bit w r

goal (1 subgoal):
 1. Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)]))) proof (state)
this:
Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (chain)
picking this:
Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)]))) proof (prove)
using this:
Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))

goal (1 subgoal):
 1. word_log2 w = Max {x. bit w x} proof (state)
this:
word_log2 w = Max {x. bit w x}

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (chain)
picking this:
w \<noteq> 0
word_log2 w = Max {x. bit w x} proof (prove)
using this:
w \<noteq> 0
word_log2 w = Max {x. bit w x}

goal (1 subgoal):
 1. word_log2 w = (if w = 0 then 0 else Max {n. bit w n}) proof (state)
this:
word_log2 w = (if w = 0 then 0 else Max {n. bit w n})

goal:
No subgoals!