src/HOLCF/IOA/meta_theory/CompoExecs.thy
author wenzelm
Fri Sep 02 17:23:59 2005 +0200 (2005-09-02)
changeset 17233 41eee2e7b465
parent 14981 e73f8140af78
child 19741 f65265d71426
permissions -rw-r--r--
converted specifications to Isar theories;
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
mueller@3275
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
wenzelm@17233
     4
*)
mueller@3071
     5
wenzelm@17233
     6
header {* Compositionality on Execution level *}
mueller@3071
     7
wenzelm@17233
     8
theory CompoExecs
wenzelm@17233
     9
imports Traces
wenzelm@17233
    10
begin
mueller@3071
    11
wenzelm@17233
    12
consts
mueller@3071
    13
mueller@3071
    14
 ProjA      ::"('a,'s * 't)execution => ('a,'s)execution"
mueller@3071
    15
 ProjA2     ::"('a,'s * 't)pairs     -> ('a,'s)pairs"
mueller@3071
    16
 ProjB      ::"('a,'s * 't)execution => ('a,'t)execution"
mueller@3071
    17
 ProjB2     ::"('a,'s * 't)pairs     -> ('a,'t)pairs"
mueller@3521
    18
 Filter_ex  ::"'a signature => ('a,'s)execution => ('a,'s)execution"
wenzelm@17233
    19
 Filter_ex2 ::"'a signature => ('a,'s)pairs     -> ('a,'s)pairs"
wenzelm@17233
    20
 stutter    ::"'a signature => ('a,'s)execution => bool"
mueller@3521
    21
 stutter2   ::"'a signature => ('a,'s)pairs     -> ('s => tr)"
mueller@3521
    22
mueller@3521
    23
 par_execs  ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module"
mueller@3071
    24
mueller@3071
    25
wenzelm@17233
    26
defs
mueller@3071
    27
mueller@3071
    28
wenzelm@17233
    29
ProjA_def:
wenzelm@17233
    30
 "ProjA ex == (fst (fst ex), ProjA2$(snd ex))"
mueller@3071
    31
wenzelm@17233
    32
ProjB_def:
wenzelm@17233
    33
 "ProjB ex == (snd (fst ex), ProjB2$(snd ex))"
mueller@3071
    34
mueller@3071
    35
wenzelm@17233
    36
ProjA2_def:
mueller@3071
    37
  "ProjA2 == Map (%x.(fst x,fst(snd x)))"
mueller@3071
    38
wenzelm@17233
    39
ProjB2_def:
mueller@3071
    40
  "ProjB2 == Map (%x.(fst x,snd(snd x)))"
wenzelm@17233
    41
mueller@3071
    42
wenzelm@17233
    43
Filter_ex_def:
nipkow@10835
    44
  "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))"
mueller@3071
    45
mueller@3071
    46
wenzelm@17233
    47
Filter_ex2_def:
wenzelm@3842
    48
  "Filter_ex2 sig ==  Filter (%x. fst x:actions sig)"
mueller@3071
    49
wenzelm@17233
    50
stutter_def:
nipkow@10835
    51
  "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
mueller@3071
    52
wenzelm@17233
    53
stutter2_def:
wenzelm@17233
    54
  "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of
mueller@3071
    55
      nil => TT
wenzelm@17233
    56
    | x##xs => (flift1
mueller@3521
    57
            (%p.(If Def ((fst p)~:actions sig)
wenzelm@17233
    58
                 then Def (s=(snd p))
mueller@3071
    59
                 else TT fi)
wenzelm@17233
    60
                andalso (h$xs) (snd p))
nipkow@10835
    61
             $x)
wenzelm@17233
    62
   )))"
mueller@3071
    63
wenzelm@17233
    64
par_execs_def:
wenzelm@17233
    65
  "par_execs ExecsA ExecsB ==
wenzelm@17233
    66
       let exA = fst ExecsA; sigA = snd ExecsA;
wenzelm@17233
    67
           exB = fst ExecsB; sigB = snd ExecsB
mueller@3521
    68
       in
mueller@3521
    69
       (    {ex. Filter_ex sigA (ProjA ex) : exA}
mueller@3521
    70
        Int {ex. Filter_ex sigB (ProjB ex) : exB}
mueller@3521
    71
        Int {ex. stutter sigA (ProjA ex)}
mueller@3521
    72
        Int {ex. stutter sigB (ProjB ex)}
wenzelm@3842
    73
        Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
mueller@3521
    74
        asig_comp sigA sigB)"
mueller@3071
    75
wenzelm@17233
    76
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17233
    77
wenzelm@17233
    78
end