src/HOL/Auth/Public.ML
changeset 3730 6933d20f335f
parent 3683 aafe719dff14
child 3919 c036caebfc75
equal deleted inserted replaced
3729:6be7cf5086ab 3730:6933d20f335f
    14 (*** Basic properties of pubK & priK ***)
    14 (*** Basic properties of pubK & priK ***)
    15 
    15 
    16 AddIffs [inj_pubK RS inj_eq];
    16 AddIffs [inj_pubK RS inj_eq];
    17 
    17 
    18 goal thy "!!A B. (priK A = priK B) = (A=B)";
    18 goal thy "!!A B. (priK A = priK B) = (A=B)";
    19 by (Step_tac 1);
    19 by Safe_tac;
    20 by (dres_inst_tac [("f","invKey")] arg_cong 1);
    20 by (dres_inst_tac [("f","invKey")] arg_cong 1);
    21 by (Full_simp_tac 1);
    21 by (Full_simp_tac 1);
    22 qed "priK_inj_eq";
    22 qed "priK_inj_eq";
    23 
    23 
    24 AddIffs [priK_inj_eq];
    24 AddIffs [priK_inj_eq];
    87       (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
    87       (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
    88        REPEAT_DETERM (etac MPair_analz 1) THEN
    88        REPEAT_DETERM (etac MPair_analz 1) THEN
    89        THEN_BEST_FIRST 
    89        THEN_BEST_FIRST 
    90          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
    90          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
    91          (has_fewer_prems 1, size_of_thm)
    91          (has_fewer_prems 1, size_of_thm)
    92          (Step_tac 1));
    92          Safe_tac);
    93 
    93 
    94 
    94 
    95 (*** Fresh nonces ***)
    95 (*** Fresh nonces ***)
    96 
    96 
    97 goal thy "Nonce N ~: parts (initState B)";
    97 goal thy "Nonce N ~: parts (initState B)";
   113 by (induct_tac "evs" 1);
   113 by (induct_tac "evs" 1);
   114 by (res_inst_tac [("x","0")] exI 1);
   114 by (res_inst_tac [("x","0")] exI 1);
   115 by (ALLGOALS (asm_simp_tac
   115 by (ALLGOALS (asm_simp_tac
   116 	      (!simpset addsimps [used_Cons]
   116 	      (!simpset addsimps [used_Cons]
   117 			setloop split_tac [expand_event_case, expand_if])));
   117 			setloop split_tac [expand_event_case, expand_if])));
   118 by (Step_tac 1);
   118 by Safe_tac;
   119 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
   119 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
   120 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
   120 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
   121 val lemma = result();
   121 val lemma = result();
   122 
   122 
   123 goal thy "EX N. Nonce N ~: used evs";
   123 goal thy "EX N. Nonce N ~: used evs";