Quellcode-Bibliothek LiveIOA.thy
Sprache: unbekannt
(* Title: HOL/HOLCF/IOA/LiveIOA.thy Author: Olaf Müller \<open>Live I/O automata -- specified by temproal formulas\<close> theory LiveIOAimports TLSbegin 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 \ \<and> out (fst CL) = out (fst AM) \<and> \<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 \ \<and> \<forall>exec \<in> executions (fst CL). (exec \<TTurnstile> (snd CL)) \<longrightarrow> \<TTurnstile> snd AM))" lemma live_implements_trans:"live_implements (A, LA) (B, LB) \ live_implements (B, LB) (C, LC) \ " by (auto simp: live_implements_def)\<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 autoapply (rule_tac x = "corresp_ex A f ex" in exI)apply autotext \<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 quality 100%
[ 0.3Quellennavigators
Projekt
]
2026-03-28
