src/HOL/Auth/Message.thy
changeset 27225 b316dde851f5
parent 27154 026f3db3f5c6
child 27239 f2f42f9fa09d
     1.1 --- a/src/HOL/Auth/Message.thy	Mon Jun 16 14:18:55 2008 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Mon Jun 16 17:54:35 2008 +0200
     1.3 @@ -819,20 +819,22 @@
     1.4  
     1.5  text{*Rewrites to push in Key and Crypt messages, so that other messages can
     1.6      be pulled out using the @{text analz_insert} rules*}
     1.7 -ML
     1.8 -{*
     1.9 -fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
    1.10  
    1.11 -bind_thms ("pushKeys",
    1.12 -           map (insComm "Key ?K") 
    1.13 -                   ["Agent ?C", "Nonce ?N", "Number ?N", 
    1.14 -		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
    1.15 +lemmas pushKeys [standard] =
    1.16 +  insert_commute [of "Key K" "Agent C"]
    1.17 +  insert_commute [of "Key K" "Nonce N"]
    1.18 +  insert_commute [of "Key K" "Number N"]
    1.19 +  insert_commute [of "Key K" "Hash X"]
    1.20 +  insert_commute [of "Key K" "MPair X Y"]
    1.21 +  insert_commute [of "Key K" "Crypt X K'"]
    1.22  
    1.23 -bind_thms ("pushCrypts",
    1.24 -           map (insComm "Crypt ?X ?K") 
    1.25 -                     ["Agent ?C", "Nonce ?N", "Number ?N", 
    1.26 -		      "Hash ?X'", "MPair ?X' ?Y"]);
    1.27 -*}
    1.28 +lemmas pushCrypts [standard] =
    1.29 +  insert_commute [of "Crypt X K" "Agent C"]
    1.30 +  insert_commute [of "Crypt X K" "Agent C"]
    1.31 +  insert_commute [of "Crypt X K" "Nonce N"]
    1.32 +  insert_commute [of "Crypt X K" "Number N"]
    1.33 +  insert_commute [of "Crypt X K" "Hash X'"]
    1.34 +  insert_commute [of "Crypt X K" "MPair X' Y"]
    1.35  
    1.36  text{*Cannot be added with @{text "[simp]"} -- messages should not always be
    1.37    re-ordered. *}