src/HOL/UNITY/Follows.thy
author paulson
Wed Dec 22 17:18:03 1999 +0100 (1999-12-22)
changeset 8074 36a6c38e0eca
parent 6809 5b8912f7bb69
child 8122 b43ad07660b9
permissions -rw-r--r--
Working version after a FAILED attempt to base Follows upon LeadsETo
     1 (*  Title:      HOL/UNITY/Follows
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The Follows relation of Charpentier and Sivilotte
     7 
     8 The safety conditions ensures that "givenBy f" is implementable in the
     9   progress part: g cannot do anything silly.
    10 *)
    11 
    12 Follows = ELT +
    13 
    14 constdefs
    15 
    16   Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
    17                  (infixl "Fols" 65)
    18    "f Fols g == Increasing g Int Increasing f Int
    19                 Always {s. f s <= g s} Int
    20                 (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
    21 
    22 
    23 end