src/HOL/TLA/TLA.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9168 77658111e122
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 TLA/TLA.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@6255
     4
    Copyright:   1998 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
Lemmas and tactics for temporal reasoning.
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@6255
     9
(* Specialize intensional introduction/elimination rules for temporal formulas *)
wenzelm@3807
    10
wenzelm@6255
    11
qed_goal "tempI" TLA.thy "(!!sigma. sigma |= (F::temporal)) ==> |- F"
wenzelm@3807
    12
  (fn [prem] => [ REPEAT (resolve_tac [prem,intI] 1) ]);
wenzelm@3807
    13
wenzelm@6255
    14
qed_goal "tempD" TLA.thy "|- (F::temporal) ==> sigma |= F"
wenzelm@6255
    15
  (fn [prem] => [ rtac (prem RS intD) 1 ]);
wenzelm@3807
    16
wenzelm@3807
    17
wenzelm@6255
    18
(* ======== Functions to "unlift" temporal theorems ====== *)
wenzelm@3807
    19
wenzelm@6255
    20
(* The following functions are specialized versions of the corresponding
wenzelm@6255
    21
   functions defined in Intensional.ML in that they introduce a
wenzelm@6255
    22
   "world" parameter of type "behavior".
wenzelm@3807
    23
*)
wenzelm@6255
    24
fun temp_unlift th = 
wenzelm@6255
    25
    (rewrite_rule action_rews (th RS tempD))
wenzelm@6255
    26
    handle _ => action_unlift th;
wenzelm@3807
    27
wenzelm@6255
    28
(* Turn  |- F = G  into meta-level rewrite rule  F == G *)
wenzelm@6255
    29
val temp_rewrite = int_rewrite;
wenzelm@3807
    30
wenzelm@6255
    31
fun temp_use th = 
wenzelm@6255
    32
    case (concl_of th) of
wenzelm@6255
    33
      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
wenzelm@6255
    34
              ((flatten (temp_unlift th)) handle _ => th)
wenzelm@6255
    35
    | _ => th;
wenzelm@3807
    36
wenzelm@3807
    37
(* Update classical reasoner---will be updated once more below! *)
wenzelm@3807
    38
wenzelm@3807
    39
AddSIs [tempI];
wenzelm@3807
    40
AddDs [tempD];
wenzelm@3807
    41
wenzelm@6255
    42
val temp_css = (claset(), simpset());
oheimb@4651
    43
val temp_cs = op addss temp_css;
wenzelm@3807
    44
wenzelm@6255
    45
(* Modify the functions that add rules to simpsets, classical sets,
wenzelm@6255
    46
   and clasimpsets in order to accept "lifted" theorems
wenzelm@6255
    47
*)
wenzelm@3807
    48
wenzelm@6255
    49
local
wenzelm@6255
    50
  fun try_rewrite th =
wenzelm@6255
    51
      (temp_rewrite th) handle _ => temp_use th
wenzelm@6255
    52
in
wenzelm@6255
    53
  val op addsimps = fn (ss, ts) => ss addsimps (map try_rewrite ts)
wenzelm@6255
    54
  val op addsimps2 = fn (css, ts) => css addsimps2 (map try_rewrite ts)
wenzelm@6255
    55
end;
wenzelm@3807
    56
wenzelm@6255
    57
val op addSIs = fn (cs, ts) => cs addSIs (map temp_use ts);
wenzelm@6255
    58
val op addSEs = fn (cs, ts) => cs addSEs (map temp_use ts);
wenzelm@6255
    59
val op addSDs = fn (cs, ts) => cs addSDs (map temp_use ts);
wenzelm@6255
    60
val op addIs = fn (cs, ts) => cs addIs (map temp_use ts);
wenzelm@6255
    61
val op addEs = fn (cs, ts) => cs addEs (map temp_use ts);
wenzelm@6255
    62
val op addDs = fn (cs, ts) => cs addDs (map temp_use ts);
wenzelm@3807
    63
wenzelm@6255
    64
val op addSIs2 = fn (css, ts) => css addSIs2 (map temp_use ts);
wenzelm@6255
    65
val op addSEs2 = fn (css, ts) => css addSEs2 (map temp_use ts);
wenzelm@6255
    66
val op addSDs2 = fn (css, ts) => css addSDs2 (map temp_use ts);
wenzelm@6255
    67
val op addIs2 = fn (css, ts) => css addIs2 (map temp_use ts);
wenzelm@6255
    68
val op addEs2 = fn (css, ts) => css addEs2 (map temp_use ts);
wenzelm@6255
    69
val op addDs2 = fn (css, ts) => css addDs2 (map temp_use ts);
wenzelm@3807
    70
wenzelm@3807
    71
wenzelm@3807
    72
(* ------------------------------------------------------------------------- *)
wenzelm@3807
    73
(***           "Simple temporal logic": only [] and <>                     ***)
wenzelm@3807
    74
(* ------------------------------------------------------------------------- *)
wenzelm@3807
    75
section "Simple temporal logic";
wenzelm@3807
    76
wenzelm@6255
    77
(* []~F == []~Init F *)
wenzelm@6255
    78
bind_thm("boxNotInit", rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] boxInit));
wenzelm@6255
    79
wenzelm@6255
    80
qed_goalw "dmdInit" TLA.thy [dmd_def] "TEMP <>F == TEMP <> Init F"
wenzelm@6255
    81
  (fn _ => [rewtac (read_instantiate [("F", "LIFT ~F")] boxInit),
wenzelm@6255
    82
            simp_tac (simpset() addsimps Init_simps) 1]);
wenzelm@6255
    83
wenzelm@6255
    84
bind_thm("dmdNotInit", rewrite_rule Init_simps (read_instantiate [("F", "LIFT ~F")] dmdInit));
wenzelm@6255
    85
wenzelm@6255
    86
(* boxInit and dmdInit cannot be used as rewrites, because they loop.
wenzelm@6255
    87
   Non-looping instances for state predicates and actions are occasionally useful.
wenzelm@6255
    88
*)
wenzelm@6255
    89
bind_thm("boxInit_stp", read_instantiate [("'a","state")] boxInit);
wenzelm@6255
    90
bind_thm("boxInit_act", read_instantiate [("'a","state * state")] boxInit);
wenzelm@6255
    91
bind_thm("dmdInit_stp", read_instantiate [("'a","state")] dmdInit);
wenzelm@6255
    92
bind_thm("dmdInit_act", read_instantiate [("'a","state * state")] dmdInit);
wenzelm@6255
    93
wenzelm@6255
    94
(* The symmetric equations can be used to get rid of Init *)
wenzelm@6255
    95
bind_thm("boxInitD", symmetric boxInit);
wenzelm@6255
    96
bind_thm("dmdInitD", symmetric dmdInit);
wenzelm@6255
    97
bind_thm("boxNotInitD", symmetric boxNotInit);
wenzelm@6255
    98
bind_thm("dmdNotInitD", symmetric dmdNotInit);
wenzelm@6255
    99
wenzelm@6255
   100
val Init_simps = Init_simps @ [boxInitD, dmdInitD, boxNotInitD, dmdNotInitD];
wenzelm@6255
   101
wenzelm@3807
   102
(* ------------------------ STL2 ------------------------------------------- *)
wenzelm@3807
   103
bind_thm("STL2", reflT);
wenzelm@3807
   104
wenzelm@6255
   105
(* The "polymorphic" (generic) variant *)
wenzelm@6255
   106
qed_goal "STL2_gen" TLA.thy "|- []F --> Init F"
wenzelm@6255
   107
  (fn _ => [rewtac (read_instantiate [("F", "F")] boxInit),
wenzelm@6255
   108
            rtac STL2 1]);
wenzelm@6255
   109
wenzelm@6255
   110
(* see also STL2_pr below: "|- []P --> Init P & Init (P`)" *)
wenzelm@6255
   111
wenzelm@3807
   112
wenzelm@3807
   113
(* Dual versions for <> *)
wenzelm@6255
   114
qed_goalw "InitDmd" TLA.thy [dmd_def] "|- F --> <> F"
wenzelm@6255
   115
   (fn _ => [ auto_tac (temp_css addSDs2 [STL2]) ]);
wenzelm@3807
   116
wenzelm@6255
   117
qed_goal "InitDmd_gen" TLA.thy "|- Init F --> <>F"
wenzelm@6255
   118
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   119
             dtac (temp_use InitDmd) 1,
wenzelm@6255
   120
             asm_full_simp_tac (simpset() addsimps [dmdInitD]) 1]);
wenzelm@3807
   121
wenzelm@3807
   122
wenzelm@3807
   123
(* ------------------------ STL3 ------------------------------------------- *)
wenzelm@6255
   124
qed_goal "STL3" TLA.thy "|- ([][]F) = ([]F)"
wenzelm@6255
   125
   (K [force_tac (temp_css addEs2 [transT,STL2]) 1]);
wenzelm@3807
   126
wenzelm@3807
   127
