src/HOL/TLA/Action.thy

A formalization of TLA in HOL -- by Stephan Merz;

(* 
    File:	 TLA/Action.thy
    Author:      Stephan Merz
    Copyright:   1997 University of Munich

    Theory Name: Action
    Logic Image: HOL

Define the action level of TLA as an Isabelle theory.
*)

Action  =  Intensional + Stfun +

types
    state2      (* intention: pair of states *)
    'a trfct = "('a, state2) term"
    action   = "state2 form"

arities
    state2 :: world
    
consts
  mkstate2      :: "[state,state] => state2"  ("([[_,_]])")

  (* lift state variables to transition functions *)
  before        :: "'a stfun => 'a trfct"            ("($_)"  [100] 99)
  after         :: "'a stfun => 'a trfct"            ("(_$)"  [100] 99)
  unchanged     :: "'a stfun => action"

  (* Priming *)
  prime         :: "'a trfct => 'a trfct"            ("(_`)" [90] 89)

  SqAct         :: "[action, 'a stfun] => action"    ("([_]'_(_))" [0,60] 59)
  AnAct         :: "[action, 'a stfun] => action"    ("(<_>'_(_))" [0,60] 59)
  Enabled       :: "action => stpred"

rules
  (* The following says that state2 is generated by mkstate2 *)
  state2_ext    "(!!s t. [[s,t]] |= (A::action)) ==> (st::state2) |= A"

  unl_before    "($v) [[s,t]] == v s"
  unl_after     "(v$) [[s,t]] == v t"

  pr_con        "(#c)` == #c"
  pr_before     "($v)` == v$"
  (* no corresponding rule for "after"! *)
  pr_lift       "(F[x])` == F[x`]"
  pr_lift2      "(F[x,y])` == F[x`,y`]"
  pr_lift3      "(F[x,y,z])` == F[x`,y`,z`]"
  pr_all        "(RALL x. P(x))` == (RALL x. P(x)`)"
  pr_ex         "(REX x. P(x))` == (REX x. P(x)`)"

  unchanged_def "(unchanged v) [[s,t]] == (v t = v s)"
  square_def    "[A]_v == A .| unchanged v"
  angle_def     "<A>_v == A .& .~ unchanged v"

  enabled_def   "(Enabled A) s  ==  EX u. A[[s,u]]"
end