Theory TLS

theory TLS
imports IOA TL
```(*  Title:      HOL/HOLCF/IOA/TLS.thy
Author:     Olaf MÃ¼ller
*)

section ‹Temporal Logic of Steps -- tailored for I/O automata›

theory TLS
imports IOA TL
begin

default_sort type

type_synonym ('a, 's) ioa_temp  = "('a option, 's) transition temporal"

type_synonym ('a, 's) step_pred = "('a option, 's) transition predicate"

type_synonym 's state_pred = "'s predicate"

definition mkfin :: "'a Seq ⇒ 'a Seq"
where "mkfin s = (if Partial s then SOME t. Finite t ∧ s = t @@ UU else s)"

definition option_lift :: "('a ⇒ 'b) ⇒ 'b ⇒ 'a option ⇒ 'b"
where "option_lift f s y = (case y of None ⇒ s | Some x ⇒ f x)"

definition plift :: "('a ⇒ bool) ⇒ 'a option ⇒ bool"
(* plift is used to determine that None action is always false in
transition predicates *)
where "plift P = option_lift P False"

definition xt1 :: "'s predicate ⇒ ('a, 's) step_pred"
where "xt1 P tr = P (fst tr)"

definition xt2 :: "'a option predicate ⇒ ('a, 's) step_pred"
where "xt2 P tr = P (fst (snd tr))"

definition ex2seqC :: "('a, 's) pairs → ('s ⇒ ('a option, 's) transition Seq)"
where "ex2seqC =
(fix ⋅ (LAM h ex. (λs. case ex of
nil ⇒ (s, None, s) ↝ nil
| x ## xs ⇒ (flift1 (λpr. (s, Some (fst pr), snd pr) ↝ (h ⋅ xs) (snd pr)) ⋅ x))))"

definition ex2seq :: "('a, 's) execution ⇒ ('a option, 's) transition Seq"
where "ex2seq ex = (ex2seqC ⋅ (mkfin (snd ex))) (fst ex)"

definition temp_sat :: "('a, 's) execution ⇒ ('a, 's) ioa_temp ⇒ bool"  (infixr "⊫" 22)
where "(ex ⊫ P) ⟷ ((ex2seq ex) ⊨ P)"

definition validTE :: "('a, 's) ioa_temp ⇒ bool"
where "validTE P ⟷ (∀ex. (ex ⊫ P))"

definition validIOA :: "('a, 's) ioa ⇒ ('a, 's) ioa_temp ⇒ bool"
where "validIOA A P ⟷ (∀ex ∈ executions A. (ex ⊫ P))"

lemma IMPLIES_temp_sat [simp]: "(ex ⊫ P ❙⟶ Q) ⟷ ((ex ⊫ P) ⟶ (ex ⊫ Q))"
by (simp add: IMPLIES_def temp_sat_def satisfies_def)

lemma AND_temp_sat [simp]: "(ex ⊫ P ❙∧ Q) ⟷ ((ex ⊫ P) ∧ (ex ⊫ Q))"
by (simp add: AND_def temp_sat_def satisfies_def)

lemma OR_temp_sat [simp]: "(ex ⊫ P ❙∨ Q) ⟷ ((ex ⊫ P) ∨ (ex ⊫ Q))"
by (simp add: OR_def temp_sat_def satisfies_def)

lemma NOT_temp_sat [simp]: "(ex ⊫ ❙¬ P) ⟷ (¬ (ex ⊫ P))"
by (simp add: NOT_def temp_sat_def satisfies_def)

axiomatization
where mkfin_UU [simp]: "mkfin UU = nil"
and mkfin_nil [simp]: "mkfin nil = nil"
and mkfin_cons [simp]: "mkfin (a ↝ s) = a ↝ mkfin s"

lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex

setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")›

subsection ‹ex2seqC›

lemma ex2seqC_unfold:
"ex2seqC =
(LAM ex. (λs. case ex of
nil ⇒ (s, None, s) ↝ nil
| x ## xs ⇒
(flift1 (λpr. (s, Some (fst pr), snd pr) ↝ (ex2seqC ⋅ xs) (snd pr)) ⋅ x)))"
apply (rule trans)
apply (rule fix_eq4)
apply (rule ex2seqC_def)
apply (rule beta_cfun)
done

lemma ex2seqC_UU [simp]: "(ex2seqC ⋅ UU) s = UU"
apply (subst ex2seqC_unfold)
apply simp
done

lemma ex2seqC_nil [simp]: "(ex2seqC ⋅ nil) s = (s, None, s) ↝ nil"
apply (subst ex2seqC_unfold)
apply simp
done

lemma ex2seqC_cons [simp]: "(ex2seqC ⋅ ((a, t) ↝ xs)) s = (s, Some a,t ) ↝ (ex2seqC ⋅ xs) t"
apply (rule trans)
apply (subst ex2seqC_unfold)
done

lemma ex2seq_UU: "ex2seq (s, UU) = (s, None, s) ↝ nil"

lemma ex2seq_nil: "ex2seq (s, nil) = (s, None, s) ↝ nil"

lemma ex2seq_cons: "ex2seq (s, (a, t) ↝ ex) = (s, Some a, t) ↝ ex2seq (t, ex)"

declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]

lemma ex2seq_nUUnnil: "ex2seq exec ≠ UU ∧ ex2seq exec ≠ nil"
apply (pair exec)
apply (Seq_case_simp x2)
apply (pair a)
done

subsection ‹Interface TL -- TLS›

(* uses the fact that in executions states overlap, which is lost in
after the translation via ex2seq !! *)

lemma TL_TLS:
"∀s a t. (P s) ∧ s ─a─A→ t ⟶ (Q t)
⟹ ex ⊫ (Init (λ(s, a, t). P s) ❙∧ Init (λ(s, a, t). s ─a─A→ t)
❙⟶ (○(Init (λ(s, a, t). Q s))))"
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
apply clarify
apply (simp split: if_split)
text ‹‹TL = UU››
apply (rule conjI)
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
text ‹‹TL = nil››
apply (rule conjI)
apply (pair ex)
apply (Seq_case x2)
apply fast
apply fast
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
text ‹‹TL = cons››