src/ZF/UNITY/Follows.thy
author paulson
Wed, 28 May 2003 18:13:41 +0200
changeset 14052 e9c9f69e4f63
child 14093 24382760fd89
permissions -rw-r--r--
some new ZF/UNITY material from Sidi Ehmety
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/Follows
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     2
    ID:         $Id$
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     3
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     4
    Copyright   2002  University of Cambridge
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     5
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     6
The "Follows" relation of Charpentier and Sivilotte
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     7
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     8
Theory ported from HOL.
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     9
*)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    10
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    11
Follows = SubstAx + Increasing +
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    12
constdefs
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    13
  Follows :: "[i, i, i=>i, i=>i] => i"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    14
  "Follows(A, r, f, g) == 
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    15
            Increasing(A, r, g) Int
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    16
            Increasing(A, r,f) Int
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    17
            Always({s:state. <f(s), g(s)>:r}) Int
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    18
           (INT k:A. {s:state. <k, g(s)>:r} LeadsTo {s:state. <k,f(s)>:r})"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    19
consts
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    20
  Incr :: [i=>i]=>i   
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    21
  n_Incr :: [i=>i]=>i
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    22
  m_Incr :: [i=>i]=>i
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    23
  s_Incr :: [i=>i]=>i
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    24
  n_Fols :: [i=>i, i=>i]=>i   (infixl "n'_Fols" 65)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    25
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    26
syntax
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    27
  Follows' :: "[i=>i, i=>i, i, i] => i"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    28
        ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    29
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    30
  
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    31
translations
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    32
  "Incr(f)" == "Increasing(list(nat), prefix(nat), f)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    33
  "n_Incr(f)" == "Increasing(nat, Le, f)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    34
  "s_Incr(f)" == "Increasing(Pow(nat), SetLe(nat), f)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    35
  "m_Incr(f)" == "Increasing(Mult(nat), MultLe(nat, Le), f)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    36
  
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    37
  "f n_Fols g" == "Follows(nat, Le, f, g)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    38
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    39
  "Follows'(f,g,r,A)" == "Follows(A,r,f,g)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    40
end