src/HOL/UNITY/WFair.ML
author paulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826 c6a8b73b6c2a
parent 7594 8a188ef6545e
child 7963 e7beff82e1ba
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
paulson@4776
     1
(*  Title:      HOL/UNITY/WFair
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Weak Fairness versions of transient, ensures, leadsTo.
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     9
*)
paulson@4776
    10
paulson@4776
    11
paulson@5648
    12
overload_1st_set "WFair.transient";
paulson@5648
    13
overload_1st_set "WFair.ensures";
paulson@6536
    14
overload_1st_set "WFair.op leadsTo";
paulson@5340
    15
paulson@4776
    16
(*** transient ***)
paulson@4776
    17
wenzelm@5069
    18
Goalw [stable_def, constrains_def, transient_def]
paulson@5648
    19
    "[| F : stable A; F : transient A |] ==> A = {}";
paulson@4776
    20
by (Blast_tac 1);
paulson@4776
    21
qed "stable_transient_empty";
paulson@4776
    22
wenzelm@5069
    23
Goalw [transient_def]
paulson@5648
    24
    "[| F : transient A; B<=A |] ==> F : transient B";
paulson@4776
    25
by (Clarify_tac 1);
paulson@6012
    26
by (blast_tac (claset() addSIs [rev_bexI]) 1);
paulson@4776
    27
qed "transient_strengthen";
paulson@4776
    28
wenzelm@5069
    29
Goalw [transient_def]
paulson@5648
    30
    "[| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> F : transient A";
paulson@4776
    31
by (Blast_tac 1);
paulson@4776
    32
qed "transient_mem";
paulson@4776
    33
paulson@7826
    34
Goalw [transient_def] "transient UNIV = {}";
paulson@7826
    35
by Auto_tac;
paulson@7826
    36
qed "transient_UNIV";
paulson@7826
    37
paulson@7826
    38
Goalw [transient_def] "transient {} = UNIV";
paulson@7826
    39
by Auto_tac;
paulson@7826
    40
qed "transient_empty";
paulson@7826
    41
Addsimps [transient_UNIV, transient_empty];
paulson@7826
    42
paulson@4776
    43
paulson@4776
    44
(*** ensures ***)
paulson@4776
    45
wenzelm@5069
    46
Goalw [ensures_def]
paulson@7524
    47
    "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B";
paulson@4776
    48
by (Blast_tac 1);
paulson@4776
    49
qed "ensuresI";
paulson@4776
    50
wenzelm@5069
    51
Goalw [ensures_def]
paulson@6536
    52
    "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)";
paulson@4776
    53
by (Blast_tac 1);
paulson@4776
    54
qed "ensuresD";
paulson@4776
    55
paulson@4776
    56
