28 qed "common_Invariant"; |
28 qed "common_Invariant"; |
29 |
29 |
30 |
30 |
31 (*** Some programs that implement the safety property above ***) |
31 (*** Some programs that implement the safety property above ***) |
32 |
32 |
33 Goal "SKIP UNIV : constrains {m} (maxfg m)"; |
33 Goal "SKIP : constrains {m} (maxfg m)"; |
34 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, |
34 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, |
35 fasc]) 1); |
35 fasc]) 1); |
36 result(); |
36 result(); |
37 |
37 |
38 (*This one is t := ftime t || t := gtime t*) |
38 (*This one is t := ftime t || t := gtime t*) |
39 Goal "mk_program (UNIV, UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \ |
39 Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \ |
40 \ : constrains {m} (maxfg m)"; |
40 \ : constrains {m} (maxfg m)"; |
41 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, |
41 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, |
42 le_max_iff_disj, fasc]) 1); |
42 le_max_iff_disj, fasc]) 1); |
43 by (Blast_tac 1); |
43 by (Blast_tac 1); |
44 result(); |
44 result(); |
45 |
45 |
46 (*This one is t := max (ftime t) (gtime t)*) |
46 (*This one is t := max (ftime t) (gtime t)*) |
47 Goal "mk_program (UNIV, UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \ |
47 Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \ |
48 \ : constrains {m} (maxfg m)"; |
48 \ : constrains {m} (maxfg m)"; |
49 by (simp_tac |
49 by (simp_tac |
50 (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
50 (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
51 by (Blast_tac 1); |
51 by (Blast_tac 1); |
52 result(); |
52 result(); |
53 |
53 |
54 (*This one is t := t+1 if t <max (ftime t) (gtime t) *) |
54 (*This one is t := t+1 if t <max (ftime t) (gtime t) *) |
55 Goal "mk_program (UNIV, UNIV, \ |
55 Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \ |
56 \ { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \ |
|
57 \ : constrains {m} (maxfg m)"; |
56 \ : constrains {m} (maxfg m)"; |
58 by (simp_tac |
57 by (simp_tac |
59 (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
58 (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
60 by (blast_tac (claset() addIs [Suc_leI]) 1); |
59 by (blast_tac (claset() addIs [Suc_leI]) 1); |
61 result(); |
60 result(); |