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)"
unfolding suffix_def by (simp add: add.assoc)

lemma suffix_commute: "((σ |⇩s n) |⇩s m) = ((σ |⇩s m) |⇩s n)"
by (simp add: suffix_plus add.commute)

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

lemma stake_add[simp]:
  "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
\<^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, opaque_lifting) 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
by (metis safety_always_eventually add_diff_cancel_right' diff_le_self le_add_same_cancel2)

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