src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
changeset 62004 8c6226d88ced
parent 62002 f1599e98c4d0
equal deleted inserted replaced
62003:ba465fcd0267 62004:8c6226d88ced
    17   validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
    17   validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
    18   "validLIOA AL P = validIOA (fst AL) ((snd AL) \<^bold>\<longrightarrow> P)"
    18   "validLIOA AL P = validIOA (fst AL) ((snd AL) \<^bold>\<longrightarrow> P)"
    19 
    19 
    20 definition
    20 definition
    21   WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    21   WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    22   "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
    22   "WF A acts = (\<diamond>\<box>\<langle>%(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (%a. a : acts))\<rangle>)"
    23 definition
    23 definition
    24   SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    24   SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
    25   "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
    25   "SF A acts = (\<box>\<diamond>\<langle>%(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (%a. a : acts))\<rangle>)"
    26 
    26 
    27 definition
    27 definition
    28   liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
    28   liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
    29   "liveexecutions AP = {exec. exec : executions (fst AP) & (exec \<TTurnstile> (snd AP))}"
    29   "liveexecutions AP = {exec. exec : executions (fst AP) & (exec \<TTurnstile> (snd AP))}"
    30 definition
    30 definition