# HG changeset patch # User nipkow # Date 1056644044 -7200 # Node ID 93dfce3b6f86281e9d4afcce6cf41a4c18c8d678 # Parent 21e2ff495d81ded0f6c6dc68aa9a20e835fc1800 *** empty log message *** diff -r 21e2ff495d81 -r 93dfce3b6f86 src/HOL/Hoare/Pointer_Examples.thy --- a/src/HOL/Hoare/Pointer_Examples.thy Thu Jun 26 15:48:33 2003 +0200 +++ b/src/HOL/Hoare/Pointer_Examples.thy Thu Jun 26 18:14:04 2003 +0200 @@ -258,10 +258,51 @@ apply(clarsimp simp add:List_app) done +text{* And now with ghost variables: *} -text{* More of the proof can be automated, but the runtime goes up -drastically. In general it is usually more efficient to give the -witness directly than to have it found by proof. +lemma "VARS elem next p q r s ps qs rs a + {List next p Ps \ List next q Qs \ set Ps \ set Qs = {} \ + (p \ Null \ q \ Null) \ ps = Ps \ qs = Qs} + IF cor (q = Null) (cand (p \ Null) (p^.elem \ q^.elem)) + THEN r := p; p := p^.next; ps := tl ps + ELSE r := q; q := q^.next; qs := tl qs FI; + s := r; rs := []; a := addr s; + WHILE p \ Null \ q \ Null + INV {Path next r rs s \ List next p ps \ List next q qs \ + distinct(a # ps @ qs @ rs) \ s = Ref a \ + merge(Ps,Qs,\x y. elem x \ elem y) = + rs @ a # merge(ps,qs,\x y. elem x \ elem y) \ + (next a = p \ next a = q)} + DO IF cor (q = Null) (cand (p \ Null) (p^.elem \ q^.elem)) + THEN s^.next := p; p := p^.next; ps := tl ps + ELSE s^.next := q; q := q^.next; qs := tl qs FI; + rs := rs @ [a]; s := s^.next; a := addr s + OD + {List next r (merge(Ps,Qs,\x y. elem x \ elem y))}" +apply vcg_simp +apply (simp_all add: cand_def cor_def) + +apply (fastsimp) + +apply clarsimp +apply(rule conjI) +apply(clarsimp) +apply(rule conjI) +apply(clarsimp simp:neq_commute) +apply(clarsimp simp:neq_commute) +apply(clarsimp simp:neq_commute) + +apply(clarsimp simp add:List_app) +done + +text{* The proof is a LOT simpler because it does not need +instantiations anymore, but it is still not quite automatic, probably +because of this wrong orientation business. *} + +text{* More of the previous proof without ghost variables can be +automated, but the runtime goes up drastically. In general it is +usually more efficient to give the witness directly than to have it +found by proof. Now we try a functional version of the abstraction relation @{term Path}. Since the result is not that convincing, we do not prove any of @@ -332,47 +373,6 @@ text"The proof is automatic, but requires a numbet of special lemmas." -text{* And now with ghost variables: *} - -lemma "VARS elem next p q r s ps qs rs a - {List next p Ps \ List next q Qs \ set Ps \ set Qs = {} \ - (p \ Null \ q \ Null) \ ps = Ps \ qs = Qs} - IF cor (q = Null) (cand (p \ Null) (p^.elem \ q^.elem)) - THEN r := p; p := p^.next; ps := tl ps - ELSE r := q; q := q^.next; qs := tl qs FI; - s := r; rs := []; a := addr s; - WHILE p \ Null \ q \ Null - INV {Path next r rs s \ List next p ps \ List next q qs \ - distinct(a # ps @ qs @ rs) \ s = Ref a \ - merge(Ps,Qs,\x y. elem x \ elem y) = - rs @ a # merge(ps,qs,\x y. elem x \ elem y) \ - (next a = p \ next a = q)} - DO IF cor (q = Null) (cand (p \ Null) (p^.elem \ q^.elem)) - THEN s^.next := p; p := p^.next; ps := tl ps - ELSE s^.next := q; q := q^.next; qs := tl qs FI; - rs := rs @ [a]; s := s^.next; a := addr s - OD - {List next r (merge(Ps,Qs,\x y. elem x \ elem y))}" -apply vcg_simp -apply (simp_all add: cand_def cor_def) - -apply (fastsimp) - -apply clarsimp -apply(rule conjI) -apply(clarsimp) -apply(rule conjI) -apply(clarsimp simp:eq_sym_conv) -apply(clarsimp simp:eq_sym_conv) -apply(clarsimp simp:eq_sym_conv) - -apply(clarsimp simp add:List_app) -done - -text{* The proof is a LOT simpler because it does not need -instantiations anymore, but it is still not quite automatic, probably -because of this wrong orientation business. *} - subsection "Storage allocation" constdefs new :: "'a set \ 'a" diff -r 21e2ff495d81 -r 93dfce3b6f86 src/HOL/Hoare/SepLogHeap.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/SepLogHeap.thy Thu Jun 26 18:14:04 2003 +0200 @@ -0,0 +1,104 @@ +(* Title: HOL/Hoare/Heap.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 2002 TUM + +Heap abstractions (at the moment only Path and List) +for Separation Logic. +*) + +theory SepLogHeap = Main: + +types heap = "(nat \ nat option)" + +text{* Some means allocated, none means free. Address 0 serves as the +null reference. *} + +subsection "Paths in the heap" + +consts + Path :: "heap \ nat \ nat list \ nat \ bool" +primrec +"Path h x [] y = (x = y)" +"Path h x (a#as) y = (x\0 \ a=x \ (\b. h x = Some b \ Path h b as y))" + +lemma [iff]: "Path h 0 xs y = (xs = [] \ y = 0)" +apply(case_tac xs) +apply fastsimp +apply fastsimp +done + +lemma [simp]: "x\0 \ Path h x as z = + (as = [] \ z = x \ (\y bs. as = x#bs \ h x = Some y & Path h y bs z))" +apply(case_tac as) +apply fastsimp +apply fastsimp +done + +lemma [simp]: "\x. Path f x (as@bs) z = (\y. Path f x as y \ Path f y bs z)" +by(induct as, auto) + +lemma Path_upd[simp]: + "\x. u \ set as \ Path (f(u := v)) x as y = Path f x as y" +by(induct as, simp, simp add:eq_sym_conv) + + +subsection "Lists on the heap" + +constdefs + List :: "heap \ nat \ nat list \ bool" +"List h x as == Path h x as 0" + +lemma [simp]: "List h x [] = (x = 0)" +by(simp add:List_def) + +lemma [simp]: + "List h x (a#as) = (x\0 \ a=x \ (\y. h x = Some y \ List h y as))" +by(simp add:List_def) + +lemma [simp]: "List h 0 as = (as = [])" +by(case_tac as, simp_all) + +lemma List_non_null: "a\0 \ + List h a as = (\b bs. as = a#bs \ h a = Some b \ List h b bs)" +by(case_tac as, simp_all) + +theorem notin_List_update[simp]: + "\x. a \ set as \ List (h(a := y)) x as = List h x as" +apply(induct as) +apply simp +apply(clarsimp simp add:fun_upd_apply) +done + +lemma List_unique: "\x bs. List h x as \ List h x bs \ as = bs" +by(induct as, auto simp add:List_non_null) + +lemma List_unique1: "List h p as \ \!as. List h p as" +by(blast intro:List_unique) + +lemma List_app: "\x. List h x (as@bs) = (\y. Path h x as y \ List h y bs)" +by(induct as, auto) + +lemma List_hd_not_in_tl[simp]: "List h b as \ h a = Some b \ a \ set as" +apply (clarsimp simp add:in_set_conv_decomp) +apply(frule List_app[THEN iffD1]) +apply(fastsimp dest: List_unique) +done + +lemma List_distinct[simp]: "\x. List h x as \ distinct as" +apply(induct as, simp) +apply(fastsimp dest:List_hd_not_in_tl) +done + +lemma list_in_heap: "\p. List h p ps \ set ps \ dom h" +by(induct ps, auto) + +lemma list_ortho_sum1[simp]: + "\p. \ List h1 p ps; dom h1 \ dom h2 = {}\ \ List (h1++h2) p ps" +by(induct ps, auto simp add:map_add_def split:option.split) + +lemma list_ortho_sum2[simp]: + "\p. \ List h2 p ps; dom h1 \ dom h2 = {}\ \ List (h1++h2) p ps" +by(induct ps, auto simp add:map_add_def split:option.split) + +end diff -r 21e2ff495d81 -r 93dfce3b6f86 src/HOL/Hoare/Separation.thy --- a/src/HOL/Hoare/Separation.thy Thu Jun 26 15:48:33 2003 +0200 +++ b/src/HOL/Hoare/Separation.thy Thu Jun 26 18:14:04 2003 +0200 @@ -4,11 +4,16 @@ Copyright 2003 TUM A first attempt at a nice syntactic embedding of separation logic. +Already builds on the theory for list abstractions. + +If we suppress the H parameter for "List", we have to hardwired this +into parser and pretty printer, which is not very modular. +Alternative: some syntax like

