Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: TLS.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.