Safety, liveness and refinement of simple TLA+ clock specifications in Isabelle/HOL

Clock.thy

theory Clock
  imports "HOL-TLA.TLA"
begin

lemma imp_imp_leadsto:
  fixes F G :: stpred
  fixes S :: temporal
  assumes "⊢ F ⟶ G"
  shows "⊢ S ⟶ (F ↝ G)"
  apply (auto simp add: Valid_def)
  using ImplLeadsto_simple assms by blast

lemma imp_leadsto_transitive[trans]:
  fixes F G H :: stpred
  fixes S :: temporal
  assumes "⊢ S ⟶ (F ↝ G)"
  assumes "⊢ S ⟶ (G ↝ H)"
  shows "⊢ S ⟶ (F ↝ H)"
  using assms
  apply (auto simp add: Valid_def)
  using LatticeTransitivity by fastforce

lemma temp_impI:
  assumes "sigma ⊨ P ⟹ sigma ⊨ Q"
  shows "sigma ⊨ P ⟶ Q"
  using assms by auto

lemma temp_conjI:
  assumes "sigma ⊨ P" "sigma ⊨ Q"
  shows "sigma ⊨ P ∧ Q"
  using assms by auto

lemma temp_conjE:
  assumes "sigma ⊨ F ∧ G"
  assumes  "⟦ sigma ⊨ F; sigma ⊨ G ⟧ ⟹ P"
  shows "P"
  using assms by auto

lemma temp_imp_conjI:
  assumes "⊢ S ⟶ P" "⊢ S ⟶ Q"
  shows "⊢ S ⟶ P ∧ Q"
  using assms unfolding Valid_def
  by auto

lemma temp_box_conjE:
  assumes "sigma ⊨ □(F ∧ G)"
  assumes  "⟦ sigma ⊨ □F; sigma ⊨ □G ⟧ ⟹ P"
  shows "P"
  using assms STL5 unfolding Valid_def
  by (simp add: split_box_conj)

lemma temp_imp_trans [trans]:
  assumes "⊢ F ⟶ G"
  assumes "⊢ G ⟶ H"
  shows "⊢ F ⟶ H"
  using assms unfolding Valid_def by auto

lemma imp_leadsto_invariant:
  fixes S :: temporal
  fixes P I :: stpred
  assumes "⊢ S ⟶ □I"
  shows "⊢ S ⟶ (P ↝ I)"
proof (intro tempI temp_impI)
  fix sigma
  assume S: "sigma ⊨ S"
  with assms have "sigma ⊨ □I" by auto
  thus "sigma ⊨ P ↝ I"
    unfolding leadsto_def
    by (metis InitDmd STL4E boxInit_stp dmdInit_stp intI temp_impI)
qed

lemma imp_forall_leadsto:
  fixes S :: temporal
  fixes P :: "'a ⇒ bool"
  fixes Q :: "'a ⇒ stpred"
  fixes R :: stpred
  assumes "⋀x. P x ⟹ ⊢ S ⟶ (Q x ↝ R)"
  shows "⊢ S ⟶ (∀ x. (#(P x) ∧ Q x) ↝ R)"
  using assms
  unfolding Valid_def leadsto_def
  apply auto
  by (metis (full_types) ImplLeadsto_simple TrueW int_simps(11) int_simps(17) int_simps(19) inteq_reflection leadsto_def tempD)

lemma temp_dmd_box_imp: 
  assumes "sigma ⊨ ◇□ P"
  assumes "⊢ P ⟶ Q"
  shows "sigma ⊨ ◇□ Q"
  using assms DmdImplE STL4 by blast

lemma temp_box_dmd_imp: 
  assumes "sigma ⊨ □◇ P"
  assumes "⊢ P ⟶ Q"
  shows "sigma ⊨ □◇ Q"
  using assms DmdImpl STL4E by blast

