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"