equal
deleted
inserted
replaced
128 |
128 |
129 (*In any trace, there is an upper bound N on the greatest nonce in use.*) |
129 (*In any trace, there is an upper bound N on the greatest nonce in use.*) |
130 lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs" |
130 lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs" |
131 apply (induct_tac "evs") |
131 apply (induct_tac "evs") |
132 apply (rule_tac x = 0 in exI) |
132 apply (rule_tac x = 0 in exI) |
133 apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) |
133 apply (simp_all (no_asm_simp) add: used_Cons split: event.split) |
134 apply safe |
134 apply safe |
135 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
135 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
136 done |
136 done |
137 |
137 |
138 lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs" |
138 lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs" |