(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
wenzelm@5069
    57
Goalw [ensures_def]
paulson@6536
    58
    "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
paulson@4776
    59
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
paulson@4776
    60
qed "ensures_weaken_R";
paulson@4776
    61
wenzelm@5069
    62
Goalw [ensures_def, constrains_def, transient_def]
paulson@6536
    63
    "F : A ensures UNIV";
paulson@5340
    64
by Auto_tac;
paulson@4776
    65
qed "ensures_UNIV";
paulson@4776
    66
wenzelm@5069
    67
Goalw [ensures_def]
paulson@5648
    68
    "[| F : stable C; \
paulson@6536
    69
\       F : (C Int (A - A')) co (A Un A'); \
paulson@5648
    70
\       F : transient (C Int (A-A')) |]   \
paulson@6536
    71
\   ==> F : (C Int A) ensures (C Int A')";
paulson@4776
    72
by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
paulson@4776
    73
				      Diff_Int_distrib RS sym,
paulson@4776
    74
				      stable_constrains_Int]) 1);
paulson@4776
    75
qed "stable_ensures_Int";
paulson@4776
    76
paulson@6536
    77
Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B";
paulson@5640
    78
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
paulson@5640
    79
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
paulson@5640
    80
qed "stable_transient_ensures";
paulson@5640
    81
paulson@4776
    82
paulson@4776
    83
(*** leadsTo ***)
paulson@4776
    84
paulson@6536
    85
Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B";
paulson@6801
    86
by (blast_tac (claset() addIs [leads.Basis]) 1);
paulson@5648
    87
qed "leadsTo_Basis";
paulson@4776
    88
paulson@5648
    89
Goalw [leadsTo_def]
paulson@6536
    90
     "[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C";
paulson@6801
    91
by (blast_tac (claset() addIs [leads.Trans]) 1);
paulson@5648
    92
qed "leadsTo_Trans";
paulson@5648
    93
paulson@6536
    94
Goal "F : transient A ==> F : A leadsTo (-A)";
paulson@5640
    95
by (asm_simp_tac 
paulson@5640
    96
    (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
paulson@5640
    97
qed "transient_imp_leadsTo";
paulson@5640
    98
paulson@6536
    99
Goal "F : A leadsTo UNIV";
paulson@4776
   100
by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
paulson@4776
   101
qed "leadsTo_UNIV";
paulson@4776
   102
Addsimps [leadsTo_UNIV];
paulson@4776
   103
paulson@4776
   104
(*Useful with cancellation, disjunction*)
paulson@6536
   105
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
paulson@4776
   106
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
paulson@4776
   107
qed "leadsTo_Un_duplicate";
paulson@4776
   108
paulson@6536
   109
Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)";
paulson@4776
   110
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
paulson@4776
   111
qed "leadsTo_Un_duplicate2";
paulson@4776
   112
paulson@4776
   113
(*The Union introduction rule as we should have liked to state it*)
paulson@5648
   114
val prems = Goalw [leadsTo_def]
paulson@6536
   115
    "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B";
paulson@6801
   116
by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
paulson@4776
   117
qed "leadsTo_Union";
paulson@4776
   118
paulson@6295
   119
val prems = Goalw [leadsTo_def]
paulson@7524
   120
 "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B";
paulson@6295
   121
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
paulson@6801
   122
by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
paulson@6295
   123
qed "leadsTo_Union_Int";
paulson@6295
   124
paulson@5648
   125
val prems = Goal
paulson@6536
   126
    "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B";
paulson@6295
   127
by (stac (Union_image_eq RS sym) 1);
paulson@5648
   128
by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
paulson@4776
   129
qed "leadsTo_UN";
paulson@4776
   130
paulson@4776
   131
(*Binary union introduction rule*)
paulson@6536
   132
Goal "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C";
paulson@4776
   133
by (stac Un_eq_Union 1);
paulson@4776
   134
by (blast_tac (claset() addIs [leadsTo_Union]) 1);
paulson@4776
   135
qed "leadsTo_Un";
paulson@4776
   136
paulson@6714
   137
val prems = 
paulson@6714
   138
Goal "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B";
paulson@6714
   139
by (stac (UN_singleton RS sym) 1 THEN rtac leadsTo_UN 1);
paulson@6714
   140
by (blast_tac (claset() addIs prems) 1);
paulson@6714
   141
qed "single_leadsTo_I";
paulson@6714
   142
paulson@4776
   143
paulson@4776
   144
(*The INDUCTION rule as we should have liked to state it*)
paulson@5648
   145
val major::prems = Goalw [leadsTo_def]
paulson@6536
   146
  "[| F : za leadsTo zb;  \
paulson@6536
   147
\     !!A B. F : A ensures B ==> P A B; \
paulson@6536
   148
\     !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] \
paulson@4776
   149
\              ==> P A C; \
paulson@6536
   150
\     !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \
paulson@4776
   151
\  |] ==> P za zb";
paulson@6801
   152
by (rtac (major RS CollectD RS leads.induct) 1);
paulson@4776
   153
by (REPEAT (blast_tac (claset() addIs prems) 1));
paulson@4776
   154
qed "leadsTo_induct";
paulson@4776
   155
paulson@4776
   156
paulson@7594
   157
Goal "A<=B ==> F : A ensures B";
paulson@4776
   158
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
paulson@4776
   159
by (Blast_tac 1);
paulson@7594
   160
qed "subset_imp_ensures";
paulson@7594
   161
paulson@7594
   162
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis);
paulson@4776
   163
paulson@4776
   164
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
paulson@4776
   165
Addsimps [empty_leadsTo];
paulson@4776
   166
paulson@4776
   167
paulson@6536
   168
Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
paulson@5648
   169
