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