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



Hi David,

On 11.01.2013 14:33, David Greenaway wrote:
On 11/01/13 03:59, Lars Noschinski wrote:
[...]
 > This leaves me with the following subgoal, which I am not able to
 > prove:
 >
 > 1. ⋀globals x a.
 > lift_t⇡c (hrs_mem (t_hrs_' globals), hrs_htd (t_hrs_' globals)) x =
Some a ⟹
 > h_val (hrs_mem (t_hrs_' globals)) (Ptr &(x→[''cnt_C''])) = cnt_C a
 >
 > So, how do I relate the projections of an abstracted struct to a field
 > with the pointer access to said field of the concrete struct?

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:
[...]

Thanks for this lemma; this allows me indeed to make some progress.

  -- Lars





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