src/ZF/UNITY/Constrains.thy

new ZF/UNITY theory

(*  Title:      ZF/UNITY/Constrains.thy
    ID:         $Id$
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   2001  University of Cambridge

Safety relations: restricted to the set of reachable states.

Theory ported from HOL.
*)

Constrains = UNITY +
consts traces :: "[i, i] => i"
  (* Initial states and program => (final state, reversed trace to it)... 
      the domain might also be state*list(state) *)
inductive 
  domains 
     "traces(init, acts)" <=
         "(init Un (UN act:acts. field(act)))*list(UN act:acts. field(act))"
  intrs 
         (*Initial trace is empty*)
    Init  "s: init ==> <s,[]> : traces(init,acts)"

    Acts  "[| act:acts;  <s,evs> : traces(init,acts);  <s,s'>: act |]
           ==> <s', Cons(s,evs)> : traces(init, acts)"
  
  type_intrs "list.intrs@[UnI1, UnI2, UN_I, fieldI2, fieldI1]"

  consts reachable :: "i=>i"

inductive
  domains
  "reachable(F)" <= "Init(F) Un (UN act:Acts(F). field(act))"
  intrs 
    Init  "s:Init(F) ==> s:reachable(F)"

    Acts  "[| act: Acts(F);  s:reachable(F);  <s,s'>: act |]
           ==> s':reachable(F)"

  type_intrs "[UnI1, UnI2, fieldI2, UN_I]"

  
consts
  Constrains :: "[i,i] => i"  (infixl "Co"     60)
  op_Unless  :: "[i, i] => i"  (infixl "Unless" 60)

defs
  Constrains_def
    "A Co B == {F:program. F:(reachable(F) Int A) co B &
		           A:condition & B:condition}"

  Unless_def
    "A Unless B == (A-B) Co (A Un B)"

constdefs
  Stable     :: "i => i"
    "Stable(A) == A Co A"
  (*Always is the weak form of "invariant"*)
  Always :: "i => i"
    "Always(A) == {F:program. Init(F) <= A} Int Stable(A)"

  (*
  The constant Increasing_on defines a weak form of the Charpentier's
  increasing notion.  It should not be confused with the ZF's
  increasing constant which have a different meaning.
  Increasing's parameters: a state function f,
  a domain A and a order relation r over the domain A.
  Should f be a meta function instead ?
  *)
  Increasing_on :: [i,i, i] => i  ("Increasing[_]'(_,_')")
  "Increasing[A](f, r) == {F:program. f:state->A &
			      part_order(A,r) &
			      F: (INT z:A. Stable({s:state.  <z, f`s>:r}))}"

end