*** empty log message ***
authornipkow
Thu Jun 26 18:14:04 2003 +0200 (2003-06-26)
changeset 1407493dfce3b6f86
parent 14073 21e2ff495d81
child 14075 ab2e26ae90e3
*** empty log message ***
src/HOL/Hoare/Pointer_Examples.thy
src/HOL/Hoare/SepLogHeap.thy
src/HOL/Hoare/Separation.thy
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Thu Jun 26 15:48:33 2003 +0200
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Thu Jun 26 18:14:04 2003 +0200
     1.3 @@ -258,10 +258,51 @@
     1.4  apply(clarsimp simp add:List_app)
     1.5  done
     1.6  
     1.7 +text{* And now with ghost variables: *}
     1.8  
     1.9 -text{* More of the proof can be automated, but the runtime goes up
    1.10 -drastically. In general it is usually more efficient to give the
    1.11 -witness directly than to have it found by proof.
    1.12 +lemma "VARS elem next p q r s ps qs rs a
    1.13 + {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    1.14 +  (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
    1.15 + IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.16 + THEN r := p; p := p^.next; ps := tl ps
    1.17 + ELSE r := q; q := q^.next; qs := tl qs FI;
    1.18 + s := r; rs := []; a := addr s;
    1.19 + WHILE p \<noteq> Null \<or> q \<noteq> Null
    1.20 + INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
    1.21 +      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
    1.22 +      merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
    1.23 +      rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
    1.24 +      (next a = p \<or> next a = q)}
    1.25 + DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.26 +    THEN s^.next := p; p := p^.next; ps := tl ps
    1.27 +    ELSE s^.next := q; q := q^.next; qs := tl qs FI;
    1.28 +    rs := rs @ [a]; s := s^.next; a := addr s
    1.29 + OD
    1.30 + {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
    1.31 +apply vcg_simp
    1.32 +apply (simp_all add: cand_def cor_def)
    1.33 +
    1.34 +apply (fastsimp)
    1.35 +
    1.36 +apply clarsimp
    1.37 +apply(rule conjI)
    1.38 +apply(clarsimp)
    1.39 +apply(rule conjI)
    1.40 +apply(clarsimp simp:neq_commute)
    1.41 +apply(clarsimp simp:neq_commute)
    1.42 +apply(clarsimp simp:neq_commute)
    1.43 +
    1.44 +apply(clarsimp simp add:List_app)
    1.45 +done
    1.46 +
    1.47 +text{* The proof is a LOT simpler because it does not need
    1.48 +instantiations anymore, but it is still not quite automatic, probably
    1.49 +because of this wrong orientation business. *}
    1.50 +
    1.51 +text{* More of the previous proof without ghost variables can be
    1.52 +automated, but the runtime goes up drastically. In general it is
    1.53 +usually more efficient to give the witness directly than to have it
    1.54 +found by proof.
    1.55  
    1.56  Now we try a functional version of the abstraction relation @{term
    1.57  Path}. Since the result is not that convincing, we do not prove any of
    1.58 @@ -332,47 +373,6 @@
    1.59  
    1.60  text"The proof is automatic, but requires a numbet of special lemmas."
    1.61  
    1.62 -text{* And now with ghost variables: *}
    1.63 -
    1.64 -lemma "VARS elem next p q r s ps qs rs a
    1.65 - {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    1.66 -  (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
    1.67 - IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.68 - THEN r := p; p := p^.next; ps := tl ps
    1.69 - ELSE r := q; q := q^.next; qs := tl qs FI;
    1.70 - s := r; rs := []; a := addr s;
    1.71 - WHILE p \<noteq> Null \<or> q \<noteq> Null
    1.72 - INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
    1.73 -      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
    1.74 -      merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
    1.75 -      rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
    1.76 -      (next a = p \<or> next a = q)}
    1.77 - DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.78 -    THEN s^.next := p; p := p^.next; ps := tl ps
    1.79 -    ELSE s^.next := q; q := q^.next; qs := tl qs FI;
    1.80 -    rs := rs @ [a]; s := s^.next; a := addr s
    1.81 - OD
    1.82 - {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
    1.83 -apply vcg_simp
    1.84 -apply (simp_all add: cand_def cor_def)
    1.85 -
    1.86 -apply (fastsimp)
    1.87 -
    1.88 -apply clarsimp
    1.89 -apply(rule conjI)
    1.90 -apply(clarsimp)
    1.91 -apply(rule conjI)
    1.92 -apply(clarsimp simp:eq_sym_conv)
    1.93 -apply(clarsimp simp:eq_sym_conv)
    1.94 -apply(clarsimp simp:eq_sym_conv)
    1.95 -
    1.96 -apply(clarsimp simp add:List_app)
    1.97 -done
    1.98 -
    1.99 -text{* The proof is a LOT simpler because it does not need
   1.100 -instantiations anymore, but it is still not quite automatic, probably
   1.101 -because of this wrong orientation business. *}
   1.102 -
   1.103  subsection "Storage allocation"
   1.104  
   1.105  constdefs new :: "'a set \<Rightarrow> 'a"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Hoare/SepLogHeap.thy	Thu Jun 26 18:14:04 2003 +0200
     2.3 @@ -0,0 +1,104 @@
     2.4 +(*  Title:      HOL/Hoare/Heap.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   2002 TUM
     2.8 +
     2.9 +Heap abstractions (at the moment only Path and List)
    2.10 +for Separation Logic.
    2.11 +*)
    2.12 +
    2.13 +theory SepLogHeap = Main:
    2.14 +
    2.15 +types heap = "(nat \<Rightarrow> nat option)"
    2.16 +
    2.17 +text{* Some means allocated, none means free. Address 0 serves as the
    2.18 +null reference. *}
    2.19 +
    2.20 +subsection "Paths in the heap"
    2.21 +
    2.22 +consts
    2.23 + Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
    2.24 +primrec
    2.25 +"Path h x [] y = (x = y)"
    2.26 +"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))"
    2.27 +
    2.28 +lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
    2.29 +apply(case_tac xs)
    2.30 +apply fastsimp
    2.31 +apply fastsimp
    2.32 +done
    2.33 +
    2.34 +lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z =
    2.35 + (as = [] \<and> z = x  \<or>  (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))"
    2.36 +apply(case_tac as)
    2.37 +apply fastsimp
    2.38 +apply fastsimp
    2.39 +done
    2.40 +
    2.41 +lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
    2.42 +by(induct as, auto)
    2.43 +
    2.44 +lemma Path_upd[simp]:
    2.45 + "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
    2.46 +by(induct as, simp, simp add:eq_sym_conv)
    2.47 +
    2.48 +
    2.49 +subsection "Lists on the heap"
    2.50 +
    2.51 +constdefs
    2.52 + List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
    2.53 +"List h x as == Path h x as 0"
    2.54 +
    2.55 +lemma [simp]: "List h x [] = (x = 0)"
    2.56 +by(simp add:List_def)
    2.57 +
    2.58 +lemma [simp]:
    2.59 + "List h x (a#as) = (x\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> List h y as))"
    2.60 +by(simp add:List_def)
    2.61 +
    2.62 +lemma [simp]: "List h 0 as = (as = [])"
    2.63 +by(case_tac as, simp_all)
    2.64 +
    2.65 +lemma List_non_null: "a\<noteq>0 \<Longrightarrow>
    2.66 + List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)"
    2.67 +by(case_tac as, simp_all)
    2.68 +
    2.69 +theorem notin_List_update[simp]:
    2.70 + "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
    2.71 +apply(induct as)
    2.72 +apply simp
    2.73 +apply(clarsimp simp add:fun_upd_apply)
    2.74 +done
    2.75 +
    2.76 +lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
    2.77 +by(induct as, auto simp add:List_non_null)
    2.78 +
    2.79 +lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
    2.80 +by(blast intro:List_unique)
    2.81 +
    2.82 +lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
    2.83 +by(induct as, auto)
    2.84 +
    2.85 +lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as"
    2.86 +apply (clarsimp simp add:in_set_conv_decomp)
    2.87 +apply(frule List_app[THEN iffD1])
    2.88 +apply(fastsimp dest: List_unique)
    2.89 +done
    2.90 +
    2.91 +lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
    2.92 +apply(induct as, simp)
    2.93 +apply(fastsimp dest:List_hd_not_in_tl)
    2.94 +done
    2.95 +
    2.96 +lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h"
    2.97 +by(induct ps, auto)
    2.98 +
    2.99 +lemma list_ortho_sum1[simp]:
   2.100 + "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
   2.101 +by(induct ps, auto simp add:map_add_def split:option.split)
   2.102 +
   2.103 +lemma list_ortho_sum2[simp]:
   2.104 + "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
   2.105 +by(induct ps, auto simp add:map_add_def split:option.split)
   2.106 +
   2.107 +end
     3.1 --- a/src/HOL/Hoare/Separation.thy	Thu Jun 26 15:48:33 2003 +0200
     3.2 +++ b/src/HOL/Hoare/Separation.thy	Thu Jun 26 18:14:04 2003 +0200
     3.3 @@ -4,11 +4,16 @@
     3.4      Copyright   2003 TUM
     3.5  
     3.6  A first attempt at a nice syntactic embedding of separation logic.
     3.7 +Already builds on the theory for list abstractions.
     3.8 +
     3.9 +If we suppress the H parameter for "List", we have to hardwired this
    3.10 +into parser and pretty printer, which is not very modular.
    3.11 +Alternative: some syntax like <P> which stands for P H. No more
    3.12 +compact, but avoids the funny H.
    3.13 +
    3.14  *)
    3.15  
    3.16 -theory Separation = HoareAbort:
    3.17 -
    3.18 -types heap = "(nat \<Rightarrow> nat option)"
    3.19 +theory Separation = HoareAbort + SepLogHeap:
    3.20  
    3.21  text{* The semantic definition of a few connectives: *}
    3.22  
    3.23 @@ -54,6 +59,9 @@
    3.24  (* free_tr takes care of free vars in the scope of sep. logic connectives:
    3.25     they are implicitly applied to the heap *)
    3.26  fun free_tr(t as Free _) = t $ Syntax.free "H"
    3.27 +(*
    3.28 +  | free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps
    3.29 +*)
    3.30    | free_tr t = t
    3.31  
    3.32  fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
    3.33 @@ -107,6 +115,9 @@
    3.34  local
    3.35  fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
    3.36    | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
    3.37 +(*
    3.38 +  | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps
    3.39 +*)
    3.40    | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
    3.41    | strip (Abs(_,_,P)) = P
    3.42    | strip (Const("is_empty",_)) = Syntax.const "@emp"
    3.43 @@ -159,4 +170,53 @@
    3.44  apply(simp add: star_comm)
    3.45  done
    3.46  
    3.47 +
    3.48 +lemma "VARS H
    3.49 + {p\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs}
    3.50 + H := H(p \<mapsto> q)
    3.51 + {List H p (p#qs)}"
    3.52 +apply vcg
    3.53 +apply(simp add: star_def ortho_def singl_def)
    3.54 +apply clarify
    3.55 +apply(subgoal_tac "p \<notin> set qs")
    3.56 + prefer 2
    3.57 + apply(blast dest:list_in_heap)
    3.58 +apply simp
    3.59 +done
    3.60 +
    3.61 +lemma "VARS H p q r
    3.62 +  {List H p Ps ** List H q Qs}
    3.63 +  WHILE p \<noteq> 0
    3.64 +  INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs}
    3.65 +  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
    3.66 +  {List H q (rev Ps @ Qs)}"
    3.67 +apply vcg
    3.68 +apply(simp_all add: star_def ortho_def singl_def)
    3.69 +
    3.70 +apply fastsimp
    3.71 +
    3.72 +apply (clarsimp simp add:List_non_null)
    3.73 +apply(rename_tac ps')
    3.74 +apply(rule_tac x = ps' in exI)
    3.75 +apply(rule_tac x = "p#qs" in exI)
    3.76 +apply simp
    3.77 +apply(rule_tac x = "h1(p:=None)" in exI)
    3.78 +apply(rule_tac x = "h2(p\<mapsto>q)" in exI)
    3.79 +apply simp
    3.80 +apply(rule conjI)
    3.81 + apply(rule ext)
    3.82 + apply(simp add:map_add_def split:option.split)
    3.83 +apply(rule conjI)
    3.84 + apply blast
    3.85 +apply(simp add:map_add_def split:option.split)
    3.86 +apply(rule conjI)
    3.87 +apply(subgoal_tac "p \<notin> set qs")
    3.88 + prefer 2
    3.89 + apply(blast dest:list_in_heap)
    3.90 +apply(simp)
    3.91 +apply fast
    3.92 +
    3.93 +apply(fastsimp)
    3.94 +done
    3.95 +
    3.96  end