# Theory Action

```(*  Title:      HOL/TLA/Action.thy
Author:     Stephan Merz
*)

section ‹The action level of TLA as an Isabelle theory›

theory Action
imports Stfun
begin

type_synonym 'a trfun = "state × state ⇒ 'a"
type_synonym action = "bool trfun"

instance prod :: (world, world) world ..

definition enabled :: "action ⇒ stpred"
where "enabled A s ≡ ∃u. (s,u) ⊨ A"

consts
before :: "'a stfun ⇒ 'a trfun"
after :: "'a stfun ⇒ 'a trfun"
unch :: "'a stfun ⇒ action"

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)

"_Enabled"    :: "lift ⇒ lift"                    ("(Enabled _)" [100] 100)

translations
"ACT A"            =>   "(A::state*state ⇒ _)"
"_before"          ==   "CONST before"
"_after"           ==   "CONST after"
"_prime"           =>   "_after"
"_unchanged"       ==   "CONST unch"
"_Enabled"         ==   "CONST enabled"
"s ⊨ Enabled A"   <=   "_Enabled A s"
"w ⊨ unchanged f" <=   "_unchanged f w"

axiomatization where
unl_before:    "(ACT \$v) (s,t) ≡ v s" and
unl_after:     "(ACT v\$) (s,t) ≡ v t" and
unchanged_def: "(s,t) ⊨ unchanged v ≡ (v t = v s)"

definition SqAct :: "[action, 'a stfun] ⇒ action"
where square_def: "SqAct A v ≡ ACT (A ∨ unchanged v)"

definition AnAct :: "[action, 'a stfun] ⇒ action"
where angle_def: "AnAct A v ≡ ACT (A ∧ ¬ unchanged v)"

syntax
"_SqAct" :: "[lift, lift] ⇒ lift"  ("([_]'_(_))" [0, 1000] 99)
"_AnAct" :: "[lift, lift] ⇒ lift"  ("(<_>'_(_))" [0, 1000] 99)
translations
"_SqAct" == "CONST SqAct"
"_AnAct" == "CONST AnAct"
"w ⊨ [A]_v" ↽ "_SqAct A v w"
"w ⊨ <A>_v" ↽ "_AnAct A v w"

(* The following assertion specializes "intI" for any world type
which is a pair, not just for "state * state".
*)

lemma actionI [intro!]:
assumes "⋀s t. (s,t) ⊨ A"
shows "⊢ A"
apply (rule assms intI prod.induct)+
done

lemma actionD [dest]: "⊢ A ⟹ (s,t) ⊨ A"
apply (erule intD)
done

lemma pr_rews [int_rewrite]:
"⊢ (#c)` = #c"
"⋀f. ⊢ f<x>` = f<x` >"
"⋀f. ⊢ f<x,y>` = f<x`,y` >"
"⋀f. ⊢ f<x,y,z>` = f<x`,y`,z` >"
"⊢ (∀x. P x)` = (∀x. (P x)`)"
"⊢ (∃x. P x)` = (∃x. (P x)`)"
by (rule actionI, unfold unl_after intensional_rews, rule refl)+

lemmas act_rews [simp] = unl_before unl_after unchanged_def pr_rews

lemmas action_rews = act_rews intensional_rews

(* ================ Functions to "unlift" action theorems into HOL rules ================ *)

ML ‹
(* The following functions are specialized versions of the corresponding
functions defined in Intensional.ML in that they introduce a
"world" parameter of the form (s,t) and apply additional rewrites.
*)

fun action_unlift ctxt th =
(rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD}))
handle THM _ => int_unlift ctxt th;

(* Turn  ⊢ A = B  into meta-level rewrite rule  A == B *)
val action_rewrite = int_rewrite

fun action_use ctxt th =
case Thm.concl_of th of
Const _ \$ (Const (\<^const_name>‹Valid›, _) \$ _) =>
(flatten (action_unlift ctxt th) handle THM _ => th)
| _ => th;
›

attribute_setup action_unlift =
‹Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))›
attribute_setup action_rewrite =
‹Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))›
attribute_setup action_use =
‹Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))›

(* =========================== square / angle brackets =========================== *)

lemma idle_squareI: "(s,t) ⊨ unchanged v ⟹ (s,t) ⊨ [A]_v"

lemma busy_squareI: "(s,t) ⊨ A ⟹ (s,t) ⊨ [A]_v"

lemma squareE [elim]:
"⟦ (s,t) ⊨ [A]_v; A (s,t) ⟹ B (s,t); v t = v s ⟹ B (s,t) ⟧ ⟹ B (s,t)"
apply (unfold square_def action_rews)
apply (erule disjE)
apply simp_all
done

lemma squareCI [intro]: "⟦ v t ≠ v s ⟹ A (s,t) ⟧ ⟹ (s,t) ⊨ [A]_v"
apply (unfold square_def action_rews)
apply (rule disjCI)
apply (erule (1) meta_mp)
done

