src/HOL/UNITY/UNITY.thy
author paulson
Sat Sep 23 16:02:01 2000 +0200 (2000-09-23)
changeset 10064 1a77667b21ef
parent 8948 b797cfa3548d
child 10797 028d22926a41
permissions -rw-r--r--
added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.
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@8948
    11
UNITY = Main + 
paulson@6535
    12
paulson@6535
    13
typedef (Program)
paulson@10064
    14
  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
paulson@10064
    15
		  allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
paulson@4776
    16
paulson@6536
    17
consts
paulson@6823
    18
  constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
paulson@6823
    19
  op_unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
paulson@6536
    20
paulson@4776
    21
constdefs
paulson@10064
    22
    mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
paulson@10064
    23
		   => 'a program"
paulson@10064
    24
    "mk_program == %(init, acts, allowed).
paulson@10064
    25
                      Abs_Program (init, insert Id acts, insert Id allowed)"
paulson@6535
    26
paulson@6535
    27
  Init :: "'a program => 'a set"
paulson@10064
    28
    "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
paulson@6535
    29
paulson@6535
    30
  Acts :: "'a program => ('a * 'a)set set"
paulson@10064
    31
    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
paulson@10064
    32
paulson@10064
    33
  AllowedActs :: "'a program => ('a * 'a)set set"
paulson@10064
    34
    "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
paulson@10064
    35
paulson@10064
    36
  Allowed :: "'a program => 'a program set"
paulson@10064
    37
    "Allowed F == {G. Acts G <= AllowedActs F}"
paulson@4776
    38
paulson@5648
    39
  stable     :: "'a set => 'a program set"
paulson@6536
    40
    "stable A == A co A"
paulson@4776
    41
paulson@5648
    42
  strongest_rhs :: "['a program, 'a set] => 'a set"
paulson@6536
    43
    "strongest_rhs F A == Inter {B. F : A co B}"
paulson@4776
    44
paulson@5648
    45
  invariant :: "'a set => 'a program set"
paulson@5648
    46
    "invariant A == {F. Init F <= A} Int stable A"
paulson@4776
    47
paulson@5648
    48
  (*Polymorphic in both states and the meaning of <= *)
paulson@6713
    49
  increasing :: "['a => 'b::{order}] => 'a program set"
paulson@5648
    50
    "increasing f == INT z. stable {s. z <= f s}"
paulson@4776
    51
paulson@6536
    52
paulson@6536
    53
defs
paulson@6536
    54
  constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}"
paulson@6536
    55
paulson@6536
    56
  unless_def     "A unless B == (A-B) co (A Un B)"
paulson@6536
    57
paulson@4776
    58
end