Theory SchorrWaite_Ex

(* SPDX-License-Identifier: BSD-3-Clause *)
(*
 * Copyright (C) 2003 Farhad Mehta (TUM)
 * Copyright (C) 2013--2014 Japheth Lim (NICTA)
 * Copyright (C) 2013--2014 David Greenaway (NICTA)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 * * Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright
 * notice, this list of conditions and the following disclaimer in the
 * documentation and/or other materials provided with the distribution.
 *
 * * Neither the name of the University of Cambridge or the Technische
 * Universitaet Muenchen nor the names of their contributors may be used
 * to endorse or promote products derived from this software without
 * specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
 * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
 * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)

(*
 * This file contains a proof of a C implementation of the Schorr-Waite
 * graph marking algorithm.
 *
 * The original proof was carried out by Farhad Mehta, and is
 * distributed as part of Isabelle 2013-2.
 *
 * The proof minimally modified to hook up to the output of AutoCorres
 * by Japheth Lim and David Greenaway. Japheth Lim additionally modified
 * the proof to show fault-avoidence and termination.
 *)
theory SchorrWaite_Ex imports
  "HOL-Library.Product_Lexorder"
  "AutoCorres2_Main.AutoCorres_Main"
begin

declare fun_upd_apply[simp del]

install_C_file "schorr_waite.c"


autocorres [heap_abs_syntax] "schorr_waite.c"

abbreviation Cbool where "Cbool b ≡ if b then 1 else 0"

declare fun_upd_apply [simp]

(*** Base List definitions ***)

section "The heap"

subsection "Paths in the heap"

primrec Path :: "('p ptr ⇒ 'p ptr) ⇒ 'p ptr ⇒ 'p ptr list ⇒ 'p ptr ⇒ bool" where
  "Path s x [] y = (x = y)"
| "Path s x (a#as) y = (x ≠ NULL ∧ x = a ∧ Path s (s x) as y)"

lemma Path_NULL[iff]: "Path h NULL xs y = (xs = [] ∧ y = NULL)"
  by (cases xs; fastforce)

lemma Path_neq_NULL[simp]:
  "a ≠ NULL ⟹ Path h a as z = (as = [] ∧ z = a ∨ (∃bs. as = a#bs ∧ Path h (h a) bs z))"
  by (cases as; fastforce)

lemma Path_append[simp]: "⋀x. Path f x (as@bs) z = (∃y. Path f x as y ∧ Path f y bs z)"
  by (induct as; simp)

lemma Path_upd[simp]:
  "⋀x. u ∉ set as ⟹ Path (f(u := v)) x as y = Path f x as y"
  by (induct as; simp add: eq_sym_conv)

lemma Path_snoc:
  "a ≠ NULL ⟹ Path (f(a := q)) p as a ⟹ Path (f(a := q)) p (as @ [a]) q"
  by simp


subsection "Lists on the heap"

subsubsection "Relational abstraction"

definition List :: "('a ptr ⇒ 'a ptr) ⇒ 'a ptr ⇒ 'a ptr list ⇒ bool" where
  "List h x as = Path h x as NULL"

lemma List_Nil[simp]: "List h x [] = (x = NULL)"
  by (simp add: List_def)

lemma List_Cons[simp]: "List h x (a#as) = (x ≠ NULL ∧ x = a ∧ List h (h x) as)"
  by (simp add: List_def)

lemma List_NULL[simp]: "List h NULL as = (as = [])"
  by (case_tac as; simp)

lemma List_Ref[simp]: "a ≠ NULL ⟹ List h a as = (∃bs. as = a#bs ∧ List h (h a) bs)"
  by (case_tac as) auto

theorem notin_List_update[simp]:
  "⋀x. a ∉ set as ⟹ List (h(a := y)) x as = List h x as"
  by (induct as; clarsimp)

lemma List_unique: "⋀x bs. List h x as ⟹ List h x bs ⟹ as = bs"
  by (induct as; clarsimp)

lemma List_unique1: "List h p as ⟹ ∃!as. List h p as"
  by (blast intro: List_unique)

lemma List_app: "⋀x. List h x (as@bs) = (∃y. Path h x as y ∧ List h y bs)"
  by (induct as; clarsimp)

lemma List_hd_not_in_tl[simp]: "List h (h a) as ⟹ a ∉ set as"
  apply (clarsimp simp: in_set_conv_decomp)
  apply (frule List_app[THEN iffD1])
  apply (fastforce dest: List_unique)
  done

lemma List_distinct[simp]: "⋀x. List h x as ⟹ distinct as"
  by (induct as; fastforce dest:List_hd_not_in_tl)

lemma Path_is_List:
  "⟦ Path h b Ps a; a ∉ set Ps; a ≠ NULL ⟧ ⟹ List (h(a := NULL)) b (Ps @ [a])"
  by (induct Ps arbitrary: b) auto

lemma List_eq_select [elim]: "⟦ List s p xs; ∀x ∈ set xs. s x = t x ⟧ ⟹ List t p xs"
  by (induct xs arbitrary: p) auto

(*** Main Proof ***)

section ‹Machinery for the Schorr-Waite proof›

definition ― ‹Relations induced by a mapping›
  rel :: "('a ptr ⇒ 'a ptr) ⇒ ('a ptr × 'a ptr) set" where
  "rel m = {(x,y). m x = y ∧ y ≠ NULL}"

definition
  relS :: "('a ptr ⇒ 'a ptr) set ⇒ ('a ptr × 'a ptr) set" where
  "relS M = (⋃ m ∈ M. rel m)"

definition
  addrs :: "'a ptr set ⇒ 'a ptr set" where
  "addrs P = {a ∈ P. a ≠ NULL}"

definition
  reachable :: "('a ptr × 'a ptr) set ⇒ 'a ptr set ⇒ 'a ptr set" where
  "reachable r P = (r* `` addrs P)"

lemmas rel_defs = relS_def rel_def

text ‹Rewrite rules for relations induced by a mapping›

lemma self_reachable: "b ∈ B ⟹ b ∈ R* `` B"
  by blast

lemma oneStep_reachable: "b ∈ R``B ⟹ b ∈ R* `` B"
  by blast

