src/HOL/IOA/IOA.thy
changeset 62145 5b946c81dfbf
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
     1.1 --- a/src/HOL/IOA/IOA.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/IOA/IOA.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -15,183 +15,148 @@
     1.4  type_synonym ('a, 's) transition = "('s * 'a * 's)"
     1.5  type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
     1.6  
     1.7 -consts
     1.8 +(* IO automata *)
     1.9 +
    1.10 +definition state_trans :: "['action signature, ('action,'state)transition set] => bool"
    1.11 +  where "state_trans asig R ==
    1.12 +     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
    1.13 +     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
    1.14 +
    1.15 +definition asig_of :: "('action,'state)ioa => 'action signature"
    1.16 +  where "asig_of == fst"
    1.17  
    1.18 -  (* IO automata *)
    1.19 -  state_trans::"['action signature, ('action,'state)transition set] => bool"
    1.20 -  asig_of    ::"('action,'state)ioa => 'action signature"
    1.21 -  starts_of  ::"('action,'state)ioa => 'state set"
    1.22 -  trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
    1.23 -  IOA        ::"('action,'state)ioa => bool"
    1.24 +definition starts_of :: "('action,'state)ioa => 'state set"
    1.25 +  where "starts_of == (fst o snd)"
    1.26 +
    1.27 +definition trans_of :: "('action,'state)ioa => ('action,'state)transition set"
    1.28 +  where "trans_of == (snd o snd)"
    1.29  
    1.30 -  (* Executions, schedules, and traces *)
    1.31 +definition IOA :: "('action,'state)ioa => bool"
    1.32 +  where "IOA(ioa) == (is_asig(asig_of(ioa)) &
    1.33 +                (~ starts_of(ioa) = {}) &
    1.34 +                state_trans (asig_of ioa) (trans_of ioa))"
    1.35 +
    1.36 +
    1.37 +(* Executions, schedules, and traces *)
    1.38  
    1.39 -  is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
    1.40 -  has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
    1.41 -  executions    :: "('action,'state)ioa => ('action,'state)execution set"
    1.42 -  mk_trace  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
    1.43 -  reachable     :: "[('action,'state)ioa, 'state] => bool"
    1.44 -  invariant     :: "[('action,'state)ioa, 'state=>bool] => bool"
    1.45 -  has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
    1.46 -  traces    :: "('action,'state)ioa => 'action oseq set"
    1.47 -  NF            :: "'a oseq => 'a oseq"
    1.48 +(* An execution fragment is modelled with a pair of sequences:
    1.49 +   the first is the action options, the second the state sequence.
    1.50 +   Finite executions have None actions from some point on. *)
    1.51 +definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool"
    1.52 +  where "is_execution_fragment A ex ==
    1.53 +     let act = fst(ex); state = snd(ex)
    1.54 +     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
    1.55 +              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
    1.56 +
    1.57 +definition executions :: "('action,'state)ioa => ('action,'state)execution set"
    1.58 +  where "executions(ioa) == {e. snd e 0:starts_of(ioa) & is_execution_fragment ioa e}"
    1.59  
    1.60 -  (* Composition of action signatures and automata *)
    1.61 +
    1.62 +definition reachable :: "[('action,'state)ioa, 'state] => bool"
    1.63 +  where "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
    1.64 +
    1.65 +definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
    1.66 +  where "invariant A P == (!s. reachable A s --> P(s))"
    1.67 +
    1.68 +
    1.69 +(* Composition of action signatures and automata *)
    1.70 +
    1.71 +consts
    1.72    compatible_asigs ::"('a => 'action signature) => bool"
    1.73    asig_composition ::"('a => 'action signature) => 'action signature"
    1.74    compatible_ioas  ::"('a => ('action,'state)ioa) => bool"
    1.75    ioa_composition  ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
    1.76  
    1.77 -  (* binary composition of action signatures and automata *)
    1.78 -  compat_asigs ::"['action signature, 'action signature] => bool"
    1.79 -  asig_comp    ::"['action signature, 'action signature] => 'action signature"
    1.80 -  compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
    1.81 -  par         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
    1.82 +
    1.83 +(* binary composition of action signatures and automata *)
    1.84  
    1.85 -  (* Filtering and hiding *)
    1.86 -  filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"
    1.87 +definition compat_asigs ::"['action signature, 'action signature] => bool"
    1.88 +  where "compat_asigs a1 a2 ==
    1.89 +   (((outputs(a1) Int outputs(a2)) = {}) &
    1.90 +    ((internals(a1) Int actions(a2)) = {}) &
    1.91 +    ((internals(a2) Int actions(a1)) = {}))"
    1.92  
    1.93 -  restrict_asig :: "['a signature, 'a set] => 'a signature"
    1.94 -  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
    1.95 +definition compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
    1.96 +  where "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
    1.97  
    1.98 -  (* Notions of correctness *)
    1.99 -  ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
   1.100 -
   1.101 -  (* Instantiation of abstract IOA by concrete actions *)
   1.102 -  rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
   1.103 +definition asig_comp :: "['action signature, 'action signature] => 'action signature"
   1.104 +  where "asig_comp a1 a2 ==
   1.105 +      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
   1.106 +        (outputs(a1) Un outputs(a2)),
   1.107 +        (internals(a1) Un internals(a2))))"
   1.108  
   1.109 -defs
   1.110 -
   1.111 -state_trans_def:
   1.112 -  "state_trans asig R ==
   1.113 -     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
   1.114 -     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
   1.115 +definition par :: "[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
   1.116 +  where "(ioa1 || ioa2) ==
   1.117 +     (asig_comp (asig_of ioa1) (asig_of ioa2),
   1.118 +      {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
   1.119 +      {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
   1.120 +           in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
   1.121 +              (if a:actions(asig_of(ioa1)) then
   1.122 +                 (fst(s),a,fst(t)):trans_of(ioa1)
   1.123 +               else fst(t) = fst(s))
   1.124 +              &
   1.125 +              (if a:actions(asig_of(ioa2)) then
   1.126 +                 (snd(s),a,snd(t)):trans_of(ioa2)
   1.127 +               else snd(t) = snd(s))})"
   1.128  
   1.129  
   1.130 -asig_of_def:   "asig_of == fst"
   1.131 -starts_of_def: "starts_of == (fst o snd)"
   1.132 -trans_of_def:  "trans_of == (snd o snd)"
   1.133 -
   1.134 -ioa_def:
   1.135 -  "IOA(ioa) == (is_asig(asig_of(ioa))      &
   1.136 -                (~ starts_of(ioa) = {})    &
   1.137 -                state_trans (asig_of ioa) (trans_of ioa))"
   1.138 -
   1.139 -
   1.140 -(* An execution fragment is modelled with a pair of sequences:
   1.141 - * the first is the action options, the second the state sequence.
   1.142 - * Finite executions have None actions from some point on.
   1.143 - *******)
   1.144 -is_execution_fragment_def:
   1.145 -  "is_execution_fragment A ex ==
   1.146 -     let act = fst(ex); state = snd(ex)
   1.147 -     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
   1.148 -              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
   1.149 -
   1.150 -
   1.151 -executions_def:
   1.152 -  "executions(ioa) == {e. snd e 0:starts_of(ioa) &
   1.153 -                        is_execution_fragment ioa e}"
   1.154 -
   1.155 -
   1.156 -reachable_def:
   1.157 -  "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
   1.158 -
   1.159 -
   1.160 -invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
   1.161 -
   1.162 +(* Filtering and hiding *)
   1.163  
   1.164  (* Restrict the trace to those members of the set s *)
   1.165 -filter_oseq_def:
   1.166 -  "filter_oseq p s ==
   1.167 +definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
   1.168 +  where "filter_oseq p s ==
   1.169     (%i. case s(i)
   1.170           of None => None
   1.171            | Some(x) => if p x then Some x else None)"
   1.172  
   1.173 -
   1.174 -mk_trace_def:
   1.175 -  "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
   1.176 -
   1.177 +definition mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
   1.178 +  where "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
   1.179  
   1.180  (* Does an ioa have an execution with the given trace *)
   1.181 -has_trace_def:
   1.182 -  "has_trace ioa b ==
   1.183 -     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
   1.184 +definition has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
   1.185 +  where "has_trace ioa b == (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
   1.186  
   1.187 -normal_form_def:
   1.188 -  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
   1.189 +definition NF :: "'a oseq => 'a oseq"
   1.190 +  where "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
   1.191                      (!j. j ~: range(f) --> nf(j)= None) &
   1.192 -                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
   1.193 +                    (!i. nf(i)=None --> (nf (Suc i)) = None)"
   1.194  
   1.195  (* All the traces of an ioa *)
   1.196 -
   1.197 -  traces_def:
   1.198 -  "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
   1.199 -
   1.200 -(*
   1.201 -  traces_def:
   1.202 -  "traces(ioa) == {tr. has_trace ioa tr}"
   1.203 -*)
   1.204 -
   1.205 -compat_asigs_def:
   1.206 -  "compat_asigs a1 a2 ==
   1.207 -   (((outputs(a1) Int outputs(a2)) = {}) &
   1.208 -    ((internals(a1) Int actions(a2)) = {}) &
   1.209 -    ((internals(a2) Int actions(a1)) = {}))"
   1.210 -
   1.211 -
   1.212 -compat_ioas_def:
   1.213 -  "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
   1.214 +definition traces :: "('action,'state)ioa => 'action oseq set"
   1.215 +  where "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
   1.216  
   1.217  
   1.218 -asig_comp_def:
   1.219 -  "asig_comp a1 a2 ==
   1.220 -      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
   1.221 -        (outputs(a1) Un outputs(a2)),
   1.222 -        (internals(a1) Un internals(a2))))"
   1.223 -
   1.224 -
   1.225 -par_def:
   1.226 -  "(ioa1 || ioa2) ==
   1.227 -       (asig_comp (asig_of ioa1) (asig_of ioa2),
   1.228 -        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
   1.229 -        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
   1.230 -             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
   1.231 -                (if a:actions(asig_of(ioa1)) then
   1.232 -                   (fst(s),a,fst(t)):trans_of(ioa1)
   1.233 -                 else fst(t) = fst(s))
   1.234 -                &
   1.235 -                (if a:actions(asig_of(ioa2)) then
   1.236 -                   (snd(s),a,snd(t)):trans_of(ioa2)
   1.237 -                 else snd(t) = snd(s))})"
   1.238 -
   1.239 -
   1.240 -restrict_asig_def:
   1.241 -  "restrict_asig asig actns ==
   1.242 +definition restrict_asig :: "['a signature, 'a set] => 'a signature"
   1.243 +  where "restrict_asig asig actns ==
   1.244      (inputs(asig) Int actns, outputs(asig) Int actns,
   1.245       internals(asig) Un (externals(asig) - actns))"
   1.246  
   1.247 -
   1.248 -restrict_def:
   1.249 -  "restrict ioa actns ==
   1.250 +definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
   1.251 +  where "restrict ioa actns ==
   1.252      (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
   1.253  
   1.254  
   1.255 -ioa_implements_def:
   1.256 -  "ioa_implements ioa1 ioa2 ==
   1.257 +
   1.258 +(* Notions of correctness *)
   1.259 +
   1.260 +definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
   1.261 +  where "ioa_implements ioa1 ioa2 ==
   1.262    ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
   1.263       (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
   1.264        traces(ioa1) <= traces(ioa2))"
   1.265  
   1.266 -rename_def:
   1.267 -"rename ioa ren ==
   1.268 -  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
   1.269 -    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
   1.270 -    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
   1.271 -              starts_of(ioa)   ,
   1.272 -   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
   1.273 -        in
   1.274 -        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
   1.275 +
   1.276 +(* Instantiation of abstract IOA by concrete actions *)
   1.277 +
   1.278 +definition rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
   1.279 +  where "rename ioa ren ==
   1.280 +    (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
   1.281 +      {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
   1.282 +      {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
   1.283 +                starts_of(ioa)   ,
   1.284 +     {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
   1.285 +          in
   1.286 +          ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
   1.287  
   1.288  
   1.289  declare Let_def [simp]
   1.290 @@ -206,7 +171,7 @@
   1.291  
   1.292  lemma trans_in_actions:
   1.293    "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"
   1.294 -  apply (unfold ioa_def state_trans_def actions_def is_asig_def)
   1.295 +  apply (unfold IOA_def state_trans_def actions_def is_asig_def)
   1.296    apply (erule conjE)+
   1.297    apply (erule allE, erule impE, assumption)
   1.298    apply simp