which stands for P H. No more +compact, but avoids the funny H. + *) -theory Separation = HoareAbort: - -types heap = "(nat \ nat option)" +theory Separation = HoareAbort + SepLogHeap: text{* The semantic definition of a few connectives: *} @@ -54,6 +59,9 @@ (* free_tr takes care of free vars in the scope of sep. logic connectives: they are implicitly applied to the heap *) fun free_tr(t as Free _) = t $ Syntax.free "H" +(* + | free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps +*) | free_tr t = t fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H" @@ -107,6 +115,9 @@ local fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t +(* + | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps +*) | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t | strip (Abs(_,_,P)) = P | strip (Const("is_empty",_)) = Syntax.const "@emp" @@ -159,4 +170,53 @@ apply(simp add: star_comm) done + +lemma "VARS H + {p\0 \ [p \ x] ** List H q qs} + H := H(p \ q) + {List H p (p#qs)}" +apply vcg +apply(simp add: star_def ortho_def singl_def) +apply clarify +apply(subgoal_tac "p \ set qs") + prefer 2 + apply(blast dest:list_in_heap) +apply simp +done + +lemma "VARS H p q r + {List H p Ps ** List H q Qs} + WHILE p \ 0 + INV {\ps qs. (List H p ps ** List H q qs) \ rev ps @ qs = rev Ps @ Qs} + DO r := p; p := the(H p); H := H(r \ q); q := r OD + {List H q (rev Ps @ Qs)}" +apply vcg +apply(simp_all add: star_def ortho_def singl_def) + +apply fastsimp + +apply (clarsimp simp add:List_non_null) +apply(rename_tac ps') +apply(rule_tac x = ps' in exI) +apply(rule_tac x = "p#qs" in exI) +apply simp +apply(rule_tac x = "h1(p:=None)" in exI) +apply(rule_tac x = "h2(p\q)" in exI) +apply simp +apply(rule conjI) + apply(rule ext) + apply(simp add:map_add_def split:option.split) +apply(rule conjI) + apply blast +apply(simp add:map_add_def split:option.split) +apply(rule conjI) +apply(subgoal_tac "p \ set qs") + prefer 2 + apply(blast dest:list_in_heap) +apply(simp) +apply fast + +apply(fastsimp) +done + end