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