Theory CTL

section CTL

theory CTL
  imports Graphs
begin

lemmas [simp] = holds.simps

context Graph_Defs
begin

definition
  "Alw_ev φ x ≡ ∀ xs. run (x ## xs) ⟶ ev (holds φ) (x ## xs)"

definition
  "Alw_alw φ x ≡ ∀ xs. run (x ## xs) ⟶ alw (holds φ) (x ## xs)"

definition
  "Ex_ev φ x ≡ ∃ xs. run (x ## xs) ∧ ev (holds φ) (x ## xs)"

definition
  "Ex_alw φ x ≡ ∃ xs. run (x ## xs) ∧ alw (holds φ) (x ## xs)"

definition
  "leadsto φ ψ x ≡ Alw_alw (λ x. φ x ⟶ Alw_ev ψ x) x"

definition
  "deadlocked x ≡ ¬ (∃ y. x → y)"

definition
  "deadlock x ≡ ∃ y. reaches x y ∧ deadlocked y"

lemma no_deadlockD:
  "¬ deadlocked y" if "¬ deadlock x" "reaches x y"
  using that unfolding deadlock_def by auto

lemma not_deadlockedE:
  assumes "¬ deadlocked x"
  obtains y where "x → y"
  using assms unfolding deadlocked_def by auto

lemma holds_Not:
  "holds (Not ∘ φ) = (λ x. ¬ holds φ x)"
  by auto

lemma Alw_alw_iff:
  "Alw_alw φ x ⟷ ¬ Ex_ev (Not o φ) x"
  unfolding Alw_alw_def Ex_ev_def holds_Not not_ev_not[symmetric] by simp

lemma Ex_alw_iff:
  "Ex_alw φ x ⟷ ¬ Alw_ev (Not o φ) x"
  unfolding Alw_ev_def Ex_alw_def holds_Not not_ev_not[symmetric] by simp

lemma leadsto_iff:
  "leadsto φ ψ x ⟷ ¬ Ex_ev (λ x. φ x ∧ ¬ Alw_ev ψ x) x"
  unfolding leadsto_def Alw_alw_iff by (simp add: comp_def)

lemma run_siterate_from:
  assumes "∀y. x →* y ⟶ (∃ z. y → z)"
  shows "run (siterate (λ x. SOME y. x → y) x)" (is "run (siterate ?f x)")
  using assms
proof (coinduction arbitrary: x)
  case (run x)
  let ?y = "SOME y. x → y"
  from run have "x → ?y"
    by (auto intro: someI)
  with run show ?case including graph_automation_aggressive by auto
qed

(* XXX Move *)
lemma extend_run':
  "run zs" if "steps xs" "run ys" "last xs = shd ys" "xs @- stl ys = zs"
  (* s/h *)
  by (metis
      Graph_Defs.run.cases Graph_Defs.steps_non_empty' extend_run
      stream.exhaust_sel stream.inject that)

lemma no_deadlock_run_extend:
  "∃ ys. run (x ## xs @- ys)" if "¬ deadlock x" "steps (x # xs)"