lemma still_reachable:
  "⟦B⊆Ra*``A; ∀ (x,y) ∈ Rb-Ra. y∈ (Ra*``A)⟧ ⟹ Rb* `` B ⊆ Ra* `` A "
  apply (clarsimp simp only: Image_iff)
  apply (erule rtrancl_induct, blast)
  apply (fastforce intro: rtrancl_into_rtrancl)
  done

lemma still_reachable_eq:
  "⟦ A⊆Rb*``B; B⊆Ra*``A; ∀ (x,y) ∈ Ra-Rb. y ∈(Rb*``B); ∀ (x,y) ∈ Rb-Ra. y∈ (Ra*``A)⟧ ⟹
   Ra*``A =  Rb*``B "
  by (rule equalityI; erule (1) still_reachable)

lemma reachable_null: "reachable mS {NULL} = {}"
  by (simp add: reachable_def addrs_def)

lemma reachable_empty: "reachable mS {} = {}"
  by (simp add: reachable_def addrs_def)

lemma reachable_union: "(reachable mS aS ∪ reachable mS bS) = reachable mS (aS ∪ bS)"
  by (simp add: reachable_def rel_defs addrs_def) blast

lemma reachable_null': "reachable mS {x, NULL} = reachable mS {x}"
  using reachable_null reachable_union
  by (metis insert_is_Un reachable_empty)


lemma reachable_union_sym: "reachable r (insert a aS) = (r* `` addrs {a}) ∪ reachable r aS"
  by (simp add: reachable_def rel_defs addrs_def) blast

lemma rel_upd1: "(a,b) ∉ rel (r(q:=t)) ⟹ (a,b) ∈ rel r ⟹ a=q"
  by (rule classical) (simp add: rel_defs)

lemma rel_upd2: "(a,b)  ∉ rel r ⟹ (a,b) ∈ rel (r(q:=t)) ⟹ a=q"
  by (rule classical) (simp add:rel_defs)

definition ― ‹Restriction of a relation›
  restr :: "('a ptr × 'a ptr) set ⇒ ('a ptr ⇒ bool) ⇒ ('a ptr × 'a ptr) set"
           ("(_/ | _)" [50, 51] 50)
  where
  "restr r m = {(x,y). (x,y) ∈ r ∧ ¬ m x}"

no_notation disj (infixr "|" 30) ― ‹Avoid syntax conflict with restr›

text ‹Rewrite rules for the restriction of a relation›

lemma restr_identity[simp]:
  "(∀x. ¬ m x) ⟹ (R|m) = R"
  by (auto simp add:restr_def)

lemma restr_rtrancl[simp]: " ⟦m l⟧ ⟹ (R | m)* `` {l} = {l}"
  by (auto simp add:restr_def elim:converse_rtranclE)

lemma [simp]: " ⟦m l⟧ ⟹ (l,x) ∈ (R | m)* = (l=x)"
  by (auto simp add:restr_def elim:converse_rtranclE)

lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
  by (auto simp:restr_def rel_def)

lemma restr_un: "((r ∪ s)|m) = (r|m) ∪ (s|m)"
  by (auto simp add:restr_def)

lemma rel_upd3: "(a, b) ∉ (r|(m(q := t))) ⟹ (a,b) ∈ (r|m) ⟹ a = q "
  by (rule classical) (simp add:restr_def)

definition
  ― ‹A short form for the stack mapping function for List›
  S :: "('a ptr ⇒ bool) ⇒ ('a ptr ⇒ 'a ptr) ⇒ ('a ptr ⇒ 'a ptr) ⇒ ('a ptr ⇒ 'a ptr)"
  where "S c l r = (λx. if c x then r x else l x)"

text ‹Rewrite rules for Lists using S as their mapping›

lemma [rule_format,simp]:
  "∀p. a ∉ set stack ⟶ List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
  by (induct_tac stack; simp add: S_def)

lemma [rule_format,simp]:
  "∀p. a ∉ set stack ⟶ List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
  by (induct_tac stack; simp add: S_def)

lemma [rule_format,simp]:
  "∀p. a ∉ set stack ⟶ List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
  by (induct_tac stack; simp add: S_def)

lemma [rule_format,simp]:
  "∀p. a ∉ set stack ⟶ List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
  by (induct_tac stack; simp add: S_def)


primrec
  ― ‹Recursive definition of what is means for a the graph/stack structure to be reconstructible›
  stkOk :: "('a ptr ⇒ bool) ⇒ ('a ptr ⇒ 'a ptr) ⇒ ('a ptr ⇒ 'a ptr) ⇒ ('a ptr ⇒ 'a ptr) ⇒ ('a ptr ⇒ 'a ptr) ⇒ 'a ptr ⇒'a ptr list ⇒  bool"
  where
    stkOk_nil:  "stkOk c l r iL iR t [] = True"
  | stkOk_cons:
    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR p stk ∧
      iL p = (if c p then l p else t) ∧
      iR p = (if c p then t else r p) ∧
      p ≠ NULL)"

text ‹Rewrite rules for stkOk›

lemma stkOk_cx[simp]:
  "⋀t. ⟦ x ∉ set xs; x ≠ t ⟧ ⟹ stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
  by (induct xs) (auto simp:eq_sym_conv)

lemma stkOk_lx[simp]:
  "⋀t. ⟦ x ∉ set xs; x≠t ⟧ ⟹ stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
  by (induct xs) (auto simp:eq_sym_conv)

lemma stkOk_r[simp]:
  "⋀t. ⟦ x ∉ set xs; x≠t ⟧ ⟹ stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
  by (induct xs) (auto simp:eq_sym_conv)

lemma stkOk_r_rewrite [simp]:
  "⋀x. x ∉ set xs ⟹ stkOk c l (r(x := g)) iL iR x xs = stkOk c l r iL iR x xs"
  by (induct xs) (auto simp:eq_sym_conv)

lemma stkOk_l[simp]:
  "⋀x. x ∉ set xs ⟹ stkOk c (l(x := g)) r iL iR x xs = stkOk c l r iL iR x xs"
  by (induct xs) (auto simp:eq_sym_conv)

lemma stkOk_c[simp]:
  "⋀x. x ∉ set xs ⟹ stkOk (c(x := g)) l r iL iR x xs = stkOk c l r iL iR x xs"
  by (induct xs) (auto simp:eq_sym_conv)

lemma stkOk_eq_select[elim]:
  "⟦ stkOk s a b c d p xs; ∀x ∈ set xs. s x = t x ⟧ ⟹ stkOk t a b c d p xs"
  by (induct xs arbitrary: p) auto

