src/HOL/TLA/Action.ML

A formalization of TLA in HOL -- by Stephan Merz;

(* 
    File:	 Action.ML
    Author:      Stephan Merz
    Copyright:   1997 University of Munich

Lemmas and tactics for TLA actions.
*)

val act_rews = [pairSF_def RS eq_reflection,unl_before,unl_after,unchanged_def,
                pr_con,pr_before,pr_lift,pr_lift2,pr_lift3,pr_all,pr_ex];

val action_rews = act_rews @ intensional_rews;

qed_goal "actionI" Action.thy "(!!s t. ([[s,t]] |= A)) ==> A"
  (fn [prem] => [REPEAT (resolve_tac [prem,intI,state2_ext] 1)]);

qed_goal "actionD" Action.thy "A ==> ([[s,t]] |= A)"
  (fn [prem] => [REPEAT (resolve_tac [prem,intD] 1)]);



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

(* Basic unlifting introduces a world parameter and applies basic rewrites, e.g.
   A .= B    gets   ([[s,t]] |= A) = ([[s,t]] |= B)
   A .-> B   gets   ([[s,t]] |= A) --> ([[s,t]] |= B)
*)
fun action_unlift th = rewrite_rule action_rews (th RS actionD);

(* A .-> B   becomes   A [[s,t]] ==> B [[s,t]] *)
fun action_mp th = zero_var_indexes ((action_unlift th) RS mp);

(* A .-> B   becomes   [| A[[s,t]]; B[[s,t]] ==> R |] ==> R 
   so that it can be used as an elimination rule
*)
fun action_impE th = zero_var_indexes ((action_unlift th) RS impE);

(* A .& B .-> C  becomes  [| A[[s,t]]; B[[s,t]] |] ==> C[[s,t]] *)
fun action_conjmp th = zero_var_indexes (conjI RS (action_mp th));

(* A .& B .-> C  becomes  [| A[[s,t]]; B[[s,t]]; (C[[s,t]] ==> R) |] ==> R *)
fun action_conjimpE th = zero_var_indexes (conjI RS (action_impE th));

(* Turn  A .= B  into meta-level rewrite rule  A == B *)
fun action_rewrite th = (rewrite_rule action_rews (th RS inteq_reflection));

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

(* Make the simplifier use action_unlift rather than int_unlift 
   when action simplifications are added.
*)
fun maybe_unlift th =
    (case concl_of th of
         Const("TrueInt",_) $ p 
           => (action_unlift th
                  handle _ => int_unlift th)
       | _ => th);

simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift);

(* make act_rews be always active -- intensional_rews has been added before *)
Addsimps act_rews;

use "cladata.ML";        (* local version! *)

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

(* A dumb simplification 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 i =
    (asm_full_simp_tac 
         (ss setloop ((resolve_tac (intros @ [refl,impI,conjI,actionI,allI]))
		      ORELSE' (eresolve_tac (elims @ [conjE,disjE,exE_prop]))))
         i);
(* default version without additional plug-in rules *)
fun Action_simp_tac i = (action_simp_tac (!simpset) [] [] i);


(* ==================== Simplification of abstractions ==================== *)

(* Somewhat obscure simplifications, rarely necessary to get rid
   of abstractions that may be introduced by higher-order unification.
*)

qed_goal "pr_con_abs" Action.thy "(%w. c)` .= #c"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac (con_abs::action_rews),
            rtac refl 1
           ]);

qed_goal "pr_lift_abs" Action.thy "(%w. f(x w))` .= f[x`]"
  (fn _ => [rtac actionI 1,
              (* give all rewrites to the engine and it loops! *)
            rewrite_goals_tac intensional_rews,
            rewtac lift_abs,
            rewtac pr_lift,
            rewtac unl_lift,
            rtac refl 1
           ]);

qed_goal "pr_lift2_abs" Action.thy "(%w. f(x w) (y w))` .= f[x`,y`]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift2_abs,
            rewtac pr_lift2,
            rewtac unl_lift2,
            rtac refl 1
           ]);

qed_goal "pr_lift2_abs_con1" Action.thy "(%w. f x (y w))` .= f[#x, y`]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift2_abs_con1,
            rewtac pr_lift2,
            rewtac unl_lift2,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

