src/HOL/UNITY/Follows.ML
author wenzelm
Wed Oct 18 23:42:18 2000 +0200 (2000-10-18)
changeset 10265 4e004b548049
parent 9104 89ca2a172f84
child 11786 51ce34ef5113
permissions -rw-r--r--
use Multiset from HOL/Library;
paulson@6706
     1
(*  Title:      HOL/UNITY/Follows
paulson@6706
     2
    ID:         $Id$
paulson@6706
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6706
     4
    Copyright   1998  University of Cambridge
paulson@6706
     5
paulson@6706
     6
The Follows relation of Charpentier and Sivilotte
paulson@6706
     7
*)
paulson@6706
     8
paulson@6706
     9
(*Does this hold for "invariant"?*)
paulson@6706
    10
Goal "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}";
paulson@6706
    11
by (asm_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
paulson@6706
    12
by (blast_tac (claset() addIs [monoD]) 1);
paulson@6706
    13
qed "mono_Always_o";
paulson@6706
    14
paulson@7363
    15
Goal "mono (h::'a::order => 'b::order) \
paulson@7363
    16
\     ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
paulson@7363
    17
\         (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
paulson@6706
    18
by Auto_tac;
paulson@6706
    19
by (rtac single_LeadsTo_I 1);
paulson@6706
    20
by (dres_inst_tac [("x", "g s")] spec 1);
paulson@6706
    21
by (etac LeadsTo_weaken 1);
paulson@6706
    22
by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
paulson@6706
    23
qed "mono_LeadsTo_o";
paulson@6706
    24
paulson@9019
    25
Goalw [Follows_def] "F : (%s. c) Fols (%s. c)";
paulson@9019
    26
by Auto_tac; 
paulson@9019
    27
qed "Follows_constant";
paulson@9019
    28
AddIffs [Follows_constant];
paulson@9019
    29
paulson@6809
    30
Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
paulson@6706
    31
by (Clarify_tac 1);
paulson@6706
    32
by (asm_full_simp_tac
paulson@6706
    33
    (simpset() addsimps [impOfSubs mono_Increasing_o,
paulson@6706
    34
			 impOfSubs mono_Always_o,
paulson@6706
    35
			 impOfSubs mono_LeadsTo_o RS INT_D]) 1);
paulson@6706
    36
qed "mono_Follows_o";
paulson@6706
    37
paulson@7542
    38
Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";
paulson@7542
    39
by (dtac mono_Follows_o 1);
paulson@7542
    40
by (force_tac (claset(), simpset() addsimps [o_def]) 1);
paulson@7542
    41
qed "mono_Follows_apply";
paulson@7542
    42
paulson@6706
    43
Goalw [Follows_def]
paulson@6809
    44
     "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h";
paulson@6706
    45
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
paulson@6706
    46
by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
paulson@6706
    47
qed "Follows_trans";
paulson@6706
    48
paulson@6706
    49
paulson@7363
    50
(** Destructiom rules **)
paulson@7363
    51
paulson@7363
    52
Goalw [Follows_def]
paulson@7363
    53
     "F : f Fols g ==> F : Increasing f";
paulson@7363
    54
by (Blast_tac 1);
paulson@7363
    55
qed "Follows_Increasing1";
paulson@7363
    56
paulson@7363
    57
Goalw [Follows_def]
paulson@7363
    58
     "F : f Fols g ==> F : Increasing g";
paulson@7363
    59
by (Blast_tac 1);
paulson@7363
    60
qed "Follows_Increasing2";
paulson@7363
    61
paulson@7363
    62
Goalw [Follows_def]
paulson@7363
    63
     "F : f Fols g ==> F : Always {s. f s <= g s}";
paulson@7363
    64
by (Blast_tac 1);
paulson@7363
    65
qed "Follows_Bounded";
paulson@7363
    66
paulson@7363
    67
Goalw [Follows_def]
paulson@7363
    68
     "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}";
paulson@7363
    69
by (Blast_tac 1);
paulson@7363
    70
qed "Follows_LeadsTo";
paulson@7363
    71
paulson@8128
    72
Goal "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}";
paulson@8128
    73
by (rtac single_LeadsTo_I 1);
paulson@8128
    74
by (Clarify_tac 1);
paulson@8128
    75
by (dtac Follows_LeadsTo 1);
paulson@8128
    76
by (etac LeadsTo_weaken 1);
paulson@8128
    77
by (blast_tac set_cs 1);
paulson@8128
    78
by (blast_tac (claset() addIs [pfixLe_trans, prefix_imp_pfixLe]) 1);
paulson@8128
    79
qed "Follows_LeadsTo_pfixLe";
paulson@8128
    80
paulson@8128
    81
Goal "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}";
paulson@8128
    82
by (rtac single_LeadsTo_I 1);
paulson@8128
    83
by (Clarify_tac 1);
paulson@8128
    84
by (dtac Follows_LeadsTo 1);
paulson@8128
    85
by (etac LeadsTo_weaken 1);
paulson@8128
    86
by (blast_tac set_cs 1);
paulson@8128
    87
by (blast_tac (claset() addIs [pfixGe_trans, prefix_imp_pfixGe]) 1);
paulson@8128
    88
qed "Follows_LeadsTo_pfixGe";
paulson@8128
    89
paulson@7363
    90
paulson@9019
    91
Goalw [Follows_def, Increasing_def, Stable_def]
paulson@9019
    92
     "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g"; 
paulson@9019
    93
by Auto_tac;
paulson@9019
    94
by (etac Always_LeadsTo_weaken 3);
paulson@9019
    95
by (eres_inst_tac [("A", "{s. z <= f s}"), ("A'", "{s. z <= f s}")] 
paulson@9019
    96
                  Always_Constrains_weaken 1);
paulson@9019
    97
by Auto_tac;
paulson@9019
    98
by (dtac Always_Int_I 1);
paulson@9019
    99
by (assume_tac 1);
paulson@9019
   100
by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
paulson@9104
   101
qed "Always_Follows1";
paulson@9104
   102
paulson@9104
   103
Goalw [Follows_def, Increasing_def, Stable_def]
paulson@9104
   104
     "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'"; 
paulson@9104
   105
by Auto_tac;
paulson@9104
   106
by (etac Always_LeadsTo_weaken 3);
paulson@9104
   107
by (eres_inst_tac [("A", "{s. z <= g s}"), ("A'", "{s. z <= g s}")] 
paulson@9104
   108
                  Always_Constrains_weaken 1);
paulson@9104
   109
by Auto_tac;
paulson@9104
   110
by (dtac Always_Int_I 1);
paulson@9104
   111
by (assume_tac 1);
paulson@9104
   112
by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
paulson@9104
   113
qed "Always_Follows2";
paulson@9019
   114
paulson@9019
   115
paulson@9019
   116
(** Union properties (with the subset ordering) **)
paulson@9019
   117
paulson@6706
   118
(*Can replace "Un" by any sup.  But existing max only works for linorders.*)
paulson@6706
   119
Goalw [increasing_def, stable_def, constrains_def]
paulson@6706
   120
    "[| F : increasing f;  F: increasing g |] \
paulson@6706
   121
\    ==> F : increasing (%s. (f s) Un (g s))";
paulson@6706
   122
by Auto_tac;
paulson@6706
   123
by (dres_inst_tac [("x","f xa")] spec 1);
paulson@6706
   124
by (dres_inst_tac [("x","g xa")] spec 1);
paulson@6706
   125
by (blast_tac (claset() addSDs [bspec]) 1);
paulson@6706
   126
qed "increasing_Un";
paulson@6706
   127
paulson@6706
   128
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
paulson@6706
   129
    "[| F : Increasing f;  F: Increasing g |] \
paulson@6706
   130
\    ==> F : Increasing (%s. (f s) Un (g s))";
paulson@6706
   131
by Auto_tac;
paulson@6706
   132
by (dres_inst_tac [("x","f xa")] spec 1);
paulson@6706
   133
by (dres_inst_tac [("x","g xa")] spec 1);
paulson@6706
   134
by (blast_tac (claset() addSDs [bspec]) 1);
paulson@6706
   135
qed "Increasing_Un";
paulson@6706
   136
paulson@6706
   137
paulson@6706
   138
Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
paulson@6706
   139
\     ==> F : Always {s. f' s Un g' s <= f s Un g s}";
paulson@6706
   140
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
paulson@6706
   141
by (Blast_tac 1);
paulson@6706
   142
qed "Always_Un";
paulson@6706
   143
paulson@6706
   144
(*Lemma to re-use the argument that one variable increases (progress)
paulson@6706
   145
  while the other variable doesn't decrease (safety)*)
paulson@6706
   146
Goal "[| F : Increasing f; F : Increasing g; \
paulson@6706
   147
\        F : Increasing g'; F : Always {s. f' s <= f s};\
paulson@6706
   148
\        ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
paulson@6706
   149
\     ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}";
paulson@6706
   150
by (rtac single_LeadsTo_I 1);
paulson@6706
   151
by (dres_inst_tac [("x", "f s")] IncreasingD 1);
paulson@6706
   152
by (dres_inst_tac [("x", "g s")] IncreasingD 1);
paulson@6706
   153
by (rtac LeadsTo_weaken 1);
paulson@6706
   154
by (rtac PSP_Stable 1);
paulson@6706
   155
by (eres_inst_tac [("x", "f s")] spec 1);
paulson@6706
   156
by (etac Stable_Int 1);
paulson@6706
   157
by (assume_tac 1);
paulson@6706
   158
by (Blast_tac 1);
paulson@6706
   159
by (Blast_tac 1);
paulson@6706
   160
qed "Follows_Un_lemma";
paulson@6706
   161
paulson@6706
   162
Goalw [Follows_def]
paulson@6809
   163
    "[| F : f' Fols f;  F: g' Fols g |] \
paulson@6809
   164
\    ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))";
paulson@6706
   165