definition measure :: "('a ⇒ ('n :: wellorder)) ⇒ ('a × 'a) set"
  where
    "measure r ≡ {(s', s). r s' < r s}"

lemma in_measure[simp, code_unfold]: "((x,y) : measure f) = (f x < f y)"
  by (simp add:measure_def)

lemma wf_measure [iff]: "wf (measure f)"
  by (metis SchorrWaite_Ex.in_measure measure_induct_rule wf_def)


abbreviation schorr_waite'_inv where
  "schorr_waite'_inv s s0 R p t cond stack ≡
       ― ‹i1› List (S (λx. s[x]→c ≠ 0) (λx. s[x]→l) (λx. s[x]→r)) p stack ∧
       ― ‹i2› (∀x ∈ set stack. s[x]→m ≠ 0) ∧
       ― ‹i3› R = reachable (relS {λx. s[x]→l, λx. s[x]→r}) {t, p} ∧
       ― ‹i4› (∀x. x ∈ R ∧ s[x]→m = 0 ⟶
                     x ∈ reachable (restr (relS {λx. s[x]→l, λx. s[x]→r}) (λx. s[x]→m ≠ 0))
                                   ({t} ∪ set (map (λx. s[x]→r) stack))) ∧
       ― ‹i5› (∀x. s[x]→m ≠ 0 ⟶ x ∈ R) ∧
       ― ‹i6› (∀x. x ∉ set stack ⟶ s[x]→r = s0[x]→r ∧ s[x]→l = s0[x]→l) ∧
       ― ‹i7› (stkOk (λx. s[x]→c ≠ 0) (λx. s[x]→l) (λx. s[x]→r) (λx. s0[x]→l) (λx. s0[x]→r) t stack) ∧
       ― ‹i8› (∀x. x ∈ R ⟶ ptr_valid (heap_typing s) x) ∧
       ― ‹i9› cond = Cbool (p = NULL ⟶ (t ≠ NULL ∧ s[t]→m = 0))"

