(* Title: HOL/HOLCF/IOA/TLS.thy
Author: Olaf Müller
*)
section \<open>Temporal Logic of Steps -- tailored for I/O automata\<close>
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 \<cdot> (LAM h ex. (\<lambda>s. case ex of
nil \<Rightarrow> (s, None, s) \<leadsto> nil
| x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h \<cdot> xs) (snd pr)) \<cdot> 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 \<^bold>\ Q) \ ((ex \ P) \ (ex \ Q))"
by (simp add: IMPLIES_def temp_sat_def satisfies_def)
lemma AND_temp_sat [simp]: "(ex \ P \<^bold>\ Q) \ ((ex \ P) \ (ex \ Q))"
by (simp add: AND_def temp_sat_def satisfies_def)
lemma OR_temp_sat [simp]: "(ex \ P \<^bold>\ Q) \ ((ex \ P) \ (ex \ Q))"
by (simp add: OR_def temp_sat_def satisfies_def)
lemma NOT_temp_sat [simp]: "(ex \ \<^bold>\ 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 \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
subsection \<open>ex2seqC\<close>
lemma ex2seqC_unfold:
"ex2seqC =
(LAM ex. (\<lambda>s. case ex of
nil \<Rightarrow> (s, None, s) \<leadsto> nil
| x ## xs \<Rightarrow>
(flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC \<cdot> xs) (snd pr)) \<cdot> x)))"
apply (rule trans)
apply (rule fix_eq4)
apply (rule ex2seqC_def)
apply (rule beta_cfun)
apply (simp add: flift1_def)
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)
apply (simp add: Consq_def flift1_def)
apply (simp add: Consq_def flift1_def)
done
lemma ex2seq_UU: "ex2seq (s, UU) = (s, None, s) \ nil"
by (simp add: ex2seq_def)
lemma ex2seq_nil: "ex2seq (s, nil) = (s, None, s) \ nil"
by (simp add: ex2seq_def)
lemma ex2seq_cons: "ex2seq (s, (a, t) \ ex) = (s, Some a, t) \ ex2seq (t, ex)"
by (simp add: ex2seq_def)
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 \<open>Interface TL -- TLS\<close>
(* 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)
\<Longrightarrow> ex \<TTurnstile> (Init (\<lambda>(s, a, t). P s) \<^bold>\<and> Init (\<lambda>(s, a, t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
\<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(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 \<open>\<open>TL = UU\<close>\<close>
apply (rule conjI)
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
text \<open>\<open>TL = nil\<close>\<close>
apply (rule conjI)
apply (pair ex)
apply (Seq_case x2)
apply (simp add: unlift_def)
apply (simp add: unlift_def)
apply (simp add: unlift_def)
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
text \<open>\<open>TL = cons\<close>\<close>
apply (simp add: unlift_def)
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
done
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
