theory StoreWord_C

lemma more_pageBits_inner_beauty:
  fixes x :: "10 word"
  fixes p :: word32
  assumes x: "x \<noteq> ucast (p && mask pageBits >> 2)"
  shows "(p && ~~ mask pageBits) + (ucast x * 4) \<noteq> p" apply clarsimp apply (simp add: word_shift_by_2) apply (subst (asm) word_plus_and_or_coroll) apply word_eqI apply (drule test_bit_size) apply (clarsimp simp: word_size pageBits_def) apply arith apply (insert x) apply (erule notE) apply word_eqI apply (erule_tac x="n+2" in allE) apply (clarsimp simp: word_ops_nth_size word_size) apply (clarsimp simp: pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) x * 4 \<noteq> p proof (prove)
goal (1 subgoal):
 1. (p && ~~ mask pageBits) + UCAST(10 \<rightarrow> 32) x * 4 = p \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. (p && ~~ mask pageBits) + (UCAST(10 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. (p && ~~ mask pageBits) && (UCAST(10 \<rightarrow> 32) x << 2) = 0
 2. p && ~~ mask pageBits || (UCAST(10 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < 32; 2 \<le> n; pageBits \<le> n; p !! n; n - 2 < 10; x !! (n - 2)\<rbrakk> \<Longrightarrow> False
 2. p && ~~ mask pageBits || (UCAST(10 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < 32; 2 \<le> n; pageBits \<le> n; n - 2 < 10; x !! (n - 2); n < size p\<rbrakk> \<Longrightarrow> False
 2. p && ~~ mask pageBits || (UCAST(10 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < 32; 12 \<le> n; n - 2 < 10; x !! 0\<rbrakk> \<Longrightarrow> False
 2. p && ~~ mask pageBits || (UCAST(10 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. p && ~~ mask pageBits || (UCAST(10 \<rightarrow> 32) x << 2) = p \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p && ~~ mask pageBits || (UCAST(10 \<rightarrow> 32) x << 2) = p; x \<noteq> UCAST(32 \<rightarrow> 10) (p && mask pageBits >> 2)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. p && ~~ mask pageBits || (UCAST(10 \<rightarrow> 32) x << 2) = p \<Longrightarrow> x = UCAST(32 \<rightarrow> 10) (p && mask pageBits >> 2) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n. (p !! n \<and> n < 32 \<and> (32 \<le> n \<or> pageBits \<le> n) \<or> 2 \<le> n \<and> n < 32 \<and> n - 2 < 32 \<and> x !! (n - 2)) = p !! n; n < 10\<rbrakk> \<Longrightarrow> x !! n = (p !! Suc (Suc n) \<and> Suc (Suc n) < pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 10; (p !! (n + 2) \<and> n + 2 < 32 \<and> (32 \<le> n + 2 \<or> pageBits \<le> n + 2) \<or> 2 \<le> n + 2 \<and> n + 2 < 32 \<and> n + 2 - 2 < 32 \<and> x !! (n + 2 - 2)) = p !! (n + 2)\<rbrakk> \<Longrightarrow> x !! n = (p !! Suc (Suc n) \<and> Suc (Suc n) < pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 10; (p !! Suc (Suc n) \<and> pageBits \<le> Suc (Suc n) \<or> x !! n) = p !! Suc (Suc n)\<rbrakk> \<Longrightarrow> x !! n = (p !! Suc (Suc n) \<and> Suc (Suc n) < pageBits) proof (prove)
goal:
No subgoals!