lib: Helper lemmas for simplifying writes via char pointers.
This commit is contained in:
parent
7850af557b
commit
b053ce7647
|
@ -728,10 +728,9 @@ lemma heap_access_Array_element':
|
||||||
apply (rule refl)
|
apply (rule refl)
|
||||||
apply (simp add: split_upt_on_n[OF less])
|
apply (simp add: split_upt_on_n[OF less])
|
||||||
apply (rule trans, rule foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
|
apply (rule trans, rule foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
|
||||||
apply (simp add: index_update2)
|
apply simp+
|
||||||
apply (simp add: index_update)
|
|
||||||
apply (subst foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
|
apply (subst foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
|
||||||
apply (simp add: index_update2)
|
apply simp
|
||||||
apply (simp add: drop_heap_list_le take_heap_list_le)
|
apply (simp add: drop_heap_list_le take_heap_list_le)
|
||||||
apply (subst take_heap_list_le)
|
apply (subst take_heap_list_le)
|
||||||
apply (simp add: le_diff_conv2)
|
apply (simp add: le_diff_conv2)
|
||||||
|
@ -754,7 +753,7 @@ lemma heap_update_id:
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (simp add: from_bytes_def to_bytes_def update_ti_t_def
|
apply (simp add: from_bytes_def to_bytes_def update_ti_t_def
|
||||||
size_of_def field_access_update_same
|
size_of_def field_access_update_same
|
||||||
td_fafu_idem wf_fd)
|
td_fafu_idem)
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma fold_cong':
|
lemma fold_cong':
|
||||||
|
@ -1079,4 +1078,17 @@ qed
|
||||||
lemma FCP_arg_cong:"f = g \<Longrightarrow> FCP f = FCP g"
|
lemma FCP_arg_cong:"f = g \<Longrightarrow> FCP f = FCP g"
|
||||||
by simp
|
by simp
|
||||||
|
|
||||||
|
lemma h_val_id:
|
||||||
|
"h_val (hrs_mem (hrs_mem_update (heap_update x y) s)) x = (y::'a::mem_type)"
|
||||||
|
apply (subst hrs_mem_update)
|
||||||
|
apply (rule h_val_heap_update)
|
||||||
|
done
|
||||||
|
|
||||||
|
lemma heap_update_id2:
|
||||||
|
"hrs_mem_update (heap_update p ((h_val (hrs_mem s) p)::'a::packed_type)) s = s"
|
||||||
|
apply (clarsimp simp:hrs_mem_update_def case_prod_beta)
|
||||||
|
apply (subst heap_update_id)
|
||||||
|
apply (simp add:hrs_mem_def)+
|
||||||
|
done
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
Loading…
Reference in New Issue