qed_goal "pr_lift2_abs_con2" Action.thy "(%w. f (x w) y)` .= f[x`, #y]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift2_abs_con2,
            rewtac pr_lift2,
            rewtac unl_lift2,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

qed_goal "pr_lift3_abs" Action.thy "(%w. f(x w) (y w) (z w))` .= f[x`,y`,z`]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift3_abs,
            rewtac pr_lift3,
            rewtac unl_lift3,
            rtac refl 1
           ]);

qed_goal "pr_lift3_abs_con1" Action.thy "(%w. f x (y w) (z w))` .= f[#x, y`, z`]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift3_abs_con1,
            rewtac pr_lift3,
            rewtac unl_lift3,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

qed_goal "pr_lift3_abs_con2" Action.thy "(%w. f (x w) y (z w))` .= f[x`, #y, z`]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift3_abs_con2,
            rewtac pr_lift3,
            rewtac unl_lift3,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

qed_goal "pr_lift3_abs_con3" Action.thy "(%w. f (x w) (y w) z)` .= f[x`, y`, #z]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift3_abs_con3,
            rewtac pr_lift3,
            rewtac unl_lift3,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

qed_goal "pr_lift3_abs_con12" Action.thy "(%w. f x y (z w))` .= f[#x, #y, z`]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift3_abs_con12,
            rewtac pr_lift3,
            rewtac unl_lift3,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

qed_goal "pr_lift3_abs_con13" Action.thy "(%w. f x (y w) z)` .= f[#x, y`, #z]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift3_abs_con13,
            rewtac pr_lift3,
            rewtac unl_lift3,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

qed_goal "pr_lift3_abs_con23" Action.thy "(%w. f (x w) y z)` .= f[x`, #y, #z]"
  (fn _ => [rtac actionI 1,
            rewrite_goals_tac intensional_rews,
            rewtac lift3_abs_con23,
            rewtac pr_lift3,
            rewtac unl_lift3,
            rewtac pr_con,
            rewtac unl_con,
            rtac refl 1
           ]);

(* We don't add these as default rewrite rules, because they are
   rarely needed and may slow down automatic proofs.
*)
val pr_abs_rews = map (fn th => th RS inteq_reflection) 
                      [pr_con_abs,
                       pr_lift_abs,pr_lift2_abs,pr_lift2_abs_con1,pr_lift2_abs_con2,
                       pr_lift3_abs,pr_lift3_abs_con1,pr_lift3_abs_con2,pr_lift3_abs_con3,
                       pr_lift3_abs_con12,pr_lift3_abs_con13,pr_lift3_abs_con23];

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

qed_goalw "idle_squareI" Action.thy [square_def]
   "!!s t. ([[s,t]] |= unchanged v) ==> ([[s,t]] |= [A]_v)"
   (fn _ => [ Auto_tac() ]);

qed_goalw "busy_squareI" Action.thy [square_def]
   "!!s t. ([[s,t]] |= A) ==> ([[s,t]] |= [A]_v)"
   (fn _ => [ Auto_tac() ]);

qed_goalw "square_simulation" Action.thy [square_def]
   "[| unchanged f .& .~B .-> unchanged g;   \
\      A .& .~unchanged g .-> B              \
\   |] ==> [A]_f .-> [B]_g"
   (fn [p1,p2] => [Auto_tac(),
                   etac (action_conjimpE p2) 1,
                   etac swap 3, etac (action_conjimpE p1) 3,
                   ALLGOALS atac
                  ]);
                   
qed_goalw "not_square" Action.thy [square_def,angle_def]
   "(.~ [A]_v) .= <.~A>_v"
   (fn _ => [ Auto_tac() ]);

qed_goalw "not_angle" Action.thy [square_def,angle_def]
   "(.~ <A>_v) .= [.~A]_v"
   (fn _ => [ Auto_tac() ]);

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

qed_goalw "enabledI" Action.thy [enabled_def]
  "A [[s,t]] ==> (Enabled A) s"
  (fn prems => [ REPEAT (resolve_tac (exI::prems) 1) ]);

qed_goalw "enabledE" Action.thy [enabled_def]
  "[| (Enabled A) s; !!u. A[[s,u]] ==> PROP R |] ==> PROP R"
  (fn prems => [cut_facts_tac prems 1,
                etac exE_prop 1,
                resolve_tac prems 1, atac 1
               ]);