by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
paulson@5648
   170
qed "leadsTo_weaken_R";
paulson@4776
   171
paulson@6536
   172
Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
paulson@6295
   173
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
paulson@4776
   174
qed_spec_mp "leadsTo_weaken_L";
paulson@4776
   175
paulson@4776
   176
(*Distributes over binary unions*)
paulson@6536
   177
Goal "F : (A Un B) leadsTo C  =  (F : A leadsTo C & F : B leadsTo C)";
paulson@4776
   178
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
paulson@4776
   179
qed "leadsTo_Un_distrib";
paulson@4776
   180
paulson@6536
   181
Goal "F : (UN i:I. A i) leadsTo B  =  (ALL i : I. F : (A i) leadsTo B)";
paulson@4776
   182
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
paulson@4776
   183
qed "leadsTo_UN_distrib";
paulson@4776
   184
paulson@6536
   185
Goal "F : (Union S) leadsTo B  =  (ALL A : S. F : A leadsTo B)";
paulson@4776
   186
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
paulson@4776
   187
qed "leadsTo_Union_distrib";
paulson@4776
   188
paulson@4776
   189
paulson@6536
   190
Goal "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'";
paulson@5340
   191
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
paulson@5340
   192
			       leadsTo_Trans]) 1);
paulson@4776
   193
qed "leadsTo_weaken";
paulson@4776
   194
paulson@4776
   195
paulson@4776
   196
(*Set difference: maybe combine with leadsTo_weaken_L??*)
paulson@6536
   197
Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C";
paulson@4776
   198
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
paulson@4776
   199
qed "leadsTo_Diff";
paulson@4776
   200
paulson@4776
   201
paulson@4776
   202
(** Meta or object quantifier ???
paulson@4776
   203
    see ball_constrains_UN in UNITY.ML***)
paulson@4776
   204
paulson@4776
   205
val prems = goal thy
paulson@6536
   206
   "(!! i. i:I ==> F : (A i) leadsTo (A' i)) \
paulson@6536
   207
\   ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)";
paulson@6295
   208
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
paulson@4776
   209
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
paulson@4776
   210
                        addIs prems) 1);
paulson@4776
   211
qed "leadsTo_UN_UN";
paulson@4776
   212
paulson@4776
   213
paulson@4776
   214
(*Version with no index set*)
paulson@4776
   215
val prems = goal thy
paulson@6536
   216
   "(!! i. F : (A i) leadsTo (A' i)) \
paulson@6536
   217
\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
paulson@4776
   218
by (blast_tac (claset() addIs [leadsTo_UN_UN] 
paulson@4776
   219
                        addIs prems) 1);
paulson@4776
   220
qed "leadsTo_UN_UN_noindex";
paulson@4776
   221
paulson@4776
   222
(*Version with no index set*)
paulson@6536
   223
Goal "ALL i. F : (A i) leadsTo (A' i) \
paulson@6536
   224
\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
paulson@4776
   225
by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
paulson@4776
   226
qed "all_leadsTo_UN_UN";
paulson@4776
   227
paulson@4776
   228
paulson@4776
   229
(*Binary union version*)
paulson@6714
   230
Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
paulson@6714
   231
\     ==> F : (A Un B) leadsTo (A' Un B')";
paulson@4776
   232
by (blast_tac (claset() addIs [leadsTo_Un, 
paulson@4776
   233
			       leadsTo_weaken_R]) 1);
paulson@4776
   234
qed "leadsTo_Un_Un";
paulson@4776
   235
paulson@4776
   236
paulson@4776
   237
(** The cancellation law **)
paulson@4776
   238
paulson@6536
   239
Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \
paulson@6714
   240
\     ==> F : A leadsTo (A' Un B')";
paulson@4776
   241
by (blast_tac (claset() addIs [leadsTo_Un_Un, 
paulson@4776
   242
			       subset_imp_leadsTo, leadsTo_Trans]) 1);
paulson@4776
   243
qed "leadsTo_cancel2";
paulson@4776
   244
paulson@6536
   245
Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \
paulson@6714
   246
\     ==> F : A leadsTo (A' Un B')";
paulson@4776
   247
by (rtac leadsTo_cancel2 1);
paulson@4776
   248
