src/ZF/UNITY/State.thy

converted domrange to Isar and merged with equalities

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

Formalizes UNITY-program states using dependent types so that:
 - variables are typed.
 - the state space is uniform, common to all defined programs.
 - variables can be quantified over.
*)

State = UNITYMisc +

consts var::i
datatype var = Var("i:list(nat)")
         type_intrs "[list_nat_into_univ]"

consts
  type_of :: i=>i
  some    :: i
  state   :: i
  st_set  :: i =>o
translations
  "state" == "Pi(var, type_of)"

defs  
  (* To prevent typing conditions (like `A<=state') from
     being used in combination with the rules `constrains_weaken', etc. *)
  st_set_def "st_set(A) == A<=state"

rules
  some_assume "some:state"

(***
REMARKS:
  1. The reason of indexing variables by lists instead of integers is that,
at the time I was writing this theory, translations like `foo == Var(#1)'
mysteriously provoke a syntactical error. Such translations are used
for introducing variable names when specifying programs.

  2. State space `state' is required to be not empty. This requirement
can be achieved by definition: the space "PROD x:var. type_of(x) Un {0}"
includes the state `lam x:state. 0'. However, such definition leads to
complications later during program type-chinking. For example, to prove
that the assignment `foo:=#1' is well typed, for `foo' an integer
variable, we would have to show two things: (a) that #1 is an integer
but also (b) that #1 is different from 0. Hence axiom `some_assume'.
***)
end