equal
deleted
inserted
replaced
53 specification (publicKey) |
53 specification (publicKey) |
54 injective_publicKey: |
54 injective_publicKey: |
55 "publicKey b A = publicKey c A' ==> b=c & A=A'" |
55 "publicKey b A = publicKey c A' ==> b=c & A=A'" |
56 apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"]) |
56 apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"]) |
57 apply (auto simp add: inj_on_def split: agent.split, presburger+) |
57 apply (auto simp add: inj_on_def split: agent.split, presburger+) |
58 (*faster would be this: |
|
59 apply (simp split: agent.split, auto) |
|
60 apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ |
|
61 *) |
|
62 done |
58 done |
63 |
59 |
64 |
60 |
65 axioms |
61 axioms |
66 (*No private key equals any public key (essential to ensure that private |
62 (*No private key equals any public key (essential to ensure that private |