Quellcode-Bibliothek LiveIOA.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/LiveIOA.thy
    Author:     Olaf Müller
*)

section \<open>Live I/O automata -- specified by temproal formulas\<close>

theory LiveIOA
imports TLS
begin

default_sort type

type_synonym ('a, 's) live_ioa = "('a, 's)ioa \ ('a, 's) ioa_temp"

definition validLIOA :: "('a, 's) live_ioa \ ('a, 's) ioa_temp \ bool"
  where "validLIOA AL P \ validIOA (fst AL) (snd AL \<^bold>\ P)"

definition WF :: "('a, 's) ioa \ 'a set \ ('a, 's) ioa_temp"
  where "WF A acts = (\\\\(s,a,t). Enabled A acts s\ \<^bold>\ \\\xt2 (plift (\a. a \ acts))\)"

definition SF :: "('a, 's) ioa \ 'a set \ ('a, 's) ioa_temp"
  where "SF A acts = (\\\\(s,a,t). Enabled A acts s\ \<^bold>\ \\\xt2 (plift (\a. a \ acts))\)"

definition liveexecutions :: "('a, 's) live_ioa \ ('a, 's) execution set"
  where "liveexecutions AP = {exec. exec \ executions (fst AP) \ (exec \ snd AP)}"

definition livetraces :: "('a, 's) live_ioa \ 'a trace set"
  where "livetraces AP = {mk_trace (fst AP) \ (snd ex) |ex. ex \ liveexecutions AP}"

definition live_implements :: "('a, 's1) live_ioa \ ('a, 's2) live_ioa \ bool"
  where "live_implements CL AM \
    inp (fst CL) = inp (fst AM) \<and> out (fst CL) = out (fst AM) \<and>
      livetraces CL \<subseteq> livetraces AM"

definition is_live_ref_map :: "('s1 \ 's2) \ ('a, 's1) live_ioa \ ('a, 's2) live_ioa \ bool"
  where "is_live_ref_map f CL AM \
    is_ref_map f (fst CL ) (fst AM) \<and>
    (\<forall>exec \<in> executions (fst CL). (exec \<TTurnstile> (snd CL)) \<longrightarrow>
      (corresp_ex (fst AM) f exec \<TTurnstile> snd AM))"

lemma live_implements_trans:
  "live_implements (A, LA) (B, LB) \ live_implements (B, LB) (C, LC) \
    live_implements (A, LA) (C, LC)"
  by (auto simp: live_implements_def)

subsection \<open>Correctness of live refmap\<close>

lemma live_implements:
  "inp C = inp A \ out C = out A \ is_live_ref_map f (C, M) (A, L)
    \<Longrightarrow> live_implements (C, M) (A, L)"
  apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
  apply auto
  apply (rule_tac x = "corresp_ex A f ex" in exI)
  apply auto
  text \<open>Traces coincide, Lemma 1\<close>
  apply (pair ex)
  apply (erule lemma_1 [THEN spec, THEN mp])
  apply (simp (no_asm) add: externals_def)
  apply (auto)[1]
  apply (simp add: executions_def reachable.reachable_0)
  text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
  apply (pair ex)
  apply (simp add: executions_def)
  text \<open>start state\<close>
  apply (rule conjI)
  apply (simp add: is_ref_map_def corresp_ex_def)
  text \<open>\<open>is_execution_fragment\<close>\<close>
  apply (erule lemma_2 [THEN spec, THEN mp])
  apply (simp add: reachable.reachable_0)
  done

end

quality100%

¤ 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.0.10Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.