kings-crown/FVELER_Isabelle huggingface dataset:
theory FieldAccessors

lemma field_lookup_to_bytes:
  "\<lbrakk> field_lookup (typ_info_t TYPE('a :: mem_type)) f 0
        \<equiv> Some (adjust_ti (typ_info_t TYPE('b :: mem_type)) accsr
           (updtr \<circ> (\<lambda>x _. x)),
          n);
        size_of TYPE('a) = length bs \<rbrakk>
    \<Longrightarrow> take (size_of TYPE('b)) (drop n (to_bytes v bs))
        = to_bytes (accsr v) (take (size_of TYPE ('b)) (drop n bs))" apply (drule meta_eq_to_obj_eq) apply (simp add: to_bytes_def) apply (frule_tac v=v and bs="bs"
    in field_access_take_drop_general(1)[rule_format]) apply (simp add: size_of_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); size_of TYPE('a) = length bs\<rbrakk> \<Longrightarrow> take (size_of TYPE('b)) (drop n (to_bytes v bs)) = to_bytes (accsr v) (take (size_of TYPE('b)) (drop n bs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size_of TYPE('a) = length bs; field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n)\<rbrakk> \<Longrightarrow> take (size_of TYPE('b)) (drop n (to_bytes v bs)) = to_bytes (accsr v) (take (size_of TYPE('b)) (drop n bs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size_of TYPE('a) = length bs; field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n)\<rbrakk> \<Longrightarrow> take (size_of TYPE('b)) (drop n (access_ti (typ_info_t TYPE('a)) v bs)) = access_ti (typ_info_t TYPE('b)) (accsr v) (take (size_of TYPE('b)) (drop n bs)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>size_of TYPE('a) = length bs; field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n)\<rbrakk> \<Longrightarrow> wf_fd (typ_info_t TYPE('a))
 2. \<lbrakk>size_of TYPE('a) = length bs; field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n)\<rbrakk> \<Longrightarrow> length bs = size_td (typ_info_t TYPE('a))
 3. \<lbrakk>size_of TYPE('a) = length bs; field_lookup (typ_info_t TYPE('a)) f 0 = Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); take (size_td (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)))) (drop (n - 0) (access_ti (typ_info_t TYPE('a)) v bs)) = access_ti (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x))) v (take (size_td (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)))) (drop (n - 0) bs))\<rbrakk> \<Longrightarrow> take (size_of TYPE('b)) (drop n (access_ti (typ_info_t TYPE('a)) v bs)) = access_ti (typ_info_t TYPE('b)) (accsr v) (take (size_of TYPE('b)) (drop n bs)) proof (prove)
goal:
No subgoals!
theory FieldAccessors

lemma field_lookup_to_bytes_split_step:
  "\<lbrakk> to_bytes v (heap_list hp (size_of TYPE('a)) addr)
            = xs @ drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr));
        field_lookup (typ_info_t TYPE('a :: mem_type)) f 0
            \<equiv> Some (adjust_ti (typ_info_t TYPE('b :: mem_type)) accsr
                (updtr \<circ> (\<lambda>x _. x)), n);
        m = n + size_of TYPE('b) \<rbrakk>
    \<Longrightarrow> to_bytes v (heap_list hp (size_of TYPE('a)) addr)
        = (xs @ to_bytes (accsr v) (heap_list hp (size_of TYPE ('b)) (addr + of_nat n)))
            @ drop m (to_bytes v (heap_list hp (size_of TYPE('a)) addr))" by (simp add: field_lookup_to_bytes_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_bytes v (heap_list hp (size_of TYPE('a)) addr) = xs @ drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr)); field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> to_bytes v (heap_list hp (size_of TYPE('a)) addr) = (xs @ to_bytes (accsr v) (heap_list hp (size_of TYPE('b)) (addr + word_of_nat n))) @ drop m (to_bytes v (heap_list hp (size_of TYPE('a)) addr))
theory FieldAccessors

lemma field_lookup_to_bytes_split_init:
  "to_bytes v (heap_list hp (size_of TYPE('a :: c_type)) addr)
            = [] @ drop 0 (to_bytes v (heap_list hp (size_of TYPE('a)) addr))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bytes v (heap_list hp (size_of TYPE('a)) addr) = [] @ drop 0 (to_bytes v (heap_list hp (size_of TYPE('a)) addr))
theory FieldAccessors

lemma take_heap_list_min:
  "take n (heap_list hp m addr) = heap_list hp (min n m) addr" by (simp add: min_def take_heap_list_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take n (heap_list hp m addr) = heap_list hp (min n m) addr
theory FieldAccessors

lemma drop_heap_list_general:
  "drop n (heap_list hp m addr) = heap_list hp (m - n) (addr + of_nat n)" apply (cases "n \<le> m") apply (simp_all add: drop_heap_list_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop n (heap_list hp m addr) = heap_list hp (m - n) (addr + word_of_nat n) proof (prove)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> drop n (heap_list hp m addr) = heap_list hp (m - n) (addr + word_of_nat n)
 2. \<not> n \<le> m \<Longrightarrow> drop n (heap_list hp m addr) = heap_list hp (m - n) (addr + word_of_nat n) proof (prove)
goal:
No subgoals!
theory FieldAccessors

lemma heap_update_mono_to_field_rewrite:
  "\<lbrakk> field_lookup (typ_info_t TYPE('a)) [s] 0
        \<equiv> field_lookup (adjust_ti (typ_info_t TYPE('b)) f upds) [] n;
      export_uinfo (adjust_ti (typ_info_t TYPE('b)) f upds)
        = export_uinfo (typ_info_t TYPE('b));
      align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; align_of TYPE('a) \<noteq> 0 \<rbrakk>
    \<Longrightarrow> heap_update (p::'a::packed_type ptr)
           (update_ti_t (adjust_ti (typ_info_t TYPE('b)) f upds) (to_bytes_p v)
               str) hp
         = heap_update (Ptr (&(p\<rightarrow>[s]))::'b::packed_type ptr) v (heap_update p str hp)" by (simp add: typ_uinfo_t_def heap_update_field2
                packed_heap_update_collapse h_val_heap_update
                field_ti_def update_ti_t_def size_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) [s] 0 \<equiv> field_lookup (adjust_ti (typ_info_t TYPE('b)) f upds) [] n; export_uinfo (adjust_ti (typ_info_t TYPE('b)) f upds) = export_uinfo (typ_info_t TYPE('b)); align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; align_of TYPE('a) \<noteq> 0\<rbrakk> \<Longrightarrow> heap_update p (update_ti_t (adjust_ti (typ_info_t TYPE('b)) f upds) (to_bytes_p v) str) hp = heap_update (PTR('b) &(p\<rightarrow>[s])) v (heap_update p str hp)
theory AsmSemanticsRespects

lemma asm_semantics_protects_globs_revD[OF refl]:
  "sw = globals_swap mem memu symtab xs
    \<Longrightarrow> (v', m', ms')
            \<in> asm_semantics specname v
                (hrs_mem (mem (sw s)), ms s)
    \<Longrightarrow> asm_semantics_protects_globs mem memu ms symtab xs
            \<longrightarrow> const_globals_in_memory symtab xs
                (hrs_mem (mem (sw (sw s))))
            \<longrightarrow> const_globals_in_memory symtab xs
                (hrs_mem (mem (sw (memu (hrs_mem_update (\<lambda>_. m')) (sw s)))))" apply (simp add: asm_semantics_protects_globs_def Let_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = globals_swap mem memu symtab xs; (v', m', ms') \<in> asm_semantics specname v (hrs_mem (mem (sw s)), ms s)\<rbrakk> \<Longrightarrow> asm_semantics_protects_globs mem memu ms symtab xs \<longrightarrow> const_globals_in_memory symtab xs (hrs_mem (mem (sw (sw s)))) \<longrightarrow> const_globals_in_memory symtab xs (hrs_mem (mem (sw (memu (hrs_mem_update (\<lambda>_. m')) (sw s))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = globals_swap mem memu symtab xs; (v', m', ms') \<in> asm_semantics specname v (hrs_mem (mem (globals_swap mem memu symtab xs s)), ms s)\<rbrakk> \<Longrightarrow> (\<forall>v v' s m'. (\<exists>ms' specname. (v', m', ms') \<in> asm_semantics specname v (hrs_mem (mem (globals_swap mem memu symtab xs s)), ms s)) \<longrightarrow> const_globals_in_memory symtab xs (hrs_mem (mem (globals_swap mem memu symtab xs (globals_swap mem memu symtab xs s)))) \<longrightarrow> const_globals_in_memory symtab xs (hrs_mem (mem (globals_swap mem memu symtab xs (memu (hrs_mem_update (\<lambda>_. m')) (globals_swap mem memu symtab xs s)))))) \<longrightarrow> const_globals_in_memory symtab xs (hrs_mem (mem (globals_swap mem memu symtab xs (globals_swap mem memu symtab xs s)))) \<longrightarrow> const_globals_in_memory symtab xs (hrs_mem (mem (globals_swap mem memu symtab xs (memu (hrs_mem_update (\<lambda>_. m')) (globals_swap mem memu symtab xs s))))) proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma const_globals_in_memory_heap_updateE:
  "\<lbrakk> globals_list_distinct D symtab gs;
    const_globals_in_memory symtab gs hmem;
    htd_safe D htd;
    ptr_safe (p :: ('a :: wf_type) ptr) htd \<rbrakk>
     \<Longrightarrow> const_globals_in_memory symtab gs (heap_update p val hmem)" by (simp add: const_globals_in_memory_heap_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_distinct D symtab gs; const_globals_in_memory symtab gs hmem; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> const_globals_in_memory symtab gs (heap_update p val hmem)
theory ProveGraphRefine

lemma disjoint_h_val_globals_swap_insert:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
     globals_list_distinct D symtab xs;
     htd_safe D htd;
     ptr_safe (p :: ('a :: wf_type) ptr) htd \<rbrakk>
     \<Longrightarrow> h_val (hrs_mem (g_hrs (globals s))) p
         = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs (globals s)))) p" 
  (* the current apparatus produces goals where the Simpl-derived
     h_vals are applied to a globals swap and the graph-derived
     h_vals lack it. we thus *add* a globals swap since that is the
     case where we can prove ptr_safe *)
   apply (rule disjoint_h_val_globals_swap[symmetric], assumption+) apply (clarsimp simp: ptr_safe_def htd_safe_def del: subsetI) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> h_val (hrs_mem (g_hrs (globals s))) p = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs (globals s)))) p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> h_val (hrs_mem (g_hrs (globals s))) p = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs (globals s)))) p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> s_footprint p \<subseteq> D \<times> UNIV proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; dom_s htd \<subseteq> D \<times> UNIV; s_footprint p \<subseteq> dom_s htd\<rbrakk> \<Longrightarrow> s_footprint p \<subseteq> D \<times> UNIV proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma disjoint_heap_update_globals_swap_rearranged:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
     globals_list_distinct D symtab xs;
     htd_safe D htd;
     ptr_safe (p :: ('a :: wf_type) ptr) htd \<rbrakk>
     \<Longrightarrow> hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (heap_update p v)) gs)))
         = heap_update p v (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs)))" apply (subst disjoint_heap_update_globals_swap[symmetric], assumption+) apply (clarsimp simp: ptr_safe_def htd_safe_def del: subsetI) apply blast apply (simp add: global_acc_valid_def hrs_mem_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (heap_update p v)) gs))) = heap_update p v (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> s_footprint p \<subseteq> D \<times> UNIV
 2. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> hrs_mem (g_hrs (g_hrs_upd (hrs_mem_update (heap_update p v)) (globals_swap g_hrs g_hrs_upd symtab xs gs))) = heap_update p v (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; dom_s htd \<subseteq> D \<times> UNIV; s_footprint p \<subseteq> dom_s htd\<rbrakk> \<Longrightarrow> s_footprint p \<subseteq> D \<times> UNIV
 2. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> hrs_mem (g_hrs (g_hrs_upd (hrs_mem_update (heap_update p v)) (globals_swap g_hrs g_hrs_upd symtab xs gs))) = heap_update p v (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; htd_safe D htd; ptr_safe p htd\<rbrakk> \<Longrightarrow> hrs_mem (g_hrs (g_hrs_upd (hrs_mem_update (heap_update p v)) (globals_swap g_hrs g_hrs_upd symtab xs gs))) = heap_update p v (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma hrs_mem_update_triv:
  "hrs_mem_update (\<lambda>_. hrs_mem x) x = x" by (cases x, simp_all add: hrs_mem_update_def hrs_mem_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hrs_mem_update (\<lambda>_. hrs_mem x) x = x
theory ProveGraphRefine

lemma h_t_valid_orig_and_ptr_safe:
  "h_t_valid d g p \<Longrightarrow> h_t_valid d g p \<and> ptr_safe p d" by (simp add: h_t_valid_ptr_safe)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. d,g \<Turnstile>\<^sub>t p \<Longrightarrow> d,g \<Turnstile>\<^sub>t p \<and> ptr_safe p d
theory ProveGraphRefine

lemma array_ptr_index_coerce:
  fixes p :: "(('a :: c_type)['b :: finite]) ptr"
  shows "n < CARD ('b)
    \<Longrightarrow> array_ptr_index p False n = array_ptr_index p True n" by (simp add: array_ptr_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < CARD('b) \<Longrightarrow> array_ptr_index p False n = array_ptr_index p True n
theory ProveGraphRefine

lemma unat_mono_thms:
  "unat (a + b :: ('a :: len) word) \<le> unat a + unat b"
  "unat (a * b) \<le> unat a * unat b" by (simp_all add: unat_word_ariths)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (a + b) \<le> unat a + unat b &&& unat (a * b) \<le> unat a * unat b
theory ProveGraphRefine

lemma unat_mono_intro:
  "unat a \<le> x \<Longrightarrow> x < b \<Longrightarrow> unat a < b"
  "unat a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> unat a \<le> b"
  "unat a \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> unat a = 0" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>unat a \<le> x; x < b\<rbrakk> \<Longrightarrow> unat a < b) &&& (\<lbrakk>unat a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> unat a \<le> b) &&& (\<lbrakk>unat a \<le> x; x \<le> 0\<rbrakk> \<Longrightarrow> unat a = 0)
theory ProveGraphRefine

lemma word_neq_0_conv_neg_conv:
  "(\<not> 0 < (n :: ('a :: len) word)) = (n = 0)" by (cases "n = 0", simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> 0 < n) = (n = 0)
theory ProveGraphRefine

lemma sint_drop_sign_isomorphism:
  "sint (drop_sign x) = sint x" by (simp add: drop_sign_def word_sint_msb_eq uint_up_ucast is_up_def
                source_size_def target_size_def word_size msb_ucast_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint (drop_sign x) = sint x
theory ProveGraphRefine

lemma drop_sign_isomorphism_ariths:
  "(x = y) = (drop_sign x = drop_sign y)"
  "(x < y) = (drop_sign x < drop_sign y)"
  "(x \<le> y) = (drop_sign x \<le> drop_sign y)"
  "(x <s y) = (drop_sign x <s drop_sign y)"
  "(x <=s y) = (drop_sign x <=s drop_sign y)"
  "drop_sign (x + y) = drop_sign x + drop_sign y"
  "drop_sign (x - y) = drop_sign x - drop_sign y"
  "drop_sign (x * y) = drop_sign x * drop_sign y"
  "drop_sign (x div y) = drop_sign x div drop_sign y"
  "drop_sign (x sdiv y) = drop_sign x sdiv drop_sign y"
  "drop_sign (- y) = - drop_sign y"
  "drop_sign (if P then x else y) = (if P then drop_sign x else drop_sign y)"
  "drop_sign (w ^ n) = drop_sign w ^ n" by (simp_all add: drop_sign_def word_less_def
                    word_le_def word_sless_def word_sle_def
                    sint_drop_sign_isomorphism[unfolded drop_sign_def]
                    word_uint.Rep_inject[symmetric]
                    uint_up_ucast is_up_def source_size_def
                    target_size_def word_size
                    uint_word_arith_bintrs
                    word_arith_power_alt
                    uint_word_of_int
                    uint_div_alt sdiv_word_def sdiv_int_def
               del: word_uint.Rep_inject of_int_power)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((x = y) = (drop_sign x = drop_sign y) &&& (x < y) = (drop_sign x < drop_sign y) &&& (x \<le> y) = (drop_sign x \<le> drop_sign y)) &&& (x <s y) = (drop_sign x <s drop_sign y) &&& (x \<le>s y) = (drop_sign x \<le>s drop_sign y) &&& drop_sign (x + y) = drop_sign x + drop_sign y) &&& (drop_sign (x - y) = drop_sign x - drop_sign y &&& drop_sign (x * y) = drop_sign x * drop_sign y &&& drop_sign (x div y) = drop_sign x div drop_sign y) &&& (drop_sign (x sdiv y) = drop_sign x sdiv drop_sign y &&& drop_sign (- y) = - drop_sign y) &&& drop_sign (if P then x else y) = (if P then drop_sign x else drop_sign y) &&& drop_sign (w ^ n) = drop_sign w ^ n
theory ProveGraphRefine

lemma drop_sign_isomorphism_bitwise:
  "drop_sign (x AND y) = drop_sign x AND drop_sign y"
  "drop_sign (x OR y) = (drop_sign x) OR (drop_sign y)"
  "drop_sign (x XOR y) = drop_sign x XOR drop_sign y"
  "drop_sign (~~ y) = ~~ drop_sign y"
  "drop_sign (shiftl x n) = shiftl (drop_sign x) n"
  "drop_sign (shiftr x n) = shiftr (drop_sign x) n"
  "drop_sign (sshiftr x n) = sshiftr (drop_sign x) n"
  "drop_sign (ucast z) = ucast z"
  "drop_sign (scast z) = scast z"
  "ucast x = ucast (drop_sign x)"
  "scast x = scast (drop_sign x)" by (all \<open>(word_eqI_solve simp: drop_sign_def test_bit_bin)\<close>)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((drop_sign (x && y) = drop_sign x && drop_sign y &&& drop_sign (x || y) = drop_sign x || drop_sign y) &&& drop_sign (x xor y) = drop_sign x xor drop_sign y &&& drop_sign (~~ y) = ~~ drop_sign y &&& drop_sign (x << n) = drop_sign x << n) &&& (drop_sign (x >> n) = drop_sign x >> n &&& drop_sign (x >>> n) = drop_sign x >>> n &&& drop_sign (UCAST('c \<rightarrow> 'b signed) z) = UCAST('c \<rightarrow> 'b) z) &&& drop_sign (SCAST('c \<rightarrow> 'd signed) z) = SCAST('c \<rightarrow> 'd) z &&& UCAST('a signed \<rightarrow> 'e) x = UCAST('a \<rightarrow> 'e) (drop_sign x) &&& SCAST('a signed \<rightarrow> 'f) x = SCAST('a \<rightarrow> 'f) (drop_sign x)
theory ProveGraphRefine

lemma drop_sign_of_nat:
  "drop_sign (of_nat n) = of_nat n" by (metis down_cast_same drop_sign_def is_up_is_down_remove_sign(2) scast_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_sign (word_of_nat n) = word_of_nat n
theory ProveGraphRefine

lemma drop_sign_to_bl:
  "to_bl (drop_sign w) = to_bl w" by (simp add: drop_sign_def to_bl_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (drop_sign w) = to_bl w
theory ProveGraphRefine

lemma drop_sign_extra_bl_ops:
  "drop_sign (bv_clz w) = bv_clz (drop_sign w)"
  "drop_sign (bv_ctz w) = bv_ctz (drop_sign w)"
  "drop_sign (bv_popcount w) = bv_popcount (drop_sign w)" by (simp_all add: bv_clz_def bv_ctz_def bv_popcount_def drop_sign_of_nat
                    word_ctz_def word_clz_def pop_count_def drop_sign_to_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_sign (bv_clz w) = bv_clz (drop_sign w) &&& drop_sign (bv_ctz w) = bv_ctz (drop_sign w) &&& drop_sign (bv_popcount w) = bv_popcount (drop_sign w)
theory ProveGraphRefine

lemma drop_sign_number[simp]:
  "drop_sign (numeral n) = numeral n"
  "drop_sign (- numeral n) = - numeral n"
  "drop_sign 0 = 0" "drop_sign 1 = 1" by (simp_all add: drop_sign_def ucast_def del: unsigned_numeral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (drop_sign (numeral n) = numeral n &&& drop_sign (- numeral n) = - numeral n) &&& drop_sign 0 = 0 &&& drop_sign 1 = 1
theory ProveGraphRefine

lemma drop_sign_minus_1[simp]:
  "drop_sign (-1) = (-1)" by (clarsimp simp add: drop_sign_def ucast_def uint_word_ariths)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_sign (- 1) = - 1
theory ProveGraphRefine

lemma drop_sign_projections:
  "unat x = unat (drop_sign x)"
  "uint x = uint (drop_sign x)"
  "sint x = sint (drop_sign x)" apply (simp_all add: sint_drop_sign_isomorphism) apply (auto simp: unat_ucast_upcast uint_up_ucast drop_sign_def is_up_def
                    source_size_def target_size_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x = unat (drop_sign x) &&& uint x = uint (drop_sign x) &&& sint x = sint (drop_sign x) proof (prove)
goal (2 subgoals):
 1. unat x = unat (drop_sign x)
 2. uint x = uint (drop_sign x) proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma drop_sign_h_val[simp]:
  "drop_sign (h_val hp p :: ('a :: len8) signed word) = h_val hp (ptr_coerce p)" using len8_dv8[where 'a='a] apply (simp add: h_val_def drop_sign_def) apply (simp add: from_bytes_ucast_isom word_size size_of_def typ_info_word) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_sign (h_val hp p) = h_val hp (PTR_COERCE('a signed word \<rightarrow> 'a word) p) proof (prove)
using this:
8 dvd LENGTH('a)

goal (1 subgoal):
 1. drop_sign (h_val hp p) = h_val hp (PTR_COERCE('a signed word \<rightarrow> 'a word) p) proof (prove)
goal (1 subgoal):
 1. 8 dvd LENGTH('a) \<Longrightarrow> UCAST('a signed \<rightarrow> 'a) (from_bytes (heap_list hp (size_of TYPE('a signed word)) (ptr_val p))) = from_bytes (heap_list hp (size_of TYPE('a word)) (ptr_val p)) proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma drop_sign_heap_update[simp]:
  "heap_update p v = heap_update (ptr_coerce p) (drop_sign v)" using len8_dv8[where 'a='a] apply (simp add: heap_update_def drop_sign_def fun_eq_iff) apply (simp add: to_bytes_ucast_isom word_size size_of_def typ_info_word) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p v = heap_update (PTR_COERCE('a signed word \<rightarrow> 'a word) p) (drop_sign v) proof (prove)
using this:
8 dvd LENGTH('a)

goal (1 subgoal):
 1. heap_update p v = heap_update (PTR_COERCE('a signed word \<rightarrow> 'a word) p) (drop_sign v) proof (prove)
goal (1 subgoal):
 1. 8 dvd LENGTH('a) \<Longrightarrow> \<forall>x xa. heap_update_list (ptr_val p) (to_bytes v (heap_list x (size_of TYPE('a signed word)) (ptr_val p))) x xa = heap_update_list (ptr_val p) (to_bytes (UCAST('a signed \<rightarrow> 'a) v) (heap_list x (size_of TYPE('a word)) (ptr_val p))) x xa proof (prove)
goal:
No subgoals!