*To*: cl-isabelle-users at lists.cam.ac.uk, Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] Norrish's C-parser and structs*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Tue, 26 Feb 2013 18:03:07 +1100*In-reply-to*: <51273FF8.6010102@in.tum.de>*References*: <50EEF369.5030005@in.tum.de> <50F014B7.8020609@nicta.com.au> <51273FF8.6010102@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

Hello Lars.

lemma lift_t_h_val: "lift_t g hp p = Some x ==> h_val (hrs_mem hp) p = x" apply (cases hp) apply (rule lift_t_lift[unfolded lift_def]) apply (simp add: hrs_mem_def) done thm lift_t_h_val[OF trans, OF lift_t_hrs_mem_update_fld[THEN fun_cong]]

Yours, Thomas.

I feel there should be a similar lemma for field updates, too. Maybesomething along the lines oflemma h_val_update: fixes h val f pdefines "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_tTYPE('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

**References**:**Re: [isabelle] Norrish's C-parser and structs***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Suggesting to add common isabelle user questions to the wiki
- Next by Date: Re: [isabelle] Isabelle Community (was "stackexchange.com use for proof assistants and related software")
- Previous by Thread: Re: [isabelle] Norrish's C-parser and structs
- Next by Thread: [isabelle] AI4FM 2013 : First Call For Papers (ITP 2013 workshop)
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list