src/HOLCF/IOA/meta_theory/Traces.thy
author wenzelm
Wed, 19 Mar 2008 22:47:35 +0100
changeset 26339 7825c83c9eff
parent 22808 a7daa74e2980
child 26359 6d437bde2f1d
permissions -rw-r--r--
eliminated change_claset/simpset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/Traces.thy
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     2
    ID:         $Id$
12218
wenzelm
parents: 12028
diff changeset
     3
    Author:     Olaf Müller
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     4
*)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     6
header {* Executions and Traces of I/O automata in HOLCF *}
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     8
theory Traces
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     9
imports Sequence Automata
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    10
begin
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    11
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    12
defaultsort type
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    13
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    14
types
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    15
   ('a,'s)pairs            =    "('a * 's) Seq"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    16
   ('a,'s)execution        =    "'s * ('a,'s)pairs"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    17
   'a trace                =    "'a Seq"
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    18
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    19
   ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    20
   'a schedule_module      = "'a trace set * 'a signature"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    21
   'a trace_module         = "'a trace set * 'a signature"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    22
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    23
consts
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    24
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    25
   (* Executions *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
    26
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    27
  is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr"
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    28
  is_exec_frag  ::"[('a,'s)ioa, ('a,'s)execution] => bool"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    29
  has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    30
  executions    :: "('a,'s)ioa => ('a,'s)execution set"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    31
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    32
  (* Schedules and traces *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    33
  filter_act    ::"('a,'s)pairs -> 'a trace"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    34
  has_schedule  :: "[('a,'s)ioa, 'a trace] => bool"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    35
  has_trace     :: "[('a,'s)ioa, 'a trace] => bool"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    36
  schedules     :: "('a,'s)ioa => 'a trace set"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    37
  traces        :: "('a,'s)ioa => 'a trace set"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    38
  mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    39
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    40
  laststate    ::"('a,'s)execution => 's"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    41
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    42
  (* A predicate holds infinitely (finitely) often in a sequence *)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    43
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    44
  inf_often      ::"('a => bool) => 'a Seq => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    45
  fin_often      ::"('a => bool) => 'a Seq => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    46
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    47
  (* fairness of executions *)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    48
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    49
  wfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    50
  sfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    51
  is_wfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    52
  is_sfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    53
  fair_ex        ::"('a,'s)ioa => ('a,'s)execution => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    54
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    55
  (* fair behavior sets *)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    56
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    57
  fairexecutions ::"('a,'s)ioa => ('a,'s)execution set"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    58
  fairtraces     ::"('a,'s)ioa => 'a trace set"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    59
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    60
  (* Notions of implementation *)
22808
a7daa74e2980 eliminated unnamed infixes, tuned syntax;
wenzelm
parents: 19741
diff changeset
    61
  ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr "=<|" 12)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
    62
  fair_implements  :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    63
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    64
  (* Execution, schedule and trace modules *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    65
  Execs         ::  "('a,'s)ioa => ('a,'s)execution_module"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    66
  Scheds        ::  "('a,'s)ioa => 'a schedule_module"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    67
  Traces        ::  "('a,'s)ioa => 'a trace_module"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
    68
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    69
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    70
defs
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    71
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    72
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    73
(*  ------------------- Executions ------------------------------ *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    74
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    75
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    76
is_exec_frag_def:
10835
nipkow
parents: 5976
diff changeset
    77
  "is_exec_frag A ex ==  ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    78
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
    79
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    80
is_exec_fragC_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    81
  "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    82
      nil => TT
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    83
    | x##xs => (flift1
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    84
            (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p))
10835
nipkow
parents: 5976
diff changeset
    85
             $x)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    86
   )))"
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
    87
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
    88
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
    89
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    90
executions_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    91
  "executions ioa == {e. ((fst e) : starts_of(ioa)) &
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
    92
                         is_exec_frag ioa e}"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    93
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    94
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    95
(*  ------------------- Schedules ------------------------------ *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    96
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    97
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    98
filter_act_def:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    99
  "filter_act == Map fst"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   100
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   101
has_schedule_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   102
  "has_schedule ioa sch ==
10835
nipkow
parents: 5976
diff changeset
   103
     (? ex:executions ioa. sch = filter_act$(snd ex))"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   104
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   105
schedules_def:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   106
  "schedules ioa == {sch. has_schedule ioa sch}"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   107
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   108
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   109
(*  ------------------- Traces ------------------------------ *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   110
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   111
has_trace_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   112
  "has_trace ioa tr ==
10835
nipkow
parents: 5976
diff changeset
   113
     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   114
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   115
traces_def:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   116
  "traces ioa == {tr. has_trace ioa tr}"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   117
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   118
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   119
mk_trace_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   120
  "mk_trace ioa == LAM tr.
10835
nipkow
parents: 5976
diff changeset
   121
     Filter (%a. a:ext(ioa))$(filter_act$tr)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   122
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   123
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   124
(*  ------------------- Fair Traces ------------------------------ *)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   125
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   126
laststate_def:
10835
nipkow
parents: 5976
diff changeset
   127
  "laststate ex == case Last$(snd ex) of
12028
52aa183c15bb replaced Undef by UU;
wenzelm
parents: 10835
diff changeset
   128
                      UU  => fst ex
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   129
                    | Def at => snd at"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   130
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   131
inf_often_def:
10835
nipkow
parents: 5976
diff changeset
   132
  "inf_often P s == Infinite (Filter P$s)"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   133
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   134
(*  filtering P yields a finite or partial sequence *)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   135
fin_often_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   136
  "fin_often P s == ~inf_often P s"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   137
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   138
(* Note that partial execs cannot be wfair as the inf_often predicate in the
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   139
   else branch prohibits it. However they can be sfair in the case when all W
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   140
   are only finitely often enabled: Is this the right model?
5976
44290b71a85f tuning to assimiliate it with PhD;
mueller
parents: 4559
diff changeset
   141
   See LiveIOA for solution conforming with the literature and superseding this one *)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   142
wfair_ex_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   143
  "wfair_ex A ex == ! W : wfair_of A.
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   144
                      if   Finite (snd ex)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   145
                      then ~Enabled A W (laststate ex)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   146
                      else is_wfair A W ex"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   147
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   148
is_wfair_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   149
  "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   150
                     | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   151
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   152
sfair_ex_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   153
  "sfair_ex A ex == ! W : sfair_of A.
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   154
                      if   Finite (snd ex)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   155
                      then ~Enabled A W (laststate ex)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   156
                      else is_sfair A W ex"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   157
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   158
is_sfair_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   159
  "is_sfair A W ex ==  (inf_often (%x. fst x:W) (snd ex)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   160
                      | fin_often (%x. Enabled A W (snd x)) (snd ex))"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   161
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   162
fair_ex_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   163
  "fair_ex A ex == wfair_ex A ex & sfair_ex A ex"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   164
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   165
fairexecutions_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   166
  "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   167
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   168
fairtraces_def:
10835
nipkow
parents: 5976
diff changeset
   169
  "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   170
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   171
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   172
(*  ------------------- Implementation ------------------------------ *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   173
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   174
ioa_implements_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   175
  "ioa1 =<| ioa2 ==
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   176
    (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   177
     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   178
      traces(ioa1) <= traces(ioa2))"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   179
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   180
fair_implements_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   181
  "fair_implements C A == inp(C) = inp(A) &  out(C)=out(A) &
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   182
                          fairtraces(C) <= fairtraces(A)"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents: 3842
diff changeset
   183
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   184
(*  ------------------- Modules ------------------------------ *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   185
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   186
Execs_def:
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   187
  "Execs A  == (executions A, asig_of A)"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   188
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   189
Scheds_def:
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   190
  "Scheds A == (schedules A, asig_of A)"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   191
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   192
Traces_def:
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   193
  "Traces A == (traces A,asig_of A)"
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3433
diff changeset
   194
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   195
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   196
lemmas [simp del] = ex_simps all_simps split_paired_Ex
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   197
declare Let_def [simp]
26339
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 22808
diff changeset
   198
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   199
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   200
lemmas exec_rws = executions_def is_exec_frag_def
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   201
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   202
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   203
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   204
subsection "recursive equations of operators"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   205
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   206
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   207
(*                               filter_act                         *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   208
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   209
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   210
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   211
lemma filter_act_UU: "filter_act$UU = UU"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   212
apply (simp add: filter_act_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   213
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   214
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   215
lemma filter_act_nil: "filter_act$nil = nil"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   216
apply (simp add: filter_act_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   217
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   218
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   219
lemma filter_act_cons: "filter_act$(x>>xs) = (fst x) >> filter_act$xs"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   220
apply (simp add: filter_act_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   221
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   222
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   223
declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   224
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   225
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   226
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   227
(*                             mk_trace                             *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   228
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   229
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   230
lemma mk_trace_UU: "mk_trace A$UU=UU"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   231
apply (simp add: mk_trace_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   232
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   233
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   234
lemma mk_trace_nil: "mk_trace A$nil=nil"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   235
apply (simp add: mk_trace_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   236
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   237
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   238
lemma mk_trace_cons: "mk_trace A$(at >> xs) =     
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   239
             (if ((fst at):ext A)            
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   240
                  then (fst at) >> (mk_trace A$xs)     
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   241
                  else mk_trace A$xs)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   242
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   243
apply (simp add: mk_trace_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   244
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   245
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   246
declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   247
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   248
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   249
(*                             is_exec_fragC                             *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   250
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   251
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   252
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   253
lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   254
       nil => TT  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   255
     | x##xs => (flift1   
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   256
             (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p))  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   257
              $x)  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   258
    ))"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   259
apply (rule trans)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   260
apply (rule fix_eq2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   261
apply (rule is_exec_fragC_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   262
apply (rule beta_cfun)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   263
apply (simp add: flift1_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   264
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   265
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   266
lemma is_exec_fragC_UU: "(is_exec_fragC A$UU) s=UU"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   267
apply (subst is_exec_fragC_unfold)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   268
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   269
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   270
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   271
lemma is_exec_fragC_nil: "(is_exec_fragC A$nil) s = TT"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   272
apply (subst is_exec_fragC_unfold)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   273
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   274
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   275
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   276
lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr>>xs)) s =  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   277
                         (Def ((s,pr):trans_of A)  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   278
                 andalso (is_exec_fragC A$xs)(snd pr))"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   279
apply (rule trans)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   280
apply (subst is_exec_fragC_unfold)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   281
apply (simp add: Consq_def flift1_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   282
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   283
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   284
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   285
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   286
declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   287
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   288
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   289
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   290
(*                        is_exec_frag                              *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   291
(* ---------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   292
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   293
lemma is_exec_frag_UU: "is_exec_frag A (s, UU)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   294
apply (simp add: is_exec_frag_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   295
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   296
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   297
lemma is_exec_frag_nil: "is_exec_frag A (s, nil)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   298
apply (simp add: is_exec_frag_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   299
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   300
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   301
lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)>>ex) =  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   302
                                (((s,a,t):trans_of A) &  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   303
                                is_exec_frag A (t, ex))"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   304
apply (simp add: is_exec_frag_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   305
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   306
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   307
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   308
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   309
declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   310
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   311
(* ---------------------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   312
                           section "laststate"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   313
(* ---------------------------------------------------------------------------- *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   314
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   315
lemma laststate_UU: "laststate (s,UU) = s"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   316
apply (simp add: laststate_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   317
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   318
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   319
lemma laststate_nil: "laststate (s,nil) = s"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   320
apply (simp add: laststate_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   321
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   322
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   323
lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   324
apply (simp (no_asm) add: laststate_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   325
apply (case_tac "ex=nil")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   326
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   327
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   328
apply (drule Finite_Last1 [THEN mp])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   329
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   330
apply (tactic "def_tac 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   331
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   332
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   333
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   334
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   335
lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   336
apply (tactic "Seq_Finite_induct_tac 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   337
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   338
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   339
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   340
subsection "has_trace, mk_trace"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   341
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   342
(* alternative definition of has_trace tailored for the refinement proof, as it does not 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   343
   take the detour of schedules *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   344
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   345
lemma has_trace_def2: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   346
"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   347
apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   348
apply (tactic "safe_tac set_cs")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   349
(* 1 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   350
apply (rule_tac x = "ex" in bexI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   351
apply (simplesubst beta_cfun)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   352
apply (tactic "cont_tacR 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   353
apply (simp (no_asm))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   354
apply (simp (no_asm_simp))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   355
(* 2 *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   356
apply (rule_tac x = "filter_act$ (snd ex) " in bexI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   357
apply (simplesubst beta_cfun)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   358
apply (tactic "cont_tacR 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   359
apply (simp (no_asm))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   360
apply (tactic "safe_tac set_cs")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   361
apply (rule_tac x = "ex" in bexI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   362
apply simp_all
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   363
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   364
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   365
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   366
subsection "signatures and executions, schedules"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   367
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   368
(* All executions of A have only actions of A. This is only true because of the 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   369
   predicate state_trans (part of the predicate IOA): We have no dependent types.
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   370
   For executions of parallel automata this assumption is not needed, as in par_def
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   371
   this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   372
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   373
lemma execfrag_in_sig: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   374
  "!! A. is_trans_of A ==>  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   375
  ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   376
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def",
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   377
  thm "Forall_def", thm "sforall_def"] 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   378
(* main case *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   379
apply (rename_tac ss a t)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   380
apply (tactic "safe_tac set_cs")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   381
apply (simp_all add: is_trans_of_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   382
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   383
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   384
lemma exec_in_sig: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   385
  "!! A.[|  is_trans_of A; x:executions A |] ==>  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   386
  Forall (%a. a:act A) (filter_act$(snd x))"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   387
apply (simp add: executions_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   388
apply (tactic {* pair_tac "x" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   389
apply (rule execfrag_in_sig [THEN spec, THEN mp])
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   390
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   391
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   392
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   393
lemma scheds_in_sig: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   394
  "!! A.[|  is_trans_of A; x:schedules A |] ==>  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   395
    Forall (%a. a:act A) x"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   396
apply (unfold schedules_def has_schedule_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   397
apply (fast intro!: exec_in_sig)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   398
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   399
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   400
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   401
subsection "executions are prefix closed"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   402
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   403
(* only admissible in y, not if done in x !! *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   404
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   405
apply (tactic {* pair_induct_tac "y" [thm "is_exec_frag_def"] 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   406
apply (intro strip)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   407
apply (tactic {* Seq_case_simp_tac "xa" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   408
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   409
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   410
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   411
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   412
lemmas exec_prefixclosed =
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   413
  conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp], standard]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   414
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   415
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   416
(* second prefix notion for Finite x *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   417
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   418
lemma exec_prefix2closed [rule_format]:
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   419
  "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   420
apply (tactic {* pair_induct_tac "x" [thm "is_exec_frag_def"] 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   421
apply (intro strip)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   422
apply (tactic {* Seq_case_simp_tac "s" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   423
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   424
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   425
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   426
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   427
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   428
end