equal
deleted
inserted
replaced
221 ==> ? sch. sch : schedules A & |
221 ==> ? sch. sch : schedules A & |
222 tr = Filter (%a. a:ext A)$sch & |
222 tr = Filter (%a. a:ext A)$sch & |
223 LastActExtsch A sch" |
223 LastActExtsch A sch" |
224 |
224 |
225 apply (unfold schedules_def has_schedule_def) |
225 apply (unfold schedules_def has_schedule_def) |
226 apply (tactic "safe_tac set_cs") |
226 apply auto |
227 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI) |
227 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI) |
228 apply (simp add: executions_def) |
228 apply (simp add: executions_def) |
229 apply (tactic {* pair_tac "ex" 1 *}) |
229 apply (tactic {* pair_tac "ex" 1 *}) |
230 apply (tactic "safe_tac set_cs") |
230 apply auto |
231 apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI) |
231 apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI) |
232 apply (simp (no_asm_simp)) |
232 apply (simp (no_asm_simp)) |
233 |
233 |
234 (* Subgoal 1: Lemma: propagation of execution through Cut *) |
234 (* Subgoal 1: Lemma: propagation of execution through Cut *) |
235 |
235 |