theory CSpace_AI

lemma guard_mask_shift:
  fixes cref' :: "'a::len word"
  assumes postfix: "to_bl cref' = xs @ cref"
  shows
  "(length guard \<le> length cref \<and>
    (cref' >> (length cref - length guard)) && mask (length guard) = of_bl guard)
  = (guard \<le> cref)" (is "(_ \<and> ?l = ?r) = _ " is "(?len \<and> ?shift) = ?prefix") proof let ?w_len = "len_of TYPE('a)" from postfix have "length (to_bl cref') = length xs + length cref" by simp hence w_len: "?w_len = \<dots>" by simp assume "?len \<and> ?shift" hence shift: ?shift and c_len: ?len by auto from w_len c_len have "length guard \<le> ?w_len" by simp with shift have "(replicate (?w_len - length guard) False) @ guard = to_bl ?l" by (simp add: word_rep_drop) also have "\<dots> = replicate (?w_len - length guard) False @
        drop (?w_len - length guard) (to_bl (cref' >> (length cref - length guard)))" by (simp add: bl_and_mask) also from c_len have "\<dots> = replicate (?w_len - length guard) False @ take (length guard) cref" by (simp add: bl_shiftr w_len word_size postfix) finally have "take (length guard) cref = guard" by simp thus ?prefix by (simp add: take_prefix) next let ?w_len = "len_of TYPE('a)" assume ?prefix then obtain zs where cref: "cref = guard @ zs" by (auto simp: prefix_def less_eq_list_def) with postfix have to_bl_c: "to_bl cref' = xs @ guard @ zs" by simp hence "length (to_bl cref') = length \<dots>" by simp hence w_len: "?w_len = \<dots>" by simp from cref have c_len: "length guard \<le> length cref" by simp from cref have "length cref - length guard = length zs" by simp hence "to_bl ?l = replicate (?w_len - length guard) False @
                   drop (?w_len - length guard) (to_bl (cref' >> (length zs)))" by (simp add: bl_and_mask) also have "drop (?w_len - length guard) (to_bl (cref' >> (length zs))) = guard" by (simp add: bl_shiftr word_size w_len to_bl_c) finally have "to_bl ?l = to_bl ?r" by (simp add: word_rep_drop w_len) with c_len show "?len \<and> ?shift" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard) = (guard \<le> cref) proof (state)
goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
to_bl cref' = xs @ cref proof (prove)
using this:
to_bl cref' = xs @ cref

goal (1 subgoal):
 1. length (to_bl cref') = length xs + length cref proof (state)
this:
length (to_bl cref') = length xs + length cref

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
using this:
length (to_bl cref') = length xs + length cref

goal (1 subgoal):
 1. LENGTH('a) = length xs + length cref proof (state)
this:
LENGTH('a) = length xs + length cref

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
this:
length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
using this:
length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard

goal (1 subgoal):
 1. (cref' >> length cref - length guard) && mask (length guard) = of_bl guard &&& length guard \<le> length cref proof (state)
this:
(cref' >> length cref - length guard) && mask (length guard) = of_bl guard
length guard \<le> length cref

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
LENGTH('a) = length xs + length cref
length guard \<le> length cref proof (prove)
using this:
LENGTH('a) = length xs + length cref
length guard \<le> length cref

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

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
(cref' >> length cref - length guard) && mask (length guard) = of_bl guard
length guard \<le> LENGTH('a) proof (prove)
using this:
(cref' >> length cref - length guard) && mask (length guard) = of_bl guard
length guard \<le> LENGTH('a)

goal (1 subgoal):
 1. replicate (LENGTH('a) - length guard) False @ guard = to_bl ((cref' >> length cref - length guard) && mask (length guard)) proof (state)
this:
replicate (LENGTH('a) - length guard) False @ guard = to_bl ((cref' >> length cref - length guard) && mask (length guard))

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
this:
replicate (LENGTH('a) - length guard) False @ guard = to_bl ((cref' >> length cref - length guard) && mask (length guard))

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
goal (1 subgoal):
 1. to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length cref - length guard)) proof (state)
this:
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length cref - length guard))

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
this:
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length cref - length guard))

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
length guard \<le> length cref proof (prove)
using this:
length guard \<le> length cref

goal (1 subgoal):
 1. replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length cref - length guard)) = replicate (LENGTH('a) - length guard) False @ take (length guard) cref proof (state)
this:
replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length cref - length guard)) = replicate (LENGTH('a) - length guard) False @ take (length guard) cref

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
replicate (LENGTH('a) - length guard) False @ guard = replicate (LENGTH('a) - length guard) False @ take (length guard) cref proof (prove)
using this:
replicate (LENGTH('a) - length guard) False @ guard = replicate (LENGTH('a) - length guard) False @ take (length guard) cref

goal (1 subgoal):
 1. take (length guard) cref = guard proof (state)
this:
take (length guard) cref = guard

goal (2 subgoals):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard \<Longrightarrow> guard \<le> cref
 2. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
using this:
take (length guard) cref = guard

goal (1 subgoal):
 1. guard \<le> cref proof (state)
this:
guard \<le> cref

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
this:
guard \<le> cref

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
guard \<le> cref proof (prove)
using this:
guard \<le> cref

goal (1 subgoal):
 1. (\<And>zs. cref = guard @ zs \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
cref = guard @ zs

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
to_bl cref' = xs @ cref
cref = guard @ zs proof (prove)
using this:
to_bl cref' = xs @ cref
cref = guard @ zs

goal (1 subgoal):
 1. to_bl cref' = xs @ guard @ zs proof (state)
this:
to_bl cref' = xs @ guard @ zs

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
using this:
to_bl cref' = xs @ guard @ zs

goal (1 subgoal):
 1. length (to_bl cref') = length (xs @ guard @ zs) proof (state)
this:
length (to_bl cref') = length (xs @ guard @ zs)

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
using this:
length (to_bl cref') = length (xs @ guard @ zs)

goal (1 subgoal):
 1. LENGTH('a) = length (xs @ guard @ zs) proof (state)
this:
LENGTH('a) = length (xs @ guard @ zs)

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
cref = guard @ zs proof (prove)
using this:
cref = guard @ zs

goal (1 subgoal):
 1. length guard \<le> length cref proof (state)
this:
length guard \<le> length cref

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
cref = guard @ zs proof (prove)
using this:
cref = guard @ zs

goal (1 subgoal):
 1. length cref - length guard = length zs proof (state)
this:
length cref - length guard = length zs

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
using this:
length cref - length guard = length zs

goal (1 subgoal):
 1. to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length zs)) proof (state)
this:
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length zs))

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
this:
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ drop (LENGTH('a) - length guard) (to_bl (cref' >> length zs))

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (prove)
goal (1 subgoal):
 1. drop (LENGTH('a) - length guard) (to_bl (cref' >> length zs)) = guard proof (state)
this:
drop (LENGTH('a) - length guard) (to_bl (cref' >> length zs)) = guard

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ guard proof (prove)
using this:
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = replicate (LENGTH('a) - length guard) False @ guard

goal (1 subgoal):
 1. to_bl ((cref' >> length cref - length guard) && mask (length guard)) = to_bl (of_bl guard) proof (state)
this:
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = to_bl (of_bl guard)

goal (1 subgoal):
 1. guard \<le> cref \<Longrightarrow> length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (chain)
picking this:
length guard \<le> length cref
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = to_bl (of_bl guard) proof (prove)
using this:
length guard \<le> length cref
to_bl ((cref' >> length cref - length guard) && mask (length guard)) = to_bl (of_bl guard)

goal (1 subgoal):
 1. length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard proof (state)
this:
length guard \<le> length cref \<and> (cref' >> length cref - length guard) && mask (length guard) = of_bl guard

goal:
No subgoals!