src/HOL/TLA/Stfun.thy
changeset 17309 c43ed29bd197
parent 12607 16b63730cfbb
child 21624 6f79647cf536
     1.1 --- a/src/HOL/TLA/Stfun.thy	Wed Sep 07 20:22:15 2005 +0200
     1.2 +++ b/src/HOL/TLA/Stfun.thy	Wed Sep 07 20:22:39 2005 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4 -(* 
     1.5 -    File:	 TLA/Stfun.thy
     1.6 +(*
     1.7 +    File:        TLA/Stfun.thy
     1.8 +    ID:          $Id$
     1.9      Author:      Stephan Merz
    1.10      Copyright:   1998 University of Munich
    1.11  
    1.12 @@ -9,18 +10,18 @@
    1.13  States and state functions for TLA as an "intensional" logic.
    1.14  *)
    1.15  
    1.16 -Stfun  =  Intensional +
    1.17 +theory Stfun
    1.18 +imports Intensional
    1.19 +begin
    1.20 +
    1.21 +typedecl state
    1.22 +
    1.23 +instance state :: world ..
    1.24  
    1.25  types
    1.26 -    state
    1.27 -    'a stfun = "state => 'a"
    1.28 -    stpred   = "bool stfun"
    1.29 +  'a stfun = "state => 'a"
    1.30 +  stpred  = "bool stfun"
    1.31  
    1.32 -arities
    1.33 -  state :: type
    1.34 -
    1.35 -instance
    1.36 -  state :: world
    1.37  
    1.38  consts
    1.39    (* Formalizing type "state" would require formulas to be tagged with
    1.40 @@ -39,20 +40,22 @@
    1.41    stvars    :: "'a stfun => bool"
    1.42  
    1.43  syntax
    1.44 -  "PRED"    :: lift => 'a                          ("PRED _")
    1.45 -  "_stvars" :: lift => bool                        ("basevars _")
    1.46 +  "PRED"    :: "lift => 'a"                          ("PRED _")
    1.47 +  "_stvars" :: "lift => bool"                        ("basevars _")
    1.48  
    1.49  translations
    1.50    "PRED P"   =>  "(P::state => _)"
    1.51    "_stvars"  ==  "stvars"
    1.52  
    1.53  defs
    1.54 -  (* Base variables may be assigned arbitrary (type-correct) values. 
    1.55 +  (* Base variables may be assigned arbitrary (type-correct) values.
    1.56       Note that vs may be a tuple of variables. The correct identification
    1.57       of base variables is up to the user who must take care not to
    1.58       introduce an inconsistency. For example, "basevars (x,x)" would
    1.59       definitely be inconsistent.
    1.60    *)
    1.61 -  basevars_def	"stvars vs == range vs = UNIV"
    1.62 +  basevars_def:  "stvars vs == range vs = UNIV"
    1.63 +
    1.64 +ML {* use_legacy_bindings (the_context ()) *}
    1.65  
    1.66  end