src/HOL/TLA/Stfun.thy
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 6255 db63752140c7
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 TLA/Stfun.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: Stfun
wenzelm@3807
     7
    Logic Image: HOL
wenzelm@3807
     8
wenzelm@3807
     9
States and state functions for TLA
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@3807
    12
Stfun  =  Prod +
wenzelm@3807
    13
wenzelm@3807
    14
types
wenzelm@3807
    15
    state
wenzelm@3807
    16
    'a stfun = "state => 'a"
wenzelm@3807
    17
    stpred   = "bool stfun"
wenzelm@3807
    18
wenzelm@3807
    19
arities
wenzelm@3807
    20
    state :: term
wenzelm@3807
    21
wenzelm@3807
    22
consts
wenzelm@3807
    23
  (* For simplicity, we do not syntactically distinguish between state variables
wenzelm@3807
    24
     and state functions, and treat "state" as an anonymous type. But we need a 
wenzelm@3807
    25
     "meta-predicate" to identify "base" state variables that represent the state
wenzelm@3807
    26
     components of a system, in particular to define the enabledness of actions.
wenzelm@3807
    27
  *)
wenzelm@3807
    28
  base_var  :: "'a stfun => bool"
wenzelm@3807
    29
wenzelm@3807
    30
  (* lift tupling to state functions *)
wenzelm@3807
    31
  pairSF    :: "['a stfun, 'b stfun] => ('a * 'b) stfun"
wenzelm@3807
    32
wenzelm@3807
    33
syntax
wenzelm@3807
    34
  "@tupleSF"     :: "args => ('a * 'b) stfun"  ("(1<_>)")
wenzelm@3807
    35
wenzelm@3807
    36
translations
wenzelm@3807
    37
  "<x,y,z>"   == "<x, <y,z> >"
wenzelm@3807
    38
  "<x,y>"     == "pairSF x y"
wenzelm@3807
    39
  "<x>"       => "x"
wenzelm@3807
    40
wenzelm@3807
    41
rules
wenzelm@3807
    42
  (* tupling *)
wenzelm@3807
    43
  pairSF_def  "<v,w>(s) = (v(s),w(s))"
wenzelm@3807
    44
wenzelm@3807
    45
  (* "base" variables may be assigned arbitrary values by states.
wenzelm@3807
    46
     NB: It's really stronger than that because "u" doesn't depend 
wenzelm@3807
    47
         on either c or v. In particular, if "==>" were replaced
wenzelm@3807
    48
         with "==", base_pair would (still) not be derivable.
wenzelm@3807
    49
  *)
wenzelm@3807
    50
  base_var    "base_var v ==> EX u. v u = c"
wenzelm@3807
    51
wenzelm@3807
    52
  (* a tuple of variables is "base" if each variable is "base" *)
wenzelm@3807
    53
  base_pair   "base_var <v,w> = (base_var v & base_var w)"
wenzelm@3807
    54
end
wenzelm@3807
    55
wenzelm@3807
    56
ML