src/HOL/Hoare/Separation.thy
author wenzelm
Wed, 11 Aug 2010 18:41:06 +0200
changeset 38353 d98baa2cf589
parent 35416 d8d7d1b785af
child 44241 7943b69f0188
permissions -rw-r--r--
modernized specifications; tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
     1
(*  Title:      HOL/Hoare/Separation.thy
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
     2
    Author:     Tobias Nipkow
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
     3
    Copyright   2003 TUM
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
     4
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
     5
A first attempt at a nice syntactic embedding of separation logic.
14074
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
     6
Already builds on the theory for list abstractions.
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
     7
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
     8
If we suppress the H parameter for "List", we have to hardwired this
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
     9
into parser and pretty printer, which is not very modular.
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
    10
Alternative: some syntax like <P> which stands for P H. No more
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
    11
compact, but avoids the funny H.
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
    12
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    13
*)
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    14
35316
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 35113
diff changeset
    15
theory Separation imports Hoare_Logic_Abort SepLogHeap begin
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    16
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    17
text{* The semantic definition of a few connectives: *}
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    18
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    19
definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    20
  where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    21
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    22
definition is_empty :: "heap \<Rightarrow> bool"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    23
  where "is_empty h \<longleftrightarrow> h = empty"
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    24
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    25
definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    26
  where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    27
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    28
definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    29
  where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    30
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    31
definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    32
  where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    33
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    34
text{*This is what assertions look like without any syntactic sugar: *}
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    35
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    36
lemma "VARS x y z w h
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    37
 {star (%h. singl h x y) (%h. singl h z w) h}
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    38
 SKIP
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    39
 {x \<noteq> z}"
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    40
apply vcg
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    41
apply(auto simp:star_def ortho_def singl_def)
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    42
done
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    43
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    44
text{* Now we add nice input syntax.  To suppress the heap parameter
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    45
of the connectives, we assume it is always called H and add/remove it
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    46
upon parsing/printing. Thus every pointer program needs to have a
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    47
program variable H, and assertions should not contain any locally
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    48
bound Hs - otherwise they may bind the implicit H. *}
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    49
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    50
syntax
35101
6ce9177d6b38 modernized translations;
wenzelm
parents: 18447
diff changeset
    51
 "_emp" :: "bool" ("emp")
6ce9177d6b38 modernized translations;
wenzelm
parents: 18447
diff changeset
    52
 "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
6ce9177d6b38 modernized translations;
wenzelm
parents: 18447
diff changeset
    53
 "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
6ce9177d6b38 modernized translations;
wenzelm
parents: 18447
diff changeset
    54
 "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    55
17781
32bb237158a5 print_translation: does not handle _idtdummy;
wenzelm
parents: 16417
diff changeset
    56
