src/HOL/TLA/Action.ML
author wenzelm
Mon Feb 08 13:02:56 1999 +0100 (1999-02-08)
changeset 6255 db63752140c7
parent 4477 b3e5857d8d99
child 6301 08245f5a436d
permissions -rw-r--r--
updated (Stephan Merz);
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@6255
    12
qed_goal "actionI" Action.thy "(!!s t. (s,t) |= A) ==> |- A"
wenzelm@6255
    13
  (fn [prem] => [REPEAT (resolve_tac [prem,intI,prod_induct] 1)]);
wenzelm@6255
    14
wenzelm@6255
    15
qed_goal "actionD" Action.thy "|- A ==> (s,t) |= A"
wenzelm@6255
    16
  (fn [prem] => [rtac (prem RS intD) 1]);
wenzelm@6255
    17
wenzelm@6255
    18
local
wenzelm@6255
    19
  fun prover s = prove_goal Action.thy s 
wenzelm@6255
    20
                    (fn _ => [rtac actionI 1, 
wenzelm@6255
    21
                              rewrite_goals_tac (unl_after::intensional_rews),
wenzelm@6255
    22
                              rtac refl 1])
wenzelm@6255
    23
in
wenzelm@6255
    24
  val pr_rews = map (int_rewrite o prover)
wenzelm@6255
    25
    [ "|- (#c)` = #c",
wenzelm@6255
    26
      "|- f<x>` = f<x`>",
wenzelm@6255
    27
      "|- f<x,y>` = f<x`,y`>",
wenzelm@6255
    28
      "|- f<x,y,z>` = f<x`,y`,z`>",
wenzelm@6255
    29
      "|- (! x. P x)` = (! x. (P x)`)",
wenzelm@6255
    30
      "|- (? x. P x)` = (? x. (P x)`)"
wenzelm@6255
    31
    ]
wenzelm@6255
    32
end;
wenzelm@6255
    33
wenzelm@6255
    34
val act_rews = [unl_before,unl_after,unchanged_def] @ pr_rews;
wenzelm@6255
    35
Addsimps act_rews;
wenzelm@3807
    36
wenzelm@3807
    37
val action_rews = act_rews @ intensional_rews;
wenzelm@3807
    38
wenzelm@3807
    39
(* ================ Functions to "unlift" action theorems into HOL rules ================ *)
wenzelm@3807
    40
wenzelm@6255
    41
(* The following functions are specialized versions of the corresponding
wenzelm@6255
    42
   functions defined in Intensional.ML in that they introduce a
wenzelm@6255
    43
   "world" parameter of the form (s,t) and apply additional rewrites.
wenzelm@3807
    44
*)
wenzelm@6255
    45
fun action_unlift th = 
wenzelm@6255
    46
    (rewrite_rule action_rews (th RS actionD)) 
wenzelm@6255
    47
    handle _ => int_unlift th;
wenzelm@3807
    48
wenzelm@6255
    49
(* Turn  |- A = B  into meta-level rewrite rule  A == B *)
wenzelm@6255
    50
val action_rewrite = int_rewrite;
wenzelm@3807
    51
wenzelm@6255
    52
fun action_use th =
wenzelm@6255
    53
    case (concl_of th) of
wenzelm@6255
    54
      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
wenzelm@6255
    55
              ((flatten (action_unlift th)) handle _ => th)
wenzelm@6255
    56
    | _ => th;
wenzelm@3807
    57
wenzelm@3807
    58
(* ===================== Update simpset and classical prover ============================= *)
wenzelm@3807
    59
wenzelm@6255
    60
(***
wenzelm@6255
    61
(* Make the simplifier use action_use rather than int_use
wenzelm@3807
    62
   when action simplifications are added.
wenzelm@3807
    63
*)
wenzelm@3807
    64
wenzelm@6255
    65
let
wenzelm@6255
    66
  val ss = simpset_ref()
wenzelm@6255
    67
  fun try_rewrite th = 
wenzelm@6255
    68
      (action_rewrite th) handle _ => (action_use th) handle _ => th
wenzelm@6255
    69
in
wenzelm@6255
    70
  ss := !ss setmksimps ((mksimps mksimps_pairs) o try_rewrite)
wenzelm@6255
    71
end;
wenzelm@6255
    72
***)
wenzelm@3807
    73
wenzelm@6255
    74
AddSIs [actionI];
wenzelm@6255
    75
AddDs  [actionD];
wenzelm@3807
    76
wenzelm@3807
    77
(* =========================== square / angle brackets =========================== *)
wenzelm@3807
    78
wenzelm@3807
    79
qed_goalw "idle_squareI" Action.thy [square_def]
wenzelm@6255
    80
   "!!s t. (s,t) |= unchanged v ==> (s,t) |= [A]_v"
wenzelm@6255
    81
   (fn _ => [ Asm_full_simp_tac 1 ]);
wenzelm@3807
    82
wenzelm@3807
    83