proof -
  include graph_automation
  let ?x = "last (x # xs)" let ?f = "λ x. SOME y. x → y" let ?ys = "siterate ?f ?x"
  have "∃z. y → z" if "?x →* y" for y
  proof -
    from ‹steps (x # xs)› have "x →* ?x"
    by auto
    from ‹x →* ?x› ‹?x →* y› have "x →* y"
      by auto
    with ‹¬ deadlock x› show ?thesis
      by (auto dest: no_deadlockD elim: not_deadlockedE)
  qed
  then have "run ?ys"
    by (blast intro: run_siterate_from)
  with ‹steps (x # xs)› show ?thesis
    by (fastforce intro: extend_run')
qed

lemma Ex_ev:
  "Ex_ev φ x ⟷ (∃ y. x →* y ∧ φ y)" if "¬ deadlock x"
  unfolding Ex_ev_def
proof safe
  fix xs assume prems: "run (x ## xs)" "ev (holds φ) (x ## xs)"
  show "∃y. x →* y ∧ φ y"
  proof (cases "φ x")
    case True
    then show ?thesis
      by auto
  next
    case False
    with prems obtain y ys zs where
      "φ y" "xs = ys @- y ## zs" "y ∉ set ys"
      unfolding ev_holds_sset by (auto elim!:split_stream_first')
    with prems have "steps (x # ys @ [y])"
      by (auto intro: run_decomp[THEN conjunct1]) (* XXX *)
    with ‹φ y› show ?thesis
      including graph_automation by (auto 4 3)
  qed
next
  fix y assume "x →* y" "φ y"
  then obtain xs where
    "φ (last xs)" "x = hd xs" "steps xs" "y = last xs"
    by (auto dest: reaches_steps)
  then show "∃xs. run (x ## xs) ∧ ev (holds φ) (x ## xs)"
    by (cases xs)
       (auto split: if_split_asm simp: ev_holds_sset dest!: no_deadlock_run_extend[OF that])
qed

lemma Alw_ev:
  "Alw_ev φ x ⟷ ¬ (∃ xs. run (x ## xs) ∧ alw (holds (Not o φ)) (x ## xs))"
  unfolding Alw_ev_def
proof (safe, goal_cases)
  case prems: (1 xs)
  then have "ev (holds φ) (x ## xs)" by auto
  then show ?case
    using prems(2,3) by induction (auto intro: run_stl)
next
  case prems: (2 xs)
  then have "¬ alw (holds (Not ∘ φ)) (x ## xs)"
    by auto
  moreover have "(λ x. ¬ holds (Not ∘ φ) x) = holds φ"
    by (rule ext) simp
  ultimately show ?case
    unfolding not_alw_iff by simp
qed

lemma leadsto_iff':
  "leadsto φ ψ x ⟷ (∄y. x →* y ∧ φ y ∧ ¬ Alw_ev ψ y)" if "¬ deadlock x"
  unfolding leadsto_iff Ex_ev[OF ‹¬ deadlock x›] ..

end (* Graph Defs *)

context Bisimulation_Invariant
begin

context
  fixes φ :: "'a ⇒ bool" and ψ :: "'b ⇒ bool"
  assumes compatible: "A_B.equiv' a b ⟹ φ a ⟷ ψ b"
begin

lemma ev_ψ_φ:
  "ev (holds φ) xs" if "stream_all2 B_A.equiv' ys xs" "ev (holds ψ) ys"
  using that
  apply -
  apply (drule stream_all2_rotate_1)
  apply (drule ev_imp_shift)
  apply clarify
  unfolding stream_all2_shift2
  apply (subst (asm) stream.rel_sel)
  apply (auto intro!: ev_shift dest!: compatible[symmetric])
  done

lemma ev_φ_ψ:
  "ev (holds ψ) ys" if "stream_all2 A_B.equiv' xs ys" "ev (holds φ) xs"
  using that
  apply -
  apply (subst (asm) stream.rel_flip[symmetric])
  apply (drule ev_imp_shift)
  apply clarify
  unfolding stream_all2_shift2
  apply (subst (asm) stream.rel_sel)
  apply (auto intro!: ev_shift dest!: compatible)
  done

lemma Ex_ev_iff:
  "A.Ex_ev φ a ⟷ B.Ex_ev ψ b" if "A_B.equiv' a b"
  unfolding Graph_Defs.Ex_ev_def
  apply safe
  subgoal for xs
    apply (drule A_B.simulation_run[of a xs b])
    subgoal
      using that .
    apply clarify
    subgoal for ys
      apply (inst_existentials ys)
      using that
       apply (auto intro!: ev_φ_ψ dest: stream_all2_rotate_1)
      done
    done
  subgoal for ys
    apply (drule B_A.simulation_run[of b ys a])
    subgoal
      using that by (rule equiv'_rotate_1)
    apply clarify
    subgoal for xs
      apply (inst_existentials xs)
      using that
       apply (auto intro!: ev_ψ_φ dest: equiv'_rotate_1)
      done
    done
  done

lemma Alw_ev_iff:
  "A.Alw_ev φ a ⟷ B.Alw_ev ψ b" if "A_B.equiv' a b"
  unfolding Graph_Defs.Alw_ev_def
  apply safe
  subgoal for ys
    apply (drule B_A.simulation_run[of b ys a])
    subgoal
      using that by (rule equiv'_rotate_1)
    apply safe
    subgoal for xs
      apply (inst_existentials xs)
        apply (elim allE impE, assumption)
      using that
        apply (auto intro!: ev_φ_ψ dest: stream_all2_rotate_1)
      done
    done
  subgoal for xs
    apply (drule A_B.simulation_run[of a xs b])
    subgoal
      using that .
    apply safe
    subgoal for ys
      apply (inst_existentials ys)
      apply (elim allE impE, assumption)
      using that
      apply (auto intro!: ev_ψ_φ elim!: equiv'_rotate_1 stream_all2_rotate_2)
      done
    done
  done  

end (* Compatiblity *)

context
  fixes φ :: "'a ⇒ bool" and ψ :: "'b ⇒ bool"
  assumes compatible1: "A_B.equiv' a b ⟹ φ a ⟷ ψ b"
begin

lemma Alw_alw_iff_strong:
  "A.Alw_alw φ a ⟷ B.Alw_alw ψ b" if "A_B.equiv' a b"
  unfolding Graph_Defs.Alw_alw_iff using that by (auto dest: compatible1 intro!: Ex_ev_iff)

lemma Ex_alw_iff:
  "A.Ex_alw φ a ⟷ B.Ex_alw ψ b" if "A_B.equiv' a b"
  unfolding Graph_Defs.Ex_alw_iff using that by (auto dest: compatible1 intro!: Alw_ev_iff)

end (* Compatibility *)

context
  fixes φ :: "'a ⇒ bool" and ψ :: "'b ⇒ bool"
    and φ' :: "'a ⇒ bool" and ψ' :: "'b ⇒ bool"
  assumes compatible1: "A_B.equiv' a b ⟹ φ a ⟷ ψ b"
  assumes compatible2: "A_B.equiv' a b ⟹ φ' a ⟷ ψ' b"
begin

lemma Leadsto_iff:
  "A.leadsto φ φ' a ⟷ B.leadsto ψ ψ' b" if "A_B.equiv' a b"
  unfolding Graph_Defs.leadsto_def
  by (auto
        dest: Alw_ev_iff[of φ' ψ', rotated] compatible1 compatible2 equiv'_D
        intro!: Alw_alw_iff_strong[OF _ that]
     )

end (* Compatibility *)

lemma deadlock_iff:
  "A.deadlock a ⟷ B.deadlock b" if "a ∼ b" "PA a" "PB b"
  using that unfolding A.deadlock_def A.deadlocked_def B.deadlock_def B.deadlocked_def
  by (force dest: A_B_step B_A_step B_A.simulation_reaches A_B.simulation_reaches)

end

lemmas [simp del] = holds.simps

end (* Theory *)