(* corresponding elimination rule introduces double boxes: 
wenzelm@3807
   128
   [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
wenzelm@3807
   129
*)
wenzelm@3807
   130
bind_thm("dup_boxE", make_elim((temp_unlift STL3) RS iffD2));
wenzelm@3807
   131
bind_thm("dup_boxD", (temp_unlift STL3) RS iffD1);
wenzelm@3807
   132
wenzelm@3807
   133
(* dual versions for <> *)
wenzelm@6255
   134
qed_goalw "DmdDmd" TLA.thy [dmd_def] "|- (<><>F) = (<>F)"
wenzelm@3807
   135
   (fn _ => [ auto_tac (temp_css addsimps2 [STL3]) ]);
wenzelm@3807
   136
bind_thm("dup_dmdE", make_elim((temp_unlift DmdDmd) RS iffD2));
wenzelm@3807
   137
bind_thm("dup_dmdD", (temp_unlift DmdDmd) RS iffD1);
wenzelm@3807
   138
wenzelm@3807
   139
wenzelm@3807
   140
(* ------------------------ STL4 ------------------------------------------- *)
wenzelm@6255
   141
qed_goal "STL4" TLA.thy "|- F --> G  ==> |- []F --> []G"
wenzelm@6255
   142
   (fn [prem] => [Clarsimp_tac 1,
wenzelm@6255
   143
		  rtac (temp_use normalT) 1,
wenzelm@6255
   144
                  rtac (temp_use (prem RS necT)) 1,
wenzelm@6255
   145
		  atac 1
wenzelm@3807
   146
		 ]);
wenzelm@3807
   147
wenzelm@6255
   148
(* Unlifted version as an elimination rule *)
wenzelm@3807
   149
qed_goal "STL4E" TLA.thy 
wenzelm@6255
   150
         "[| sigma |= []F; |- F --> G |] ==> sigma |= []G"
wenzelm@6255
   151
   (fn prems => [ REPEAT (resolve_tac (prems @ [temp_use STL4]) 1) ]);
wenzelm@6255
   152
wenzelm@6255
   153
qed_goal "STL4_gen" TLA.thy "|- Init F --> Init G ==> |- []F --> []G"
wenzelm@6255
   154
   (fn [prem] => [rtac (rewrite_rule [boxInitD] (prem RS STL4)) 1]);
wenzelm@6255
   155
wenzelm@6255
   156
qed_goal "STL4E_gen" TLA.thy
wenzelm@6255
   157
         "[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G"
wenzelm@6255
   158
   (fn prems => [ REPEAT (resolve_tac (prems @ [temp_use STL4_gen]) 1) ]);
wenzelm@3807
   159
wenzelm@3807
   160
(* see also STL4Edup below, which allows an auxiliary boxed formula:
wenzelm@3807
   161
       []A /\ F => G
wenzelm@3807
   162
     -----------------
wenzelm@3807
   163
     []A /\ []F => []G
wenzelm@3807
   164
*)
wenzelm@3807
   165
wenzelm@3807
   166
(* The dual versions for <> *)
wenzelm@3807
   167
qed_goalw "DmdImpl" TLA.thy [dmd_def]
wenzelm@6255
   168
   "|- F --> G ==> |- <>F --> <>G"
wenzelm@6255
   169
   (fn [prem] => [fast_tac (temp_cs addSIs [prem] addSEs [STL4E]) 1]);
wenzelm@3807
   170
wenzelm@3807
   171
qed_goal "DmdImplE" TLA.thy
wenzelm@6255
   172
   "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G"
wenzelm@6255
   173
   (fn prems => [ REPEAT (resolve_tac (prems @ [temp_use DmdImpl]) 1) ]);
wenzelm@3807
   174
wenzelm@3807
   175
wenzelm@3807
   176
(* ------------------------ STL5 ------------------------------------------- *)
wenzelm@6255
   177
qed_goal "STL5" TLA.thy "|- ([]F & []G) = ([](F & G))"
paulson@4477
   178
   (fn _ => [Auto_tac,
wenzelm@6255
   179
	     subgoal_tac "sigma |= [](G --> (F & G))" 1,
wenzelm@6255
   180
	     etac (temp_use normalT) 1, atac 1,
wenzelm@3807
   181
	     ALLGOALS (fast_tac (temp_cs addSEs [STL4E]))
wenzelm@3807
   182
	    ]);
wenzelm@3807
   183
(* rewrite rule to split conjunctions under boxes *)
wenzelm@3807
   184
bind_thm("split_box_conj", (temp_unlift STL5) RS sym);
wenzelm@3807
   185
wenzelm@3807
   186
(* the corresponding elimination rule allows to combine boxes in the hypotheses
wenzelm@3807
   187
   (NB: F and G must have the same type, i.e., both actions or temporals.)
wenzelm@6255
   188
   Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
wenzelm@3807
   189
*)
wenzelm@3807
   190
qed_goal "box_conjE" TLA.thy
wenzelm@6255
   191
   "[| sigma |= []F; sigma |= []G; sigma |= [](F&G) ==> PROP R |] ==> PROP R"
wenzelm@3807
   192
   (fn prems => [ REPEAT (resolve_tac
wenzelm@3807
   193
			   (prems @ [(temp_unlift STL5) RS iffD1, conjI]) 1) ]);
wenzelm@3807
   194
wenzelm@6255
   195
(* Instances of box_conjE for state predicates, actions, and temporals
wenzelm@6255
   196
   in case the general rule is "too polymorphic".
wenzelm@6255
   197
*)
wenzelm@6255
   198
bind_thm("box_conjE_temp", read_instantiate [("'a","behavior")] box_conjE);
wenzelm@6255
   199
bind_thm("box_conjE_stp", read_instantiate [("'a","state")] box_conjE);
wenzelm@6255
   200
bind_thm("box_conjE_act", read_instantiate [("'a","state * state")] box_conjE);
wenzelm@6255
   201
wenzelm@3807
   202
(* Define a tactic that tries to merge all boxes in an antecedent. The definition is
wenzelm@6255
   203
   a bit kludgy in order to simulate "double elim-resolution".
wenzelm@3807
   204
*)
wenzelm@6255
   205
wenzelm@6255
   206
Goal "[| sigma |= []F; PROP W |] ==> PROP W";
wenzelm@6255
   207
by (atac 1);
wenzelm@6255
   208
val box_thin = result();
wenzelm@3807
   209
wenzelm@3807
   210
fun merge_box_tac i =
wenzelm@3807
   211
   REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i]);
wenzelm@3807
   212
wenzelm@3807
   213
fun merge_temp_box_tac i =
wenzelm@6255
   214
   REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i, 
wenzelm@6255
   215
                         eres_inst_tac [("'a","behavior")] box_thin i]);
wenzelm@3807
   216
wenzelm@6255
   217
fun merge_stp_box_tac i =
wenzelm@6255
   218
   REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i, 
wenzelm@6255
   219
                         eres_inst_tac [("'a","state")] box_thin i]);
wenzelm@6255
   220
wenzelm@3807
   221
fun merge_act_box_tac i =
wenzelm@6255
   222
   REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i, 
wenzelm@6255
   223
                         eres_inst_tac [("'a","state * state")] box_thin i]);
wenzelm@6255
   224
wenzelm@3807
   225
wenzelm@3807
   226
(* rewrite rule to push universal quantification through box:
wenzelm@6255
   227
      (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
wenzelm@3807
   228
*)
wenzelm@3807
   229
bind_thm("all_box", standard((temp_unlift allT) RS sym));
wenzelm@3807
   230
wenzelm@3807
   231
wenzelm@6255
   232
qed_goal "DmdOr" TLA.thy "|- (<>(F | G)) = (<>F | <>G)"
wenzelm@3807
   233
   (fn _ => [auto_tac (temp_css addsimps2 [dmd_def,split_box_conj]),
wenzelm@3807
   234
             TRYALL (EVERY' [etac swap, 
wenzelm@3807
   235
                             merge_box_tac, 
wenzelm@3807
   236
                             fast_tac (temp_cs addSEs [STL4E])])
wenzelm@3807
   237
            ]);
wenzelm@3807
   238
wenzelm@6255
   239
qed_goal "exT" TLA.thy "|- (? x. <>(F x)) = (<>(? x. F x))"
wenzelm@6255
   240
   (fn _ => [ auto_tac (temp_css addsimps2 [dmd_def,Not_Rex,all_box]) ]);
wenzelm@3807
   241
wenzelm@3807
   242
bind_thm("ex_dmd", standard((temp_unlift exT) RS sym));
wenzelm@3807
   243
	     
wenzelm@3807
   244
wenzelm@3807
   245
qed_goal "STL4Edup" TLA.thy
wenzelm@6255
   246
   "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
wenzelm@3807
   247
   (fn _ => [etac dup_boxE 1,
wenzelm@3807
   248
	     merge_box_tac 1,
wenzelm@3807
   249
	     etac STL4E 1,
wenzelm@3807
   250
	     atac 1
wenzelm@3807
   251
	    ]);
wenzelm@3807
   252
wenzelm@3807
   253
qed_goalw "DmdImpl2" TLA.thy [dmd_def]
wenzelm@6255
   254
   "!!sigma. [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G"
paulson@4477
   255
   (fn _ => [Auto_tac,
wenzelm@3807
   256
	     etac notE 1,
wenzelm@3807
   257
	     merge_box_tac 1,
wenzelm@3807
   258
	     fast_tac (temp_cs addSEs [STL4E]) 1
wenzelm@3807
   259
	    ]);
wenzelm@3807
   260
wenzelm@3807
   261
qed_goal "InfImpl" TLA.thy
wenzelm@6255
   262
   "[| sigma |= []<>F; sigma |= []G; |- F & G --> H |] ==> sigma |= []<>H"
wenzelm@3807
   263
   (fn [prem1,prem2,prem3] 
wenzelm@3807
   264
       => [cut_facts_tac [prem1,prem2] 1,
wenzelm@3807
   265
	   eres_inst_tac [("F","G")] dup_boxE 1,
wenzelm@3807
   266
	   merge_box_tac 1,
wenzelm@6255
   267
	   fast_tac (temp_cs addSEs [STL4E,DmdImpl2] addSIs [prem3]) 1
wenzelm@3807
   268
	  ]);
wenzelm@3807
   269
wenzelm@3807
   270
(* ------------------------ STL6 ------------------------------------------- *)
wenzelm@3807
   271
(* Used in the proof of STL6, but useful in itself. *)
wenzelm@6255
   272
