equal
deleted
inserted
replaced
11 Spriner LNCS 1586 (1999), pages 1215-1227. |
11 Spriner LNCS 1586 (1999), pages 1215-1227. |
12 *) |
12 *) |
13 |
13 |
14 Addsimps [Component_def RS def_prg_Init, |
14 Addsimps [Component_def RS def_prg_Init, |
15 Component_def RS def_prg_AllowedActs]; |
15 Component_def RS def_prg_AllowedActs]; |
16 program_defs_ref := [Component_def]; |
|
17 Addsimps (map simp_of_act [a_def]); |
16 Addsimps (map simp_of_act [a_def]); |
18 |
17 |
19 (* Theorems about sum and sumj *) |
18 (* Theorems about sum and sumj *) |
20 Goal "ALL i. I<i--> (sum I s = sumj I i s)"; |
19 Goal "ALL i. I<i--> (sum I s = sumj I i s)"; |
21 by (induct_tac "I" 1); |
20 by (induct_tac "I" 1); |
55 AddIffs [OK_iff_ok]; |
54 AddIffs [OK_iff_ok]; |
56 Addsimps [preserves_def]; |
55 Addsimps [preserves_def]; |
57 |
56 |
58 |
57 |
59 Goal "Component i: stable {s. C s = (c s) i + k}"; |
58 Goal "Component i: stable {s. C s = (c s) i + k}"; |
|
59 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
60 by (constrains_tac 1); |
60 by (constrains_tac 1); |
61 qed "p2"; |
61 qed "p2"; |
62 |
62 |
63 Goal "[| OK I Component; i:I |] \ |
63 Goal "[| OK I Component; i:I |] \ |
64 \ ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}"; |
64 \ ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}"; |