# Theory CIMP_pred

(*<*)
(*
* 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_pred
imports
Main
begin

(* Extra HOL *)

lemma triv: "P ⟹ P"
by simp

lemma always_eventually_pigeonhole:
"(∀i. ∃n≥i. ∃m≤k. P m n) ⟷ (∃m≤k::nat. ∀i::nat. ∃n≥i. P m n)"
proof(induct k)
case (Suc k) then show ?case
apply (auto 8 0)
using le_SucI apply blast
apply (metis (full_types) le_Suc_eq nat_le_linear order_trans)
done
qed simp

(*>*)
section‹ Point-free notation ›

text‹

\label{sec:cimp-lifted-predicates}

Typically we define predicates as functions of a state. The following
provide a somewhat comfortable point-free imitation of Isabelle/HOL's
operators.

›

abbreviation (input)
pred_K :: "'b ⇒ 'a ⇒ 'b" ("⟨_⟩") where
"⟨f⟩ ≡ λs. f"

abbreviation (input)
pred_not :: "('a ⇒ bool) ⇒ 'a ⇒ bool" ("❙¬ _" [40] 40) where
"❙¬a ≡ λs. ¬a s"

abbreviation (input)
pred_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr "❙∧" 35) where
"a ❙∧ b ≡ λs. a s ∧ b s"

abbreviation (input)
pred_disj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr "❙∨" 30) where
"a ❙∨ b ≡ λs. a s ∨ b s"

abbreviation (input)
pred_implies :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr "❙⟶" 25) where
"a ❙⟶ b ≡ λs. a s ⟶ b s"

abbreviation (input)
pred_iff :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr "❙⟷" 25) where
"a ❙⟷ b ≡ λs. a s ⟷ b s"

abbreviation (input)
pred_eq :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix "❙=" 40) where
"a ❙= b ≡ λs. a s = b s"

abbreviation (input)
pred_member :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ bool" (infix "❙∈" 40) where
"a ❙∈ b ≡ λs. a s ∈ b s"

abbreviation (input)
pred_neq :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix "❙≠" 40) where
"a ❙≠ b ≡ λs. a s ≠ b s"

abbreviation (input)
pred_If :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" ("(If (_)/ Then (_)/ Else (_))" [0, 0, 10] 10)
where "If P Then x Else y ≡ λs. if P s then x s else y s"

abbreviation (input)
pred_less :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix "❙<" 40) where
"a ❙< b ≡ λs. a s < b s"

abbreviation (input)
pred_le :: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ bool" (infix "❙≤" 40) where
"a ❙≤ b ≡ λs. a s ≤ b s"

abbreviation (input)
pred_plus :: "('a ⇒ 'b::plus) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl "❙+" 65) where
"a ❙+ b ≡ λs. a s + b s"

abbreviation (input)
pred_minus :: "('a ⇒ 'b::minus) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixl "❙-" 65) where
"a ❙- b ≡ λs. a s - b s"

abbreviation (input)
fun_fanout :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infix "❙⨝" 35) where
"f ❙⨝ g ≡ λx. (f x, g x)"

abbreviation (input)
pred_all :: "('b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" (binder "❙∀" 10) where
"❙∀x. P x ≡ λs. ∀x. P x s"

abbreviation (input)
pred_ex :: "('b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" (binder "❙∃" 10) where
"❙∃x. P x ≡ λs. ∃x. P x s"

abbreviation (input)
pred_app :: "('b ⇒ 'a ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c" (infixl "❙$" 100) where "f ❙$ g ≡ λs. f (g s) s"

abbreviation (input)
pred_subseteq :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ bool" (infix "❙⊆" 50) where
"A ❙⊆ B ≡ λs. A s ⊆ B s"

abbreviation (input)
pred_union :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ 'b set" (infixl "❙∪" 65) where
"a ❙∪ b ≡ λs. a s ∪ b s"

abbreviation (input)
pred_inter :: "('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ 'a ⇒ 'b set" (infixl "❙∩" 65) where
"a ❙∩ b ≡ λs. a s ∩ b s"

text‹

More application specific.

›

abbreviation (input)
pred_conjoin :: "('a ⇒ bool) list ⇒ 'a ⇒ bool" where
"pred_conjoin xs ≡ foldr (❙∧) xs ⟨True⟩"

abbreviation (input)
pred_disjoin :: "('a ⇒ bool) list ⇒ 'a ⇒ bool" where
"pred_disjoin xs ≡ foldr (❙∨) xs ⟨False⟩"

abbreviation (input)
pred_is_none :: "('a ⇒ 'b option) ⇒ 'a ⇒ bool" ("NULL _" [40] 40) where
"NULL a ≡ λs. a s = None"

abbreviation (input)
pred_empty :: "('a ⇒ 'b set) ⇒ 'a ⇒ bool" ("EMPTY _" [40] 40) where
"EMPTY a ≡ λs. a s = {}"

abbreviation (input)
pred_list_null :: "('a ⇒ 'b list) ⇒ 'a ⇒ bool" ("LIST'_NULL _" [40] 40) where
"LIST_NULL a ≡ λs. a s = []"

abbreviation (input)
pred_list_append :: "('a ⇒ 'b list) ⇒ ('a ⇒ 'b list) ⇒ 'a ⇒ 'b list" (infixr "❙@" 65) where
"xs ❙@ ys ≡ λs. xs s @ ys s"

abbreviation (input)
pred_pair :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infixr "❙⊗" 60) where
"a ❙⊗ b ≡ λs. (a s, b s)"

abbreviation (input)
pred_singleton :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b set" where
"pred_singleton x ≡ λs. {x s}"
(*<*)

end
(*>*)


# Theory Infinite_Sequences

(*<*)
theory Infinite_Sequences
imports
CIMP_pred
begin

(*>*)
section‹ Infinite Sequences \label{sec:infinite_sequences}›

text‹

Infinite sequences and some operations on them.

We use the customary function-based representation.

›

type_synonym 'a seq = "nat ⇒ 'a"
type_synonym 'a seq_pred = "'a seq ⇒ bool"

definition suffix :: "'a seq ⇒ nat ⇒ 'a seq" (infixl "|⇩s" 60) where
"σ |⇩s i ≡ λj. σ (j + i)"

primrec stake :: "nat ⇒ 'a seq ⇒ 'a list" where
"stake 0 σ = []"
| "stake (Suc n) σ = σ 0 # stake n (σ |⇩s 1)"

primrec shift :: "'a list ⇒ 'a seq ⇒ 'a seq" (infixr ‹@-› 65) where
"shift [] σ = σ"
| "shift (x # xs) σ = (λi. case i of 0 ⇒ x | Suc i ⇒ shift xs σ i)"

(* FIXME misleading: this is σ(i, i+j). Use a bundle for this notation. FIXME move *)
abbreviation interval_syn ("_'(_ → _')" [69, 0, 0] 70) where (* FIXME priorities *)
"σ(i → j) ≡ stake j (σ |⇩s i)"

lemma suffix_eval: "(σ |⇩s i) j = σ (j + i)"
unfolding suffix_def by simp

lemma suffix_plus: "σ |⇩s n |⇩s m = σ |⇩s (m + n)"

lemma suffix_commute: "((σ |⇩s n) |⇩s m) = ((σ |⇩s m) |⇩s n)"

lemma suffix_plus_com: "σ |⇩s m |⇩s n = σ |⇩s (m + n)"
proof -
have "σ |⇩s n |⇩s m = σ |⇩s (m + n)" by (rule suffix_plus)
then show "σ |⇩s m |⇩s n = σ |⇩s (m + n)" by (simp add: suffix_commute)
qed

lemma suffix_zero: "σ |⇩s 0 = σ"
unfolding suffix_def by simp

lemma comp_suffix: "f ∘ σ |⇩s i = (f ∘ σ) |⇩s i"
unfolding suffix_def comp_def by simp

lemmas suffix_simps[simp] =
comp_suffix
suffix_eval
suffix_plus_com
suffix_zero

lemma length_stake[simp]: "length (stake n s) = n"
by (induct n arbitrary: s) auto

lemma shift_simps[simp]:
"(xs @- σ) 0 = (if xs = [] then σ 0 else hd xs)"
"(xs @- σ) |⇩s Suc 0 = (if xs = [] then σ |⇩s Suc 0 else tl xs @- σ)"
by (induct xs) auto

lemma stake_nil[simp]:
"stake i σ = [] ⟷ i = 0"
by (cases i; clarsimp)

lemma stake_shift:
"stake i (w @- σ) = take i w @ stake (i - length w) σ"
by (induct i arbitrary: w) (auto simp: neq_Nil_conv)

lemma shift_snth_less[simp]:
assumes "i < length xs"
shows "(xs @- σ) i = xs ! i"
using assms
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case by (cases xs) simp_all
qed (simp add: hd_conv_nth nth_tl)

lemma shift_snth_ge[simp]:
assumes "i ≥ length xs"
shows "(xs @- σ) i = σ (i - length xs)"
using assms
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case by (cases xs) simp_all
qed simp

lemma shift_snth:
"(xs @- σ) i = (if i < length xs then xs ! i else σ (i - length xs))"
by simp

lemma suffix_shift:
"(xs @- σ) |⇩s i = drop i xs @- (σ |⇩s i - length xs)"
proof(induct i arbitrary: xs)
case (Suc i xs) then show ?case by (cases xs) simp_all
qed simp

