# Theory Init

Up to index of Isabelle/HOL/TLA

theory Init
imports Action
uses [Init.ML]
begin

    (*
        File:        TLA/Init.thy
        ID:          $Id: Init.thy,v 1.4 2005/09/07 18:22:39 wenzelm Exp $
        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

theorem Init_stp_act:

      |- Init $P = (Init P)

theorem Init_stp_act_rev:

      Init P == Init $P

theorem Init_temp:

      |- Init F = F

theorem Init_stp:

      (sigma |= Init P) = P (st1 sigma)

theorem Init_act:

      (sigma |= Init A) = A (st1 sigma, st2 sigma)