by (assume_tac 2);
paulson@4776
   249
by (ALLGOALS Asm_simp_tac);
paulson@4776
   250
qed "leadsTo_cancel_Diff2";
paulson@4776
   251
paulson@6536
   252
Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \
paulson@6536
   253
\   ==> F : A leadsTo (B' Un A')";
paulson@4776
   254
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
paulson@4776
   255
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
paulson@4776
   256
qed "leadsTo_cancel1";
paulson@4776
   257
paulson@6536
   258
Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \
paulson@6536
   259
\   ==> F : A leadsTo (B' Un A')";
paulson@4776
   260
by (rtac leadsTo_cancel1 1);
paulson@4776
   261
by (assume_tac 2);
paulson@4776
   262
by (ALLGOALS Asm_simp_tac);
paulson@4776
   263
qed "leadsTo_cancel_Diff1";
paulson@4776
   264
paulson@4776
   265
paulson@4776
   266
paulson@4776
   267
(** The impossibility law **)
paulson@4776
   268
paulson@6536
   269
Goal "F : A leadsTo B ==> B={} --> A={}";
paulson@4776
   270
by (etac leadsTo_induct 1);
paulson@4776
   271
by (ALLGOALS Asm_simp_tac);
paulson@4776
   272
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
paulson@4776
   273
by (Blast_tac 1);
paulson@4776
   274
val lemma = result() RS mp;
paulson@4776
   275
paulson@6536
   276
Goal "F : A leadsTo {} ==> A={}";
paulson@4776
   277
by (blast_tac (claset() addSIs [lemma]) 1);
paulson@4776
   278
qed "leadsTo_empty";
paulson@4776
   279
paulson@4776
   280
paulson@4776
   281
(** PSP: Progress-Safety-Progress **)
paulson@4776
   282
paulson@5640
   283
(*Special case of PSP: Misra's "stable conjunction"*)
wenzelm@5069
   284
Goalw [stable_def]
paulson@6536
   285
   "[| F : A leadsTo A'; F : stable B |] \
paulson@6536
   286
\   ==> F : (A Int B) leadsTo (A' Int B)";
paulson@4776
   287
by (etac leadsTo_induct 1);
paulson@6295
   288
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
paulson@4776
   289
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
paulson@4776
   290
by (rtac leadsTo_Basis 1);
paulson@4776
   291
by (asm_full_simp_tac
paulson@4776
   292
    (simpset() addsimps [ensures_def, 
paulson@4776
   293
			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
paulson@4776
   294
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
paulson@5277
   295
qed "psp_stable";
paulson@4776
   296
paulson@7524
   297
Goal
paulson@7524
   298
   "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')";
paulson@5536
   299
by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
paulson@5277
   300
qed "psp_stable2";
paulson@4776
   301
paulson@5277
   302
Goalw [ensures_def, constrains_def]
paulson@6536
   303
   "[| F : A ensures A'; F : B co B' |] \
paulson@6714
   304
\   ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))";
paulson@6714
   305
by (Clarify_tac 1);  (*speeds up the proof*)
paulson@5277
   306
by (blast_tac (claset() addIs [transient_strengthen]) 1);
paulson@5277
   307
qed "psp_ensures";
paulson@4776
   308
paulson@6536
   309
Goal "[| F : A leadsTo A'; F : B co B' |] \
paulson@6714
   310
\     ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))";
paulson@4776
   311
by (etac leadsTo_induct 1);
paulson@6295
   312
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
paulson@4776
   313
(*Transitivity case has a delicate argument involving "cancellation"*)
paulson@4776
   314
by (rtac leadsTo_Un_duplicate2 2);
paulson@4776
   315
by (etac leadsTo_cancel_Diff1 2);
paulson@4776
   316
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
paulson@6714
   317
by (blast_tac (claset() addIs [leadsTo_weaken_L] 
paulson@6714
   318
                        addDs [constrains_imp_subset]) 2);
paulson@4776
   319
(*Basis case*)
paulson@5277
   320
by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
paulson@5277
   321
qed "psp";
paulson@4776
   322
paulson@6536
   323
Goal "[| F : A leadsTo A'; F : B co B' |] \
paulson@6714
   324
\   ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))";
paulson@5536
   325
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
paulson@5277
   326
