src/HOL/Hoare/SchorrWaite.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 62042 6c6ccf573479
child 67410 64d928bacddd
permissions -rw-r--r--
tuned: each session has at most one defining entry;
mehta@13820
     1
(*  Title:      HOL/Hoare/SchorrWaite.thy
mehta@13820
     2
    Author:     Farhad Mehta
mehta@13820
     3
    Copyright   2003 TUM
mehta@13820
     4
mehta@13820
     5
Proof of the Schorr-Waite graph marking algorithm.
mehta@13820
     6
*)
mehta@13820
     7
mehta@13820
     8
haftmann@16417
     9
theory SchorrWaite imports HeapSyntax begin
mehta@13820
    10
wenzelm@62042
    11
section \<open>Machinery for the Schorr-Waite proof\<close>
mehta@13820
    12
wenzelm@36866
    13
definition
wenzelm@62042
    14
  \<comment> "Relations induced by a mapping"
mehta@13820
    15
  rel :: "('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
wenzelm@36866
    16
  where "rel m = {(x,y). m x = Ref y}"
wenzelm@36866
    17
wenzelm@36866
    18
definition
mehta@13820
    19
  relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
wenzelm@60585
    20
  where "relS M = (\<Union>m \<in> M. rel m)"
wenzelm@36866
    21
wenzelm@36866
    22
definition
mehta@13820
    23
  addrs :: "'a ref set \<Rightarrow> 'a set"
wenzelm@36866
    24
  where "addrs P = {a. Ref a \<in> P}"
wenzelm@36866
    25
wenzelm@36866
    26
definition
mehta@13820
    27
  reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> 'a set"
wenzelm@36866
    28
  where "reachable r P = (r\<^sup>* `` addrs P)"
mehta@13820
    29
mehta@13820
    30
lemmas rel_defs = relS_def rel_def
mehta@13820
    31
wenzelm@62042
    32
text \<open>Rewrite rules for relations induced by a mapping\<close>
mehta@13820
    33
mehta@13820
    34
lemma self_reachable: "b \<in> B \<Longrightarrow> b \<in> R\<^sup>* `` B"
mehta@13820
    35
apply blast
mehta@13820
    36
done
mehta@13820
    37
mehta@13820
    38
lemma oneStep_reachable: "b \<in> R``B \<Longrightarrow> b \<in> R\<^sup>* `` B"
mehta@13820
    39
apply blast
mehta@13820
    40
done
mehta@13820
    41
mehta@13820
    42
lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
wenzelm@42154
    43
apply (clarsimp simp only:Image_iff)
mehta@13820
    44
apply (erule rtrancl_induct)
mehta@13820
    45
 apply blast
mehta@13820
    46
apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
mehta@13820
    47
 apply (erule UnE)
mehta@13820
    48
 apply (auto intro:rtrancl_into_rtrancl)
mehta@13820
    49
apply blast
mehta@13820
    50
done
mehta@13820
    51
mehta@13820
    52
lemma still_reachable_eq: "\<lbrakk> A\<subseteq>Rb\<^sup>*``B; B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Ra-Rb. y \<in>(Rb\<^sup>*``B); \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Ra\<^sup>*``A =  Rb\<^sup>*``B "
mehta@13820
    53
apply (rule equalityI)
mehta@13820
    54
 apply (erule still_reachable ,assumption)+
mehta@13820
    55
done
mehta@13820
    56
mehta@13820
    57
lemma reachable_null: "reachable mS {Null} = {}"
mehta@13820
    58
apply (simp add: reachable_def addrs_def)
mehta@13820
    59
done
mehta@13820
    60
mehta@13820
    61
lemma reachable_empty: "reachable mS {} = {}"
mehta@13820
    62
apply (simp add: reachable_def addrs_def)
mehta@13820
    63
done
mehta@13820
    64
mehta@13820
    65
lemma reachable_union: "(reachable mS aS \<union> reachable mS bS) = reachable mS (aS \<union> bS)"
mehta@13820
    66