lemma not_stuck_forever:
  fixes Stuck :: stpred
  fixes Progress :: action
  assumes "⊢ Progress ⟶ $Stuck ⟶ ¬ Stuck$"
  shows "⊢ □◇Progress ⟶ ¬ ◇□Stuck"
  using assms
  by (unfold dmd_def, simp, intro STL4, simp, intro TLA2, auto)

lemma stable_dmd_stuck:
  assumes "⊢ S ⟶ stable P"
  assumes "⊢ S ⟶ ◇P"
  shows "⊢ S ⟶ ◇□P"
  using assms DmdStable by (meson temp_imp_conjI temp_imp_trans)

lemma enabled_before_conj[simp]:
  "PRED Enabled ($P ∧ Q) = (PRED (P ∧ Enabled Q))"
  unfolding enabled_def by (intro ext, auto)

definition next_hour :: "nat ⇒ nat" where "⋀n. next_hour n ≡ if n = 12 then 1 else n+1"

lemma next_hour_induct [case_names base step, consumes 1]:
  fixes m :: nat
  assumes type: "m ∈ {1..12}"
  assumes base: "P 1"
  assumes step: "⋀n. 1 ≤ n ⟹ n < 12 ⟹ P n ⟹ P (next_hour n)"
  shows "P m"
  using type
proof (induct m)
  case 0 thus ?case by simp
next
  case (Suc m)
  from `Suc m ∈ {1..12}` have "m = 0 ∨ (m ∈ {1..12} ∧ 1 ≤ m ∧ m < 12)" by auto
  thus ?case
  proof (elim disjE conjE)
    assume "m = 0" with base show ?case by simp
  next
    assume "m ∈ {1..12}" with Suc have "P m" "1 ≤ m" "m < 12" by simp_all
    hence "P (next_hour m)" by (intro step, auto)
    with `m < 12` show ?case by (simp add: next_hour_def)
  qed
qed

locale HourClock =
  fixes hr :: "nat stfun"
  assumes hr_basevar: "basevars hr"
  fixes HCini HCnxt HC
  defines "HCini ≡ PRED hr ∈ #{1..12}"
  defines "HCnxt ≡ ACT hr$ = next_hour<$hr>"
  defines "HC    ≡ TEMP Init HCini ∧ □[HCnxt]_hr ∧ WF(HCnxt)_hr"

context HourClock
begin

lemma HCnxt_angle[simp]: "ACT <HCnxt>_hr = ACT HCnxt"
  unfolding HCnxt_def angle_def next_hour_def by auto

lemma HCnxt_enabled[simp]: "PRED (Enabled HCnxt) = PRED #True"
  using basevars [OF hr_basevar] unfolding enabled_def HCnxt_def by auto

lemma HC_safety: "⊢ HC ⟶ □ HCini"
  unfolding HC_def HCini_def HCnxt_def next_hour_def by (auto_invariant, auto)

lemma HC_liveness_step:
  assumes n: "n ∈ {1..12}"
  shows "⊢ HC ⟶ (hr = #n ↝ hr = #(next_hour n))"
proof -
  from basevars [OF hr_basevar]
  have "⊢ □[HCnxt]_hr ∧ WF(HCnxt)_hr ⟶ (hr = #n ↝ hr = #(next_hour n))"
    apply (intro WF1, auto simp add: HCnxt_def square_def next_hour_def angle_def enabled_def, auto)
    apply fastforce
    by fastforce
  thus ?thesis
    by (auto simp add: HC_def)
qed

lemma HC_liveness_progress_forwards:
  assumes m: "m ∈ {1..12}"
  assumes n: "n ∈ {1..12}"
  assumes mn: "m ≤ n"
  shows "⊢ HC ⟶ (hr = #m ↝ hr = #n)"
  using n mn
proof (induct n rule: next_hour_induct)
  case base with m show ?case apply auto using LatticeReflexivity by blast
