# HG changeset patch
# User krauss
# Date 1267458165 -3600
# Node ID 83b0f75810f02f121bb1055ee539778ab517b09e
# Parent  47ee18b6ae324891b95a24206e6612500f52e08c
killed recdefs in HOL-Auth

diff -r 47ee18b6ae32 -r 83b0f75810f0 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Mon Mar 01 16:42:45 2010 +0100
@@ -54,9 +54,7 @@
 
 subsubsection{*extract the agent number of an Agent message*}
 
-consts agt_nb :: "msg => agent"
-
-recdef agt_nb "measure size"
+primrec agt_nb :: "msg => agent" where
 "agt_nb (Agent A) = A"
 
 subsubsection{*messages that are pairs*}
@@ -224,13 +222,12 @@
 
 subsubsection{*greatest nonce used in a message*}
 
-consts greatest_msg :: "msg => nat"
-
-recdef greatest_msg "measure size"
-"greatest_msg (Nonce n) = n"
-"greatest_msg {|X,Y|} = max (greatest_msg X) (greatest_msg Y)"
-"greatest_msg (Crypt K X) = greatest_msg X"
-"greatest_msg other = 0"
+fun greatest_msg :: "msg => nat"
+where
+  "greatest_msg (Nonce n) = n"
+| "greatest_msg {|X,Y|} = max (greatest_msg X) (greatest_msg Y)"
+| "greatest_msg (Crypt K X) = greatest_msg X"
+| "greatest_msg other = 0"
 
 lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
 by (induct X, auto)
@@ -629,12 +626,11 @@
 
 subsubsection{*message of an event*}
 
-consts msg :: "event => msg"
-
-recdef msg "measure size"
-"msg (Says A B X) = X"
-"msg (Gets A X) = X"
-"msg (Notes A X) = X"
+primrec msg :: "event => msg"
+where
+  "msg (Says A B X) = X"
+| "msg (Gets A X) = X"
+| "msg (Notes A X) = X"
 
 lemma used_sub_parts_used: "X:used (ev # evs) ==> X:parts {msg ev} Un used evs"
 by (induct ev, auto)