qed_goalw "BoxDmd" TLA.thy [dmd_def] "|- []F & <>G --> <>([]F & G)"
wenzelm@6255
   273
  (fn _ => [ Clarsimp_tac 1,
wenzelm@3807
   274
             etac dup_boxE 1,
wenzelm@3807
   275
	     merge_box_tac 1,
wenzelm@3807
   276
             etac swap 1,
wenzelm@3807
   277
             fast_tac (temp_cs addSEs [STL4E]) 1 ]);
wenzelm@3807
   278
wenzelm@3807
   279
(* weaker than BoxDmd, but more polymorphic (and often just right) *)
wenzelm@6255
   280
qed_goalw "BoxDmd_simple" TLA.thy [dmd_def] "|- []F & <>G --> <>(F & G)"
wenzelm@6255
   281
  (fn _ => [ Clarsimp_tac 1,
wenzelm@6255
   282
	     merge_box_tac 1,
wenzelm@6255
   283
             fast_tac (temp_cs addSEs [notE,STL4E]) 1
wenzelm@6255
   284
	   ]);
wenzelm@6255
   285
wenzelm@6255
   286
qed_goalw "BoxDmd2_simple" TLA.thy [dmd_def] "|- []F & <>G --> <>(G & F)"
wenzelm@6255
   287
  (fn _ => [ Clarsimp_tac 1,
wenzelm@3807
   288
	     merge_box_tac 1,
wenzelm@3807
   289
             fast_tac (temp_cs addSEs [notE,STL4E]) 1
wenzelm@3807
   290
	   ]);
wenzelm@3807
   291
wenzelm@6255
   292
qed_goal "DmdImpldup" TLA.thy 
wenzelm@6255
   293
   "[| sigma |= []A; sigma |= <>F; |- []A & F --> G |] ==> sigma |= <>G"
wenzelm@6255
   294
   (fn [p1,p2,p3] => [rtac ((p2 RS (p1 RS (temp_use BoxDmd))) RS DmdImplE) 1,
wenzelm@6255
   295
                      rtac p3 1]);
wenzelm@6255
   296
wenzelm@6255
   297
qed_goal "STL6" TLA.thy "|- <>[]F & <>[]G --> <>[](F & G)"
wenzelm@3807
   298
  (fn _ => [auto_tac (temp_css addsimps2 [symmetric (temp_rewrite STL5)]),
wenzelm@6255
   299
	    dtac (temp_use linT) 1, atac 1, etac thin_rl 1,
wenzelm@3807
   300
	    rtac ((temp_unlift DmdDmd) RS iffD1) 1,
wenzelm@3807
   301
	    etac disjE 1,
wenzelm@6255
   302
	    etac DmdImplE 1, rtac BoxDmd 1,
wenzelm@6255
   303
	    (* the second subgoal needs commutativity of &, which complicates the proof *)
wenzelm@3807
   304
	    etac DmdImplE 1,
paulson@4477
   305
	    Auto_tac,
wenzelm@6255
   306
	    dtac (temp_use BoxDmd) 1, atac 1, etac thin_rl 1,
wenzelm@3807
   307
	    fast_tac (temp_cs addSEs [DmdImplE]) 1
wenzelm@3807
   308
	   ]);
wenzelm@3807
   309
wenzelm@3807
   310
wenzelm@3807
   311
(* ------------------------ True / False ----------------------------------------- *)
wenzelm@3807
   312
section "Simplification of constants";
wenzelm@3807
   313
wenzelm@6255
   314
qed_goal "BoxConst" TLA.thy "|- ([]#P) = #P"
wenzelm@6255
   315
  (fn _ => [rtac tempI 1,
wenzelm@6255
   316
            case_tac "P" 1,
wenzelm@6255
   317
            auto_tac (temp_css addSIs2 [necT] addDs2 [STL2_gen] 
wenzelm@6255
   318
                               addsimps2 Init_simps)
wenzelm@6255
   319
           ]);
wenzelm@3807
   320
wenzelm@6255
   321
qed_goalw "DmdConst" TLA.thy [dmd_def] "|- (<>#P) = #P"
wenzelm@6255
   322
  (fn _ => [case_tac "P" 1,
wenzelm@6255
   323
            ALLGOALS (asm_full_simp_tac (simpset() addsimps [BoxConst]))
wenzelm@6255
   324
           ]);
wenzelm@3807
   325
wenzelm@6255
   326
val temp_simps = map temp_rewrite [BoxConst, DmdConst];
wenzelm@3807
   327
wenzelm@3807
   328
(* Make these rewrites active by default *)
wenzelm@3807
   329
Addsimps temp_simps;
wenzelm@3807
   330
val temp_css = temp_css addsimps2 temp_simps;
oheimb@4651
   331
val temp_cs = op addss temp_css;
wenzelm@3807
   332
wenzelm@3807
   333
wenzelm@3807
   334
(* ------------------------ Further rewrites ----------------------------------------- *)
wenzelm@3807
   335
section "Further rewrites";
wenzelm@3807
   336
wenzelm@6255
   337
qed_goalw "NotBox" TLA.thy [dmd_def] "|- (~[]F) = (<>~F)"
wenzelm@6255
   338
   (fn _ => [ Simp_tac 1 ]);
wenzelm@3807
   339
wenzelm@6255
   340
qed_goalw "NotDmd" TLA.thy [dmd_def] "|- (~<>F) = ([]~F)"
wenzelm@6255
   341
   (fn _ => [ Simp_tac 1 ]);
wenzelm@3807
   342
wenzelm@3807
   343
(* These are not by default included in temp_css, because they could be harmful,
wenzelm@6255
   344
   e.g. []F & ~[]F becomes []F & <>~F !! *)
wenzelm@3807
   345
val more_temp_simps =  (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd])
wenzelm@3807
   346
                       @ (map (fn th => (temp_unlift th) RS eq_reflection)
wenzelm@3807
   347
		         [NotBox, NotDmd]);
wenzelm@3807
   348
wenzelm@6255
   349
qed_goal "BoxDmdBox" TLA.thy "|- ([]<>[]F) = (<>[]F)"
wenzelm@6255
   350
   (fn _ => [ auto_tac (temp_css addSDs2 [STL2]),
wenzelm@3807
   351
              rtac ccontr 1,
wenzelm@6255
   352
              subgoal_tac "sigma |= <>[][]F & <>[]~[]F" 1,
wenzelm@3807
   353
              etac thin_rl 1,
paulson@4477
   354
              Auto_tac,
wenzelm@6255
   355
	      dtac (temp_use STL6) 1, atac 1,
wenzelm@3807
   356
	      Asm_full_simp_tac 1,
wenzelm@4089
   357
	      ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps))
wenzelm@3807
   358
	    ]);
wenzelm@3807
   359
wenzelm@6255
   360
qed_goalw "DmdBoxDmd" TLA.thy [dmd_def] "|- (<>[]<>F) = ([]<>F)"
wenzelm@6255
   361
  (fn _ => [ auto_tac (temp_css addsimps2 [rewrite_rule [dmd_def] BoxDmdBox]) ]);
wenzelm@3807
   362
wenzelm@3807
   363
val more_temp_simps = more_temp_simps @ (map temp_rewrite [BoxDmdBox, DmdBoxDmd]);
wenzelm@3807
   364
wenzelm@3807
   365
wenzelm@3807
   366
(* ------------------------ Miscellaneous ----------------------------------- *)
wenzelm@3807
   367
wenzelm@3807
   368
qed_goal "BoxOr" TLA.thy 
wenzelm@6255
   369
   "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)"
wenzelm@3807
   370
   (fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]);
wenzelm@3807
   371
wenzelm@6255
   372
(* "persistently implies infinitely often" *)
wenzelm@6255
   373
qed_goal "DBImplBD" TLA.thy "|- <>[]F --> []<>F"
wenzelm@6255
   374
  (fn _ => [Clarsimp_tac 1,
wenzelm@3807
   375
	    rtac ccontr 1,
wenzelm@6255
   376
            asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
wenzelm@6255
   377
            dtac (temp_use STL6) 1, atac 1,
wenzelm@6255
   378
            Asm_full_simp_tac 1
wenzelm@3807
   379
	   ]);
wenzelm@3807
   380
wenzelm@3807
   381
qed_goal "BoxDmdDmdBox" TLA.thy
wenzelm@6255
   382
   "|- []<>F & <>[]G --> []<>(F & G)"
wenzelm@6255
   383
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   384
             rtac ccontr 1,
wenzelm@3807
   385
	     rewrite_goals_tac more_temp_simps,
wenzelm@6255
   386
	     dtac (temp_use STL6) 1, atac 1,
wenzelm@6255
   387
	     subgoal_tac "sigma |= <>[]~F" 1,
oheimb@5755
   388
	     force_tac (temp_css addsimps2 [dmd_def]) 1,
wenzelm@3807
   389
	     fast_tac (temp_cs addEs [DmdImplE,STL4E]) 1
wenzelm@3807
   390
	    ]);
wenzelm@3807
   391
wenzelm@3807
   392
wenzelm@3807
   393
(* ------------------------------------------------------------------------- *)
wenzelm@3807
   394
(***          TLA-specific theorems: primed formulas                       ***)
wenzelm@3807
   395
(* ------------------------------------------------------------------------- *)
wenzelm@3807
   396
section "priming";
wenzelm@3807
   397
wenzelm@3807
   398
(* ------------------------ TLA2 ------------------------------------------- *)
wenzelm@6255
   399
qed_goal "STL2_pr" TLA.thy
wenzelm@6255
   400
  "|- []P --> Init P & Init P`"
wenzelm@6255
   401
  (fn _ => [fast_tac (temp_cs addSIs [primeI, STL2_gen]) 1]);
wenzelm@3807
   402
wenzelm@3807
   403
(* Auxiliary lemma allows priming of boxed actions *)
wenzelm@6255
   404
