Theory Example_Instantiation

(*<*)
theory Example_Instantiation
  imports
    Reduction_of_Bisimilarity
begin
(*>*)

chapter ‹Example Instantiation›
text ‹\label{chap:example_instantiation}›

text ‹To complete the proofs from \cref{chap:reductions}, I will show that mappings ‹stabilise› (‹ε(_)›) and ‹in_env› (‹θ?[_](_)›), whose existence we assumed up to now, do, in fact, exist. I will define example mappings and show that, together with these, arbitrary ‹lts_timeout› can be interpreted as ‹lts_timeout_mappable›, thereby showing that the reductions are valid for arbitrary \LTSt{}s.

First, we define the types for $\Proc_\vartheta$ and $\Act_\vartheta$ in dependence on arbitrary types ‹'s› and ‹'a› for $\Proc$ and $\Act$, respectively:›

datatype ('s,'a)Proc_θ = triggered 's | stable ‹'a set› 's | DumpState
datatype ('a)Act_θ = act 'a | t_ε | ε ‹'a set› | DumpAction

text ‹Since $\Act \neq \Act_\vartheta$, we define a new predicate ‹tran_mappable›.›
context lts_timeout begin

inductive tran_mappable
  :: ‹'s ⇒ ('a)Act_θ ⇒ 's ⇒ bool› 
  where ‹tran p α p' ⟹ tran_mappable p (act α) p'›

text ‹We can now specify mappings ‹stabilise› and ‹in_env›, mapping those ‹X› for which $\varepsilon_X$ and $\vartheta_X$ are undefined to the ‹DumpAction›/‹DumpState›.›

function stabilise :: ‹('a)Act_θ set ⇒ ('a)Act_θ›
  where 
    ‹∀ α∈X. (∃ α'. α = act α') ⟹ stabilise X = ε {α' . act α' ∈ X}›
  | ‹∃ α∈X. (∄ α'. α = act α') ⟹ stabilise X = DumpAction› 
  by metis+
termination using "termination" by blast

