src/HOL/UNITY/UNITY.thy
author paulson
Thu Apr 29 10:51:58 1999 +0200 (1999-04-29)
changeset 6536 281d44905cab
parent 6535 880f31a62784
child 6713 614a76ce9bc6
permissions -rw-r--r--
made many specification operators infix
paulson@4776
     1
(*  Title:      HOL/UNITY/UNITY
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
The basic UNITY theory (revised version, based upon the "co" operator)
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     9
*)
paulson@4776
    10
paulson@6535
    11
UNITY = LessThan + Prefix +
paulson@6535
    12
paulson@6535
    13
paulson@6535
    14
typedef (Program)
paulson@6535
    15
  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
paulson@4776
    16
paulson@6536
    17
consts
paulson@6536
    18
  co, unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson@6536
    19
paulson@4776
    20
constdefs
paulson@6535
    21
    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
paulson@6535
    22
    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
paulson@6535
    23
paulson@6535
    24
  Init :: "'a program => 'a set"
paulson@6535
    25
    "Init F == (%(init, acts). init) (Rep_Program F)"
paulson@6535
    26
paulson@6535
    27
  Acts :: "'a program => ('a * 'a)set set"
paulson@6535
    28
    "Acts F == (%(init, acts). acts) (Rep_Program F)"
paulson@4776
    29
paulson@5648
    30
  stable     :: "'a set => 'a program set"
paulson@6536
    31
    "stable A == A co A"
paulson@4776
    32
paulson@5648
    33
  strongest_rhs :: "['a program, 'a set] => 'a set"
paulson@6536
    34
    "strongest_rhs F A == Inter {B. F : A co B}"
paulson@4776
    35
paulson@5648
    36
  invariant :: "'a set => 'a program set"
paulson@5648
    37
    "invariant A == {F. Init F <= A} Int stable A"
paulson@4776
    38
paulson@5648
    39
  (*Polymorphic in both states and the meaning of <= *)
paulson@5648
    40
  increasing :: "['a => 'b::{ord}] => 'a program set"
paulson@5648
    41
    "increasing f == INT z. stable {s. z <= f s}"
paulson@4776
    42
paulson@6536
    43
paulson@6536
    44
defs
paulson@6536
    45
  constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}"
paulson@6536
    46
paulson@6536
    47
  unless_def     "A unless B == (A-B) co (A Un B)"
paulson@6536
    48
paulson@4776
    49
end