apply (simp add: reachable_def rel_defs addrs_def)
mehta@13820
    67
apply blast
mehta@13820
    68
done
mehta@13820
    69
mehta@13820
    70
lemma reachable_union_sym: "reachable r (insert a aS) = (r\<^sup>* `` addrs {a}) \<union> reachable r aS"
mehta@13820
    71
apply (simp add: reachable_def rel_defs addrs_def)
mehta@13820
    72
apply blast
mehta@13820
    73
done
mehta@13820
    74
mehta@13820
    75
lemma rel_upd1: "(a,b) \<notin> rel (r(q:=t)) \<Longrightarrow> (a,b) \<in> rel r \<Longrightarrow> a=q"
mehta@13820
    76
apply (rule classical)
mehta@13820
    77
apply (simp add:rel_defs fun_upd_apply)
mehta@13820
    78
done
mehta@13820
    79
mehta@13820
    80
lemma rel_upd2: "(a,b)  \<notin> rel r \<Longrightarrow> (a,b) \<in> rel (r(q:=t)) \<Longrightarrow> a=q"
mehta@13820
    81
apply (rule classical)
mehta@13820
    82
apply (simp add:rel_defs fun_upd_apply)
mehta@13820
    83
done
mehta@13820
    84
wenzelm@36866
    85
definition
wenzelm@62042
    86
  \<comment> "Restriction of a relation"
mehta@13820
    87
  restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set"       ("(_/ | _)" [50, 51] 50)
wenzelm@36866
    88
  where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}"
mehta@13820
    89
wenzelm@62042
    90
text \<open>Rewrite rules for the restriction of a relation\<close>
mehta@13820
    91
mehta@13820
    92
lemma restr_identity[simp]:
mehta@13820
    93
 " (\<forall>x. \<not> m x) \<Longrightarrow> (R |m) = R"
mehta@13820
    94
by (auto simp add:restr_def)
mehta@13820
    95
mehta@13820
    96