qed "psp2";
paulson@4776
   327
paulson@4776
   328
wenzelm@5069
   329
Goalw [unless_def]
paulson@6536
   330
   "[| F : A leadsTo A';  F : B unless B' |] \
paulson@6536
   331
\   ==> F : (A Int B) leadsTo ((A' Int B) Un B')";
paulson@5277
   332
by (dtac psp 1);
paulson@4776
   333
by (assume_tac 1);
paulson@6714
   334
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
paulson@5277
   335
qed "psp_unless";
paulson@4776
   336
paulson@4776
   337
paulson@4776
   338
(*** Proving the induction rules ***)
paulson@4776
   339
paulson@5257
   340
(** The most general rule: r is any wf relation; f is any variant function **)
paulson@5257
   341
paulson@5239
   342
Goal "[| wf r;     \
paulson@6536
   343
\        ALL m. F : (A Int f-``{m}) leadsTo                     \
paulson@7524
   344
\                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
paulson@6536
   345
\     ==> F : (A Int f-``{m}) leadsTo B";
paulson@4776
   346
by (eres_inst_tac [("a","m")] wf_induct 1);
paulson@6536
   347
by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1);
paulson@4776
   348
by (stac vimage_eq_UN 2);
paulson@4776
   349
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
paulson@4776
   350
by (blast_tac (claset() addIs [leadsTo_UN]) 2);
paulson@4776
   351
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
paulson@4776
   352
val lemma = result();
paulson@4776
   353
paulson@4776
   354
paulson@4776
   355
(** Meta or object quantifier ????? **)
paulson@5239
   356
Goal "[| wf r;     \
paulson@6536
   357
\        ALL m. F : (A Int f-``{m}) leadsTo                     \
paulson@7524
   358
\                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
paulson@6536
   359
\     ==> F : A leadsTo B";
paulson@4776
   360
by (res_inst_tac [("t", "A")] subst 1);
paulson@4776
   361
by (rtac leadsTo_UN 2);
paulson@4776
   362
by (etac lemma 2);
paulson@4776
   363
by (REPEAT (assume_tac 2));
paulson@4776
   364
by (Fast_tac 1);    (*Blast_tac: Function unknown's argument not a parameter*)
paulson@4776
   365
qed "leadsTo_wf_induct";
paulson@4776
   366
paulson@4776
   367
paulson@5239
   368
Goal "[| wf r;     \
paulson@6536
   369
\        ALL m:I. F : (A Int f-``{m}) leadsTo                   \
paulson@7524
   370
\                     ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
paulson@6536
   371
\     ==> F : A leadsTo ((A - (f-``I)) Un B)";
paulson@4776
   372
by (etac leadsTo_wf_induct 1);
paulson@4776
   373
by Safe_tac;
paulson@4776
   374
by (case_tac "m:I" 1);
paulson@4776
   375
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
paulson@4776
   376
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
paulson@4776
   377
qed "bounded_induct";
paulson@4776
   378
paulson@4776
   379
paulson@6536
   380
(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
paulson@6536
   381
Goal "[| ALL m. F : (A Int f-``{m}) leadsTo                     \
paulson@7524
   382
\                   ((A Int f-``(lessThan m)) Un B) |] \
paulson@6536
   383
\     ==> F : A leadsTo B";
paulson@4776
   384
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
paulson@4776
   385
by (Asm_simp_tac 1);
paulson@4776
   386
qed "lessThan_induct";
paulson@4776
   387
paulson@7524
   388
Goal "[| ALL m:(greaterThan l).    \
paulson@7524
   389
\           F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
paulson@6536
   390
\     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
paulson@5648
   391
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
paulson@5648
   392
			       Compl_greaterThan RS sym]) 1);
paulson@4776
   393
by (rtac (wf_less_than RS bounded_induct) 1);
paulson@4776
   394
by (Asm_simp_tac 1);
paulson@4776
   395
qed "lessThan_bounded_induct";
paulson@4776
   396
paulson@7524
   397
Goal "[| ALL m:(lessThan l).    \
paulson@7524
   398
\           F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
paulson@6536
   399