qed_goal "BoxPrime" TLA.thy "|- []P --> []($P & P$)"
wenzelm@6255
   405
  (fn _ => [Clarsimp_tac 1,
wenzelm@3807
   406
	    etac dup_boxE 1,
wenzelm@6255
   407
            rewtac boxInit_act,
wenzelm@6255
   408
            etac STL4E 1,
wenzelm@6255
   409
	    auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_pr])
wenzelm@3807
   410
	   ]);
wenzelm@3807
   411
wenzelm@6255
   412
qed_goal "TLA2" TLA.thy "|- $P & P$ --> A  ==>  |- []P --> []A"
wenzelm@6255
   413
  (fn prems => [Clarsimp_tac 1,
wenzelm@6255
   414
                dtac (temp_use BoxPrime) 1,
wenzelm@6255
   415
                auto_tac (temp_css addsimps2 [Init_stp_act_rev] addSIs2 prems addSEs2 [STL4E])
wenzelm@6255
   416
               ]);
wenzelm@3807
   417
wenzelm@3807
   418
qed_goal "TLA2E" TLA.thy 
wenzelm@6255
   419
   "[| sigma |= []P; |- $P & P$ --> A |] ==> sigma |= []A"
wenzelm@6255
   420
   (fn prems => [REPEAT (resolve_tac (prems @ (prems RL [temp_use TLA2])) 1)]);
wenzelm@3807
   421
wenzelm@6255
   422
qed_goalw "DmdPrime" TLA.thy [dmd_def] "|- (<>P`) --> (<>P)"
wenzelm@3807
   423
   (fn _ => [ fast_tac (temp_cs addSEs [TLA2E]) 1 ]);
wenzelm@3807
   424
wenzelm@6255
   425
bind_thm("PrimeDmd", (temp_use InitDmd_gen) RS (temp_use DmdPrime));
wenzelm@3807
   426
wenzelm@3807
   427
(* ------------------------ INV1, stable --------------------------------------- *)
wenzelm@3807
   428
section "stable, invariant";
wenzelm@3807
   429
wenzelm@3807
   430
qed_goal "ind_rule" TLA.thy
wenzelm@6255
   431
   "[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |] \
wenzelm@6255
   432
\   ==> sigma |= []F"
wenzelm@6255
   433
   (fn prems => [rtac (temp_use indT) 1,
wenzelm@3807
   434
		 REPEAT (resolve_tac (prems @ (prems RL [STL4E])) 1)]);
wenzelm@6255
   435
wenzelm@6255
   436
qed_goalw "box_stp_act" TLA.thy [boxInit_act] "|- ([]$P) = ([]P)"
wenzelm@6255
   437
  (K [simp_tac (simpset() addsimps Init_simps) 1]);
wenzelm@6255
   438
bind_thm("box_stp_actI", zero_var_indexes ((temp_use box_stp_act) RS iffD2));
wenzelm@6255
   439
bind_thm("box_stp_actD", zero_var_indexes ((temp_use box_stp_act) RS iffD1));
wenzelm@3807
   440
wenzelm@6255
   441
val more_temp_simps = (temp_rewrite box_stp_act)::more_temp_simps;
wenzelm@3807
   442
wenzelm@6255
   443
qed_goalw "INV1" TLA.thy [stable_def,boxInit_stp,boxInit_act] 
wenzelm@6255
   444
  "|- (Init P) --> (stable P) --> []P"
wenzelm@6255
   445
  (K [Clarsimp_tac 1,
wenzelm@6255
   446
      etac ind_rule 1,
wenzelm@6255
   447
      auto_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule])
wenzelm@6255
   448
     ]);
wenzelm@6255
   449
wenzelm@6255
   450
qed_goalw "StableT" TLA.thy [stable_def]
wenzelm@6255
   451
   "|- $P & A --> P` ==> |- []A --> stable P"
wenzelm@6255
   452
   (fn [prem] => [fast_tac (temp_cs addSEs [STL4E] addIs [prem]) 1]);
wenzelm@3807
   453
wenzelm@3807
   454
qed_goal "Stable" TLA.thy
wenzelm@6255
   455
   "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P"
wenzelm@6255
   456
   (fn prems => [ REPEAT (resolve_tac (prems @ [temp_use StableT]) 1) ]);
wenzelm@3807
   457
wenzelm@3807
   458
(* Generalization of INV1 *)
wenzelm@3807
   459
qed_goalw "StableBox" TLA.thy [stable_def]
wenzelm@6255
   460
   "|- (stable P) --> [](Init P --> []P)"
wenzelm@6255
   461
   (K [Clarsimp_tac 1,
wenzelm@6255
   462
       etac dup_boxE 1,
wenzelm@6255
   463
       force_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1]) 1]);
wenzelm@6255
   464
wenzelm@3807
   465
qed_goal "DmdStable" TLA.thy 
wenzelm@6255
   466
   "|- (stable P) & <>P --> <>[]P"
wenzelm@6255
   467
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   468
             rtac DmdImpl2 1,
wenzelm@6255
   469
	     etac (temp_use StableBox) 2,
wenzelm@6255
   470
	     asm_simp_tac (simpset() addsimps [dmdInitD]) 1
wenzelm@3807
   471
	    ]);
wenzelm@3807
   472
wenzelm@3807
   473
(* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
wenzelm@3807
   474
wenzelm@3807
   475
(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
oheimb@5755
   476
fun inv_tac css = SELECT_GOAL
wenzelm@3807
   477
     (EVERY [auto_tac css,
wenzelm@3807
   478
             TRY (merge_box_tac 1),
wenzelm@6255
   479
             rtac (temp_use INV1) 1, (* fail if the goal is not a box *)
wenzelm@3807
   480
             TRYALL (etac Stable)]);
wenzelm@3807
   481
wenzelm@3807
   482
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals;
wenzelm@6255
   483
   in simple cases it may be able to handle goals like |- MyProg --> []Inv.
wenzelm@3807
   484
   In these simple cases the simplifier seems to be more useful than the
wenzelm@3807
   485
   auto-tactic, which applies too much propositional logic and simplifies
wenzelm@3807
   486
   too late.
wenzelm@3807
   487
*)
wenzelm@3807
   488
oheimb@5755
   489
fun auto_inv_tac ss = SELECT_GOAL
wenzelm@4089
   490
    ((inv_tac (claset(),ss) 1) THEN
wenzelm@6255
   491
     (TRYALL (action_simp_tac (ss addsimps [Init_stp,Init_act]) [] [squareE])));
wenzelm@3807
   492
wenzelm@3807
   493
wenzelm@3807
   494
qed_goalw "unless" TLA.thy [dmd_def]
wenzelm@6255
   495
   "|- []($P --> P` | Q`) --> (stable P) | <>Q"
wenzelm@6255
   496
   (fn _ => [clarsimp_tac (temp_css addSDs2 [BoxPrime]) 1,
wenzelm@3807
   497
	     merge_box_tac 1,
wenzelm@6255
   498
             etac swap 1,
wenzelm@3807
   499
	     fast_tac (temp_cs addSEs [Stable]) 1
wenzelm@3807
   500
	    ]);
wenzelm@3807
   501
wenzelm@3807
   502
wenzelm@3807
   503
(* --------------------- Recursive expansions --------------------------------------- *)
wenzelm@3807
   504
section "recursive expansions";
wenzelm@3807
   505
wenzelm@6255
   506
(* Recursive expansions of [] and <> for state predicates *)
wenzelm@6255
   507
qed_goal "BoxRec" TLA.thy "|- ([]P) = (Init P & []P`)"
wenzelm@6255
   508
   (fn _ => [auto_tac (temp_css addSIs2 [STL2_gen]),
wenzelm@3807
   509
	     fast_tac (temp_cs addSEs [TLA2E]) 1,
wenzelm@6255
   510
	     auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1,STL4E])
wenzelm@3807
   511
	    ]);
wenzelm@3807
   512
wenzelm@6255
   513
qed_goalw "DmdRec" TLA.thy [dmd_def, temp_rewrite BoxRec] "|- (<>P) = (Init P | <>P`)" 
wenzelm@6255
   514
  (K [ auto_tac (temp_css addsimps2 Init_simps) ]);
wenzelm@3807
   515
wenzelm@3807
   516
qed_goal "DmdRec2" TLA.thy
wenzelm@6255
   517
 "!!sigma. [| sigma |= <>P; sigma |= []~P` |] ==> sigma |= Init P"
wenzelm@6255
   518
   (K [ force_tac (temp_css addsimps2 [DmdRec,dmd_def]) 1]);
wenzelm@3807
   519
wenzelm@6255
   520
(* The "-->" part of the following is a little intricate. *)
wenzelm@6255
   521
qed_goal "InfinitePrime" TLA.thy "|- ([]<>P) = ([]<>P`)"
paulson@4477
   522
   (fn _ => [Auto_tac,
wenzelm@3807
   523
	     rtac classical 1,
wenzelm@6255
   524
	     rtac (temp_use DBImplBD) 1,
wenzelm@6255
   525
	     subgoal_tac "sigma |= <>[]P" 1,
wenzelm@3807
   526
	     fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1,
wenzelm@6255
   527
	     subgoal_tac "sigma |= <>[](<>P & []~P`)" 1,
wenzelm@6255
   528
	     force_tac (temp_css addsimps2 [boxInit_stp]
oheimb@5755
   529
			             addSEs2 [DmdImplE,STL4E,DmdRec2]) 1,
wenzelm@6255
   530
	     force_tac (temp_css addSIs2 [STL6] addsimps2 more_temp_simps) 1,
wenzelm@6255
   531
	     fast_tac (temp_cs addIs [DmdPrime] addSEs [STL4E]) 1
wenzelm@3807
   532
	    ]);
wenzelm@3807
   533
wenzelm@6255
   534
qed_goal "InfiniteEnsures" TLA.thy
wenzelm@6255
   535
   "[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P"
