src/HOL/TLA/Stfun.thy
author wenzelm
Sat, 29 Dec 2001 13:14:11 +0100
changeset 12607 16b63730cfbb
parent 12338 de0f4a63baa5
child 17309 c43ed29bd197
permissions -rw-r--r--
update by Stephan Merz;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     1
(* 
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     2
    File:	 TLA/Stfun.thy
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     3
    Author:      Stephan Merz
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
     4
    Copyright:   1998 University of Munich
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     5
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     6
    Theory Name: Stfun
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     7
    Logic Image: HOL
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     8
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
     9
States and state functions for TLA as an "intensional" logic.
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    10
*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    11
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    12
Stfun  =  Intensional +
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    13
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    14
types
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    15
    state
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    16
    'a stfun = "state => 'a"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    17
    stpred   = "bool stfun"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    18
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    19
arities
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 11703
diff changeset
    20
  state :: type
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    21
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    22
instance
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    23
  state :: world
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    24
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    25
consts
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    26
  (* Formalizing type "state" would require formulas to be tagged with
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    27
     their underlying state space and would result in a system that is
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    28
     much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    29
     over state variables, and therefore one usually works with different
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    30
     state spaces within a single specification.) Instead, "state" is just
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    31
     an anonymous type whose only purpose is to provide "Skolem" constants.
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    32
     Moreover, we do not define a type of state variables separate from that
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    33
     of arbitrary state functions, again in order to simplify the definition
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    34
     of flexible quantification later on. Nevertheless, we need to distinguish
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    35
     state variables, mainly to define the enabledness of actions. The user
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    36
     identifies (tuples of) "base" state variables in a specification via the
12607
16b63730cfbb update by Stephan Merz;
wenzelm
parents: 12338
diff changeset
    37
     "meta predicate" basevars, which is defined here.
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    38
  *)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    39
  stvars    :: "'a stfun => bool"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    40
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    41
syntax
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    42
  "PRED"    :: lift => 'a                          ("PRED _")
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    43
  "_stvars" :: lift => bool                        ("basevars _")
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    44
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    45
translations
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    46
  "PRED P"   =>  "(P::state => _)"
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    47
  "_stvars"  ==  "stvars"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    48
12607
16b63730cfbb update by Stephan Merz;
wenzelm
parents: 12338
diff changeset
    49
defs
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    50
  (* Base variables may be assigned arbitrary (type-correct) values. 
12607
16b63730cfbb update by Stephan Merz;
wenzelm
parents: 12338
diff changeset
    51
     Note that vs may be a tuple of variables. The correct identification
16b63730cfbb update by Stephan Merz;
wenzelm
parents: 12338
diff changeset
    52
     of base variables is up to the user who must take care not to
16b63730cfbb update by Stephan Merz;
wenzelm
parents: 12338
diff changeset
    53
     introduce an inconsistency. For example, "basevars (x,x)" would
16b63730cfbb update by Stephan Merz;
wenzelm
parents: 12338
diff changeset
    54
     definitely be inconsistent.
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    55
  *)
12607
16b63730cfbb update by Stephan Merz;
wenzelm
parents: 12338
diff changeset
    56
  basevars_def	"stvars vs == range vs = UNIV"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    57
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    58
end