--- 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 \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
+ (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
+ IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> 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 \<noteq> Null \<or> q \<noteq> Null
+ INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
+ distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
+ merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
+ rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
+ (next a = p \<or> next a = q)}
+ DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> 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,\<lambda>x y. elem x \<le> 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 \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
- (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
- IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> 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 \<noteq> Null \<or> q \<noteq> Null
- INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
- distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
- merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
- rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
- (next a = p \<or> next a = q)}
- DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> 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,\<lambda>x y. elem x \<le> 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 \<Rightarrow> 'a"
--- /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 \<Rightarrow> nat option)"
+
+text{* Some means allocated, none means free. Address 0 serves as the
+null reference. *}
+
+subsection "Paths in the heap"
+
+consts
+ Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
+primrec
+"Path h x [] y = (x = y)"
+"Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
+
+lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
+apply(case_tac xs)
+apply fastsimp
+apply fastsimp
+done
+
+lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z =
+ (as = [] \<and> z = x \<or> (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))"
+apply(case_tac as)
+apply fastsimp
+apply fastsimp
+done
+
+lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
+by(induct as, auto)
+
+lemma Path_upd[simp]:
+ "\<And>x. u \<notin> set as \<Longrightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 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\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> 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\<noteq>0 \<Longrightarrow>
+ List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)"
+by(case_tac as, simp_all)
+
+theorem notin_List_update[simp]:
+ "\<And>x. a \<notin> set as \<Longrightarrow> 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: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
+by(induct as, auto simp add:List_non_null)
+
+lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
+by(blast intro:List_unique)
+
+lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
+by(induct as, auto)
+
+lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> 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]: "\<And>x. List h x as \<Longrightarrow> distinct as"
+apply(induct as, simp)
+apply(fastsimp dest:List_hd_not_in_tl)
+done
+
+lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h"
+by(induct ps, auto)
+
+lemma list_ortho_sum1[simp]:
+ "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
+by(induct ps, auto simp add:map_add_def split:option.split)
+
+lemma list_ortho_sum2[simp]:
+ "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
+by(induct ps, auto simp add:map_add_def split:option.split)
+
+end
--- 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 <P> which stands for P H. No more
+compact, but avoids the funny H.
+
*)
-theory Separation = HoareAbort:
-
-types heap = "(nat \<Rightarrow> 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\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs}
+ H := H(p \<mapsto> q)
+ {List H p (p#qs)}"
+apply vcg
+apply(simp add: star_def ortho_def singl_def)
+apply clarify
+apply(subgoal_tac "p \<notin> 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 \<noteq> 0
+ INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs}
+ DO r := p; p := the(H p); H := H(r \<mapsto> 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\<mapsto>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 \<notin> set qs")
+ prefer 2
+ apply(blast dest:list_in_heap)
+apply(simp)
+apply fast
+
+apply(fastsimp)
+done
+
end