(* Title: HOL/TLA/Action.thy
Author: Stephan Merz
Copyright: 1998 University of Munich
*)
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 \ _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` = f"
"\f. \ f` = f"
"\f. \ f` = f"
"\ (\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 \<turnstile> 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 (
🍋‹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"
by (simp add: square_def)
lemma busy_squareI:
"(s,t) \ A \ (s,t) \ [A]_v"
by (simp add: square_def)
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) \ _v"
by (simp add: angle_def)
lemma angleE [elim]:
"\ (s,t) \ _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)
apply (auto simp add: square_def)
done
lemma not_square:
"\ (\ [A]_v) = <\A>_v"
by (auto simp: square_def angle_def)
lemma not_angle:
"\ (\ _v) = [\A]_v"
by (auto simp: square_def angle_def)
(* ============================== Facts about ENABLED ============================== *)
lemma enabledI:
"\ A \ $Enabled A"
by (auto simp add: enabled_def)
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"
by (auto simp add: enabled_def)
(* 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"
by (auto simp add: enabled_def)
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))"
by (force simp add: enabled_def)
(* 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 |> Simplifier.set_loop (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
