theory More_Word

lemma upper_bits_unset_is_l2p:
  \<open>(\<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n') \<longleftrightarrow> (p < 2 ^ n)\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
    if \<open>n < LENGTH('a)\<close>
    for p :: "'a :: len word" proof assume ?Q then show ?P by (meson bang_is_le le_less_trans not_le word_power_increasing) next assume ?P have \<open>take_bit n p = p\<close> proof (rule bit_word_eqI) fix q assume \<open>q < LENGTH('a)\<close> show \<open>bit (take_bit n p) q \<longleftrightarrow> bit p q\<close> proof (cases \<open>q < n\<close>) case True then show ?thesis by (auto simp add: bit_simps) next case False then have \<open>n \<le> q\<close> by simp with \<open>?P\<close> \<open>q < LENGTH('a)\<close> have \<open>\<not> bit p q\<close> by simp then show ?thesis by (simp add: bit_simps) qed qed with that show ?Q using take_bit_word_eq_self_iff [of n p] by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n') = (p < 2 ^ n) proof (state)
goal (2 subgoals):
 1. \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' \<Longrightarrow> p < 2 ^ n
 2. p < 2 ^ n \<Longrightarrow> \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' proof (state)
this:
p < 2 ^ n

goal (2 subgoals):
 1. \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' \<Longrightarrow> p < 2 ^ n
 2. p < 2 ^ n \<Longrightarrow> \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' proof (chain)
picking this:
p < 2 ^ n proof (prove)
using this:
p < 2 ^ n

goal (1 subgoal):
 1. \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' proof (state)
this:
\<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'

goal (1 subgoal):
 1. \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' \<Longrightarrow> p < 2 ^ n proof (state)
goal (1 subgoal):
 1. \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' \<Longrightarrow> p < 2 ^ n proof (state)
this:
\<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'

goal (1 subgoal):
 1. \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' \<Longrightarrow> p < 2 ^ n proof (prove)
goal (1 subgoal):
 1. take_bit n p = p proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (take_bit n p) na = bit p na proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (take_bit n p) na = bit p na proof (state)
this:
q < LENGTH('a)

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (take_bit n p) na = bit p na proof (prove)
goal (1 subgoal):
 1. bit (take_bit n p) q = bit p q proof (state)
goal (2 subgoals):
 1. q < n \<Longrightarrow> bit (take_bit n p) q = bit p q
 2. \<not> q < n \<Longrightarrow> bit (take_bit n p) q = bit p q proof (state)
this:
q < n

goal (2 subgoals):
 1. q < n \<Longrightarrow> bit (take_bit n p) q = bit p q
 2. \<not> q < n \<Longrightarrow> bit (take_bit n p) q = bit p q proof (chain)
picking this:
q < n proof (prove)
using this:
q < n

goal (1 subgoal):
 1. bit (take_bit n p) q = bit p q proof (state)
this:
bit (take_bit n p) q = bit p q

goal (1 subgoal):
 1. \<not> q < n \<Longrightarrow> bit (take_bit n p) q = bit p q proof (state)
goal (1 subgoal):
 1. \<not> q < n \<Longrightarrow> bit (take_bit n p) q = bit p q proof (state)
this:
\<not> q < n

goal (1 subgoal):
 1. \<not> q < n \<Longrightarrow> bit (take_bit n p) q = bit p q proof (chain)
picking this:
\<not> q < n proof (prove)
using this:
\<not> q < n

goal (1 subgoal):
 1. n \<le> q proof (state)
this:
n \<le> q

goal (1 subgoal):
 1. \<not> q < n \<Longrightarrow> bit (take_bit n p) q = bit p q proof (chain)
picking this:
\<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'
q < LENGTH('a)
n \<le> q proof (prove)
using this:
\<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'
q < LENGTH('a)
n \<le> q

goal (1 subgoal):
 1. \<not> bit p q proof (state)
this:
\<not> bit p q

goal (1 subgoal):
 1. \<not> q < n \<Longrightarrow> bit (take_bit n p) q = bit p q proof (chain)
picking this:
\<not> bit p q proof (prove)
using this:
\<not> bit p q

goal (1 subgoal):
 1. bit (take_bit n p) q = bit p q proof (state)
this:
bit (take_bit n p) q = bit p q

goal:
No subgoals! proof (state)
this:
bit (take_bit n p) q = bit p q

goal:
No subgoals! proof (state)
this:
take_bit n p = p

goal (1 subgoal):
 1. \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n' \<Longrightarrow> p < 2 ^ n proof (chain)
picking this:
n < LENGTH('a)
take_bit n p = p proof (prove)
using this:
n < LENGTH('a)
take_bit n p = p

goal (1 subgoal):
 1. p < 2 ^ n proof (prove)
using this:
n < LENGTH('a)
take_bit n p = p
(take_bit n p = p) = (LENGTH('a) \<le> n \<or> p < 2 ^ n)

goal (1 subgoal):
 1. p < 2 ^ n proof (state)
this:
p < 2 ^ n

goal:
No subgoals!