src/HOL/Auth/Guard/P1.thy

 lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}"
 by (auto simp: chain_def sign_def)
 
 subsubsection{*agent whose key is used to sign an offer*}
 
-consts shop :: "msg => msg"
-
-recdef shop "measure size"
+fun shop :: "msg => msg" where
 "shop {|B,X,Crypt K H|} = Agent (agt K)"
 
 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
 by (simp add: chain_def sign_def)
 
 subsubsection{*nonce used in an offer*}
 
-consts nonce :: "msg => msg"
-
-recdef nonce "measure size"
+fun nonce :: "msg => msg" where
 "nonce {|B,{|Crypt K ofr,m2|},CryptH|} = ofr"
 
 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
 by (simp add: chain_def sign_def)
 
 subsubsection{*next shop*}
 
-consts next_shop :: "msg => agent"
-
-recdef next_shop "measure size"
+fun next_shop :: "msg => agent" where
 "next_shop {|B,{|m1,Hash{|headL,Agent C|}|},CryptH|} = C"
 
 lemma next_shop_chain [iff]: "next_shop (chain B ofr A L C) = C"
 by (simp add: chain_def sign_def)
 

 by (erule valid.induct, auto simp: anchor_def chain_def sign_def
 offer_nonces_def initState.simps)
 
 subsubsection{*list of offers*}
 
-consts offers :: "msg => msg"
-
-recdef offers "measure size"
-"offers (cons M L) = cons {|shop M, nonce M|} (offers L)"
+fun offers :: "msg => msg" where
+"offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
 "offers other = nil"
 
 subsubsection{*list of agents whose keys are used to sign a list of offers*}
 
-consts shops :: "msg => msg"
-
-recdef shops "measure size"
-"shops (cons M L) = cons (shop M) (shops L)"
+fun shops :: "msg => msg" where
+"shops (cons M L) = cons (shop M) (shops L)" |
 "shops other = other"
 
 lemma shops_in_agl: "L:valid A n B ==> shops L:agl"
 by (erule valid.induct, auto simp: anchor_def chain_def sign_def)
 
 subsubsection{*builds a trace from an itinerary*}
 
-consts offer_list :: "agent * nat * agent * msg * nat => msg"
-
-recdef offer_list "measure (%(A,n,B,I,ofr). size I)"
-"offer_list (A,n,B,nil,ofr) = cons (anchor A n B) nil"
+fun offer_list :: "agent * nat * agent * msg * nat => msg" where
+"offer_list (A,n,B,nil,ofr) = cons (anchor A n B) nil" |
 "offer_list (A,n,B,cons (Agent C) I,ofr) = (
 let L = offer_list (A,n,B,I,Suc ofr) in
 cons (chain (next_shop (head L)) ofr A L C) L)"
 
 lemma "I:agl ==> ALL ofr. offer_list (A,n,B,I,ofr):valid A n B"
 by (erule agl.induct, auto)
 
-consts trace :: "agent * nat * agent * nat * msg * msg * msg
-=> event list"
-
-recdef trace "measure (%(B,ofr,A,r,I,L,K). size K)"
-"trace (B,ofr,A,r,I,L,nil) = []"
+fun trace :: "agent * nat * agent * nat * msg * msg * msg
+=> event list" where
+"trace (B,ofr,A,r,I,L,nil) = []" |
 "trace (B,ofr,A,r,I,L,cons (Agent D) K) = (
 let C = (if K=nil then B else agt_nb (head K)) in
 let I' = (if K=nil then cons (Agent A) (cons (Agent B) I)
           else cons (Agent A) (app (I, cons (head K) nil))) in
 let I'' = app (I, cons (head K) nil) in