lemma stake_nth[simp]:
assumes "i < j"
shows "stake j s ! i = s i"
using assms by (induct j arbitrary: s i) (simp_all add: nth_Cons')

lemma stake_suffix_id:
"stake i σ @- (σ |⇩s i) = σ"
by (induct i) (simp_all add: fun_eq_iff shift_snth split: nat.splits)

lemma id_stake_snth_suffix:
"σ = (stake i σ @ [σ i]) @- (σ |⇩s Suc i)"
using stake_suffix_id
apply (metis Suc_diff_le append_Nil2 diff_is_0_eq length_stake lessI nat.simps(3) nat_le_linear shift_snth stake_nil stake_shift take_Suc_conv_app_nth)
done

"stake i σ @ stake j (σ |⇩s i) = stake (i + j) σ"
apply (induct i arbitrary: σ)
apply simp
apply auto
apply (metis One_nat_def plus_1_eq_Suc suffix_plus_com)
done

lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s"
proof (induct n arbitrary: u)
case (Suc n) then show ?case
apply clarsimp
apply (cases u)
apply auto
done
qed auto

lemma stake_shift_stake_shift:
"stake i σ @- stake j (σ |⇩s i) @- β = stake (i + j) σ @- β"
apply (induct i arbitrary: σ)
apply simp
apply auto
apply (metis One_nat_def plus_1_eq_Suc suffix_plus_com)
done

lemma stake_suffix_drop:
"stake i (σ |⇩s j) = drop j (stake (i + j) σ)"
by (metis append_eq_conv_conj length_stake semiring_normalization_rules(24) stake_add)

lemma stake_suffix:
assumes "i ≤ j"
shows "stake j σ @- u |⇩s i = σ(i → j - i) @- u"
by (simp add: assms stake_suffix_drop suffix_shift)

subsection‹Decomposing safety and liveness \label{sec:infinite_sequences-safety-liveness}›

text‹

Famously properties on infinite sequences can be decomposed into
@{emph ‹safety›} and @{emph ‹liveness›}
properties @{cite "AlpernSchneider:1985" and "Schneider:1987"}. See
@{cite [cite_macro=citet] "Kindler:1994"} for an overview.

›

definition safety :: "'a seq_pred ⇒ bool" where
"safety P ⟷ (∀σ. ¬P σ ⟶ (∃i. ∀β. ¬P (stake i σ @- β)))"

lemma safety_def2: ― ‹Contraposition gives the customary prefix-closure definition›
"safety P ⟷ (∀σ. (∀i. ∃β. P (stake i σ @- β)) ⟶ P σ)"
unfolding safety_def by blast

definition liveness :: "'a seq_pred ⇒ bool" where
"liveness P ⟷ (∀α. ∃σ. P (α @- σ))"

lemmas safetyI = iffD2[OF safety_def, rule_format]
lemmas safetyI2 = iffD2[OF safety_def2, rule_format]
lemmas livenessI = iffD2[OF liveness_def, rule_format]

lemma safety_False:
shows "safety (λσ. False)"
by (rule safetyI) simp

lemma safety_True:
shows "safety (λσ. True)"
by (rule safetyI) simp

lemma safety_state_prop:
shows "safety (λσ. P (σ 0))"
by (rule safetyI) auto

lemma safety_invariant:
shows "safety (λσ. ∀i. P (σ i))"
apply (rule safetyI)
apply clarsimp
apply (metis length_stake lessI shift_snth_less stake_nth)
done

lemma safety_transition_relation:
shows "safety (λσ. ∀i. (σ i, σ (i + 1)) ∈ R)"
apply (rule safetyI)
apply clarsimp
apply (metis (no_types, hide_lams) Suc_eq_plus1 add.left_neutral add_Suc_right add_diff_cancel_left' le_add1 list.sel(1) list.simps(3) shift_simps(1) stake.simps(2) stake_suffix suffix_def)
done

lemma safety_conj:
assumes "safety P"
assumes "safety Q"
shows "safety (P ❙∧ Q)"
using assms unfolding safety_def by blast

lemma safety_always_eventually[simplified]:
assumes "safety P"
assumes "∀i. ∃j≥i. ∃β. P (σ(0 → j) @- β)"
shows "P σ"
using assms unfolding safety_def2
apply -
apply (drule_tac x=σ in spec)
apply clarsimp
apply (drule_tac x=i in spec)
apply clarsimp
apply (rule_tac x="(stake j σ @- β) |⇩s i" in exI)
apply (simp add: stake_shift_stake_shift stake_suffix)
done

lemma safety_disj:
assumes "safety P"
assumes "safety Q"
shows "safety (P ❙∨ Q)"
unfolding safety_def2 using assms

text‹

The decomposition is given by a form of closure.

›

definition M⇩p :: "'a seq_pred ⇒ 'a seq_pred" where
"M⇩p P = (λσ. ∀i. ∃β. P (stake i σ @- β))"

definition Safe :: "'a seq_pred ⇒ 'a seq_pred" where
"Safe P = (P ❙∨ M⇩p P)"

definition Live :: "'a seq_pred ⇒ 'a seq_pred" where
"Live P = (P ❙∨ ❙¬M⇩p P)"

lemma decomp:
"P = (Safe P ❙∧ Live P)"
unfolding Safe_def Live_def by blast

lemma safe:
"safety (Safe P)"
unfolding Safe_def safety_def M⇩p_def
apply clarsimp
apply (simp add: stake_shift)
apply (rule_tac x=i in exI)
apply clarsimp
apply (rule_tac x=i in exI)
apply clarsimp
done

lemma live:
"liveness (Live P)"
proof(rule livenessI)
fix α
have "(∃β. P (α @- β)) ∨ ¬(∃β. P (α @- β))" by blast
also have "?this ⟷ (∃β. P (α @- β) ∨ (∀γ. ¬P (α @- γ)))" by blast
also have "… ⟷ (∃β. P (α @- β) ∨ (∃i. i = length α ∧ (∀γ. ¬P (stake i (α @- β) @- γ))))" by (simp add: stake_shift)
also have "… ⟶ (∃β. P (α @- β) ∨ (∃i. (∀γ. ¬P (stake i (α @- β) @- γ))))" by blast
finally have "∃β. P (α @- β) ∨ (∃i. ∀γ. ¬ P (stake i (α @- β) @- γ))" .
then show "∃σ. Live P (α @- σ)" unfolding Live_def M⇩p_def by simp
qed

text‹

@{cite "Sistla:1994"} proceeds to give a topological analysis of fairness. An ∗‹absolute›
liveness property is a liveness property whose complement is stable.

›

definition absolute_liveness :: "'a seq_pred ⇒ bool" where ― ‹ closed under prepending any finite sequence ›
"absolute_liveness P ⟷ (∃σ. P σ) ∧ (∀σ α. P σ ⟶ P (α @- σ))"

definition stable :: "'a seq_pred ⇒ bool" where ― ‹ closed under suffixes ›
"stable P ⟷ (∃σ. P σ) ∧ (∀σ i. P σ ⟶ P (σ |⇩s i))"

lemma absolute_liveness_liveness:
assumes "absolute_liveness P"
shows "liveness P"
using assms unfolding absolute_liveness_def liveness_def by blast

lemma stable_absolute_liveness:
assumes "P σ"
assumes "¬P σ'" ―‹ extra hypothesis ›
shows "stable P ⟷ absolute_liveness (❙¬ P)"
using assms unfolding stable_def absolute_liveness_def
apply auto
apply (metis cancel_comm_monoid_add_class.diff_cancel drop_eq_Nil order_refl shift.simps(1) suffix_shift suffix_zero)
apply (metis stake_suffix_id)
done

(*
text‹

Fairness ala Sistla. Unmotivated.

FIXME safety properties are insensitive to fairness.
FIXME typically we prove ‹sys ⟶ safety›. The result below doesn't appear strong enough.
FIXME observe fairness is a special liveness property.

›
*)

definition fairness :: "'a seq_pred ⇒ bool" where
"fairness P ⟷ stable P ∧ absolute_liveness P"

lemma fairness_safety:
assumes "safety P"
assumes "fairness F"
shows "(∀σ. F σ ⟶ P σ) ⟷ (∀σ. P σ)"
apply rule
using assms
apply clarsimp
unfolding safety_def fairness_def stable_def absolute_liveness_def
apply clarsimp
apply blast+
done

(*<*)

end
(*>*)


# Theory LTL

(*<*)
theory LTL
imports
CIMP_pred
Infinite_Sequences
begin

(*>*)
section‹ Linear Temporal Logic \label{sec:ltl}›

text‹

To talk about liveness we need to consider infinitary behaviour on
sequences. Traditionally future-time linear temporal logic (LTL) is used to do
this @{cite "MannaPnueli:1991" and "OwickiLamport:1982"}.

The following is a straightforward shallow embedding of the
now-traditional anchored semantics of LTL @{cite "MannaPnueli:1988"}. Some of it is adapted
from the sophisticated TLA development in the AFP due to @{cite [cite_macro=citet] "TLA-AFP"}.

Unlike @{cite [cite_macro=citet] "Lamport:2002"}, include the
next operator, which is convenient for stating rules. Sometimes it allows us to
ignore the system, i.e. to state rules as temporally valid
(LTL-valid) rather than just temporally program valid (LTL-cimp-), in Jackson's terminology.

›

definition state_prop :: "('a ⇒ bool) ⇒ 'a seq_pred" ("⌈_⌉") where
"⌈P⌉ = (λσ. P (σ 0))"

definition "next" :: "'a seq_pred ⇒ 'a seq_pred" ("○_" [80] 80) where
"(○P) = (λσ. P (σ |⇩s 1))"

definition always :: "'a seq_pred ⇒ 'a seq_pred" ("□_" [80] 80) where
"(□P) = (λσ. ∀i. P (σ |⇩s i))"

definition until :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr "𝒰" 30) where (* FIXME priority, binds tighter than ❙⟶ *)
"(P 𝒰 Q) = (λσ. ∃i. Q (σ |⇩s i) ∧ (∀k<i. P (σ |⇩s k)))"

definition eventually :: "'a seq_pred ⇒ 'a seq_pred" ("◇_" [80] 80) where (* FIXME priority, consider making an abbreviation *)
"(◇P) = (⟨True⟩ 𝒰 P)"

definition release :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr "ℛ" 30) where (* FIXME priority, dual of Until *)
"(P ℛ Q) = (❙¬(❙¬P 𝒰 ❙¬Q))"

definition unless :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr "𝒲" 30) where (* FIXME priority, aka weak until *)
"(P 𝒲 Q) = ((P 𝒰 Q) ❙∨ □P)"

abbreviation (input)
pred_always_imp_syn :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr "❙↪" 25) where
"P ❙↪ Q ≡ □(P ❙⟶ Q)"

lemmas defs =
state_prop_def
always_def
eventually_def
next_def
release_def
unless_def
until_def

lemma suffix_state_prop[simp]:
shows "⌈P⌉ (σ |⇩s i) = P (σ i)"
unfolding defs by simp

lemma alwaysI[intro]:
assumes "⋀i. P (σ |⇩s i)"
shows "(□P) σ"
unfolding defs using assms by blast

lemma alwaysD:
assumes "(□P) σ"
shows "P (σ |⇩s i)"
using assms unfolding defs by blast

lemma alwaysE: "⟦(□P) σ; P (σ |⇩s i) ⟹ Q⟧ ⟹ Q"
unfolding defs by blast

lemma always_induct:
assumes "P σ"
assumes "(□(P ❙⟶ ○P)) σ"
shows "(□P) σ"
proof(rule alwaysI)
fix i from assms show "P (σ |⇩s i)"
unfolding defs by (induct i) simp_all
qed

lemma seq_comp:
fixes σ :: "'a seq"
fixes P :: "'b seq_pred"
fixes f :: "'a ⇒ 'b"
shows
"(□P) (f ∘ σ) ⟷ (□(λσ. P (f ∘ σ))) σ"
"(◇P) (f ∘ σ) ⟷ (◇(λσ. P (f ∘ σ))) σ"
"(P 𝒰 Q) (f ∘ σ) ⟷ ((λσ. P (f ∘ σ)) 𝒰 (λσ. Q (f ∘ σ))) σ"
"(P 𝒲 Q) (f ∘ σ) ⟷ ((λσ. P (f ∘ σ)) 𝒲 (λσ. Q (f ∘ σ))) σ"
unfolding defs by simp_all

lemma nextI[intro]:
assumes "P (σ |⇩s Suc 0)"
shows "(○P) σ"
using assms unfolding defs by simp

lemma untilI[intro]:
assumes "Q (σ |⇩s i)"
assumes "∀k<i. P (σ |⇩s k)"
shows "(P 𝒰 Q) σ"
unfolding defs using assms by blast

lemma untilE:
assumes "(P 𝒰 Q) σ"
obtains i where "Q (σ |⇩s i)" and "∀k<i. P (σ |⇩s k)"
using assms unfolding until_def by blast

lemma eventuallyI[intro]:
assumes "P (σ |⇩s i)"
shows "(◇P) σ"
unfolding eventually_def using assms by blast

lemma eventuallyE[elim]:
assumes "(◇P) σ"
obtains i where "P (σ |⇩s i)"
using assms unfolding defs by (blast elim: untilE)

lemma unless_alwaysI:
assumes "(□ P) σ"
shows "(P 𝒲 Q) σ"
using assms unfolding defs by blast

lemma unless_untilI:
assumes "Q (σ |⇩s j)"
assumes "⋀i. i < j ⟹ P (σ |⇩s i)"
shows "(P 𝒲 Q) σ"
unfolding defs using assms by blast

lemma always_imp_refl[iff]:
shows "(P ❙↪ P) σ"
unfolding defs by blast

lemma always_imp_trans:
assumes "(P ❙↪ Q) σ"
assumes "(Q ❙↪ R) σ"
shows "(P ❙↪ R) σ"
using assms unfolding defs by blast

lemma always_imp_mp:
assumes "(P ❙↪ Q) σ"
assumes "P σ"
shows "Q σ"
using assms unfolding defs by (metis suffix_zero)

lemma always_imp_mp_suffix:
assumes "(P ❙↪ Q) σ"
assumes "P (σ |⇩s i)"
shows "Q (σ |⇩s i)"
using assms unfolding defs by metis

text‹

Some basic facts and equivalences, mostly sanity.

›

lemma necessitation:
"(⋀s. P s) ⟹ (□P) σ"
"(⋀s. P s) ⟹ (◇P) σ"
"(⋀s. P s) ⟹ (P 𝒲 Q) σ"
"(⋀s. Q s) ⟹ (P 𝒰 Q) σ"
unfolding defs by auto

lemma cong:
"(⋀s. P s = P' s) ⟹ ⌈P⌉ = ⌈P'⌉"
"(⋀σ. P σ = P' σ) ⟹ (□P) = (□P')"
"(⋀σ. P σ = P' σ) ⟹ (◇P) = (◇P')"
"(⋀σ. P σ = P' σ) ⟹ (○P) = (○P')"
"⟦⋀σ. P σ = P' σ; ⋀σ. Q σ = Q' σ⟧ ⟹ (P 𝒰 Q) = (P' 𝒰 Q')"
"⟦⋀σ. P σ = P' σ; ⋀σ. Q σ = Q' σ⟧ ⟹ (P 𝒲 Q) = (P' 𝒲 Q')"
unfolding defs by auto

lemma norm[simp]:
"⌈⟨False⟩⌉ = ⟨False⟩"
"⌈⟨True⟩⌉ = ⟨True⟩"
"(❙¬⌈p⌉) = ⌈❙¬p⌉"
"(⌈p⌉ ❙∧ ⌈q⌉) = ⌈p ❙∧ q⌉"
"(⌈p⌉ ❙∨ ⌈q⌉) = ⌈p ❙∨ q⌉"
"(⌈p⌉ ❙⟶ ⌈q⌉) = ⌈p ❙⟶ q⌉"
"(⌈p⌉ σ ∧ ⌈q⌉ σ) = ⌈p ❙∧ q⌉ σ"
"(⌈p⌉ σ ∨ ⌈q⌉ σ) = ⌈p ❙∨ q⌉ σ"
"(⌈p⌉ σ ⟶ ⌈q⌉ σ) = ⌈p ❙⟶ q⌉ σ"

"(○⟨False⟩) = ⟨False⟩"
"(○⟨True⟩) = ⟨True⟩"

"(□⟨False⟩) = ⟨False⟩"
"(□⟨True⟩) = ⟨True⟩"
"(❙¬□ P) σ = (◇ (❙¬ P)) σ"
"(□□ P) = (□ P)"

"(◇⟨False⟩) = ⟨False⟩"
"(◇⟨True⟩) = ⟨True⟩"
"(❙¬◇ P) = (□ (❙¬ P))"
"(◇◇ P) = (◇ P)"

"(P 𝒲 ⟨False⟩) = (□ P)"

"(❙¬(P 𝒰 Q)) σ = (❙¬P ℛ ❙¬Q) σ"
"(⟨False⟩ 𝒰 P) = P"
"(P 𝒰 ⟨False⟩) = ⟨False⟩"
"(P 𝒰 ⟨True⟩) = ⟨True⟩"
"(⟨True⟩ 𝒰 P) = (◇ P)"
"(P 𝒰 (P 𝒰 Q)) = (P 𝒰 Q)"

"(❙¬(P ℛ Q)) σ = (❙¬P 𝒰 ❙¬Q) σ"
"(⟨False⟩ ℛ P) = (□P)"
"(P ℛ ⟨False⟩) = ⟨False⟩"
"(⟨True⟩ ℛ P) = P"
"(P ℛ ⟨True⟩) = ⟨True⟩"
(*
"(P 𝒰 (P 𝒰 Q)) σ = (P 𝒰 Q) σ" FIXME for Release
*)
unfolding defs
apply (auto simp: fun_eq_iff)
apply (metis suffix_plus suffix_zero)
apply (metis suffix_plus suffix_zero)
apply fastforce
apply force
apply (metis add.right_neutral not_less0)
apply force
apply fastforce
done

lemma always_conj_distrib: "(□(P ❙∧ Q)) = (□P ❙∧ □Q)"
unfolding defs by auto

