src/HOL/TLA/Init.thy

tuned concrete syntax -- abbreviation/const_syntax;

(*
    File:        TLA/Init.thy
    ID:          $Id$
    Author:      Stephan Merz
    Copyright:   1998 University of Munich

    Theory Name: Init
    Logic Image: HOL

Introduces type of temporal formulas. Defines interface between
temporal formulas and its "subformulas" (state predicates and actions).
*)

theory Init
imports Action
begin

typedecl behavior
instance behavior :: world ..

types
  temporal = "behavior form"


consts
  Initial     :: "('w::world => bool) => temporal"
  first_world :: "behavior => ('w::world)"
  st1         :: "behavior => state"
  st2         :: "behavior => state"

syntax
  TEMP       :: "lift => 'a"                          ("(TEMP _)")
  "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)

translations
  "TEMP F"   => "(F::behavior => _)"
  "_Init"    == "Initial"
  "sigma |= Init F"  <= "_Init F sigma"

defs
  Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
  fw_temp_def: "first_world == %sigma. sigma"
  fw_stp_def:  "first_world == st1"
  fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"

ML {* use_legacy_bindings (the_context ()) *}

end