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