theory More_Word_Operations

lemma word_less_bitD:
  fixes a::"'a::len word"
  assumes less: "a < b"
  shows "\<exists>n. (\<forall>i > n. bit a i = bit b i) \<and> \<not>bit a n \<and> bit b n" proof - define xs where "xs \<equiv> zip (to_bl a) (to_bl b)" define tk where "tk \<equiv> length (takeWhile (\<lambda>(x,y). x = y) xs)" define  n where  "n \<equiv> LENGTH('a) - Suc tk" have n_less: "n < LENGTH('a)" by (simp add: n_def) moreover { fix i have "\<not> i < LENGTH('a) \<Longrightarrow> bit a i = bit b i" using bit_imp_le_length by blast moreover assume "i > n" with n_less have "i < LENGTH('a) \<Longrightarrow> LENGTH('a) - Suc i < tk" unfolding n_def by arith hence "i < LENGTH('a) \<Longrightarrow> bit a i = bit b i" unfolding n_def tk_def xs_def by (fastforce dest: takeWhile_take_has_property_nth simp: rev_nth simp flip: nth_rev_to_bl) ultimately have "bit a i = bit b i" by blast } note all = this moreover from less have "a \<noteq> b" by simp then obtain i where "to_bl a ! i \<noteq> to_bl b ! i" using nth_equalityI word_bl.Rep_eqD word_rotate.lbl_lbl by blast then have "tk \<noteq> length xs" unfolding tk_def xs_def by (metis length_takeWhile_less list_eq_iff_zip_eq nat_neq_iff word_rotate.lbl_lbl) then have "tk < length xs" using length_takeWhile_le order_le_neq_trans tk_def by blast from nth_length_takeWhile[OF this[unfolded tk_def]] have "fst (xs ! tk) \<noteq> snd (xs ! tk)" by (clarsimp simp: tk_def) with `tk < length xs` have "bit a n \<noteq> bit b n" by (clarsimp simp: xs_def n_def tk_def nth_rev simp flip: nth_rev_to_bl) with less all have "\<not>bit a n \<and> bit b n" by (metis n_less order.asym word_less_bitI) ultimately show ?thesis by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
