theory Reversed_Bit_Lists

lemma unat_of_bl_length:
  "unat (of_bl xs :: 'a::len word) < 2 ^ (length xs)" proof (cases "length xs < LENGTH('a)") case True then have "(of_bl xs::'a::len word) < 2 ^ length xs" by (simp add: of_bl_length_less) with True show ?thesis by (simp add: word_less_nat_alt unat_of_nat) next case False have "unat (of_bl xs::'a::len word) < 2 ^ LENGTH('a)" by (simp split: unat_split) also from False have "LENGTH('a) \<le> length xs" by simp then have "2 ^ LENGTH('a) \<le> (2::nat) ^ length xs" by (rule power_increasing) simp finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ length xs proof (state)
goal (2 subgoals):
 1. length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
 2. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (state)
this:
length xs < LENGTH('a)

goal (2 subgoals):
 1. length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
 2. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (chain)
picking this:
length xs < LENGTH('a) proof (prove)
using this:
length xs < LENGTH('a)

goal (1 subgoal):
 1. of_bl xs < 2 ^ length xs proof (state)
this:
of_bl xs < 2 ^ length xs

goal (2 subgoals):
 1. length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
 2. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (chain)
picking this:
length xs < LENGTH('a)
of_bl xs < 2 ^ length xs proof (prove)
using this:
length xs < LENGTH('a)
of_bl xs < 2 ^ length xs

goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ length xs proof (state)
this:
unat (of_bl xs) < 2 ^ length xs

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (state)
goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (state)
this:
\<not> length xs < LENGTH('a)

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (prove)
goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ LENGTH('a) proof (state)
this:
unat (of_bl xs) < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (state)
this:
unat (of_bl xs) < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (chain)
picking this:
\<not> length xs < LENGTH('a) proof (prove)
using this:
\<not> length xs < LENGTH('a)

goal (1 subgoal):
 1. LENGTH('a) \<le> length xs proof (state)
this:
LENGTH('a) \<le> length xs

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (chain)
picking this:
LENGTH('a) \<le> length xs proof (prove)
using this:
LENGTH('a) \<le> length xs

goal (1 subgoal):
 1. 2 ^ LENGTH('a) \<le> 2 ^ length xs proof (state)
this:
2 ^ LENGTH('a) \<le> 2 ^ length xs

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs proof (chain)
picking this:
unat (of_bl xs) < 2 ^ length xs proof (prove)
using this:
unat (of_bl xs) < 2 ^ length xs

goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ length xs proof (state)
this:
unat (of_bl xs) < 2 ^ length xs

goal:
No subgoals!