equal
deleted
inserted
replaced
108 \ ==> F : Always {s. f' s Un g' s <= f s Un g s}"; |
108 \ ==> F : Always {s. f' s Un g' s <= f s Un g s}"; |
109 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); |
109 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); |
110 by (Blast_tac 1); |
110 by (Blast_tac 1); |
111 qed "Always_Un"; |
111 qed "Always_Un"; |
112 |
112 |
113 Goalw [Increasing_def] |
|
114 "F : Increasing f ==> F : Stable {s. x <= f s}"; |
|
115 by (Blast_tac 1); |
|
116 qed "IncreasingD"; |
|
117 |
|
118 (*Lemma to re-use the argument that one variable increases (progress) |
113 (*Lemma to re-use the argument that one variable increases (progress) |
119 while the other variable doesn't decrease (safety)*) |
114 while the other variable doesn't decrease (safety)*) |
120 Goal "[| F : Increasing f; F : Increasing g; \ |
115 Goal "[| F : Increasing f; F : Increasing g; \ |
121 \ F : Increasing g'; F : Always {s. f' s <= f s};\ |
116 \ F : Increasing g'; F : Always {s. f' s <= f s};\ |
122 \ ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\ |
117 \ ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\ |