lemma eventually_disj_distrib: "(◇(P ❙∨ Q)) = (◇P ❙∨ ◇Q)"
unfolding defs by auto

lemma always_eventually[elim!]:
assumes "(□P) σ"
shows "(◇P) σ"
using assms unfolding defs by auto

lemma eventually_imp_conv_disj: "(◇(P ❙⟶ Q)) = (◇(❙¬P) ❙∨ ◇Q)"
unfolding defs by auto

lemma eventually_imp_distrib:
"(◇(P ❙⟶ Q)) = (□P ❙⟶ ◇Q)"
unfolding defs by auto

lemma unfold:
"(□ P) σ = (P ❙∧ ○□P) σ"
"(◇ P) σ = (P ❙∨ ○◇P) σ"
"(P 𝒲 Q) σ = (Q ❙∨ (P ❙∧ ○(P 𝒲 Q))) σ"
"(P 𝒰 Q) σ = (Q ❙∨ (P ❙∧ ○(P 𝒰 Q))) σ"
"(P ℛ Q) σ = (Q ❙∧ (P ❙∨ ○(P ℛ Q))) σ"
unfolding defs
apply -
apply (metis (full_types) add.commute add_diff_inverse_nat less_one suffix_plus suffix_zero)
apply (metis (full_types) One_nat_def add.right_neutral add_Suc_right lessI less_Suc_eq_0_disj suffix_plus suffix_zero)

apply auto
apply fastforce
apply (metis gr0_conv_Suc nat_neq_iff not_less_eq suffix_zero)
apply (metis suffix_zero)
apply force
using less_Suc_eq_0_disj apply fastforce
apply (metis gr0_conv_Suc nat_neq_iff not_less0 suffix_zero)

apply fastforce
apply (case_tac i; auto)
apply force
using less_Suc_eq_0_disj apply force

apply force
using less_Suc_eq_0_disj apply fastforce
apply fastforce
apply (case_tac i; auto)
done

lemma mono:
"⟦(□P) σ; ⋀σ. P σ ⟹  P' σ⟧ ⟹ (□P') σ"
"⟦(◇P) σ; ⋀σ. P σ ⟹  P' σ⟧ ⟹ (◇P') σ"
"⟦(P 𝒰 Q) σ; ⋀σ. P σ ⟹ P' σ; ⋀σ. Q σ ⟹ Q' σ⟧ ⟹ (P' 𝒰 Q') σ"
"⟦(P 𝒲 Q) σ; ⋀σ. P σ ⟹ P' σ; ⋀σ. Q σ ⟹ Q' σ⟧ ⟹ (P' 𝒲 Q') σ"
unfolding defs by force+

lemma always_imp_mono:
"⟦(□P) σ; (P ❙↪ P') σ⟧ ⟹ (□P') σ"
"⟦(◇P) σ; (P ❙↪ P') σ⟧ ⟹ (◇P') σ"
"⟦(P 𝒰 Q) σ; (P ❙↪ P') σ; (Q ❙↪ Q') σ⟧ ⟹ (P' 𝒰 Q') σ"
"⟦(P 𝒲 Q) σ; (P ❙↪ P') σ; (Q ❙↪ Q') σ⟧ ⟹ (P' 𝒲 Q') σ"
unfolding defs by force+

lemma next_conj_distrib:
"(○(P ❙∧ Q)) = (○P ❙∧ ○Q)"
unfolding defs by auto

lemma next_disj_distrib:
"(○(P ❙∨ Q)) = (○P ❙∨ ○Q)"
unfolding defs by auto

lemma until_next_distrib:
"(○(P 𝒰 Q)) = (○P 𝒰 ○Q)"
unfolding defs by (auto simp: fun_eq_iff)

lemma until_imp_eventually:
"((P 𝒰 Q) ❙⟶ ◇Q) σ"
unfolding defs by auto

lemma until_until_disj:
assumes "(P 𝒰 Q 𝒰 R) σ"
shows "((P ❙∨ Q) 𝒰 R) σ"
using assms unfolding defs
apply clarsimp
done

lemma unless_unless_disj:
assumes "(P 𝒲 Q 𝒲 R) σ"
shows "((P ❙∨ Q) 𝒲 R) σ"
using assms unfolding defs
apply auto
done

lemma until_conj_distrib:
"((P ❙∧ Q) 𝒰 R) = ((P 𝒰 R) ❙∧ (Q 𝒰 R))"
unfolding defs
apply (auto simp: fun_eq_iff)
apply (metis dual_order.strict_trans nat_neq_iff)
done

lemma until_disj_distrib:
"(P 𝒰 (Q ❙∨ R)) = ((P 𝒰 Q) ❙∨ (P 𝒰 R))"
unfolding defs by (auto simp: fun_eq_iff)

lemma eventually_until:
"(◇P) = (❙¬P 𝒰 P)"
unfolding defs
apply (auto simp: fun_eq_iff)
apply (case_tac "P (x |⇩s 0)")
apply blast
apply (drule (1) ex_least_nat_less)
apply (metis le_simps(2))
done

lemma eventually_until_eventually:
"(◇(P 𝒰 Q)) = (◇Q)"
unfolding defs by force

lemma eventually_unless_until:
"((P 𝒲 Q) ❙∧ ◇Q) = (P 𝒰 Q)"
unfolding defs by force

lemma eventually_always_imp_always_eventually:
assumes "(◇□P) σ"
shows "(□◇P) σ"
using assms unfolding defs by (metis suffix_commute)

lemma eventually_always_next_stable:
assumes "(◇P) σ"
assumes "(P ❙↪ ○P) σ"
shows "(◇□P) σ"
using assms by (metis (no_types) eventuallyI alwaysD always_induct eventuallyE norm(15))

lemma next_stable_imp_eventually_always:
assumes "(P ❙↪ ○P) σ"
shows "(◇P ❙⟶ ◇□P) σ"
using assms eventually_always_next_stable by blast

lemma always_eventually_always:
"◇□◇P = □◇P"
unfolding defs by (clarsimp simp: fun_eq_iff) (metis add.left_commute semiring_normalization_rules(25))

(* FIXME define "stable", develop more rules for it *)
lemma stable_unless:
assumes "(P ❙↪ ○(P ❙∨ Q)) σ"
shows "(P ❙↪ (P 𝒲 Q)) σ"
using assms unfolding defs
apply -
apply (rule ccontr)
apply clarsimp
apply (drule (1) ex_least_nat_less[where P="λj. ¬P (σ |⇩s i + j)" for i, simplified])
apply clarsimp
apply (metis add_Suc_right le_less less_Suc_eq)
done

lemma unless_induct: ―‹ Rule \texttt{WAIT} from @{cite [cite_macro=citet] ‹Fig~3.3› "MannaPnueli:1995"}›
assumes I: "(I ❙↪ ○(I ❙∨ R)) σ"
assumes P: "(P ❙↪ I ❙∨ R) σ"
assumes Q: "(I ❙↪ Q) σ"
shows "(P ❙↪ Q 𝒲 R) σ"
apply (intro alwaysI impI)
apply (erule impE[OF alwaysD[OF P]])
apply (erule disjE)
apply (rule always_imp_mono(4)[where P=I and Q=R])
apply (erule mp[OF alwaysD[OF stable_unless[OF I]]])
apply (simp add: Q alwaysD)
apply blast
apply (simp add: unfold)
done

text‹

Most of our assertions will be of the form @{term "A ❙⟶ ◇C"} (pronounced ‹A› leads to ‹C›'')
or @{term "A ❙⟶ B 𝒰 C"} (‹A› leads to ‹C› via ‹B›'').

Most of these rules are due to @{cite [cite_macro=citet]
"Jackson:1998"} who used leads-to-via in a sequential setting. Others
are due to @{cite [cite_macro=citet] "MannaPnueli:1991"}.

The leads-to-via connective is similar to the ensures'' modality of @{cite [cite_macro=citet] ‹\S3.4.4› "ChandyMisra:1989"}.

›

abbreviation (input)
leads_to :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr "❙↝" 25) where (* FIXME priority *)
"P ❙↝ Q ≡ P ❙↪ ◇Q"

shows "(P ❙↝ P) σ"
by (metis (no_types, lifting) necessitation(1) unfold(2))

assumes "(P ❙↝ Q) σ"
assumes "(Q ❙↝ R) σ"
shows "(P ❙↝ R) σ"
using assms unfolding defs by clarsimp (metis semiring_normalization_rules(25))

assumes "(P ❙↝ Q) σ"
assumes "(◇P) σ"
shows "(◇Q) σ"
using assms unfolding defs by auto

assumes "(P' ❙↪ P) σ"
assumes "(Q ❙↪ Q') σ"
assumes "(P ❙↝ Q) σ"
shows "(P' ❙↝ Q') σ"
using assms unfolding defs by clarsimp blast

shows "(P ❙↝ Q ❙⟶ ◇P ❙⟶ ◇Q) σ"
by (metis (no_types, lifting) alwaysI unfold(2))

assumes "(P ❙↝ R) σ"
assumes "(Q ❙↝ R) σ"
shows "((P ❙∨ Q) ❙↝ R) σ"
using assms unfolding defs by simp

shows "((P ❙↪ P 𝒰 Q) ❙⟶ P ❙↝ Q) σ"
unfolding defs by clarsimp blast

assumes "(R ❙↪ R') σ"
assumes "(P ❙↪ Q 𝒰 R) σ"
shows "(P ❙↪ Q 𝒰 R') σ"
using assms unfolding LTL.defs by force

assumes "(A ❙↪ B 𝒰 C) σ"
assumes "(C ❙↪ D 𝒰 E) σ"
shows "(A ❙↪ (B ❙∨ D) 𝒰 E) σ"
proof(rule alwaysI, rule impI)
fix i assume "A (σ |⇩s i)" with assms show "((B ❙∨ D) 𝒰 E) (σ |⇩s i)"
apply -
apply (erule alwaysE[where i=i])
apply clarsimp
apply (erule untilE)
apply clarsimp (* suffix *)
apply (drule (1) always_imp_mp_suffix)
apply (erule untilE)
apply clarsimp (* suffix *)
apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps)
apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less) (* arithmetic *)
done
qed

lemma leads_to_via_disj: ― ‹ useful for case distinctions ›
assumes "(P ❙↪ Q 𝒰 R) σ"
assumes "(P' ❙↪ Q' 𝒰 R) σ"
shows "(P ❙∨ P' ❙↪ (Q ❙∨ Q') 𝒰 R) σ"
using assms unfolding defs by (auto 10 0)

lemma leads_to_via_disj': ― ‹ more like a chaining rule ›
assumes "(A ❙↪ B 𝒰 C) σ"
assumes "(C ❙↪ D 𝒰 E) σ"
shows "(A ❙∨ C ❙↪ (B ❙∨ D) 𝒰 E) σ"
proof(rule alwaysI, rule impI, erule disjE)
fix i assume "A (σ |⇩s i)" with assms show "((B ❙∨ D) 𝒰 E) (σ |⇩s i)"
apply -
apply (erule alwaysE[where i=i])
apply clarsimp
apply (erule untilE)
apply clarsimp (* suffix *)
apply (drule (1) always_imp_mp_suffix)
apply (erule untilE)
apply clarsimp (* suffix *)
apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps)
apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less) (* arithmetic *)
done
next
fix i assume "C (σ |⇩s i)" with assms(2) show "((B ❙∨ D) 𝒰 E) (σ |⇩s i)"
apply -
apply (erule alwaysE[where i=i])
apply (simp add: mono)
done
qed

assumes stable: "(P ❙∧ Q ❙↪ ○Q) σ"
assumes U: "(A ❙↪ P 𝒰 C) σ"
shows "((A ❙∧ Q) ❙↪ P 𝒰 (C ❙∧ Q)) σ"
proof(intro alwaysI impI, elim conjE)
fix i assume AP: "A (σ |⇩s i)" "Q (σ |⇩s i)"
have "Q (σ |⇩s (j + i))" if "Q (σ |⇩s i)" and "∀k<j. P (σ |⇩s (k + i))" for j
using that stable by (induct j; force simp: defs)
with U AP show "(P 𝒰 (λσ. C σ ∧ Q σ)) (σ |⇩s i)"
unfolding defs by clarsimp (metis (full_types) add.commute)
qed

assumes "wf R"
assumes indhyp: "⋀t. (A ❙∧ ⌈δ ❙= ⟨t⟩⌉ ❙↪ B 𝒰 (A ❙∧ ⌈δ ❙⊗ ⟨t⟩ ❙∈ ⟨R⟩⌉ ❙∨ C)) σ"
shows "(A ❙↪ B 𝒰 C) σ"
proof(intro alwaysI impI)
fix i assume "A (σ |⇩s i)" with ‹wf R› show "(B 𝒰 C) (σ |⇩s i)"
proof(induct "δ (σ i)" arbitrary: i)
case (less i) with indhyp[where t="δ (σ i)"] show ?case
apply -
apply (drule alwaysD[where i=i])
apply clarsimp
apply (erule untilE)
apply (rename_tac j)
apply (erule disjE; clarsimp)
apply (drule_tac x="i + j" in meta_spec; clarsimp)
apply (erule untilE; clarsimp)
apply (rename_tac j k)
apply (rule_tac i="j + k" in untilI)
apply clarsimp
apply auto
done
qed
qed

text‹

The well-founded response rule due to @{cite [cite_macro=citet] ‹Fig~1.23: \texttt{WELL} (well-founded response)›"MannaPnueli:2010"},
generalised to an arbitrary set of assertions and sequence predicates.
▪ ‹W1› generalised to be contingent.
▪ ‹W2› is a well-founded set of assertions that by ‹W1› includes ‹P›

›

