equal
deleted
inserted
replaced
210 \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<and> LastActExtsch A sch" |
210 \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<and> LastActExtsch A sch" |
211 apply (unfold schedules_def has_schedule_def [abs_def]) |
211 apply (unfold schedules_def has_schedule_def [abs_def]) |
212 apply auto |
212 apply auto |
213 apply (rule_tac x = "filter_act $ (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI) |
213 apply (rule_tac x = "filter_act $ (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI) |
214 apply (simp add: executions_def) |
214 apply (simp add: executions_def) |
215 apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
215 apply (pair ex) |
216 apply auto |
216 apply auto |
217 apply (rule_tac x = "(x1, Cut (\<lambda>a. fst a \<in> ext A) x2)" in exI) |
217 apply (rule_tac x = "(x1, Cut (\<lambda>a. fst a \<in> ext A) x2)" in exI) |
218 apply simp |
218 apply simp |
219 |
219 |
220 text \<open>Subgoal 1: Lemma: propagation of execution through \<open>Cut\<close>\<close> |
220 text \<open>Subgoal 1: Lemma: propagation of execution through \<open>Cut\<close>\<close> |