equal
deleted
inserted
replaced
32 val nodeOrder_def = (thm "nodeOrder_def"); |
32 val nodeOrder_def = (thm "nodeOrder_def"); |
33 val next_def = (thm "next_def"); |
33 val next_def = (thm "next_def"); |
34 |
34 |
35 AddIffs [thm "N_positive", thm"skip"]; |
35 AddIffs [thm "N_positive", thm"skip"]; |
36 |
36 |
37 Goalw [stable_def] "stable acts (Compl(E i) Un (HasTok i))"; |
37 Goalw [stable_def] "stable acts (-(E i) Un (HasTok i))"; |
38 by (rtac constrains_weaken 1); |
38 by (rtac constrains_weaken 1); |
39 by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1); |
39 by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1); |
40 by (auto_tac (claset(), simpset() addsimps [not_E_eq])); |
40 by (auto_tac (claset(), simpset() addsimps [not_E_eq])); |
41 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def]))); |
41 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def]))); |
42 qed "token_stable"; |
42 qed "token_stable"; |
94 |
94 |
95 |
95 |
96 (*Misra's TR9: the token reaches an arbitrary node*) |
96 (*Misra's TR9: the token reaches an arbitrary node*) |
97 Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)"; |
97 Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)"; |
98 by (rtac leadsTo_weaken_R 1); |
98 by (rtac leadsTo_weaken_R 1); |
99 by (res_inst_tac [("I", "Compl{j}"), ("f", "token"), ("B", "{}")] |
99 by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] |
100 (wf_nodeOrder RS bounded_induct) 1); |
100 (wf_nodeOrder RS bounded_induct) 1); |
101 by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
101 by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
102 HasTok_def]))); |
102 HasTok_def]))); |
103 by (Blast_tac 2); |
103 by (Blast_tac 2); |
104 by (Clarify_tac 1); |
104 by (Clarify_tac 1); |