\     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
paulson@4776
   400
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
paulson@4776
   401
    (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
paulson@4776
   402
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
paulson@4776
   403
by (Clarify_tac 1);
paulson@4776
   404
by (case_tac "m<l" 1);
paulson@4776
   405
by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2);
paulson@4776
   406
by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1);
paulson@4776
   407
qed "greaterThan_bounded_induct";
paulson@4776
   408
paulson@4776
   409
paulson@4776
   410
(*** wlt ****)
paulson@4776
   411
paulson@4776
   412
(*Misra's property W3*)
paulson@6536
   413
Goalw [wlt_def] "F : (wlt F B) leadsTo B";
paulson@4776
   414
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
paulson@4776
   415
qed "wlt_leadsTo";
paulson@4776
   416
paulson@6536
   417
Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B";
paulson@4776
   418
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
paulson@4776
   419
qed "leadsTo_subset";
paulson@4776
   420
paulson@4776
   421
(*Misra's property W2*)
paulson@6536
   422
Goal "F : A leadsTo B = (A <= wlt F B)";
paulson@4776
   423
by (blast_tac (claset() addSIs [leadsTo_subset, 
paulson@4776
   424
				wlt_leadsTo RS leadsTo_weaken_L]) 1);
paulson@4776
   425
qed "leadsTo_eq_subset_wlt";
paulson@4776
   426
paulson@4776
   427
(*Misra's property W4*)
paulson@5648
   428
Goal "B <= wlt F B";
paulson@4776
   429
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
paulson@4776
   430
				      subset_imp_leadsTo]) 1);
paulson@4776
   431
qed "wlt_increasing";
paulson@4776
   432
paulson@4776
   433
paulson@4776
   434
(*Used in the Trans case below*)
wenzelm@5069
   435
Goalw [constrains_def]
paulson@5111
   436
   "[| B <= A2;  \
paulson@6536
   437
\      F : (A1 - B) co (A1 Un B); \
paulson@6536
   438
\      F : (A2 - C) co (A2 Un C) |] \
paulson@6536
   439
\   ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
paulson@5669
   440
by (Clarify_tac 1);
paulson@5620
   441
by (Blast_tac 1);
paulson@4776
   442
val lemma1 = result();
paulson@4776
   443
paulson@4776
   444
paulson@4776
   445
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
paulson@6536
   446
Goal "F : A leadsTo A' ==> \
paulson@6536
   447
\     EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')";
paulson@4776
   448
by (etac leadsTo_induct 1);
paulson@4776
   449
(*Basis*)
paulson@4776
   450
by (blast_tac (claset() addIs [leadsTo_Basis]
paulson@4776
   451
                        addDs [ensuresD]) 1);
paulson@4776
   452
(*Trans*)
paulson@4776
   453
by (Clarify_tac 1);
paulson@4776
   454
by (res_inst_tac [("x", "Ba Un Bb")] exI 1);
paulson@4776
   455
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,
paulson@4776
   456
			       leadsTo_Un_duplicate]) 1);
paulson@4776
   457
(*Union*)
paulson@4776
   458
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1,
paulson@4776
   459
				  bchoice, ball_constrains_UN]) 1);;
paulson@4776
   460
by (res_inst_tac [("x", "UN A:S. f A")] exI 1);
paulson@4776
   461
by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
paulson@4776
   462
qed "leadsTo_123";
paulson@4776
   463
paulson@4776
   464
paulson@4776
   465
(*Misra's property W5*)
paulson@6536
   466
Goal "F : (wlt F B - B) co (wlt F B)";
paulson@5648
   467
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
paulson@4776
   468
by (Clarify_tac 1);
paulson@5648
   469
by (subgoal_tac "Ba = wlt F B" 1);
paulson@5648
   470
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2);
paulson@4776
   471
by (Clarify_tac 1);
paulson@4776
   472
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
paulson@4776
   473
qed "wlt_constrains_wlt";
paulson@4776
   474
paulson@4776
   475
paulson@4776
   476
(*** Completion: Binary and General Finite versions ***)
paulson@4776
   477
paulson@6536
   478
Goal "[| F : A leadsTo A';  F : stable A';   \
paulson@6536
   479
\        F : B leadsTo B';  F : stable B' |] \
paulson@6536
   480
