New tactic: prove_unique_tac
authorpaulson
Mon Dec 16 11:08:11 1996 +0100 (1996-12-16)
changeset 241795f275c8476e
parent 2416 8ba800a46e14
child 2418 6b6a92d05fb2
New tactic: prove_unique_tac
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Dec 16 10:50:08 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Dec 16 11:08:11 1996 +0100
     1.3 @@ -306,11 +306,7 @@
     1.4  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
     1.5  \            : set_of_list evs;                                    \
     1.6  \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
     1.7 -by (dtac lemma 1);
     1.8 -by (REPEAT (etac exE 1));
     1.9 -(*Duplicate the assumption*)
    1.10 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.11 -by (fast_tac (!claset addSDs [spec]) 1);
    1.12 +by (prove_unique_tac lemma 1);
    1.13  qed "unique_session_keys";
    1.14  
    1.15  
    1.16 @@ -349,12 +345,7 @@
    1.17  \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
    1.18  \          evs : otway lost;  A ~: lost |]                                    \
    1.19  \        ==> B = C";
    1.20 -by (dtac lemma 1);
    1.21 -by (assume_tac 1);
    1.22 -by (etac exE 1);
    1.23 -(*Duplicate the assumption*)
    1.24 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.25 -by (fast_tac (!claset addSDs [spec]) 1);
    1.26 +by (prove_unique_tac lemma 1);
    1.27  qed "unique_NA";
    1.28  
    1.29  
    1.30 @@ -529,12 +520,7 @@
    1.31  \                  : parts(sees lost Spy evs);         \
    1.32  \          evs : otway lost;  B ~: lost |]             \
    1.33  \        ==> NC = NA & C = A";
    1.34 -by (dtac lemma 1);
    1.35 -by (assume_tac 1);
    1.36 -by (REPEAT (etac exE 1));
    1.37 -(*Duplicate the assumption*)
    1.38 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    1.39 -by (fast_tac (!claset addSDs [spec]) 1);
    1.40 +by (prove_unique_tac lemma 1);
    1.41  qed "unique_NB";
    1.42  
    1.43  
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Dec 16 10:50:08 1996 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Dec 16 11:08:11 1996 +0100
     2.3 @@ -276,11 +276,7 @@
     2.4  \           : set_of_list evs;                                     \
     2.5  \          evs : otway lost |]                                     \
     2.6  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
     2.7 -by (dtac lemma 1);
     2.8 -by (REPEAT (etac exE 1));
     2.9 -(*Duplicate the assumption*)
    2.10 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    2.11 -by (fast_tac (!claset addSDs [spec]) 1);
    2.12 +by (prove_unique_tac lemma 1);
    2.13  qed "unique_session_keys";
    2.14  
    2.15  
     3.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Dec 16 10:50:08 1996 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Dec 16 11:08:11 1996 +0100
     3.3 @@ -317,11 +317,7 @@
     3.4  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
     3.5  \            : set_of_list evs;                                    \
     3.6  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
     3.7 -by (dtac lemma 1);
     3.8 -by (REPEAT (etac exE 1));
     3.9 -(*Duplicate the assumption*)
    3.10 -by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
    3.11 -by (fast_tac (!claset addSDs [spec]) 1);
    3.12 +by (prove_unique_tac lemma 1);
    3.13  qed "unique_session_keys";
    3.14  
    3.15