new destruction rules
authorpaulson
Thu Aug 26 11:37:43 1999 +0200 (1999-08-26)
changeset 7363eddb3d77a363
parent 7362 f08fade5ea0d
child 7364 a979e8a2ee18
new destruction rules
src/HOL/UNITY/Follows.ML
     1.1 --- a/src/HOL/UNITY/Follows.ML	Thu Aug 26 11:37:22 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Follows.ML	Thu Aug 26 11:37:43 1999 +0200
     1.3 @@ -12,10 +12,9 @@
     1.4  by (blast_tac (claset() addIs [monoD]) 1);
     1.5  qed "mono_Always_o";
     1.6  
     1.7 -Goalw [Follows_def]
     1.8 -    "mono (h::'a::order => 'b::order) \
     1.9 -\    ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
    1.10 -\        (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
    1.11 +Goal "mono (h::'a::order => 'b::order) \
    1.12 +\     ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
    1.13 +\         (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
    1.14  by Auto_tac;
    1.15  by (rtac single_LeadsTo_I 1);
    1.16  by (dres_inst_tac [("x", "g s")] spec 1);
    1.17 @@ -38,6 +37,29 @@
    1.18  qed "Follows_trans";
    1.19  
    1.20  
    1.21 +(** Destructiom rules **)
    1.22 +
    1.23 +Goalw [Follows_def]
    1.24 +     "F : f Fols g ==> F : Increasing f";
    1.25 +by (Blast_tac 1);
    1.26 +qed "Follows_Increasing1";
    1.27 +
    1.28 +Goalw [Follows_def]
    1.29 +     "F : f Fols g ==> F : Increasing g";
    1.30 +by (Blast_tac 1);
    1.31 +qed "Follows_Increasing2";
    1.32 +
    1.33 +Goalw [Follows_def]
    1.34 +     "F : f Fols g ==> F : Always {s. f s <= g s}";
    1.35 +by (Blast_tac 1);
    1.36 +qed "Follows_Bounded";
    1.37 +
    1.38 +Goalw [Follows_def]
    1.39 +     "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}";
    1.40 +by (Blast_tac 1);
    1.41 +qed "Follows_LeadsTo";
    1.42 +
    1.43 +
    1.44  (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
    1.45  
    1.46  Goalw [increasing_def, stable_def, constrains_def]