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