abbreviation schorr_waite'_measure where
  "schorr_waite'_measure s s0 R p t cond ≡
       let stack = (THE stack. schorr_waite'_inv s s0 R p t cond stack)
       in (card {x ∈ R. s[x]→m = 0}, card {x ∈ set stack. s[x]→c = 0}, length stack)"

(* Helper for the termination proof. *)
lemma the_equality': "⋀P a. ⟦P a; ⋀x. ⟦ P a; P x ⟧ ⟹ x = a⟧ ⟹ (THE x. P x) = a"
  by blast

(* Variant using the same order as in former nondet-monad setting *)
lemma runs_to_whileLoop_res':
  assumes B[runs_to_vcg]: "⋀a s. I a s ⟹ C a s ⟹
    B a  ∙ s ⦃λr t. (∀b. r = Result b ⟶ I b t ∧ ((b, t), (a, s)) ∈ R)⦄"
  assumes R: "wf R"
  assumes *: "I a s"
  assumes P_Result: "⋀a s. I a s ⟹ ¬ C a s ⟹ P (Result a) s"
  shows "(whileLoop C B a::('a, 's) res_monad) ∙ s ⦃P⦄"
  apply (rule runs_to_whileLoop [OF R, where I = "λException _ ⇒ (λ_. False) | Result v ⇒ I v"])
  subgoal using * by auto
  subgoal using P_Result by auto
  subgoal by auto
  subgoal by runs_to_vcg
  done

lemmas runs_to_whileLoop3 =  runs_to_whileLoop_res' [split_tuple C and B arity: 3]


(*** Main Proof ***)

declare fun_upd_apply[simp del] fun_upd_other[simp]

section‹The Schorr-Waite algorithm›

text ‹
The following Isar proof might look weird at first sight. It follows the structure of the
former ‹wp› method, which was replaced by @{method runs_to_vcg}. One decisive difference between
both verification condition generators is: 
▪ ‹wp› introduces (nested) ‹if ... then ... else ...› for const‹condition›
▪ @{method runs_to_vcg} introduces separate subgoals instead.

So the structured Isar part of the proof resembles the subgoals introduced by ‹wp›. We just prove
them as before replacing @{command show} with @{command have} and afterwards use these results
to solve the new subgoals that are introduced by @{method runs_to_vcg}.
›


theorem (in ts_definition_schorr_waite) SchorrWaiteAlgorithm:
  assumes Pre: "R = reachable (relS {λx. s0[x]→l, λx. s0[x]→r}) {root_ptr} ∧ (∀x. s0[x]→m = 0) ∧ (∀x∈R. ptr_valid (heap_typing s0) x)"
    (is "?Pre root_ptr s0")
  shows "
  schorr_waite' root_ptr ∙ s0
 ⦃λr s. ∀x. (x ∈ R) = (s[x]→m ≠ 0) ∧ s[x]→l = s0[x]→l ∧ s[x]→r = s0[x]→r⦄"
proof -
  {
  let "_ ∙ s0 ⦃ ?Post ⦄" = ?thesis
  fix p :: "node_C ptr" and t :: "node_C ptr" and
    s :: "lifted_globals" and cond :: "int"
  let "?cond p t s" = "p = NULL ⟶ t ≠ NULL ∧ s[t]→m = 0"
  let "?inv p t cond s" = "∃stack. schorr_waite'_inv s s0 R p t cond stack"
  let "?measure p t cond s" = "schorr_waite'_measure s s0 R p t cond"

  let "∃stack. ?Inv p t cond s stack" = "?inv p t cond s"

  {

    assume "?Pre root_ptr s0"
    then have "∀x. ?inv NULL root_ptr (Cbool (root_ptr ≠ NULL ∧ s0[root_ptr]→m = 0)) s0 ∧
              (root_ptr ≠ NULL ⟶ ptr_valid (heap_typing s0) root_ptr)"
      by (auto simp: reachable_def addrs_def )
  } note goal1 = this
(*
  {

    fix x s p t cond
    assume a: "?inv p t cond s" and b: "¬ cond ≠ 0"
    then obtain stack where inv: "?Inv p t cond s stack" by blast
    from a b have pNull: "p = NULL" and tDisj: "t=NULL ∨ (t≠NULL ∧ s[t]→m ≠ 0)" by auto
    let "?I1 ∧ _ ∧ _ ∧ ?I4 ∧ ?I5 ∧ ?I6 ∧ _ ∧ _ ∧ _"  =  "?Inv p t cond s stack"
    from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
    from pNull i1 have stackEmpty: "stack = []" by simp
    from tDisj i4 have RisMarked[rule_format]: "∀x. x ∈ R ⟶ s[x]→m ≠ 0" using inv by(auto simp: reachable_def addrs_def stackEmpty)
    from i5 i6 have "(x ∈ R) = (s[x]→m ≠ 0) ∧ s[x]→l = s0[x]→l ∧ s[x]→r = s0[x]→r" by(auto simp: stackEmpty fun_eq_iff RisMarked)
  } note goal2 = this
*)

    {
      fix s p t cond stack_tl
      assume stackInv: "?Inv p t cond s (p # stack_tl)"
        and whileB: "cond ≠ 0" (is "?whileB")
        and ifB1: "t = NULL ∨ s[t]→m ≠ 0" (is "?ifB1") and ifB2: "s[p]→c ≠ 0" (is "?ifB2")
      let "?I1 ∧ ?I2 ∧ ?I3 ∧ ?I4 ∧ ?I5 ∧ ?I6 ∧ ?I7 ∧ ?I8 ∧ ?I9" = "?Inv p t cond s (p # stack_tl)"
      from stackInv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
        and i5: "?I5" and i6: "?I6" and i7: "?I7" and i8: "?I8"
        and cond: "?I9" by simp+
      have stackDist: "distinct (p # stack_tl)" using i1 by (rule List_distinct)
      from whileB and ifB1 and cond have pNotNULL [iff]: "p ≠ NULL" by simp
      with i2 have m_p: "s[p]→m ≠ 0" by auto
      from stackDist have p_notin_stack_tl: "p ∉ set stack_tl" by simp
      let "?pop_s" = "s[p→r := t]"
      have "?Inv (s[p]→r) p (Cbool (?cond (s[p]→r) p ?pop_s)) ?pop_s stack_tl"
        (is "?poI1∧ ?poI2∧ ?poI3∧ ?poI4∧ ?poI5∧ ?poI6∧ ?poI7∧ ?poI8∧ ?poI9")
      proof -
        ― ‹List property is maintained:›
        from i1 p_notin_stack_tl ifB2
        have poI1: "List (S (λx. ?pop_s[x]→c ≠ 0) (λx. ?pop_s[x]→l) (λx. ?pop_s[x]→r)) (s[p]→r) stack_tl"
          by(simp, simp add: S_def)

        moreover
          ― ‹Everything on the stack is marked:›
        from i2 have poI2: "∀ x ∈ set stack_tl. s[x]→m ≠ 0" by simp
        moreover

― ‹Everything is still reachable:›
        let "(R = reachable ?Ra ?A)" = "?I3"
        let "?Rb" = "relS {λx. ?pop_s[x]→l, λx. ?pop_s[x]→r}"
        let "?B" = "{p, s[p]→r}"
          ― ‹Our goal is @{text"R = reachable ?Rb ?B"}.›
        have "?Ra* `` addrs ?A = ?Rb* `` addrs ?B" (is "?L = ?R")
        proof
          show "?L ⊆ ?R"
          proof (rule still_reachable)
            show "addrs ?A ⊆ ?Rb* `` addrs ?B"
              by(fastforce simp:addrs_def relS_def rel_def
                         intro:oneStep_reachable Image_iff[THEN iffD2])
            show "∀(x,y) ∈ ?Ra-?Rb. y ∈ (?Rb* `` addrs ?B)"
              by (clarsimp simp:relS_def)
                 (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
          qed
          show "?R ⊆ ?L"
          proof (rule still_reachable)
            show "addrs ?B ⊆ ?Ra* `` addrs ?A"
              by (fastforce simp: addrs_def rel_defs
                          intro: oneStep_reachable Image_iff[THEN iffD2])
          next
            show "∀(x, y)∈?Rb-?Ra. y∈(?Ra*``addrs ?A)"
              by (clarsimp simp:relS_def)
                   (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
          qed
        qed
        with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def)
        moreover

― ‹If it is reachable and not marked, it is still reachable using...›
        let "∀x. x ∈ R ∧ s[x]→m = 0 ⟶ x ∈ reachable ?Ra ?A"  =  ?I4
        let "?Rb" = "restr (relS {λx. ?pop_s[x]→l, λx. ?pop_s[x]→r}) (λx. ?pop_s[x]→m ≠ 0)"
        let "?B" = "{p} ∪ set (map (λx. ?pop_s[x]→r) stack_tl)"
          ― ‹Our goal is @{text"∀x. x ∈ R ∧ ¬ m x ⟶ x ∈ reachable ?Rb ?B"}.›
        let ?T = "{t, s[p]→r}"

        have "?Ra* `` addrs ?A ⊆ ?Rb* `` (addrs ?B ∪ addrs ?T)"
        proof (rule still_reachable)
          have rewrite: "∀x∈set stack_tl. ?pop_s[x]→r = s[x]→r"
            by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
          show "addrs ?A ⊆ ?Rb* `` (addrs ?B ∪ addrs ?T)"
            by (fastforce cong:map_cong simp:addrs_def rewrite fun_upd_apply intro:self_reachable)
          show "∀(x, y)∈?Ra-?Rb. y∈(?Rb*``(addrs ?B ∪ addrs ?T))"
            by (clarsimp simp:restr_def relS_def)
                (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
        qed
            ― ‹We now bring a term from the right to the left of the subset relation.›
        hence subset: "?Ra* `` addrs ?A - ?Rb* `` addrs ?T ⊆ ?Rb* `` addrs ?B"
          by blast
        have poI4: "∀x. x ∈ R ∧ ?pop_s[x]→m = 0 ⟶ x ∈ reachable ?Rb ?B"
        proof (rule allI, rule impI)
          fix x
          assume a: "x ∈ R ∧ ?pop_s[x]→m = 0"
            ― ‹First, a disjunction on @{term "s[p]→r"} used later in the proof›
          have pDisj:"s[p]→r = NULL ∨ (s[p]→r ≠ NULL ∧ s[(s[p]→r)]→m ≠ 0)" using poI1 poI2
            by (case_tac stack_tl, auto simp: List_def)
              ― ‹@{term x} belongs to the left hand side of @{thm[source] subset}:›
          have incl: "x ∈ ?Ra*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
          have excl: "x ∉ ?Rb*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
          ― ‹And therefore also belongs to the right hand side of @{thm[source]subset},›
          ― ‹which corresponds to our goal.›
          from incl excl subset  show "x ∈ reachable ?Rb ?B" by (auto simp add:reachable_def)
        qed
        moreover

― ‹If it is marked, then it is reachable›
        from i5 have poI5: "∀x. ?pop_s[x]→m ≠ 0 ⟶ x ∈ R" by simp
        moreover

― ‹If it is not on the stack, then its @{term l} and @{term r} fields are unchanged›
        from i7 i6 ifB2
        have poI6: "∀x. x ∉ set stack_tl ⟶ ?pop_s[x]→r = s0[x]→r ∧ ?pop_s[x]→l = s0[x]→l"
          by(auto simp: fun_upd_apply)

        moreover

― ‹If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed›
        from p_notin_stack_tl i7 have poI7: "stkOk (λx. ?pop_s[x]→c ≠ 0) (λx. ?pop_s[x]→l) (λx. ?pop_s[x]→r) (λx. s0[x]→l) (λx. s0[x]→r) p stack_tl"
          by clarsimp
        moreover

        from i8 have poI8: "∀x. x ∈ R ⟶ ptr_valid (heap_typing ?pop_s) x"
          by simp

        ultimately show "?thesis" by simp
      qed
    }
    note popStack = this

― ‹Proofs of the Swing and Push arm follow.›
― ‹Since they are in principle simmilar to the Pop arm proof,›
― ‹we show fewer comments and use frequent pattern matching.›
    {
      ― ‹Swing arm›
      fix s p t cond stack
      assume stackInv: "?Inv p t cond s stack"
        and whileB: "cond ≠ 0" (is "?whileB")
        and ifB1: "t = NULL ∨ s[t]→m ≠ 0" (is "?ifB1") and nifB2: "¬ s[p]→c ≠ 0" (is "¬ ?ifB2")
      let "?I1 ∧ ?I2 ∧ ?I3 ∧ ?I4 ∧ ?I5 ∧ ?I6 ∧ ?I7 ∧ ?I8 ∧ ?I9" = "?Inv p t cond s stack"
      from stackInv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
        and i5: "?I5" and i6: "?I6" and i7: "?I7" and i8: "?I8"
        and cond: "?I9" by simp+
      have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
      from whileB and ifB1 and cond have pNotNULL [iff]: "p ≠ NULL" by simp
      with i1 obtain stack_tl where stack_eq: "stack = p # stack_tl"
        by (case_tac stack) (auto simp: List_def)
      with i2 have m_p: "s[p]→m ≠ 0" by auto
      from stack_eq stackDist have p_notin_stack_tl: "p ∉ set stack_tl" by simp

      let "?sw_s"  = "((s[p→r := s[p]→l])[p→l := t])[p→c := 1]"
      have "?Inv p (s[p]→r) (Cbool (?cond p (s[p]→r) ?sw_s)) ?sw_s stack"
        (is "?swI1∧?swI2∧?swI3∧?swI4∧?swI5∧?swI6∧?swI7∧?swI8∧?swI9")
      proof -

― ‹List property is maintained:›
        from i1 p_notin_stack_tl nifB2
        have swI1: "?swI1"
          by (simp add: stack_eq, auto simp: S_def fun_upd_apply)
        moreover

― ‹Everything on the stack is marked:›
        from i2
        have swI2: "?swI2" by simp
        moreover

― ‹Everything is still reachable:›
        let "R = reachable ?Ra ?A" = "?I3"
        let "R = reachable ?Rb ?B" = "?swI3"
        have "?Ra* `` addrs ?A = ?Rb* `` addrs ?B"
        proof (rule still_reachable_eq)
          show "addrs ?A ⊆ ?Rb* `` addrs ?B"
            by(fastforce simp:addrs_def rel_defs intro:oneStep_reachable Image_iff[THEN iffD2])
        next
          show "addrs ?B ⊆ ?Ra* `` addrs ?A"
            by(fastforce simp:addrs_def rel_defs intro:oneStep_reachable Image_iff[THEN iffD2])
        next
          show "∀(x, y)∈?Ra-?Rb. y∈(?Rb*``addrs ?B)"
            by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
        next
          show "∀(x, y)∈?Rb-?Ra. y∈(?Ra*``addrs ?A)"
            by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
        qed
        with i3
        have swI3: "?swI3" by (simp add:reachable_def)
        moreover

― ‹If it is reachable and not marked, it is still reachable using...›
        let "∀x. x ∈ R ∧ s[x]→m = 0 ⟶ x ∈ reachable ?Ra ?A" = ?I4
        let "∀x. x ∈ R ∧ _[x]→m = 0 ⟶ x ∈ reachable ?Rb ?B" = ?swI4
        let ?T = "{t}"
        have "?Ra*``addrs ?A ⊆ ?Rb*``(addrs ?B ∪ addrs ?T)"
        proof (rule still_reachable)
          have rewrite: "(∀x∈set stack_tl. ?sw_s[x]→r = s[x]→r)"
            by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
          show "addrs ?A ⊆ ?Rb* `` (addrs ?B ∪ addrs ?T)"
            by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite fun_upd_apply intro:self_reachable)
        next
          show "∀(x, y)∈?Ra-?Rb. y∈(?Rb*``(addrs ?B ∪ addrs ?T))"
            by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
        qed
        then have subset: "?Ra*``addrs ?A - ?Rb*``addrs ?T ⊆ ?Rb*``addrs ?B"
          by blast
        have ?swI4
        proof (rule allI, rule impI)
          fix x
          assume a: "x ∈ R ∧ ?sw_s[x]→m = 0"
          with i4 stack_eq  have inc: "x ∈ ?Ra*``addrs ?A"
            by (simp only:reachable_def, clarsimp)
          with ifB1 a
          have exc: "x ∉ ?Rb*`` addrs ?T"
            by (auto simp add:addrs_def)
          from inc exc subset  show "x ∈ reachable ?Rb ?B"
            by (auto simp add:reachable_def)
        qed
        moreover

― ‹If it is marked, then it is reachable›
        from i5
        have "?swI5" by simp
        moreover

― ‹If it is not on the stack, then its @{term l} and @{term r} fields are unchanged›
        from i6 stack_eq
        have "?swI6"
          by clarsimp
        moreover

― ‹If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed›
        from stackDist i7 nifB2
        have "?swI7"
          by (simp add: stack_eq) (auto simp: fun_upd_apply)
        moreover

        from i8
        have "?swI8"
          by simp
        ultimately show ?thesis by simp
      qed
    }
    note swStack = this

    {
      ― ‹Push arm›
      fix s p t cond stack
      assume stackInv: "?Inv p t cond s stack"
        and whileB: "cond ≠ 0" (is "?whileB")
        and nifB1: "¬ (t = NULL ∨ s[t]→m ≠ 0)" (is "¬ ?ifB1")
      let "?I1 ∧ ?I2 ∧ ?I3 ∧ ?I4 ∧ ?I5 ∧ ?I6 ∧ ?I7 ∧ ?I8 ∧ ?I9" = "?Inv p t cond s stack"
      from stackInv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
        and i5: "?I5" and i6: "?I6" and i7: "?I7" and i8: "?I8"
        and cond: "?I9" by simp+
      have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
      from whileB and nifB1 and cond have tNotNULL [iff]: "t ≠ NULL" by simp
      with i1 obtain new_stack where new_stack_eq: "new_stack = t # stack" by clarsimp
      from tNotNULL nifB1 cond have n_m_t: "s[t]→m = 0" by clarsimp
      with i2 have t_notin_stack: "t ∉ set stack" by blast

      let "?pu_s"  = "((s[t→l := p])[t→m := 1])[t→c := 0]"
      have "?Inv t (s[t]→l) (Cbool (?cond t (s[t]→l) ?pu_s)) ?pu_s new_stack"
        (is "?puI1∧?puI2∧?puI3∧?puI4∧?puI5∧?puI6∧?puI7∧?puI8∧?puI9")
      proof -
        ― ‹List property is maintained:›
        from i1 t_notin_stack new_stack_eq
        have puI1: "?puI1"
          by (simp add: new_stack_eq) (auto simp:S_def fun_upd_apply)
        moreover

― ‹Everything on the stack is marked:›
        from i2
        have puI2: "?puI2"
          by (simp add:new_stack_eq fun_upd_apply)
        moreover

― ‹Everything is still reachable:›
        let "R = reachable ?Ra ?A" = "?I3"
        let "R = reachable ?Rb ?B" = "?puI3"
        have "?Ra* `` addrs ?A = ?Rb* `` addrs ?B"
        proof (rule still_reachable_eq)
          show "addrs ?A ⊆ ?Rb* `` addrs ?B"
            by(fastforce simp:addrs_def rel_defs intro:oneStep_reachable Image_iff[THEN iffD2])
        next
          show "addrs ?B ⊆ ?Ra* `` addrs ?A"
            by(fastforce simp:addrs_def rel_defs intro:oneStep_reachable Image_iff[THEN iffD2])
        next
          show "∀(x, y)∈?Ra-?Rb. y∈(?Rb*``addrs ?B)"
            by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
        next
          show "∀(x, y)∈?Rb-?Ra. y∈(?Ra*``addrs ?A)"
            by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
        qed
        with i3
        have puI3: "?puI3" by (simp add:reachable_def addrs_def)
        moreover

― ‹If it is reachable and not marked, it is still reachable using...›
        let "∀x. x ∈ R ∧ s[x]→m = 0 ⟶ x ∈ reachable ?Ra ?A" = ?I4
        let "∀x. x ∈ R ∧ _[x]→m = 0 ⟶ x ∈ reachable ?Rb ?B" = ?puI4
        let ?T = "{t}"
        have "?Ra*``addrs ?A ⊆ ?Rb*``(addrs ?B ∪ addrs ?T)"
        proof (rule still_reachable)
          show "addrs ?A ⊆ ?Rb* `` (addrs ?B ∪ addrs ?T)"
            by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
        next
          show "∀(x, y)∈?Ra-?Rb. y∈(?Rb*``(addrs ?B ∪ addrs ?T))"
            by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd)
               (auto simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply dest:rel_upd3)
        qed
        then have subset: "?Ra*``addrs ?A - ?Rb*``addrs ?T ⊆ ?Rb*``addrs ?B"
          by blast
        have ?puI4
        proof (rule allI, rule impI)
          fix x
          assume a: "x ∈ R ∧ ?pu_s[x]→m = 0"
          have xDisj: "x = t ∨ x ≠ t" by simp
          with i4 a have inc: "x ∈ ?Ra*``addrs ?A"
            by (fastforce simp: addrs_def reachable_def intro:self_reachable)
          have exc: "x ∉ ?Rb*`` addrs ?T"
            using xDisj a n_m_t
            by (clarsimp simp add:addrs_def)
          from inc exc subset  show "x ∈ reachable ?Rb ?B"
            by (auto simp add:reachable_def)
        qed
        moreover

― ‹If it is marked, then it is reachable›
        from i5
        have "?puI5"
          by (auto simp:addrs_def i3 reachable_def fun_upd_apply intro:self_reachable)
        moreover

― ‹If it is not on the stack, then its @{term l} and @{term r} fields are unchanged›
        from i6
        have "?puI6"
          by (simp add:new_stack_eq)
        moreover

― ‹If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed›
        from stackDist i6 t_notin_stack i7
        have "?puI7" by (simp add: new_stack_eq) (auto simp: fun_upd_apply)
        moreover

        from i8
        have "?puI8"
          by simp

        ultimately show ?thesis by auto
      qed
        (* replace new_stack because it has been locally obtained *)
      hence "?Inv t (s[t]→l) (Cbool (?cond t (s[t]→l) ?pu_s)) ?pu_s (t # stack)"
        by (fastforce simp: new_stack_eq)
    }
    note puStack = this

    txt ‹Loop invariant and correctness›
    {
      fix s p t cond
      assume loopInv: "?inv p t cond s ∧ cond ≠ 0" (is "_ ∧ ?whileB")
      then have exStack: "?inv p t cond s" and whileB: "?whileB" by simp+
      from loopInv obtain stack where stackInv: "?Inv p t cond s stack" by blast

      from stackInv have stackDist: "distinct (stack)" by auto
      from stackInv have tValid: "t ≠ NULL ⟶ ptr_valid (heap_typing s) t"
        and pValid: "p ≠ NULL ⟶ ptr_valid (heap_typing s) p"
        by (auto simp: reachable_def addrs_def)

      let "?pop_s" = "s[p→r := t]"
      let "?sw_s"  = "((s[p→r := s[p]→l])[p→l := t])[p→c := 1]"
      let "?pu_s"  = "((s[t→l := p])[t→m := 1])[t→c := 0]"

      have "(if t = NULL ∨ s[t]→m ≠ 0
             then (if s[p]→c ≠ 0
                   then ?inv (s[p]→r) p (Cbool (?cond (s[p]→r) p ?pop_s)) ?pop_s ∧
                        (s[p]→r = NULL ⟶ p ≠ NULL ⟶ ptr_valid (heap_typing ?pop_s) p)
                   else ?inv p (s[p]→r) (Cbool (?cond p (s[p]→r) ?sw_s)) ?sw_s ∧
                        (p = NULL ⟶ s[p]→r ≠ NULL ⟶ ptr_valid (heap_typing ?sw_s) (s[p]→r))) ∧
                  ptr_valid (heap_typing s) p
             else (?inv t (s[t]→l) (Cbool (?cond t (s[t]→l) ?pu_s)) ?pu_s ∧
                   (t = NULL ⟶ s[t]→l ≠ NULL ⟶ ptr_valid (heap_typing ?pu_s) (s[t]→l))) ∧
                  ptr_valid (heap_typing s) t) ∧
            (t ≠ NULL ⟶ ptr_valid (heap_typing s) t)"
        (is "(if ?ifB1 then (if ?ifB2 then ?popInv else ?swInv) ∧ _ else ?puInv) ∧ _")
      proof -
        {
          have "t ≠ NULL ⟶ ptr_valid (heap_typing s) t"
            using stackInv whileB by (auto simp: reachable_def addrs_def)
        }
        note tValid = this

        moreover
        {
          assume ifB1: "?ifB1" and ifB2: "?ifB2"
          then obtain stack_tl where stack_eq: "stack = p # stack_tl"
            using stackInv whileB by (case_tac stack) (auto simp: List_def)
          have pNotNULL: "p ≠ NULL" using whileB ifB1 stackInv by simp
          have pValid: "ptr_valid (heap_typing ?pop_s) p"
            using pNotNULL stackInv by (auto simp: reachable_def addrs_def)

          have "?popInv"
            using popStack[OF stackInv[unfolded stack_eq] whileB ifB1 ifB2] pValid
            by blast
        }

        moreover
        {
          assume ifB1: "?ifB1" and nifB2: "¬ ?ifB2"
          have pNotNULL: "p ≠ NULL" using whileB ifB1 stackInv by simp
          have prValid: "s[p]→r ≠ NULL ⟶ ptr_valid (heap_typing ?sw_s) (s[p]→r)"
          proof -
            have "s[p]→r ≠ NULL ⟶ s[p]→r ∈ R"
              using stackInv by (auto simp: pNotNULL reachable_def rel_defs addrs_def)
            then show ?thesis using stackInv by auto
          qed

          have "?swInv"
            using swStack[OF stackInv whileB ifB1 nifB2] prValid by blast
        }

        moreover
        {
          assume nifB1: "¬ ?ifB1"
          have tNotNULL: "t ≠ NULL" using whileB nifB1 stackInv by simp
          have tlValid: "s[t]→l ≠ NULL ⟶ ptr_valid (heap_typing ?pu_s) (s[t]→l)"
          proof -
            have "s[t]→l ≠ NULL ⟶ s[t]→l ∈ R"
              using stackInv tNotNULL by (auto simp: reachable_def rel_defs addrs_def)
            then show ?thesis using stackInv by auto
          qed

          have "?puInv"
            using puStack[OF stackInv whileB nifB1] tValid tNotNULL tlValid by blast
        }

        moreover
        {
          assume "?ifB1"
          then have "ptr_valid (heap_typing s) p"
            using whileB stackInv by (auto simp: reachable_def addrs_def)
        }

        ultimately show "?thesis" by presburger
      qed
    } note loop_correct = this

    txt ‹Loop termination›
    {
      fix p t cond m1 m2 m3 s
      assume loopInv: "?inv p t cond s ∧ cond ≠ 0
                          ∧ schorr_waite'_measure s s0 R p t cond = (m1, m2, m3)"
        (is "_ ∧ _ ∧ ?prevMeasure")
      then have exStack: "∃stack. ?Inv p t cond s stack"
        and whileB: "cond ≠ 0" (is "?whileB")
        and measure: "?prevMeasure" by blast+

      from exStack obtain stack where stackInv: "?Inv p t cond s stack" by blast
      from stackInv have stackDist: "distinct stack" by auto
      have theStack: "⋀p t cond s stack. ?Inv p t cond s stack ⟹
                         (THE stack. ?Inv p t cond s stack) = stack"
        by (auto simp: the_equality List_unique)

      have measure': "(m1, m2, m3) = (card {x ∈ R. s[x]→m = 0}, card {x ∈ set stack. s[x]→c = 0}, length stack)"
        using theStack[OF stackInv] measure by auto

      let "?pop_s" = "s[p→r := t]"
      let "?sw_s"  = "((s[p→r := s[p]→l])[p→l := t])[p→c := 1]"
      let "?pu_s"  = "((s[t→l := p])[t→m := 1])[t→c := 0]"

      let "?decreasing p t s" = "schorr_waite'_measure s s0 R p t
                                     (Cbool (?cond p t s) :: int)
                              < (m1, m2, m3)"

      have weird_mp: "⋀a b. (a ∧ (a ⟶ b)) = (a ∧ b)" by blast

      have "(t ≠ NULL ⟶ ptr_valid (heap_typing s) t) ⟶
            (if t = NULL ∨ s[t]→m ≠ 0
             then ptr_valid (heap_typing s) p ⟶
                  (if s[p]→c ≠ 0
                   then (s[p]→r = NULL ⟶ p ≠ NULL ⟶ ptr_valid (heap_typing ?pop_s) p) ⟶
                          ?decreasing (s[p]→r) p ?pop_s
                   else (p = NULL ⟶ s[p]→r ≠ NULL ⟶ ptr_valid (heap_typing ?sw_s) (s[p]→r)) ⟶
                          ?decreasing p (s[p]→r) ?sw_s)
             else ptr_valid (heap_typing s) t ⟶
                   (t = NULL ⟶ s[t]→l ≠ NULL ⟶ ptr_valid (heap_typing ?pu_s) (s[t]→l)) ⟶
                    ?decreasing t (s[t]→l) ?pu_s)"
        (is "_ ⟶ (if ?ifB1
                      then _ ⟶ (if ?ifB2 then _ ⟶ ?popMeasure else ?swMeasure)
                      else _ ⟶ ?puMeasure)")
      proof -
        {
          assume ifB1: "?ifB1" and ifB2: "?ifB2"
          then have pNotNULL: "p ≠ NULL" using stackInv whileB by simp
          from stackInv pNotNULL obtain stack_tl where stack_eq: "stack = p # stack_tl"
            by (case_tac stack, auto simp: List_def)
          have stack_tlDist: "distinct stack_tl" using stackDist stack_eq by simp
          have conv: "⋀P xs. distinct xs ⟹ card {x ∈ set xs. P x} = length [x←xs. P x]"
            by (subst set_filter[symmetric])
               (metis distinct_card distinct_filter)

          have stackC_mono: "card {x ∈ set stack_tl. s[x]→c = 0} ≤ card {x ∈ set stack. s[x]→c = 0}"
            by (simp add: conv[OF stackDist] conv[OF stack_tlDist])
               (simp add: stack_eq)
          have "?popMeasure"
            using theStack[OF popStack[OF stackInv[unfolded stack_eq] whileB ifB1 ifB2]] stackC_mono
            by (simp add: pNotNULL stack_eq prod_less_def measure')
        }

        moreover
        {
          assume ifB1: "?ifB1" and nifB2: "¬ ?ifB2"
          then have pNotNULL: "p ≠ NULL" using stackInv whileB by simp
          from stackInv pNotNULL obtain stack_tl where stack_eq: "stack = p # stack_tl"
            by (case_tac stack, auto simp: List_def)
          from stack_eq stackDist have p_notin_stack_tl: "p ∉ set stack_tl" by simp

          have notin_filter: "⋀xs a P. a ∉ set xs ⟹ filter P xs = filter (λx. x ≠ a ∧ P x) xs"
          proof -
            fix xs a P
            show "a ∉ set xs ⟹ ?thesis xs a P" by (induct xs) auto
          qed
          have decrease: "card {x ∈ set stack. ?sw_s[x]→c = 0} < card {x ∈ set stack. s[x]→c = 0}"
          proof -
            have conv: "⋀P. card {x ∈ set stack. P x} = length [x←stack. P x]"
              by (subst set_filter[symmetric])
                 (metis stackDist distinct_card distinct_filter)

            show ?thesis
              unfolding conv
              by (simp add: stack_eq nifB2 weird_mp fun_upd_apply
                          notin_filter[OF p_notin_stack_tl, symmetric])
          qed

          hence "?swMeasure"
            using theStack[OF swStack[OF stackInv[unfolded stack_eq] whileB ifB1 nifB2]]
            by (simp add: stack_eq[symmetric] prod_less_def measure')
        }

        moreover
        {
          assume nifB1: "¬?ifB1"
          from nifB1 whileB stackInv have tNotNULL: "t ≠ NULL" by clarsimp
          from stackInv obtain new_stack where new_stack_eq: "new_stack = t # stack" by clarsimp
          from tNotNULL nifB1 stackInv have n_m_t: "s[t]→m = 0" by clarsimp
          with stackInv have t_notin_stack: "t ∉ set stack" by blast
          let "?puI1∧?puI2∧?puI3∧?puI4∧?puI5∧?puI6∧?puI7∧?puI8∧?puI9" =
              "?Inv t (s[t]→l) t_cond ?pu_s new_stack"

          have set_filter_remove: "⋀s a P. a ∈ s ⟹ {x. x ≠ a ∧ x ∈ s ∧ P x} = {x∈s. P x} - {a}"
            by blast

          have decrease: "card {x ∈ R. ?pu_s[x]→m = 0} < card {x ∈ R. s[x]→m = 0}"
          proof -
            have new_stackDist: "distinct new_stack"
              by (simp add: new_stack_eq t_notin_stack stackDist)
            have t_reachable: "t ∈ R" using stackInv tNotNULL
              by (auto simp: reachable_def addrs_def)

            have new_m: "{x ∈ R. ?pu_s[x]→m = 0} = {x ∈ R. s[x]→m = 0} - {t}"
              by (auto simp: set_filter_remove fun_upd_apply)

            show ?thesis
              by (subst new_m card.remove[of "{x∈R. s[x]→m = 0}" t])+
                 (auto simp: t_reachable n_m_t)
          qed

          have "?puMeasure"
            using theStack[OF puStack[OF stackInv whileB nifB1]] decrease
            by (simp add: measure' prod_less_def)
        } 
        ultimately show ?thesis by presburger
      qed
      
    } note loop_termination = this

    note goal1 loop_correct loop_termination
  }
  note goals = this
  show ?thesis
    unfolding schorr_waite'_def
    supply if_split [split del] (* FIXME: otherwise prepare state_only_simp of runs_to_vcg splits postcondition! *)
    supply runs_to_whileLoop3 
      [where I = "λ(p, cond, t) s. ∃stack. schorr_waite'_inv s s0 R p t cond stack"
              and R = "measure' (λ((p, cond, t), s). schorr_waite'_measure s s0 R p t cond)", runs_to_vcg]
    apply (runs_to_vcg (trace) (nosplit) (no_unsafe_hyp_subst))
                     (*   apply (simp_all (no_asm_use) only: split_tupled_all split_conv upd_fun_def) *)
    subgoal using goals(1)[OF Pre] 
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]  
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]  
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]  
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]  
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]  goals(3) [of s p t cond] 
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]  
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]  
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond] goals(3) [of s p t cond]
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond]
      by force
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond] 
      by auto
    subgoal for v t1 p cond t s stack using goals(2) [of s p t cond] goals(3) [of s p t cond]  
      by auto
    subgoal using Pre
      by (simp add: reachable_null' )
     subgoal using Pre  
       by auto
     subgoal using Pre  
       by auto
     subgoal using Pre  
       by auto
     subgoal for p cond t s stack x
       by (smt (verit, del_insts) CollectD ImageE ImageI addrs_def 
           reachable_def restr_rtrancl singletonD)
     done
 qed

end