wenzelm@6255
   536
   (fn prems => [rewtac (temp_rewrite InfinitePrime),
wenzelm@6255
   537
                 rtac InfImpl 1,
wenzelm@6255
   538
                 REPEAT (resolve_tac prems 1)
wenzelm@6255
   539
                ]);
wenzelm@6255
   540
wenzelm@3807
   541
(* ------------------------ fairness ------------------------------------------- *)
wenzelm@3807
   542
section "fairness";
wenzelm@3807
   543
wenzelm@3807
   544
(* alternative definitions of fairness *)
wenzelm@3807
   545
qed_goalw "WF_alt" TLA.thy [WF_def,dmd_def] 
wenzelm@6255
   546
   "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)"
wenzelm@3807
   547
   (fn _ => [ fast_tac temp_cs 1 ]);
wenzelm@3807
   548
wenzelm@3807
   549
qed_goalw "SF_alt" TLA.thy [SF_def,dmd_def]
wenzelm@6255
   550
   "|- SF(A)_v = (<>[]~Enabled(<A>_v) | []<><A>_v)"
wenzelm@3807
   551
   (fn _ => [ fast_tac temp_cs 1 ]);
wenzelm@3807
   552
wenzelm@3807
   553
(* theorems to "box" fairness conditions *)
wenzelm@6255
   554
qed_goal "BoxWFI" TLA.thy "|- WF(A)_v --> []WF(A)_v"
wenzelm@6255
   555
   (fn _ => [ auto_tac (temp_css addsimps2 (WF_alt::more_temp_simps) 
wenzelm@6255
   556
                                 addSIs2 [BoxOr]) ]);
wenzelm@3807
   557
wenzelm@6255
   558
qed_goal "WF_Box" TLA.thy "|- ([]WF(A)_v) = WF(A)_v"
wenzelm@6255
   559
  (fn prems => [ fast_tac (temp_cs addSIs [BoxWFI] addSDs [STL2]) 1 ]);
wenzelm@3807
   560
wenzelm@6255
   561
qed_goal "BoxSFI" TLA.thy "|- SF(A)_v --> []SF(A)_v"
wenzelm@6255
   562
   (fn _ => [ auto_tac (temp_css addsimps2 (SF_alt::more_temp_simps) 
wenzelm@6255
   563
                                 addSIs2 [BoxOr]) ]);
wenzelm@3807
   564
wenzelm@6255
   565
qed_goal "SF_Box" TLA.thy "|- ([]SF(A)_v) = SF(A)_v"
wenzelm@6255
   566
  (fn prems => [ fast_tac (temp_cs addSIs [BoxSFI] addSDs [STL2]) 1 ]);
wenzelm@3807
   567
wenzelm@3807
   568
val more_temp_simps = more_temp_simps @ (map temp_rewrite [WF_Box, SF_Box]);
wenzelm@3807
   569
wenzelm@6255
   570
qed_goalw "SFImplWF" TLA.thy [SF_def,WF_def] "|- SF(A)_v --> WF(A)_v"
wenzelm@6255
   571
  (fn _ => [ fast_tac (temp_cs addSDs [DBImplBD]) 1 ]);
wenzelm@3807
   572
wenzelm@3807
   573
(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
wenzelm@3807
   574
val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1));
wenzelm@3807
   575
wenzelm@3807
   576
wenzelm@3807
   577
(* ------------------------------ leads-to ------------------------------ *)
wenzelm@3807
   578
wenzelm@3807
   579
section "~>";
wenzelm@3807
   580
wenzelm@6255
   581
qed_goalw "leadsto_init" TLA.thy [leadsto_def]
wenzelm@6255
   582
   "|- (Init F) & (F ~> G) --> <>G"
wenzelm@6255
   583
   (fn _ => [ auto_tac (temp_css addSDs2 [STL2]) ]);
wenzelm@3807
   584
wenzelm@6255
   585
(* |- F & (F ~> G) --> <>G *)
wenzelm@6255
   586
bind_thm("leadsto_init_temp", 
wenzelm@6255
   587
         rewrite_rule Init_simps (read_instantiate [("'a","behavior")] leadsto_init));
wenzelm@6255
   588
wenzelm@6255
   589
qed_goalw "streett_leadsto" TLA.thy [leadsto_def]
wenzelm@6255
   590
   "|- ([]<>Init F --> []<>G) = (<>(F ~> G))" (K [
oheimb@5755
   591
             Auto_tac,
wenzelm@4089
   592
             asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
wenzelm@6255
   593
             fast_tac (temp_cs addSEs [DmdImplE,STL4E]) 1,
wenzelm@6255
   594
             fast_tac (temp_cs addSIs [InitDmd] addSEs [STL4E]) 1,
wenzelm@6255
   595
             subgoal_tac "sigma |= []<><>G" 1,
wenzelm@6255
   596
             asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
wenzelm@6255
   597
             dtac (temp_use BoxDmdDmdBox) 1, atac 1,
wenzelm@6255
   598
             fast_tac (temp_cs addSEs [DmdImplE,STL4E]) 1
wenzelm@3807
   599
            ]);
wenzelm@3807
   600
wenzelm@3807
   601
qed_goal "leadsto_infinite" TLA.thy
wenzelm@6255
   602
   "|- []<>F & (F ~> G) --> []<>G"
wenzelm@6255
   603
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   604
             etac ((temp_use InitDmd) RS 
wenzelm@6255
   605
                   ((temp_unlift streett_leadsto) RS iffD2 RS mp)) 1,
wenzelm@6255
   606
             asm_simp_tac (simpset() addsimps [dmdInitD]) 1
wenzelm@3807
   607
            ]);
wenzelm@3807
   608
wenzelm@3807
   609
(* In particular, strong fairness is a Streett condition. The following
wenzelm@3807
   610
   rules are sometimes easier to use than WF2 or SF2 below.
wenzelm@3807
   611
*)
wenzelm@3807
   612
qed_goalw "leadsto_SF" TLA.thy [SF_def]
wenzelm@6255
   613
  "|- (Enabled(<A>_v) ~> <A>_v) --> SF(A)_v"
wenzelm@6255
   614
  (K [clarsimp_tac (temp_css addSEs2 [leadsto_infinite]) 1]);
wenzelm@3807
   615
wenzelm@6255
   616
qed_goal "leadsto_WF" TLA.thy 
wenzelm@6255
   617
  "|- (Enabled(<A>_v) ~> <A>_v) --> WF(A)_v"
wenzelm@6255
   618
  (K [ clarsimp_tac (temp_css addSIs2 [SFImplWF, leadsto_SF]) 1 ]);
wenzelm@3807
   619
wenzelm@3807
   620
(* introduce an invariant into the proof of a leadsto assertion.
wenzelm@6255
   621
   []I --> ((P ~> Q)  =  (P /\ I ~> Q))
wenzelm@3807
   622
*)
wenzelm@6255
   623
qed_goalw "INV_leadsto" TLA.thy [leadsto_def]
wenzelm@6255
   624
   "|- []I & (P & I ~> Q) --> (P ~> Q)"
wenzelm@6255
   625
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   626
             etac STL4Edup 1, atac 1,
wenzelm@6255
   627
	     auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2_gen])
wenzelm@3807
   628
	    ]);
wenzelm@3807
   629
wenzelm@6255
   630
qed_goalw "leadsto_classical" TLA.thy [leadsto_def,dmd_def]
wenzelm@6255
   631
   "|- (Init F & []~G ~> G) --> (F ~> G)"
wenzelm@6255
   632
   (fn _ => [force_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E]) 1]);
wenzelm@3807
   633
wenzelm@6255
   634
qed_goalw "leadsto_false" TLA.thy [leadsto_def]
wenzelm@6255
   635
  "|- (F ~> #False) = ([]~F)"
wenzelm@6255
   636
  (fn _ => [ simp_tac (simpset() addsimps [boxNotInitD]) 1 ]);
wenzelm@6255
   637
wenzelm@6255
   638
qed_goalw "leadsto_exists" TLA.thy [leadsto_def]
wenzelm@6255
   639
  "|- ((? x. F x) ~> G) = (!x. (F x ~> G))"
wenzelm@6255
   640
  (K [auto_tac (temp_css addsimps2 allT::Init_simps addSEs2 [STL4E])]);
wenzelm@6255
   641
wenzelm@3807
   642
wenzelm@3807
   643
(* basic leadsto properties, cf. Unity *)
wenzelm@3807
   644
wenzelm@6255
   645
qed_goalw "ImplLeadsto_gen" TLA.thy [leadsto_def]
wenzelm@6255
   646
   "|- [](Init F --> Init G) --> (F ~> G)"
wenzelm@6255
   647
   (fn _ => [auto_tac (temp_css addSIs2 [InitDmd_gen] 
wenzelm@6255
   648
                                addSEs2 [STL4E_gen] addsimps2 Init_simps)
wenzelm@3807
   649
	    ]);
wenzelm@3807
   650
wenzelm@6255
   651
bind_thm("ImplLeadsto",
wenzelm@6255
   652
         rewrite_rule Init_simps 
wenzelm@6255
   653
             (read_instantiate [("'a","behavior"), ("'b","behavior")] ImplLeadsto_gen));
wenzelm@6255
   654
wenzelm@6255
   655
qed_goal "ImplLeadsto_simple" TLA.thy
wenzelm@6255
   656
  "|- F --> G ==> |- F ~> G"
wenzelm@6255
   657
  (fn [prem] => [auto_tac (temp_css addsimps2 [Init_def] 
wenzelm@6255
   658
                                    addSIs2 [ImplLeadsto_gen,necT,prem])]);
wenzelm@6255
   659
wenzelm@6255
   660
