equal
deleted
inserted
replaced
50 |
50 |
51 Goalw [nodeOrder_def, next_def, inv_image_def] |
51 Goalw [nodeOrder_def, next_def, inv_image_def] |
52 "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"; |
52 "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"; |
53 by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq])); |
53 by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq])); |
54 by (auto_tac (claset(), |
54 by (auto_tac (claset(), |
55 simpset() addsplits [nat_diff_split'] |
55 simpset() addsplits [nat_diff_split] |
56 addsimps [linorder_neq_iff, mod_geq])); |
56 addsimps [linorder_neq_iff, mod_geq])); |
57 qed "nodeOrder_eq"; |
57 qed "nodeOrder_eq"; |
58 |
58 |
59 (*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
59 (*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
60 Note the use of case_tac. Reasoning about leadsTo takes practice!*) |
60 Note the use of case_tac. Reasoning about leadsTo takes practice!*) |