src/HOL/IOA/IOA.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44066 d74182c93f04
child 58889 5b7a9633cfa8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4530
ac1821645636 corrected Title
oheimb
parents: 3842
diff changeset
     1
(*  Title:      HOL/IOA/IOA.thy
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     2
    Author:     Tobias Nipkow & Konrad Slind
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     3
    Copyright   1994  TU Muenchen
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     4
*)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
     5
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
     6
header {* The I/O automata of Lynch and Tuttle *}
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
     7
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
     8
theory IOA
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
     9
imports Asig
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    10
begin
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    11
42174
d0be2722ce9f modernized specifications;
wenzelm
parents: 36862
diff changeset
    12
type_synonym 'a seq = "nat => 'a"
d0be2722ce9f modernized specifications;
wenzelm
parents: 36862
diff changeset
    13
type_synonym 'a oseq = "nat => 'a option"
d0be2722ce9f modernized specifications;
wenzelm
parents: 36862
diff changeset
    14
type_synonym ('a, 'b) execution = "'a oseq * 'b seq"
d0be2722ce9f modernized specifications;
wenzelm
parents: 36862
diff changeset
    15
type_synonym ('a, 's) transition = "('s * 'a * 's)"
d0be2722ce9f modernized specifications;
wenzelm
parents: 36862
diff changeset
    16
