diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/IOA/IOA.thy --- a/src/HOL/IOA/IOA.thy Mon Jan 11 21:20:44 2016 +0100 +++ b/src/HOL/IOA/IOA.thy Mon Jan 11 21:21:02 2016 +0100 @@ -15,183 +15,148 @@ type_synonym ('a, 's) transition = "('s * 'a * 's)" type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set" -consts +(* IO automata *) + +definition state_trans :: "['action signature, ('action,'state)transition set] => bool" + where "state_trans asig R == + (!triple. triple:R --> fst(snd(triple)):actions(asig)) & + (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" + +definition asig_of :: "('action,'state)ioa => 'action signature" + where "asig_of == fst" - (* IO automata *) - state_trans::"['action signature, ('action,'state)transition set] => bool" - asig_of ::"('action,'state)ioa => 'action signature" - starts_of ::"('action,'state)ioa => 'state set" - trans_of ::"('action,'state)ioa => ('action,'state)transition set" - IOA ::"('action,'state)ioa => bool" +definition starts_of :: "('action,'state)ioa => 'state set" + where "starts_of == (fst o snd)" + +definition trans_of :: "('action,'state)ioa => ('action,'state)transition set" + where "trans_of == (snd o snd)" - (* Executions, schedules, and traces *) +definition IOA :: "('action,'state)ioa => bool" + where "IOA(ioa) == (is_asig(asig_of(ioa)) & + (~ starts_of(ioa) = {}) & + state_trans (asig_of ioa) (trans_of ioa))" + + +(* Executions, schedules, and traces *) - is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool" - has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool" - executions :: "('action,'state)ioa => ('action,'state)execution set" - mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq" - reachable :: "[('action,'state)ioa, 'state] => bool" - invariant :: "[('action,'state)ioa, 'state=>bool] => bool" - has_trace :: "[('action,'state)ioa, 'action oseq] => bool" - traces :: "('action,'state)ioa => 'action oseq set" - NF :: "'a oseq => 'a oseq" +(* An execution fragment is modelled with a pair of sequences: + the first is the action options, the second the state sequence. + Finite executions have None actions from some point on. *) +definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool" + where "is_execution_fragment A ex == + let act = fst(ex); state = snd(ex) + in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & + (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))" + +definition executions :: "('action,'state)ioa => ('action,'state)execution set" + where "executions(ioa) == {e. snd e 0:starts_of(ioa) & is_execution_fragment ioa e}" - (* Composition of action signatures and automata *) + +definition reachable :: "[('action,'state)ioa, 'state] => bool" + where "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)" + +definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool" + where "invariant A P == (!s. reachable A s --> P(s))" + + +(* Composition of action signatures and automata *) + +consts compatible_asigs ::"('a => 'action signature) => bool" asig_composition ::"('a => 'action signature) => 'action signature" compatible_ioas ::"('a => ('action,'state)ioa) => bool" ioa_composition ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa" - (* binary composition of action signatures and automata *) - compat_asigs ::"['action signature, 'action signature] => bool" - asig_comp ::"['action signature, 'action signature] => 'action signature" - compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] => bool" - par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "||" 10) + +(* binary composition of action signatures and automata *) - (* Filtering and hiding *) - filter_oseq :: "('a => bool) => 'a oseq => 'a oseq" +definition compat_asigs ::"['action signature, 'action signature] => bool" + where "compat_asigs a1 a2 == + (((outputs(a1) Int outputs(a2)) = {}) & + ((internals(a1) Int actions(a2)) = {}) & + ((internals(a2) Int actions(a1)) = {}))" - restrict_asig :: "['a signature, 'a set] => 'a signature" - restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" +definition compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] => bool" + where "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" - (* Notions of correctness *) - ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" - - (* Instantiation of abstract IOA by concrete actions *) - rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" +definition asig_comp :: "['action signature, 'action signature] => 'action signature" + where "asig_comp a1 a2 == + (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), + (outputs(a1) Un outputs(a2)), + (internals(a1) Un internals(a2))))" -defs - -state_trans_def: - "state_trans asig R == - (!triple. triple:R --> fst(snd(triple)):actions(asig)) & - (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" +definition par :: "[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "||" 10) + where "(ioa1 || ioa2) == + (asig_comp (asig_of ioa1) (asig_of ioa2), + {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, + {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) + in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & + (if a:actions(asig_of(ioa1)) then + (fst(s),a,fst(t)):trans_of(ioa1) + else fst(t) = fst(s)) + & + (if a:actions(asig_of(ioa2)) then + (snd(s),a,snd(t)):trans_of(ioa2) + else snd(t) = snd(s))})" -asig_of_def: "asig_of == fst" -starts_of_def: "starts_of == (fst o snd)" -trans_of_def: "trans_of == (snd o snd)" - -ioa_def: - "IOA(ioa) == (is_asig(asig_of(ioa)) & - (~ starts_of(ioa) = {}) & - state_trans (asig_of ioa) (trans_of ioa))" - - -(* An execution fragment is modelled with a pair of sequences: - * the first is the action options, the second the state sequence. - * Finite executions have None actions from some point on. - *******) -is_execution_fragment_def: - "is_execution_fragment A ex == - let act = fst(ex); state = snd(ex) - in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & - (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))" - - -executions_def: - "executions(ioa) == {e. snd e 0:starts_of(ioa) & - is_execution_fragment ioa e}" - - -reachable_def: - "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)" - - -invariant_def: "invariant A P == (!s. reachable A s --> P(s))" - +(* Filtering and hiding *) (* Restrict the trace to those members of the set s *) -filter_oseq_def: - "filter_oseq p s == +definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq" + where "filter_oseq p s == (%i. case s(i) of None => None | Some(x) => if p x then Some x else None)" - -mk_trace_def: - "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))" - +definition mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq" + where "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))" (* Does an ioa have an execution with the given trace *) -has_trace_def: - "has_trace ioa b == - (? ex:executions(ioa). b = mk_trace ioa (fst ex))" +definition has_trace :: "[('action,'state)ioa, 'action oseq] => bool" + where "has_trace ioa b == (? ex:executions(ioa). b = mk_trace ioa (fst ex))" -normal_form_def: - "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) & +definition NF :: "'a oseq => 'a oseq" + where "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) & (!j. j ~: range(f) --> nf(j)= None) & - (!i. nf(i)=None --> (nf (Suc i)) = None) " + (!i. nf(i)=None --> (nf (Suc i)) = None)" (* All the traces of an ioa *) - - traces_def: - "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}" - -(* - traces_def: - "traces(ioa) == {tr. has_trace ioa tr}" -*) - -compat_asigs_def: - "compat_asigs a1 a2 == - (((outputs(a1) Int outputs(a2)) = {}) & - ((internals(a1) Int actions(a2)) = {}) & - ((internals(a2) Int actions(a1)) = {}))" - - -compat_ioas_def: - "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" +definition traces :: "('action,'state)ioa => 'action oseq set" + where "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}" -asig_comp_def: - "asig_comp a1 a2 == - (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), - (outputs(a1) Un outputs(a2)), - (internals(a1) Un internals(a2))))" - - -par_def: - "(ioa1 || ioa2) == - (asig_comp (asig_of ioa1) (asig_of ioa2), - {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, - {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) - in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & - (if a:actions(asig_of(ioa1)) then - (fst(s),a,fst(t)):trans_of(ioa1) - else fst(t) = fst(s)) - & - (if a:actions(asig_of(ioa2)) then - (snd(s),a,snd(t)):trans_of(ioa2) - else snd(t) = snd(s))})" - - -restrict_asig_def: - "restrict_asig asig actns == +definition restrict_asig :: "['a signature, 'a set] => 'a signature" + where "restrict_asig asig actns == (inputs(asig) Int actns, outputs(asig) Int actns, internals(asig) Un (externals(asig) - actns))" - -restrict_def: - "restrict ioa actns == +definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" + where "restrict ioa actns == (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" -ioa_implements_def: - "ioa_implements ioa1 ioa2 == + +(* Notions of correctness *) + +definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" + where "ioa_implements ioa1 ioa2 == ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) & traces(ioa1) <= traces(ioa2))" -rename_def: -"rename ioa ren == - (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))}, - {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))}, - {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}), - starts_of(ioa) , - {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) - in - ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" + +(* Instantiation of abstract IOA by concrete actions *) + +definition rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" + where "rename ioa ren == + (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))}, + {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))}, + {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}), + starts_of(ioa) , + {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) + in + ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" declare Let_def [simp] @@ -206,7 +171,7 @@ lemma trans_in_actions: "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))" - apply (unfold ioa_def state_trans_def actions_def is_asig_def) + apply (unfold IOA_def state_trans_def actions_def is_asig_def) apply (erule conjE)+ apply (erule allE, erule impE, assumption) apply simp