src/HOL/HOLCF/IOA/ABP/Spec.thy
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 66453 cc19f7ca2ed6
child 67369 7360fe6bb423
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40945
diff changeset
     1
(*  Title:      HOL/HOLCF/IOA/ABP/Spec.thy
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
     2
    Author:     Olaf Müller
3072
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 59503
diff changeset
     5
section \<open>The specification of reliable transmission\<close>
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
theory Spec
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 62009
diff changeset
     8
imports IOA.IOA Action
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
begin
3072
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    10
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    11
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    12
  spec_sig :: "'m action signature" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    13
  sig_def: "spec_sig = (UN m.{S_msg(m)},
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    14
                       UN m.{R_msg(m)} Un {Next},
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    15
                       {})"
3072
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    17
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    18
  spec_trans :: "('m action, 'm list)transition set" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    19
  trans_def: "spec_trans =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    20
   {tr. let s = fst(tr);
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    21
            t = snd(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    22
        in
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    23
        case fst(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    24
        of
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    25
        Next =>  t=s |            (* Note that there is condition as in Sender *)
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    26
        S_msg(m) => t = s@[m]  |
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    27
        R_msg(m) => s = (m#t)  |
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    28
        S_pkt(pkt) => False |
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    29
        R_pkt(pkt) => False |
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    30
        S_ack(b) => False |
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    31
        R_ack(b) => False}"
3072
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    32
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    33
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 17244
diff changeset
    34
  spec_ioa :: "('m action, 'm list)ioa" where
59503
9937bc07202b check unused theory;
wenzelm
parents: 58880
diff changeset
    35
  ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans, {}, {})"
3072
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    36
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    37
end