equal
deleted
inserted
replaced
93 |
93 |
94 lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs" |
94 lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs" |
95 apply (induct evs, auto simp: initState.simps) |
95 apply (induct evs, auto simp: initState.simps) |
96 apply (drule used_sub_parts_used, safe) |
96 apply (drule used_sub_parts_used, safe) |
97 apply (drule greatest_msg_is_greatest, arith) |
97 apply (drule greatest_msg_is_greatest, arith) |
98 by (simp, arith) |
98 by simp |
99 |
99 |
100 subsubsection{*function giving a new nonce*} |
100 subsubsection{*function giving a new nonce*} |
101 |
101 |
102 constdefs new :: "event list => nat" |
102 constdefs new :: "event list => nat" |
103 "new evs == Suc (greatest evs)" |
103 "new evs == Suc (greatest evs)" |