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