# File Action.ML

    (*
        File:        Action.ML
        ID:          $Id: Action.ML,v 1.10 2005/09/07 18:22:39 wenzelm Exp $
        Author:      Stephan Merz
        Copyright:   1997 University of Munich

    Lemmas and tactics for TLA actions.
    *)

    (* The following assertion specializes "intI" for any world type
       which is a pair, not just for "state * state".
    *)
    val [prem] = goal (the_context ()) "(!!s t. (s,t) |= A) ==> |- A";
    by (REPEAT (resolve_tac [prem,intI,prod_induct] 1));
    qed "actionI";

    Goal "|- A ==> (s,t) |= A";
    by (etac intD 1);
    qed "actionD";

    local
      fun prover s = prove_goal (the_context ()) s
                        (fn _ => [rtac actionI 1,
                                  rewrite_goals_tac (unl_after::intensional_rews),
                                  rtac refl 1])
    in
      val pr_rews = map (int_rewrite o prover)
        [ "|- (#c)` = #c",
          "|- f<x>` = f<x` >",
          "|- f<x,y>` = f<x`,y` >",
          "|- f<x,y,z>` = f<x`,y`,z` >",
          "|- (! x. P x)` = (! x. (P x)`)",
          "|- (? x. P x)` = (? x. (P x)`)"
        ]
    end;

    val act_rews = [unl_before,unl_after,unchanged_def] @ pr_rews;
    Addsimps act_rews;

    val action_rews = act_rews @ intensional_rews;

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

    (* 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 th =
        (rewrite_rule action_rews (th RS actionD))
        handle _ => int_unlift th;

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

    fun action_use th =
        case (concl_of th) of
          Const _ $ (Const ("Intensional.Valid", _) $ _) =>
                  ((flatten (action_unlift th)) handle _ => th)
        | _ => th;

    (* ===================== Update simpset and classical prover ============================= *)

    AddSIs [actionI];
    AddDs  [actionD];

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

    Goalw [square_def] "(s,t) |= unchanged v ==> (s,t) |= [A]_v";
    by (Asm_full_simp_tac 1);
    qed "idle_squareI";

    Goalw [square_def] "(s,t) |= A ==> (s,t) |= [A]_v";
    by (Asm_simp_tac 1);
    qed "busy_squareI";

    val prems = goal (the_context ())
      "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)";
    by (cut_facts_tac prems 1);
    by (rewrite_goals_tac (square_def::action_rews));
    by (etac disjE 1);
    by (REPEAT (eresolve_tac prems 1));
    qed "squareE";

    val prems = goalw (the_context ()) (square_def::action_rews)
      "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v";
    by (rtac disjCI 1);
    by (eresolve_tac prems 1);
    qed "squareCI";

    goalw (the_context ()) [angle_def]
      "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v";
    by (Asm_simp_tac 1);
    qed "angleI";

    val prems = goalw (the_context ()) (angle_def::action_rews)
      "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R";
    by (cut_facts_tac prems 1);
    by (etac conjE 1);
    by (REPEAT (ares_tac prems 1));
    qed "angleE";

    AddIs [angleI, squareCI];
    AddEs [angleE, squareE];

    goal (the_context ())
       "!!f. [| |- unchanged f & ~B --> unchanged g;   \
    \           |- A & ~unchanged g --> B              \
    \        |] ==> |- [A]_f --> [B]_g";
    by (Clarsimp_tac 1);
    by (etac squareE 1);
    by (auto_tac (claset(), simpset() addsimps [square_def]));
    qed "square_simulation";

    goalw (the_context ()) [square_def,angle_def]
       "|- (~ [A]_v) = <~A>_v";
    by Auto_tac;
    qed "not_square";

    goalw (the_context ()) [square_def,angle_def]
       "|- (~ <A>_v) = [~A]_v";
    by Auto_tac;
    qed "not_angle";

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

    goal (the_context ()) "|- A --> $Enabled A";
    by (auto_tac (claset(), simpset() addsimps [enabled_def]));
    qed "enabledI";

    val prems = goalw (the_context ()) [enabled_def]
      "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q";
    by (cut_facts_tac prems 1);
    by (etac exE 1);
    by (resolve_tac prems 1);
    by (atac 1);
    qed "enabledE";

    goal (the_context ()) "|- ~$Enabled G --> ~ G";
    by (auto_tac (claset(), simpset() addsimps [enabled_def]));
    qed "notEnabledD";

    (* Monotonicity *)
    val [min,maj] = goal (the_context ())
      "[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G";
    by (rtac (min RS enabledE) 1);
    by (rtac (action_use enabledI) 1);
    by (etac (action_use maj) 1);
    qed "enabled_mono";

    (* stronger variant *)
    val [min,maj] = goal (the_context ())
      "[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G";
    by (rtac (min RS enabledE) 1);
    by (rtac (action_use enabledI) 1);
    by (etac maj 1);
    qed "enabled_mono2";

    goal (the_context ()) "|- Enabled F --> Enabled (F | G)";
    by (auto_tac (claset() addSEs [enabled_mono], simpset()));
    qed "enabled_disj1";

    goal (the_context ()) "|- Enabled G --> Enabled (F | G)";
    by (auto_tac (claset() addSEs [enabled_mono], simpset()));
    qed "enabled_disj2";

    goal (the_context ()) "|- Enabled (F & G) --> Enabled F";
    by (auto_tac (claset() addSEs [enabled_mono], simpset()));
    qed "enabled_conj1";

    goal (the_context ()) "|- Enabled (F & G) --> Enabled G";
    by (auto_tac (claset() addSEs [enabled_mono], simpset()));
    qed "enabled_conj2";

    val prems = goal (the_context ())
      "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q";
    by (cut_facts_tac prems 1);
    by (resolve_tac prems 1);
    by (etac (action_use enabled_conj1) 1);
    by (etac (action_use enabled_conj2) 1);
    qed "enabled_conjE";

    goal (the_context ()) "|- Enabled (F | G) --> Enabled F | Enabled G";
    by (auto_tac (claset(), simpset() addsimps [enabled_def]));
    qed "enabled_disjD";

    goal (the_context ()) "|- Enabled (F | G) = (Enabled F | Enabled G)";
    by (Clarsimp_tac 1);
    by (rtac iffI 1);
    by (etac (action_use enabled_disjD) 1);
    by (REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1));
    qed "enabled_disj";

    goal (the_context ()) "|- Enabled (EX x. F x) = (EX x. Enabled (F x))";
    by (force_tac (claset(), simpset() addsimps [enabled_def]) 1);
    qed "enabled_ex";

    (* A rule that combines enabledI and baseE, but generates fewer instantiations *)
    val prems = goal (the_context ())
      "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A";
    by (cut_facts_tac prems 1);
    by (etac exE 1);
    by (etac baseE 1);
    by (rtac (action_use enabledI) 1);
    by (etac allE 1);
    by (etac mp 1);
    by (atac 1);
    qed "base_enabled";

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

    (* 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 ss intros elims =
        asm_full_simp_tac
             (ss setloop ((resolve_tac ((map action_use intros)
                                        @ [refl,impI,conjI,actionI,intI,allI]))
                          ORELSE' (eresolve_tac ((map action_use elims)
                                                 @ [conjE,disjE,exE]))));

    (* default version without additional plug-in rules *)
    val Action_simp_tac = action_simp_tac (simpset()) [] [];

    (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
    (* "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 base_vars =
        clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());

    (* Example:

    val [prem] = goal (the_context ()) "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
    by (enabled_tac prem 1);
    by Auto_tac;

    *)