src/HOL/TLA/Action.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14100 804be4c4b642
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
     1 (* 
     2     File:	 Action.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6 Lemmas and tactics for TLA actions.
     7 *)
     8 
     9 (* The following assertion specializes "intI" for any world type 
    10    which is a pair, not just for "state * state".
    11 *)
    12 val [prem] = goal thy "(!!s t. (s,t) |= A) ==> |- A";
    13 by (REPEAT (resolve_tac [prem,intI,prod_induct] 1));
    14 qed "actionI";
    15 
    16 Goal "|- A ==> (s,t) |= A";
    17 by (etac intD 1);
    18 qed "actionD";
    19 
    20 local
    21   fun prover s = prove_goal Action.thy s 
    22                     (fn _ => [rtac actionI 1, 
    23                               rewrite_goals_tac (unl_after::intensional_rews),
    24                               rtac refl 1])
    25 in
    26   val pr_rews = map (int_rewrite o prover)
    27     [ "|- (#c)` = #c",
    28       "|- f<x>` = f<x` >",
    29       "|- f<x,y>` = f<x`,y` >",
    30       "|- f<x,y,z>` = f<x`,y`,z` >",
    31       "|- (! x. P x)` = (! x. (P x)`)",
    32       "|- (? x. P x)` = (? x. (P x)`)"
    33     ]
    34 end;
    35 
    36 val act_rews = [unl_before,unl_after,unchanged_def] @ pr_rews;
    37 Addsimps act_rews;
    38 
    39 val action_rews = act_rews @ intensional_rews;
    40 
    41 (* ================ Functions to "unlift" action theorems into HOL rules ================ *)
    42 
    43 (* The following functions are specialized versions of the corresponding
    44    functions defined in Intensional.ML in that they introduce a
    45    "world" parameter of the form (s,t) and apply additional rewrites.
    46 *)
    47 fun action_unlift th = 
    48     (rewrite_rule action_rews (th RS actionD)) 
    49     handle _ => int_unlift th;
    50 
    51 (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
    52 val action_rewrite = int_rewrite;
    53 
    54 fun action_use th =
    55     case (concl_of th) of
    56       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    57               ((flatten (action_unlift th)) handle _ => th)
    58     | _ => th;
    59 
    60 (* ===================== Update simpset and classical prover ============================= *)
    61 
    62 AddSIs [actionI];
    63 AddDs  [actionD];
    64 
    65 (* =========================== square / angle brackets =========================== *)
    66 
    67 Goalw [square_def] "(s,t) |= unchanged v ==> (s,t) |= [A]_v";
    68 by (Asm_full_simp_tac 1);
    69 qed "idle_squareI";
    70 
    71 Goalw [square_def] "(s,t) |= A ==> (s,t) |= [A]_v";
    72 by (Asm_simp_tac 1);
    73 qed "busy_squareI";
    74 
    75 val prems = goal thy
    76   "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)";
    77 by (cut_facts_tac prems 1);
    78 by (rewrite_goals_tac (square_def::action_rews));
    79 by (etac disjE 1);
    80 by (REPEAT (eresolve_tac prems 1));
    81 qed "squareE";
    82 
    83 val prems = goalw thy (square_def::action_rews)
    84   "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v";
    85 by (rtac disjCI 1);
    86 by (eresolve_tac prems 1);
    87 qed "squareCI";
    88 
    89 goalw thy [angle_def]
    90   "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v";
    91 by (Asm_simp_tac 1);
    92 qed "angleI";
    93 
    94 val prems = goalw thy (angle_def::action_rews)
    95   "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R";
    96 by (cut_facts_tac prems 1);
    97 by (etac conjE 1);
    98 by (REPEAT (ares_tac prems 1));
    99 qed "angleE";
   100 
   101 AddIs [angleI, squareCI];
   102 AddEs [angleE, squareE];
   103 
   104 goal thy
   105    "!!f. [| |- unchanged f & ~B --> unchanged g;   \
   106 \           |- A & ~unchanged g --> B              \
   107 \        |] ==> |- [A]_f --> [B]_g";
   108 by (Clarsimp_tac 1);
   109 by (etac squareE 1);
   110 by (auto_tac (claset(), simpset() addsimps [square_def]));
   111 qed "square_simulation";
   112 
   113 goalw thy [square_def,angle_def]
   114    "|- (~ [A]_v) = <~A>_v";
   115 by Auto_tac;
   116 qed "not_square";
   117 
   118 goalw thy [square_def,angle_def]
   119    "|- (~ <A>_v) = [~A]_v";
   120 by Auto_tac;
   121 qed "not_angle";
   122 
   123 (* ============================== Facts about ENABLED ============================== *)
   124 
   125 goal thy "|- A --> $Enabled A";
   126 by (auto_tac (claset(), simpset() addsimps [enabled_def]));
   127 qed "enabledI";
   128 
   129 val prems = goalw thy [enabled_def]
   130   "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q";
   131 by (cut_facts_tac prems 1);
   132 by (etac exE 1);
   133 by (resolve_tac prems 1);
   134 by (atac 1);
   135 qed "enabledE";
   136 
   137 goal thy "|- ~$Enabled G --> ~ G";
   138 by (auto_tac (claset(), simpset() addsimps [enabled_def]));
   139 qed "notEnabledD";
   140 
   141 (* Monotonicity *)
   142 val [min,maj] = goal thy
   143   "[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G";
   144 by (rtac (min RS enabledE) 1);
   145 by (rtac (action_use enabledI) 1);
   146 by (etac (action_use maj) 1);
   147 qed "enabled_mono";
   148 
   149 (* stronger variant *)
   150 val [min,maj] = goal thy
   151   "[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G";
   152 by (rtac (min RS enabledE) 1);
   153 by (rtac (action_use enabledI) 1);
   154 by (etac maj 1);
   155 qed "enabled_mono2";
   156 
   157 goal thy "|- Enabled F --> Enabled (F | G)";
   158 by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   159 qed "enabled_disj1";
   160 
   161 goal thy "|- Enabled G --> Enabled (F | G)";
   162 by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   163 qed "enabled_disj2";
   164 
   165 goal thy "|- Enabled (F & G) --> Enabled F";
   166 by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   167 qed "enabled_conj1";
   168 
   169 goal thy "|- Enabled (F & G) --> Enabled G";
   170 by (auto_tac (claset() addSEs [enabled_mono], simpset()));
   171 qed "enabled_conj2";
   172 
   173 val prems = goal thy
   174   "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q";
   175 by (cut_facts_tac prems 1);
   176 by (resolve_tac prems 1);
   177 by (etac (action_use enabled_conj1) 1);
   178 by (etac (action_use enabled_conj2) 1);
   179 qed "enabled_conjE";
   180 
   181 goal thy "|- Enabled (F | G) --> Enabled F | Enabled G";
   182 by (auto_tac (claset(), simpset() addsimps [enabled_def]));
   183 qed "enabled_disjD";
   184 
   185 goal thy "|- Enabled (F | G) = (Enabled F | Enabled G)";
   186 by (Clarsimp_tac 1);
   187 by (rtac iffI 1);
   188 by (etac (action_use enabled_disjD) 1);
   189 by (REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1));
   190 qed "enabled_disj";
   191 
   192 goal thy "|- Enabled (EX x. F x) = (EX x. Enabled (F x))";
   193 by (force_tac (claset(), simpset() addsimps [enabled_def]) 1);
   194 qed "enabled_ex";
   195 
   196 
   197 (* A rule that combines enabledI and baseE, but generates fewer instantiations *)
   198 val prems = goal thy
   199   "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A";
   200 by (cut_facts_tac prems 1);
   201 by (etac exE 1);
   202 by (etac baseE 1);
   203 by (rtac (action_use enabledI) 1);
   204 by (etac allE 1);
   205 by (etac mp 1);
   206 by (atac 1);
   207 qed "base_enabled";
   208 
   209 (* ======================= action_simp_tac ============================== *)
   210 
   211 (* A dumb simplification-based tactic with just a little first-order logic:
   212    should plug in only "very safe" rules that can be applied blindly.
   213    Note that it applies whatever simplifications are currently active.
   214 *)
   215 fun action_simp_tac ss intros elims =
   216     asm_full_simp_tac 
   217          (ss setloop ((resolve_tac ((map action_use intros)
   218                                     @ [refl,impI,conjI,actionI,intI,allI]))
   219 		      ORELSE' (eresolve_tac ((map action_use elims) 
   220                                              @ [conjE,disjE,exE]))));
   221 
   222 (* default version without additional plug-in rules *)
   223 val Action_simp_tac = action_simp_tac (simpset()) [] [];
   224 
   225 
   226 
   227 (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
   228 (* "Enabled A" can be proven as follows:
   229    - Assume that we know which state variables are "base variables";
   230      this should be expressed by a theorem of the form "basevars (x,y,z,...)".
   231    - Resolve this theorem with baseE to introduce a constant for the value of the
   232      variables in the successor state, and resolve the goal with the result.
   233    - Resolve with enabledI and do some rewriting.
   234    - Solve for the unknowns using standard HOL reasoning.
   235    The following tactic combines these steps except the final one.
   236 *)
   237 
   238 fun enabled_tac base_vars =
   239     clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());
   240 
   241 (* Example:
   242 
   243 val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
   244 by (enabled_tac prem 1);
   245 by Auto_tac;
   246 
   247 *)