(* FIXME: Does ‹Is› need to be consistent? *)
fixes Is :: "('a seq_pred × ('a ⇒ 'b)) set"
assumes "wf (R :: 'b rel)"
assumes W1: "(□(❙∃φ. ⌈⟨φ∈fst  Is⟩⌉ ❙∧ (P ❙⟶ φ))) σ"
assumes W2: "∀(φ, δ)∈Is. ∃(φ', δ')∈insert (Q, δ0) Is. ∀t. (φ ❙∧ ⌈δ ❙= ⟨t⟩⌉ ❙↝ φ' ❙∧ ⌈δ' ❙⊗ ⟨t⟩ ❙∈ ⟨R⟩⌉) σ"
shows "(P ❙↝ Q) σ"
proof -
have "(φ ❙∧ ⌈δ ❙= ⟨t⟩⌉ ❙↝ Q) σ" if "(φ, δ) ∈ Is" for φ δ t
using ‹wf R› that W2
apply (induct t arbitrary: φ δ)
unfolding LTL.defs split_def
apply clarsimp
apply (metis (no_types, hide_lams) ab_semigroup_add_class.add_ac(1) fst_eqD snd_conv surjective_pairing)
done
with W1 show ?thesis
apply -
apply (rule alwaysI)
apply clarsimp
apply (erule_tac i=i in alwaysE)
apply clarsimp
using alwaysD suffix_state_prop apply blast
done
qed

subsection‹Fairness›

text‹

A few renderings of weak fairness. @{cite [cite_macro=citet] "vanGlabbeekHofner:2019"} call this
"response to insistence" as a generalisation of weak fairness.

›

definition weakly_fair :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" where
"weakly_fair enabled taken = (□enabled ❙↪ ◇taken)"

lemma weakly_fair_def2:
shows "weakly_fair enabled taken = □(❙¬□(enabled ❙∧ ❙¬taken))"
unfolding weakly_fair_def by (metis (full_types) always_conj_distrib norm(18))

lemma weakly_fair_def3:
shows "weakly_fair enabled taken = (◇□enabled ❙⟶ □◇taken)"
unfolding weakly_fair_def2
apply (clarsimp simp: fun_eq_iff)

unfolding defs (* True, but can we get there deductively? *)
apply auto
apply (metis (full_types) add.left_commute semiring_normalization_rules(25))
done

lemma weakly_fair_def4:
shows "weakly_fair enabled taken = □◇(enabled ❙⟶ taken)"
using weakly_fair_def2 by force

lemma mp_weakly_fair:
assumes "weakly_fair enabled taken σ"
assumes "(□enabled) σ"
shows "(◇taken) σ"
using assms unfolding weakly_fair_def using always_imp_mp by blast

lemma always_weakly_fair:
shows "□(weakly_fair enabled taken) = weakly_fair enabled taken"
unfolding weakly_fair_def by simp

lemma eventually_weakly_fair:
shows "◇(weakly_fair enabled taken) = weakly_fair enabled taken"
unfolding weakly_fair_def2 by (simp add: always_eventually_always)

lemma weakly_fair_weaken:
assumes "(enabled' ❙↪ enabled) σ"
assumes "(taken ❙↪ taken') σ"
shows "(weakly_fair enabled taken ❙↪  weakly_fair enabled' taken') σ"
using assms unfolding weakly_fair_def defs by simp blast

lemma weakly_fair_unless_until:
shows "(weakly_fair enabled taken ❙∧ (enabled ❙↪ enabled 𝒲 taken)) = (enabled ❙↪ enabled 𝒰 taken)"
unfolding defs weakly_fair_def
apply (auto simp: fun_eq_iff)
done

assumes "(enabled ❙↪ ○(enabled ❙∨ taken)) σ"
shows "(enabled ❙↪ (□enabled ❙∨ ◇taken)) σ"
using assms unfolding defs
apply -
apply (rule ccontr)
apply clarsimp
apply (drule (1) ex_least_nat_less[where P="λj. ¬ enabled (σ |⇩s i + j)" for i, simplified])
apply clarsimp
apply (metis add_Suc_right leI less_irrefl_nat)
done

assumes "(weakly_fair enabled taken) σ"
assumes "(enabled ❙↪ ○(enabled ❙∨ taken)) σ"
shows "(enabled ❙↝ taken) σ"
using stable_leads_to_eventually[OF assms(2)] assms(1) unfolding defs weakly_fair_def
by (auto simp: fun_eq_iff)

assumes "(weakly_fair enabled taken) σ"
assumes "(enabled ❙↪ ○(enabled ❙∨ taken)) σ"
shows "(enabled ❙↪ enabled 𝒰 taken) σ"
using stable_unless[OF assms(2)] assms(1) by (metis (mono_tags) weakly_fair_unless_until)

text‹

Similarly for strong fairness. @{cite [cite_macro=citet] "vanGlabbeekHofner:2019"} call this
"response to persistence" as a generalisation of strong fairness.

›

definition strongly_fair :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" where
"strongly_fair enabled taken = (□◇enabled ❙↪ ◇taken)"

lemma strongly_fair_def2:
"strongly_fair enabled taken = □(❙¬□(◇enabled ❙∧ ❙¬taken))"
unfolding strongly_fair_def by (metis weakly_fair_def weakly_fair_def2)

lemma strongly_fair_def3:
"strongly_fair enabled taken = (□◇enabled ❙⟶ □◇taken)"
unfolding strongly_fair_def2 by (metis (full_types) always_eventually_always weakly_fair_def2 weakly_fair_def3)

lemma always_strongly_fair:
"□(strongly_fair enabled taken) = strongly_fair enabled taken"
unfolding strongly_fair_def by simp

lemma eventually_strongly_fair:
"◇(strongly_fair enabled taken) = strongly_fair enabled taken"
unfolding strongly_fair_def2 by (simp add: always_eventually_always)

lemma strongly_fair_disj_distrib: ― ‹not true for ‹weakly_fair››
"strongly_fair (enabled1 ❙∨ enabled2) taken = (strongly_fair enabled1 taken ❙∧ strongly_fair enabled2 taken)"
unfolding strongly_fair_def defs
apply (auto simp: fun_eq_iff)
apply blast
apply blast
apply (metis (full_types) semiring_normalization_rules(25))
done

lemma strongly_fair_imp_weakly_fair:
assumes "strongly_fair enabled taken σ"
shows "weakly_fair enabled taken σ"
using assms unfolding strongly_fair_def3 weakly_fair_def3 by (simp add: eventually_always_imp_always_eventually)

lemma always_enabled_weakly_fair_strongly_fair:
assumes "(□enabled) σ"
shows "weakly_fair enabled taken σ = strongly_fair enabled taken σ"
using assms by (metis strongly_fair_def3 strongly_fair_imp_weakly_fair unfold(2) weakly_fair_def3)

subsection‹Safety and liveness \label{sec:ltl-safety-liveness}›

text‹

@{cite [cite_macro=citet] "Sistla:1994"} shows some characterisations
of LTL formulas in terms of safety and liveness. Note his @{term
"(𝒰)"} is actually @{term "(𝒲)"}.

›

lemma safety_state_prop:
shows "safety ⌈P⌉"
unfolding defs by (rule safety_state_prop)

lemma safety_Next:
assumes "safety P"
shows "safety (○P)"
using assms unfolding defs safety_def
apply clarsimp
apply (metis (mono_tags) One_nat_def list.sel(3) nat.simps(3) stake.simps(2))
done

lemma safety_unless:
assumes "safety P"
assumes "safety Q"
shows "safety (P 𝒲 Q)"
proof(rule safetyI2)
fix σ assume X: "∃β. (P 𝒲 Q) (stake i σ @- β)" for i
then show "(P 𝒲 Q) σ"
proof(cases "∀i j. ∃β. P (σ(i → j) @- β)")
case True
with ‹safety P› have "∀i. P (σ |⇩s i)" unfolding safety_def2 by blast
then show ?thesis by (blast intro: unless_alwaysI)
next
case False
then obtain k k' where "∀β. ¬ P (σ(k → k') @- β)" by clarsimp
then have "∀i u. k + k' ≤ i ⟶ ¬P ((stake i σ @- u) |⇩s k)"
by (metis add.commute diff_add stake_shift_stake_shift stake_suffix_drop suffix_shift)
then have "∀i u. k + k' ≤ i ∧ (P 𝒲 Q) (stake i σ @- u) ⟶ (∃m≤k. Q ((stake i σ @- u) |⇩s m) ∧ (∀p<m. P ((stake i σ @- u) |⇩s p)))"
unfolding defs using leI by blast
then have "∀i u. k + k' ≤ i ∧ (P 𝒲 Q) (stake i σ @- u) ⟶ (∃m≤k. Q (σ(m → i - m) @- u) ∧ (∀p<m. P (σ(p → i - p) @- u)))"
by (metis stake_suffix add_leE nat_less_le order_trans)
then have "∀i. ∃n≥i. ∃m≤k. ∃u. Q (σ(m → n - m) @- u) ∧ (∀p<m. P (σ(p → n - p) @- u))"
then have "∃m≤k. ∀i. ∃n≥i. ∃u. Q (σ(m → n - m) @- u) ∧ (∀p<m. P (σ(p → n - p) @- u))"
by (simp add: always_eventually_pigeonhole)
with ‹safety P› ‹safety Q› show "(P 𝒲 Q) σ"
unfolding defs by (metis Nat.le_diff_conv2 add_leE safety_always_eventually)
qed
qed

lemma safety_always:
assumes "safety P"
shows "safety (□P)"
using assms by (metis norm(20) safety_def safety_unless)

lemma absolute_liveness_eventually:
shows "absolute_liveness P ⟷ (∃σ. P σ) ∧ P = ◇P"
unfolding absolute_liveness_def defs
by (metis cancel_comm_monoid_add_class.diff_cancel drop_eq_Nil order_refl shift.simps(1) stake_suffix_id suffix_shift suffix_zero)

lemma stable_always:
shows "stable P ⟷ (∃σ. P σ) ∧ P = □P"
unfolding stable_def defs by (metis suffix_zero)

(* FIXME Sistla's examples of stable properties are boring and follow directly from this lemma.
FIXME the fairness "type of formulas" follow from the above and the fairness def. *)

text‹

To show that @{const ‹weakly_fair›} is a @{const ‹fairness›} property requires some constraints on ‹enabled› and ‹taken›:
▪ it is reasonable to assume they are state formulas
▪ ‹taken› must be satisfiable

›

lemma fairness_weakly_fair:
assumes "∃s. taken s"
shows "fairness (weakly_fair ⌈enabled⌉ ⌈taken⌉)"
unfolding fairness_def stable_def absolute_liveness_def weakly_fair_def
using assms
apply auto
apply (rule_tac x="λ_ .s" in exI)
apply fastforce
apply (simp add: alwaysD)
apply (rule_tac x="λ_ .s" in exI)
apply fastforce
apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def)
done

lemma fairness_strongly_fair:
assumes "∃s. taken s"
shows "fairness (strongly_fair ⌈enabled⌉ ⌈taken⌉)"
unfolding fairness_def stable_def absolute_liveness_def strongly_fair_def
using assms
apply auto
apply (rule_tac x="λ_ .s" in exI)
apply fastforce
apply (simp add: alwaysD)
apply (rule_tac x="λ_ .s" in exI)
apply fastforce
apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def)
done

(*<*)

end
(*>*)


# Theory CIMP_lang

(*<*)
(*
* 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_lang
imports
CIMP_pred
LTL
begin

(*>*)
section‹CIMP syntax and semantics \label{sec:cimp-syntax-semantics}›

text‹

We define a small sequential programming language with synchronous
message passing primitives for describing the individual
processes. This has the advantage over raw transition systems in that
it is programmer-readable, includes sequential composition, supports a
program logic and VCG (\S\ref{sec:cimp-vcg}), etc. These processes are
composed in parallel at the top-level.

CIMP is inspired by IMP, as presented by @{cite [cite_macro=citet]
"Winskel:1993"} and @{cite [cite_macro=citet]
"ConcreteSemantics:2014"}, and the classical process algebras CCS
@{cite [cite_macro=citep] "Milner:1980" and "Milner:1989"} and CSP
@{cite [cite_macro=citep] "Hoare:1985"}. Note that the algebraic
properties of this language have not been developed.

As we operate in a concurrent setting, we need to provide a small-step
semantics (\S\ref{sec:cimp-semantics}), which we give in the style of
\emph{structural operational semantics} (SOS) as popularised by @{cite
[cite_macro=citet] "DBLP:journals/jlp/Plotkin04"}. The semantics of a
complete system (\S\ref{sec:cimp-system-steps}) is presently taken
simply to be the states reachable by interleaving the enabled steps of
the individual processes, subject to message passing rendezvous. We
leave a trace or branching semantics to future work.

This theory contains all the trusted definitions. The soundness of the other
theories supervenes upon this one.

›

subsection‹Syntax›

text‹

Programs are represented using an explicit (deep embedding) of their
syntax, as the semantics needs to track the progress of multiple
threads of control. Each (atomic) \emph{basic command}
(\S\ref{sec:cimp-decompose}) is annotated with a @{typ "'location"},
which we use in our assertions (\S\ref{sec:cimp-control-predicates}).
These locations need not be unique, though in practice they likely
will be.

Processes maintain \emph{local states} of type @{typ "'state"}. These
can be updated with arbitrary relations of @{typ "'state ⇒ 'state
set"} with ‹LocalOp›, and conditions of type @{typ "'s ⇒
bool"} are similarly shallowly embedded. This arrangement allows the
end-user to select their own level of atomicity.

The sequential composition operator and control constructs are
standard. We add the infinite looping construct ‹Loop› so we
can construct single-state reactive systems; this has implications for
fairness assertions.

›

type_synonym 's bexp = "'s ⇒ bool"

datatype ('answer, 'location, 'question, 'state) com
= Request  "'location" "'state ⇒ 'question" "'answer ⇒ 'state ⇒ 'state set"        ("⦃_⦄ Request _ _"  [0, 70, 70] 71)
| Response "'location" "'question ⇒ 'state ⇒ ('state × 'answer) set"               ("⦃_⦄ Response _"  [0, 70] 71)
| LocalOp  "'location" "'state ⇒ 'state set"                                       ("⦃_⦄ LocalOp _" [0, 70] 71)
| Cond1    "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" ("⦃_⦄ IF _ THEN _ FI" [0, 0, 0] 71)
| Cond2    "'location" "'state bexp" "('answer, 'location, 'question, 'state) com"
"('answer, 'location, 'question, 'state) com"             ("⦃_⦄ IF _/ THEN _/ ELSE _/ FI"  [0, 0, 0, 0] 71)
| Loop     "('answer, 'location, 'question, 'state) com"                           ("LOOP DO _/ OD"  [0] 71)
| While    "'location" "'state bexp" "('answer, 'location, 'question, 'state) com" ("⦃_⦄ WHILE _/ DO _/ OD"  [0, 0, 0] 71)
| Seq      "('answer, 'location, 'question, 'state) com"
"('answer, 'location, 'question, 'state) com"                           (infixr ";;" 69)
| Choose   "('answer, 'location, 'question, 'state) com"
"('answer, 'location, 'question, 'state) com"                           (infixl "⊕" 68)

text‹

We provide a one-armed conditional as it is the common form and avoids
the need to discover a label for an internal ‹SKIP› and/or
trickier proofs about the VCG.

In contrast to classical process algebras, we have local state and
distinct request and response actions. These provide an interface to
Isabelle/HOL's datatypes that avoids the need for binding (ala the
$\pi$-calculus of @{cite [cite_macro=citet] "Milner:1989"}) or large
non-deterministic sums (ala CCS @{cite [cite_macro=citep] ‹\S2.8›
"Milner:1980"}). Intuitively the requester poses a @{typ "'question"} with
a ‹Request› command, which upon rendezvous with a
responder's ‹Response› command receives an @{typ
"'answer"}. The @{typ "'question"} is a deterministic function of the
requester's local state, whereas responses can be
non-deterministic. Note that CIMP does not provide a notion of
channel; these can be modelled by a judicious choice of @{typ
"'question"}.

