Theory Temporal_Logics

theory Temporal_Logics
  imports Timed_Automata.CTL LTL.LTL LTL_Master_Theorem.Omega_Words_Fun_Stream
begin

lemmas [simp] = holds.simps

lemma suffix_stl:
  "suffix (Suc 0) (snth xs) = snth (stl xs)"
  unfolding suffix_def by auto

lemma suntil_iff_sdrop:
  "(φ suntil ψ) xs ⟷ (∃i. ψ (sdrop i xs) ∧ (∀j<i. φ (sdrop j xs)))"
proof safe
  show "∃i. ψ (sdrop i xs) ∧ (∀j<i. φ (sdrop j xs))" if "(φ suntil ψ) xs"
    using that
  proof (induction rule: suntil.induct)
    case (base ω)
    then show ?case
      by force
  next
    case (step ω)
    then obtain i where "ψ (sdrop i (stl ω))" "∀j<i. φ (sdrop j (stl ω))"
      by safe
    with ‹φ ω› have "φ (sdrop j ω)" if "j<i + 1" for j
      using that by (cases j) auto
    with ‹ψ (sdrop i (stl ω))› show ?case
      by (inst_existentials "i + 1") auto
  qed
  show "(φ suntil ψ) xs" if "ψ (sdrop i xs)" "∀j<i. φ (sdrop j xs)" for i
    using that by (induction i arbitrary: xs; fastforce intro: suntil.intros)
qed

lemma to_stream_suffix_Suc:
  "to_stream (suffix (Suc k) xs) = stl (to_stream (suffix k xs))"
  by (metis add.right_neutral add_Suc_right suffix_stl suffix_suffix
        to_omega_def to_omega_to_stream to_stream_to_omega)

lemma to_stream_stake:
  "sdrop k (to_stream w) = to_stream (suffix k w)"
  by (induction k arbitrary: w) (auto simp: sdrop_stl to_stream_suffix_Suc)

lemma to_omega_suffix[simp]:
  "suffix k (to_omega s) = to_omega (sdrop k s)"
  by auto

