Theory LTL_Compat

theory LTL_Compat
imports LTL LTL_FGXU
(*  
    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 truen = true"
| "ltln_to_ltl falsen = false"
| "ltln_to_ltl propn(q) = p(q)"
| "ltln_to_ltl npropn(q) = np(q)"
| "ltln_to_ltl (φ andn ψ) = ltln_to_ltl φ and ltln_to_ltl ψ"
| "ltln_to_ltl (φ orn ψ) = ltln_to_ltl φ or ltln_to_ltl ψ"
| "ltln_to_ltl (φ Un ψ) = (if φ = truen then F (ltln_to_ltl ψ) else (ltln_to_ltl φ) U (ltln_to_ltl ψ))"
| "ltln_to_ltl (φ Rn ψ) = (if φ = falsen then G (ltln_to_ltl ψ) else (ltln_to_ltl φ) R (ltln_to_ltl ψ))"
| "ltln_to_ltl (φ Wn ψ) = (if ψ = falsen then G (ltln_to_ltl φ) else (ltln_to_ltl φ) W (ltln_to_ltl ψ))"
| "ltln_to_ltl (φ Mn ψ) = (if ψ = truen then F (ltln_to_ltl φ) else (ltln_to_ltl φ) M (ltln_to_ltl ψ))"
| "ltln_to_ltl (Xn φ) = 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 (φ andn ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ orn ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ Un ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ Rn ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ Wn ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (φ Mn ψ) = List.union (atoms_list φ) (atoms_list ψ)"
| "atoms_list (Xn φ) = atoms_list φ"
| "atoms_list (propn(a)) = [a]"
| "atoms_list (npropn(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