Reordering of premises for cut theorems, and new law MPair_synth_analz
authorpaulson
Fri Sep 13 18:46:08 1996 +0200 (1996-09-13)
changeset 1998f8230821f1e8
parent 1997 6efba890341e
child 1999 b5efc4108d04
Reordering of premises for cut theorems, and new law MPair_synth_analz
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Sep 13 13:22:08 1996 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Sep 13 18:46:08 1996 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4  qed "parts_trans";
     1.5  
     1.6  (*Cut*)
     1.7 -goal thy "!!H. [| X: parts H;  Y: parts (insert X H) |] ==> Y: parts H";
     1.8 +goal thy "!!H. [| Y: parts (insert X H);  X: parts H |] ==> Y: parts H";
     1.9  be parts_trans 1;
    1.10  by (Fast_tac 1);
    1.11  qed "parts_cut";
    1.12 @@ -432,7 +432,7 @@
    1.13  qed "analz_trans";
    1.14  
    1.15  (*Cut; Lemma 2 of Lowe*)
    1.16 -goal thy "!!H. [| X: analz H;  Y: analz (insert X H) |] ==> Y: analz H";
    1.17 +goal thy "!!H. [| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
    1.18  be analz_trans 1;
    1.19  by (Fast_tac 1);
    1.20  qed "analz_cut";
    1.21 @@ -528,7 +528,7 @@
    1.22  qed "synth_trans";
    1.23  
    1.24  (*Cut; Lemma 2 of Lowe*)
    1.25 -goal thy "!!H. [| X: synth H;  Y: synth (insert X H) |] ==> Y: synth H";
    1.26 +goal thy "!!H. [| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
    1.27  be synth_trans 1;
    1.28  by (Fast_tac 1);
    1.29  qed "synth_cut";
    1.30 @@ -634,6 +634,14 @@
    1.31  by (Fast_tac 1);
    1.32  qed "Fake_analz_insert";
    1.33  
    1.34 +(*Without this equation, other rules for synth and analz would yield
    1.35 +  redundant cases*)
    1.36 +goal thy "({|X,Y|} : synth (analz H)) = \
    1.37 +\         (X : synth (analz H) & Y : synth (analz H))";
    1.38 +by (Fast_tac 1);
    1.39 +qed "MPair_synth_analz";
    1.40 +
    1.41 +AddIffs [MPair_synth_analz];
    1.42  
    1.43  
    1.44  (*We do NOT want Crypt... messages broken up in protocols!!*)