Theory Mapping_for_Formulas

(*<*)
theory Mapping_for_Formulas
  imports
    Mapping_for_Transition_Systems
    HM_Logic
    HM_Logic_with_TimeOuts
begin
(*>*)

section ‹A Mapping for Formulas›
text ‹\label{sec:mapping_formulas}›

text ‹We will now introduce a mapping $\sigma(\cdot)$ that maps formulas of \HMLt{} to formulas of HML, in the context of the process mapping from \cref{sec:mapping_lts}, such that $\vartheta(p)$ satisfies $\sigma(\varphi)$ iff $p$ satisfies $\varphi$.

Again, we have $\mathbb{T} = (\Proc, \Act, \rightarrow)$ and $\mathbb{T}_\vartheta = (\Proc_\vartheta, \Act_\vartheta, \rightarrow_\vartheta)$ as defined in \cref{sec:mapping_lts}, with $A = \Act \!\setminus\! \{\tau, t\}$, and we assume that $t_\varepsilon \notin \Act$ and $\forall X \subseteq A.\; \varepsilon_X \notin \Act$.

Let $\sigma : (\text{\HMLt{} formulas}) \longrightarrow (\text{HML formulas})$ be recursively defined by
\begin{align*}
    \sigma(\textstyle\bigwedge_{i \in I} \varphi_i) =\;& \textstyle\bigwedge_{i \in I} \sigma(\varphi_i) &\\
    \sigma(\neg\varphi) =\;& \neg\,\sigma(\varphi)\\
    \sigma(\langle\tau\rangle\varphi) =\;& \langle\tau\rangle\,\sigma(\varphi)\\
    \sigma(\langle\alpha\rangle\varphi) =\;& 
        \langle\alpha\rangle\,\sigma(\varphi)\;\vee\\
        &\langle\varepsilon_A\rangle\langle\alpha\rangle\,\sigma(\varphi)\;\vee\\ 
        &\langle{}t_\varepsilon\rangle\langle\varepsilon_A\rangle\langle\alpha\rangle\,\sigma(\varphi) && \text{if $\alpha \in A$}\\
    \sigma(\langle\alpha\rangle\varphi) =\;& f\!\!f && \text{if $\alpha \notin A \cup \{\tau\}$}\\
    \sigma(\langle{}X\rangle\varphi) =\;&
        \langle\varepsilon_X\rangle\langle{}t\rangle\,\sigma(\varphi)\;\vee\\
        &\langle{}t_\varepsilon\rangle\langle\varepsilon_X\rangle\langle{}t\rangle\,\sigma(\varphi) && \text{if $X \subseteq A$} \\
    \sigma(\langle{}X\rangle\varphi) =\;& f\!\!f && \text{if $X \not\subseteq A$}
\end{align*}

This mapping simply expresses the time-out semantics given by the satisfaction relations of \HMLt{} (\cref{sec:HMLt}) in terms of ordinary HML evaluated on our mapped LTS $\mathbb{T}_\vartheta$. The disjunctive clauses compensate for the additional environment transitions ($\varepsilon$-actions) that are not present in $\mathbb{T}$.
\pagebreak›


subsection ‹Isabelle›

text ‹The implementation of the mapping in Isabelle is rather straightforward, although some details might not be obvious: 

‹cimage (λ φ. σ(φ)) Φ› is the image of the countable set ‹Φ› under the function ‹λ φ. σ(φ)›, so it corresponds to $\{ \sigma(\varphi) \mid \varphi \in \Phi \}$ for countable $\Phi$.

‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X])› corresponds to $\alpha \in A$ with our assumption about there being no $\varepsilon$-actions in $\Act$. Similarly, \linebreak ‹α = t ∨ α = t_ε ∨ α = ε[X]› corresponds to $\alpha \notin A \cup \{\tau\}$.›

context lts_timeout_mappable begin

function HMt_mapping :: ‹('a)HMLt_formula ⇒ ('a)HML_formula› 
  (‹σ'(_')›)
  where
    ‹σ(HMLt_conj Φ) = HML_conj (cimage (λ φ. σ(φ)) Φ)›
  | ‹σ(HMLt_neg φ) = HML_neg σ(φ)›
  | ‹α = τ ⟹
      σ(HMLt_poss α φ) = HML_poss α σ(φ)›
  | ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X]) ⟹
      σ(HMLt_poss α φ) = HML_disj (acset {
        HML_poss α σ(φ),
        HML_poss ε[visible_actions] (HML_poss α σ(φ)),
        HML_poss t_ε (HML_poss ε[visible_actions] (HML_poss α σ(φ)))
      })›
  | ‹α = t ∨ α = t_ε ∨ α = ε[X] ⟹
      σ(HMLt_poss α φ) = HML_false›
  | ‹X ⊆ visible_actions ⟹
      σ(HMLt_time X φ) = HML_disj (acset {
        HML_poss ε[X] (HML_poss t σ(φ)),
        HML_poss t_ε (HML_poss ε[X] (HML_poss t σ(φ)))
      })›
  | ‹¬ X ⊆ visible_actions ⟹
      σ(HMLt_time X φ) = HML_false›  
  by (metis HMLt_formula.exhaust, auto+, (simp add: distinctness_special_actions(1,2))+, metis distinctness_special_actions(4))

text ‹Again, we show that the function terminates using a well-founded relation.›

inductive_set sigma_wf_rel :: ‹(('a)HMLt_formula) rel› 
  where
    ‹φ ∈⇩c Φ ⟹ (φ, HMLt_conj Φ) ∈ sigma_wf_rel› 
  | ‹(φ, HMLt_neg φ) ∈ sigma_wf_rel› 
  | ‹(φ, HMLt_poss α φ) ∈ sigma_wf_rel› 
  | ‹(φ, HMLt_time X φ) ∈ sigma_wf_rel›

(*<*)
lemma✐‹tag (proof) unimportant› sigma_wf_rel_is_wf: ‹wf sigma_wf_rel› 
  unfolding wf_def
proof (rule allI, rule impI, rule allI)
  fix P::‹('a)HMLt_formula ⇒ bool› and t::‹('a)HMLt_formula›
  assume ‹∀x. (∀y. (y, x) ∈ sigma_wf_rel ⟶ P y) ⟶ P x›
  thus ‹P t›
    apply (induction t)
    apply (metis HMLt_formula.distinct(1,3,5) HMLt_formula.inject(1) sigma_wf_rel.cases cin.rep_eq)
    apply (metis HMLt_formula.distinct(2,8,10) HMLt_formula.inject(2) sigma_wf_rel.cases)
    apply (metis HMLt_formula.distinct(3,7,11) HMLt_formula.inject(3) sigma_wf_rel.cases)
    apply (metis HMLt_formula.distinct(5,9,11) HMLt_formula.inject(4) sigma_wf_rel.cases)
    done
qed
(*>*)


termination HMt_mapping using sigma_wf_rel_is_wf by (standard, (simp add: cin.rep_eq sigma_wf_rel.intros)+)

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