Theory LTL_Compat

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹LTL Translation Layer›

theory LTL_Compat
  imports Main LTL.LTL "../LTL_FGXU"
begin

― ‹The following infrastructure translates the generic @{datatype ltln} datatype to special structure used in this project›

abbreviation LTLRelease :: "'a ltl ⇒ 'a ltl ⇒ 'a ltl" (‹_ R _› [87,87] 86)
where
  "φ R ψ ≡ (G ψ) or (ψ U (φ and ψ))"

abbreviation LTLWeakUntil :: "'a ltl ⇒ 'a ltl ⇒ 'a ltl" (‹_ W _› [87,87] 86)
where
  "φ W ψ ≡ (φ U ψ) or (G φ)"

abbreviation LTLStrongRelease :: "'a ltl ⇒ 'a ltl ⇒ 'a ltl" (‹_ M _› [87,87] 86)
where
  "φ M ψ ≡ ψ U (φ and ψ)"

fun ltln_to_ltl :: "'a ltln ⇒ 'a ltl"
where
  "ltln_to_ltl true⇩n = true"
| "ltln_to_ltl false⇩n = false"
| "ltln_to_ltl prop⇩n(q) = p(q)"
| "ltln_to_ltl nprop⇩n(q) = np(q)"
| "ltln_to_ltl (φ and⇩n ψ) = ltln_to_ltl φ and ltln_to_ltl ψ"
| "ltln_to_ltl (φ or⇩n ψ) = ltln_to_ltl φ or ltln_to_ltl ψ"
| "ltln_to_ltl (φ U⇩n ψ) = (if φ = true⇩n then F (ltln_to_ltl ψ) else (ltln_to_ltl φ) U (ltln_to_ltl ψ))"
| "ltln_to_ltl (φ R⇩n ψ) = (if φ = false⇩n then G (ltln_to_ltl ψ) else (ltln_to_ltl φ) R (ltln_to_ltl ψ))"
| "ltln_to_ltl (φ W⇩n ψ) = (if ψ = false⇩n then G (ltln_to_ltl φ) else (ltln_to_ltl φ) W (ltln_to_ltl ψ))"
| "ltln_to_ltl (φ M⇩n ψ) = (if ψ = true⇩n then F (ltln_to_ltl φ) else (ltln_to_ltl φ) M (ltln_to_ltl ψ))"
| "ltln_to_ltl (X⇩n φ) = X (ltln_to_ltl φ)"

lemma ltln_to_ltl_semantics:
  "w ⊨ ltln_to_ltl φ ⟷ w ⊨⇩n φ"
  by (induction φ arbitrary: w)
     (simp_all del: semantics_ltln.simps(9-11), unfold ltln_Release_alterdef ltln_weak_strong(1) ltl_StrongRelease_Until_con, insert nat_less_le, auto)

lemma ltln_to_ltl_atoms:
  "vars (ltln_to_ltl φ) = atoms_ltln φ"
  by (induction φ) auto

fun atoms_list :: "'a ltln ⇒'a list"
where 
  "atoms_list (φ and⇩n ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ or⇩n ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ U⇩n ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ R⇩n ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ W⇩n ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ M⇩n ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (X⇩n φ) = atoms_list φ"
| "atoms_list (prop⇩n(a)) = [a]"
| "atoms_list (nprop⇩n(a)) = [a]"
| "atoms_list _ = []"

lemma atoms_list_correct:
  "set (atoms_list φ) = atoms_ltln φ"
  by (induction φ) auto

lemma atoms_list_distinct:
  "distinct (atoms_list φ)"
  by (induction φ) auto

end