6706

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 

7363

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)})";

6706

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 

6809

25 
Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";

6706

26 
by (Clarify_tac 1);


27 
by (asm_full_simp_tac


28 
(simpset() addsimps [impOfSubs mono_Increasing_o,


29 
impOfSubs mono_Always_o,


30 
impOfSubs mono_LeadsTo_o RS INT_D]) 1);


31 
qed "mono_Follows_o";


32 

7542

33 
Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";


34 
by (dtac mono_Follows_o 1);


35 
by (force_tac (claset(), simpset() addsimps [o_def]) 1);


36 
qed "mono_Follows_apply";


37 

6706

38 
Goalw [Follows_def]

6809

39 
"[ F : f Fols g; F: g Fols h ] ==> F : f Fols h";

6706

40 
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);


41 
by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);


42 
qed "Follows_trans";


43 


44 

7363

45 
(** Destructiom rules **)


46 


47 
Goalw [Follows_def]


48 
"F : f Fols g ==> F : Increasing f";


49 
by (Blast_tac 1);


50 
qed "Follows_Increasing1";


51 


52 
Goalw [Follows_def]


53 
"F : f Fols g ==> F : Increasing g";


54 
by (Blast_tac 1);


55 
qed "Follows_Increasing2";


56 


57 
Goalw [Follows_def]


58 
"F : f Fols g ==> F : Always {s. f s <= g s}";


59 
by (Blast_tac 1);


60 
qed "Follows_Bounded";


61 


62 
Goalw [Follows_def]


63 
"F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}";


64 
by (Blast_tac 1);


65 
qed "Follows_LeadsTo";


66 


67 

6706

68 
(*Can replace "Un" by any sup. But existing max only works for linorders.*)


69 


70 
Goalw [increasing_def, stable_def, constrains_def]


71 
"[ F : increasing f; F: increasing g ] \


72 
\ ==> F : increasing (%s. (f s) Un (g s))";


73 
by Auto_tac;


74 
by (dres_inst_tac [("x","f xa")] spec 1);


75 
by (dres_inst_tac [("x","g xa")] spec 1);


76 
by (blast_tac (claset() addSDs [bspec]) 1);


77 
qed "increasing_Un";


78 


79 
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]


80 
"[ F : Increasing f; F: Increasing g ] \


81 
\ ==> F : Increasing (%s. (f s) Un (g s))";


82 
by Auto_tac;


83 
by (dres_inst_tac [("x","f xa")] spec 1);


84 
by (dres_inst_tac [("x","g xa")] spec 1);


85 
by (blast_tac (claset() addSDs [bspec]) 1);


86 
qed "Increasing_Un";


87 


88 


89 
Goal "[ F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} ] \


90 
\ ==> F : Always {s. f' s Un g' s <= f s Un g s}";


91 
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);


92 
by (Blast_tac 1);


93 
qed "Always_Un";


94 


95 


96 


97 
Goalw [Increasing_def]


98 
"F : Increasing f ==> F : Stable {s. x <= f s}";


99 
by (Blast_tac 1);


100 
qed "IncreasingD";


101 


102 


103 
(*Lemma to reuse the argument that one variable increases (progress)


104 
while the other variable doesn't decrease (safety)*)


105 
Goal "[ F : Increasing f; F : Increasing g; \


106 
\ F : Increasing g'; F : Always {s. f' s <= f s};\


107 
\ ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} ]\


108 
\ ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}";


109 
by (rtac single_LeadsTo_I 1);


110 
by (dres_inst_tac [("x", "f s")] IncreasingD 1);


111 
by (dres_inst_tac [("x", "g s")] IncreasingD 1);


112 
by (rtac LeadsTo_weaken 1);


113 
by (rtac PSP_Stable 1);


114 
by (eres_inst_tac [("x", "f s")] spec 1);


115 
by (etac Stable_Int 1);


116 
by (assume_tac 1);


117 
by (Blast_tac 1);


118 
by (Blast_tac 1);


119 
qed "Follows_Un_lemma";


120 


121 
Goalw [Follows_def]

6809

122 
"[ F : f' Fols f; F: g' Fols g ] \


123 
\ ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))";

6706

124 
by (asm_full_simp_tac (simpset() addsimps [Increasing_Un, Always_Un]) 1);


125 
by Auto_tac;


126 
by (rtac LeadsTo_Trans 1);


127 
by (blast_tac (claset() addIs [Follows_Un_lemma]) 1);


128 
(*Weakening is used to exchange Un's arguments*)


129 
by (blast_tac (claset() addIs [Follows_Un_lemma RS LeadsTo_weaken]) 1);


130 
qed "Follows_Un";


131 