qed_goalw "EnsuresLeadsto" TLA.thy [leadsto_def]
wenzelm@6255
   661
   "|- A & $P --> Q` ==> |- []A --> (P ~> Q)" (fn [prem] => [
wenzelm@6255
   662
		  clarsimp_tac (temp_css addSEs2 [INV_leadsto]) 1, 
wenzelm@6255
   663
                  etac STL4E_gen 1,
wenzelm@6255
   664
                  auto_tac (temp_css addsimps2 Init_defs
wenzelm@6255
   665
                                     addSIs2 [PrimeDmd, prem])
wenzelm@6255
   666
                 ]);
wenzelm@6255
   667
wenzelm@6255
   668
qed_goalw "EnsuresLeadsto2" TLA.thy [leadsto_def]
wenzelm@6255
   669
   "|- []($P --> Q`) --> (P ~> Q)"
wenzelm@6255
   670
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   671
             etac STL4E_gen 1,
wenzelm@6255
   672
             auto_tac (temp_css addsimps2 Init_simps addSIs2 [PrimeDmd])
wenzelm@6255
   673
            ]);
wenzelm@3807
   674
wenzelm@6255
   675
qed_goalw "ensures" TLA.thy [leadsto_def]
wenzelm@6255
   676
  "[| |- $P & N --> P` | Q`; \
wenzelm@6255
   677
\     |- ($P & N) & A --> Q` \
wenzelm@6255
   678
\  |] ==> |- []N & []([]P --> <>A) --> (P ~> Q)"
wenzelm@6255
   679
  (fn [p1,p2] => [Clarsimp_tac 1,
wenzelm@6255
   680
                  etac STL4Edup 1, atac 1,
wenzelm@6255
   681
                  Clarsimp_tac 1,
wenzelm@6255
   682
                  subgoal_tac "sigmaa |= []($P --> P` | Q`)" 1,
wenzelm@6255
   683
                   dtac (temp_use unless) 1,
wenzelm@6255
   684
                   clarsimp_tac (temp_css addSDs2 [INV1]) 1,
wenzelm@6255
   685
                   rtac ((temp_use (p2 RS DmdImpl)) RS (temp_use DmdPrime)) 1,
wenzelm@6255
   686
                   force_tac (temp_css addSIs2 [BoxDmd_simple]
wenzelm@6255
   687
                                       addsimps2 [split_box_conj,box_stp_act]) 1,
wenzelm@6255
   688
                  force_tac (temp_css addEs2 [STL4E] addDs2 [p1]) 1
wenzelm@6255
   689
                 ]);
wenzelm@6255
   690
wenzelm@6255
   691
qed_goal "ensures_simple" TLA.thy
wenzelm@6255
   692
  "[| |- $P & N --> P` | Q`; \
wenzelm@6255
   693
\     |- ($P & N) & A --> Q` \
wenzelm@6255
   694
\  |] ==> |- []N & []<>A --> (P ~> Q)"
wenzelm@6255
   695
  (fn prems => [Clarsimp_tac 1,
wenzelm@6255
   696
                rtac (temp_use ensures) 1,
wenzelm@6255
   697
                TRYALL (ares_tac prems),
wenzelm@6255
   698
                force_tac (temp_css addSEs2 [STL4E]) 1
wenzelm@6255
   699
               ]);
wenzelm@6255
   700
wenzelm@3807
   701
qed_goal "EnsuresInfinite" TLA.thy
wenzelm@6255
   702
   "[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q"
wenzelm@6255
   703
   (fn prems => [REPEAT (resolve_tac (prems @ [temp_use leadsto_infinite,
wenzelm@6255
   704
					       temp_use EnsuresLeadsto]) 1)]);
wenzelm@6255
   705
wenzelm@3807
   706
wenzelm@3807
   707
(*** Gronning's lattice rules (taken from TLP) ***)
wenzelm@3807
   708
section "Lattice rules";
wenzelm@3807
   709
wenzelm@6255
   710
qed_goalw "LatticeReflexivity" TLA.thy [leadsto_def] "|- F ~> F"
wenzelm@6255
   711
   (fn _ => [REPEAT (resolve_tac [necT,InitDmd_gen] 1)]);
wenzelm@3807
   712
wenzelm@6255
   713
qed_goalw "LatticeTransitivity" TLA.thy [leadsto_def]
wenzelm@6255
   714
   "|- (G ~> H) & (F ~> G) --> (F ~> H)"
wenzelm@6255
   715
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   716
             etac dup_boxE 1,  (* [][](Init G --> H) *)
wenzelm@3807
   717
	     merge_box_tac 1,
wenzelm@6255
   718
	     clarsimp_tac (temp_css addSEs2 [STL4E]) 1,
wenzelm@6255
   719
             rtac dup_dmdD 1,
wenzelm@6255
   720
             subgoal_tac "sigmaa |= <>Init G" 1,
wenzelm@6255
   721
             etac DmdImpl2 1, atac 1,
wenzelm@6255
   722
             asm_simp_tac (simpset() addsimps [dmdInitD]) 1
wenzelm@3807
   723
	    ]);
wenzelm@3807
   724
wenzelm@6255
   725
qed_goalw "LatticeDisjunctionElim1" TLA.thy [leadsto_def]
wenzelm@6255
   726
   "|- (F | G ~> H) --> (F ~> H)"
wenzelm@6255
   727
   (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E]) ]);
wenzelm@3807
   728
wenzelm@6255
   729
qed_goalw "LatticeDisjunctionElim2" TLA.thy [leadsto_def]
wenzelm@6255
   730
   "|- (F | G ~> H) --> (G ~> H)"
wenzelm@6255
   731
   (fn _ => [ auto_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E]) ]);
wenzelm@3807
   732
wenzelm@6255
   733
qed_goalw "LatticeDisjunctionIntro" TLA.thy [leadsto_def]
wenzelm@6255
   734
   "|- (F ~> H) & (G ~> H) --> (F | G ~> H)"
wenzelm@6255
   735
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   736
             merge_box_tac 1,
wenzelm@6255
   737
	     auto_tac (temp_css addsimps2 Init_simps addSEs2 [STL4E])
wenzelm@3807
   738
	    ]);
wenzelm@3807
   739
wenzelm@6255
   740
qed_goal "LatticeDisjunction" TLA.thy
wenzelm@6255
   741
   "|- (F | G ~> H) = ((F ~> H) & (G ~> H))"
wenzelm@6255
   742
   (fn _ => [auto_tac (temp_css addIs2 [LatticeDisjunctionIntro,
wenzelm@6255
   743
                                LatticeDisjunctionElim1, LatticeDisjunctionElim2])]);
wenzelm@6255
   744
wenzelm@3807
   745
qed_goal "LatticeDiamond" TLA.thy
wenzelm@6255
   746
   "|- (A ~> B | C) & (B ~> D) & (C ~> D) --> (A ~> D)"
wenzelm@6255
   747
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   748
             subgoal_tac "sigma |= (B | C) ~> D" 1,
wenzelm@6255
   749
	     eres_inst_tac [("G", "LIFT (B | C)")] (temp_use LatticeTransitivity) 1,
wenzelm@3807
   750
	     ALLGOALS (fast_tac (temp_cs addSIs [LatticeDisjunctionIntro]))
wenzelm@3807
   751
	    ]);
wenzelm@3807
   752
wenzelm@3807
   753
qed_goal "LatticeTriangle" TLA.thy
wenzelm@6255
   754
   "|- (A ~> D | B) & (B ~> D) --> (A ~> D)"
wenzelm@6255
   755
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   756
             subgoal_tac "sigma |= (D | B) ~> D" 1,
wenzelm@6255
   757
	     eres_inst_tac [("G", "LIFT (D | B)")] (temp_use LatticeTransitivity) 1, atac 1,
wenzelm@6255
   758
	     auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] 
wenzelm@6255
   759
                                addIs2 [LatticeReflexivity])
wenzelm@6255
   760
	    ]);
wenzelm@6255
   761
wenzelm@6255
   762
qed_goal "LatticeTriangle2" TLA.thy
wenzelm@6255
   763
   "|- (A ~> B | D) & (B ~> D) --> (A ~> D)"
wenzelm@6255
   764
   (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   765
             subgoal_tac "sigma |= B | D ~> D" 1,
wenzelm@6255
   766
	     eres_inst_tac [("G", "LIFT (B | D)")] (temp_use LatticeTransitivity) 1, atac 1,
wenzelm@6255
   767
	     auto_tac (temp_css addSIs2 [LatticeDisjunctionIntro] 
wenzelm@6255
   768
                                addIs2 [LatticeReflexivity])
wenzelm@3807
   769
	    ]);
wenzelm@3807
   770
wenzelm@3807
   771
