1(* Title: HOL/HOLCF/IOA/ShortExecutions.thy 2 Author: Olaf M��ller 3*) 4 5theory ShortExecutions 6imports Traces 7begin 8 9text \<open> 10 Some properties about \<open>Cut ex\<close>, defined as follows: 11 12 For every execution ex there is another shorter execution \<open>Cut ex\<close> 13 that has the same trace as ex, but its schedule ends with an external action. 14\<close> 15 16definition oraclebuild :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq" 17 where "oraclebuild P = 18 (fix \<cdot> 19 (LAM h s t. 20 case t of 21 nil \<Rightarrow> nil 22 | x ## xs \<Rightarrow> 23 (case x of 24 UU \<Rightarrow> UU 25 | Def y \<Rightarrow> 26 (Takewhile (\<lambda>x. \<not> P x) \<cdot> s) @@ 27 (y \<leadsto> (h \<cdot> (TL \<cdot> (Dropwhile (\<lambda>x. \<not> P x) \<cdot> s)) \<cdot> xs)))))" 28 29definition Cut :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> 'a Seq" 30 where "Cut P s = oraclebuild P \<cdot> s \<cdot> (Filter P \<cdot> s)" 31 32definition LastActExtsch :: "('a,'s) ioa \<Rightarrow> 'a Seq \<Rightarrow> bool" 33 where "LastActExtsch A sch \<longleftrightarrow> Cut (\<lambda>x. x \<in> ext A) sch = sch" 34 35axiomatization where 36 Cut_prefixcl_Finite: "Finite s \<Longrightarrow> \<exists>y. s = Cut P s @@ y" 37 38axiomatization where 39 LastActExtsmall1: "LastActExtsch A sch \<Longrightarrow> LastActExtsch A (TL \<cdot> (Dropwhile P \<cdot> sch))" 40 41axiomatization where 42 LastActExtsmall2: "Finite sch1 \<Longrightarrow> LastActExtsch A (sch1 @@ sch2) \<Longrightarrow> LastActExtsch A sch2" 43 44ML \<open> 45fun thin_tac' ctxt j = 46 rotate_tac (j - 1) THEN' 47 eresolve_tac ctxt [thin_rl] THEN' 48 rotate_tac (~ (j - 1)) 49\<close> 50 51 52subsection \<open>\<open>oraclebuild\<close> rewrite rules\<close> 53 54lemma oraclebuild_unfold: 55 "oraclebuild P = 56 (LAM s t. 57 case t of 58 nil \<Rightarrow> nil 59 | x ## xs \<Rightarrow> 60 (case x of 61 UU \<Rightarrow> UU 62 | Def y \<Rightarrow> 63 (Takewhile (\<lambda>a. \<not> P a) \<cdot> s) @@ 64 (y \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> xs))))" 65 apply (rule trans) 66 apply (rule fix_eq2) 67 apply (simp only: oraclebuild_def) 68 apply (rule beta_cfun) 69 apply simp 70 done 71 72lemma oraclebuild_UU: "oraclebuild P \<cdot> sch \<cdot> UU = UU" 73 apply (subst oraclebuild_unfold) 74 apply simp 75 done 76 77lemma oraclebuild_nil: "oraclebuild P \<cdot> sch \<cdot> nil = nil" 78 apply (subst oraclebuild_unfold) 79 apply simp 80 done 81 82lemma oraclebuild_cons: 83 "oraclebuild P \<cdot> s \<cdot> (x \<leadsto> t) = 84 (Takewhile (\<lambda>a. \<not> P a) \<cdot> s) @@ 85 (x \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> t))" 86 apply (rule trans) 87 apply (subst oraclebuild_unfold) 88 apply (simp add: Consq_def) 89 apply (simp add: Consq_def) 90 done 91 92 93subsection \<open>Cut rewrite rules\<close> 94 95lemma Cut_nil: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> Finite s \<Longrightarrow> Cut P s = nil" 96 apply (unfold Cut_def) 97 apply (subgoal_tac "Filter P \<cdot> s = nil") 98 apply (simp add: oraclebuild_nil) 99 apply (rule ForallQFilterPnil) 100 apply assumption+ 101 done 102 103lemma Cut_UU: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> \<not> Finite s \<Longrightarrow> Cut P s = UU" 104 apply (unfold Cut_def) 105 apply (subgoal_tac "Filter P \<cdot> s = UU") 106 apply (simp add: oraclebuild_UU) 107 apply (rule ForallQFilterPUU) 108 apply assumption+ 109 done 110 111lemma Cut_Cons: 112 "P t \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ss \<Longrightarrow> Finite ss \<Longrightarrow> 113 Cut P (ss @@ (t \<leadsto> rs)) = ss @@ (t \<leadsto> Cut P rs)" 114 apply (unfold Cut_def) 115 apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc) 116 done 117 118 119subsection \<open>Cut lemmas for main theorem\<close> 120 121lemma FilterCut: "Filter P \<cdot> s = Filter P \<cdot> (Cut P s)" 122 apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp]) 123 prefer 3 124 apply fast 125 apply (case_tac "Finite s") 126 apply (simp add: Cut_nil ForallQFilterPnil) 127 apply (simp add: Cut_UU ForallQFilterPUU) 128 text \<open>main case\<close> 129 apply (simp add: Cut_Cons ForallQFilterPnil) 130 done 131 132lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)" 133 apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P x" and x1 = "s" in 134 take_lemma_less_induct [THEN mp]) 135 prefer 3 136 apply fast 137 apply (case_tac "Finite s") 138 apply (simp add: Cut_nil ForallQFilterPnil) 139 apply (simp add: Cut_UU ForallQFilterPUU) 140 text \<open>main case\<close> 141 apply (simp add: Cut_Cons ForallQFilterPnil) 142 apply (rule take_reduction) 143 apply auto 144 done 145 146lemma MapCut: "Map f\<cdot>(Cut (P \<circ> f) s) = Cut P (Map f\<cdot>s)" 147 apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P (f x) " and x1 = "s" in 148 take_lemma_less_induct [THEN mp]) 149 prefer 3 150 apply fast 151 apply (case_tac "Finite s") 152 apply (simp add: Cut_nil) 153 apply (rule Cut_nil [symmetric]) 154 apply (simp add: ForallMap o_def) 155 apply (simp add: Map2Finite) 156 text \<open>case \<open>\<not> Finite s\<close>\<close> 157 apply (simp add: Cut_UU) 158 apply (rule Cut_UU) 159 apply (simp add: ForallMap o_def) 160 apply (simp add: Map2Finite) 161 text \<open>main case\<close> 162 apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def) 163 apply (rule take_reduction) 164 apply auto 165 done 166 167lemma Cut_prefixcl_nFinite [rule_format]: "\<not> Finite s \<longrightarrow> Cut P s \<sqsubseteq> s" 168 apply (intro strip) 169 apply (rule take_lemma_less [THEN iffD1]) 170 apply (intro strip) 171 apply (rule mp) 172 prefer 2 173 apply assumption 174 apply (tactic "thin_tac' \<^context> 1 1") 175 apply (rule_tac x = "s" in spec) 176 apply (rule nat_less_induct) 177 apply (intro strip) 178 apply (rename_tac na n s) 179 apply (case_tac "Forall (\<lambda>x. \<not> P x) s") 180 apply (rule take_lemma_less [THEN iffD2, THEN spec]) 181 apply (simp add: Cut_UU) 182 text \<open>main case\<close> 183 apply (drule divide_Seq3) 184 apply (erule exE)+ 185 apply (erule conjE)+ 186 apply hypsubst 187 apply (simp add: Cut_Cons) 188 apply (rule take_reduction_less) 189 text \<open>auto makes also reasoning about Finiteness of parts of \<open>s\<close>!\<close> 190 apply auto 191 done 192 193lemma execThruCut: "is_exec_frag A (s, ex) \<Longrightarrow> is_exec_frag A (s, Cut P ex)" 194 apply (case_tac "Finite ex") 195 apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite) 196 apply assumption 197 apply (erule exE) 198 apply (rule exec_prefix2closed) 199 apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst) 200 apply assumption 201 apply (erule exec_prefixclosed) 202 apply (erule Cut_prefixcl_nFinite) 203 done 204 205 206subsection \<open>Main Cut Theorem\<close> 207 208lemma exists_LastActExtsch: 209 "sch \<in> schedules A \<Longrightarrow> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> sch \<Longrightarrow> 210 \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> sch \<and> LastActExtsch A sch" 211 apply (unfold schedules_def has_schedule_def [abs_def]) 212 apply auto 213 apply (rule_tac x = "filter_act \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI) 214 apply (simp add: executions_def) 215 apply (pair ex) 216 apply auto 217 apply (rule_tac x = "(x1, Cut (\<lambda>a. fst a \<in> ext A) x2)" in exI) 218 apply simp 219 220 text \<open>Subgoal 1: Lemma: propagation of execution through \<open>Cut\<close>\<close> 221 apply (simp add: execThruCut) 222 223 text \<open>Subgoal 2: Lemma: \<open>Filter P s = Filter P (Cut P s)\<close>\<close> 224 apply (simp add: filter_act_def) 225 apply (subgoal_tac "Map fst \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst \<cdot> x2)") 226 apply (rule_tac [2] MapCut [unfolded o_def]) 227 apply (simp add: FilterCut [symmetric]) 228 229 text \<open>Subgoal 3: Lemma: \<open>Cut\<close> idempotent\<close> 230 apply (simp add: LastActExtsch_def filter_act_def) 231 apply (subgoal_tac "Map fst \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst \<cdot> x2)") 232 apply (rule_tac [2] MapCut [unfolded o_def]) 233 apply (simp add: Cut_idemp) 234 done 235 236 237subsection \<open>Further Cut lemmas\<close> 238 239lemma LastActExtimplnil: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) \<cdot> sch = nil \<Longrightarrow> sch = nil" 240 apply (unfold LastActExtsch_def) 241 apply (drule FilternPnilForallP) 242 apply (erule conjE) 243 apply (drule Cut_nil) 244 apply assumption 245 apply simp 246 done 247 248lemma LastActExtimplUU: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) \<cdot> sch = UU \<Longrightarrow> sch = UU" 249 apply (unfold LastActExtsch_def) 250 apply (drule FilternPUUForallP) 251 apply (erule conjE) 252 apply (drule Cut_UU) 253 apply assumption 254 apply simp 255 done 256 257end 258