(* 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