(*** Lamport's fairness rules ***)
wenzelm@3807
   772
section "Fairness rules";
wenzelm@3807
   773
wenzelm@6255
   774
qed_goal "WF1" TLA.thy
wenzelm@6255
   775
   "[| |- $P & N  --> P` | Q`;   \
wenzelm@6255
   776
\      |- ($P & N) & <A>_v --> Q`;   \
wenzelm@6255
   777
\      |- $P & N --> $(Enabled(<A>_v)) |]   \
wenzelm@6255
   778
\  ==> |- []N & WF(A)_v --> (P ~> Q)"  (fn prems => [
wenzelm@6255
   779
             clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1,
wenzelm@6255
   780
             rtac (temp_use ensures) 1,
wenzelm@6255
   781
             TRYALL (ares_tac prems),
wenzelm@6255
   782
             etac STL4Edup 1, atac 1,
wenzelm@6255
   783
             clarsimp_tac (temp_css addsimps2 [WF_def]) 1,
wenzelm@6255
   784
             rtac (temp_use STL2) 1,
wenzelm@6255
   785
             clarsimp_tac (temp_css addSEs2 [mp] addSIs2 [InitDmd]) 1,
wenzelm@6255
   786
             resolve_tac ((map temp_use (prems RL [STL4])) RL [box_stp_actD]) 1,
wenzelm@6255
   787
             asm_simp_tac (simpset() addsimps [split_box_conj,box_stp_actI]) 1
wenzelm@6255
   788
            ]);
wenzelm@3807
   789
wenzelm@3807
   790
(* Sometimes easier to use; designed for action B rather than state predicate Q *)
wenzelm@6255
   791
qed_goalw "WF_leadsto" TLA.thy [leadsto_def]
wenzelm@6255
   792
   "[| |- N & $P --> $Enabled (<A>_v);            \
wenzelm@6255
   793
\      |- N & <A>_v --> B;                  \ 
wenzelm@6255
   794
\      |- [](N & [~A]_v) --> stable P  |]  \
wenzelm@6255
   795
\   ==> |- []N & WF(A)_v --> (P ~> B)"
wenzelm@3807
   796
   (fn [prem1,prem2,prem3]
wenzelm@6255
   797
       => [clarsimp_tac (temp_css addSDs2 [BoxWFI]) 1,
wenzelm@3807
   798
           etac STL4Edup 1, atac 1,
wenzelm@6255
   799
           Clarsimp_tac 1,
wenzelm@6255
   800
           rtac (temp_use (prem2 RS DmdImpl)) 1,
wenzelm@6255
   801
           rtac (temp_use BoxDmd_simple) 1, atac 1,
wenzelm@3807
   802
           rtac classical 1,
wenzelm@6255
   803
           rtac (temp_use STL2) 1,
wenzelm@6255
   804
           clarsimp_tac (temp_css addsimps2 [WF_def] addSEs2 [mp] addSIs2 [InitDmd]) 1,
wenzelm@6255
   805
           rtac ((temp_use (prem1 RS STL4)) RS box_stp_actD) 1,
wenzelm@6255
   806
           asm_simp_tac (simpset() addsimps [split_box_conj,box_stp_act]) 1,
wenzelm@6255
   807
           etac (temp_use INV1) 1,
wenzelm@6255
   808
           rtac (temp_use prem3) 1,
wenzelm@6255
   809
           asm_full_simp_tac (simpset() addsimps [split_box_conj,temp_use NotDmd,not_angle]) 1
wenzelm@3807
   810
          ]);
wenzelm@3807
   811
wenzelm@6255
   812
qed_goal "SF1" TLA.thy
wenzelm@6255
   813
   "[| |- $P & N  --> P` | Q`;   \
wenzelm@6255
   814
\      |- ($P & N) & <A>_v --> Q`;   \
wenzelm@6255
   815
\      |- []P & []N & []F --> <>Enabled(<A>_v) |]   \
wenzelm@6255
   816
\  ==> |- []N & SF(A)_v & []F --> (P ~> Q)"
wenzelm@6255
   817
   (fn prems => [
wenzelm@6255
   818
             clarsimp_tac (temp_css addSDs2 [BoxSFI]) 1,
wenzelm@6255
   819
             rtac (temp_use ensures) 1,
wenzelm@6255
   820
             TRYALL (ares_tac prems),
wenzelm@6255
   821
             eres_inst_tac [("F","F")] dup_boxE 1,
wenzelm@6255
   822
             merge_temp_box_tac 1,
wenzelm@6255
   823
             etac STL4Edup 1, atac 1,
wenzelm@6255
   824
             clarsimp_tac (temp_css addsimps2 [SF_def]) 1,
wenzelm@6255
   825
             rtac (temp_use STL2) 1, etac mp 1,
wenzelm@6255
   826
             resolve_tac (map temp_use (prems RL [STL4])) 1,
wenzelm@6255
   827
             asm_simp_tac (simpset() addsimps [split_box_conj, STL3]) 1
wenzelm@6255
   828
            ]);
wenzelm@3807
   829
wenzelm@3807
   830
qed_goal "WF2" TLA.thy
wenzelm@6255
   831
   "[| |- N & <B>_f --> <M>_g;   \
wenzelm@6255
   832
\      |- $P & P` & <N & A>_f --> B;   \
wenzelm@6255
   833
\      |- P & Enabled(<M>_g) --> Enabled(<A>_f);   \
wenzelm@6255
   834
\      |- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P |]   \
wenzelm@6255
   835
\  ==> |- []N & WF(A)_f & []F --> WF(M)_g"
wenzelm@6255
   836
(fn [prem1,prem2,prem3,prem4] => [
wenzelm@6255
   837
	   clarsimp_tac (temp_css addSDs2 [BoxWFI, (temp_use BoxDmdBox) RS iffD2] 
wenzelm@6255
   838
                            addsimps2 [read_instantiate [("A","M")] WF_def]) 1,
wenzelm@6255
   839
           eres_inst_tac [("F","F")] dup_boxE 1,
wenzelm@6255
   840
           merge_temp_box_tac 1,
wenzelm@6255
   841
           etac STL4Edup 1, atac 1,
wenzelm@6255
   842
           clarsimp_tac (temp_css addSIs2 [(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1,
wenzelm@6255
   843
           rtac classical 1,
wenzelm@6255
   844
           subgoal_tac "sigmaa |= <>(($P & P` & N) & <A>_f)" 1,
wenzelm@6255
   845
           force_tac (temp_css addsimps2 [angle_def] addSIs2 [prem2] addSEs2 [DmdImplE]) 1,
wenzelm@6255
   846
           rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1,
wenzelm@6255
   847
           asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1,
wenzelm@6255
   848
           merge_act_box_tac 1,
wenzelm@6255
   849
           forward_tac [temp_use prem4] 1, TRYALL atac,
wenzelm@6255
   850
           dtac (temp_use STL6) 1, atac 1, 
wenzelm@6255
   851
           eres_inst_tac [("V","sigmaa |= <>[]P")] thin_rl 1,
wenzelm@6255
   852
           eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1,
wenzelm@6255
   853
           dtac (temp_use BoxWFI) 1,
wenzelm@6255
   854
           eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1,
wenzelm@6255
   855
           merge_temp_box_tac 1,
wenzelm@6255
   856
           etac DmdImpldup 1, atac 1,
wenzelm@6255
   857
           auto_tac (temp_css addsimps2 [split_box_conj,STL3,WF_Box,box_stp_act]),
wenzelm@6255
   858
           force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1,
wenzelm@6255
   859
           rtac (temp_use STL2) 1,
wenzelm@6255
   860
           force_tac (temp_css addsimps2 [WF_def,split_box_conj] addSEs2 [mp] 
wenzelm@6255
   861
                               addSIs2 [InitDmd, prem3 RS STL4]) 1
wenzelm@3807
   862
	  ]);
wenzelm@3807
   863
wenzelm@3807
   864
qed_goal "SF2" TLA.thy
wenzelm@6255
   865
   "[| |- N & <B>_f --> <M>_g;   \
wenzelm@6255
   866
\      |- $P & P` & <N & A>_f --> B;   \
wenzelm@6255
   867
\      |- P & Enabled(<M>_g) --> Enabled(<A>_f);   \
wenzelm@6255
   868
\      |- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P |]   \
wenzelm@6255
   869
\  ==> |- []N & SF(A)_f & []F --> SF(M)_g"
wenzelm@6255
   870
(fn [prem1,prem2,prem3,prem4] => [
wenzelm@6255
   871
	   clarsimp_tac (temp_css addSDs2 [BoxSFI] 
wenzelm@6255
   872
                            addsimps2 [read_instantiate [("A","M")] SF_def]) 1,
wenzelm@6255
   873
           eres_inst_tac [("F","F")] dup_boxE 1,
wenzelm@6255
   874
           eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1,
wenzelm@6255
   875
           merge_temp_box_tac 1,
wenzelm@6255
   876
           etac STL4Edup 1, atac 1,
wenzelm@6255
   877
           clarsimp_tac (temp_css addSIs2 [(temp_use BoxDmd_simple) RS (temp_use (prem1 RS DmdImpl))]) 1,
wenzelm@6255
   878
           rtac classical 1,
wenzelm@6255
   879
           subgoal_tac "sigmaa |= <>(($P & P` & N) & <A>_f)" 1,
wenzelm@6255
   880
           force_tac (temp_css addsimps2 [angle_def] addSIs2 [prem2] addSEs2 [DmdImplE]) 1,
wenzelm@6255
   881
           rtac (temp_use (rewrite_rule [temp_rewrite DmdDmd] (BoxDmd_simple RS DmdImpl))) 1,
wenzelm@6255
   882
           asm_full_simp_tac (simpset() addsimps [temp_use NotDmd, not_angle]) 1,
wenzelm@6255
   883
           merge_act_box_tac 1,
wenzelm@6255
   884
           forward_tac [temp_use prem4] 1, TRYALL atac,
wenzelm@6255
   885
           eres_inst_tac [("V","sigmaa |= []F")] thin_rl 1,
wenzelm@6255
   886
           dtac (temp_use BoxSFI) 1,
wenzelm@6255
   887
           eres_inst_tac [("F","TEMP <>Enabled(<M>_g)")] dup_boxE 1,
wenzelm@6255
   888
           eres_inst_tac [("F", "ACT N & [~B]_f")] dup_boxE 1,
wenzelm@6255
   889
           merge_temp_box_tac 1,
wenzelm@6255
   890
           etac DmdImpldup 1, atac 1,
wenzelm@6255
   891
           auto_tac (temp_css addsimps2 [split_box_conj,STL3,SF_Box,box_stp_act]),
wenzelm@6255
   892
           force_tac (temp_css addSEs2 [read_instantiate [("P","P")] TLA2E]) 1,
wenzelm@6255
   893
           rtac (temp_use STL2) 1,
wenzelm@6255
   894
           force_tac (temp_css addsimps2 [SF_def,split_box_conj] addSEs2 [mp,InfImpl] 
wenzelm@6255
   895
                               addSIs2 [prem3]) 1
wenzelm@3807
   896
	  ]);
wenzelm@3807
   897
wenzelm@3807
   898
(* ------------------------------------------------------------------------- *)
wenzelm@3807
   899
