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