Theory Action

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

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"

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

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

  "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)"

  "_SqAct" :: "[lift, lift]  lift"  ("([_]'_(_))" [0, 1000] 99)
  "_AnAct" :: "[lift, lift]  lift"  ("(<_>'_(_))" [0, 1000] 99)
  "_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)+

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

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_nameValid, _) $ _) =>
              (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

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)

lemma angleI [intro]: "s t.  A (s,t); v t  v s   (s,t)  <A>_v"
  by (simp add: angle_def)

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

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)

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"
  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

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])

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

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

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])+

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

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

  assumes "basevars (x,y,z)"
  shows " x  Enabled ($x  (y$ = #False))"
  apply (enabled assms)
  apply auto