src/HOL/TLA/Buffer/Buffer.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41589 bbd861837ebc
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:
41589
bbd861837ebc tuned headers;
wenzelm
parents: 21624
diff changeset
     1
(*  Title:      HOL/TLA/Buffer/Buffer.thy
bbd861837ebc tuned headers;
wenzelm
parents: 21624
diff changeset
     2
    Author:     Stephan Merz, University of Munich
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     3
*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     4
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     5
header {* A simple FIFO buffer (synchronous communication, interleaving) *}
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     6
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     7
theory Buffer
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     8
imports TLA
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     9
begin
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    10
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    11
consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    12
  (* actions *)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    13
  BInit     :: "'a stfun => 'a list stfun => 'a stfun => stpred"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    14
  Enq       :: "'a stfun => 'a list stfun => 'a stfun => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    15
  Deq       :: "'a stfun => 'a list stfun => 'a stfun => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    16
  Next      :: "'a stfun => 'a list stfun => 'a stfun => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    17
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    18
  (* temporal formulas *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    19
  IBuffer   :: "'a stfun => 'a list stfun => 'a stfun => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    20
  Buffer    :: "'a stfun => 'a stfun => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    21
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    22
defs
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    23
  BInit_def:   "BInit ic q oc    == PRED q = #[]"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    24
  Enq_def:     "Enq ic q oc      == ACT (ic$ ~= $ic)
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    25
                                     & (q$ = $q @ [ ic$ ])
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    26
                                     & (oc$ = $oc)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    27
  Deq_def:     "Deq ic q oc      == ACT ($q ~= #[])
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    28
                                     & (oc$ = hd< $q >)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    29
                                     & (q$ = tl< $q >)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    30
                                     & (ic$ = $ic)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    31
  Next_def:    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    32
  IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    33
                                      & [][Next ic q oc]_(ic,q,oc)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    34
                                      & WF(Deq ic q oc)_(ic,q,oc)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    35
  Buffer_def:  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    36
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    37
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    38
(* ---------------------------- Data lemmas ---------------------------- *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    39
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    40
(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    41
lemma tl_not_self [simp]: "xs ~= [] ==> tl xs ~= xs"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    42
  by (auto simp: neq_Nil_conv)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    43
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    44
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    45
(* ---------------------------- Action lemmas ---------------------------- *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    46
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    47
(* Dequeue is visible *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    48
lemma Deq_visible: "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    49
  apply (unfold angle_def Deq_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    50
  apply (safe, simp (asm_lr))+
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    51
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    52
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    53
(* Enabling condition for dequeue -- NOT NEEDED *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    54
lemma Deq_enabled: 
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    55
    "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    56
  apply (unfold Deq_visible [temp_rewrite])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    57
  apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    58
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    59
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    60
(* For the left-to-right implication, we don't need the base variable stuff *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    61
lemma Deq_enabledE: 
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    62
    "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    63
  apply (unfold Deq_visible [temp_rewrite])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    64
  apply (auto elim!: enabledE simp add: Deq_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    65
  done
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    66
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    67
end