eparation logic - a beginning.
authornipkow
Wed May 14 14:20:55 2003 +0200 (2003-05-14)
changeset 14028ff6eb32b30a1
parent 14027 68d247b7b14b
child 14029 fe031a7c75bc
eparation logic - a beginning.
src/HOL/Hoare/ROOT.ML
src/HOL/Hoare/Separation.thy
     1.1 --- a/src/HOL/Hoare/ROOT.ML	Wed May 14 11:15:18 2003 +0200
     1.2 +++ b/src/HOL/Hoare/ROOT.ML	Wed May 14 14:20:55 2003 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/IMP/ROOT.ML
     1.5      ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7 -    Copyright   1998 TUM
     1.8 +    Copyright   1998-2003 TUM
     1.9  *)
    1.10  
    1.11  time_use_thy "Examples";
    1.12 @@ -10,3 +10,4 @@
    1.13  time_use_thy "Pointer_Examples";
    1.14  time_use_thy "Pointer_ExamplesAbort";
    1.15  time_use_thy "SchorrWaite";
    1.16 +time_use_thy "Separation";
     2.1 --- a/src/HOL/Hoare/Separation.thy	Wed May 14 11:15:18 2003 +0200
     2.2 +++ b/src/HOL/Hoare/Separation.thy	Wed May 14 14:20:55 2003 +0200
     2.3 @@ -145,16 +145,10 @@
     2.4  proofs. Here comes a simple example of a program proof that uses a law
     2.5  of separation logic instead. *}
     2.6  
     2.7 -(* move to Map.thy *)
     2.8 -lemma override_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
     2.9 -apply(rule ext)
    2.10 -apply(fastsimp simp:override_def split:option.split)
    2.11 -done
    2.12 -
    2.13  (* a law of separation logic *)
    2.14  lemma star_comm: "P ** Q = Q ** P"
    2.15  apply(simp add:star_def ortho_def)
    2.16 -apply(blast intro:override_comm)
    2.17 +apply(blast intro:map_add_comm)
    2.18  done
    2.19  
    2.20  lemma "VARS H x y z w