src/HOL/UNITY/Common.thy
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5648 fe887910e32e
child 7537 875754b599df
permissions -rw-r--r--
Drule.rev_triv_goal;

(*  Title:      HOL/UNITY/Common
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Common Meeting Time example from Misra (1994)

The state is identified with the one variable in existence.

From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)

Common = SubstAx + Union + 

consts
  ftime,gtime :: nat=>nat

rules
  fmono "m <= n ==> ftime m <= ftime n"
  gmono "m <= n ==> gtime m <= gtime n"

  fasc  "m <= ftime n"
  gasc  "m <= gtime n"

constdefs
  common :: nat set
    "common == {n. ftime n = n & gtime n = n}"

  maxfg :: nat => nat set
    "maxfg m == {t. t <= max (ftime m) (gtime m)}"

end