# HG changeset patch # User nipkow # Date 1021046448 -7200 # Node ID 03d20664cb792ce6b99b38319579d06af703eee7 # Parent d7f33559f871ed9b12272ef325138f32e283e6aa A new theory of pointer program examples diff -r d7f33559f871 -r 03d20664cb79 src/HOL/Hoare/Pointers.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Pointers.thy Fri May 10 18:00:48 2002 +0200 @@ -0,0 +1,128 @@ +(* Title: HOL/Hoare/Pointers.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 2002 TUM + +How to use Hoare logic to verify pointer manipulating programs. +The old idea: the store is a global mapping from pointers to values. +Pointers are modelled by type 'a option, where None is Nil. +Thus the heap is of type 'a \ 'a (see theory Map). + +The List reversal example is taken from Richard Bornat's paper +Proving pointer programs in Hoare logic +What's new? We formalize the foundations, ie the abstraction from the pointer +chains to HOL lists. This is merely axiomatized by Bornat. +*) + +theory Pointers = Hoare: + +section"The heap" + +subsection"Paths in the heap" + +consts + path :: "('a \ 'a) \ 'a option \ 'a list \ 'a option \ bool" +primrec +"path h x [] y = (x = y)" +"path h x (a#as) y = (x = Some a \ path h (h a) as y)" + +(* useful? +lemma [simp]: "!x. reach h x (as @ [a]) (h a) = reach h x as (Some a)" +apply(induct_tac as) +apply(clarsimp) +apply(clarsimp) +done +*) + +subsection "Lists on the heap" + +constdefs + list :: "('a \ 'a) \ 'a option \ 'a list \ bool" +"list h x as == path h x as None" + +lemma [simp]: "list h x [] = (x = None)" +by(simp add:list_def) + +lemma [simp]: "list h x (a#as) = (x = Some a \ list h (h a) as)" +by(simp add:list_def) + +lemma [simp]: "list h None as = (as = [])" +by(case_tac as, simp_all) + +lemma [simp]: "list h (Some a) as = (\bs. as = a#bs \ list h (h a) bs)" +by(case_tac as, simp_all, fast) + + +declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp] + +lemma list_unique: "\x bs. list h x as \ list h x bs \ as = bs" +by(induct as, simp, clarsimp) + +lemma list_app: "\x. list h x (as@bs) = (\y. path h x as y \ list h y bs)" +by(induct as, simp, clarsimp) + +lemma list_hd_not_in_tl: "list h (h a) as \ a \ set as" +apply (clarsimp simp add:in_set_conv_decomp) +apply(frule list_app[THEN iffD1]) +apply(fastsimp dest:list_app[THEN iffD1] list_unique) +done + +lemma list_distinct: "\x. list h x as \ distinct as" +apply(induct as, simp) +apply(fastsimp dest:list_hd_not_in_tl) +done + +theorem notin_list_update[rule_format,simp]: + "\x. a \ set as \ list (h(a := y)) x as = list h x as" +apply(induct_tac as) +apply simp +apply(simp add:fun_upd_apply) +done + +lemma [simp]: "list h (h a) as \ list (h(a := y)) (h a) as" +by(simp add:list_hd_not_in_tl) +(* Note that the opposite direction does NOT hold: + If h = (a \ Some a) + then list (h(a := None)) (h a) [a] + but not list h (h a) [] (because h is cyclic) +*) + +section"Hoare logic" + +(* This should already be done in Hoare.thy, which should be converted to +Isar *) + +method_setup vcg_simp_tac = {* + Method.no_args + (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac Asm_full_simp_tac)) *} + "verification condition generator plus simplification" + +subsection"List reversal" + +lemma "|- VARS tl p q r. + {list tl p As \ list tl q Bs \ set As \ set Bs = {}} + WHILE p ~= None + INV {\As' Bs'. list tl p As' \ list tl q Bs' \ set As' \ set Bs' = {} \ + rev As' @ Bs' = rev As @ Bs} + DO r := p; p := tl(the p); tl := tl(the r := q); q := r OD + {list tl q (rev As @ Bs)}" +apply vcg_simp_tac + +apply(rule_tac x = As in exI) +apply simp + +prefer 2 +apply clarsimp + +apply clarify +apply(rename_tac As' b Bs') +apply(frule list_distinct) +apply clarsimp +apply(rename_tac As'') +apply(rule_tac x = As'' in exI) +apply simp +apply(rule_tac x = "b#Bs'" in exI) +apply simp +done + +end