Theory of the "Follows" relation
authorpaulson
Mon May 24 15:47:06 1999 +0200 (1999-05-24)
changeset 6706d8067e272d4f
parent 6705 b2662096ccd0
child 6707 3b07e62a718c
Theory of the "Follows" relation
src/HOL/UNITY/Follows.ML
src/HOL/UNITY/Follows.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Follows.ML	Mon May 24 15:47:06 1999 +0200
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Title:      HOL/UNITY/Follows
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +The Follows relation of Charpentier and Sivilotte
    1.10 +*)
    1.11 +
    1.12 +(*Does this hold for "invariant"?*)
    1.13 +Goal "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}";
    1.14 +by (asm_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.15 +by (blast_tac (claset() addIs [monoD]) 1);
    1.16 +qed "mono_Always_o";
    1.17 +
    1.18 +Goalw [Follows_def]
    1.19 +    "mono (h::'a::order => 'b::order) \
    1.20 +\    ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
    1.21 +\        (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
    1.22 +by Auto_tac;
    1.23 +by (rtac single_LeadsTo_I 1);
    1.24 +by (dres_inst_tac [("x", "g s")] spec 1);
    1.25 +by (etac LeadsTo_weaken 1);
    1.26 +by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
    1.27 +qed "mono_LeadsTo_o";
    1.28 +
    1.29 +Goalw [Follows_def] "mono h ==> f Follows g <= (h o f) Follows (h o g)";
    1.30 +by (Clarify_tac 1);
    1.31 +by (asm_full_simp_tac
    1.32 +    (simpset() addsimps [impOfSubs mono_Increasing_o,
    1.33 +			 impOfSubs mono_Always_o,
    1.34 +			 impOfSubs mono_LeadsTo_o RS INT_D]) 1);
    1.35 +qed "mono_Follows_o";
    1.36 +
    1.37 +Goalw [Follows_def]
    1.38 +     "[| F : f Follows g;  F: g Follows h |] ==> F : f Follows h";
    1.39 +by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.40 +by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
    1.41 +qed "Follows_trans";
    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]
    1.47 +    "[| F : increasing f;  F: increasing g |] \
    1.48 +\    ==> F : increasing (%s. (f s) Un (g s))";
    1.49 +by Auto_tac;
    1.50 +by (dres_inst_tac [("x","f xa")] spec 1);
    1.51 +by (dres_inst_tac [("x","g xa")] spec 1);
    1.52 +by (blast_tac (claset() addSDs [bspec]) 1);
    1.53 +qed "increasing_Un";
    1.54 +
    1.55 +Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
    1.56 +    "[| F : Increasing f;  F: Increasing g |] \
    1.57 +\    ==> F : Increasing (%s. (f s) Un (g s))";
    1.58 +by Auto_tac;
    1.59 +by (dres_inst_tac [("x","f xa")] spec 1);
    1.60 +by (dres_inst_tac [("x","g xa")] spec 1);
    1.61 +by (blast_tac (claset() addSDs [bspec]) 1);
    1.62 +qed "Increasing_Un";
    1.63 +
    1.64 +
    1.65 +Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
    1.66 +\     ==> F : Always {s. f' s Un g' s <= f s Un g s}";
    1.67 +by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.68 +by (Blast_tac 1);
    1.69 +qed "Always_Un";
    1.70 +
    1.71 +
    1.72 +
    1.73 +Goalw [Increasing_def]
    1.74 +     "F : Increasing f ==> F : Stable {s. x <= f s}";
    1.75 +by (Blast_tac 1);
    1.76 +qed "IncreasingD";
    1.77 +
    1.78 +
    1.79 +(*Lemma to re-use the argument that one variable increases (progress)
    1.80 +  while the other variable doesn't decrease (safety)*)
    1.81 +Goal "[| F : Increasing f; F : Increasing g; \
    1.82 +\        F : Increasing g'; F : Always {s. f' s <= f s};\
    1.83 +\        ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
    1.84 +\     ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}";
    1.85 +by (rtac single_LeadsTo_I 1);
    1.86 +by (dres_inst_tac [("x", "f s")] IncreasingD 1);
    1.87 +by (dres_inst_tac [("x", "g s")] IncreasingD 1);
    1.88 +by (rtac LeadsTo_weaken 1);
    1.89 +by (rtac PSP_Stable 1);
    1.90 +by (eres_inst_tac [("x", "f s")] spec 1);
    1.91 +by (etac Stable_Int 1);
    1.92 +by (assume_tac 1);
    1.93 +by (Blast_tac 1);
    1.94 +by (Blast_tac 1);
    1.95 +qed "Follows_Un_lemma";
    1.96 +
    1.97 +Goalw [Follows_def]
    1.98 +    "[| F : f' Follows f;  F: g' Follows g |] \
    1.99 +\    ==> F : (%s. (f' s) Un (g' s)) Follows (%s. (f s) Un (g s))";
   1.100 +by (asm_full_simp_tac (simpset() addsimps [Increasing_Un, Always_Un]) 1);
   1.101 +by Auto_tac;
   1.102 +by (rtac LeadsTo_Trans 1);
   1.103 +by (blast_tac (claset() addIs [Follows_Un_lemma]) 1);
   1.104 +(*Weakening is used to exchange Un's arguments*)
   1.105 +by (blast_tac (claset() addIs [Follows_Un_lemma RS LeadsTo_weaken]) 1);
   1.106 +qed "Follows_Un";
   1.107 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Follows.thy	Mon May 24 15:47:06 1999 +0200
     2.3 @@ -0,0 +1,20 @@
     2.4 +(*  Title:      HOL/UNITY/Follows
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +
     2.9 +The Follows relation of Charpentier and Sivilotte
    2.10 +*)
    2.11 +
    2.12 +Follows = Union +
    2.13 +
    2.14 +constdefs
    2.15 +
    2.16 +  Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
    2.17 +                 (infixl 65)
    2.18 +   "f Follows g == Increasing g Int Increasing f Int
    2.19 +                   Always {s. f s <= g s} Int
    2.20 +                   (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
    2.21 +
    2.22 +
    2.23 +end