Re: [isabelle] Norrish's C-parser and structs



On 11.01.2013 14:33, David Greenaway wrote:
I found to make much progress with Tuch's framework, I needed the
following lemma (the proof is long and ugly, most of it hastily clagged
from Tuch's proof of "lift_typ_heap_mono":

lemma h_val_field_from_bytes:
"\<lbrakk> field_ti TYPE('a::{mem_type}) f = Some t;
export_uinfo t = export_uinfo (typ_info_t TYPE('b::{mem_type}))
\<rbrakk> \<Longrightarrow>
h_val (hrs_mem h) (Ptr &(pa\<rightarrow>f) :: 'b ptr) = from_bytes
(access_ti\<^isub>0 t (h_val (hrs_mem h) pa))"

This Lemma has been very useful for me. Maybe it should be part of the Framework?

I feel there should be a similar lemma for field updates, too. Maybe something along the lines of

lemma h_val_update:
  fixes h val f p
  defines "h' ≡ hrs_mem_update (heap_update (Ptr &(p→f) :: 'b ptr) val) h"
  assumes fl: "field_ti TYPE('a::{mem_type}) f = Some t"
  assumes "export_uinfo t = export_uinfo (typ_info_t TYPE('b::{mem_type}))"
  shows "h_val (hrs_mem h') p =
update_ti_t t (to_bytes val (replicate (size_td t) 0)) (h_val (hrs_mem h) p)"

Has somebody proved something similar already?

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.