text ‹\pagebreak›
function in_env :: ‹('a)Act_θ set option ⇒ 's ⇒ ('s,'a)Proc_θ›
  where 
    ‹in_env None p = triggered p›
  | ‹∀ α∈X. (∃ α'. α = act α') ⟹ 
      in_env (Some X) p = stable {α' . act α' ∈ X} p›
  | ‹∃ α∈X. (∄ α'. α = act α') ⟹ 
      in_env (Some X) p = DumpState›
  by (auto, meson Proc_θ.exhaust option.exhaust_sel)
termination using "termination" by blast

text ‹We show that, with these mappings, any ‹lts_timeout› (the context we are in) is an ‹lts_timeout_mappable›: when the variables that were fixed in the locale definition are instantiated by the terms and mappings from the current context, we prove that the assumptions of the locale definition hold. Thus, the reduction works for all \LTSt{}s.›

(* For the following proofs, I gave up on writing readable proofs and simply used what sledgehammer gave me. This is the only part of the the thesis where I do this. I'm ‹sorry›... *)
(*<*)
lemma✐‹tag (proof) unimportant› l1:
  fixes X Y x
  assumes a1: ‹X ⊆ lts_timeout.visible_actions tran_mappable (act τ) (act t)›
  assumes a2: ‹stabilise X = stabilise Y›
  assumes a3: ‹x ∈ X›
  shows ‹x ∈ Y›
proof -
  from a1 have ‹∀ x ∈ X. (∃ α. x = act α)›
    by (smt (verit, best) tau_not_t Act_θ.inject(1) lts_timeout.intro lts_timeout.visible_actions_def mem_Collect_eq subset_iff tran_mappable.cases)
  thus ‹x ∈ Y›
    by (metis (no_types, lifting) Act_θ.distinct(11) Act_θ.inject(2) a2 a3 mem_Collect_eq stabilise.elims)
qed

lemma✐‹tag (proof) unimportant› l2:
  fixes X Y x
  assumes a1: ‹X ⊆ lts_timeout.visible_actions tran_mappable (act τ) (act t)›
  assumes a2: ‹stabilise X = stabilise Y›
  assumes a3: ‹x ∈ Y›
  shows ‹x ∈ X›
proof -
  from a1 have ‹∀ x ∈ X. (∃ α. x = act α)›
    by (smt (verit, best) tau_not_t Act_θ.inject(1) lts_timeout.intro lts_timeout.visible_actions_def mem_Collect_eq subset_iff tran_mappable.cases)
  thus ‹x ∈ X›
    by (metis (no_types, lifting) Act_θ.distinct(11) Act_θ.inject(2) a2 a3 mem_Collect_eq stabilise.elims)
qed
(*>*)
  
lemma is_mappable: ‹lts_timeout_mappable 
  tran_mappable (act τ) (act t) t_ε stabilise in_env›
  apply standard
  apply auto 
  using stabilise.elims tau_not_t apply fastforce
  using stabilise.elims apply blast
  using stabilise.elims apply blast
  apply (metis Act_θ.distinct(7) Act_θ.distinct(9) stabilise.elims)
  using l1 apply blast
  using l2 apply blast 
  apply (metis Proc_θ.distinct(1) Proc_θ.distinct(3) in_env.simps(2) in_env.simps(3))
  apply (metis (no_types, lifting) Proc_θ.distinct(6) Proc_θ.inject(2) l1 in_env.simps(2) in_env.simps(3) stabilise.simps(1) stabilise.simps(2))
  subgoal proof -
    fix X Y p q x
    assume a1: ‹X ⊆ lts_timeout.visible_actions tran_mappable (act τ) (act t)›
    assume a2: ‹in_env (Some X) p = in_env (Some Y) q›
    assume a3: ‹x ∈ Y›

    from a1 have q1: ‹∀ x∈X. (∃ α. x = act α)›
      by (metis empty_iff insert_iff l1 l2 stabilise.simps(2))
    hence p1: ‹in_env (Some X) p = stable {α . act α ∈ X} p›
      using in_env.simps(2) by presburger

    show ‹x ∈ X› proof (cases ‹in_env (Some Y) q = DumpState›)
      case True
      with a2 have ‹in_env (Some X) p = DumpState› by simp
      hence ‹∃ x∈X. (∄ α. x = act α)›
        by (metis Proc_θ.distinct(6) in_env.simps(2))
      with a1 have False
        by (smt (verit, best) tau_not_t Act_θ.inject(1) in_mono lts_timeout.intro lts_timeout.visible_actions_def mem_Collect_eq tran_mappable.cases)
      then show ?thesis ..
    next
      case False
      hence ‹in_env (Some Y) q = stable {α . act α ∈ Y} q›
        by (metis in_env.simps(2) in_env.simps(3))
      hence q2: ‹∀ x∈Y. (∃ α. x = act α)›
        using "False" in_env.simps(3) by blast
      hence p2: ‹in_env (Some Y) q = stable {α . act α ∈ Y} q›
        using in_env.simps(2) by presburger
      with p1 a2 have ‹stable {α . act α ∈ X} p = stable {α . act α ∈ Y} q› by simp
      hence ‹{α . act α ∈ X} = {α . act α ∈ Y}› by force
      with q1 q2 have ‹stabilise X = stabilise Y› by simp
      from l2[OF a1 this a3] show ?thesis .
    qed
  qed
  subgoal proof -
    (* This is an automatically sledgehammer-generated Isar proof in all its beauty... See my apology above...*)
    fix X Y p q
    assume a1: "X ⊆ lts_timeout.visible_actions tran_mappable (act τ) (act t)"
    assume a2: "in_env (Some X) p = in_env (Some Y) q"
    obtain aa where
      f3: "∀A p. aa A ∈ A ∧ (∀a. aa A ≠ act a) ∨ in_env (Some A) p = stable {a. act a ∈ A} p"
      by moura
    obtain pp :: "('a)Act_θ ⇒ ('s ⇒ ('a)Act_θ ⇒ 's ⇒ bool) ⇒ 's" and ppa :: "('a)Act_θ ⇒ ('s ⇒ ('a)Act_θ ⇒ 's ⇒ bool) ⇒ 's" where
      "∀x0 x1. (∃v4 v5. x1 v4 x0 v5) = x1 (pp x0 x1) x0 (ppa x0 x1)"
      by moura
    then have "aa X ∈ X ∧ (∀a. aa X ≠ act a) ⟶ aa X ≠ act τ ∧ aa X ≠ act t ∧ tran_mappable (pp (aa X) tran_mappable) (aa X) (ppa (aa X) tran_mappable)"
      using a1
      by (smt (verit, ccfv_threshold) Act_θ.inject(1) lts_timeout.intro lts_timeout.visible_actions_def mem_Collect_eq subsetD tau_not_t)
    then have f4: "in_env (Some X) p = stable {a. act a ∈ X} p"
      using f3 by (meson tran_mappable.cases)
    then have "in_env (Some Y) q ≠ DumpState"
      using a2 by (metis Proc_θ.distinct(6))
    then have "in_env (Some Y) q = stable {a. act a ∈ Y} q"
      using f3 by (meson in_env.simps(3))
    then show ‹p = q›
      using f4 a2 by (metis (no_types) Proc_θ.inject(2))
  qed
  apply (metis Act_θ.distinct(4) Act_θ.simps(8) stabilise.elims tran_mappable.simps)
  apply (simp add: tran_mappable.simps)
  done

end ― ‹of ‹context lts_timeout››


subsubsection ‹A Tiny Example \LTSt{}›

text ‹\lts{
    \node[state]    (p0)                            {$p_0$};
    \node[state]    (p1) [below left of=p0]         {$p_1$};
    \node[state]    (p2) [below right of=p0]        {$p_2$};
    \node[state]    (q0) [right of=p0,xshift=3cm]   {$q_0$};
    \node[state]    (q1) [below of=q0]         {$q_1$};
    
    \path   (p0) edge node[above left]  {$\tau$}(p1)
                 edge node              {$t$}   (p2)
            (q0) edge node[above left]  {$\tau$}(q1);
}›

datatype Proc = p0|p1|p2|q0|q1
datatype Act = τ|t
inductive Tran :: ‹Proc ⇒ Act ⇒ Proc ⇒ bool›
  where 
    ‹Tran p0 τ p1›
  | ‹Tran p0 t p2›
  | ‹Tran q0 τ q1›

text ‹We interpret the ‹Tran› predicate as an ‹lts_timeout›, and then together with our mappings as an ‹lts_timeout_mappable›.›

interpretation✐‹tag (proof) visible› tiny_lts: 
  lts_timeout Tran τ t
  by (simp add: lts_timeout.intro)
interpretation✐‹tag (proof) visible› tiny_lts_mappable: 
  lts_timeout_mappable tiny_lts.tran_mappable ‹act τ› ‹act t› ‹t_ε› 
  tiny_lts.stabilise tiny_lts.in_env 
  using tiny_lts.is_mappable .
― ‹(notation assignments omitted from thesis document)›

(*<*)
notation tiny_lts.tran_mappable ("_ ⟼_ _" [70, 70, 70] 80)
notation tiny_lts.stabilise (‹ε[_]›) 
notation tiny_lts_mappable.triggered_env (‹θ'(_')›)
notation tiny_lts_mappable.stable_env (‹θ[_]'(_')›)
notation tiny_lts_mappable.strongly_reactive_bisimilar (‹_ ↔⇩_r _› [70, 70] 70)
notation tiny_lts_mappable.strongly_X_bisimilar (‹_ ↔⇩_r⇧_ _› [70, 70, 70] 70)
notation tiny_lts_mappable.tran_theta (‹_ ⟼⇧^θ_ _› [70, 70, 70] 70)
abbreviation strongly_bisimilar_theta 
  (‹_ ↔ _› [70, 70] 70)
  where ‹strongly_bisimilar_theta ≡ lts.strongly_bisimilar tiny_lts_mappable.tran_theta›
