equal
deleted
inserted
replaced
432 Goalw [constrains_def] |
432 Goalw [constrains_def] |
433 "[| B <= A2; \ |
433 "[| B <= A2; \ |
434 \ constrains acts (A1 - B) (A1 Un B); \ |
434 \ constrains acts (A1 - B) (A1 Un B); \ |
435 \ constrains acts (A2 - C) (A2 Un C) |] \ |
435 \ constrains acts (A2 - C) (A2 Un C) |] \ |
436 \ ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)"; |
436 \ ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)"; |
437 by(Blast_tac 1); |
437 by (Blast_tac 1); |
438 val lemma1 = result(); |
438 val lemma1 = result(); |
439 |
439 |
440 |
440 |
441 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
441 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
442 Goal "[| leadsTo acts A A'; Id: acts |] ==> \ |
442 Goal "[| leadsTo acts A A'; Id: acts |] ==> \ |