next
  case (step n)
  hence "m ≤ n ∨ m = next_hour n" by (auto simp add: next_hour_def)
  thus ?case
  proof (elim disjE)
    assume "m = next_hour n" thus ?case apply auto using LatticeReflexivity by blast
  next
    assume "m ≤ n"
    with step have "⊢ HC ⟶ (hr = #m ↝ hr = #n)" by blast
    also from step have "⊢ HC ⟶ (hr = #n ↝ hr = #(next_hour n))"
      by (intro HC_liveness_step, auto)
    finally show ?thesis .
  qed
qed

lemma HC_liveness_progress:
  assumes m: "m ∈ {1..12}"
  assumes n: "n ∈ {1..12}"
  shows "⊢ HC ⟶ (hr = #m ↝ hr = #n)"
proof -
  from m have "⊢ HC ⟶ (hr = #m ↝ hr = #12)" by (intro HC_liveness_progress_forwards, auto)
  also from HC_liveness_step [where n = 12]
  have "⊢ HC ⟶ (hr = #12 ↝ hr = #1)" by (simp add: next_hour_def)
  also from n have "⊢ HC ⟶ (hr = #1 ↝ hr = #n)" by (intro HC_liveness_progress_forwards, auto)
  finally show ?thesis .
qed

lemma HC_liveness:
  assumes n: "n ∈ {1..12}"
  shows "⊢ HC ⟶ □◇ hr = #n"
proof -
  from HC_safety have "⊢ HC ⟶ ((#True :: stpred) ↝ HCini)"
    by (intro imp_leadsto_invariant, simp)

  also have "⊢ HC ⟶ (HCini ↝ (∃ h0. #(h0 ∈ {1..12}) ∧ hr = #h0))"
    by (intro imp_imp_leadsto, auto simp add: HCini_def)

  also have "⊢ HC ⟶ ((∃ h0. #(h0 ∈ {1..12}) ∧ hr = #h0) ↝ hr = #n)"
    unfolding inteq_reflection [OF leadsto_exists]
  proof (intro imp_forall_leadsto)
    fix h0
    from n show "h0 ∈ {1..12} ⟹ ⊢ HC ⟶ (hr = #h0 ↝ hr = #n)" by (intro HC_liveness_progress)
  qed

  finally have "⊢ HC ⟶ ((#True :: stpred) ↝ hr = #n)" .
  thus ?thesis unfolding leadsto_def by auto
qed

end

locale HourMinuteClock = HourClock +
  fixes mn :: "nat stfun"
  assumes hr_mn_basevars: "basevars (hr,mn)"
  fixes HMCini Mn Hr HMCnxt HMC
  defines "HMCini ≡ PRED HCini ∧ mn ∈ #{0..59}"
  defines "Mn     ≡ ACT mn$ = (if $mn = #59 then #0 else $mn + #1)"
  defines "Hr     ≡ ACT ($mn = #59 ∧ HCnxt) ∨ ($mn < #59 ∧ unchanged hr)"
  defines "HMCnxt ≡ ACT (Mn ∧ Hr)"
  defines "HMC    ≡ TEMP Init HMCini ∧ □[HMCnxt]_(hr, mn) ∧ WF(HMCnxt)_(hr, mn)"

context HourMinuteClock
begin