xs \<equiv> zip (to_bl a) (to_bl b)

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
tk \<equiv> length (takeWhile (\<lambda>(x, y). x = y) xs)

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
n \<equiv> LENGTH('a) - Suc tk

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (prove)
goal (1 subgoal):
 1. \<not> i < LENGTH('a) \<Longrightarrow> bit a i = bit b i proof (prove)
using this:
bit ?w ?n \<Longrightarrow> ?n < LENGTH(?'a)

goal (1 subgoal):
 1. \<not> i < LENGTH('a) \<Longrightarrow> bit a i = bit b i proof (state)
this:
\<not> i < LENGTH('a) \<Longrightarrow> bit a i = bit b i

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
\<not> i < LENGTH('a) \<Longrightarrow> bit a i = bit b i

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
n < i

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
n < LENGTH('a)
n < i proof (prove)
using this:
n < LENGTH('a)
n < i

goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> LENGTH('a) - Suc i < tk proof (prove)
using this:
LENGTH('a) - Suc tk < LENGTH('a)
LENGTH('a) - Suc tk < i

goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> LENGTH('a) - Suc i < tk proof (state)
this:
i < LENGTH('a) \<Longrightarrow> LENGTH('a) - Suc i < tk

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (prove)
using this:
i < LENGTH('a) \<Longrightarrow> LENGTH('a) - Suc i < tk

goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> bit a i = bit b i proof (prove)
using this:
i < LENGTH('a) \<Longrightarrow> LENGTH('a) - Suc i < length (takeWhile (\<lambda>(x, y). x = y) (zip (to_bl a) (to_bl b)))

goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> bit a i = bit b i proof (state)
this:
i < LENGTH('a) \<Longrightarrow> bit a i = bit b i

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
\<not> i < LENGTH('a) \<Longrightarrow> bit a i = bit b i
i < LENGTH('a) \<Longrightarrow> bit a i = bit b i proof (prove)
using this:
\<not> i < LENGTH('a) \<Longrightarrow> bit a i = bit b i
i < LENGTH('a) \<Longrightarrow> bit a i = bit b i

goal (1 subgoal):
 1. bit a i = bit b i proof (state)
this:
bit a i = bit b i

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
n < ?i2 \<Longrightarrow> bit a ?i2 = bit b ?i2

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
n < ?i2 \<Longrightarrow> bit a ?i2 = bit b ?i2

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
n < ?i2 \<Longrightarrow> bit a ?i2 = bit b ?i2

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
a < b proof (prove)
using this:
a < b

goal (1 subgoal):
 1. a \<noteq> b proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
a \<noteq> b proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. (\<And>i. to_bl a ! i \<noteq> to_bl b ! i \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
a \<noteq> b
\<lbrakk>length ?xs = length ?ys; \<And>i. i < length ?xs \<Longrightarrow> ?xs ! i = ?ys ! i\<rbrakk> \<Longrightarrow> ?xs = ?ys
to_bl ?x = to_bl ?y \<Longrightarrow> ?x = ?y
length (to_bl ?xa) = length (to_bl ?x)

goal (1 subgoal):
 1. (\<And>i. to_bl a ! i \<noteq> to_bl b ! i \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
to_bl a ! i \<noteq> to_bl b ! i

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
to_bl a ! i \<noteq> to_bl b ! i proof (prove)
using this:
to_bl a ! i \<noteq> to_bl b ! i

goal (1 subgoal):
 1. tk \<noteq> length xs proof (prove)
using this:
to_bl a ! i \<noteq> to_bl b ! i

goal (1 subgoal):
 1. length (takeWhile (\<lambda>(x, y). x = y) (zip (to_bl a) (to_bl b))) \<noteq> length (zip (to_bl a) (to_bl b)) proof (state)
this:
tk \<noteq> length xs

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
tk \<noteq> length xs proof (prove)
using this:
tk \<noteq> length xs

goal (1 subgoal):
 1. tk < length xs proof (prove)
using this:
tk \<noteq> length xs
length (takeWhile ?P ?xs) \<le> length ?xs
\<lbrakk>?a \<le> ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?a < ?b
tk \<equiv> length (takeWhile (\<lambda>(x, y). x = y) xs)

goal (1 subgoal):
 1. tk < length xs proof (state)
this:
tk < length xs

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
\<not> (case xs ! length (takeWhile (\<lambda>(x, y). x = y) xs) of (x, y) \<Rightarrow> x = y) proof (prove)
using this:
\<not> (case xs ! length (takeWhile (\<lambda>(x, y). x = y) xs) of (x, y) \<Rightarrow> x = y)

goal (1 subgoal):
 1. fst (xs ! tk) \<noteq> snd (xs ! tk) proof (state)
this:
fst (xs ! tk) \<noteq> snd (xs ! tk)

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
tk < length xs
fst (xs ! tk) \<noteq> snd (xs ! tk) proof (prove)
using this:
tk < length xs
fst (xs ! tk) \<noteq> snd (xs ! tk)

goal (1 subgoal):
 1. bit a n \<noteq> bit b n proof (state)
this:
bit a n \<noteq> bit b n

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
a < b
n < ?i2 \<Longrightarrow> bit a ?i2 = bit b ?i2
bit a n \<noteq> bit b n proof (prove)
using this:
a < b
n < ?i2 \<Longrightarrow> bit a ?i2 = bit b ?i2
bit a n \<noteq> bit b n

goal (1 subgoal):
 1. \<not> bit a n \<and> bit b n proof (state)
this:
\<not> bit a n \<and> bit b n

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (chain)
picking this:
n < LENGTH('a)
n < ?i2 \<Longrightarrow> bit a ?i2 = bit b ?i2
\<not> bit a n \<and> bit b n proof (prove)
using this:
n < LENGTH('a)
n < ?i2 \<Longrightarrow> bit a ?i2 = bit b ?i2
\<not> bit a n \<and> bit b n

goal (1 subgoal):
 1. \<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n proof (state)
this:
\<exists>n. (\<forall>i>n. bit a i = bit b i) \<and> \<not> bit a n \<and> bit b n

goal:
No subgoals!