by (asm_full_simp_tac (simpset() addsimps [Increasing_Un, Always_Un]) 1);
paulson@6706
   166
by Auto_tac;
paulson@6706
   167
by (rtac LeadsTo_Trans 1);
paulson@6706
   168
by (blast_tac (claset() addIs [Follows_Un_lemma]) 1);
paulson@6706
   169
(*Weakening is used to exchange Un's arguments*)
paulson@6706
   170
by (blast_tac (claset() addIs [Follows_Un_lemma RS LeadsTo_weaken]) 1);
paulson@6706
   171
qed "Follows_Un";
paulson@6706
   172
paulson@8314
   173
paulson@9019
   174
(** Multiset union properties (with the multiset ordering) **)
paulson@9019
   175
paulson@9019
   176
Goalw [increasing_def, stable_def, constrains_def]
paulson@9019
   177
    "[| F : increasing f;  F: increasing g |] \
paulson@9019
   178
\    ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))";
paulson@9019
   179
by Auto_tac;
paulson@9019
   180
by (dres_inst_tac [("x","f xa")] spec 1);
paulson@9019
   181
by (dres_inst_tac [("x","g xa")] spec 1);
paulson@9019
   182
by (ball_tac 1);
wenzelm@10265
   183
by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
paulson@9019
   184
