equal
deleted
inserted
replaced
17 Goalw [transient_def] |
17 Goalw [transient_def] |
18 "F:transient(A) ==> F:program & st_set(A)"; |
18 "F:transient(A) ==> F:program & st_set(A)"; |
19 by Auto_tac; |
19 by Auto_tac; |
20 qed "transientD2"; |
20 qed "transientD2"; |
21 |
21 |
22 Goalw [stable_def, constrains_def, transient_def] |
22 Goal "[| F : stable(A); F : transient(A) |] ==> A = 0"; |
23 "[| F : stable(A); F : transient(A) |] ==> A = 0"; |
23 by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, transient_def]) 1); |
24 by (Asm_full_simp_tac 1); |
24 by (Fast_tac 1); |
25 by (Blast.depth_tac (claset()) 10 1); |
|
26 qed "stable_transient_empty"; |
25 qed "stable_transient_empty"; |
27 |
26 |
28 Goalw [transient_def, st_set_def] |
27 Goalw [transient_def, st_set_def] "[|F:transient(A); B<=A|] ==> F:transient(B)"; |
29 "[|F:transient(A); B<=A|] ==> F:transient(B)"; |
|
30 by Safe_tac; |
28 by Safe_tac; |
31 by (res_inst_tac [("x", "act")] bexI 1); |
29 by (res_inst_tac [("x", "act")] bexI 1); |
32 by (ALLGOALS(Asm_full_simp_tac)); |
30 by (ALLGOALS(Asm_full_simp_tac)); |
33 by (Blast_tac 1); |
31 by (Blast_tac 1); |
34 by Auto_tac; |
32 by Auto_tac; |
607 Goalw [constrains_def, st_set_def] |
605 Goalw [constrains_def, st_set_def] |
608 "[| B <= A2; \ |
606 "[| B <= A2; \ |
609 \ F : (A1 - B) co (A1 Un B); \ |
607 \ F : (A1 - B) co (A1 Un B); \ |
610 \ F : (A2 - C) co (A2 Un C) |] \ |
608 \ F : (A2 - C) co (A2 Un C) |] \ |
611 \ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"; |
609 \ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"; |
612 by (Clarify_tac 1); |
|
613 by (Blast_tac 1); |
610 by (Blast_tac 1); |
614 qed "leadsTo_123_aux"; |
611 qed "leadsTo_123_aux"; |
615 |
612 |
616 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
613 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
617 (* slightly different from the HOL one: B here is bounded *) |
614 (* slightly different from the HOL one: B here is bounded *) |