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