primrec semantics_ltlc' :: "['a word, ('a ⇒ bool) ltlc] ⇒ bool" ("_ ⊨c'' _" [80,80] 80)
where
  "ξ ⊨c' truec = True"
| "ξ ⊨c' falsec = False"
| "ξ ⊨c' propc(q) = (q (ξ 0))"
| "ξ ⊨c' notc φ = (¬ ξ ⊨c' φ)"
| "ξ ⊨c' φ andc ψ = (ξ ⊨c' φ ∧ ξ ⊨c' ψ)"
| "ξ ⊨c' φ orc ψ = (ξ ⊨c' φ ∨ ξ ⊨c' ψ)"
| "ξ ⊨c' φ impliesc ψ = (ξ ⊨c' φ ⟶ ξ ⊨c' ψ)"
| "ξ ⊨c' Xc φ = (suffix 1 ξ ⊨c' φ)"
| "ξ ⊨c' Fc φ = (∃i. suffix i ξ ⊨c' φ)"
| "ξ ⊨c' Gc φ = (∀i. suffix i ξ ⊨c' φ)"
| "ξ ⊨c' φ Uc ψ = (∃i. suffix i ξ ⊨c' ψ ∧ (∀j<i. suffix j ξ ⊨c' φ))"
| "ξ ⊨c' φ Rc ψ = (∀i. suffix i ξ ⊨c' ψ ∨ (∃j<i. suffix j ξ ⊨c' φ))"
| "ξ ⊨c' φ Wc ψ = (∀i. suffix i ξ ⊨c' φ ∨ (∃j≤i. suffix j ξ ⊨c' ψ))"
| "ξ ⊨c' φ Mc ψ = (∃i. suffix i ξ ⊨c' φ ∧ (∀j≤i. suffix j ξ ⊨c' ψ))"

lemma semantics_ltlc'_sugar [simp]:
  "ξ ⊨c' φ iffc ψ = (ξ ⊨c' φ ⟷ ξ ⊨c' ψ)"
  "ξ ⊨c' Fc φ = ξ ⊨c' (truec Uc φ)"
  "ξ ⊨c' Gc φ = ξ ⊨c' (falsec Rc φ)"
  by (auto simp add: Iff_ltlc_def)

definition "language_ltlc' φ ≡ {ξ. ξ ⊨c' φ}"

fun ltlc_to_pltl :: "('a ⇒ bool) ltlc ⇒ 'a pltl"
where
  "ltlc_to_pltl truec = truep"
| "ltlc_to_pltl falsec = falsep"
| "ltlc_to_pltl (propc(q)) = atomp(q)"
| "ltlc_to_pltl (notc φ) = notp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (φ andc ψ) = (ltlc_to_pltl φ) andp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ orc ψ) = (ltlc_to_pltl φ) orp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ impliesc ψ) = (ltlc_to_pltl φ) impliesp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (Xc φ) = Xp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (Fc φ) = Fp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (Gc φ) = Gp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (φ Uc ψ) = (ltlc_to_pltl φ) Up (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ Rc ψ) = (ltlc_to_pltl φ) Rp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ Wc ψ) = (ltlc_to_pltl φ) Wp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ Mc ψ) = (ltlc_to_pltl φ) Mp (ltlc_to_pltl ψ)"

lemma ltlc_to_pltl_semantics [simp]:
  "w ⊨p ltlc_to_pltl φ ⟷ w ⊨c' φ"
  by (induction φ arbitrary: w) simp_all

lemma semantics_ltlc'_semantics_ltlc_atoms_iff:
  "w ⊨c' φ ⟷ (λi. {a ∈ atoms_ltlc φ. a (w i)}) ⊨c φ"
proof -
  have *:
    "(λi. {a. (a ∈ atoms_ltlc φ1 ∨ a ∈ atoms_ltlc φ2) ∧ a (w i)}) ⊨c φ1
    ⟷ ((λi. {a ∈ atoms_ltlc φ1. a (w i)}) ⊨c φ1)" for w :: "nat ⇒ 'a" and φ1 φ2
    by (rule ltlc_eq_on) (auto simp: pw_eq_on_def)
  have **:
    "(λi. {a. (a ∈ atoms_ltlc φ1 ∨ a ∈ atoms_ltlc φ2) ∧ a (w i)}) ⊨c φ2
    ⟷ ((λi. {a ∈ atoms_ltlc φ2. a (w i)}) ⊨c φ2)"  for w :: "nat ⇒ 'a" and φ1 φ2
      by (rule ltlc_eq_on) (auto simp: pw_eq_on_def)
  show ?thesis
    by (induction φ arbitrary: w) (simp_all add: suffix_def * **)
qed

lemma semantics_ltlc'_semantics_ltlc_atoms_iff':
  "w ⊨c' φ ⟷ ((λx. {a ∈ atoms_ltlc φ. a x}) o w) ⊨c φ"
  unfolding comp_def by (rule semantics_ltlc'_semantics_ltlc_atoms_iff)

lemma map_semantics_ltlc_inj:
  assumes "inj f"
  shows "w ⊨c φ ⟷ (image f o w) ⊨c map_ltlc f φ"
  using assms unfolding comp_def by (intro map_semantics_ltlc_aux) auto

lemma semantics_ltlc'_abstract:
  assumes "inj abstr" "⋀x. label x = abstr ` {a ∈ atoms_ltlc φ. a x}"
  shows "w ⊨c' φ ⟷ (label o w) ⊨c map_ltlc abstr φ"
  by (subst semantics_ltlc'_semantics_ltlc_atoms_iff')
     (simp add: comp_def assms(2) map_semantics_ltlc_inj[OF ‹inj abstr›])

context
  includes lifting_syntax
begin

lemma holds_transfer:
  "((R ===> (=)) ===> stream_all2 R ===> (=)) holds holds"
  apply (intro rel_funI)
  subgoal for φ ψ xs ys
    by (cases xs; cases ys) (auto dest: rel_funD)
  done

lemma alw_mono1:
  "alw φ xs" if "(stream_all2 R ===> (=)) φ ψ" "stream_all2 R xs ys" "alw ψ ys"
  using that(2,3)
  by (coinduction arbitrary: xs ys) (use that(1) stream.rel_sel in ‹auto dest!: rel_funD›)

lemma alw_mono2:
  "alw ψ ys" if "(stream_all2 R ===> (=)) φ ψ" "stream_all2 R xs ys" "alw φ xs"
  using that(2,3)
  by (coinduction arbitrary: xs ys) (use that(1) stream.rel_sel in ‹auto dest!: rel_funD›)

lemma alw_transfer':
  "alw x xs = alw y ys" if "(stream_all2 R ===> (=)) x y" "stream_all2 R xs ys"
  using alw_mono1 alw_mono2 that by blast

lemma alw_transfer:
  "((stream_all2 R ===> (=)) ===> stream_all2 R ===> (=)) alw alw"
  by (intro rel_funI) (rule alw_transfer')

lemma nxt_transfer:
  "((stream_all2 R ===> (=)) ===> stream_all2 R ===> (=)) nxt nxt"
  by (intro rel_funI) (simp, meson rel_funD stream.rel_sel)

lemma suntil_mono1:
  "(φ suntil ψ) xs"
  if "(stream_all2 R ===> (=)) φ φ'" "(stream_all2 R ===> (=)) ψ ψ'" "stream_all2 R xs ys"
     "(φ' suntil ψ') ys"
  using that(4,3)
proof (induction arbitrary: xs)
  case (base ω)
  then show ?case
    using that(1,2) by (auto dest!: rel_funD intro: suntil.base)
next
  case (step ω)
  from ‹stream_all2 R xs ω› have "stream_all2 R (stl xs) (stl ω)"
    using stream.rel_sel by auto
  from ‹φ' ω› ‹stream_all2 R xs ω› have "φ xs"
    using that(1,2) by (auto dest!: rel_funD)
  moreover from step.IH ‹stream_all2 R xs ω› have "(φ suntil ψ) (stl xs)"
    using stream.rel_sel by auto
  ultimately show ?case ..
qed

lemma suntil_mono2:
  "(φ' suntil ψ') ys"
  if "(stream_all2 R ===> (=)) φ φ'" "(stream_all2 R ===> (=)) ψ ψ'" "stream_all2 R xs ys"
     "(φ suntil ψ) xs"
  using that(4,3)
proof (induction arbitrary: ys)
  case (base ω)
  then show ?case
    using that(1,2) by (auto dest!: rel_funD intro: suntil.base)
next
  case (step xs ω)
  from ‹stream_all2 R xs ω› have "stream_all2 R (stl xs) (stl ω)"
    using stream.rel_sel by auto
  from ‹φ xs› ‹stream_all2 R xs ω› have "φ' ω"
    using that(1,2) by (auto dest!: rel_funD)
  moreover from step.IH ‹stream_all2 R xs ω› have "(φ' suntil ψ') (stl ω)"
    using stream.rel_sel by auto
  ultimately show ?case ..
qed

lemma suntil_transfer':
  "(φ suntil ψ) xs = (φ' suntil ψ') ys"
  if "(stream_all2 R ===> (=)) φ φ'" "(stream_all2 R ===> (=)) ψ ψ'" "stream_all2 R xs ys"
  using suntil_mono1 suntil_mono2 that by metis

lemma suntil_transfer:
  "((stream_all2 R ===> (=)) ===> (stream_all2 R ===> (=)) ===> stream_all2 R ===> (=))
    Linear_Temporal_Logic_on_Streams.suntil Linear_Temporal_Logic_on_Streams.suntil"
  by (intro rel_funI) (rule suntil_transfer')

lemma ev_mono1:
  "ev φ xs" if "(stream_all2 R ===> (=)) φ ψ" "stream_all2 R xs ys" "ev ψ ys"
  using that(3,2) by (induction arbitrary: xs; use that(1) stream.rel_sel in ‹blast dest: rel_funD›)

lemma ev_mono2:
  "ev ψ ys" if "(stream_all2 R ===> (=)) φ ψ" "stream_all2 R xs ys" "ev φ xs"
  using that(3,2) by (induction arbitrary: ys; use that(1) stream.rel_sel in ‹blast dest: rel_funD›)

lemma ev_transfer':
  "ev x xs = ev y ys" if "(stream_all2 R ===> (=)) x y" "stream_all2 R xs ys"
  using ev_mono1 ev_mono2 that by blast

lemma ev_transfer:
  "((stream_all2 R ===> (=)) ===> (stream_all2 R ===> (=))) ev ev"
  by (intro rel_funI) (rule ev_transfer')

end

datatype 'a ctl_formula =
  AG "'a ctl_formula" | AX "'a ctl_formula" | EG "'a ctl_formula" | EX "'a ctl_formula" | PropC 'a |
  ImpliesC "'a ctl_formula" "'a ctl_formula" | NotC "'a ctl_formula"

datatype 'a state_formula =
  All "'a path_formula" | Ex "'a path_formula"
| ImpliesS "'a state_formula" "'a state_formula" | NotS "'a state_formula" | PropS 'a
and 'a path_formula =
  G "'a path_formula" | F "'a path_formula"
| X "'a path_formula" | Until "'a path_formula" "'a path_formula"
| ImpliesP "'a path_formula" "'a path_formula" | NotP "'a path_formula" | State "'a state_formula"
| FalseP

fun ctl_to_state where
  "ctl_to_state (AG φ) = All (G (State (ctl_to_state φ)))"
| "ctl_to_state (AX φ) = All (F (State (ctl_to_state φ)))"
| "ctl_to_state (EG φ) = Ex  (G (State (ctl_to_state φ)))"
| "ctl_to_state (ctl_formula.EX φ) = Ex (F (State (ctl_to_state φ)))"
| "ctl_to_state (PropC φ) = PropS φ"
| "ctl_to_state (ImpliesC φ ψ) = ImpliesS (ctl_to_state φ) (ctl_to_state ψ)"
| "ctl_to_state (NotC φ) = NotS (ctl_to_state φ)"

fun ltlp_to_path where
  "ltlp_to_path falsep = FalseP"
| "ltlp_to_path (atomp(φ)) = State (PropS φ)"
| "ltlp_to_path (φ impliesp ψ) = ImpliesP (ltlp_to_path φ) (ltlp_to_path ψ)"
| "ltlp_to_path (Xp φ) = X (ltlp_to_path φ)"
| "ltlp_to_path (φ Up ψ) = Until (ltlp_to_path φ) (ltlp_to_path ψ)"

fun rel_pltl where
  "rel_pltl R falsep falsep = True"
| "rel_pltl R atomp(x) atomp(y) = R x y"
| "rel_pltl R (x impliesp y) (x' impliesp y') ⟷ rel_pltl R x x' ∧ rel_pltl R y y'"
| "rel_pltl R (x Up y) (x' Up y') ⟷ rel_pltl R x x' ∧ rel_pltl R y y'"
| "rel_pltl R (Xp x) (Xp y) ⟷ rel_pltl R x y"
| "rel_pltl _ _ _ = False"

lemma rel_ltlp_to_path:
  "rel_pltl R φ ψ ⟷ rel_path_formula R (ltlp_to_path φ) (ltlp_to_path ψ)"
  by (induction R φ ψ rule: rel_pltl.induct) auto

lemma [simp]:
  "falsep = truep ⟷ False"
  unfolding True_ltlp_def Not_ltlp_def by auto

lemmas ltlp_defs =
  True_ltlp_def Not_ltlp_def And_ltlp_def Or_ltlp_def
  Eventually_ltlp_def Always_ltlp_def Release_ltlp_def WeakUntil_ltlp_def StrongRelease_ltlp_def

text ‹The converse does not hold!›
lemma rel_ltlc_to_pltl:
  "rel_pltl R (ltlc_to_pltl φ) (ltlc_to_pltl ψ)" if "rel_ltlc R φ ψ"
  using that by (induction rule: ltlc.rel_induct) (auto simp: ltlp_defs)

context Graph_Defs
begin

fun models_state and models_path where
  "models_state (PropS P) x = P x"
| "models_state (All φ) x = (∀xs. run (x ## xs) ⟶ models_path φ (x ## xs))"
| "models_state (Ex φ) x = (∃xs. run (x ## xs) ∧ models_path φ (x ## xs))"
| "models_state (ImpliesS ψ ψ') xs = (models_state ψ xs ⟶ models_state ψ' xs)"
| "models_state (NotS ψ) xs = (¬ models_state ψ xs)"
| "models_path  (State ψ) = holds (models_state ψ)"
| "models_path  (G ψ) = alw (models_path ψ)"
| "models_path  (F ψ) = ev (models_path ψ)"
| "models_path  (X ψ) = nxt (models_path ψ)"
| "models_path  (Until ψ ψ') = models_path ψ suntil models_path ψ'"
| "models_path  FalseP = (λ_. False)"
| "models_path  (ImpliesP ψ ψ') = (λxs. models_path ψ xs ⟶ models_path ψ' xs)"
| "models_path  (NotP ψ) = (λxs. ¬ models_path ψ xs)"

fun models_ctl where
  "models_ctl (PropC P) = P"
| "models_ctl (AG φ) = Alw_alw (models_ctl φ)"
| "models_ctl (AX φ) = Alw_ev (models_ctl φ)"
| "models_ctl (EG φ) = Ex_alw (models_ctl φ)"
| "models_ctl (ctl_formula.EX φ) = Ex_ev (models_ctl φ)"
| "models_ctl (ImpliesC φ ψ) = (λx. models_ctl φ x ⟶ models_ctl ψ x)"
| "models_ctl (NotC φ) = (λx. ¬ models_ctl φ x)"

fun models_ltlp where
  "models_ltlp falsep = (λ_. False)"
| "models_ltlp (atomp(P)) = holds P"
| "models_ltlp (φ impliesp ψ) = (λx. models_ltlp φ x ⟶ models_ltlp ψ x)"
| "models_ltlp (φ Up ψ) = models_ltlp φ suntil models_ltlp ψ"
| "models_ltlp (Xp φ) = nxt (models_ltlp φ)"

lemma models_ltlp_correct:
  "models_ltlp φ xs ⟷ to_omega xs ⊨p φ"
  by (induction φ arbitrary: xs; simp add: suntil_iff_sdrop)

definition
  "models_ltlc φ xs = to_omega xs ⊨c' φ"

lemma models_ltlc_alt_def:
  "models_ltlc φ = models_ltlp (ltlc_to_pltl φ)"
  unfolding models_ltlc_def models_ltlp_correct by simp

theorem ctl_to_state_correct:
  "models_ctl φ = models_state (ctl_to_state φ)"
  by (induction φ) (simp add: Alw_alw_def Alw_ev_def Ex_ev_def Ex_alw_def)+

theorem ltlp_to_path_correct:
  "models_ltlp φ = models_path (ltlp_to_path φ)"
  by (induction φ; simp)

end

context Bisimulation_Invariant
begin

context
  includes lifting_syntax
begin

abbreviation compatible where
  "compatible ≡ A_B.equiv' ===> (=)"

abbreviation (input)
  "compatible_op ≡ compatible ===> compatible"

abbreviation
  "compatible_path ≡ stream_all2 A_B.equiv' ===> (=)"

named_theorems compatible

lemma compatible_opI:
  assumes "⋀φ ψ. compatible φ ψ ⟹ compatible (Φ φ) (Ψ ψ)"
  shows "compatible_op Φ Ψ"
  using assms unfolding rel_fun_def by auto

lemma compatible_opE:
  assumes "compatible_op Φ Ψ" "compatible φ ψ"
  shows "compatible (Φ φ) (Ψ ψ)"
  using assms unfolding rel_fun_def by auto

lemma Ex_ev_compatible[compatible, transfer_rule]:
  "compatible_op A.Ex_ev B.Ex_ev"
  using Ex_ev_iff unfolding rel_fun_def by blast

lemma Alw_ev_compatible[compatible, transfer_rule]:
  "compatible_op A.Alw_ev B.Alw_ev"
  using Alw_ev_iff unfolding rel_fun_def by blast

lemma Not_compatible[compatible]:
  "compatible_op ((∘) Not) ((∘) Not)"
  unfolding rel_fun_def by simp

lemma compatible_op_compI:
  assumes [transfer_rule]: "compatible_op Φ Ψ" "compatible_op Φ' Ψ'"
  shows "compatible_op (Φ o Φ') (Ψ o Ψ')"
  by transfer_prover

lemma compatible_op_NotI:
  assumes "compatible_op Φ Ψ"
  shows "compatible_op (λφ x. ¬ Φ φ x) (λψ x. ¬ Ψ ψ x)"
  by (rule compatible_op_compI[unfolded comp_def],
      rule Not_compatible[unfolded comp_def], rule assms)

lemma
  shows Alw_alw_compatible[compatible, transfer_rule]: "compatible_op A.Alw_alw B.Alw_alw"
    and Ex_alw_compatible[compatible, transfer_rule]:  "compatible_op A.Ex_alw B.Ex_alw"
  unfolding Graph_Defs.Alw_alw_iff Graph_Defs.Ex_alw_iff
  by (rule compatible_op_NotI, rule compatible_op_compI[unfolded comp_def]; (rule compatible))+

lemma conj_compatible:
  "(compatible ===> compatible ===> compatible) (λφ φ' x. φ x ∧ φ' x) (λψ ψ' x. ψ x ∧ ψ' x)"
  by transfer_prover

lemma implies_compatible:
  "(compatible ===> compatible ===> compatible) (λφ φ' x. φ x ⟶ φ' x) (λψ ψ' x. ψ x ⟶ ψ' x)"
  by transfer_prover

lemma disj_compatible:
  "(compatible ===> compatible ===> compatible) (λφ φ' x. φ x ∨ φ' x) (λψ ψ' x. ψ x ∨ ψ' x)"
  by transfer_prover

lemma Leadsto_compatible:
  "(compatible ===> compatible ===> compatible) A.leadsto B.leadsto"
  unfolding A.leadsto_def B.leadsto_def by transfer_prover

lemmas [compatible] = implies_compatible[THEN rel_funD]

definition
  "protect x = x"

lemma protect_cong[cong]:
  "protect x = protect x"
  unfolding protect_def ..

lemmas [compatible] = Not_compatible[unfolded comp_def]

lemma CTL_compatible:
  assumes "rel_ctl_formula compatible φ ψ"
  shows "compatible (A.models_ctl φ) (B.models_ctl ψ)"
  using assms by induction (simp; rule compatible_opE, rule compatible, assumption)+

lemma ctl_star_compatible_aux:
  "(rel_state_formula compatible φ φ' ⟶ compatible (A.models_state φ) (B.models_state φ'))
∧ (rel_path_formula compatible ψ ψ' ⟶ compatible_path (A.models_path ψ) (B.models_path ψ'))"
proof (induction rule: state_formula_path_formula.rel_induct)
  case (All a b) ― ‹State›
  then show ?case
    by - (drule holds_transfer[THEN rel_funD], unfold A.models_path.simps B.models_path.simps)
next
  case (ImpliesS a b) ― ‹All›
  then show ?case
    apply simp
    apply (intro rel_funI allI iffI impI)
     apply (auto 4 4
        dest!: B_A.simulation_run stream_all2_rotate_1 dest: rel_funD elim: equiv'_rotate_1; fail)
    by (auto 4 4 dest!: A_B.simulation_run dest: rel_funD)
next
  case (NotS a12 b12) ― ‹Ex›
  then show ?case
    apply simp
    apply (intro rel_funI allI iffI impI)
     apply (smt A_B.simulation_run rel_fun_def stream.rel_sel stream.sel(1) stream.sel(2))
    by (smt B_A.simulation_run equiv'_rotate_1 rel_fun_def stream.rel_inject stream_all2_rotate_1)
next
  case (Until a22 b22) ― ‹F›
  then show ?case
    by - (drule ev_transfer[THEN rel_funD], unfold A.models_path.simps B.models_path.simps)
next
  case (X a b) ― ‹G›
  then show ?case
    by - (drule alw_transfer[THEN rel_funD], unfold A.models_path.simps B.models_path.simps)
next
  case (ImpliesP a b) ― ‹X›
  then show ?case
    by - (drule nxt_transfer[THEN rel_funD], unfold A.models_path.simps B.models_path.simps)
next
  case (NotP a22 b22) ― ‹Until›
  then show ?case
    by - (drule suntil_transfer[THEN rel_funD, THEN rel_funD],
          unfold A.models_path.simps B.models_path.simps)
qed (simp add: rel_fun_def; fail | auto; fail)+

lemmas models_state_compatible = ctl_star_compatible_aux[THEN conjunct1, rule_format]
   and models_path_compatible  = ctl_star_compatible_aux[THEN conjunct2, rule_format]

lemma
  "(compatible_path ===> compatible_path) alw alw"
  by (rule alw_transfer)

lemma
  "(compatible_path ===> compatible_path) ev ev"
  by (rule ev_transfer)

lemma holds_compatible:
  "(compatible ===> compatible_path) holds holds"
  by (rule holds_transfer)

lemma models_ltlp_compatible:
  assumes "rel_pltl compatible ψ ψ'"
  shows "compatible_path (A.models_ltlp ψ) (B.models_ltlp ψ')"
  by (metis assms
      A.ltlp_to_path_correct B.ltlp_to_path_correct models_path_compatible rel_ltlp_to_path)

lemma models_ltlc_compatible:
  assumes "rel_ltlc compatible ψ ψ'"
  shows "compatible_path (A.models_ltlc ψ) (B.models_ltlc ψ')"
  using assms unfolding A.models_ltlc_alt_def
  by (intro models_ltlp_compatible) (simp only: rel_ltlc_to_pltl)

end (* Transfer Syntax *)

end (* Bisimulation Invariant *)

lemmas [simp del] = holds.simps

end (* Theory *)