qed "increasing_union";
paulson@9019
   185
paulson@9019
   186
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
paulson@9019
   187
    "[| F : Increasing f;  F: Increasing g |] \
paulson@9019
   188
\    ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))";
paulson@9019
   189
by Auto_tac;
paulson@9019
   190
by (dres_inst_tac [("x","f xa")] spec 1);
paulson@9019
   191
by (dres_inst_tac [("x","g xa")] spec 1);
paulson@9019
   192
by (ball_tac 1);
wenzelm@10265
   193
by (blast_tac (claset()  addIs [thm "union_le_mono", order_trans]) 1);
paulson@9019
   194
qed "Increasing_union";
paulson@9019
   195
paulson@9019
   196
Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
paulson@9019
   197
\     ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
paulson@9019
   198
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
wenzelm@10265
   199
by (blast_tac (claset()  addIs [thm "union_le_mono"]) 1);
paulson@9019
   200
qed "Always_union";
paulson@9019
   201
paulson@9019
   202
(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
paulson@9019
   203
Goal "[| F : Increasing f; F : Increasing g; \
paulson@9019
   204
\        F : Increasing g'; F : Always {s. f' s <= f s};\
paulson@9019
   205
\        ALL k::('a::order) multiset. \
paulson@9019
   206
\          F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
paulson@9019
   207
\     ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}";
paulson@9019
   208
