1(* Title: HOL/HOLCF/IOA/LiveIOA.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Live I/O automata -- specified by temproal formulas\<close> 6 7theory LiveIOA 8imports TLS 9begin 10 11default_sort type 12 13type_synonym ('a, 's) live_ioa = "('a, 's)ioa \<times> ('a, 's) ioa_temp" 14 15definition validLIOA :: "('a, 's) live_ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" 16 where "validLIOA AL P \<longleftrightarrow> validIOA (fst AL) (snd AL \<^bold>\<longrightarrow> P)" 17 18definition WF :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa_temp" 19 where "WF A acts = (\<diamond>\<box>\<langle>\<lambda>(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (\<lambda>a. a \<in> acts))\<rangle>)" 20 21definition SF :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa_temp" 22 where "SF A acts = (\<box>\<diamond>\<langle>\<lambda>(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (\<lambda>a. a \<in> acts))\<rangle>)" 23 24definition liveexecutions :: "('a, 's) live_ioa \<Rightarrow> ('a, 's) execution set" 25 where "liveexecutions AP = {exec. exec \<in> executions (fst AP) \<and> (exec \<TTurnstile> snd AP)}" 26 27definition livetraces :: "('a, 's) live_ioa \<Rightarrow> 'a trace set" 28 where "livetraces AP = {mk_trace (fst AP) \<cdot> (snd ex) |ex. ex \<in> liveexecutions AP}" 29 30definition live_implements :: "('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool" 31 where "live_implements CL AM \<longleftrightarrow> 32 inp (fst CL) = inp (fst AM) \<and> out (fst CL) = out (fst AM) \<and> 33 livetraces CL \<subseteq> livetraces AM" 34 35definition is_live_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool" 36 where "is_live_ref_map f CL AM \<longleftrightarrow> 37 is_ref_map f (fst CL ) (fst AM) \<and> 38 (\<forall>exec \<in> executions (fst CL). (exec \<TTurnstile> (snd CL)) \<longrightarrow> 39 (corresp_ex (fst AM) f exec \<TTurnstile> snd AM))" 40 41lemma live_implements_trans: 42 "live_implements (A, LA) (B, LB) \<Longrightarrow> live_implements (B, LB) (C, LC) \<Longrightarrow> 43 live_implements (A, LA) (C, LC)" 44 by (auto simp: live_implements_def) 45 46 47subsection \<open>Correctness of live refmap\<close> 48 49lemma live_implements: 50 "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_live_ref_map f (C, M) (A, L) 51 \<Longrightarrow> live_implements (C, M) (A, L)" 52 apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def) 53 apply auto 54 apply (rule_tac x = "corresp_ex A f ex" in exI) 55 apply auto 56 text \<open>Traces coincide, Lemma 1\<close> 57 apply (pair ex) 58 apply (erule lemma_1 [THEN spec, THEN mp]) 59 apply (simp (no_asm) add: externals_def) 60 apply (auto)[1] 61 apply (simp add: executions_def reachable.reachable_0) 62 text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close> 63 apply (pair ex) 64 apply (simp add: executions_def) 65 text \<open>start state\<close> 66 apply (rule conjI) 67 apply (simp add: is_ref_map_def corresp_ex_def) 68 text \<open>\<open>is_execution_fragment\<close>\<close> 69 apply (erule lemma_2 [THEN spec, THEN mp]) 70 apply (simp add: reachable.reachable_0) 71 done 72 73end 74