src/HOL/Hoare/Separation.thy
changeset 13857 11d7c5a8dbb7
child 13867 1fdecd15437f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare/Separation.thy	Tue Mar 11 15:04:24 2003 +0100
     1.3 @@ -0,0 +1,90 @@
     1.4 +theory Separation = HoareAbort:
     1.5 +
     1.6 +types heap = "(nat \<Rightarrow> nat option)"
     1.7 +
     1.8 +
     1.9 +text{* The semantic definition of a few connectives: *}
    1.10 +
    1.11 +constdefs
    1.12 + R:: "heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> bool"
    1.13 +"R h h1 h2 == dom h1 \<inter> dom h2 = {} \<and> h = h1 ++ h2"
    1.14 +
    1.15 + star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
    1.16 +"star P Q == \<lambda>h. \<exists>h1 h2. R h h1 h2 \<and> P h1 \<and> Q h2"
    1.17 +
    1.18 + singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    1.19 +"singl h x y == dom h = {x} & h x = Some y"
    1.20 +
    1.21 +lemma "VARS x y z w h
    1.22 + {star (%h. singl h x y) (%h. singl h z w) h}
    1.23 + SKIP
    1.24 + {x \<noteq> z}"
    1.25 +apply vcg
    1.26 +apply(auto simp:star_def R_def singl_def)
    1.27 +done
    1.28 +
    1.29 +text{* To suppress the heap parameter of the connectives, we assume it
    1.30 +is always called H and add/remove it upon parsing/printing. Thus
    1.31 +every pointer program needs to have a program variable H, and
    1.32 +assertions should not contain any locally bound Hs - otherwise they
    1.33 +may bind the implicit H. *}
    1.34 +
    1.35 +text{* Nice input syntax: *}
    1.36 +
    1.37 +syntax
    1.38 + "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
    1.39 + "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
    1.40 +
    1.41 +ML{*
    1.42 +fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
    1.43 +  | singl_tr ts = raise TERM ("singl_tr", ts);
    1.44 +fun star_tr [P,Q] = Syntax.const "star" $
    1.45 +      absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
    1.46 +  | star_tr ts = raise TERM ("star_tr", ts);
    1.47 +*}
    1.48 +
    1.49 +parse_translation {* [("@singl", singl_tr),("@star", star_tr)] *}
    1.50 +
    1.51 +lemma "VARS H x y z w
    1.52 + {[x\<mapsto>y] ** [z\<mapsto>w]}
    1.53 + SKIP
    1.54 + {x \<noteq> z}"
    1.55 +apply vcg
    1.56 +apply(auto simp:star_def R_def singl_def)
    1.57 +done
    1.58 +
    1.59 +text{* Nice output syntax: *}
    1.60 +
    1.61 +ML{*
    1.62 +fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
    1.63 +fun star_tr' [Abs(_,_,P),Abs(_,_,Q),_] = Syntax.const "@star" $ P $ Q
    1.64 +*}
    1.65 +
    1.66 +print_translation {* [("singl", singl_tr'),("star", star_tr')] *}
    1.67 +
    1.68 +lemma "VARS H x y z w
    1.69 + {[x\<mapsto>y] ** [z\<mapsto>w]}
    1.70 + SKIP
    1.71 + {x \<noteq> z}"
    1.72 +apply vcg
    1.73 +apply(auto simp:star_def R_def singl_def)
    1.74 +done
    1.75 +
    1.76 +
    1.77 +consts llist :: "(heap * nat)set"
    1.78 +inductive llist
    1.79 +intros
    1.80 +empty: "(%n. None, 0) : llist"
    1.81 +cons: "\<lbrakk> R h h1 h2; pto h1 p q; (h2,q):llist \<rbrakk> \<Longrightarrow> (h,p):llist"
    1.82 +
    1.83 +lemma "VARS p q h
    1.84 + {(h,p) : llist}
    1.85 + h := h(q \<mapsto> p)
    1.86 + {(h,q) : llist}"
    1.87 +apply vcg
    1.88 +apply(rule_tac "h1.0" = "%n. if n=q then Some p else None" in llist.cons)
    1.89 +prefer 3 apply assumption
    1.90 +prefer 2 apply(simp add:singl_def dom_def)
    1.91 +apply(simp add:R_def dom_def)
    1.92 +
    1.93 +