type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    17
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    18
consts
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    19
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    20
  (* IO automata *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    21
  state_trans::"['action signature, ('action,'state)transition set] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    22
  asig_of    ::"('action,'state)ioa => 'action signature"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    23
  starts_of  ::"('action,'state)ioa => 'state set"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    24
  trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    25
  IOA        ::"('action,'state)ioa => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    26
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    27
  (* Executions, schedules, and traces *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    28
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    29
  is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    30
  has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    31
  executions    :: "('action,'state)ioa => ('action,'state)execution set"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    32
  mk_trace  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    33
  reachable     :: "[('action,'state)ioa, 'state] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    34
  invariant     :: "[('action,'state)ioa, 'state=>bool] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    35
  has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    36
  traces    :: "('action,'state)ioa => 'action oseq set"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    37
  NF            :: "'a oseq => 'a oseq"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    38
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    39
  (* Composition of action signatures and automata *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    40
  compatible_asigs ::"('a => 'action signature) => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    41
  asig_composition ::"('a => 'action signature) => 'action signature"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    42
  compatible_ioas  ::"('a => ('action,'state)ioa) => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    43
  ioa_composition  ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    44
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    45
  (* binary composition of action signatures and automata *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    46
  compat_asigs ::"['action signature, 'action signature] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    47
  asig_comp    ::"['action signature, 'action signature] => 'action signature"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    48
  compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    49
  par         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    50
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    51
  (* Filtering and hiding *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    52
  filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    53
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    54
  restrict_asig :: "['a signature, 'a set] => 'a signature"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    55
  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    56
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    57
  (* Notions of correctness *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    58
  ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    59
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    60
  (* Instantiation of abstract IOA by concrete actions *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    61
  rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    62
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    63
defs
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    64
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    65
state_trans_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    66
  "state_trans asig R ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    67
     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    68
     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    69
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    70
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    71
asig_of_def:   "asig_of == fst"
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    72
starts_of_def: "starts_of == (fst o snd)"
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    73
trans_of_def:  "trans_of == (snd o snd)"
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    74
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    75
ioa_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    76
  "IOA(ioa) == (is_asig(asig_of(ioa))      &
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    77
                (~ starts_of(ioa) = {})    &
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    78
                state_trans (asig_of ioa) (trans_of ioa))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    79
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    80
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    81
(* An execution fragment is modelled with a pair of sequences:
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    82
 * the first is the action options, the second the state sequence.
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    83
 * Finite executions have None actions from some point on.
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    84
 *******)
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    85
is_execution_fragment_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    86
  "is_execution_fragment A ex ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    87
     let act = fst(ex); state = snd(ex)
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    88
     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    89
              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    90
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    91
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    92
executions_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    93
  "executions(ioa) == {e. snd e 0:starts_of(ioa) &
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    94
                        is_execution_fragment ioa e}"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    95
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    96
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
    97
reachable_def:
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    98
  "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
    99
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   100
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   101
invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   102
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   103
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   104
(* Restrict the trace to those members of the set s *)
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   105
filter_oseq_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   106
  "filter_oseq p s ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   107
   (%i. case s(i)
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   108
         of None => None
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   109
          | Some(x) => if p x then Some x else None)"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   110
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   111
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   112
mk_trace_def:
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3078
diff changeset
   113
  "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   114
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   115
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   116
(* Does an ioa have an execution with the given trace *)
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   117
has_trace_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   118
  "has_trace ioa b ==
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   119
     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   120
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   121
normal_form_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   122
  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   123
                    (!j. j ~: range(f) --> nf(j)= None) &
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   124
                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   125
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   126
(* All the traces of an ioa *)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   127
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   128
  traces_def:
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   129
  "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   130
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   131
(*
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   132
  traces_def:
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   133
  "traces(ioa) == {tr. has_trace ioa tr}"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   134
*)
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   135
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   136
compat_asigs_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   137
  "compat_asigs a1 a2 ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   138
   (((outputs(a1) Int outputs(a2)) = {}) &
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   139
    ((internals(a1) Int actions(a2)) = {}) &
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   140
    ((internals(a2) Int actions(a1)) = {}))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   141
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   142
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   143
compat_ioas_def:
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   144
  "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   145
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   146
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   147
asig_comp_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   148
  "asig_comp a1 a2 ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   149
      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   150
        (outputs(a1) Un outputs(a2)),
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   151
        (internals(a1) Un internals(a2))))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   152
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   153
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   154
par_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   155
  "(ioa1 || ioa2) ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   156
       (asig_comp (asig_of ioa1) (asig_of ioa2),
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   157
        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   158
        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   159
             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   160
                (if a:actions(asig_of(ioa1)) then
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   161
                   (fst(s),a,fst(t)):trans_of(ioa1)
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   162
                 else fst(t) = fst(s))
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   163
                &
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   164
                (if a:actions(asig_of(ioa2)) then
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   165
                   (snd(s),a,snd(t)):trans_of(ioa2)
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   166
                 else snd(t) = snd(s))})"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   167
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   168
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   169
restrict_asig_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   170
  "restrict_asig asig actns ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   171
    (inputs(asig) Int actns, outputs(asig) Int actns,
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   172
     internals(asig) Un (externals(asig) - actns))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   173
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   174
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   175
restrict_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   176
  "restrict ioa actns ==
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   177
    (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   178
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   179
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   180
ioa_implements_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   181
  "ioa_implements ioa1 ioa2 ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   182
  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   183
     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   184
      traces(ioa1) <= traces(ioa2))"
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   185
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   186
rename_def:
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   187
"rename ioa ren ==
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   188
  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   189
    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   190
    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   191
              starts_of(ioa)   ,
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   192
   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   193
        in
3078
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   194
        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff changeset
   195
19801
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   196
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   197
declare Let_def [simp]
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   198
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   199
lemmas ioa_projections = asig_of_def starts_of_def trans_of_def
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   200
  and exec_rws = executions_def is_execution_fragment_def
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   201
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   202
lemma ioa_triple_proj:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   203
    "asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   204
  apply (simp add: ioa_projections)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   205
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   206
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   207
lemma trans_in_actions:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   208
  "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   209
  apply (unfold ioa_def state_trans_def actions_def is_asig_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   210
  apply (erule conjE)+
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   211
  apply (erule allE, erule impE, assumption)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   212
  apply simp
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   213
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   214
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   215
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   216
lemma filter_oseq_idemp: "filter_oseq p (filter_oseq p s) = filter_oseq p s"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   217
  apply (simp add: filter_oseq_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   218
  apply (rule ext)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   219
  apply (case_tac "s i")
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   220
  apply simp_all
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   221
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   222
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   223
lemma mk_trace_thm:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   224
"(mk_trace A s n = None) =
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   225
   (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A))))
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   226
   &
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   227
   (mk_trace A s n = Some(a)) =
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   228
    (s(n)=Some(a) & a : externals(asig_of(A)))"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   229
  apply (unfold mk_trace_def filter_oseq_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   230
  apply (case_tac "s n")
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   231
  apply auto
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   232
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   233
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   234
lemma reachable_0: "s:starts_of(A) ==> reachable A s"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   235
  apply (unfold reachable_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   236
  apply (rule_tac x = "(%i. None, %i. s)" in bexI)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   237
  apply simp
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   238
  apply (simp add: exec_rws)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   239
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   240
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   241
lemma reachable_n:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   242
  "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   243
  apply (unfold reachable_def exec_rws)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   244
  apply (simp del: bex_simps)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   245
  apply (simp (no_asm_simp) only: split_tupled_all)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   246
  apply safe
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   247
  apply (rename_tac ex1 ex2 n)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   248
  apply (rule_tac x = "(%i. if i<n then ex1 i else (if i=n then Some a else None) , %i. if i<Suc n then ex2 i else t)" in bexI)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   249
   apply (rule_tac x = "Suc n" in exI)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   250
   apply (simp (no_asm))
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   251
  apply simp
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 19801
diff changeset
   252
  apply (metis ioa_triple_proj less_antisym)
19801
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   253
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   254
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   255
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   256
lemma invariantI:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   257
  assumes p1: "!!s. s:starts_of(A) ==> P(s)"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   258
    and p2: "!!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t)"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   259
  shows "invariant A P"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   260
  apply (unfold invariant_def reachable_def Let_def exec_rws)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   261
  apply safe
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   262
  apply (rename_tac ex1 ex2 n)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   263
  apply (rule_tac Q = "reachable A (ex2 n) " in conjunct1)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   264
  apply simp
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   265
  apply (induct_tac n)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   266
   apply (fast intro: p1 reachable_0)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   267
  apply (erule_tac x = na in allE)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   268
  apply (case_tac "ex1 na", simp_all)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   269
  apply safe
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   270
   apply (erule p2 [THEN mp])
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   271
    apply (fast dest: reachable_n)+
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   272
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   273
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   274
lemma invariantI1:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   275
 "[| !!s. s : starts_of(A) ==> P(s);
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   276
     !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   277
  |] ==> invariant A P"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   278
  apply (blast intro!: invariantI)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   279
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   280
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   281
lemma invariantE:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   282
  "[| invariant A P; reachable A s |] ==> P(s)"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   283
  apply (unfold invariant_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   284
  apply blast
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   285
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   286
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   287
lemma actions_asig_comp:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   288
  "actions(asig_comp a b) = actions(a) Un actions(b)"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   289
  apply (auto simp add: actions_def asig_comp_def asig_projections)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   290
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   291
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   292
lemma starts_of_par:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   293
  "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   294
  apply (simp add: par_def ioa_projections)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   295
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   296
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   297
(* Every state in an execution is reachable *)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   298
lemma states_of_exec_reachable:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   299
  "ex:executions(A) ==> !n. reachable A (snd ex n)"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   300
  apply (unfold reachable_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   301
  apply fast
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   302
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   303
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   304
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   305
lemma trans_of_par4:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   306
"(s,a,t) : trans_of(A || B || C || D) =
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   307
  ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   308
    a:actions(asig_of(D))) &
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   309
   (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   310
    else fst t=fst s) &
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   311
   (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   312
    else fst(snd(t))=fst(snd(s))) &
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   313
   (if a:actions(asig_of(C)) then
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   314
      (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   315
    else fst(snd(snd(t)))=fst(snd(snd(s)))) &
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   316
   (if a:actions(asig_of(D)) then
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   317
      (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   318
    else snd(snd(snd(t)))=snd(snd(snd(s)))))"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   319
  (*SLOW*)
44066
d74182c93f04 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents: 42174
diff changeset
   320
  apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff ioa_projections)
19801
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   321
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   322
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   323
lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   324
              trans_of(restrict ioa acts) = trans_of(ioa) &
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   325
              reachable (restrict ioa acts) s = reachable ioa s"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   326
  apply (simp add: is_execution_fragment_def executions_def
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   327
    reachable_def restrict_def ioa_projections)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   328
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   329
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   330
lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   331
  apply (simp add: par_def ioa_projections)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   332
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   333
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   334
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   335
lemma externals_of_par: "externals(asig_of(A1||A2)) =
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   336
   (externals(asig_of(A1)) Un externals(asig_of(A2)))"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   337
  apply (simp add: externals_def asig_of_par asig_comp_def
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 24742
diff changeset
   338
    asig_inputs_def asig_outputs_def Un_def set_diff_eq)
19801
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   339
  apply blast
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   340
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   341
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   342
lemma ext1_is_not_int2:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   343
  "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   344
  apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   345
  apply auto
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   346
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   347
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   348
lemma ext2_is_not_int1:
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   349
 "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   350
  apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def)
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   351
  apply auto
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   352
  done
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   353
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   354
lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 17288
diff changeset
   355
  and ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
17288
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   356
aa3833fb7bee converted to Isar theory format;
wenzelm
parents: 11482
diff changeset
   357
end