src/HOL/UNITY/Common.thy
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5648 fe887910e32e
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
paulson@4776
     1
(*  Title:      HOL/UNITY/Common
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Common Meeting Time example from Misra (1994)
paulson@4776
     7
paulson@4776
     8
The state is identified with the one variable in existence.
paulson@4776
     9
paulson@4776
    10
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
paulson@4776
    11
*)
paulson@4776
    12
paulson@5313
    13
Common = SubstAx +
paulson@4776
    14
paulson@4776
    15
consts
paulson@4776
    16
  ftime,gtime :: nat=>nat
paulson@4776
    17
paulson@4776
    18
rules
paulson@4776
    19
  fmono "m <= n ==> ftime m <= ftime n"
paulson@4776
    20
  gmono "m <= n ==> gtime m <= gtime n"
paulson@4776
    21
paulson@4776
    22
  fasc  "m <= ftime n"
paulson@4776
    23
  gasc  "m <= gtime n"
paulson@4776
    24
paulson@4776
    25
constdefs
paulson@4776
    26
  common :: nat set
paulson@4776
    27
    "common == {n. ftime n = n & gtime n = n}"
paulson@4776
    28
paulson@4776
    29
  maxfg :: nat => nat set
paulson@4776
    30
    "maxfg m == {t. t <= max (ftime m) (gtime m)}"
paulson@4776
    31
paulson@4776
    32
end