src/HOL/UNITY/UNITY.thy

new proof of drop_prog_correct for new definition of project_act

(*  Title:      HOL/UNITY/UNITY
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

The basic UNITY theory (revised version, based upon the "co" operator)

From Misra, "A Logic for Concurrent Programming", 1994
*)

UNITY = LessThan + ListOrder +


typedef (Program)
  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"

consts
  constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
  op_unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)

constdefs
    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"

  Init :: "'a program => 'a set"
    "Init F == (%(init, acts). init) (Rep_Program F)"

  Acts :: "'a program => ('a * 'a)set set"
    "Acts F == (%(init, acts). acts) (Rep_Program F)"

  stable     :: "'a set => 'a program set"
    "stable A == A co A"

  strongest_rhs :: "['a program, 'a set] => 'a set"
    "strongest_rhs F A == Inter {B. F : A co B}"

  invariant :: "'a set => 'a program set"
    "invariant A == {F. Init F <= A} Int stable A"

  (*Polymorphic in both states and the meaning of <= *)
  increasing :: "['a => 'b::{order}] => 'a program set"
    "increasing f == INT z. stable {s. z <= f s}"


defs
  constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}"

  unless_def     "A unless B == (A-B) co (A Un B)"

end