theory More_Word_Operations

lemma sign_extended_add:
  assumes p: "is_aligned p n"
  assumes f: "f < 2 ^ n"
  assumes e: "n \<le> e"
  assumes "sign_extended e p"
  shows "sign_extended e (p + f)" proof (cases "e < size p") case True note and_or = is_aligned_add_or[OF p f] have "\<not> bit f e" using True e less_2p_is_upper_bits_unset[THEN iffD1, OF f] by (fastforce simp: word_size) hence i: "bit (p + f) e = bit p e" by (simp add: and_or bit_simps) have fm: "f AND mask e = f" by (fastforce intro: subst[where P="\<lambda>f. f AND mask e = f", OF less_mask_eq[OF f]]
                  simp: mask_twice e) show ?thesis using assms apply (simp add: sign_extended_iff_sign_extend sign_extend_def i) apply (simp add: and_or word_bw_comms[of p f]) apply (clarsimp simp: word_ao_dist fm word_bw_assocs split: if_splits) done next case False thus ?thesis by (simp add: sign_extended_def word_size) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sign_extended e (p + f) proof (state)
goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (state)
this:
e < size p

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (state)
this:
p + f = p OR f

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (prove)
goal (1 subgoal):
 1. \<not> bit f e proof (prove)
using this:
e < size p
n \<le> e
n < LENGTH('a) \<and> (\<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit f n')

goal (1 subgoal):
 1. \<not> bit f e proof (state)
this:
\<not> bit f e

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (prove)
using this:
\<not> bit f e

goal (1 subgoal):
 1. bit (p + f) e = bit p e proof (state)
this:
bit (p + f) e = bit p e

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (prove)
goal (1 subgoal):
 1. f AND mask e = f proof (state)
this:
f AND mask e = f

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (prove)
goal (1 subgoal):
 1. sign_extended e (p + f) proof (prove)
using this:
is_aligned p n
f < 2 ^ n
n \<le> e
sign_extended e p

goal (1 subgoal):
 1. sign_extended e (p + f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; f < 2 ^ n; n \<le> e; (if bit p e then p OR NOT (mask e) else p AND mask e) = p\<rbrakk> \<Longrightarrow> (bit p e \<longrightarrow> p + f OR NOT (mask e) = p + f) \<and> (\<not> bit p e \<longrightarrow> p + f AND mask e = p + f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; f < 2 ^ n; n \<le> e; (if bit p e then p OR NOT (mask e) else p AND mask e) = p\<rbrakk> \<Longrightarrow> (bit p e \<longrightarrow> (f OR p) OR NOT (mask e) = f OR p) \<and> (\<not> bit p e \<longrightarrow> (f OR p) AND mask e = f OR p) proof (prove)
goal:
No subgoals! proof (state)
this:
sign_extended e (p + f)

goal (1 subgoal):
 1. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (state)
goal (1 subgoal):
 1. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (state)
this:
\<not> e < size p

goal (1 subgoal):
 1. \<not> e < size p \<Longrightarrow> sign_extended e (p + f) proof (prove)
using this:
\<not> e < size p

goal (1 subgoal):
 1. sign_extended e (p + f) proof (state)
this:
sign_extended e (p + f)

goal:
No subgoals!