Re: [isabelle] Norrish's C-parser and structs
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
> 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":
Thanks for this lemma; this allows me indeed to make some progress.
This archive was generated by a fusion of
Pipermail (Mailman edition) and