equal
deleted
inserted
replaced
116 text\<open>Added to extend initstate with set of nonces\<close> |
116 text\<open>Added to extend initstate with set of nonces\<close> |
117 lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N" |
117 lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N" |
118 by auto |
118 by auto |
119 |
119 |
120 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
120 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
121 apply (unfold keysFor_def) |
121 unfolding keysFor_def |
122 apply (induct_tac "C", auto) |
122 apply (induct_tac "C", auto) |
123 done |
123 done |
124 |
124 |
125 (*Specialized to shared-key model: no @{term invKey}*) |
125 (*Specialized to shared-key model: no @{term invKey}*) |
126 lemma keysFor_parts_insert: |
126 lemma keysFor_parts_insert: |