lemma angleI [intro]: "⋀s t. ⟦ A (s,t); v t ≠ v s ⟧ ⟹ (s,t) ⊨ <A>_v"

lemma angleE [elim]: "⟦ (s,t) ⊨ <A>_v; ⟦ A (s,t); v t ≠ v s ⟧ ⟹ R ⟧ ⟹ R"
apply (unfold angle_def action_rews)
apply (erule conjE)
apply simp
done

lemma square_simulation:
"⋀f. ⟦ ⊢ unchanged f ∧ ¬B ⟶ unchanged g;
⊢ A ∧ ¬unchanged g ⟶ B
⟧ ⟹ ⊢ [A]_f ⟶ [B]_g"
apply clarsimp
apply (erule squareE)
done

lemma not_square: "⊢ (¬ [A]_v) = <¬A>_v"
by (auto simp: square_def angle_def)

lemma not_angle: "⊢ (¬ <A>_v) = [¬A]_v"
by (auto simp: square_def angle_def)

(* ============================== Facts about ENABLED ============================== *)

lemma enabledI: "⊢ A ⟶ \$Enabled A"

lemma enabledE: "⟦ s ⊨ Enabled A; ⋀u. A (s,u) ⟹ Q ⟧ ⟹ Q"
apply (unfold enabled_def)
apply (erule exE)
apply simp
done

lemma notEnabledD: "⊢ ¬\$Enabled G ⟶ ¬ G"

(* Monotonicity *)
lemma enabled_mono:
assumes min: "s ⊨ Enabled F"
and maj: "⊢ F ⟶ G"
shows "s ⊨ Enabled G"
apply (rule min [THEN enabledE])
apply (rule enabledI [action_use])
apply (erule maj [action_use])
done

(* stronger variant *)
lemma enabled_mono2:
assumes min: "s ⊨ Enabled F"
and maj: "⋀t. F (s,t) ⟹ G (s,t)"
shows "s ⊨ Enabled G"
apply (rule min [THEN enabledE])
apply (rule enabledI [action_use])
apply (erule maj)
done

lemma enabled_disj1: "⊢ Enabled F ⟶ Enabled (F ∨ G)"
by (auto elim!: enabled_mono)

lemma enabled_disj2: "⊢ Enabled G ⟶ Enabled (F ∨ G)"
by (auto elim!: enabled_mono)

lemma enabled_conj1: "⊢ Enabled (F ∧ G) ⟶ Enabled F"
by (auto elim!: enabled_mono)

lemma enabled_conj2: "⊢ Enabled (F ∧ G) ⟶ Enabled G"
by (auto elim!: enabled_mono)

lemma enabled_conjE:
"⟦ s ⊨ Enabled (F ∧ G); ⟦ s ⊨ Enabled F; s ⊨ Enabled G ⟧ ⟹ Q ⟧ ⟹ Q"
apply (frule enabled_conj1 [action_use])
apply (drule enabled_conj2 [action_use])
apply simp
done

lemma enabled_disjD: "⊢ Enabled (F ∨ G) ⟶ Enabled F ∨ Enabled G"

lemma enabled_disj: "⊢ Enabled (F ∨ G) = (Enabled F ∨ Enabled G)"
apply clarsimp
apply (rule iffI)
apply (erule enabled_disjD [action_use])
apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
done

lemma enabled_ex: "⊢ Enabled (∃x. F x) = (∃x. Enabled (F x))"

(* A rule that combines enabledI and baseE, but generates fewer instantiations *)
lemma base_enabled:
"⟦ basevars vs; ∃c. ∀u. vs u = c ⟶ A(s,u) ⟧ ⟹ s ⊨ Enabled A"
apply (erule exE)
apply (erule baseE)
apply (rule enabledI [action_use])
apply (erule allE)
apply (erule mp)
apply assumption
done

(* ======================= action_simp_tac ============================== *)

ML ‹
(* A dumb simplification-based tactic with just a little first-order logic:
should plug in only "very safe" rules that can be applied blindly.
Note that it applies whatever simplifications are currently active.
*)
fun action_simp_tac ctxt intros elims =
asm_full_simp_tac
(ctxt setloop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros)
@ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims)
@ [conjE,disjE,exE]))));
›

(* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)

ML ‹
(* "Enabled A" can be proven as follows:
- Assume that we know which state variables are "base variables"
this should be expressed by a theorem of the form "basevars (x,y,z,...)".
- Resolve this theorem with baseE to introduce a constant for the value of the
variables in the successor state, and resolve the goal with the result.
- Resolve with enabledI and do some rewriting.
- Solve for the unknowns using standard HOL reasoning.
The following tactic combines these steps except the final one.
*)

fun enabled_tac ctxt base_vars =
clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
›

method_setup enabled = ‹
Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
›

(* Example *)

lemma
assumes "basevars (x,y,z)"
shows "⊢ x ⟶ Enabled (\$x ∧ (y\$ = #False))"
apply (enabled assms)
apply auto
done

end
```