by (rtac single_LeadsTo_I 1);
paulson@9019
   209
by (dres_inst_tac [("x", "f s")] IncreasingD 1);
paulson@9019
   210
by (dres_inst_tac [("x", "g s")] IncreasingD 1);
paulson@9019
   211
by (rtac LeadsTo_weaken 1);
paulson@9019
   212
by (rtac PSP_Stable 1);
paulson@9019
   213
by (eres_inst_tac [("x", "f s")] spec 1);
paulson@9019
   214
by (etac Stable_Int 1);
paulson@9019
   215
by (assume_tac 1);
paulson@9019
   216
by (Blast_tac 1);
wenzelm@10265
   217
by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
paulson@9019
   218
qed "Follows_union_lemma";
paulson@9019
   219
paulson@9019
   220
(*The !! is there to influence to effect of permutative rewriting at the end*)
paulson@9019
   221
Goalw [Follows_def]
paulson@9019
   222
     "!!g g' ::'b => ('a::order) multiset. \
paulson@9019
   223
\       [| F : f' Fols f;  F: g' Fols g |] \
paulson@9019
   224
\       ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))";
paulson@9019
   225
by (asm_full_simp_tac (simpset() addsimps [Increasing_union, Always_union]) 1);
paulson@9019
   226
by Auto_tac;
paulson@9019
   227
by (rtac LeadsTo_Trans 1);
paulson@9019
   228
by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
paulson@9019
   229
(*now exchange union's arguments*)
wenzelm@10265
   230
by (simp_tac (simpset() addsimps [thm "union_commute"]) 1); 
paulson@9019
   231
by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
paulson@9019
   232
qed "Follows_union";
paulson@9019
   233
paulson@9019
   234
Goal "!!f ::['c,'b] => ('a::order) multiset. \
paulson@9019
   235
\       [| ALL i: I. F : f' i Fols f i;  finite I |] \
paulson@9019
   236
\       ==> F : (%s. setsum (%i. f' i s) I) Fols (%s. setsum (%i. f i s) I)";
paulson@9019
   237
by (etac rev_mp 1); 
paulson@9019
   238
by (etac finite_induct 1);
paulson@9019
   239
by (asm_simp_tac (simpset() addsimps [Follows_union]) 2);
paulson@9019
   240
by (Simp_tac 1); 
paulson@9019
   241
qed "Follows_setsum";
paulson@9019
   242
paulson@9019
   243
paulson@8314
   244
(*Currently UNUSED, but possibly of interest*)
paulson@8314
   245
Goal "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}";
paulson@8314
   246
by (asm_full_simp_tac
paulson@8314
   247
    (simpset() addsimps [Increasing_def, Stable_def, Constrains_def, 
paulson@8314
   248
			 constrains_def]) 1); 
paulson@8314
   249
by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
paulson@8314
   250
			       prefix_imp_pfixGe]) 1);
paulson@8314
   251
qed "Increasing_imp_Stable_pfixGe";
paulson@8314
   252
paulson@8314
   253
(*Currently UNUSED, but possibly of interest*)
paulson@8314
   254
Goal "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s} \
paulson@8314
   255
\     ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}";
paulson@8314
   256
by (rtac single_LeadsTo_I 1);
paulson@8314
   257
by (dres_inst_tac [("x", "f s")] spec 1);
paulson@8314
   258
by (etac LeadsTo_weaken 1);
paulson@8314
   259
by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
paulson@8314
   260
			       prefix_imp_pfixGe]) 2);
paulson@8314
   261
by (Blast_tac 1);
paulson@8314
   262
qed "LeadsTo_le_imp_pfixGe";