# Theory Action

Up to index of Isabelle/HOL/TLA

theory Action
imports Stfun
uses [Action.ML]
begin

    (*
        File:        TLA/Action.thy
        ID:          $Id: Action.thy,v 1.5 2005/09/07 18:22:39 wenzelm Exp $
        Author:      Stephan Merz
        Copyright:   1998 University of Munich

        Theory Name: Action
        Logic Image: HOL

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

    theory Action
    imports Stfun
    begin

    (** abstract syntax **)

    types
      'a trfun = "(state * state) => 'a"
      action   = "bool trfun"

    instance
      "*" :: (world, world) world ..

    consts
      (** abstract syntax **)
      before        :: "'a stfun => 'a trfun"
      after         :: "'a stfun => 'a trfun"
      unch          :: "'a stfun => action"

      SqAct         :: "[action, 'a stfun] => action"
      AnAct         :: "[action, 'a stfun] => action"
      enabled       :: "action => stpred"

    (** concrete syntax **)

    syntax
      (* Syntax for writing action expressions in arbitrary contexts *)
      "ACT"         :: "lift => 'a"                      ("(ACT _)")

      "_before"     :: "lift => lift"                    ("($_)"  [100] 99)
      "_after"      :: "lift => lift"                    ("(_$)"  [100] 99)
      "_unchanged"  :: "lift => lift"                    ("(unchanged _)" [100] 99)

      (*** Priming: same as "after" ***)
      "_prime"      :: "lift => lift"                    ("(_`)" [100] 99)

      "_SqAct"      :: "[lift, lift] => lift"            ("([_]'_(_))" [0,1000] 99)
      "_AnAct"      :: "[lift, lift] => lift"            ("(<_>'_(_))" [0,1000] 99)
      "_Enabled"    :: "lift => lift"                    ("(Enabled _)" [100] 100)

    translations
      "ACT A"            =>   "(A::state*state => _)"
      "_before"          ==   "before"
      "_after"           ==   "after"
      "_prime"           =>   "_after"
      "_unchanged"       ==   "unch"
      "_SqAct"           ==   "SqAct"
      "_AnAct"           ==   "AnAct"
      "_Enabled"         ==   "enabled"
      "w |= [A]_v"       <=   "_SqAct A v w"
      "w |= <A>_v"       <=   "_AnAct A v w"
      "s |= Enabled A"   <=   "_Enabled A s"
      "w |= unchanged f" <=   "_unchanged f w"

    axioms
      unl_before:    "(ACT $v) (s,t) == v s"
      unl_after:     "(ACT v$) (s,t) == v t"

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

      enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem actionI:

      (!!s t. A (s, t)) ==> |- A

theorem actionD:

      |- A ==> A (s, t)

theorem idle_squareI:

      (s, t) |= unchanged v ==> (s, t) |= [A]_v

theorem busy_squareI:

      A (s, t) ==> (s, t) |= [A]_v

theorem squareE:

      [| (s, t) |= [A]_v; A (s, t) ==> B (s, t); v t = v s ==> B (s, t) |]
      ==> B (s, t)

theorem squareCI:

      (v t ≠ v s ==> A (s, t)) ==> (s, t) |= [A]_v

theorem angleI:

      [| A (s, t); v t ≠ v s |] ==> (s, t) |= <A>_v

theorem angleE:

      [| (s, t) |= <A>_v; [| A (s, t); v t ≠ v s |] ==> R |] ==> R

theorem square_simulation:

      [| |- unchanged f ∧ ¬ B --> unchanged g; |- A ∧ ¬ unchanged g --> B |]
      ==> |- [A]_f --> [B]_g

theorem not_square:

      |- (¬ [A]_v) = <¬ A>_v

theorem not_angle:

      |- (¬ <A>_v) = [¬ A]_v

theorem enabledI:

      |- A --> $Enabled A

theorem enabledE:

      [| s |= Enabled A; !!u. A (s, u) ==> Q |] ==> Q

theorem notEnabledD:

      |- ¬ $Enabled G --> ¬ G

theorem enabled_mono:

      [| s |= Enabled F; |- F --> G |] ==> s |= Enabled G

theorem enabled_mono2:

      [| s |= Enabled F; !!t. F (s, t) ==> G (s, t) |] ==> s |= Enabled G

theorem enabled_disj1:

      |- Enabled F --> Enabled (F ∨ G)

theorem enabled_disj2:

      |- Enabled G --> Enabled (F ∨ G)

theorem enabled_conj1:

      |- Enabled (F ∧ G) --> Enabled F

theorem enabled_conj2:

      |- Enabled (F ∧ G) --> Enabled G

theorem enabled_conjE:

      [| s |= Enabled (F ∧ G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q

theorem enabled_disjD:

      |- Enabled (F ∨ G) --> Enabled F ∨ Enabled G

theorem enabled_disj:

      |- Enabled (F ∨ G) = (Enabled F ∨ Enabled G)

theorem enabled_ex:

      |- Enabled (∃x. F x) = (∃x. Enabled F x)

theorem base_enabled:

      [| basevars vs; ∃c. ∀u. vs u = c --> A (s, u) |] ==> s |= Enabled A