theory Finalise_DR

lemma mask_compare_imply:
  "\<lbrakk> (x && mask k >> l) && mask n = (y && mask k >> l) && mask n;size x= size y; k\<le> size x; l+n \<le> k; x\<noteq>y\<rbrakk>
    \<Longrightarrow> (x && mask l \<noteq>y && mask l) \<or> (x && ~~ mask (l+n)) \<noteq> (y && ~~ mask (l+n))" apply (rule ccontr) apply (subgoal_tac "x = y") apply simp apply (rule word_eqI) apply clarsimp apply (case_tac "na<l") apply (drule_tac na = na in test_bits_mask[where l = l and y = y]) apply clarsimp+ apply (case_tac "l+n\<le> na") apply (drule_tac na = na in test_bits_neg_mask; clarsimp) apply (drule_tac na = "na-l" in test_bits_mask) apply (clarsimp simp: linorder_not_le) apply (subst (asm) add.commute[where a = l])+ apply (drule nat_diff_less) apply (clarsimp simp:word_size)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size x; l + n \<le> k; x \<noteq> y\<rbrakk> \<Longrightarrow> x && mask l \<noteq> y && mask l \<or> x && ~~ mask (l + n) \<noteq> y && ~~ mask (l + n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size x; l + n \<le> k; x \<noteq> y; \<not> (x && mask l \<noteq> y && mask l \<or> x && ~~ mask (l + n) \<noteq> y && ~~ mask (l + n))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size x; l + n \<le> k; x \<noteq> y; \<not> (x && mask l \<noteq> y && mask l \<or> x && ~~ mask (l + n) \<noteq> y && ~~ mask (l + n)); x = y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size x; l + n \<le> k; x \<noteq> y; \<not> (x && mask l \<noteq> y && mask l \<or> x && ~~ mask (l + n) \<noteq> y && ~~ mask (l + n))\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size x; l + n \<le> k; x \<noteq> y; \<not> (x && mask l \<noteq> y && mask l \<or> x && ~~ mask (l + n) \<noteq> y && ~~ mask (l + n))\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size x; l + n \<le> k; x \<noteq> y; \<not> (x && mask l \<noteq> y && mask l \<or> x && ~~ mask (l + n) \<noteq> y && ~~ mask (l + n))\<rbrakk> \<Longrightarrow> na < size x \<longrightarrow> x !! na = y !! na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; na < l\<rbrakk> \<Longrightarrow> x !! na = y !! na
 2. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (4 subgoals):
 1. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; na < l\<rbrakk> \<Longrightarrow> na < size x
 2. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; na < l\<rbrakk> \<Longrightarrow> size x = size y
 3. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; na < l; na < l \<longrightarrow> x !! na = y !! na\<rbrakk> \<Longrightarrow> x !! na = y !! na
 4. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; l + n \<le> na\<rbrakk> \<Longrightarrow> x !! na = y !! na
 2. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>(x && mask k >> l) && mask n = (y && mask k >> l) && mask n; size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na\<rbrakk> \<Longrightarrow> na - l < size (x && mask k >> l)
 2. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na\<rbrakk> \<Longrightarrow> size (x && mask k >> l) = size (y && mask k >> l)
 3. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na; na - l < n \<longrightarrow> (x && mask k >> l) !! (na - l) = (y && mask k >> l) !! (na - l)\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); \<not> na < l; na < l + n\<rbrakk> \<Longrightarrow> na - l < size (x && mask k >> l)
 2. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na\<rbrakk> \<Longrightarrow> size (x && mask k >> l) = size (y && mask k >> l)
 3. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na; na - l < n \<longrightarrow> (x && mask k >> l) !! (na - l) = (y && mask k >> l) !! (na - l)\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>size x = size y; k \<le> size y; n + l \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (n + l) = y && ~~ mask (n + l); \<not> na < l; na < n + l\<rbrakk> \<Longrightarrow> na - l < size (x && mask k >> l)
 2. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na\<rbrakk> \<Longrightarrow> size (x && mask k >> l) = size (y && mask k >> l)
 3. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na; na - l < n \<longrightarrow> (x && mask k >> l) !! (na - l) = (y && mask k >> l) !! (na - l)\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal (4 subgoals):
 1. \<And>na. \<lbrakk>size x = size y; k \<le> size y; n + l \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (n + l) = y && ~~ mask (n + l); \<not> na < l\<rbrakk> \<Longrightarrow> l \<le> na
 2. \<And>na. \<lbrakk>size x = size y; k \<le> size y; n + l \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (n + l) = y && ~~ mask (n + l); \<not> na < l; na - l < n\<rbrakk> \<Longrightarrow> na - l < size (x && mask k >> l)
 3. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na\<rbrakk> \<Longrightarrow> size (x && mask k >> l) = size (y && mask k >> l)
 4. \<And>na. \<lbrakk>size x = size y; k \<le> size y; l + n \<le> k; x \<noteq> y; x && mask l = y && mask l; x && ~~ mask (l + n) = y && ~~ mask (l + n); na < size y; \<not> na < l; \<not> l + n \<le> na; na - l < n \<longrightarrow> (x && mask k >> l) !! (na - l) = (y && mask k >> l) !! (na - l)\<rbrakk> \<Longrightarrow> x !! na = y !! na proof (prove)
goal:
No subgoals!