kings-crown/FVELER_Isabelle huggingface dataset:
theory GraphRefine

lemma c_guard_ptr_val_gt_0:
  "c_guard (p :: ('a :: mem_type) ptr) \<Longrightarrow> ptr_val p > 0" apply (simp only: word_neq_0_conv[symmetric], rule notI) apply (cases p, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p \<Longrightarrow> 0 < ptr_val p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c_guard p; ptr_val p = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma h_val_word8:
  "h_val hp p = load_word8 (ptr_val p) hp" by (simp add: h_val_def load_word8_def from_bytes_def typ_info_word
                word_rcat_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_val hp p = load_word8 (ptr_val p) hp
theory GraphRefine

lemma h_val_word32:
  "h_val hp p = load_word32 (ptr_val p) hp" by (simp add: h_val_def load_word32_def from_bytes_def typ_info_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_val hp p = load_word32 (ptr_val p) hp
theory GraphRefine

lemma h_val_word64:
  "h_val hp p = load_word64 (ptr_val p) hp" by (simp add: h_val_def load_word64_def from_bytes_def typ_info_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_val hp p = load_word64 (ptr_val p) hp
theory GraphRefine

lemma h_val_ptr:
  "h_val hp (p :: ('a :: c_type) ptr ptr) = Ptr (load_machine_word (ptr_val p) hp)" by (simp add: h_val_def load_word_defs from_bytes_def typ_info_ptr word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_val hp p = PTR('a) (load_word32 (ptr_val p) hp)
theory GraphRefine

lemma bintrunc_len_eq_signed:
  "bintrunc LENGTH('a) (uint (x :: 'a :: len signed word)) = uint x" by (metis (full_types) len_signed word_of_int_uint word_ubin.eq_norm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit LENGTH('a) (uint x) = uint x
theory GraphRefine

lemma uint_word_of_int_uint_signed_unsigned:
  "uint (word_of_int (uint (x :: 'a :: len signed word)) :: 'a word) = uint x" by (metis len_signed uint_word_of_int_eq word_uint.Rep_inverse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (word_of_int (uint x)) = uint x
theory GraphRefine

lemma is_up_is_down_remove_sign[simp]:
  "is_up (UCAST('a :: len signed \<rightarrow> 'a))"
  "is_down (UCAST('a signed \<rightarrow> 'a))" unfolding is_up_def is_down_def source_size target_size by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_up UCAST('a signed \<rightarrow> 'a) &&& is_down UCAST('a signed \<rightarrow> 'a) proof (prove)
goal (1 subgoal):
 1. LENGTH('a signed) \<le> LENGTH('a) &&& LENGTH('a) \<le> LENGTH('a signed)
theory GraphRefine

lemma to_bytes_remove_sign:
  "to_bytes (w :: 'a :: len8 signed word) = to_bytes (UCAST('a signed \<rightarrow> 'a) w)" by (simp add: to_bytes_def typ_info_word word_rsplit_def uint_up_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bytes w = to_bytes (UCAST('a signed \<rightarrow> 'a) w)
theory GraphRefine

lemma size_of_remove_sign:
  "size_of TYPE('a :: len8 signed word) = size_of TYPE('a word)" by (simp add: size_of_def typ_info_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size_of TYPE('a signed word) = size_of TYPE('a word)
theory GraphRefine

lemma heap_update_remove_sign:
  "heap_update p (w :: 'a :: len8 signed word) hp =
    heap_update (PTR_COERCE('a signed word \<rightarrow> 'a word) p) (ucast w) hp" by (simp add: heap_update_def to_bytes_remove_sign size_of_remove_sign)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p w hp = heap_update (PTR_COERCE('a signed word \<rightarrow> 'a word) p) (UCAST('a signed \<rightarrow> 'a) w) hp
theory GraphRefine

lemma heap_update_word8:
  "heap_update p (w :: 8 word) hp = store_word8 (ptr_val p) w hp" by (simp add: heap_update_def to_bytes_def typ_info_word store_word8_def word_rsplit_same)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p w hp = store_word8 (ptr_val p) w hp
theory GraphRefine

lemma heap_update_sword8:
  "heap_update p (w :: 8 signed word) hp = store_word8 (ptr_val p) (ucast w) hp" by (simp add: heap_update_def store_word8_def to_bytes_remove_sign to_bytes_word8)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p w hp = store_word8 (ptr_val p) (UCAST(8 signed \<rightarrow> 8) w) hp
theory GraphRefine

lemma heap_update_word32:
  "heap_update p w hp = store_word32 (ptr_val p) w hp" by (simp add: heap_update_def to_bytes_def typ_info_word store_word32_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p w hp = store_word32 (ptr_val p) w hp
theory GraphRefine

lemma heap_update_sword32:
  "heap_update p (w :: 32 signed word) hp = store_word32 (ptr_val p) (ucast w) hp" by (simp add: heap_update_remove_sign heap_update_word32)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p w hp = store_word32 (ptr_val p) (UCAST(32 signed \<rightarrow> 32) w) hp
theory GraphRefine

lemma heap_update_word64:
  "heap_update p w hp = store_word64 (ptr_val p) w hp" by (simp add: heap_update_def to_bytes_def typ_info_word store_word64_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p w hp = store_word64 (ptr_val p) w hp
theory GraphRefine

lemma heap_update_sword64:
  "heap_update p (w :: 64 signed word) hp = store_word64 (ptr_val p) (ucast w) hp" by (simp add: heap_update_remove_sign heap_update_word64)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p w hp = store_word64 (ptr_val p) (UCAST(64 signed \<rightarrow> 64) w) hp
theory GraphRefine

lemma heap_update_ptr:
  "heap_update (p :: ('a :: c_type) ptr ptr) p' hp = store_machine_word (ptr_val p) (ptr_val p') hp" by (simp add: heap_update_def to_bytes_def typ_info_ptr store_word_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p p' hp = store_word32 (ptr_val p) (ptr_val p') hp
theory GraphRefine

lemma from_bytes_ucast_isom[OF refl refl]:
  "x = from_bytes xs \<Longrightarrow> y = from_bytes xs
    \<Longrightarrow> size x = size y
    \<Longrightarrow> size x = length xs * 8
    \<Longrightarrow> ucast x = y" apply (clarsimp simp: word_size from_bytes_def typ_info_word) apply (rule word_eqI) apply (simp add: nth_ucast word_size test_bit_rcat[OF refl refl]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = from_bytes xs; y = from_bytes xs; size x = size y; size x = length xs * 8\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) x = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = word_rcat (rev xs); y = word_rcat (rev xs); LENGTH('a) = length xs * 8; LENGTH('b) = length xs * 8\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (word_rcat (rev xs)) = word_rcat (rev xs) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x = word_rcat (rev xs); y = word_rcat (rev xs); LENGTH('a) = length xs * 8; LENGTH('b) = length xs * 8\<rbrakk> \<Longrightarrow> n < size (UCAST('a \<rightarrow> 'b) (word_rcat (rev xs))) \<longrightarrow> UCAST('a \<rightarrow> 'b) (word_rcat (rev xs)) !! n = word_rcat (rev xs) !! n proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma h_val_sword8:
  "(h_val hp p :: 8 signed word) = ucast (h_val hp (ptr_coerce p) :: 8 word)" by (simp add: h_val_def from_bytes_ucast_isom word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_val hp p = UCAST(8 \<rightarrow> 8 signed) (h_val hp (PTR_COERCE(8 signed word \<rightarrow> 8 word) p))
theory GraphRefine

lemma h_val_sword32:
  "(h_val hp p :: 32 signed word) = ucast (h_val hp (ptr_coerce p) :: 32 word)" by (simp add: h_val_def from_bytes_ucast_isom word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_val hp p = UCAST(32 \<rightarrow> 32 signed) (h_val hp (PTR_COERCE(32 signed word \<rightarrow> 32 word) p))
theory GraphRefine

lemma h_val_sword64:
  "(h_val hp p :: 64 signed word) = ucast (h_val hp (ptr_coerce p) :: 64 word)" by (simp add: h_val_def from_bytes_ucast_isom word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_val hp p = UCAST(64 \<rightarrow> 64 signed) (h_val hp (PTR_COERCE(64 signed word \<rightarrow> 64 word) p))
theory GraphRefine

lemma to_bytes_ucast_isom[OF refl]:
  "y = ucast x
    \<Longrightarrow> size x = size y
    \<Longrightarrow> 8 dvd size x
    \<Longrightarrow> to_bytes y = to_bytes x" apply (rule ext) apply (clarsimp simp: word_size to_bytes_def typ_info_word) apply (rule nth_equalityI) apply (simp add: word_size length_word_rsplit_exp_size') apply (clarsimp simp: dvd_def) apply (rule word_eqI) apply (simp add: test_bit_rsplit_alt length_word_rsplit_exp_size' word_size
                   nth_ucast) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; size x = size y; 8 dvd size x\<rbrakk> \<Longrightarrow> to_bytes y = to_bytes x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; size x = size y; 8 dvd size x\<rbrakk> \<Longrightarrow> to_bytes y xa = to_bytes x xa proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; LENGTH('b) = LENGTH('a); 8 dvd LENGTH('a)\<rbrakk> \<Longrightarrow> word_rsplit (UCAST('b \<rightarrow> 'a) x) = word_rsplit x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; LENGTH('b) = LENGTH('a); 8 dvd LENGTH('a)\<rbrakk> \<Longrightarrow> length (word_rsplit (UCAST('b \<rightarrow> 'a) x)) = length (word_rsplit x)
 2. \<And>i. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; LENGTH('b) = LENGTH('a); 8 dvd LENGTH('a); i < length (word_rsplit (UCAST('b \<rightarrow> 'a) x))\<rbrakk> \<Longrightarrow> word_rsplit (UCAST('b \<rightarrow> 'a) x) ! i = word_rsplit x ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; LENGTH('b) = LENGTH('a); 8 dvd LENGTH('a); i < length (word_rsplit (UCAST('b \<rightarrow> 'a) x))\<rbrakk> \<Longrightarrow> word_rsplit (UCAST('b \<rightarrow> 'a) x) ! i = word_rsplit x ! i proof (prove)
goal (1 subgoal):
 1. \<And>i k. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; LENGTH('b) = 8 * k; i < length (word_rsplit (UCAST('b \<rightarrow> 'a) x)); LENGTH('a) = 8 * k\<rbrakk> \<Longrightarrow> word_rsplit (UCAST('b \<rightarrow> 'a) x) ! i = word_rsplit x ! i proof (prove)
goal (1 subgoal):
 1. \<And>i k n. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; LENGTH('b) = 8 * k; i < length (word_rsplit (UCAST('b \<rightarrow> 'a) x)); LENGTH('a) = 8 * k\<rbrakk> \<Longrightarrow> n < size (word_rsplit (UCAST('b \<rightarrow> 'a) x) ! i) \<longrightarrow> word_rsplit (UCAST('b \<rightarrow> 'a) x) ! i !! n = word_rsplit x ! i !! n proof (prove)
goal (1 subgoal):
 1. \<And>i k n. \<lbrakk>y = UCAST('b \<rightarrow> 'a) x; LENGTH('b) = 8 * k; i < k; LENGTH('a) = 8 * k\<rbrakk> \<Longrightarrow> n < 8 \<longrightarrow> ((k - Suc i) * 8 + n < 8 * k \<and> x !! ((k - Suc i) * 8 + n)) = x !! ((k - Suc i) * 8 + n) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma to_bytes_sword:
  "to_bytes (w :: ('a :: len8) signed word)
    = to_bytes (ucast w :: 'a word)" by (simp add: to_bytes_ucast_isom word_size len8_dv8)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bytes w = to_bytes (UCAST('a signed \<rightarrow> 'a) w)
theory GraphRefine

lemma heap_list_update_word8:
  "heap_update_list addr (to_bytes w (heap_list hp' 1 addr')) hp
    = store_word8 addr w hp"
  "heap_update_list addr (to_bytes w [hp' addr']) hp
    = store_word8 addr w hp" by (simp_all add: to_bytes_def store_word8_def typ_info_word word_rsplit_same)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update_list addr (to_bytes w (heap_list hp' 1 addr')) hp = store_word8 addr w hp &&& heap_update_list addr (to_bytes w [hp' addr']) hp = store_word8 addr w hp
theory GraphRefine

lemma heap_list_update_word32:
  "heap_update_list addr (to_bytes w (heap_list hp' 4 addr')) hp
    = store_word32 addr w hp" by (simp add: to_bytes_def store_word32_def typ_info_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update_list addr (to_bytes w (heap_list hp' 4 addr')) hp = store_word32 addr w hp
theory GraphRefine

lemma heap_list_update_word64:
  "heap_update_list addr (to_bytes w (heap_list hp' 8 addr')) hp
    = store_word64 addr w hp" by (simp add: to_bytes_def store_word64_def typ_info_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update_list addr (to_bytes w (heap_list hp' 8 addr')) hp = store_word64 addr w hp
theory GraphRefine

lemma heap_list_update_ptr:
  "heap_update_list addr (to_bytes p (heap_list hp' word_size addr')) hp
    = store_machine_word addr (ptr_val (p :: ('a :: c_type) ptr)) hp" by (simp add: to_bytes_def store_word_defs typ_info_ptr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update_list addr (to_bytes p (heap_list hp' word_size addr')) hp = store_word32 addr (ptr_val p) hp
theory GraphRefine

lemma field_lvalue_offset_eq:
  "field_lookup (typ_info_t TYPE('a :: c_type)) f 0 = Some v
        \<Longrightarrow> field_lvalue (ptr :: 'a ptr) f = ptr_val ptr + of_nat (snd v)" apply (cases v, simp, drule field_lookup_offset_eq) apply (simp add: field_lvalue_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. field_lookup (typ_info_t TYPE('a)) f 0 = Some v \<Longrightarrow> &(ptr\<rightarrow>f) = ptr_val ptr + word_of_nat (snd v) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>v = (a, b); field_offset TYPE('a) f = b\<rbrakk> \<Longrightarrow> &(ptr\<rightarrow>f) = ptr_val ptr + word_of_nat b proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma image_fst_cart_UNIV_subset:
  "S \<subseteq> (fst ` S) \<times> UNIV" by (auto elim: image_eqI[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> fst ` S \<times> UNIV
theory GraphRefine

lemma simpl_to_graph_impossible:
  "eq_impl nn eqs (\<lambda>_ _. False) (P \<inter> I)
    \<Longrightarrow> simpl_to_graph SGamma GGamma fname nn com n traces P I eqs out_eqs" apply (rule simpl_to_graphI, clarsimp) apply (drule(1) eq_implD, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. eq_impl nn eqs (\<lambda>_ _. False) (P \<inter> I) \<Longrightarrow> simpl_to_graph SGamma GGamma fname nn com n traces P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>eq_impl nn eqs (\<lambda>_ _. False) (P \<inter> I); tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma fname; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set traces); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma take_1_drop:
  "n < length xs \<Longrightarrow> take (Suc 0) (drop n xs) = [xs ! n]" apply (cases "drop n xs") apply simp apply (clarsimp dest!: nth_via_drop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> take (Suc 0) (drop n xs) = [xs ! n] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; drop n xs = []\<rbrakk> \<Longrightarrow> take (Suc 0) (drop n xs) = [xs ! n]
 2. \<And>a list. \<lbrakk>n < length xs; drop n xs = a # list\<rbrakk> \<Longrightarrow> take (Suc 0) (drop n xs) = [xs ! n] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>n < length xs; drop n xs = a # list\<rbrakk> \<Longrightarrow> take (Suc 0) (drop n xs) = [xs ! n] proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma ptr_safe_field:
  "\<lbrakk> ptr_safe (p :: ('a :: mem_type) ptr) d; field_ti TYPE('a) f = Some t;
        export_uinfo t = typ_uinfo_t TYPE('b) \<rbrakk>
    \<Longrightarrow> ptr_safe (Ptr &(p\<rightarrow>f) :: ('b :: mem_type) ptr) d" apply (clarsimp simp: field_ti_def split: option.split_asm) apply (erule(2) ptr_safe_mono) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr_safe p d; field_ti TYPE('a) f = Some t; export_uinfo t = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> ptr_safe (PTR('b) &(p\<rightarrow>f)) d proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>export_uinfo t = typ_uinfo_t TYPE('b); ptr_safe p d; field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, b)\<rbrakk> \<Longrightarrow> ptr_safe (PTR('b) &(p\<rightarrow>f)) d proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma heap_update_list_If2:
  "length xs \<le> addr_card
   \<Longrightarrow> heap_update_list p xs hp
     = (\<lambda>x. if x \<in> {p ..+ length xs} then xs ! unat (x - p) else hp x)" apply (simp add: heap_update_list_If1) apply (rule ext, simp add: intvl_def) apply clarsimp apply (erule notE, erule order_le_less_trans[rotated]) apply (simp add: unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> addr_card \<Longrightarrow> heap_update_list p xs hp = (\<lambda>x. if x \<in> {p..+length xs} then xs ! unat (x - p) else hp x) proof (prove)
goal (1 subgoal):
 1. length xs \<le> addr_card \<Longrightarrow> (\<lambda>x. if unat (x - p) < length xs then xs ! unat (x - p) else hp x) = (\<lambda>x. if x \<in> {p..+length xs} then xs ! unat (x - p) else hp x) proof (prove)
goal (1 subgoal):
 1. \<And>x. length xs \<le> addr_card \<Longrightarrow> \<not> unat (x - p) < length xs \<longrightarrow> (\<exists>k. x = p + word_of_nat k \<and> k < length xs) \<longrightarrow> hp x = xs ! unat (x - p) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>length xs \<le> addr_card; \<not> unat (word_of_nat k) < length xs; k < length xs\<rbrakk> \<Longrightarrow> hp (p + word_of_nat k) = xs ! unat (word_of_nat k) proof (prove)
goal (1 subgoal):
 1. \<And>k. length xs \<le> addr_card \<Longrightarrow> unat (word_of_nat k) \<le> k proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma word_sless_to_less:
  "\<lbrakk> 0 <=s x; 0 <=s y \<rbrakk> \<Longrightarrow> (x <s y) = (x < y)" apply (simp add: word_sless_alt word_sle_def word_less_def) apply (simp add: sint_eq_uint word_msb_sint) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le>s x; 0 \<le>s y\<rbrakk> \<Longrightarrow> (x <s y) = (x < y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> sint x; 0 \<le> sint y\<rbrakk> \<Longrightarrow> (sint x < sint y) = (uint x < uint y) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma word_sle_to_le:
  "\<lbrakk> 0 <=s x; 0 <=s y \<rbrakk> \<Longrightarrow> (x <=s y) = (x <= y)" apply (simp add: word_sle_def word_le_def) apply (simp add: sint_eq_uint word_msb_sint) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le>s x; 0 \<le>s y\<rbrakk> \<Longrightarrow> (x \<le>s y) = (x \<le> y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> sint x; 0 \<le> sint y\<rbrakk> \<Longrightarrow> (sint x \<le> sint y) = (uint x \<le> uint y) proof (prove)
goal:
No subgoals!
theory FieldAccessors

lemma h_val_mono:
  "\<lbrakk> field_lookup (typ_info_t TYPE('a)) f 0 = Some tp;
      h_val hp (p::'a::mem_type ptr) = v;
      export_uinfo (fst tp) = typ_uinfo_t TYPE('b) \<rbrakk> \<Longrightarrow>
          h_val hp (Ptr (&(p\<rightarrow>f))::'b::mem_type ptr) = (from_bytes (access_ti\<^sub>0 (fst tp) v))" using lift_t_mono[where p=p and f=f and v=v and g="\<lambda>_. True" and g'="\<lambda>_. True"
                        and t="fst tp" and n="snd tp" and 'b='b
                        and s="(hp, ptr_retyp p undefined)"] by (simp add: lift_t_if ptr_retyp_h_t_valid split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some tp; h_val hp p = v; export_uinfo (fst tp) = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> h_val hp (PTR('b) &(p\<rightarrow>f)) = from_bytes (access_ti\<^sub>0 (fst tp) v) proof (prove)
using this:
\<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (fst tp, snd tp); lift_t (\<lambda>_. True) (hp, ptr_retyp p undefined) p = Some v; export_uinfo (fst tp) = typ_uinfo_t TYPE('b); guard_mono (\<lambda>_. True) (\<lambda>_. True)\<rbrakk> \<Longrightarrow> lift_t (\<lambda>_. True) (hp, ptr_retyp p undefined) (PTR('b) &(p\<rightarrow>f)) = Some (from_bytes (access_ti\<^sub>0 (fst tp) v))

goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some tp; h_val hp p = v; export_uinfo (fst tp) = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> h_val hp (PTR('b) &(p\<rightarrow>f)) = from_bytes (access_ti\<^sub>0 (fst tp) v)
theory FieldAccessors

lemma h_val_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)) \<rbrakk>
    \<Longrightarrow> from_bytes (access_ti\<^sub>0 (adjust_ti (typ_info_t TYPE('b)) f upds)
               (h_val hp (p::'a::mem_type ptr)))
         = h_val hp (Ptr (&(p\<rightarrow>[s]))::'b::mem_type ptr)" by (simp add: h_val_mono typ_uinfo_t_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))\<rbrakk> \<Longrightarrow> from_bytes (access_ti\<^sub>0 (adjust_ti (typ_info_t TYPE('b)) f upds) (h_val hp p)) = h_val hp (PTR('b) &(p\<rightarrow>[s]))
theory FieldAccessors

lemma heap_list_rotate:
  "heap_list (\<lambda>x. hp (x + offs)) n p
     = heap_list hp n (p + offs)" by (induct n arbitrary: p, simp_all add: field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_list (\<lambda>x. hp (x + offs)) n p = heap_list hp n (p + offs)
theory FieldAccessors

lemma heap_update_rotate:
  "heap_update p v hp
    = (\<lambda>x. (heap_update q v (\<lambda>x. hp (x + (ptr_val p - ptr_val q))))
             (x + (ptr_val q - ptr_val p)))" by (simp add: heap_update_def heap_list_rotate
                heap_update_list_rotate)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p v hp = (\<lambda>x. heap_update q v (\<lambda>x. hp (x + (ptr_val p - ptr_val q))) (x + (ptr_val q - ptr_val p)))
theory FieldAccessors

lemma final_pad_id:
  "padup (2 ^ align_td tp) (size_td tp) = 0 \<Longrightarrow> final_pad tp = tp" by (simp add: final_pad_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. padup (2 ^ align_td tp) (size_td tp) = 0 \<Longrightarrow> final_pad tp = tp
theory FieldAccessors

lemma ti_typ_pad_combine_ti_typ_combine:
  "padup (align_of TYPE('a :: c_type)) (size_td tag) = 0
      \<Longrightarrow> ti_typ_pad_combine (t_b :: 'a itself) f_ab f_upd_ab fn tag
         = ti_typ_combine t_b f_ab f_upd_ab fn tag" by (simp add: ti_typ_pad_combine_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. padup (align_of TYPE('a)) (size_td tag) = 0 \<Longrightarrow> ti_typ_pad_combine t_b f_ab f_upd_ab fn tag = ti_typ_combine t_b f_ab f_upd_ab fn tag