diff -r 47ee18b6ae32 -r 83b0f75810f0 src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy	Mon Mar 01 16:42:45 2010 +0100
@@ -178,12 +178,11 @@
 
 subsection{*number of Crypt's in a message*}
 
-consts crypt_nb :: "msg => nat"
-
-recdef crypt_nb "measure size"
-"crypt_nb (Crypt K X) = Suc (crypt_nb X)"
-"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y"
-"crypt_nb X = 0" (* otherwise *)
+fun crypt_nb :: "msg => nat"
+where
+  "crypt_nb (Crypt K X) = Suc (crypt_nb X)"
+| "crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y"
+| "crypt_nb X = 0" (* otherwise *)
 
 subsection{*basic facts about @{term crypt_nb}*}
 
@@ -192,11 +191,10 @@
 
 subsection{*number of Crypt's in a message list*}
 
-consts cnb :: "msg list => nat"
-
-recdef cnb "measure size"
-"cnb [] = 0"
-"cnb (X#l) = crypt_nb X + cnb l"
+primrec cnb :: "msg list => nat"
+where
+  "cnb [] = 0"
+| "cnb (X#l) = crypt_nb X + cnb l"
 
 subsection{*basic facts about @{term cnb}*}
 
diff -r 47ee18b6ae32 -r 83b0f75810f0 src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy	Mon Mar 01 16:42:45 2010 +0100
@@ -176,11 +176,9 @@
 
 subsection{*number of Crypt's in a message*}
 
-consts crypt_nb :: "msg => nat"
-
-recdef crypt_nb "measure size"
-"crypt_nb (Crypt K X) = Suc (crypt_nb X)"
-"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y"
+fun crypt_nb :: "msg => nat" where
+"crypt_nb (Crypt K X) = Suc (crypt_nb X)" |
+"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" |
 "crypt_nb X = 0" (* otherwise *)
 
 subsection{*basic facts about @{term crypt_nb}*}
@@ -190,10 +188,8 @@
 
 subsection{*number of Crypt's in a message list*}
 
-consts cnb :: "msg list => nat"
-
-recdef cnb "measure size"
-"cnb [] = 0"
+primrec cnb :: "msg list => nat" where
+"cnb [] = 0" |
 "cnb (X#l) = crypt_nb X + cnb l"
 
 subsection{*basic facts about @{term cnb}*}
diff -r 47ee18b6ae32 -r 83b0f75810f0 src/HOL/Auth/Guard/Guard_Public.thy
--- a/src/HOL/Auth/Guard/Guard_Public.thy	Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy	Mon Mar 01 16:42:45 2010 +0100
@@ -85,11 +85,10 @@
 
 subsubsection{*greatest nonce used in a trace, 0 if there is no nonce*}
 
-consts greatest :: "event list => nat"
-
-recdef greatest "measure size"
-"greatest [] = 0"
-"greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)"
+primrec greatest :: "event list => nat"
+where
+  "greatest [] = 0"
+| "greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)"
 
 lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs"
 apply (induct evs, auto simp: initState.simps)
diff -r 47ee18b6ae32 -r 83b0f75810f0 src/HOL/Auth/Guard/List_Msg.thy
--- a/src/HOL/Auth/Guard/List_Msg.thy	Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy	Mon Mar 01 16:42:45 2010 +0100
@@ -29,24 +29,18 @@
 
 subsubsection{*head*}
 
-consts head :: "msg => msg"
-
-recdef head "measure size"
+primrec head :: "msg => msg" where
 "head (cons x l) = x"
 
 subsubsection{*tail*}
 
-consts tail :: "msg => msg"
-
-recdef tail "measure size"
+primrec tail :: "msg => msg" where
 "tail (cons x l) = l"
 
 subsubsection{*length*}
 
-consts len :: "msg => nat"
-
-recdef len "measure size"
-"len (cons x l) = Suc (len l)"
+fun len :: "msg => nat" where
+"len (cons x l) = Suc (len l)" |
 "len other = 0"
 
 lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
@@ -54,18 +48,14 @@
 
 subsubsection{*membership*}
 
-consts isin :: "msg * msg => bool"
-
-recdef isin "measure (%(x,l). size l)"
-"isin (x, cons y l) = (x=y | isin (x,l))"
+fun isin :: "msg * msg => bool" where
+"isin (x, cons y l) = (x=y | isin (x,l))" |
 "isin (x, other) = False"
 
 subsubsection{*delete an element*}
 
-consts del :: "msg * msg => msg"
-
-recdef del "measure (%(x,l). size l)"
-"del (x, cons y l) = (if x=y then l else cons y (del (x,l)))"
+fun del :: "msg * msg => msg" where
+"del (x, cons y l) = (if x=y then l else cons y (del (x,l)))" |
 "del (x, other) = other"
 
 lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l"
@@ -76,10 +66,8 @@
 
 subsubsection{*concatenation*}
 
-consts app :: "msg * msg => msg"
-
-recdef app "measure (%(l,l'). size l)"
-"app (cons x l, l') = cons x (app (l,l'))"
+fun app :: "msg * msg => msg" where
+"app (cons x l, l') = cons x (app (l,l'))" |
 "app (other, l') = l'"
 
 lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))"
@@ -87,20 +75,16 @@
 
 subsubsection{*replacement*}
 
-consts repl :: "msg * nat * msg => msg"
-
-recdef repl "measure (%(l,i,x'). i)"
-"repl (cons x l, Suc i, x') = cons x (repl (l,i,x'))"
-"repl (cons x l, 0, x') = cons x' l"
+fun repl :: "msg * nat * msg => msg" where
+"repl (cons x l, Suc i, x') = cons x (repl (l,i,x'))" |
+"repl (cons x l, 0, x') = cons x' l" |
 "repl (other, i, M') = other"
 
 subsubsection{*ith element*}
 
-consts ith :: "msg * nat => msg"
-
-recdef ith "measure (%(l,i). i)"
-"ith (cons x l, Suc i) = ith (l,i)"
-"ith (cons x l, 0) = x"
+fun ith :: "msg * nat => msg" where
+"ith (cons x l, Suc i) = ith (l,i)" |
+"ith (cons x l, 0) = x" |
 "ith (other, i) = other"
 
 lemma ith_head: "0 < len l ==> ith (l,0) = head l"
@@ -108,10 +92,8 @@
 
 subsubsection{*insertion*}
 
-consts ins :: "msg * nat * msg => msg"
-
-recdef ins "measure (%(l,i,x). i)"
-"ins (cons x l, Suc i, y) = cons x (ins (l,i,y))"
+fun ins :: "msg * nat * msg => msg" where
+"ins (cons x l, Suc i, y) = cons x (ins (l,i,y))" |
 "ins (l, 0, y) = cons y l"
 
 lemma ins_head [simp]: "ins (l,0,y) = cons y l"
@@ -119,10 +101,8 @@
 
 subsubsection{*truncation*}
 
-consts trunc :: "msg * nat => msg"
-
-recdef trunc "measure (%(l,i). i)"
-"trunc (l,0) = l"
+fun trunc :: "msg * nat => msg" where
+"trunc (l,0) = l" |
 "trunc (cons x l, Suc i) = trunc (l,i)"
 
 lemma trunc_zero [simp]: "trunc (l,0) = l"
diff -r 47ee18b6ae32 -r 83b0f75810f0 src/HOL/Auth/Guard/P1.thy
--- a/src/HOL/Auth/Guard/P1.thy	Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/P1.thy	Mon Mar 01 16:42:45 2010 +0100
@@ -56,9 +56,7 @@
 
 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"
@@ -66,9 +64,7 @@
 
 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"
@@ -76,9 +72,7 @@
 
 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"
@@ -209,18 +203,14 @@
 
 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"
@@ -228,10 +218,8 @@
 
 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)"
@@ -239,11 +227,9 @@
 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)