lemma HMCnxt_eq:
  "HMCnxt = ACT ($mn < #59 ∧ mn$ = $mn + #1 ∧ hr$ = $hr)
              ∨ ($mn = #59 ∧ mn$ = #0       ∧ $hr = #12 ∧ hr$ = #1)
              ∨ ($mn = #59 ∧ mn$ = #0       ∧ $hr ≠ #12 ∧ hr$ = $hr + #1)"
  by (intro ext, auto simp add: HMCnxt_def Mn_def Hr_def next_hour_def HCnxt_def)

lemma HMCnxt_angle[simp]: "ACT <HMCnxt>_(hr, mn) = ACT HMCnxt"
  by (intro ext, auto simp add: angle_def HMCnxt_eq)

lemma HMCnxt_enabled[simp]: "PRED Enabled HMCnxt = PRED mn ≤ #59"
  using basevars [OF hr_mn_basevars]
  apply (intro ext, auto simp add: enabled_def HMCnxt_eq next_hour_def)
  by (meson nat_less_le)

lemma HMC_safety: "⊢ HMC ⟶ □ (hr ∈ #{1..12} ∧ mn ∈ #{0..59})"
  unfolding HMC_def HMCini_def HCini_def HMCnxt_eq next_hour_def
  by (invariant, auto simp add: square_def Init_def)

definition timeIs :: "nat × nat ⇒ stpred" where "timeIs t ≡ PRED (hr, mn) = #t"

lemma timeIs[simp]: "PRED (timeIs (h,m)) = PRED (hr = #h ∧ mn = #m)"
  by (auto simp add: timeIs_def)

lemma HMC_liveness_step:
  assumes "m ≤ 59"
  shows "⊢ HMC ⟶ (timeIs (h, m) ↝ (timeIs (if m = 59 then (if h = 12 then (1, 0) else (h+1, 0)) else (h, m+1))))"
    (is "⊢ HMC ⟶ ?P")
proof -
  from assms
  have "⊢ □[HMCnxt]_(hr, mn) ∧ WF(HMCnxt)_(hr,mn) ⟶ ?P"
    by (intro WF1 actionI temp_impI, auto simp add: square_def, auto simp add: HMCnxt_eq)
  thus ?thesis by (auto simp add: HMC_def)
qed

lemma HMC_liveness_step_minute:
  assumes "m < 59"
  shows "⊢ HMC ⟶ (timeIs (h,m) ↝ timeIs (h, Suc m))"
  using HMC_liveness_step [of m h] assms by auto

lemma HMC_liveness_step_hour:
  shows "⊢ HMC ⟶ (timeIs (h,59) ↝ timeIs (next_hour h, 0))"
  using HMC_liveness_step [of 59 h] unfolding next_hour_def by auto

lemma HMC_liveness_progress_forwards_minute:
  assumes m12: "m1 ≤ m2" and m2: "m2 ≤ 59"
  shows "⊢ HMC ⟶ (timeIs (h,m1) ↝ timeIs (h,m2))"
  using assms
proof (induct m2)
  case 0 thus ?case apply auto using LatticeReflexivity by blast
next
  case (Suc m)
  hence m59: "m ≤ 59" by simp

  from Suc have "m1 ≤ m ∨ m1 = Suc m" by auto
  thus ?case
  proof (elim disjE)
    assume "m1 = Suc m" thus ?thesis apply auto using LatticeReflexivity by blast
  next
    assume "m1 ≤ m"
    with Suc.hyps m59
    have "⊢ HMC ⟶ (timeIs (h,m1) ↝ timeIs (h,m))" by metis

    also from Suc have "⊢ HMC ⟶ (timeIs (h,m) ↝ timeIs (h, Suc m))"
      by (intro HMC_liveness_step_minute, auto)

    finally show ?thesis .
  qed
qed

lemma HMC_liveness_progress_forwards_hour:
  assumes h1: "h1 ∈ {1..12}"
  assumes h2: "h2 ∈ {1..12}"
  assumes h1h2: "h1 ≤ h2" 
  shows "⊢ HMC ⟶ (timeIs (h1,59) ↝ timeIs (h2,59))"
  using h2 h1h2
proof (induct h2 rule: next_hour_induct)
  case base with h1 show ?case apply auto using LatticeReflexivity by blast
next
  case (step h)
  hence "h1 ≤ h ∨ h1 = next_hour h" unfolding next_hour_def by auto
  thus ?case
  proof (elim disjE)
    assume "h1 = next_hour h" thus ?thesis apply auto using LatticeReflexivity by blast
  next
    assume "h1 ≤ h"
    with step have "⊢ HMC ⟶ (timeIs (h1, 59) ↝ timeIs (h, 59))" by metis

    also have "⊢ HMC ⟶ (timeIs (h, 59) ↝ timeIs (next_hour h, 0))" by (intro HMC_liveness_step_hour)

    also have "⊢ HMC ⟶ (timeIs (next_hour h, 0) ↝ timeIs (next_hour h, 59))"
      by (intro HMC_liveness_progress_forwards_minute, simp_all)

    finally show ?thesis.
  qed
qed

lemma HMC_liveness_progress:
  assumes h1: "h1 ∈ {1..12}"
  assumes h2: "h2 ∈ {1..12}"
  assumes m1: "m1 ≤ 59"
  assumes m2: "m2 ≤ 59"
  shows "⊢ HMC ⟶ (timeIs (h1,m1) ↝ timeIs (h2,m2))"
proof -
  from m1 have "⊢ HMC ⟶ (timeIs (h1,m1) ↝ timeIs (h1,59))"
    by (intro HMC_liveness_progress_forwards_minute, simp_all)

  also from h1 have "⊢ HMC ⟶ (timeIs (h1,59) ↝ timeIs (12,59))"
    by (intro HMC_liveness_progress_forwards_hour, simp_all)

  also from HMC_liveness_step_hour [of 12]
  have "⊢ HMC ⟶ (timeIs (12,59) ↝ timeIs (1,0))"
    by (simp add: next_hour_def)

  also have "⊢ HMC ⟶ (timeIs (1,0) ↝ timeIs (h2,0))"
  proof (cases "h2 = 1")
    case True thus ?thesis apply auto using LatticeReflexivity by blast
  next
    case False
    have "⊢ HMC ⟶ (timeIs (1, 0) ↝ timeIs (1, 59))"
      by (intro HMC_liveness_progress_forwards_minute, simp_all)

    also from False h2
    have "⊢ HMC ⟶ (timeIs (1, 59) ↝ timeIs (h2 - 1, 59))"
      by (intro HMC_liveness_progress_forwards_hour, auto)

    also from False h2 have "next_hour (h2 - 1) = h2"
      by (auto simp add: next_hour_def)

    with HMC_liveness_step_hour [of "h2 - 1"]
    have "⊢ HMC ⟶ (timeIs (h2 - 1, 59) ↝ timeIs (h2, 0))" by auto
    
    finally show ?thesis .
  qed

  also from m2 have "⊢ HMC ⟶ (timeIs (h2, 0) ↝ timeIs (h2, m2))"
    by (intro HMC_liveness_progress_forwards_minute, simp_all)

  finally show ?thesis .
qed

lemma HMC_liveness: 
  assumes h: "h ∈ {1..12}"
  assumes m: "m ≤ 59"
  shows "⊢ HMC ⟶ □◇ timeIs (h,m)"
proof -
  from HMC_safety
  have "⊢ HMC ⟶ ((#True :: stpred) ↝ (hr ∈ #{1..12} ∧ mn ∈ #{0..59}))"
    by (intro imp_leadsto_invariant, simp)

  also have "⊢ HMC ⟶ ((hr ∈ #{1..12} ∧ mn ∈ #{0..59}) ↝ (∃t. #(fst t ∈ {1..12} ∧ snd t ≤ 59) ∧ timeIs t))"
    by (intro imp_imp_leadsto, auto)

  also have "⊢ HMC ⟶ ((∃t. #(fst t ∈ {1..12} ∧ snd t ≤ 59) ∧ timeIs t) ↝ timeIs (h,m))"
    unfolding inteq_reflection [OF leadsto_exists]
  proof (intro imp_forall_leadsto)
    fix t :: "nat × nat"
    obtain h' m' where t: "t = (h', m')" by fastforce
    show "fst t ∈ {1..12} ∧ snd t ≤ 59 ⟹ ⊢ HMC ⟶ (timeIs t ↝ timeIs (h, m))"
      unfolding t using h m
      by (intro HMC_liveness_progress, auto)
  qed
   
  finally show ?thesis
    by (auto simp add: leadsto_def)
qed

lemma HMC_refines_HC: "⊢ HMC ⟶ HC"
  unfolding HC_def
proof (intro temp_imp_conjI)
  show "⊢ HMC ⟶ Init HCini" by (auto simp add: HMC_def HMCini_def Init_def)

  have "⊢ HMC ⟶ □[HMCnxt]_(hr, mn)" by auto (simp add: HMC_def)
  moreover have "⊢ [HMCnxt]_(hr, mn) ⟶ [HCnxt]_hr"
  proof (intro intI temp_impI, clarify)
    fix before after
    assume "(before, after) ⊨ [HMCnxt]_(hr, mn)"
    thus "(before, after) ⊨ [HCnxt]_hr"
      by (cases "mn before = 59", auto simp add: square_def HMCnxt_eq HCnxt_def next_hour_def)
  qed
  ultimately show "⊢ HMC ⟶ □[HCnxt]_hr" by (metis STL4 temp_imp_trans)

  define P :: stpred   where "P ≡ timeIs (1,59)"
  define B :: action   where "B ≡ ACT $P"
  define F :: temporal where "F ≡ TEMP ◇P"
  define N :: action   where "N ≡ ACT [HMCnxt]_(hr,mn)"
  define A :: action   where "A ≡ HMCnxt"
    
  have "⊢ <$P ∧ HMCnxt>_(hr, mn) = ($P ∧ HMCnxt)" by (auto simp add: angle_def HMCnxt_eq)
  note eqs = inteq_reflection [OF this]

  have "⊢ HMC ⟶ □N ∧ WF(A)_(hr,mn) ∧ □F"
  proof (intro temp_imp_conjI)
    show "⊢ HMC ⟶ □N" by (auto simp add: N_def HMC_def)
    from HMC_liveness show "⊢ HMC ⟶ □F" unfolding F_def P_def by auto

    show "⊢ HMC ⟶ WF(A)_(hr, mn)"
      unfolding HMC_def WF_def eqs A_def by auto
  qed

  also have "⊢ □N ∧ WF(A)_(hr,mn) ∧ □F ⟶ WF(HCnxt)_hr"
  proof (intro WF2 stable_dmd_stuck)

    show "⊢ N ∧ <B>_(hr, mn) ⟶ <HCnxt>_hr"
      by (auto simp add: N_def square_def angle_def P_def B_def HMCnxt_eq HCnxt_def next_hour_def)

    show "⊢ $P ∧ P$ ∧ <N ∧ A>_(hr, mn) ⟶ B"
      by (auto simp add: angle_def P_def)

    show "⊢ P ∧ Enabled (<HCnxt>_hr) ⟶ Enabled (<A>_(hr, mn))"
      unfolding eqs A_def by (auto simp add: P_def)

    let ?PREM = "TEMP □(N ∧ [¬ B]_(hr, mn)) ∧ WF(A)_(hr, mn) ∧ □F ∧ ◇□Enabled (<HCnxt>_hr)"

    show "⊢ ?PREM ⟶ stable P"
      apply (intro tempI temp_impI Stable [where A = "ACT N ∧ [¬ $P]_(hr, mn)"])
      by (auto simp add: square_def P_def N_def B_def)

    have "⊢ ?PREM ⟶ □◇P" unfolding F_def by auto
    also have "⊢ □◇P ⟶ ◇P" by (intro STL2)
    finally show "⊢ ?PREM ⟶ ◇ P" .
  qed

  finally show "⊢ HMC ⟶ WF(HCnxt)_hr" .

qed

end

end