Quelle  CIMP_vcg.thy

(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory CIMP_vcg
imports
  CIMP_lang
begin

(*>*)
section‹ State-based invariants \label{sec:cimp-invariants} ›

text‹

  provide a simple-minded verification condition generator (VCG) for this language, providing
  for establishing state-based invariants. It is just one way of reasoning about CIMP programs
  is proven sound wrt to the CIMP semantics.

  approach follows 🍋‹"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"›
 and the later 🍋‹"Lamport:2002"›) and closely
  work by 🍋‹"AptFrancezDeRoever:1980"›,
 🍋‹"CousotCousot:1980"› and 🍋‹"DBLP:journals/acta/LevinG81"›, who suggest the
  of a history variable. 🍋‹"CousotCousot:1980"› apparently contains a completeness proof.
  mentions that this technique was well-known in the mid-80s
  he proposed the use of prophecy variables\footnote{@{url
 https://lamport.azurewebsites.net/pubs/pubs.html"}}. See also 🍋‹"deRoeverEtAl:2001"› for an extended discussion of
  of this.

 ›

declare small_step.intros[intro]

inductive_cases small_step_inv:
  "({l} Request action val # cs, ls) → s'"
  "({l} Response action # cs, ls) → s'"
  "({l} LocalOp R # cs, ls) → s'"
  "({l} IF b THEN c FI # cs, ls) → s'"
  "({l} IF b THEN c1 ELSE c2 FI # cs, ls) → s'"
  "({l} WHILE b DO c OD # cs, ls) → s'"
  "(LOOP DO c OD # cs, ls) → s'"

lemma small_step_stuck:
  "¬ ([], s) →_<alpha> c'"
by (auto elim: small_step.cases)

declare system_step.intros[intro]

text‹

  default we ask the simplifier to rewrite @{const "atS"} using
  @{const "AT"} information.

 ›

lemma atS_state_weak_cong[cong]:
  "AT s p = AT s' p ==> atS p ls s ⟷ atS p ls s'"
by (auto simp: atS_def)

text‹

  provide an incomplete set of basic rules for label sets.

 ›

lemma atS_simps:
  "¬atS p {} s"
  "atS p {l} s ⟷ at p l s"
  "[at p l s; l ∈ ls] ==> atS p ls s"
  "(∀l. at p l s ⟶ l ∉ ls) ==> ¬atS p ls s"
by (auto simp: atS_def)

lemma atS_mono:
  "[atS p ls s; ls ⊆ ls'] ==> atS p ls' s"
by (auto simp: atS_def)

lemma atS_un:
  "atS p (l ∪ l') s ⟷ atS p l s ∨ atS p l' s"
by (auto simp: atS_def)

lemma atLs_disj_union[simp]:
  "(atLs p label0 \<or> atLs p label1) = atLs p (label0 ∪ label1)"
unfolding atLs_def by simp

lemma atLs_insert_disj:
  "atLs p (insert l label0) = (atL p l \<or> atLs p label0)"
by simp

lemma small_step_terminated:
  "s → s' ==> atCs (fst s) = {} ==> atCs (fst s') = {}"
by (induct pred: small_step) auto

lemma atC_not_empty:
  "atC c ≠ {}"
by (induct c) auto

lemma atCs_empty:
  "atCs cs = {} ⟷ cs = []"
by (induct cs) (auto simp: atC_not_empty)

lemma terminated_no_commands:
  assumes "terminated p sh"
  shows "∃s. GST sh p = ([], s)"
using assms unfolding atLs_def AT_def by (metis atCs_empty prod.collapse singletonD)

lemma terminated_GST_stable:
  assumes "system_step q sh' sh"
  assumes "terminated p sh"
  shows "GST sh p = GST sh' p"
using assms by (auto dest!: terminated_no_commands simp: small_step_stuck elim!: system_step.cases)

lemma terminated_stable:
  assumes "system_step q sh' sh"
  assumes "terminated p sh"
  shows "terminated p sh'"
using assms unfolding atLs_def AT_def
by (fastforce split: if_splits prod.splits
               dest: small_step_terminated
              elim!: system_step.cases)

lemma system_step_pls_nonempty:
  assumes "system_step pls sh' sh"
  shows "pls ≠ {}"
using assms by cases simp_all

lemma system_step_no_change:
  assumes "system_step ps sh' sh"
  assumes "p ∉ ps"
  shows "GST sh' p = GST sh p"
using assms by cases simp_all

lemma initial_stateD:
  assumes "initial_state sys s"
  shows "AT ((GST = s, HST = [])) = atC ∘ PGMs sys ∧ INIT sys ((GST = s, HST = []))↓ ∧ (∀p l. ¬taken p l (GST = s, HST = []))"
using assms unfolding initial_state_def split_def o_def LST_def AT_def taken_def by simp

lemma initial_states_initial[iff]:
  assumes "initial_state sys s"
  shows "at p l ((GST = s, HST = [])) ⟷ l ∈ atC (PGMs sys p)"
using assms unfolding initial_state_def split_def AT_def by simp

definition
  reachable_state :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
                    ==> ('answer, 'location, 'proc, 'question, 'state) state_pred"
where
  "reachable_state sys s ⟷ (∃σ i. prerun sys σ ∧ σ i = s)"

lemma reachable_stateE:
  assumes "reachable_state sys sh"
  assumes "∧σ i. prerun sys σ ==> P (σ i)"
  shows "P sh"
using assms unfolding reachable_state_def by blast

lemma prerun_reachable_state:
  assumes "prerun sys σ"
  shows "reachable_state sys (σ i)"
using assms unfolding prerun_def LTL.defs system_step_reflclp_def reachable_state_def by auto

lemma reachable_state_induct[consumes 1, case_names init LocalStep CommunicationStep, induct set: reachable_state]:
  assumes r: "reachable_state sys sh"
  assumes i: "∧s. initial_state sys s ==> P (GST = s, HST = [])"
  assumes l: "∧sh ls' p. [reachable_state sys sh; P sh; GST sh p →_<tau> ls'] ==> P (GST = (GST sh)(p := ls'), HST = HST sh)"
  assumes c: "∧sh ls1' ls2' p1 p2 α β.
                 [reachable_state sys sh; P sh;
                 GST sh p1 →_{<guillemotleft>α, β¬} ls1'; GST sh p2 →_{<guillemotright>α, β«} ls2'; p1 ≠ p2 ]
                    ==> P (GST = (GST sh)(p1 := ls1', p2 := ls2'), HST = HST sh @ [(α, β)])"
  shows "P sh"
using r
proof(rule reachable_stateE)
  fix σ i assume "prerun sys σ" show "P (σ i)"
  proof(induct i)
    case 0 from ‹prerun sys σ› show ?case
      unfolding prerun_def by (metis (full_types) i old.unit.exhaust system_state.surjective)
  next
    case (Suc i) with ‹prerun sys σ› show ?case
unfolding prerun_def LTL.defs system_step_reflclp_def reachable_state_def
apply clarsimp
apply (drule_tac x=i in spec)
apply (erule disjE; clarsimp)
apply (erule system_step.cases; clarsimp)
 apply (metis (full_types) ‹prerun sys σ› l old.unit.exhaust prerun_reachable_state system_state.surjective)
apply (metis (full_types) ‹prerun sys σ› c old.unit.exhaust prerun_reachable_state system_state.surjective)
done
  qed
qed

lemma prerun_valid_TrueI:
  shows "sys ⊨ ⟨True⟩"
unfolding prerun_valid_def by simp

lemma prerun_valid_conjI:
  assumes "sys ⊨ P"
  assumes "sys ⊨ Q"
  shows "sys ⊨ P \<and> Q"
using assms unfolding prerun_valid_def always_def by simp

lemma valid_prerun_lift:
  assumes "sys ⊨ I"
  shows "sys ⊨ ◻⌈I⌉"
using assms unfolding prerun_valid_def valid_def run_def by blast

lemma prerun_valid_induct:
  assumes "∧σ. prerun sys σ ==> ⌈I⌉ σ"
  assumes "∧σ. prerun sys σ ==> (⌈I⌉ \<hookrightarrow> (◯⌈I⌉)) σ"
  shows "sys ⊨ I"
unfolding prerun_valid_def using assms by (simp add: always_induct)

lemma prerun_validI:
  assumes "∧s. reachable_state sys s ==> I s"
  shows "sys ⊨ I"
unfolding prerun_valid_def using assms by (simp add: alwaysI prerun_reachable_state)

lemma prerun_validE:
  assumes "reachable_state sys s"
  assumes "sys ⊨ I"
  shows "I s"
using assms unfolding prerun_valid_def
by (metis alwaysE reachable_stateE suffix_state_prop)


subsubsection‹Relating reachable states to the initial programs \label{sec:cimp-decompose-small-step}›

text‹

  usefully reason about the control locations presumably embedded in
  single global invariant, we need to link the programs we have in
  state ‹s› to the programs in the initial states. The
 ‹fragments› function decomposes the program into statements
  can be directly executed (\S\ref{sec:cimp-decompose}). We also
  the locations we could be at after executing that statement as
  function of the process's local state.

  the bodies of ‹IF› and ‹WHILE› statements
  smaller (but equivalent) proof obligations.

 ›

type_synonym  ('answer, 'location, 'question, 'state) loc_comp
  = "'state ==> 'location set"

fun lconst :: "'location set ==> ('answer, 'location, 'question, 'state) loc_comp" where
  "lconst lp s = lp"

definition lcond :: "'location set ==> 'location set ==> 'state bexp
                   ==> ('answer, 'location, 'question, 'state) loc_comp" where
  "lcond lp lp' b s = (if b s then lp else lp')"

lemma lcond_split:
  "Q (lcond lp lp' b s) ⟷ (b s ⟶ Q lp) ∧ (¬b s ⟶ Q lp')"
unfolding lcond_def by (simp split: if_splits)

lemma lcond_split_asm:
  "Q (lcond lp lp' b s) ⟷ ¬ ((b s ∧ ¬Q lp) ∨ (¬b s ∧ ¬ Q lp'))"
unfolding lcond_def by (simp split: if_splits)

lemmas lcond_splits = lcond_split lcond_split_asm

fun
  fragments :: "('answer, 'location, 'question, 'state) com
              ==> 'location set
              ==> ( ('answer, 'location, 'question, 'state) com
               × ('answer, 'location, 'question, 'state) loc_comp ) set"
where
  "fragments ({l} IF b THEN c FI) aft
       = { ({l} IF b THEN c' FI, lcond (atC c) aft b) |c'. True }
        ∪ fragments c aft"
| "fragments ({l} IF b THEN c1 ELSE c2 FI) aft
       = { ({l} IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2) b) |c1' c2'. True }
        ∪ fragments c1 aft ∪ fragments c2 aft"
| "fragments (LOOP DO c OD) aft = fragments c (atC c)"
| "fragments ({l} WHILE b DO c OD) aft
       = fragments c {l} ∪ { ({l} WHILE b DO c' OD, lcond (atC c) aft b) |c'. True }"
| "fragments (c1;; c2) aft = fragments c1 (atC c2) ∪ fragments c2 aft"
| "fragments (c1 ⊕ c2) aft = fragments c1 aft ∪ fragments c2 aft"
| "fragments c aft = { (c, lconst aft) }"

fun
  fragmentsL :: "('answer, 'location, 'question, 'state) com list
               ==> ( ('answer, 'location, 'question, 'state) com
                 × ('answer, 'location, 'question, 'state) loc_comp ) set"
where
  "fragmentsL [] = {}"
| "fragmentsL [c] = fragments c {}"
| "fragmentsL (c # c' # cs) = fragments c (atC c') ∪ fragmentsL (c' # cs)"

abbreviation
  fragmentsLS :: "('answer, 'location, 'question, 'state) local_state
               ==> ( ('answer, 'location, 'question, 'state) com
                 × ('answer, 'location, 'question, 'state) loc_comp ) set"
where
  "fragmentsLS s ≡ fragmentsL (cPGM s)"

text‹

  show that taking system steps preserves fragments.

 ›

lemma small_step_fragmentsLS:
  assumes "s →_<alpha> s'"
  shows "fragmentsLS s' ⊆ fragmentsLS s"
using assms by induct (case_tac [!] cs, auto)

lemma reachable_state_fragmentsLS:
  assumes "reachable_state sys sh"
  shows "fragmentsLS (GST sh p) ⊆ fragments (PGMs sys p) {}"
using assms
by (induct rule: reachable_state_induct)
   (auto simp: initial_state_def dest: subsetD[OF small_step_fragmentsLS])

inductive
  basic_com :: "('answer, 'location, 'question, 'state) com ==> bool"
where
  "basic_com ({l} Request action val)"
| "basic_com ({l} Response action)"
| "basic_com ({l} LocalOp R)"
| "basic_com ({l} IF b THEN c FI)"
| "basic_com ({l} IF b THEN c1 ELSE c2 FI)"
| "basic_com ({l} WHILE b DO c OD)"

lemma fragments_basic_com:
  assumes "(c', aft') ∈ fragments c aft"
  shows "basic_com c'"
using assms by (induct c arbitrary: aft) (auto intro: basic_com.intros)

lemma fragmentsL_basic_com:
  assumes "(c', aft') ∈ fragmentsL cs"
  shows "basic_com c'"
using assms
apply (induct cs)
 apply simp
apply (case_tac cs)
 apply (auto simp: fragments_basic_com)
done

text‹

  reason about system transitions we need to identify which basic
  gets executed next. To that end we factor out the recursive
  of the @{term "small_step"} semantics into \emph{contexts},
  isolate the ‹basic_com› commands with immediate
 -visible behaviour. Note that non-determinism means that
  than one ‹basic_com› can be enabled at a time.

  representation of evaluation contexts follows 🍋‹"DBLP:journals/jar/Berghofer12"›. This style of
  semantics was originated by 🍋‹"FelleisenHieb:1992"›.

 ›

type_synonym ('answer, 'location, 'question, 'state) ctxt
  = "(('answer, 'location, 'question, 'state) com ==> ('answer, 'location, 'question, 'state) com)
   × (('answer, 'location, 'question, 'state) com ==> ('answer, 'location, 'question, 'state) com list)"

inductive_set
  ctxt :: "('answer, 'location, 'question, 'state) ctxt set"
where
  C_Hole: "(id, ⟨[]⟩) ∈ ctxt"
| C_Loop: "(E, fctxt) ∈ ctxt ==> (λc1. LOOP DO E c1 OD, λc1. fctxt c1 @ [LOOP DO E c1 OD]) ∈ ctxt"
| C_Seq: "(E, fctxt) ∈ ctxt ==> (λc1. E c1;; c2, λc1. fctxt c1 @ [c2]) ∈ ctxt"
| C_Choose1: "(E, fctxt) ∈ ctxt ==> (λc1. E c1 ⊕ c2, fctxt) ∈ ctxt"
| C_Choose2: "(E, fctxt) ∈ ctxt ==> (λc2. c1 ⊕ E c2, fctxt) ∈ ctxt"

text‹

  can decompose a small step into a context and a @{const "basic_com"}.

 ›

fun
  decompose_com :: "('answer, 'location, 'question, 'state) com
                      ==> ( ('answer, 'location, 'question, 'state) com
                        × ('answer, 'location, 'question, 'state) ctxt ) set"
where
  "decompose_com (LOOP DO c1 OD) = { (c, λt. LOOP DO ictxt t OD, λt. fctxt t @ [LOOP DO ictxt t OD]) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c1 }"
| "decompose_com (c1;; c2) = { (c, λt. ictxt t;; c2, λt. fctxt t @ [c2]) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c1 }"
| "decompose_com (c1 ⊕ c2) = { (c, λt. ictxt t ⊕ c2, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c1 }
                           ∪ { (c, λt. c1 ⊕ ictxt t, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c2 }"
| "decompose_com c = {(c, id, ⟨[]⟩)}"

definition
  decomposeLS :: "('answer, 'location, 'question, 'state) local_state
               ==> ( ('answer, 'location, 'question, 'state) com
                 × (('answer, 'location, 'question, 'state) com ==> ('answer, 'location, 'question, 'state) com)
                 × (('answer, 'location, 'question, 'state) com ==> ('answer, 'location, 'question, 'state) com list) ) set"
where
  "decomposeLS s = (case cPGM s of c # _ ==> decompose_com c | _ ==> {})"

lemma ctxt_inj:
  assumes "(E, fctxt) ∈ ctxt"
  assumes "E x = E y"
  shows "x = y"
using assms by (induct set: ctxt) auto

lemma decompose_com_non_empty: "decompose_com c ≠ {}"
by (induct c) auto

lemma decompose_com_basic_com:
  assumes "(c', ctxts) ∈ decompose_com c"
  shows "basic_com c'"
using assms by (induct c arbitrary: c' ctxts) (auto intro: basic_com.intros)

lemma decomposeLS_basic_com:
  assumes "(c', ctxts) ∈ decomposeLS s"
  shows "basic_com c'"
using assms unfolding decomposeLS_def by (simp add: decompose_com_basic_com split: list.splits)

lemma decompose_com_ctxt:
  assumes "(c', ctxts) ∈ decompose_com c"
  shows "ctxts ∈ ctxt"
using assms by (induct c arbitrary: c' ctxts) (auto intro: ctxt.intros)

lemma decompose_com_ictxt:
  assumes "(c', ictxt, fctxt) ∈ decompose_com c"
  shows "ictxt c' = c"
using assms by (induct c arbitrary: c' ictxt fctxt) auto

lemma decompose_com_small_step:
  assumes as: "(c' # fctxt c' @ cs, s) →_<alpha> s'"
  assumes ds: "(c', ictxt, fctxt) ∈ decompose_com c"
  shows "(c # cs, s) →_<alpha> s'"
using decompose_com_ctxt[OF ds] as decompose_com_ictxt[OF ds]
by (induct ictxt fctxt arbitrary: c cs)
   (cases s', fastforce simp: fun_eq_iff dest: ctxt_inj)+

theorem context_decompose:
  "s →_<alpha> s' ⟷ (∃(c, ictxt, fctxt) ∈ decomposeLS s.
                     cPGM s = ictxt c # tl (cPGM s)
                   ∧ (c # fctxt c @ tl (cPGM s), cTKN s, cLST s) →_<alpha> s'
                   ∧ (∀l∈atC c. cTKN s' = Some l))" (is "?lhs = ?rhs")
proof(rule iffI)
  assume ?lhs then show ?rhs
  unfolding decomposeLS_def
  proof(induct rule: small_step.induct)
    case (Choose1 c1 cs s α cs' s' c2) then show ?case
      apply clarsimp
      apply (rename_tac c ictxt fctxt)
      apply (rule_tac x="(c, λt. ictxt t ⊕ c2, fctxt)" in bexI)
      apply auto
      done
  next
    case (Choose2 c2 cs s α cs' s' c1) then show ?case
      apply clarsimp
      apply (rename_tac c ictxt fctxt)
      apply (rule_tac x="(c, λt. c1 ⊕ ictxt t, fctxt)" in bexI)
      apply auto
      done
  qed fastforce+
next
  assume ?rhs then show ?lhs
    unfolding decomposeLS_def
    by (cases s) (auto split: list.splits dest: decompose_com_small_step)
qed

text‹

  we only use this result left-to-right (to decompose a small step
  a basic one), this equivalence shows that we lose no information
  doing so.

  a compound command preserves @{const ‹fragments›} too.

 ›

fun
  loc_compC :: "('answer, 'location, 'question, 'state) com
                            ==> ('answer, 'location, 'question, 'state) com list
                            ==> ('answer, 'location, 'question, 'state) loc_comp"
where
  "loc_compC ({l} IF b THEN c FI) cs = lcond (atC c) (atCs cs) b"
| "loc_compC ({l} IF b THEN c1 ELSE c2 FI) cs = lcond (atC c1) (atC c2) b"
| "loc_compC (LOOP DO c OD) cs = lconst (atC c)"
| "loc_compC ({l} WHILE b DO c OD) cs = lcond (atC c) (atCs cs) b"
| "loc_compC c cs = lconst (atCs cs)"

lemma decompose_fragments:
  assumes "(c, ictxt, fctxt) ∈ decompose_com c0"
  shows "(c, loc_compC c (fctxt c @ cs)) ∈ fragments c0 (atCs cs)"
using assms
proof(induct c0 arbitrary: c ictxt fctxt cs)
  case (Loop c01 c ictxt fctxt cs)
  from Loop.prems Loop.hyps(1)[where cs="ictxt c # cs"] show ?case by (auto simp: decompose_com_ictxt)
next
  case (Seq c01 c02 c ictxt fctxt cs)
  from Seq.prems Seq.hyps(1)[where cs="c02 # cs"] show ?case by auto
qed auto

lemma at_decompose:
  assumes "(c, ictxt, fctxt) ∈ decompose_com c0"
  shows "atC c ⊆ atC c0"
using assms by (induct c0 arbitrary: c ictxt fctxt; fastforce)

lemma at_decomposeLS:
  assumes "(c, ictxt, fctxt) ∈ decomposeLS s"
  shows "atC c ⊆ atCs (cPGM s)"
using assms unfolding decomposeLS_def by (auto simp: at_decompose split: list.splits)

lemma decomposeLS_fragmentsLS:
  assumes "(c, ictxt, fctxt) ∈ decomposeLS s"
  shows "(c, loc_compC c (fctxt c @ tl (cPGM s))) ∈ fragmentsLS s"
using assms
proof(cases "cPGM s")
  case (Cons d ds)
  with assms decompose_fragments[where cs="ds"] show ?thesis
    by (cases ds) (auto simp: decomposeLS_def)
qed (simp add: decomposeLS_def)

lemma small_step_loc_compC:
  assumes "basic_com c"
  assumes "(c # cs, ls) →_<alpha> ls'"
  shows "loc_compC c cs (snd ls) = atCs (cPGM ls')"
using assms by (fastforce elim: basic_com.cases elim!: small_step_inv split: lcond_splits)

text‹

  headline result allows us to constrain the initial and final states
  a given small step in terms of the original programs, provided the
  state is reachable.

 ›

theorem decompose_small_step:
  assumes "GST sh p →_<alpha> ps'"
  assumes "reachable_state sys sh"
  obtains c cs aft
    where "(c, aft) ∈ fragments (PGMs sys p) {}"
      and "atC c ⊆ atCs (cPGM (GST sh p))"
      and "aft (cLST (GST sh p)) = atCs (cPGM ps')"
      and "(c # cs, cTKN (GST sh p), cLST (GST sh p)) →_<alpha> ps'"
      and "∀l∈atC c. cTKN ps' = Some l"
using assms
apply -
apply (frule iffD1[OF context_decompose])
apply clarsimp
apply (frule decomposeLS_fragmentsLS)
apply (frule at_decomposeLS)
apply (frule (1) subsetD[OF reachable_state_fragmentsLS])
apply (frule decomposeLS_basic_com)
apply (frule (1) small_step_loc_compC)
apply simp
done

text‹

  by induction over the reachable states
  @{thm [source] "decompose_small_step"} is quite tedious. We
  a very simple VCG that generates friendlier local proof
  in \S\ref{sec:vcg}.

 ›


subsection‹Simple-minded Hoare Logic/VCG for CIMP \label{sec:vcg}›

text‹

 label{sec:cimp-vcg}

  do not develop a proper Hoare logic or full VCG for CIMP: this
  merely packages up the subgoals that arise from induction
  the reachable states (\S\ref{sec:cimp-invariants}). This is
  in the spirit of 🍋‹"Ridge:2009"›.

  that this approach is not compositional: it consults the original
  to find matching communicating pairs, and ‹aft›
  the labels of possible successor statements. More serious Hoare
  are provided by 🍋‹"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"
  "CousotCousot89-IC"›.

  we need to discharge a proof obligation for either @{const
 Request"}s or @{const "Response"}s but not both. Here we choose to
  on @{const "Request"}s as we expect to have more local
  available about these.

 ›

inductive
  vcg :: "('answer, 'location, 'proc, 'question, 'state) programs
        ==> 'proc
        ==> ('answer, 'location, 'question, 'state) loc_comp
        ==> ('answer, 'location, 'proc, 'question, 'state) state_pred
        ==> ('answer, 'location, 'question, 'state) com
        ==> ('answer, 'location, 'proc, 'question, 'state) state_pred
        ==> bool" (‹_, _, _ ⊨/ {_}/ _/ {_}› [11,0,0,0,0,0] 11)
where
  "[ ∧aft' action' s ps' p's' l' β s' p'.
      [ pre s; ({l'} Response action', aft') ∈ fragments (coms p') {}; p ≠ p';
        ps' ∈ val β (s↓ p); (p's', β) ∈ action' (action (s↓ p)) (s↓ p');
        at p l s; at p' l' s;
        AT s' = (AT s)(p := aft (s↓ p), p' := aft' (s↓ p'));
        s'↓ = s↓(p := ps', p' := p's');
        taken p l s';
        HST s' = HST s @ [(action (s↓ p), β)];
        ∀p''∈-{p,p'}. GST s' p'' = GST s p''
      ] ==> post s'
   ] ==> coms, p, aft ⊨ {pre} {l} Request action val {post}"
| "[ ∧s ps' s'.
      [ pre s; ps' ∈ f (s↓ p);
        at p l s;
        AT s' = (AT s)(p := aft (s↓ p));
        s'↓ = s↓(p := ps');
        taken p l s';
        HST s' = HST s;
        ∀p''∈-{p}. GST s' p'' = GST s p''
      ] ==> post s'
   ] ==> coms, p, aft ⊨ {pre} {l} LocalOp f {post}"
| "[ ∧s s'.
      [ pre s;
        at p l s;
        AT s' = (AT s)(p := aft (s↓ p));
        s'↓ = s↓;
        taken p l s';
        HST s' = HST s;
        ∀p''∈-{p}. GST s' p'' = GST s p''
      ] ==> post s'
   ] ==> coms, p, aft ⊨ {pre} {l} IF b THEN t FI {post}"
| "[ ∧s s'.
      [ pre s;
        at p l s;
        AT s' = (AT s)(p := aft (s↓ p));
        s'↓ = s↓;
        taken p l s';
        HST s' = HST s;
        ∀p''∈-{p}. GST s' p'' = GST s p''
      ] ==> post s'
   ] ==> coms, p, aft ⊨ {pre} {l} IF b THEN t ELSE e FI {post}"
| "[ ∧s s'.
      [ pre s;
        at p l s;
        AT s' = (AT s)(p := aft (s↓ p));
        s'↓ = s↓;
        taken p l s';
        HST s' = HST s;
        ∀p''∈-{p}. GST s' p'' = GST s p''
      ] ==> post s'
   ] ==> coms, p, aft ⊨ {pre} {l} WHILE b DO c OD {post}"
― ‹There are no proof obligations for the following commands, but including them makes some basic rules hold (\S\ref{sec:cimp:vcg_rules}):›
| "coms, p, aft ⊨ {pre} {l} Response action {post}"
| "coms, p, aft ⊨ {pre} c1 ;; c2 {post}"
| "coms, p, aft ⊨ {pre} LOOP DO c OD {post}"
| "coms, p, aft ⊨ {pre} c1 ⊕ c2 {post}"

text‹

  abbreviate invariance with one-sided validity syntax.

 ›

abbreviation valid_inv (‹_, _, _ ⊨/ {_}/ _› [11,0,0,0,0] 11) where
  "coms, p, aft ⊨ {I} c ≡ coms, p, aft ⊨ {I} c {I}"

inductive_cases vcg_inv:
  "coms, p, aft ⊨ {pre} {l} Request action val {post}"
  "coms, p, aft ⊨ {pre} {l} LocalOp f {post}"
  "coms, p, aft ⊨ {pre} {l} IF b THEN t FI {post}"
  "coms, p, aft ⊨ {pre} {l} IF b THEN t ELSE e FI {post}"
  "coms, p, aft ⊨ {pre} {l} WHILE b DO c OD {post}"
  "coms, p, aft ⊨ {pre} LOOP DO c OD {post}"
  "coms, p, aft ⊨ {pre} {l} Response action {post}"
  "coms, p, aft ⊨ {pre} c1 ;; c2 {post}"
  "coms, p, aft ⊨ {pre} Choose c1 c2 {post}"

text‹

  tweak @{const "fragments"} by omitting @{const "Response"}s,
  fewer obligations

 ›

fun
  vcg_fragments' :: "('answer, 'location, 'question, 'state) com
               ==> 'location set
               ==> ( ('answer, 'location, 'question, 'state) com
                 × ('answer, 'location, 'question, 'state) loc_comp ) set"
where
  "vcg_fragments' ({l} Response action) aft = {}"
| "vcg_fragments' ({l} IF b THEN c FI) aft
       = vcg_fragments' c aft
       ∪ { ({l} IF b THEN c' FI, lcond (atC c) aft b) |c'. True }"
| "vcg_fragments' ({l} IF b THEN c1 ELSE c2 FI) aft
       = vcg_fragments' c2 aft ∪ vcg_fragments' c1 aft
       ∪ { ({l} IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2) b) |c1' c2'. True }"
| "vcg_fragments' (LOOP DO c OD) aft = vcg_fragments' c (atC c)"
| "vcg_fragments' ({l} WHILE b DO c OD) aft
       = vcg_fragments' c {l} ∪ { ({l} WHILE b DO c' OD, lcond (atC c) aft b) |c'. True }"
| "vcg_fragments' (c1 ;; c2) aft = vcg_fragments' c2 aft ∪ vcg_fragments' c1 (atC c2)"
| "vcg_fragments' (c1 ⊕ c2) aft = vcg_fragments' c1 aft ∪ vcg_fragments' c2 aft"
| "vcg_fragments' c aft = {(c, lconst aft)}"

abbreviation
  vcg_fragments :: "('answer, 'location, 'question, 'state) com
                  ==> ( ('answer, 'location, 'question, 'state) com
                    × ('answer, 'location, 'question, 'state) loc_comp ) set"
where
  "vcg_fragments c ≡ vcg_fragments' c {}"

fun isResponse :: "('answer, 'location, 'question, 'state) com ==> bool" where
  "isResponse ({l} Response action) ⟷ True"
| "isResponse _ ⟷ False"

lemma fragments_vcg_fragments':
  "[ (c, aft) ∈ fragments c' aft'; ¬isResponse c ] ==> (c, aft) ∈ vcg_fragments' c' aft'"
by (induct c' arbitrary: aft') auto

lemma vcg_fragments'_fragments:
  "vcg_fragments' c' aft' ⊆ fragments c' aft'" 
by (induct c' arbitrary: aft') (auto 10 0)

lemma VCG_step:
  assumes V: "∧p. ∀(c, aft) ∈ vcg_fragments (PGMs sys p). PGMs sys, p, aft ⊨ {pre} c {post}"
  assumes S: "system_step p sh' sh"
  assumes R: "reachable_state sys sh"
  assumes P: "pre sh"
  shows "post sh'"
using S
proof cases
  case LocalStep with P show ?thesis
    apply -
    apply (erule decompose_small_step[OF _ R])
    apply (frule fragments_basic_com)
    apply (erule basic_com.cases)
    apply (fastforce dest!: fragments_vcg_fragments' V[rule_format]
                      elim: vcg_inv elim!: small_step_inv
                      simp: LST_def AT_def taken_def fun_eq_iff)+
    done
next
  case CommunicationStep with P show ?thesis
    apply -
    apply (erule decompose_small_step[OF _ R])
    apply (erule decompose_small_step[OF _ R])
    subgoal for c cs aft c' cs' aft'
    apply (frule fragments_basic_com[where c'=c])
    apply (frule fragments_basic_com[where c'=c'])
    apply (elim basic_com.cases; clarsimp elim!: small_step_inv)
    apply (drule fragments_vcg_fragments')
    apply (fastforce dest!: V[rule_format]
                      elim: vcg_inv elim!: small_step_inv
                      simp: LST_def AT_def taken_def fun_eq_iff)+
    done
    done
qed

text‹

  user sees the conclusion of ‹V› for each element of @{const ‹vcg_fragments›}.

 ›

lemma VCG_step_inv_stable:
  assumes V: "∧p. ∀(c, aft) ∈ vcg_fragments (PGMs sys p). PGMs sys, p, aft ⊨ {I} c"
  assumes "prerun sys σ"
  shows "(⌈I⌉ \<hookrightarrow> ◯⌈I⌉) σ"
apply (rule alwaysI)
apply clarsimp
apply (rule nextI)
apply clarsimp
using assms(2) unfolding prerun_def
apply clarsimp
apply (erule_tac i=i in alwaysE)
unfolding system_step_reflclp_def
apply clarsimp
apply (erule disjE; clarsimp)
using VCG_step[where pre=I and post=I] V assms(2) prerun_reachable_state
apply blast
done

lemma VCG:
  assumes I: "∀s. initial_state sys s ⟶ I ((GST = s, HST = []))"
  assumes V: "∧p. ∀(c, aft) ∈ vcg_fragments (PGMs sys p). PGMs sys, p, aft ⊨ {I} c"
  shows "sys ⊨ I"
apply (rule prerun_valid_induct)
 apply (clarsimp simp: prerun_def state_prop_def)
 apply (metis (full_types) I old.unit.exhaust system_state.surjective)
using VCG_step_inv_stable[OF V] apply blast
done

lemmas VCG_valid = valid_prerun_lift[OF VCG, of sys I] for sys I
(*<*)

end
(*>*)