qed_goalw "busy_squareI" Action.thy [square_def]
wenzelm@6255
    84
   "!!s t. (s,t) |= A ==> (s,t) |= [A]_v"
wenzelm@6255
    85
   (fn _ => [ Asm_simp_tac 1 ]);
wenzelm@6255
    86
wenzelm@6255
    87
qed_goal "squareE" Action.thy
wenzelm@6255
    88
  "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
wenzelm@6255
    89
  (fn prems => [cut_facts_tac prems 1,
wenzelm@6255
    90
                rewrite_goals_tac (square_def::action_rews),
wenzelm@6255
    91
                etac disjE 1,
wenzelm@6255
    92
                REPEAT (eresolve_tac prems 1)]);
wenzelm@6255
    93
wenzelm@6255
    94
qed_goalw "squareCI" Action.thy (square_def::action_rews)
wenzelm@6255
    95
  "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
wenzelm@6255
    96
  (fn prems => [rtac disjCI 1,
wenzelm@6255
    97
                eresolve_tac prems 1]);
wenzelm@6255
    98
wenzelm@6255
    99
qed_goalw "angleI" Action.thy [angle_def]
wenzelm@6255
   100
  "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
wenzelm@6255
   101
  (fn _ => [ Asm_simp_tac 1 ]);
wenzelm@3807
   102
wenzelm@6255
   103
qed_goalw "angleE" Action.thy (angle_def::action_rews)
wenzelm@6255
   104
  "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
wenzelm@6255
   105
  (fn prems => [cut_facts_tac prems 1,
wenzelm@6255
   106
                etac conjE 1,
wenzelm@6255
   107
                REPEAT (ares_tac prems 1)]);
wenzelm@6255
   108
wenzelm@6255
   109
AddIs [angleI, squareCI];
wenzelm@6255
   110
AddEs [angleE, squareE];
wenzelm@6255
   111
wenzelm@6255
   112
qed_goal "square_simulation" Action.thy
wenzelm@6255
   113
   "!!f. [| |- unchanged f & ~B --> unchanged g;   \
wenzelm@6255
   114
\           |- A & ~unchanged g --> B              \
wenzelm@6255
   115
\        |] ==> |- [A]_f --> [B]_g"
wenzelm@6255
   116
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   117
             etac squareE 1,
wenzelm@6255
   118
             auto_tac (claset(), simpset() addsimps [square_def])
wenzelm@6255
   119
            ]);
wenzelm@6255
   120
wenzelm@3807
   121
qed_goalw "not_square" Action.thy [square_def,angle_def]
wenzelm@6255
   122
   "|- (~ [A]_v) = <~A>_v"
paulson@4477
   123
   (fn _ => [ Auto_tac ]);
wenzelm@3807
   124
wenzelm@3807
   125
qed_goalw "not_angle" Action.thy [square_def,angle_def]
wenzelm@6255
   126
   "|- (~ <A>_v) = [~A]_v"
paulson@4477
   127
   (fn _ => [ Auto_tac ]);
wenzelm@3807
   128
wenzelm@3807
   129
(* ============================== Facts about ENABLED ============================== *)
wenzelm@3807
   130
wenzelm@6255
   131
qed_goal "enabledI" Action.thy
wenzelm@6255
   132
  "|- A --> $Enabled A"
wenzelm@6255
   133
  (fn _ => [ auto_tac (claset(), simpset() addsimps [enabled_def]) ]);
wenzelm@3807
   134
wenzelm@3807
   135
qed_goalw "enabledE" Action.thy [enabled_def]
wenzelm@6255
   136
  "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
wenzelm@3807
   137
  (fn prems => [cut_facts_tac prems 1,
wenzelm@6255
   138
                etac exE 1,
wenzelm@3807
   139
                resolve_tac prems 1, atac 1
wenzelm@3807
   140
               ]);
wenzelm@3807
   141
wenzelm@3807
   142
qed_goal "notEnabledD" Action.thy
wenzelm@6255
   143
  "|- ~$Enabled G --> ~ G"
wenzelm@6255
   144
  (fn _ => [ auto_tac (claset(), simpset() addsimps [enabled_def]) ]);
wenzelm@3807
   145
wenzelm@3807
   146
(* Monotonicity *)
wenzelm@3807
   147
qed_goal "enabled_mono" Action.thy
wenzelm@6255
   148
  "[| s |= Enabled F; |- F --> G |] ==> s |= Enabled G"
wenzelm@3807
   149
  (fn [min,maj] => [rtac (min RS enabledE) 1,
wenzelm@6255
   150
                    rtac (action_use enabledI) 1,
wenzelm@6255
   151
                    etac (action_use maj) 1
wenzelm@3807
   152
                   ]);
wenzelm@3807
   153
wenzelm@3807
   154
(* stronger variant *)
wenzelm@3807
   155
qed_goal "enabled_mono2" Action.thy
wenzelm@6255
   156
   "[| s |= Enabled F; !!t. F (s,t) ==> G (s,t) |] ==> s |= Enabled G"