abbreviation idle 
  where ‹idle ≡ tiny_lts_mappable.idle›
(*>*)

text ‹We can now prove a few lemmas about our example \LTSt{} that we would need for any bisimilarity proofs. I abstained from actually including a bisimilarity proof, but these lemmas should, hopefully, suffice to convince you that it would be possible.›

lemma✐‹tag (proof) visible› ‹tiny_lts_mappable.visible_actions = ∅› 
proof -
  have ‹tiny_lts.visible_actions = ∅›
    using tiny_lts.visible_actions_def 
      Act.exhaust Collect_cong empty_def
    by auto
  moreover have ‹tiny_lts_mappable.visible_actions 
      = image (λ α. act α) tiny_lts.visible_actions›
    using Act.exhaust 
      tiny_lts.tran_mappable.simps 
      tiny_lts.visible_actions_def 
      tiny_lts_mappable.visible_actions_def 
    by auto
  ultimately show ?thesis by force
qed

lemma✐‹tag (proof) visible› ‹∄ P'. θ[∅](p0) ⟼⇧^θ(act t) P'›
proof safe
  fix P'
  assume ‹θ[∅](p0) ⟼⇧^θ(act t) P'›
  hence ‹idle p0 ∅› 
    using tiny_lts_mappable.generation_sys_timeout by blast

  have ‹p0 ⟼(act τ) p1› using Tran.intros(1)
    by (simp add: tiny_lts.tran_mappable.intros)

  with ‹idle p0 ∅› show False 
    unfolding tiny_lts_mappable.initial_actions_def by blast
qed

(*<*)
end ― ‹of ‹theory››
(*>*)