We also provide a binary external choice operator @{term‹Choose›} (infix @{term‹(⊕)›}).
Internal choice can be recovered in combination with local operations
(see @{cite [cite_macro=citet] ‹\S2.3› "Milner:1980"}).

We abbreviate some common commands: ‹SKIP› is a local
operation that does nothing, and the floor brackets simplify
deterministic ‹LocalOp›s. We also adopt some syntax magic from
Makarius's ‹Hoare› and ‹Multiquote› theories in the Isabelle/HOL
distribution.

›

abbreviation SKIP_syn ("⦃_⦄/ SKIP" [0] 71) where
"⦃l⦄ SKIP ≡ ⦃l⦄ LocalOp (λs. {s})"

abbreviation (input) DetLocalOp :: "'location ⇒ ('state ⇒ 'state)
⇒ ('answer, 'location, 'question, 'state) com" ("⦃_⦄ ⌊_⌋" [0, 0] 71) where
"⦃l⦄ ⌊f⌋ ≡ ⦃l⦄ LocalOp (λs. {f s})"

syntax
"_quote"        :: "'b ⇒ ('a ⇒ 'b)" ("«_»" [0] 1000)
"_antiquote"    :: "('a ⇒ 'b) ⇒ 'b" ("´_" [1000] 1000)
"_Assign"       :: "'location ⇒ idt ⇒ 'b ⇒ ('answer, 'location, 'question, 'state) com" ("(⦃_⦄ ´_ :=/ _)" [0, 0, 70] 71)
"_NonDetAssign" :: "'location ⇒ idt ⇒ 'b set ⇒ ('answer, 'location, 'question, 'state) com" ("(⦃_⦄ ´_ :∈/ _)" [0, 0, 70] 71)

abbreviation (input) NonDetAssign :: "'location ⇒ (('val ⇒ 'val) ⇒ 'state ⇒ 'state) ⇒ ('state ⇒ 'val set)
⇒ ('answer, 'location, 'question, 'state) com" where
"NonDetAssign l upd es ≡ ⦃l⦄ LocalOp (λs. { upd ⟨e⟩ s |e. e ∈ es s })"

translations
"⦃l⦄ ´x := e" => "CONST DetLocalOp l «´(_update_name x (λ_. e))»"
"⦃l⦄ ´x :∈ es" => "CONST NonDetAssign l (_update_name x) «es»"

parse_translation ‹
let
fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $(t as Const (@{syntax_const "_antiquote"}, _)$ _)) = skip_antiquote_tr i t
| antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $t) = antiquote_tr i t$ Bound i
| antiquote_tr i (t $u) = antiquote_tr i t$ antiquote_tr i u
| antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
| antiquote_tr _ a = a
and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $t) = c$ skip_antiquote_tr i t
| skip_antiquote_tr i t = antiquote_tr i t;

fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
| quote_tr ts = raise TERM ("quote_tr", ts);
in [(@{syntax_const "_quote"}, K quote_tr)] end
›

subsection‹Process semantics \label{sec:cimp-semantics} ›

text‹

Here we define the semantics of a single process's program. We begin
by defining the type of externally-visible behaviour:

›

datatype ('answer, 'question) seq_label
= sl_Internal ("τ")
| sl_Send 'question 'answer ("«_, _»")

text‹

We define a \emph{labelled transition system} (an LTS) using an
execution-stack style of semantics that avoids special treatment of
the ‹SKIP›s introduced by a traditional small step
semantics (such as @{cite [cite_macro=citet] ‹Chapter~14›
"Winskel:1993"}) when a basic command is executed. This was suggested
by Thomas Sewell; @{cite [cite_macro=citet] "PittsAM:opespe"} gave a
semantics to an ML-like language using this approach.

We record the location of the command that was executed to support
fairness constraints.

›

type_synonym ('answer, 'location, 'question, 'state) local_state
= "('answer, 'location, 'question, 'state) com list × 'location option × 'state"

inductive
small_step :: "('answer, 'location, 'question, 'state) local_state
⇒ ('answer, 'question) seq_label
⇒ ('answer, 'location, 'question, 'state) local_state ⇒ bool" ("_ →⇘_⇙ _" [55, 0, 56] 55)
where
"⟦ α = action s; s' ∈ val β s ⟧ ⟹ (⦃l⦄ Request action val # cs, _, s) →⇘«α, β»⇙ (cs, Some l, s')"
| "(s', β) ∈ action α s ⟹ (⦃l⦄ Response action # cs, _, s) →⇘»α, β«⇙ (cs, Some l, s')"

| "s' ∈ R s ⟹ (⦃l⦄ LocalOp R # cs, _, s) →⇘τ⇙ (cs, Some l, s')"

| "b s ⟹ (⦃l⦄ IF b THEN c FI # cs, _, s) →⇘τ⇙ (c # cs, Some l, s)"
| "¬b s ⟹ (⦃l⦄ IF b THEN c FI # cs, _, s) →⇘τ⇙ (cs, Some l, s)"

| "b s ⟹ (⦃l⦄ IF b THEN c1 ELSE c2 FI # cs, _, s) →⇘τ⇙ (c1 # cs, Some l, s)"
| "¬b s ⟹ (⦃l⦄ IF b THEN c1 ELSE c2 FI # cs, _, s) →⇘τ⇙ (c2 # cs, Some l, s)"

| "(c # LOOP DO c OD # cs, s) →⇘α⇙ (cs', s') ⟹ (LOOP DO c OD # cs, s) →⇘α⇙ (cs', s')"

| "b s ⟹ (⦃l⦄ WHILE b DO c OD # cs, _, s) →⇘τ⇙ (c # ⦃l⦄ WHILE b DO c OD # cs, Some l, s)"
| "¬ b s ⟹ (⦃l⦄ WHILE b DO c OD # cs, _, s) →⇘τ⇙ (cs, Some l, s)"

| "(c1 # c2 # cs, s) →⇘α⇙ (cs', s') ⟹ (c1;; c2 # cs, s) →⇘α⇙ (cs', s')"

| Choose1: "(c1 # cs, s) →⇘α⇙ (cs', s') ⟹ (c1 ⊕ c2 # cs, s) →⇘α⇙ (cs', s')"
| Choose2: "(c2 # cs, s) →⇘α⇙ (cs', s') ⟹ (c1 ⊕ c2 # cs, s) →⇘α⇙ (cs', s')"

text‹

The following projections operate on local states. These should not
appear to the end-user.

›

abbreviation cPGM :: "('answer, 'location, 'question, 'state) local_state ⇒ ('answer, 'location, 'question, 'state) com list" where
"cPGM ≡ fst"

abbreviation cTKN :: "('answer, 'location, 'question, 'state) local_state ⇒ 'location option" where
"cTKN s ≡ fst (snd s)"

abbreviation cLST :: "('answer, 'location, 'question, 'state) local_state ⇒ 'state" where
"cLST s ≡ snd (snd s)"

subsection‹System steps \label{sec:cimp-system-steps}›

text‹

A global state maps process names to process' local states. One might
hope to allow processes to have distinct types of local state, but
there remains no good solution yet in a simply-typed setting; see
@{cite [cite_macro=citet] "DBLP:journals/entcs/SchirmerW09"}.

›