lemma restr_rtrancl[simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (R | m)\<^sup>* `` {l} = {l}"
mehta@13820
    97
by (auto simp add:restr_def elim:converse_rtranclE)
mehta@13820
    98
mehta@13820
    99
lemma [simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (l,x) \<in> (R | m)\<^sup>* = (l=x)"
mehta@13820
   100
by (auto simp add:restr_def elim:converse_rtranclE)
mehta@13820
   101
mehta@13820
   102
lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
mehta@13820
   103
apply (auto simp:restr_def rel_def fun_upd_apply)
mehta@13820
   104
apply (rename_tac a b)
mehta@13820
   105
apply (case_tac "a=q")
mehta@13820
   106
 apply auto
mehta@13820
   107
done
wenzelm@32960
   108
mehta@13820
   109
lemma restr_un: "((r \<union> s)|m) = (r|m) \<union> (s|m)"
mehta@13820
   110
  by (auto simp add:restr_def)
mehta@13820
   111
mehta@13820
   112
lemma rel_upd3: "(a, b) \<notin> (r|(m(q := t))) \<Longrightarrow> (a,b) \<in> (r|m) \<Longrightarrow> a = q "
mehta@13820
   113
apply (rule classical)
mehta@13820
   114
apply (simp add:restr_def fun_upd_apply)
wenzelm@32960
   115
done
mehta@13820
   116
wenzelm@36866
   117
definition
wenzelm@62042
   118
  \<comment> "A short form for the stack mapping function for List"
mehta@13820
   119
  S :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
wenzelm@36866
   120
  where "S c l r = (\<lambda>x. if c x then r x else l x)"
mehta@13820
   121
wenzelm@62042
   122
text \<open>Rewrite rules for Lists using S as their mapping\<close>
mehta@13820
   123
mehta@13820
   124
lemma [rule_format,simp]:
mehta@13820
   125
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
mehta@13820
   126
apply(induct_tac stack)
mehta@13820
   127
 apply(simp add:fun_upd_apply S_def)+
mehta@13820
   128
done
mehta@13820
   129
mehta@13820
   130
lemma [rule_format,simp]:
mehta@13820
   131
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
mehta@13820
   132
apply(induct_tac stack)
mehta@13820
   133
 apply(simp add:fun_upd_apply S_def)+
mehta@13820
   134
done
mehta@13820
   135
mehta@13820
   136
lemma [rule_format,simp]:
mehta@13820
   137
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
mehta@13820
   138
apply(induct_tac stack)
mehta@13820
   139
 apply(simp add:fun_upd_apply S_def)+
mehta@13820
   140
done
mehta@13820
   141
mehta@13820
   142
lemma [rule_format,simp]:
mehta@13820
   143
 "\<forall>p. a \<notin> set stack \<longrightarrow> List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
mehta@13820
   144
apply(induct_tac stack)
mehta@13820
   145
 apply(simp add:fun_upd_apply S_def)+
mehta@13820
   146
done
mehta@13820
   147
wenzelm@38353
   148
primrec
wenzelm@62042
   149
  \<comment>"Recursive definition of what is means for a the graph/stack structure to be reconstructible"
mehta@13820
   150
  stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow>  bool"
wenzelm@38353
   151
where
wenzelm@38353
   152
  stkOk_nil:  "stkOk c l r iL iR t [] = True"
wenzelm@38353
   153
| stkOk_cons:
wenzelm@38353
   154
    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
wenzelm@38353
   155
      iL p = (if c p then l p else t) \<and>
wenzelm@38353
   156
      iR p = (if c p then t else r p))"
mehta@13820
   157
wenzelm@62042
   158
text \<open>Rewrite rules for stkOk\<close>
mehta@13820
   159
mehta@13820
   160
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
mehta@13820
   161
  stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
mehta@13820
   162
apply (induct xs)
mehta@13820
   163
 apply (auto simp:eq_sym_conv)
mehta@13820
   164
done
mehta@13820
   165
mehta@13820
   166
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
mehta@13820
   167
 stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
mehta@13820
   168
apply (induct xs)
mehta@13820
   169
 apply (auto simp:eq_sym_conv)
mehta@13820
   170
done
mehta@13820
   171
mehta@13820
   172
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
mehta@13820
   173
 stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
mehta@13820
   174
apply (induct xs)
mehta@13820
   175
 apply (auto simp:eq_sym_conv)
mehta@13820
   176
done
mehta@13820
   177
mehta@13820
   178
lemma stkOk_r_rewrite [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
mehta@13820
   179
  stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
mehta@13820
   180
apply (induct xs)
mehta@13820
   181
 apply (auto simp:eq_sym_conv)
mehta@13820
   182
done
mehta@13820
   183
mehta@13820
   184
lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
mehta@13820
   185
 stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
mehta@13820
   186
apply (induct xs)
mehta@13820
   187
 apply (auto simp:eq_sym_conv)
mehta@13820
   188
done
mehta@13820
   189
mehta@13820
   190
lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
mehta@13820
   191
 stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
mehta@13820
   192
apply (induct xs)
mehta@13820
   193
 apply (auto simp:eq_sym_conv)
mehta@13820
   194
done
mehta@13820
   195
mehta@13820
   196
wenzelm@62042
   197
section\<open>The Schorr-Waite algorithm\<close>
mehta@13820
   198
mehta@13820
   199
mehta@13820
   200
theorem SchorrWaiteAlgorithm: 
mehta@13820
   201
"VARS c m l r t p q root
mehta@13820
   202
 {R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l} 
mehta@13820
   203
 t := root; p := Null;
mehta@13820
   204
 WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
mehta@13820
   205
 INV {\<exists>stack.
nipkow@13875
   206
          List (S c l r) p stack \<and>                                         (*i1*)
nipkow@13875
   207
          (\<forall>x \<in> set stack. m x) \<and>                                        (*i2*)
nipkow@13875
   208
          R = reachable (relS{l, r}) {t,p} \<and>                           (*i3*)
nipkow@13875
   209
          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                        (*i4*)
mehta@13820
   210
                 x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
nipkow@13875
   211
          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         (*i5*)
nipkow@13875
   212
          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>       (*i6*)
nipkow@13875
   213
          (stkOk c l r iL iR t stack)                                    (*i7*) }
mehta@13820
   214
 DO IF t = Null \<or> t^.m
mehta@13820
   215
      THEN IF p^.c
nipkow@13875
   216
               THEN q := t; t := p; p := p^.r; t^.r := q               (*pop*)
nipkow@13875
   217
               ELSE q := t; t := p^.r; p^.r := p^.l;                      (*swing*)
mehta@13820
   218
                        p^.l := q; p^.c := True          FI    
nipkow@13875
   219
      ELSE q := p; p := t; t := t^.l; p^.l := q;                         (*push*)
mehta@13820
   220
               p^.m := True; p^.c := False            FI       OD
mehta@13820
   221
 {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
nipkow@13875
   222
  (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
mehta@13820
   223
proof (vcg)
mehta@13820
   224
  let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
mehta@13820
   225
    {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3
mehta@13820
   226
  {
mehta@13820
   227
mehta@13820
   228
    fix c m l r t p q root
mehta@13820
   229
    assume "?Pre c m l r root"
mehta@13820
   230
    thus "?inv c m l r root Null"  by (auto simp add: reachable_def addrs_def)
mehta@13820
   231
  next
mehta@13820
   232
mehta@13820
   233
    fix c m l r t p q
mehta@13820
   234
    let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
mehta@13820
   235
    assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"  
mehta@13820
   236
    then obtain stack where inv: "?Inv stack" by blast
mehta@13820
   237
    from a have pNull: "p = Null" and tDisj: "t=Null \<or> (t\<noteq>Null \<and> t^.m )" by auto
mehta@13820
   238
    let "?I1 \<and> _ \<and> _ \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> _"  =  "?Inv stack"
mehta@13820
   239
    from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
mehta@13820
   240
    from pNull i1 have stackEmpty: "stack = []" by simp
mehta@13820
   241
    from tDisj i4 have RisMarked[rule_format]: "\<forall>x.  x \<in> R \<longrightarrow> m x"  by(auto simp: reachable_def addrs_def stackEmpty)
nipkow@39302
   242
    from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL"  by(auto simp: stackEmpty fun_eq_iff intro:RisMarked)
mehta@13820
   243
mehta@13820
   244
  next   
mehta@13820
   245
      fix c m l r t p q root
mehta@13820
   246
      let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
mehta@13820
   247
      let "\<exists>stack. ?popInv stack"  =  "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
mehta@13820
   248
      let "\<exists>stack. ?swInv stack"  =
mehta@13820
   249
        "?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
mehta@13820
   250
      let "\<exists>stack. ?puInv stack"  =
mehta@13820
   251
        "?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
mehta@13820
   252
      let "?ifB1"  =  "(t = Null \<or> t^.m)"
mehta@13820
   253
      let "?ifB2"  =  "p^.c" 
mehta@13820
   254
mehta@13820
   255
      assume "(\<exists>stack.?Inv stack) \<and> (p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)" (is "_ \<and> ?whileB")
mehta@13820
   256
      then obtain stack where inv: "?Inv stack" and whileB: "?whileB" by blast
mehta@13820
   257
      let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
mehta@13820
   258
      from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
mehta@13820
   259
                  and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+        
mehta@13820
   260
      have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
mehta@13820
   261
mehta@13820
   262
      show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and> 
mehta@13820
   263
                            (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
wenzelm@32960
   264
              (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
mehta@13820
   265
      proof - 
wenzelm@32960
   266
        {
wenzelm@32960
   267
          assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
wenzelm@32960
   268
          from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
wenzelm@32960
   269
          then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
wenzelm@32960
   270
          with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
wenzelm@32960
   271
            by auto
wenzelm@32960
   272
          with i2 have m_addr_p: "p^.m" by auto
wenzelm@32960
   273
          have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
wenzelm@32960
   274
          from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
wenzelm@32960
   275
          let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
wenzelm@32960
   276
          have "?popInv stack_tl"
wenzelm@32960
   277
          proof -
mehta@13820
   278
wenzelm@62042
   279
            \<comment> \<open>List property is maintained:\<close>
wenzelm@32960
   280
            from i1 p_notin_stack_tl ifB2
wenzelm@32960
   281
            have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl" 
wenzelm@32960
   282
              by(simp add: addr_p_eq stack_eq, simp add: S_def)
mehta@13820
   283
wenzelm@32960
   284
            moreover
wenzelm@62042
   285
            \<comment> \<open>Everything on the stack is marked:\<close>
wenzelm@32960
   286
            from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
wenzelm@32960
   287
            moreover
mehta@13820
   288
wenzelm@62042
   289
            \<comment> \<open>Everything is still reachable:\<close>
wenzelm@32960
   290
            let "(R = reachable ?Ra ?A)" = "?I3"
wenzelm@32960
   291
            let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
wenzelm@32960
   292
            let "?B" = "{p, p^.r}"
wenzelm@62042
   293
            \<comment> \<open>Our goal is \<open>R = reachable ?Rb ?B\<close>.\<close>
wenzelm@32960
   294
            have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
wenzelm@32960
   295
            proof
wenzelm@32960
   296
              show "?L \<subseteq> ?R"
wenzelm@32960
   297
              proof (rule still_reachable)
nipkow@44890
   298
                show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq 
wenzelm@32960
   299
                     intro:oneStep_reachable Image_iff[THEN iffD2])
wenzelm@32960
   300
                show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) 
nipkow@44890
   301
                     (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
wenzelm@32960
   302
              qed
wenzelm@32960
   303
              show "?R \<subseteq> ?L"
wenzelm@32960
   304
              proof (rule still_reachable)
wenzelm@32960
   305
                show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
nipkow@44890
   306
                  by(fastforce simp:addrs_def rel_defs addr_p_eq 
wenzelm@32960
   307
                      intro:oneStep_reachable Image_iff[THEN iffD2])
wenzelm@32960
   308
              next
wenzelm@32960
   309
                show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
wenzelm@32960
   310
                  by (clarsimp simp:relS_def) 
nipkow@44890
   311
                     (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
wenzelm@32960
   312
              qed
wenzelm@32960
   313
            qed
wenzelm@32960
   314
            with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def) 
wenzelm@32960
   315
            moreover
mehta@13820
   316
wenzelm@62042
   317
            \<comment> "If it is reachable and not marked, it is still reachable using..."
wenzelm@32960
   318
            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A"  =  ?I4        
wenzelm@32960
   319
            let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
wenzelm@32960
   320
            let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
wenzelm@62042
   321
            \<comment> \<open>Our goal is \<open>\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B\<close>.\<close>
wenzelm@32960
   322
            let ?T = "{t, p^.r}"
mehta@13820
   323
wenzelm@32960
   324
            have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
wenzelm@32960
   325
            proof (rule still_reachable)
wenzelm@32960
   326
              have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
wenzelm@32960
   327
                by (auto simp add:p_notin_stack_tl intro:fun_upd_other) 
wenzelm@32960
   328
              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
nipkow@44890
   329
                by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
wenzelm@32960
   330
              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
wenzelm@32960
   331
                by (clarsimp simp:restr_def relS_def) 
nipkow@44890
   332
                  (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
wenzelm@32960
   333
            qed
wenzelm@62042
   334
            \<comment> "We now bring a term from the right to the left of the subset relation."
wenzelm@32960
   335
            hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
wenzelm@32960
   336
              by blast
wenzelm@32960
   337
            have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
wenzelm@32960
   338
            proof (rule allI, rule impI)
wenzelm@32960
   339
              fix x
wenzelm@32960
   340
              assume a: "x \<in> R \<and> \<not> m x"
wenzelm@62042
   341
              \<comment> \<open>First, a disjunction on @{term"p^.r"} used later in the proof\<close>
wenzelm@32960
   342
              have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 
wenzelm@32960
   343
                by auto
wenzelm@62042
   344
              \<comment> \<open>@{term x} belongs to the left hand side of @{thm[source] subset}:\<close>
wenzelm@32960
   345
              have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
wenzelm@32960
   346
              have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
wenzelm@62042
   347
              \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close>
wenzelm@62042
   348
              \<comment> \<open>which corresponds to our goal.\<close>
wenzelm@32960
   349
              from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
wenzelm@32960
   350
            qed
wenzelm@32960
   351
            moreover
mehta@13820
   352
wenzelm@62042
   353
            \<comment> "If it is marked, then it is reachable"
wenzelm@32960
   354
            from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
wenzelm@32960
   355
            moreover
mehta@13820
   356
wenzelm@62042
   357
            \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close>
wenzelm@32960
   358
            from i7 i6 ifB2 
wenzelm@32960
   359
            have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" 
wenzelm@32960
   360
              by(auto simp: addr_p_eq stack_eq fun_upd_apply)
mehta@13820
   361
wenzelm@32960
   362
            moreover
mehta@13820
   363
wenzelm@62042
   364
            \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close>
wenzelm@32960
   365
            from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
wenzelm@32960
   366
              by (clarsimp simp:stack_eq addr_p_eq)
mehta@13820
   367
wenzelm@32960
   368
            ultimately show "?popInv stack_tl" by simp
wenzelm@32960
   369
          qed
wenzelm@32960
   370
          hence "\<exists>stack. ?popInv stack" ..
wenzelm@32960
   371
        }
wenzelm@32960
   372
        moreover
mehta@13820
   373
wenzelm@62042
   374
        \<comment> "Proofs of the Swing and Push arm follow."
wenzelm@62042
   375
        \<comment> "Since they are in principle simmilar to the Pop arm proof,"
wenzelm@62042
   376
        \<comment> "we show fewer comments and use frequent pattern matching."
wenzelm@32960
   377
        {
wenzelm@62042
   378
          \<comment> "Swing arm"
wenzelm@32960
   379
          assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
wenzelm@32960
   380
          from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
wenzelm@32960
   381
          then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
wenzelm@32960
   382
          with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
wenzelm@32960
   383
          with i2 have m_addr_p: "p^.m" by clarsimp
wenzelm@32960
   384
          from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
wenzelm@32960
   385
            by simp
wenzelm@32960
   386
          let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
wenzelm@32960
   387
          have "?swInv stack"
wenzelm@32960
   388
          proof -
wenzelm@32960
   389
            
wenzelm@62042
   390
            \<comment> \<open>List property is maintained:\<close>
wenzelm@32960
   391
            from i1 p_notin_stack_tl nifB2
wenzelm@32960
   392
            have swI1: "?swI1"
wenzelm@32960
   393
              by (simp add:addr_p_eq stack_eq, simp add:S_def)
wenzelm@32960
   394
            moreover
wenzelm@32960
   395
            
wenzelm@62042
   396
            \<comment> \<open>Everything on the stack is marked:\<close>
wenzelm@32960
   397
            from i2
wenzelm@32960
   398
            have swI2: "?swI2" .
wenzelm@32960
   399
            moreover
wenzelm@32960
   400
            
wenzelm@62042
   401
            \<comment> \<open>Everything is still reachable:\<close>
wenzelm@32960
   402
            let "R = reachable ?Ra ?A" = "?I3"
wenzelm@32960
   403
            let "R = reachable ?Rb ?B" = "?swI3"
wenzelm@32960
   404
            have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
wenzelm@32960
   405
            proof (rule still_reachable_eq)
wenzelm@32960
   406
              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
nipkow@44890
   407
                by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
wenzelm@32960
   408
            next
wenzelm@32960
   409
              show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
nipkow@44890
   410
                by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
wenzelm@32960
   411
            next
wenzelm@32960
   412
              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
nipkow@44890
   413
                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
wenzelm@32960
   414
            next
wenzelm@32960
   415
              show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
nipkow@44890
   416
                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
wenzelm@32960
   417
            qed
wenzelm@32960
   418
            with i3
wenzelm@32960
   419
            have swI3: "?swI3" by (simp add:reachable_def) 
wenzelm@32960
   420
            moreover
mehta@13820
   421
wenzelm@62042
   422
            \<comment> "If it is reachable and not marked, it is still reachable using..."
wenzelm@32960
   423
            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
wenzelm@32960
   424
            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
wenzelm@32960
   425
            let ?T = "{t}"
wenzelm@32960
   426
            have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
wenzelm@32960
   427
            proof (rule still_reachable)
wenzelm@32960
   428
              have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
wenzelm@32960
   429
                by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
wenzelm@32960
   430
              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
nipkow@44890
   431
                by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
wenzelm@32960
   432
            next
wenzelm@32960
   433
              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
nipkow@44890
   434
                by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
wenzelm@32960
   435
            qed
wenzelm@32960
   436
            then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
wenzelm@32960
   437
              by blast
wenzelm@32960
   438
            have ?swI4
wenzelm@32960
   439
            proof (rule allI, rule impI)
wenzelm@32960
   440
              fix x
wenzelm@32960
   441
              assume a: "x \<in> R \<and>\<not> m x"
wenzelm@32960
   442
              with i4 addr_p_eq stack_eq  have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" 
wenzelm@32960
   443
                by (simp only:reachable_def, clarsimp)
wenzelm@32960
   444
              with ifB1 a 
wenzelm@32960
   445
              have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" 
wenzelm@32960
   446
                by (auto simp add:addrs_def)
wenzelm@32960
   447
              from inc exc subset  show "x \<in> reachable ?Rb ?B" 
wenzelm@32960
   448
                by (auto simp add:reachable_def)
wenzelm@32960
   449
            qed
wenzelm@32960
   450
            moreover
wenzelm@32960
   451
            
wenzelm@62042
   452
            \<comment> "If it is marked, then it is reachable"
wenzelm@32960
   453
            from i5
wenzelm@32960
   454
            have "?swI5" .
wenzelm@32960
   455
            moreover
mehta@13820
   456
wenzelm@62042
   457
            \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close>
wenzelm@32960
   458
            from i6 stack_eq
wenzelm@32960
   459
            have "?swI6"
wenzelm@32960
   460
              by clarsimp           
wenzelm@32960
   461
            moreover
mehta@13820
   462
wenzelm@62042
   463
            \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close>
wenzelm@32960
   464
            from stackDist i7 nifB2 
wenzelm@32960
   465
            have "?swI7"
wenzelm@32960
   466
              by (clarsimp simp:addr_p_eq stack_eq)
mehta@13820
   467
wenzelm@32960
   468
            ultimately show ?thesis by auto
wenzelm@32960
   469
          qed
wenzelm@32960
   470
          then have "\<exists>stack. ?swInv stack" by blast
wenzelm@32960
   471
        }
wenzelm@32960
   472
        moreover
mehta@13820
   473
wenzelm@32960
   474
        {
wenzelm@62042
   475
          \<comment> "Push arm"
wenzelm@32960
   476
          assume nifB1: "\<not>?ifB1"
wenzelm@32960
   477
          from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
wenzelm@32960
   478
          then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
wenzelm@32960
   479
          with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
wenzelm@32960
   480
          from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
wenzelm@32960
   481
          with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
wenzelm@32960
   482
          let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
wenzelm@32960
   483
          have "?puInv new_stack"
wenzelm@32960
   484
          proof -
wenzelm@32960
   485
            
wenzelm@62042
   486
            \<comment> \<open>List property is maintained:\<close>
wenzelm@32960
   487
            from i1 t_notin_stack
wenzelm@32960
   488
            have puI1: "?puI1"
wenzelm@32960
   489
              by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
wenzelm@32960
   490
            moreover
wenzelm@32960
   491
            
wenzelm@62042
   492
            \<comment> \<open>Everything on the stack is marked:\<close>
wenzelm@32960
   493
            from i2
wenzelm@32960
   494
            have puI2: "?puI2" 
wenzelm@32960
   495
              by (simp add:new_stack_eq fun_upd_apply)
wenzelm@32960
   496
            moreover
wenzelm@32960
   497
            
wenzelm@62042
   498
            \<comment> \<open>Everything is still reachable:\<close>
wenzelm@32960
   499
            let "R = reachable ?Ra ?A" = "?I3"
wenzelm@32960
   500
            let "R = reachable ?Rb ?B" = "?puI3"
wenzelm@32960
   501
            have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
wenzelm@32960
   502
            proof (rule still_reachable_eq)
wenzelm@32960
   503
              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
nipkow@44890
   504
                by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
wenzelm@32960
   505
            next
wenzelm@32960
   506
              show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
nipkow@44890
   507
                by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
wenzelm@32960
   508
            next
wenzelm@32960
   509
              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
nipkow@44890
   510
                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
wenzelm@32960
   511
            next
wenzelm@32960
   512
              show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
nipkow@44890
   513
                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
wenzelm@32960
   514
            qed
wenzelm@32960
   515
            with i3
wenzelm@32960
   516
            have puI3: "?puI3" by (simp add:reachable_def) 
wenzelm@32960
   517
            moreover
wenzelm@32960
   518
            
wenzelm@62042
   519
            \<comment> "If it is reachable and not marked, it is still reachable using..."
wenzelm@32960
   520
            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
wenzelm@32960
   521
            let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
wenzelm@32960
   522
            let ?T = "{t}"
wenzelm@32960
   523
            have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
wenzelm@32960
   524
            proof (rule still_reachable)
wenzelm@32960
   525
              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
nipkow@44890
   526
                by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
wenzelm@32960
   527
            next
wenzelm@32960
   528
              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
wenzelm@32960
   529
                by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) 
nipkow@44890
   530
                   (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
wenzelm@32960
   531
            qed
wenzelm@32960
   532
            then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
wenzelm@32960
   533
              by blast
wenzelm@32960
   534
            have ?puI4
wenzelm@32960
   535
            proof (rule allI, rule impI)
wenzelm@32960
   536
              fix x
wenzelm@32960
   537
              assume a: "x \<in> R \<and> \<not> ?new_m x"
wenzelm@32960
   538
              have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
wenzelm@32960
   539
              with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
nipkow@44890
   540
                by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
wenzelm@32960
   541
              have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
wenzelm@32960
   542
                using xDisj a n_m_addr_t
wenzelm@32960
   543
                by (clarsimp simp add:addrs_def addr_t_eq) 
wenzelm@32960
   544
              from inc exc subset  show "x \<in> reachable ?Rb ?B" 
wenzelm@32960
   545
                by (auto simp add:reachable_def)
wenzelm@32960
   546
            qed  
wenzelm@32960
   547
            moreover
wenzelm@32960
   548
            
wenzelm@62042
   549
            \<comment> "If it is marked, then it is reachable"
wenzelm@32960
   550
            from i5
wenzelm@32960
   551
            have "?puI5"
wenzelm@32960
   552
              by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
wenzelm@32960
   553
            moreover
wenzelm@32960
   554
            
wenzelm@62042
   555
            \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close>
wenzelm@32960
   556
            from i6 
wenzelm@32960
   557
            have "?puI6"
wenzelm@32960
   558
              by (simp add:new_stack_eq)
wenzelm@32960
   559
            moreover
mehta@13820
   560
wenzelm@62042
   561
            \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close>
wenzelm@32960
   562
            from stackDist i6 t_notin_stack i7
wenzelm@32960
   563
            have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
mehta@13820
   564
wenzelm@32960
   565
            ultimately show ?thesis by auto
wenzelm@32960
   566
          qed
wenzelm@32960
   567
          then have "\<exists>stack. ?puInv stack" by blast
mehta@13820
   568
wenzelm@32960
   569
        }
wenzelm@32960
   570
        ultimately show ?thesis by blast
mehta@13820
   571
      qed
mehta@13820
   572
    }
mehta@13820
   573
  qed
mehta@13820
   574
mehta@13820
   575
end
mehta@13820
   576