diff -r 47ee18b6ae32 -r 83b0f75810f0 src/HOL/Auth/Guard/P2.thy
--- a/src/HOL/Auth/Guard/P2.thy	Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/P2.thy	Mon Mar 01 16:42:45 2010 +0100
@@ -43,9 +43,7 @@
 
 subsubsection{*agent whose key is used to sign an offer*}
 
-consts shop :: "msg => msg"
-
-recdef shop "measure size"
+fun shop :: "msg => msg" where
 "shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')"
 
 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
@@ -53,9 +51,7 @@
 
 subsubsection{*nonce used in an offer*}
 
-consts nonce :: "msg => msg"
-
-recdef nonce "measure size"
+fun nonce :: "msg => msg" where
 "nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr"
 
 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
@@ -63,9 +59,7 @@
 
 subsubsection{*next shop*}
 
-consts next_shop :: "msg => agent"
-
-recdef next_shop "measure size"
+fun next_shop :: "msg => agent" where
 "next_shop {|m1,Hash {|headL,Agent C|}|} = C"
 
 lemma "next_shop (chain B ofr A L C) = C"
@@ -164,11 +158,10 @@
 
 subsubsection{*list of offers*}
 
-consts offers :: "msg => msg"
-
-recdef offers "measure size"
-"offers (cons M L) = cons {|shop M, nonce M|} (offers L)"
-"offers other = nil"
+fun offers :: "msg => msg"
+where
+  "offers (cons M L) = cons {|shop M, nonce M|} (offers L)"
+| "offers other = nil"
 
 
 subsection{*Properties of Protocol P2*}