qed_goal "notEnabledD" Action.thy
  "!!G. ~ (Enabled G s) ==> ~ G [[s,t]]"
  (fn _ => [ auto_tac (action_css addsimps2 [enabled_def]) ]);

(* Monotonicity *)
qed_goal "enabled_mono" Action.thy
  "[| (Enabled F) s; F .-> G |] ==> (Enabled G) s"
  (fn [min,maj] => [rtac (min RS enabledE) 1,
                    rtac enabledI 1,
                    etac (action_mp maj) 1
                   ]);

(* stronger variant *)
qed_goal "enabled_mono2" Action.thy
   "[| (Enabled F) s; !!t. (F [[s,t]] ==> G[[s,t]] ) |] ==> (Enabled G) s"
   (fn [min,maj] => [rtac (min RS enabledE) 1,
		     rtac enabledI 1,
		     etac maj 1
		    ]);

qed_goal "enabled_disj1" Action.thy
  "!!s. (Enabled F) s ==> (Enabled (F .| G)) s"
  (fn _ => [etac enabled_mono 1, Auto_tac()
	   ]);

qed_goal "enabled_disj2" Action.thy
  "!!s. (Enabled G) s ==> (Enabled (F .| G)) s"
  (fn _ => [etac enabled_mono 1, Auto_tac()
	   ]);

qed_goal "enabled_conj1" Action.thy
  "!!s. (Enabled (F .& G)) s ==> (Enabled F) s"
  (fn _ => [etac enabled_mono 1, Auto_tac()
           ]);

qed_goal "enabled_conj2" Action.thy
  "!!s. (Enabled (F .& G)) s ==> (Enabled G) s"
  (fn _ => [etac enabled_mono 1, Auto_tac()
           ]);

qed_goal "enabled_conjE" Action.thy
  "[| (Enabled (F .& G)) s; [| (Enabled F) s; (Enabled G) s |] ==> PROP R |] ==> PROP R"
  (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
                etac enabled_conj1 1, etac enabled_conj2 1]);

qed_goal "enabled_disjD" Action.thy
  "!!s. (Enabled (F .| G)) s ==> ((Enabled F) s) | ((Enabled G) s)"
  (fn _ => [etac enabledE 1,
            auto_tac (action_css addSDs2 [notEnabledD] addSEs2 [enabledI])
           ]);

qed_goal "enabled_disj" Action.thy
  "(Enabled (F .| G)) s = ( (Enabled F) s | (Enabled G) s )"
  (fn _ => [rtac iffI 1,
            etac enabled_disjD 1,
            REPEAT (eresolve_tac [disjE,enabled_disj1,enabled_disj2] 1)
           ]);

qed_goal "enabled_ex" Action.thy
  "(Enabled (REX x. F x)) s = (EX x. (Enabled (F x)) s)"
  (fn _ => [ auto_tac (action_css addsimps2 [enabled_def]) ]);
	    

(* A rule that combines enabledI and baseE, but generates fewer possible instantiations *)
qed_goal "base_enabled" Action.thy
  "[| base_var(v); !!u. v u = c s ==> A [[s,u]] |] ==> Enabled A s"
  (fn prems => [cut_facts_tac prems 1,
		etac baseE 1, rtac enabledI 1,
		REPEAT (ares_tac prems 1)]);


(* ---------------- 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 "base_var <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.
   - E-resolve with PairVarE so that we have one constant per variable.
   - 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 i =
    EVERY [(* apply actionI (plus rewriting) if the goal is of the form $(Enabled A),
	      do nothing if it is of the form (Enabled A) s *)
	   TRY ((rtac actionI i) THEN (SELECT_GOAL (rewrite_goals_tac action_rews) i)),
	   rtac (base_vars RS base_enabled) i,
	   REPEAT_DETERM (etac PairVarE i),
	   (SELECT_GOAL (rewrite_goals_tac action_rews) i)
	  ];

(* Example of use:

val [prem] = goal Action.thy "base_var <x,y,z> ==> $x .-> $Enabled ($x .& (y$ .= #False))";
by (REPEAT ((CHANGED (Action_simp_tac 1)) ORELSE (enabled_tac prem 1)));

*)