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