equal
deleted
inserted
replaced
80 |
80 |
81 lemma nodeOrder_eq: |
81 lemma nodeOrder_eq: |
82 "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)" |
82 "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)" |
83 apply (unfold nodeOrder_def next_def) |
83 apply (unfold nodeOrder_def next_def) |
84 apply (auto simp add: mod_Suc mod_geq) |
84 apply (auto simp add: mod_Suc mod_geq) |
85 apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq) |
85 apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq) |
86 done |
86 done |
87 |
87 |
88 text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4. |
88 text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4. |
89 Note the use of \<open>cases\<close>. Reasoning about leadsTo takes practice!\<close> |
89 Note the use of \<open>cases\<close>. Reasoning about leadsTo takes practice!\<close> |
90 lemma TR7_nodeOrder: |
90 lemma TR7_nodeOrder: |