wenzelm@3807
   157
   (fn [min,maj] => [rtac (min RS enabledE) 1,
wenzelm@6255
   158
		     rtac (action_use enabledI) 1,
wenzelm@3807
   159
		     etac maj 1
wenzelm@3807
   160
		    ]);
wenzelm@3807
   161
wenzelm@3807
   162
qed_goal "enabled_disj1" Action.thy
wenzelm@6255
   163
  "|- Enabled F --> Enabled (F | G)"
wenzelm@6255
   164
  (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
wenzelm@3807
   165
wenzelm@3807
   166
qed_goal "enabled_disj2" Action.thy
wenzelm@6255
   167
  "|- Enabled G --> Enabled (F | G)"
wenzelm@6255
   168
  (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
wenzelm@3807
   169
wenzelm@3807
   170
qed_goal "enabled_conj1" Action.thy
wenzelm@6255
   171
  "|- Enabled (F & G) --> Enabled F"
wenzelm@6255
   172
  (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
wenzelm@3807
   173
wenzelm@3807
   174
qed_goal "enabled_conj2" Action.thy
wenzelm@6255
   175
  "|- Enabled (F & G) --> Enabled G"
wenzelm@6255
   176
  (fn _ => [ auto_tac (claset() addSEs [enabled_mono], simpset()) ]);
wenzelm@3807
   177
wenzelm@3807
   178
qed_goal "enabled_conjE" Action.thy
wenzelm@6255
   179
  "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"
wenzelm@3807
   180
  (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
wenzelm@6255
   181
                etac (action_use enabled_conj1) 1, 
wenzelm@6255
   182
		etac (action_use enabled_conj2) 1
wenzelm@6255
   183
	       ]);
wenzelm@3807
   184
wenzelm@3807
   185
qed_goal "enabled_disjD" Action.thy
wenzelm@6255
   186
  "|- Enabled (F | G) --> Enabled F | Enabled G"
wenzelm@6255
   187
  (fn _ => [ auto_tac (claset(), simpset() addsimps [enabled_def]) ]);
wenzelm@3807
   188
wenzelm@3807
   189
qed_goal "enabled_disj" Action.thy
wenzelm@6255
   190
  "|- Enabled (F | G) = (Enabled F | Enabled G)"
wenzelm@6255
   191
  (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   192
	    rtac iffI 1,
wenzelm@6255
   193
            etac (action_use enabled_disjD) 1,
wenzelm@6255
   194
            REPEAT (eresolve_tac (disjE::map action_use [enabled_disj1,enabled_disj2]) 1)
wenzelm@3807
   195
           ]);
wenzelm@3807
   196
wenzelm@3807
   197
qed_goal "enabled_ex" Action.thy
wenzelm@6255
   198
  "|- Enabled (? x. F x) = (? x. Enabled (F x))"
wenzelm@6255
   199
  (fn _ => [ force_tac (claset(), simpset() addsimps [enabled_def]) 1 ]);
wenzelm@6255
   200
wenzelm@3807
   201
wenzelm@3807
   202
(* A rule that combines enabledI and baseE, but generates fewer possible instantiations *)
wenzelm@3807
   203
qed_goal "base_enabled" Action.thy
wenzelm@6255
   204
  "[| basevars vs; !!u. vs u = c s ==> A (s,u) |] ==> s |= Enabled A"
wenzelm@3807
   205
  (fn prems => [cut_facts_tac prems 1,
wenzelm@6255
   206
		etac baseE 1, rtac (action_use enabledI) 1,
wenzelm@3807
   207
		REPEAT (ares_tac prems 1)]);
wenzelm@3807
   208
wenzelm@3807
   209
wenzelm@6255
   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@6255
   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@6255
   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@6255
   238
(*** old version
wenzelm@3807
   239
fun enabled_tac base_vars i =
wenzelm@3807
   240
    EVERY [(* apply actionI (plus rewriting) if the goal is of the form $(Enabled A),
wenzelm@6255
   241
	      do nothing if it is of the form s |= Enabled A *)
wenzelm@6255
   242
	   TRY ((resolve_tac [actionI,intI] i) 
wenzelm@6255
   243
                THEN (SELECT_GOAL (rewrite_goals_tac action_rews) i)),
wenzelm@6255
   244
	   clarify_tac (claset() addSIs [base_vars RS base_enabled]) i,
wenzelm@3807
   245
	   (SELECT_GOAL (rewrite_goals_tac action_rews) i)
wenzelm@3807
   246
	  ];
wenzelm@6255
   247
***)
wenzelm@3807
   248
wenzelm@6255
   249
fun enabled_tac base_vars =
wenzelm@6255
   250
    clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());
wenzelm@3807
   251
wenzelm@6255
   252
(* Example:
wenzelm@6255
   253
wenzelm@6255
   254
val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
wenzelm@6255
   255
by (enabled_tac prem 1);
wenzelm@6255
   256
auto();
wenzelm@3807
   257
wenzelm@3807
   258
*)