(***           Liveness proofs by well-founded orderings                   ***)
wenzelm@3807
   900
(* ------------------------------------------------------------------------- *)
wenzelm@3807
   901
section "Well-founded orderings";
wenzelm@3807
   902
wenzelm@6255
   903
qed_goal "wf_leadsto" TLA.thy
wenzelm@6255
   904
  "[| wf r;  \
wenzelm@6255
   905
\     !!x. sigma |= F x ~> (G | (? y. #((y,x):r) & F y))   \
wenzelm@6255
   906
\  |] ==> sigma |= F x ~> G"
wenzelm@6255
   907
  (fn p1::prems =>
wenzelm@6255
   908
     [rtac (p1 RS wf_induct) 1,
wenzelm@6255
   909
      rtac (temp_use LatticeTriangle) 1,
wenzelm@6255
   910
      resolve_tac prems 1,
wenzelm@6255
   911
      auto_tac (temp_css addsimps2 [leadsto_exists]),
wenzelm@6255
   912
      case_tac "(y,x):r" 1,
wenzelm@6255
   913
       Force_tac 1,
wenzelm@6255
   914
      force_tac (temp_css addsimps2 leadsto_def::Init_simps addSIs2 [necT]) 1]);
wenzelm@3807
   915
wenzelm@3807
   916
(* If r is well-founded, state function v cannot decrease forever *)
wenzelm@3807
   917
qed_goal "wf_not_box_decrease" TLA.thy
wenzelm@6255
   918
  "!!r. wf r ==> |- [][ (v`, $v) : #r ]_v --> <>[][#False]_v"
wenzelm@6255
   919
  (fn _ => [Clarsimp_tac 1,
wenzelm@6255
   920
            rtac ccontr 1,
wenzelm@6255
   921
            subgoal_tac "sigma |= (? x. v=#x) ~> #False" 1,
wenzelm@6255
   922
             dtac ((temp_use leadsto_false) RS iffD1 RS (temp_use STL2_gen)) 1,
wenzelm@6255
   923
             force_tac (temp_css addsimps2 Init_defs) 1,
wenzelm@6255
   924
            clarsimp_tac (temp_css addsimps2 [leadsto_exists,not_square]@more_temp_simps) 1,
wenzelm@6255
   925
            etac wf_leadsto 1,
wenzelm@6255
   926
            rtac (temp_use ensures_simple) 1, TRYALL atac,
wenzelm@6255
   927
            auto_tac (temp_css addsimps2 [square_def,angle_def])
wenzelm@3807
   928
           ]);
wenzelm@3807
   929
wenzelm@6255
   930
(* "wf r  ==>  |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *)
wenzelm@3807
   931
bind_thm("wf_not_dmd_box_decrease",
wenzelm@3807
   932
         standard(rewrite_rule more_temp_simps (wf_not_box_decrease RS DmdImpl)));
wenzelm@3807
   933
wenzelm@6255
   934
(* If there are infinitely many steps where v decreases, then there
wenzelm@3807
   935
   have to be infinitely many non-stuttering steps where v doesn't decrease.
wenzelm@3807
   936
*)
wenzelm@3807
   937
qed_goal "wf_box_dmd_decrease" TLA.thy
wenzelm@6255
   938
  "wf r ==> |- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v"
wenzelm@6255
   939
  (fn [prem] => [
wenzelm@6255
   940
            Clarsimp_tac 1,
wenzelm@6255
   941
            rtac ccontr 1,
wenzelm@6255
   942
            asm_full_simp_tac (simpset() addsimps not_angle::more_temp_simps) 1,
wenzelm@6255
   943
            dtac (prem RS (temp_use wf_not_dmd_box_decrease)) 1,
wenzelm@6255
   944
            dtac (temp_use BoxDmdDmdBox) 1, atac 1,
wenzelm@6255
   945
            subgoal_tac "sigma |= []<>((#False)::action)" 1,
wenzelm@6255
   946
            Force_tac 1,
wenzelm@6255
   947
            etac STL4E 1,
wenzelm@6255
   948
            rtac DmdImpl 1,
wenzelm@6255
   949
            force_tac (temp_css addSEs2 [prem RS wf_irrefl]) 1
wenzelm@6255
   950
           ]);
wenzelm@3807
   951
wenzelm@3807
   952
(* In particular, for natural numbers, if n decreases infinitely often
wenzelm@3807
   953
   then it has to increase infinitely often.
wenzelm@3807
   954
*)
wenzelm@6255
   955
qed_goal "nat_box_dmd_decrease" TLA.thy
wenzelm@6255
   956
  "!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)"
wenzelm@6255
   957
  (K [Clarsimp_tac 1,
wenzelm@6255
   958
      subgoal_tac "sigma |= []<><~( (n`,$n) : #less_than )>_n" 1,
wenzelm@6255
   959
      etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
wenzelm@6255
   960
      clarsimp_tac (temp_css addsimps2 [angle_def]) 1,
wenzelm@6255
   961
      rtac nat_less_cases 1,
wenzelm@6255
   962
      Auto_tac,
wenzelm@6255
   963
      rtac (temp_use wf_box_dmd_decrease) 1,
wenzelm@6255
   964
      auto_tac (temp_css addSEs2 [STL4E,DmdImplE])
wenzelm@6255
   965
     ]);
wenzelm@6255
   966
wenzelm@3807
   967
wenzelm@3807
   968
(* ------------------------------------------------------------------------- *)
wenzelm@3807
   969
(***           Flexible quantification over state variables                ***)
wenzelm@3807
   970
(* ------------------------------------------------------------------------- *)
wenzelm@3807
   971
section "Flexible quantification";
wenzelm@3807
   972
wenzelm@3807
   973
qed_goal "aallI" TLA.thy 
wenzelm@6255
   974
  "[| basevars vs; (!!x. basevars (x,vs) ==> sigma |= F x) |] ==> sigma |= (AALL x. F x)"
wenzelm@6255
   975
  (fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] 
wenzelm@6255
   976
                                   addSIs2 prems addSDs2 prems)]);
wenzelm@3807
   977
wenzelm@6255
   978
qed_goalw "aallE" TLA.thy [aall_def] "|- (AALL x. F x) --> F x"
wenzelm@6255
   979
   (K [Clarsimp_tac 1, etac swap 1,
wenzelm@6255
   980
       force_tac (temp_css addSIs2 [eexI]) 1]);
wenzelm@3807
   981
wenzelm@3807
   982
(* monotonicity of quantification *)
wenzelm@3807
   983
qed_goal "eex_mono" TLA.thy
wenzelm@6255
   984
  "[| sigma |= EEX x. F x; !!x. sigma |= F x --> G x |] ==> sigma |= EEX x. G x"
wenzelm@6255
   985
  (fn [min,maj] => [rtac (unit_base RS (min RS eexE)) 1,
wenzelm@6255
   986
                    rtac (temp_use eexI) 1,
wenzelm@6255
   987
                    etac ((rewrite_rule intensional_rews maj) RS mp) 1
wenzelm@3807
   988
                   ]);
wenzelm@3807
   989
wenzelm@3807
   990
qed_goal "aall_mono" TLA.thy
wenzelm@6255
   991
  "[| sigma |= AALL x. F(x); !!x. sigma |= F(x) --> G(x) |] ==> sigma |= AALL x. G(x)"
wenzelm@6255
   992
  (fn [min,maj] => [rtac (unit_base RS aallI) 1,
wenzelm@6255
   993
                    rtac ((rewrite_rule intensional_rews maj) RS mp) 1,
wenzelm@6255
   994
                    rtac (min RS (temp_use aallE)) 1
wenzelm@3807
   995
                   ]);
wenzelm@3807
   996
wenzelm@6255
   997
(* Derived history introduction rule *)
wenzelm@6255
   998
qed_goal "historyI" TLA.thy
wenzelm@6255
   999
  "[| sigma |= Init I; sigma |= []N; basevars vs; \
wenzelm@6255
  1000
\     (!!h. basevars(h,vs) ==> |- I & h = ha --> HI h); \
wenzelm@6255
  1001
\     (!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)) \
wenzelm@6255
  1002
\  |] ==> sigma |= EEX h. Init (HI h) & [](HN h)" 
wenzelm@6255
  1003
  (fn [p1,p2,p3,p4,p5] 
wenzelm@6255
  1004
   => [rtac ((temp_use history) RS eexE) 1,
wenzelm@6255
  1005
       rtac p3 1,
wenzelm@6255
  1006
       rtac (temp_use eexI) 1,
wenzelm@6255
  1007
       Clarsimp_tac 1, rtac conjI 1,
wenzelm@6255
  1008
       cut_facts_tac [p2] 2,
wenzelm@6255
  1009
       merge_box_tac 2,
wenzelm@6255
  1010
       force_tac (temp_css addSEs2 [STL4E,p5]) 2,
wenzelm@6255
  1011
       cut_facts_tac [p1] 1,
wenzelm@6255
  1012
       force_tac (temp_css addsimps2 Init_defs addSEs2 [p4]) 1
wenzelm@6255
  1013
      ]);
wenzelm@6255
  1014
wenzelm@3807
  1015
(* ----------------------------------------------------------------------
wenzelm@3807
  1016
   example of a history variable: existence of a clock
wenzelm@3807
  1017
wenzelm@6255
  1018
Goal "|- EEX h. Init(h = #True) & [](h` = (~$h))";
wenzelm@4423
  1019
by (rtac tempI 1);
wenzelm@4423
  1020
by (rtac historyI 1);
wenzelm@6255
  1021
by (REPEAT (force_tac (temp_css addsimps2 Init_defs addIs2 [unit_base, necT]) 1));
wenzelm@3807
  1022
(** solved **)
wenzelm@3807
  1023
wenzelm@3807
  1024
---------------------------------------------------------------------- *)
wenzelm@6255
  1025