\   ==> F : (A Int B) leadsTo (A' Int B')";
paulson@5648
   481
by (subgoal_tac "F : stable (wlt F B')" 1);
paulson@4776
   482
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
paulson@4776
   483
by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
paulson@5648
   484
	   rtac wlt_constrains_wlt 2,
paulson@4776
   485
	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
paulson@4776
   486
	   Blast_tac 2]);
paulson@6536
   487
by (subgoal_tac "F : (A Int wlt F B') leadsTo (A' Int wlt F B')" 1);
paulson@5277
   488
by (blast_tac (claset() addIs [psp_stable]) 2);
paulson@6536
   489
by (subgoal_tac "F : (A' Int wlt F B') leadsTo (A' Int B')" 1);
paulson@5277
   490
by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
paulson@6536
   491
by (subgoal_tac "F : (A Int B) leadsTo (A Int wlt F B')" 1);
paulson@4776
   492
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
paulson@4776
   493
			       subset_imp_leadsTo]) 2);
paulson@5479
   494
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
paulson@4776
   495
qed "stable_completion";
paulson@4776
   496
paulson@4776
   497
paulson@6536
   498
Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i)) -->  \
paulson@5648
   499
\                  (ALL i:I. F : stable (A' i)) -->         \
paulson@6536
   500
\                  F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
paulson@4776
   501
by (etac finite_induct 1);
paulson@4776
   502
by (Asm_simp_tac 1);
paulson@4776
   503
by (asm_simp_tac 
paulson@4776
   504
    (simpset() addsimps [stable_completion, stable_def, 
paulson@4776
   505
			 ball_constrains_INT]) 1);
paulson@4776
   506
qed_spec_mp "finite_stable_completion";
paulson@4776
   507
paulson@4776
   508
paulson@5648
   509
Goal "[| W = wlt F (B' Un C);     \
paulson@6536
   510
\      F : A leadsTo (A' Un C);  F : A' co (A' Un C);   \
paulson@6536
   511
\      F : B leadsTo (B' Un C);  F : B' co (B' Un C) |] \
paulson@6536
   512
\   ==> F : (A Int B) leadsTo ((A' Int B') Un C)";
paulson@6536
   513
by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
paulson@4776
   514
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
paulson@4776
   515
			       MRS constrains_Un RS constrains_weaken]) 2);
paulson@6536
   516
by (subgoal_tac "F : (W-C) co W" 1);
paulson@4776
   517
by (asm_full_simp_tac 
paulson@4776
   518
    (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
paulson@6536
   519
by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
paulson@4776
   520
by (simp_tac (simpset() addsimps [Int_Diff]) 2);
paulson@6714
   521
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2);
paulson@5456
   522
(** LEVEL 7 **)
paulson@6536
   523
by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
paulson@6714
   524
by (rtac leadsTo_Un_duplicate2 2);
paulson@6714
   525
by (blast_tac (claset() addIs [leadsTo_Un_Un, 
paulson@6714
   526
                               wlt_leadsTo RS psp2 RS leadsTo_weaken, 
paulson@6714
   527
                               subset_refl RS subset_imp_leadsTo]) 2);
paulson@4776
   528
by (dtac leadsTo_Diff 1);
paulson@4776
   529
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
paulson@4776
   530
by (subgoal_tac "A Int B <= A Int W" 1);
paulson@5456
   531
by (blast_tac (claset() addSDs [leadsTo_subset]
paulson@5456
   532
			addSIs [subset_refl RS Int_mono]) 2);
paulson@4776
   533
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
paulson@4776
   534
bind_thm("completion", refl RS result());
paulson@4776
   535
paulson@4776
   536
paulson@6536
   537
Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->  \
paulson@6536
   538
\                  (ALL i:I. F : (A' i) co (A' i Un C)) --> \
paulson@6536
   539
\                  F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
paulson@4776
   540
by (etac finite_induct 1);
paulson@4776
   541
by (ALLGOALS Asm_simp_tac);
paulson@4776
   542
by (Clarify_tac 1);
paulson@4776
   543
by (dtac ball_constrains_INT 1);
paulson@4776
   544
by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
paulson@6564
   545
qed_spec_mp "finite_completion";
paulson@4776
   546