type_synonym ('answer, 'location, 'proc, 'question, 'state) global_state
= "'proc ⇒ ('answer, 'location, 'question, 'state) local_state"

type_synonym ('proc, 'state) local_states
= "'proc ⇒ 'state"

text‹

An execution step of the overall system is either any enabled internal
@{term "τ"} step of any process, or a communication rendezvous between
two processes. For the latter to occur, a @{const "Request"} action
must be enabled in process @{term "p1"}, and a @{const "Response"}
action in (distinct) process @{term "p2"}, where the request/response
labels @{term "α"} and @{term "β"} (semantically) match.

We also track global communication history here to support assertional
reasoning (see \S\ref{sec:cimp-invariants}).

›

type_synonym ('answer, 'question) event = "'question × 'answer"
type_synonym ('answer, 'question) history = "('answer, 'question) event list"

record ('answer, 'location, 'proc, 'question, 'state) system_state =
GST :: "('answer, 'location, 'proc, 'question, 'state) global_state"
HST :: "('answer, 'question) history"

inductive ―‹ This is a predicate of the current state, so the successor state comes first. ›
system_step :: "'proc set
⇒ ('answer, 'location, 'proc, 'question, 'state) system_state
⇒ ('answer, 'location, 'proc, 'question, 'state) system_state
⇒ bool"
where
LocalStep: "⟦ GST sh p →⇘τ⇙ ls'; GST sh' = (GST sh)(p := ls'); HST sh' = HST sh ⟧ ⟹ system_step {p} sh' sh"
| CommunicationStep: "⟦ GST sh p →⇘«α, β»⇙ ls1'; GST sh q →⇘»α, β«⇙ ls2'; p ≠ q;
GST sh' = (GST sh)(p := ls1', q := ls2'); HST sh' = HST sh @ [(α, β)] ⟧ ⟹ system_step {p, q} sh' sh"

text‹

In classical process algebras matching communication actions yield
‹τ› steps, which aids nested parallel composition
and the restriction operation @{cite [cite_macro=citep]
‹\S2.2› "Milner:1980"}. As CIMP does not provide either
we do not need to hide communication labels. In CCS/CSP it is not
clear how one reasons about the communication history, and it seems
that assertional reasoning about these languages is not well
developed.

›

text‹

We define predicates over communication histories and system states. These are uncurried to ease composition.

›

type_synonym ('answer, 'location, 'proc, 'question, 'state) state_pred
= "('answer, 'location, 'proc, 'question, 'state) system_state ⇒ bool"

text‹

The ‹LST› operator (written as a postfix ‹↓›) projects
the local states of the processes from a \<^typ>‹('answer, 'location, 'proc, 'question, 'state) system_state›, i.e. it
discards control location information.

Conversely the ‹LSTP› operator lifts predicates over
local states into predicates over \<^typ>‹('answer, 'location, 'proc, 'question, 'state) system_state›.

Predicates that do not depend on control locations were termed @{emph
‹universal assertions›} by @{cite [cite_macro=citet]
‹\S3.6› "DBLP:journals/acta/LevinG81"}.

›

type_synonym ('proc, 'state) local_state_pred
= "('proc, 'state) local_states ⇒ bool"

definition LST :: "('answer, 'location, 'proc, 'question, 'state) system_state
⇒ ('proc, 'state) local_states" ("_↓" [1000] 1000) where
"s↓ = cLST ∘ GST s"

abbreviation (input) LSTP :: "('proc, 'state) local_state_pred
⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"LSTP P ≡ λs. P s↓"

subsection‹Control predicates \label{sec:cimp-control-predicates}›

text‹

Following @{cite [cite_macro=citet]
"DBLP:journals/acta/Lamport80"}\footnote{@{cite [cite_macro=citet]
"MannaPnueli:1995"} also develop a theory of locations. I think
Lamport attributes control predicates to Owicki in her PhD thesis
(under Gries). I did not find a treatment of procedures. @{cite
[cite_macro=citet] "MannaPnueli:1991"} observe that a notation for
making assertions over sets of locations reduces clutter
significantly.}, we define the ‹at› predicate, which
holds of a process when control resides at that location. Due to
non-determinism processes can be ‹at› a set of locations;
it is more like a statement with this location is enabled'', which
incidentally handles non-unique locations. Lamport's language is
deterministic, so he doesn't have this problem. This also allows him
to develop a stronger theory about his control predicates.

›

type_synonym 'location label = "'location set"

primrec
atC :: "('answer, 'location, 'question, 'state) com ⇒ 'location label"
where
"atC (⦃l⦄ Request action val) = {l}"
| "atC (⦃l⦄ Response action) = {l}"
| "atC (⦃l⦄ LocalOp f) = {l}"
| "atC (⦃l⦄ IF _ THEN _ FI) = {l}"
| "atC (⦃l⦄ IF _ THEN _ ELSE _ FI) = {l}"
| "atC (⦃l⦄ WHILE _ DO _ OD) = {l}"
| "atC (LOOP DO c OD) = atC c"
| "atC (c1;; c2) = atC c1"
| "atC (c1 ⊕ c2) = atC c1 ∪ atC c2"

primrec atCs :: "('answer, 'location, 'question, 'state) com list ⇒ 'location label" where
"atCs [] = {}"
| "atCs (c # _) = atC c"

text‹

We provide the following definitions to the end-user.

‹AT› maps process names to a predicate that is true of
locations where control for that process resides, and the abbreviation ‹at› provides a conventional
way to use it. The constant ‹atS› specifies that control for process ‹p› resides at one of
the given locations. This stands in for, and generalises, the ‹in› predicate of @{cite [cite_macro=citet]
"DBLP:journals/acta/Lamport80"}.

›

definition AT :: "('answer, 'location, 'proc, 'question, 'state) system_state ⇒ 'proc ⇒ 'location label" where
"AT s p = atCs (cPGM (GST s p))"

abbreviation at :: "'proc ⇒ 'location ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"at p l s ≡ l ∈ AT s p"

definition atS :: "'proc ⇒ 'location set ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"atS p ls s = (∃l∈ls. at p l s)"

(* FIXME rename, document, rules. Identifies a process's control state label precisely as one element of a set. *)
definition atLs :: "'proc ⇒ 'location label set ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"atLs p labels s = (AT s p ∈ labels)"

(* FIXME rename, document. Identifies a process's control state label precisely. Relate atL to at/atS, ex/ *)
abbreviation (input) atL :: "'proc ⇒ 'location label ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"atL p label ≡ atLs p {label}"

(* FIXME rename, document. Processes are at the given labels. *)
definition atPLs :: "('proc × 'location label) set ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"atPLs pls = (❙∀p label. ⟨(p, label) ∈ pls⟩ ❙⟶ atL p label)"

text‹

The constant ‹taken› provides a way of identifying which transition was taken. It is somewhat like
Lamport's ‹after›, but not quite due to the presence of non-determinism here. This does not work well
for invariants or preconditions.

›

definition taken :: "'proc ⇒ 'location ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"taken p l s ⟷ cTKN (GST s p) = Some l"

text‹

\label{sec:cimp-termination}

A process is terminated if it not at any control location.

›

abbreviation (input) terminated :: "'proc ⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred" where
"terminated p ≡ atL p {}"

text‹

A complete system consists of one program per process, and a (global)
constraint on their initial local states. From these we can construct
the set of initial global states and all those reachable by system
steps (\S\ref{sec:cimp-system-steps}).

›

type_synonym ('answer, 'location, 'proc, 'question, 'state) programs
= "'proc ⇒ ('answer, 'location, 'question, 'state) com"

record ('answer, 'location, 'proc, 'question, 'state) pre_system =
PGMs :: "('answer, 'location, 'proc, 'question, 'state) programs"
INIT :: "('proc, 'state) local_state_pred"

definition
initial_state :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
⇒ ('answer, 'location, 'proc, 'question, 'state) global_state
⇒ bool"
where
"initial_state sys s = ((∀p. cPGM (s p) = [PGMs sys p] ∧ cTKN (s p) = None) ∧ INIT sys (cLST ∘ s))"

text‹

We construct infinite runs of a system by allowing stuttering, i.e., arbitrary repetitions of states
following @{cite [cite_macro=citet] ‹Chapter~8›"Lamport:2002"}, by taking the reflexive
closure of the @{const system_step} relation. Therefore terminated
programs infinitely repeat their final state (but note our definition
of terminated processes in \S\ref{sec:cimp-termination}).

Some accounts define stuttering as the @{emph ‹finite›} repetition of states. With or without this constraint
‹prerun› contains @{emph ‹junk›} in the form of unfair runs, where particular processes do not progress.

›

definition
system_step_reflclp :: "('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"
where
"system_step_reflclp σ ⟷ (λsh sh'. ∃pls. system_step pls sh' sh)⇧=⇧= (σ 0) (σ 1)"

definition
prerun :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
⇒ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"
where
"prerun sys = ((λσ. initial_state sys (GST (σ 0)) ∧ HST (σ 0) = []) ❙∧ □system_step_reflclp)"

definition ―‹ state-based invariants only ›
prerun_valid :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred ⇒ bool" ("_ ⊨⇘pre⇙ _" [11, 0] 11) (* FIXME priorities *)
where
"(sys ⊨⇘pre⇙ φ) ⟷ (∀σ. prerun sys σ ⟶ (□⌈φ⌉) σ)"

text‹

A ‹run› of a system is a @{const ‹prerun›} that satisfies the ‹FAIR› requirement.
Typically this would include @{emph ‹weak fairness›} for every transition of every process.

›

record ('answer, 'location, 'proc, 'question, 'state) system =
"('answer, 'location, 'proc, 'question, 'state) pre_system"
+ FAIR :: "('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"

definition
run :: "('answer, 'location, 'proc, 'question, 'state) system
⇒ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred"
where
"run sys = (prerun sys ❙∧ FAIR sys)"

definition
valid :: "('answer, 'location, 'proc, 'question, 'state) system
⇒ ('answer, 'location, 'proc, 'question, 'state) system_state seq_pred ⇒ bool" ("_ ⊨ _" [11, 0] 11) (* FIXME priorities *)
where
"(sys ⊨ φ) ⟷ (∀σ. run sys σ ⟶ φ σ)"
(*<*)

end
(*>*)


# Theory CIMP_vcg

(*<*)
(*
* 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‹

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

Our approach follows @{cite [cite_macro=citet]
"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"}
(and the later @{cite [cite_macro=citet] "Lamport:2002"}) and closely
related work by @{cite [cite_macro=citet] "AptFrancezDeRoever:1980"},
@{cite [cite_macro=citet] "CousotCousot:1980"} and @{cite
[cite_macro=citet] "DBLP:journals/acta/LevinG81"}, who suggest the
incorporation of a history variable. @{cite [cite_macro=citet]
"CousotCousot:1980"} apparently contains a completeness proof.
Lamport mentions that this technique was well-known in the mid-80s
when he proposed the use of prophecy variables\footnote{@{url
[cite_macro=citet] "deRoeverEtAl:2001"} for an extended discussion of
some of this.

›

declare small_step.intros[intro]

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

lemma small_step_stuck:
"¬ ([], s) →⇘α⇙ c'"
by (auto elim: small_step.cases)

declare system_step.intros[intro]

text‹

By default we ask the simplifier to rewrite @{const "atS"} using
ambient @{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‹

We 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 ❙∨ atLs p label1) = atLs p (label0 ∪ label1)"
unfolding atLs_def by simp

lemma atLs_insert_disj:
"atLs p (insert l label0) = (atL p l ❙∨ atLs p label0)"
by simp

lemma small_step_terminated:
"s →⇘x⇙ 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 →⇘τ⇙ 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 →⇘«α, β»⇙ ls1'; GST sh p2 →⇘»α, β«⇙ 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 ⊨⇘pre⇙ ⟨True⟩"
unfolding prerun_valid_def by simp

lemma prerun_valid_conjI:
assumes "sys ⊨⇘pre⇙ P"
assumes "sys ⊨⇘pre⇙ Q"
shows "sys ⊨⇘pre⇙ P ❙∧ Q"
using assms unfolding prerun_valid_def always_def by simp

lemma valid_prerun_lift:
assumes "sys ⊨⇘pre⇙ 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⌉ ❙↪ (○⌈I⌉)) σ"
shows "sys ⊨⇘pre⇙ 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 ⊨⇘pre⇙ I"
unfolding prerun_valid_def using assms by (simp add: alwaysI prerun_reachable_state)

lemma prerun_validE:
assumes "reachable_state sys s"
assumes "sys ⊨⇘pre⇙ 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‹

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

Eliding the bodies of ‹IF› and ‹WHILE› statements
yields 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‹

We show that taking system steps preserves fragments.

›

lemma small_step_fragmentsLS:
assumes "s →⇘α⇙ 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‹

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

The representation of evaluation contexts follows @{cite
[cite_macro=citet] "DBLP:journals/jar/Berghofer12"}. This style of
operational semantics was originated by @{cite [cite_macro=citet]
"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‹

We 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) →⇘α⇙ s'"
assumes ds: "(c', ictxt, fctxt) ∈ decompose_com c"
shows "(c # cs, s) →⇘α⇙ 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 →⇘α⇙ s' ⟷ (∃(c, ictxt, fctxt) ∈ decomposeLS s.
cPGM s = ictxt c # tl (cPGM s)
∧ (c # fctxt c @ tl (cPGM s), cTKN s, cLST s) →⇘α⇙ 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‹

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

Decomposing 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) →⇘α⇙ 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‹

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

›

theorem decompose_small_step:
assumes "GST sh p →⇘α⇙ 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)) →⇘α⇙ 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‹

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

›

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

text‹

\label{sec:cimp-vcg}

We do not develop a proper Hoare logic or full VCG for CIMP: this
machinery merely packages up the subgoals that arise from induction
over the reachable states (\S\ref{sec:cimp-invariants}). This is
somewhat in the spirit of @{cite [cite_macro=citet] "Ridge:2009"}.

Note that this approach is not compositional: it consults the original
system to find matching communicating pairs, and ‹aft›
tracks the labels of possible successor statements. More serious Hoare
logics are provided by @{cite [cite_macro=citet]
"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"
and "CousotCousot89-IC"}.

Intuitively we need to discharge a proof obligation for either @{const
"Request"}s or @{const "Response"}s but not both. Here we choose to
focus on @{const "Request"}s as we expect to have more local
information 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‹

We 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‹

We tweak @{const "fragments"} by omitting @{const "Response"}s,
yielding 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‹

The 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⌉ ❙↪ ○⌈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 ⊨⇘pre⇙ 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
(*>*)


# Theory CIMP_vcg_rules

(*<*)
(*
* 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_rules
imports
CIMP_vcg
begin

(*>*)
subsubsection‹ VCG rules \label{sec:cimp:vcg_rules} ›

text‹

We can develop some (but not all) of the familiar Hoare rules; see
@{cite [cite_macro=citet] "DBLP:journals/acta/Lamport80"} and the
seL4/l4.verified lemma buckets for inspiration. We avoid many of the
issues Lamport mentions as we only treat basic (atomic) commands.

›

context
fixes coms :: "('answer, 'location, 'proc, 'question, 'state) programs"
fixes p :: "'proc"
fixes aft :: "('answer, 'location, 'question, 'state) loc_comp"
begin

abbreviation
valid_syn :: "('answer, 'location, 'proc, 'question, 'state) state_pred
⇒ ('answer, 'location, 'question, 'state) com
⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred ⇒ bool" where
"valid_syn P c Q ≡ coms, p, aft ⊢ ⦃P⦄ c ⦃Q⦄"
notation valid_syn ("⦃_⦄/ _/ ⦃_⦄")

abbreviation
valid_inv_syn :: "('answer, 'location, 'proc, 'question, 'state) state_pred
⇒ ('answer, 'location, 'question, 'state) com ⇒ bool" where
"valid_inv_syn P c ≡ ⦃P⦄ c ⦃P⦄"
notation valid_inv_syn ("⦃_⦄/ _")

lemma vcg_True:
"⦃P⦄ c ⦃⟨True⟩⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_conj:
"⟦ ⦃I⦄ c ⦃Q⦄; ⦃I⦄ c ⦃R⦄ ⟧ ⟹ ⦃I⦄ c ⦃Q ❙∧ R⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_pre_imp:
"⟦ ⋀s. P s ⟹ Q s; ⦃Q⦄ c ⦃R⦄ ⟧ ⟹ ⦃P⦄ c ⦃R⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemmas vcg_pre = vcg_pre_imp[rotated]

lemma vcg_post_imp:
"⟦ ⋀s. Q s ⟹ R s; ⦃P⦄ c ⦃Q⦄ ⟧ ⟹ ⦃P⦄ c ⦃R⦄"
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_prop[intro]:
"⦃⟨P⟩⦄ c"
by (cases c) (fastforce intro: vcg.intros)+

lemma vcg_drop_imp:
assumes "⦃P⦄ c ⦃Q⦄"
shows "⦃P⦄ c ⦃R ❙⟶ Q⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_conj_lift:
assumes x: "⦃P⦄ c ⦃Q⦄"
assumes y: "⦃P'⦄ c ⦃Q'⦄"
shows      "⦃P ❙∧ P'⦄ c ⦃Q ❙∧ Q'⦄"
apply (rule vcg_conj)
apply (rule vcg_pre[OF x], simp)
apply (rule vcg_pre[OF y], simp)
done

lemma vcg_disj_lift:
assumes x: "⦃P⦄  c ⦃Q⦄"
assumes y: "⦃P'⦄ c ⦃Q'⦄"
shows      "⦃P ❙∨ P'⦄ c ⦃Q ❙∨ Q'⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_imp_lift:
assumes "⦃P'⦄ c ⦃❙¬ P⦄"
assumes "⦃Q'⦄ c ⦃Q⦄"
shows "⦃P' ❙∨ Q'⦄ c ⦃P ❙⟶ Q⦄"
by (simp only: imp_conv_disj vcg_disj_lift[OF assms])

lemma vcg_ex_lift:
assumes "⋀x. ⦃P x⦄ c ⦃Q x⦄"
shows "⦃λs. ∃x. P x s⦄ c ⦃λs. ∃x. Q x s⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_all_lift:
assumes "⋀x. ⦃P x⦄ c ⦃Q x⦄"
shows "⦃λs. ∀x. P x s⦄ c ⦃λs. ∀x. Q x s⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_name_pre_state:
assumes "⋀s. P s ⟹ ⦃(=) s⦄ c ⦃Q⦄"
shows "⦃P⦄ c ⦃Q⦄"
using assms
by (cases c) (fastforce elim!: vcg_inv intro: vcg.intros)+

lemma vcg_lift_comp:
assumes f: "⋀P. ⦃λs. P (f s :: 'a :: type)⦄ c"
assumes P: "⋀x. ⦃Q x⦄ c ⦃P x⦄"
shows "⦃λs. Q (f s) s⦄ c ⦃λs. P (f s) s⦄"
apply (rule vcg_name_pre_state)
apply (rename_tac s)
apply (rule vcg_pre)
apply (rule vcg_post_imp[rotated])
apply (rule vcg_conj_lift)
apply (rule_tac x="f s" in P)
apply (rule_tac P="λfs. fs = f s" in f)
apply simp
apply simp
done

subsubsection‹Cheap non-interference rules›

text‹

These rules magically construct VCG lifting rules from the easier to
prove ‹eq_imp› facts. We don't actually use these in the GC,
but we do derive @{const "fun_upd"} equations using the same
mechanism. Thanks to Thomas Sewell for the requisite syntax magic.

As these ‹eq_imp› facts do not usefully compose, we make the
definition asymmetric (i.e., ‹g› does not get a bundle of
parameters).

Note that these are effectively parametricity rules.

›

definition eq_imp :: "('a ⇒ 'b ⇒ 'c) ⇒ ('b ⇒ 'e) ⇒ bool" where
"eq_imp f g ≡ (∀s s'. (∀x. f x s = f x s') ⟶ (g s = g s'))"

lemma eq_impD:
"⟦ eq_imp f g; ∀x. f x s = f x s' ⟧ ⟹ g s = g s'"
by (simp add: eq_imp_def)

lemma eq_imp_vcg:
assumes g: "eq_imp f g"
assumes f: "∀x P. ⦃P ∘ (f x)⦄ c"
shows "⦃P ∘ g⦄ c"
apply (rule vcg_name_pre_state)
apply (rename_tac s)
apply (rule vcg_pre)
apply (rule vcg_post_imp[rotated])
apply (rule vcg_all_lift[where 'a='a])
apply (rule_tac x=x and P="λfs. fs = f x s" in f[rule_format])
apply simp
apply (frule eq_impD[where f=f, OF g])
apply simp
apply simp
done

lemma eq_imp_vcg_LST:
assumes g: "eq_imp f g"
assumes f: "∀x P. ⦃P ∘ (f x) ∘ LST⦄ c"
shows "⦃P ∘ g ∘ LST⦄ c"
apply (rule vcg_name_pre_state)
apply (rename_tac s)
apply (rule vcg_pre)
apply (rule vcg_post_imp[rotated])
apply (rule vcg_all_lift[where 'a='a])
apply (rule_tac x=x and P="λfs. fs = f x s↓" in f[rule_format])
apply simp
apply (frule eq_impD[where f=f, OF g])
apply simp
apply simp
done

lemma eq_imp_fun_upd:
assumes g: "eq_imp f g"
assumes f: "∀x. f x (s(fld := val)) = f x s"
shows "g (s(fld := val)) = g s"
apply (rule eq_impD[OF g])
apply (rule f)
done

lemma curry_forall_eq:
"(∀f. P f) = (∀f. P (case_prod f))"
by (metis case_prod_curry)

lemma pres_tuple_vcg:
"(∀P. ⦃P ∘ (λs. (f s, g s))⦄ c)
⟷ ((∀P. ⦃P ∘ f⦄ c) ∧ (∀P. ⦃P ∘ g⦄ c))"
apply (simp add: curry_forall_eq o_def)
apply safe
apply fast
apply fast
apply (rename_tac P)
apply (rule_tac f="f" and P="λfs s. P fs (g s)" in vcg_lift_comp; simp)
done

lemma pres_tuple_vcg_LST:
"(∀P. ⦃P ∘ (λs. (f s, g s)) ∘ LST⦄ c)
⟷ ((∀P. ⦃P ∘ f ∘ LST⦄ c) ∧ (∀P. ⦃P ∘ g ∘ LST⦄ c))"
apply (simp add: curry_forall_eq o_def)
apply safe
apply fast
apply fast
apply (rename_tac P)
apply (rule_tac f="λs. f s↓" and P="λfs s. P fs (g s)" for g in vcg_lift_comp; simp)
done

no_notation valid_syn ("⦃_⦄/ _/ ⦃_⦄")

end

(*<*)

end
(*>*)


# Theory CIMP

(*<*)
(*
* 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
imports
CIMP_pred
CIMP_lang
CIMP_vcg
CIMP_vcg_rules
keywords
"locset_definition" :: thy_defn
and "intern_com" :: thy_decl
begin

text‹

Infrastructure for reasoning about CIMP programs. See AFP entry ‹ConcurrentGC› for examples
of use.

›

named_theorems locset_cache "Location set membership cache"

lemmas cleanup_simps =
atomize_eq
simp_thms

ML_file‹cimp.ML›
(*<*)

end
(*>*)


# File ‹cimp.ML›

(* Pollutes the global namespace, but we use them everywhere *)
fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
fun HOL_ss_only thms ctxt = clear_simpset (put_simpset HOL_ss ctxt) addsimps thms;

signature CIMP =
sig
val com_locs_fold : (term * 'b -> 'b) -> 'b -> term -> 'b
val com_locs_map : (term -> 'b) -> term -> 'b list
val com_locs_fold_no_response : (term * 'b -> 'b) -> 'b -> term -> 'b
val com_locs_map_no_response : (term -> 'b) -> term -> 'b list
val intern_com : Facts.ref -> local_theory -> local_theory
val def_locset : thm -> local_theory -> local_theory
end;

structure Cimp : CIMP =
struct

fun com_locs_fold f x (Const (@{const_name Request}, _) $l$ _ $_ ) = f (l, x) | com_locs_fold f x (Const (@{const_name Response}, _)$ l $_) = f (l, x) | com_locs_fold f x (Const (@{const_name LocalOp}, _)$ l $_) = f (l, x) | com_locs_fold f x (Const (@{const_name Cond1}, _)$ l $_$ c)       = com_locs_fold f (f (l, x)) c
| com_locs_fold f x (Const (@{const_name Cond2}, _) $l$ _ $c1$ c2) = com_locs_fold f (com_locs_fold f (f (l, x)) c1) c2
| com_locs_fold f x (Const (@{const_name Loop}, _) $c) = com_locs_fold f x c | com_locs_fold f x (Const (@{const_name While}, _)$ l $_$ c)       = com_locs_fold f (f (l, x)) c
| com_locs_fold f x (Const (@{const_name Seq}, _) $c1$ c2)           = com_locs_fold f (com_locs_fold f x c1) c2
| com_locs_fold f x (Const (@{const_name Choose}, _) $c1$ c2)        = com_locs_fold f (com_locs_fold f x c1) c2
| com_locs_fold _ x _ = x;

fun com_locs_map f com = com_locs_fold (fn (l, acc) => f l :: acc) [] com

fun com_locs_fold_no_response f x (Const (@{const_name Request}, _) $l$ _ $_ ) = f (l, x) | com_locs_fold_no_response _ x (Const (@{const_name Response}, _)$ _ $_) = x (* can often ignore ‹Response› *) | com_locs_fold_no_response f x (Const (@{const_name LocalOp}, _)$ l $_) = f (l, x) | com_locs_fold_no_response f x (Const (@{const_name Cond1}, _)$ l $_$ c)       = com_locs_fold_no_response f (f (l, x)) c
| com_locs_fold_no_response f x (Const (@{const_name Cond2}, _) $l$ _ $c1$ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f (f (l, x)) c1) c2
| com_locs_fold_no_response f x (Const (@{const_name Loop}, _) $c) = com_locs_fold_no_response f x c | com_locs_fold_no_response f x (Const (@{const_name While}, _)$ l $_$ c)       = com_locs_fold_no_response f (f (l, x)) c
| com_locs_fold_no_response f x (Const (@{const_name Seq}, _) $c1$ c2)           = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2
| com_locs_fold_no_response f x (Const (@{const_name Choose}, _) $c1$ c2)        = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2
| com_locs_fold_no_response _ x _ = x;

fun com_locs_map_no_response f com = com_locs_fold_no_response (fn (l, acc) => f l :: acc) [] com

fun cprop_of_equality ctxt : thm -> cterm =
Local_Defs.meta_rewrite_rule ctxt (* handle = or ≡ *)
#> Thm.cprop_of

fun equality_lhs ctxt : thm -> term =
cprop_of_equality ctxt #> Thm.dest_equals_lhs #> Thm.term_of

fun equality_rhs ctxt : thm -> term =
cprop_of_equality ctxt #> Thm.dest_equals_rhs #> Thm.term_of

(* Intern all labels mentioned in CIMP programs ‹facts›

FIXME can only use ‹com_intern› once per locale
FIXME forces all labels to be unique and distinct from other constants in the locale.
FIXME assumes the labels are character strings
*)
fun intern_com facts ctxt : local_theory =
let
val thms = Proof_Context.get_fact ctxt facts
(* Define constants with defs of the form loc.XXX_def: "XXX ≡ ''XXX''. *)
val attrs = []
fun add_literal_def (literal, (loc_defs, ctxt)) : thm list * local_theory =
let
val literal_name = HOLogic.dest_string literal (* FIXME might not be a nice name, but the error is readable so shrug. FIXME generalise to other label types *)
val literal_def_binding = Binding.empty (* Binding.qualify true "loc" (Binding.name (Thm.def_name literal_name)) No need to name individual defs *)
val ((_, (_, loc_def)), ctxt) = Local_Theory.define ((Binding.name literal_name, Mixfix.NoSyn), ((literal_def_binding, attrs), literal)) ctxt
in
(loc_def :: loc_defs, ctxt)
end;
val (loc_defs, ctxt) = List.foldl (fn (com, acc) => com_locs_fold add_literal_def acc (equality_rhs ctxt com)) ([], ctxt) thms

val coms_interned = List.map (Local_Defs.fold ctxt loc_defs) thms
val attrs = []
val (_, ctxt) = Local_Theory.note ((@{binding "loc_defs"}, attrs), loc_defs) ctxt
val (_, ctxt) = Local_Theory.note ((@{binding "com_interned"}, attrs), coms_interned) ctxt
in
ctxt
end;

(* Cache location set membership facts.

Decide membership in the given set for each label in the CIMP programs
in the Named_Theorems "com".

If the label set and com types differ, we probably get a nasty error.

*)

fun def_locset thm ctxt =
let
val set_name = equality_lhs ctxt thm
val set_name_str = case set_name of Const (c, _) => c | Free (c, _) => c | _ => error ("Not an equation of the form x = set: " ^ Thm.string_of_thm ctxt thm)
val memb_thm_name = Binding.qualify true set_name_str (Binding.name "memb")
fun mk_memb l = Thm.cterm_of ctxt (HOLogic.mk_mem (l, set_name))
(*
1. solve atomic membership yielding ‹''label'' ∈ set› or ‹''label'' ∉ set›.
2. fold ‹loc_defs›
3. cleanup with the existing ‹locset_cache›.
FIXME trim simpsets: 1: sets 2: not much 3: not much
*)
val loc_defs = Proof_Context.get_fact ctxt (Facts.named "loc_defs")
val membership_ctxt = ctxt addsimps ([thm] @ loc_defs)
val cleanup_ctxt = HOL_ss_only (@{thms cleanup_simps} @ Named_Theorems.get ctxt \<^named_theorems>‹locset_cache›) ctxt
val rewrite_tac =
Simplifier.rewrite membership_ctxt
#> Local_Defs.fold ctxt loc_defs
#> Simplifier.simplify cleanup_ctxt
val coms = Proof_Context.get_fact ctxt (Facts.named "com_interned")
(* Parallel *)
fun mk_thms coms : thm list = Par_List.map rewrite_tac (maps (equality_rhs ctxt #> com_locs_map_no_response mk_memb) coms)
(* Sequential *)
(*    fun mk_thms coms = List.foldl (fn (c, thms) => com_locs_fold (fn l => fn thms => rewrite_tac (mk_memb l) :: thms) thms c) [] coms *)
val attrs = []
val (_, ctxt) = ctxt |> Local_Theory.note ((memb_thm_name, attrs), mk_thms coms)
(* Add ‹memb_thms› to the global (and inherited by locales) ‹locset_cache› *)
val memb_thm_full_name = Local_Theory.full_name ctxt memb_thm_name
val (finish, ctxt) = Target_Context.switch_named_cmd (SOME ("-", Position.none)) (Context.Proof ctxt) (* switch to the "root" local theory *)
val memb_thms = Proof_Context.get_fact ctxt (Facts.named memb_thm_full_name)
val attrs = [Attrib.internal (K (Named_Theorems.add \<^named_theorems>‹locset_cache›))]
val (_, ctxt) = ctxt |> Local_Theory.note ((Binding.empty, attrs), memb_thms)
val ctxt = case finish ctxt of Context.Proof ctxt => ctxt | _ => error "Context.generic failure" (* Return to the locale we were in *)
in
ctxt
end;

end;

val _ =
Outer_Syntax.local_theory \<^command_keyword>‹intern_com› "intern labels in CIMP commands"
(Parse.thms1 >> (fn facts => fn ctxt => List.foldl (fn ((f, _), ctxt) => Cimp.intern_com f ctxt) ctxt facts));

val _ =
Outer_Syntax.local_theory' \<^command_keyword>‹locset_definition› "constant definition for sets of locations"
(Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => fn b => fn lthy =>
Specification.definition_cmd decl params prems spec b lthy
|> (fn ((_, (_, thm)), lthy) => (thm, lthy)) |> uncurry Cimp.def_locset));


# Theory CIMP_locales

(*<*)
theory CIMP_locales
imports
"../CIMP"
begin

(*>*)
section‹ One locale per process ›

text‹

A sketch of what we're doing in ‹ConcurrentGC›, for quicker testing.

FIXME write some lemmas that further exercise the generated thms.

›

locale P1
begin

definition com :: "(unit, string, unit, nat) com" where
"com = ⦃''A''⦄ WHILE ((<) 0) DO ⦃''B''⦄ ⌊λs. s - 1⌋ OD"

intern_com com_def
print_theorems (* P1.com_interned, P1.loc_defs *)

locset_definition "loop = {B}"
print_theorems (* P1.loop.memb, P1.loop_def *)
thm locset_cache (* the two facts in P1.loop.memb *)

definition "assertion = atS False loop"

end

thm locset_cache (* the two facts in P1.loop.memb *)

locale P2
begin

thm locset_cache (* the two facts in P1.loop.memb *)

definition com :: "(unit, string, unit, nat) com" where
"com = ⦃''C''⦄ WHILE ((<) 0) DO ⦃''A''⦄ ⌊Suc⌋ OD"

intern_com com_def
locset_definition "loop = {A}"
print_theorems

end

thm locset_cache (* four facts: P1.loop.memb, P2.loop.memb *)

primrec coms :: "bool ⇒ (unit, string, unit, nat) com" where
"coms False = P1.com"
| "coms True = P2.com"

(*<*)

end
(*>*)


# Theory CIMP_one_place_buffer

(*<*)
(*
* 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_one_place_buffer
imports
"../CIMP"
begin

(*>*)
section‹Example: a one-place buffer \label{sec:one_place_buffer}›

text‹

To demonstrate the CIMP reasoning infrastructure, we treat the trivial
one-place buffer example of @{cite [cite_macro=citet]
‹\S3.3› "DBLP:journals/toplas/LamportS84"}. Note that the
semantics for our language is different to @{cite
[cite_macro=citeauthor] "DBLP:journals/toplas/LamportS84"}'s, who
treated a historical variant of CSP (i.e., not the one in @{cite
"Hoare:1985"}).

We introduce some syntax for fixed-topology (static channel-based)
scenarios.

›

abbreviation
rcv_syn :: "'location ⇒ 'channel ⇒ ('val ⇒ 'state ⇒ 'state)
⇒ (unit, 'location, 'channel × 'val, 'state) com" ("⦃_⦄/ _▹_" [0,0,81] 81)
where
"⦃l⦄ ch▹f ≡ ⦃l⦄ Response (λq s. if fst q = ch then {(f (snd q) s, ())} else {})"

abbreviation
snd_syn :: "'location ⇒ 'channel ⇒ ('state ⇒ 'val)
⇒ (unit, 'location, 'channel × 'val, 'state) com" ("⦃_⦄/ _◃_" [0,0,81] 81)
where
"⦃l⦄ ch◃f ≡ ⦃l⦄ Request (λs. (ch, f s)) (λans s. {s})"

text‹

These definitions largely follow @{cite [cite_macro=citet]
"DBLP:journals/toplas/LamportS84"}. We have three processes
communicating over two channels. We enumerate program locations.

›

datatype ex_chname = ξ12 | ξ23
type_synonym ex_val = nat
type_synonym ex_ch = "ex_chname × ex_val"
datatype ex_loc = r12 | r23 | s23 | s12
datatype ex_proc = p1 | p2 | p3

type_synonym ex_pgm = "(unit, ex_loc, ex_ch, ex_val) com"
type_synonym ex_pred = "(unit, ex_loc, ex_proc, ex_ch, ex_val) state_pred"
type_synonym ex_state = "(unit, ex_loc, ex_proc, ex_ch, ex_val) system_state"
type_synonym ex_sys = "(unit, ex_loc, ex_proc, ex_ch, ex_val) system"
type_synonym ex_history = "(ex_ch × unit) list"

text‹

We further specialise these for our particular example.

›

primrec
ex_coms :: "ex_proc ⇒ ex_pgm"
where
"ex_coms p1 = ⦃s12⦄ ξ12◃id"
| "ex_coms p2 = LOOP DO ⦃r12⦄ ξ12▹(λv _. v) ;; ⦃s23⦄ ξ23◃id OD"
| "ex_coms p3 = ⦃r23⦄ ξ23▹(λv _. v)"

text‹

Each process starts with an arbitrary initial local state.

›

abbreviation ex_init :: "(ex_proc ⇒ ex_val) ⇒ bool" where
"ex_init ≡ ⟨True⟩"

abbreviation sys :: ex_sys where
"sys ≡ ⦇PGMs = ex_coms, INIT = ex_init, FAIR = ⟨True⟩⦈" (* FIXME add fairness hypotheses *)

text‹

The following adapts Kai Engelhardt's, from his notes titled
\emph{Proving an Asynchronous Message Passing Program Correct},
2011. The history variable tracks the causality of the system, which I
feel is missing in Lamport's treatment. We tack on Lamport's invariant
so we can establish ‹Etern_pred›.

›

abbreviation
filter_on_channel :: "ex_chname ⇒ ex_state ⇒ ex_val list" ("⇂_" [100] 101)
where
"⇂ch ≡ map (snd ∘ fst) ∘ filter ((=) ch ∘ fst ∘ fst) ∘ HST"

definition IL :: ex_pred where
"IL = pred_conjoin [
at p1 s12 ❙⟶ LIST_NULL ⇂ξ12
, terminated p1 ❙⟶ ⇂ξ12 ❙= (λs. [s↓ p1])
, at p2 r12 ❙⟶ ⇂ξ12 ❙= ⇂ξ23
, at p2 s23 ❙⟶ ⇂ξ12 ❙= ⇂ξ23 ❙@ (λs. [s↓ p2]) ❙∧ (λs. s↓ p1 = s↓ p2)
, at p3 r23 ❙⟶ LIST_NULL ⇂ξ23
, terminated p3 ❙⟶ ⇂ξ23 ❙= (λs. [s↓ p2]) ❙∧ (λs. s↓ p1 = s↓ p3)
]"

text‹

If @{const p3} terminates, then it has @{const p1}'s value. This is
stronger than @{cite [cite_macro=citeauthor]
"DBLP:journals/toplas/LamportS84"}'s as we don't ask that the first
process has also terminated.

›

definition Etern_pred :: ex_pred where
"Etern_pred = (terminated p3 ❙⟶ (λs. s↓ p1 = s↓ p3))"

text‹

Proofs from here down.

›

lemma correct_system:
assumes "IL sh"
shows "Etern_pred sh"
using assms unfolding Etern_pred_def IL_def by simp

lemma IL_p1: "ex_coms, p1, lconst {} ⊢ ⦃IL⦄ ⦃s12⦄ ξ12◃(λs. s)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp simp: IL_def atLs_def)
done

lemma IL_p2: "ex_coms, p2, lconst {r12} ⊢ ⦃IL⦄ ⦃s23⦄ ξ23◃(λs. s)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp simp: IL_def)
done

lemma IL: "sys ⊨⇘pre⇙ IL"
apply (rule VCG)
apply (clarsimp simp: IL_def atLs_def dest!: initial_stateD)
apply (rename_tac p)
apply (case_tac p; clarsimp simp: IL_p1 IL_p2)
done

lemma IL_valid: "sys ⊨ □⌈IL⌉"
by (rule valid_prerun_lift[OF IL])

(*<*)

end
(*>*)


# Theory CIMP_unbounded_buffer

(*<*)
(*
* 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_unbounded_buffer
imports
"../CIMP"
"HOL-Library.Prefix_Order"
begin

abbreviation (input)
Receive :: "'location ⇒ 'channel ⇒ ('val ⇒ 'state ⇒ 'state)
⇒ (unit, 'location, 'channel × 'val, 'state) com" ("⦃_⦄/ _▹_" [0,0,81] 81)
where
"⦃l⦄ ch▹f ≡ ⦃l⦄ Response (λq s. if fst q = ch then {(f (snd q) s, ())} else {})"

abbreviation (input)
Send :: "'location ⇒ 'channel ⇒ ('state ⇒ 'val) × ('state ⇒ 'state)
⇒ (unit, 'location, 'channel × 'val, 'state) com" ("⦃_⦄/ _◃_" [0,0,81] 81)
where
"⦃l⦄ ch◃f ≡ ⦃l⦄ Request (λs. (ch, fst f s)) (λans s. {snd f s})"

(*>*)
section‹Example: an unbounded buffer \label{sec:unbounded_buffer}›

text‹

This is more literally Kai Engelhardt's example from his notes titled
\emph{Proving an Asynchronous Message Passing Program Correct}, 2011.

›

datatype ex_chname = ξ12 | ξ23
type_synonym ex_val = nat
type_synonym ex_ls = "ex_val list"
type_synonym ex_ch = "ex_chname × ex_val"
datatype ex_loc = c1 | r12 | r23 | s23 | s12
datatype ex_proc = p1 | p2 | p3

type_synonym ex_pgm = "(unit, ex_loc, ex_ch, ex_ls) com"
type_synonym ex_pred = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) state_pred"
type_synonym ex_state = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) system_state"
type_synonym ex_sys = "(unit, ex_loc, ex_proc, ex_ch, ex_ls) system"
type_synonym ex_history = "(ex_ch × unit) list"

text‹

The local state for the producer process contains all values produced; consider that ghost state.

›

abbreviation (input) snoc :: "'a ⇒ 'a list ⇒ 'a list" where "snoc x xs ≡ xs @ [x]"

primrec ex_coms :: "ex_proc ⇒ ex_pgm" where
"ex_coms p1 = LOOP DO ⦃c1⦄ LocalOp (λxs. {snoc x xs |x. True}) ;; ⦃s12⦄ ξ12◃(last, id) OD"
| "ex_coms p2 = LOOP DO ⦃r12⦄ ξ12▹snoc
⊕ ⦃c1⦄ IF (λs. length s > 0) THEN ⦃s23⦄ ξ12◃(hd, tl) FI
OD"
| "ex_coms p3 = LOOP DO ⦃r23⦄ ξ23▹snoc OD"

abbreviation ex_init :: "(ex_proc ⇒ ex_ls) ⇒ bool" where
"ex_init s ≡ ∀p. s p = []"

abbreviation sys :: ex_sys where
"sys ≡ ⦇PGMs = ex_coms, INIT = ex_init, FAIR = ⟨True⟩⦈" (* FIXME add fairness hypotheses *)

abbreviation
filter_on_channel :: "ex_chname ⇒ ex_state ⇒ ex_val list" ("⇂_" [100] 101)
where
"⇂ch ≡ map (snd ∘ fst) ∘ filter ((=) ch ∘ fst ∘ fst) ∘ HST"

definition I_pred :: ex_pred where
"I_pred = pred_conjoin [
at p1 c1 ❙⟶ ⇂ξ12 ❙= (λs. s↓ p1)
, at p1 s12 ❙⟶ (λs. length (s↓ p1) > 0 ∧ butlast (s↓ p1) = (⇂ξ12) s)
, ⇂ξ12 ❙≤ (λs. s↓ p1)
, ⇂ξ12 ❙= ⇂ξ23 ❙@ (λs. s↓ p2)
, at p2 s23 ❙⟶ (λs. length (s↓ p2) > 0)
, (λs. s↓ p3) ❙= ⇂ξ23
]"

text‹

The local state of @{const "p3"} is some prefix of the local state of
@{const "p1"}.

›

definition Etern_pred :: ex_pred where
"Etern_pred ≡ λs. s↓ p3 ≤ s↓ p1"

lemma correct_system:
assumes "I_pred s"
shows "Etern_pred s"
using assms unfolding Etern_pred_def I_pred_def less_eq_list_def prefix_def by clarsimp

lemma p1_c1[simplified, intro]:
"ex_coms, p1, lconst {s12} ⊢ ⦃I_pred⦄ ⦃c1⦄ LocalOp (λxs. { snoc x xs |x. True })"
apply (rule vcg.intros)
apply (clarsimp simp: I_pred_def atS_def)
done

lemma p1_s12[simplified, intro]:
"ex_coms, p1, lconst {c1} ⊢ ⦃I_pred⦄ ⦃s12⦄ ξ12◃(last, id)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp)
apply (clarsimp simp: I_pred_def atS_def)
apply (metis Prefix_Order.prefix_snoc append.assoc append_butlast_last_id)
done

lemma p2_s23[simplified, intro]:
"ex_coms, p2, lconst {c1, r12} ⊢ ⦃I_pred⦄ ⦃s23⦄ ξ12◃(hd, tl)"
apply (rule vcg.intros)
apply (rename_tac p')
apply (case_tac p'; clarsimp)
done

lemma p2_pi4[intro]:
"ex_coms, p2, lcond {s23} {c1, r12} (λs. s ≠ []) ⊢ ⦃I_pred⦄ ⦃c1⦄ IF (λs. s ≠ []) THEN c' FI"
apply (rule vcg.intros)
apply (clarsimp simp: I_pred_def atS_def split: lcond_splits)
done

lemma I: "sys ⊨⇘pre⇙ I_pred"
apply (rule VCG)
apply (clarsimp dest!: initial_stateD simp: I_pred_def atS_def)
apply (rename_tac p)
apply (case_tac p; auto)
done

lemma I_valid: "sys ⊨ □⌈I_pred⌉"
by (rule valid_prerun_lift[OF I])

(*<*)

end
(*>*)
`