summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

6 Common Meeting Time example from Misra (1994)

8 The state is identified with the one variable in existence.

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

11 *)

13 Common = WFair + Traces +

15 consts

16 ftime,gtime :: nat=>nat

18 rules

19 fmono "m <= n ==> ftime m <= ftime n"

20 gmono "m <= n ==> gtime m <= gtime n"

22 fasc "m <= ftime n"

23 gasc "m <= gtime n"

25 constdefs

26 common :: nat set

27 "common == {n. ftime n = n & gtime n = n}"

29 maxfg :: nat => nat set

30 "maxfg m == {t. t <= max (ftime m) (gtime m)}"

32 end