(* FIXME does not handle "_idtdummy" *)
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    57
ML{*
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    58
(* free_tr takes care of free vars in the scope of sep. logic connectives:
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    59
   they are implicitly applied to the heap *)
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    60
fun free_tr(t as Free _) = t $ Syntax.free "H"
14074
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
    61
(*
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
    62
  | free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
    63
*)
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    64
  | free_tr t = t
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    65
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    66
fun emp_tr [] = Syntax.const @{const_syntax is_empty} $ Syntax.free "H"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    67
  | emp_tr ts = raise TERM ("emp_tr", ts);
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    68
fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    69
  | singl_tr ts = raise TERM ("singl_tr", ts);
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    70
fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    71
      absfree ("H", dummyT, free_tr P) $ absfree ("H", dummyT, free_tr Q) $
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    72
      Syntax.free "H"
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    73
  | star_tr ts = raise TERM ("star_tr", ts);
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    74
fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    75
      absfree ("H", dummyT, P) $ absfree ("H", dummyT, Q) $ Syntax.free "H"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    76
  | wand_tr ts = raise TERM ("wand_tr", ts);
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    77
*}
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    78
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    79
parse_translation {*
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    80
 [(@{syntax_const "_emp"}, emp_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    81
  (@{syntax_const "_singl"}, singl_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    82
  (@{syntax_const "_star"}, star_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    83
  (@{syntax_const "_wand"}, wand_tr)]
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
    84
*}
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    85
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    86
text{* Now it looks much better: *}
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
    87
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    88
lemma "VARS H x y z w
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    89
 {[x\<mapsto>y] ** [z\<mapsto>w]}
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    90
 SKIP
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    91
 {x \<noteq> z}"
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
    92
apply vcg
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    93
apply(auto simp:star_def ortho_def singl_def)
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    94
done
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    95
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    96
lemma "VARS H x y z w
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    97
 {emp ** emp}
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    98
 SKIP
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
    99
 {emp}"
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   100
apply vcg
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   101
apply(auto simp:star_def ortho_def is_empty_def)
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   102
done
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   103
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   104
text{* But the output is still unreadable. Thus we also strip the heap
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   105
parameters upon output: *}
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   106
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   107
ML {*
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   108
local
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   109
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   110
fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   111
  | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
14074
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   112
(*
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   113
  | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   114
*)
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   115
  | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   116
  | strip (Abs(_,_,P)) = P
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   117
  | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   118
  | strip t = t;
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   119
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   120
in
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   121
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   122
fun is_empty_tr' [_] = Syntax.const @{syntax_const "_emp"}
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   123
fun singl_tr' [_,p,q] = Syntax.const @{syntax_const "_singl"} $ p $ q
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   124
fun star_tr' [P,Q,_] = Syntax.const @{syntax_const "_star"} $ strip P $ strip Q
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   125
fun wand_tr' [P,Q,_] = Syntax.const @{syntax_const "_wand"} $ strip P $ strip Q
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   126
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   127
end
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   128
*}
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   129
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   130
print_translation {*
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   131
 [(@{const_syntax is_empty}, is_empty_tr'),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   132
  (@{const_syntax singl}, singl_tr'),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   133
  (@{const_syntax star}, star_tr'),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   134
  (@{const_syntax wand}, wand_tr')]
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35101
diff changeset
   135
*}
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   136
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   137
text{* Now the intermediate proof states are also readable: *}
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   138
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   139
lemma "VARS H x y z w
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   140
 {[x\<mapsto>y] ** [z\<mapsto>w]}
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 13857
diff changeset
   141
 y := w
13857
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   142
 {x \<noteq> z}"
11d7c5a8dbb7 *** empty log message ***
nipkow
parents:
diff changeset
   143
apply vcg
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   144
apply(auto simp:star_def ortho_def singl_def)
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   145
done
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   146
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   147
lemma "VARS H x y z w
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   148
 {emp ** emp}
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   149
 SKIP
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   150
 {emp}"
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   151
apply vcg
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   152
apply(auto simp:star_def ortho_def is_empty_def)
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   153
done
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   154
13903
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   155
text{* So far we have unfolded the separation logic connectives in
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   156
proofs. Here comes a simple example of a program proof that uses a law
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   157
of separation logic instead. *}
ad1c28671a93 First working version
nipkow
parents: 13875
diff changeset
   158
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   159
(* a law of separation logic *)
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   160
lemma star_comm: "P ** Q = Q ** P"
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17781
diff changeset
   161
  by(auto simp add:star_def ortho_def dest: map_add_comm)
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   162
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   163
lemma "VARS H x y z w
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   164
 {P ** Q}
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   165
 SKIP
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   166
 {Q ** P}"
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   167
apply vcg
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   168
apply(simp add: star_comm)
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   169
done
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   170
14074
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   171
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   172
lemma "VARS H
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   173
 {p\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs}
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   174
 H := H(p \<mapsto> q)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   175
 {List H p (p#qs)}"
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   176
apply vcg
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   177
apply(simp add: star_def ortho_def singl_def)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   178
apply clarify
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   179
apply(subgoal_tac "p \<notin> set qs")
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   180
 prefer 2
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   181
 apply(blast dest:list_in_heap)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   182
apply simp
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   183
done
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   184
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   185
lemma "VARS H p q r
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   186
  {List H p Ps ** List H q Qs}
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   187
  WHILE p \<noteq> 0
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   188
  INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs}
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   189
  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   190
  {List H q (rev Ps @ Qs)}"
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   191
apply vcg
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   192
apply(simp_all add: star_def ortho_def singl_def)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   193
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   194
apply fastsimp
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   195
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   196
apply (clarsimp simp add:List_non_null)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   197
apply(rename_tac ps')
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   198
apply(rule_tac x = ps' in exI)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   199
apply(rule_tac x = "p#qs" in exI)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   200
apply simp
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   201
apply(rule_tac x = "h1(p:=None)" in exI)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   202
apply(rule_tac x = "h2(p\<mapsto>q)" in exI)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   203
apply simp
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   204
apply(rule conjI)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   205
 apply(rule ext)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   206
 apply(simp add:map_add_def split:option.split)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   207
apply(rule conjI)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   208
 apply blast
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   209
apply(simp add:map_add_def split:option.split)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   210
apply(rule conjI)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   211
apply(subgoal_tac "p \<notin> set qs")
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   212
 prefer 2
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   213
 apply(blast dest:list_in_heap)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   214
apply(simp)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   215
apply fast
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   216
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   217
apply(fastsimp)
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   218
done
93dfce3b6f86 *** empty log message ***
nipkow
parents: 14028
diff changeset
   219
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13867
diff changeset
   220
end