# HG changeset patch
# User haftmann
# Date 1263658528 -3600
# Node ID 156925dd67af736ebe1abb20241d1851ff51bcd7
# Parent  3e80eab831a1d93490979c84958c21a9a65cb144
dropped some old primrecs and some constdefs

diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Deriv.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -19,14 +19,13 @@
           ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
   "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
 
-consts
-  Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
 primrec
-  "Bolzano_bisect P a b 0 = (a,b)"
-  "Bolzano_bisect P a b (Suc n) =
-      (let (x,y) = Bolzano_bisect P a b n
-       in if P(x, (x+y)/2) then ((x+y)/2, y)
-                            else (x, (x+y)/2))"
+  Bolzano_bisect :: "(real \<times> real \<Rightarrow> bool) \<Rightarrow> real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real \<times> real" where
+  "Bolzano_bisect P a b 0 = (a, b)"
+  | "Bolzano_bisect P a b (Suc n) =
+      (let (x, y) = Bolzano_bisect P a b n
+       in if P (x, (x+y) / 2) then ((x+y)/2, y)
+                              else (x, (x+y)/2))"
 
 
 subsection {* Derivatives *}
diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -53,15 +53,14 @@
   qed
 qed
 
-consts
+primrec
   LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
-    'a \<Rightarrow> 'b Datatype.item"
-primrec
-  "LList_corec_aux 0 f x = {}"
-  "LList_corec_aux (Suc k) f x =
-    (case f x of
-      None \<Rightarrow> NIL
-    | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
+    'a \<Rightarrow> 'b Datatype.item" where
+    "LList_corec_aux 0 f x = {}"
+  | "LList_corec_aux (Suc k) f x =
+      (case f x of
+        None \<Rightarrow> NIL
+      | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
 
 definition "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
 
diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -530,11 +530,9 @@
   The set's element type must be wellordered (e.g. the natural numbers).
 *}
 
-consts
-  enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
-primrec
-  enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
-  enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
+primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
+    enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
+  | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
 
 lemma enumerate_Suc':
     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Library/Nested_Environment.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -43,18 +43,16 @@
   @{term None}.
 *}
 
-consts
+primrec
   lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
-  lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
-
-primrec (lookup)
-  "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
-  "lookup (Env b es) xs =
-    (case xs of
-      [] => Some (Env b es)
-    | y # ys => lookup_option (es y) ys)"
-  "lookup_option None xs = None"
-  "lookup_option (Some e) xs = lookup e xs"
+  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
+    "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
+  | "lookup (Env b es) xs =
+      (case xs of
+        [] => Some (Env b es)
+      | y # ys => lookup_option (es y) ys)"
+  | "lookup_option None xs = None"
+  | "lookup_option (Some e) xs = lookup e xs"
 
 hide const lookup_option
 
@@ -76,7 +74,7 @@
     | Some e => lookup e xs)"
   by (cases "es x") simp_all
 
-lemmas lookup.simps [simp del]
+lemmas lookup_lookup_option.simps [simp del]
   and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
 
 theorem lookup_eq:
@@ -247,24 +245,22 @@
   environment is left unchanged.
 *}
 
-consts
+primrec
   update :: "'c list => ('a, 'b, 'c) env option
     => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
-  update_option :: "'c list => ('a, 'b, 'c) env option
-    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
-
-primrec (update)
-  "update xs opt (Val a) =
-    (if xs = [] then (case opt of None => Val a | Some e => e)
-    else Val a)"
-  "update xs opt (Env b es) =
-    (case xs of
-      [] => (case opt of None => Env b es | Some e => e)
-    | y # ys => Env b (es (y := update_option ys opt (es y))))"
-  "update_option xs opt None =
-    (if xs = [] then opt else None)"
-  "update_option xs opt (Some e) =
-    (if xs = [] then opt else Some (update xs opt e))"
+  and update_option :: "'c list => ('a, 'b, 'c) env option
+    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
+    "update xs opt (Val a) =
+      (if xs = [] then (case opt of None => Val a | Some e => e)
+      else Val a)"
+  | "update xs opt (Env b es) =
+      (case xs of
+        [] => (case opt of None => Env b es | Some e => e)
+      | y # ys => Env b (es (y := update_option ys opt (es y))))"
+  | "update_option xs opt None =
+      (if xs = [] then opt else None)"
+  | "update_option xs opt (Some e) =
+      (if xs = [] then opt else Some (update xs opt e))"
 
 hide const update_option
 
@@ -294,7 +290,7 @@
       | Some e => Some (update (y # ys) opt e))))"
   by (cases "es x") simp_all
 
-lemmas update.simps [simp del]
+lemmas update_update_option.simps [simp del]
   and update_simps [simp] = update_nil_none update_nil_some
     update_cons_val update_cons_nil_env update_cons_cons_env
 
diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Library/Ramsey.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -12,13 +12,10 @@
 
 subsubsection {* ``Axiom'' of Dependent Choice *}
 
-consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
+primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
   --{*An integer-indexed chain of choices*}
-primrec
-  choice_0:   "choice P r 0 = (SOME x. P x)"
-
-  choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
-
+    choice_0:   "choice P r 0 = (SOME x. P x)"
+  | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
 
 lemma choice_n: 
   assumes P0: "P x0"
diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Library/Word.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -43,11 +43,21 @@
     "bitval \<zero> = 0"
   | "bitval \<one> = 1"
 
-consts
-  bitnot :: "bit => bit"
-  bitand :: "bit => bit => bit" (infixr "bitand" 35)
-  bitor  :: "bit => bit => bit" (infixr "bitor"  30)
-  bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
+primrec bitnot :: "bit => bit" where
+    bitnot_zero: "(bitnot \<zero>) = \<one>"
+  | bitnot_one : "(bitnot \<one>)  = \<zero>"
+
+primrec bitand :: "bit => bit => bit" (infixr "bitand" 35) where
+    bitand_zero: "(\<zero> bitand y) = \<zero>"
+  | bitand_one:  "(\<one> bitand y) = y"
+
+primrec bitor  :: "bit => bit => bit" (infixr "bitor"  30) where
+    bitor_zero: "(\<zero> bitor y) = y"
+  | bitor_one:  "(\<one> bitor y) = \<one>"
+
+primrec bitxor :: "bit => bit => bit" (infixr "bitxor" 30) where
+    bitxor_zero: "(\<zero> bitxor y) = y"
+  | bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
 
 notation (xsymbols)
   bitnot ("\<not>\<^sub>b _" [40] 40) and
@@ -61,22 +71,6 @@
   bitor  (infixr "\<or>\<^sub>b" 30) and
   bitxor (infixr "\<oplus>\<^sub>b" 30)
 
-primrec
-  bitnot_zero: "(bitnot \<zero>) = \<one>"
-  bitnot_one : "(bitnot \<one>)  = \<zero>"
-
-primrec
-  bitand_zero: "(\<zero> bitand y) = \<zero>"
-  bitand_one:  "(\<one> bitand y) = y"
-
-primrec
-  bitor_zero: "(\<zero> bitor y) = y"
-  bitor_one:  "(\<one> bitor y) = \<one>"
-
-primrec
-  bitxor_zero: "(\<zero> bitxor y) = y"
-  bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
-
 lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
   by (cases b) simp_all
 
@@ -244,11 +238,9 @@
   finally show "bv_extend n b w = bv_extend n b (b#w)" .
 qed
 
-consts
-  rem_initial :: "bit => bit list => bit list"
-primrec
-  "rem_initial b [] = []"
-  "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
+primrec rem_initial :: "bit => bit list => bit list" where
+    "rem_initial b [] = []"
+  | "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
 
 lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
   by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
@@ -808,14 +800,12 @@
 
 subsection {* Signed Vectors *}
 
-consts
-  norm_signed :: "bit list => bit list"
-primrec
-  norm_signed_Nil: "norm_signed [] = []"
-  norm_signed_Cons: "norm_signed (b#bs) =
-    (case b of
-      \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
-    | \<one> => b#rem_initial b bs)"
+primrec norm_signed :: "bit list => bit list" where
+    norm_signed_Nil: "norm_signed [] = []"
+  | norm_signed_Cons: "norm_signed (b#bs) =
+      (case b of
+        \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
+      | \<one> => b#rem_initial b bs)"
 
 lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
   by simp
@@ -1005,7 +995,7 @@
 proof (rule bit_list_cases [of w],simp_all)
   fix xs
   show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
-  proof (simp add: norm_signed_list_def,auto)
+  proof (simp add: norm_signed_def,auto)
     assume "norm_unsigned xs = []"
     hence xx: "rem_initial \<zero> xs = []"
       by (simp add: norm_unsigned_def)
@@ -2232,12 +2222,10 @@
 lemma "nat_to_bv (number_of Int.Pls) = []"
   by simp
 
-consts
-  fast_bv_to_nat_helper :: "[bit list, int] => int"
-primrec
-  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
-  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
-    fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
+primrec fast_bv_to_nat_helper :: "[bit list, int] => int" where
+    fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
+  | fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
+      fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
 
 declare fast_bv_to_nat_helper.simps [code del]
 
diff -r 3e80eab831a1 -r 156925dd67af src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/List.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -13,184 +13,182 @@
     Nil    ("[]")
   | Cons 'a  "'a list"    (infixr "#" 65)
 
+syntax
+  -- {* list Enumeration *}
+  "@list" :: "args => 'a list"    ("[(_)]")
+
+translations
+  "[x, xs]" == "x#[xs]"
+  "[x]" == "x#[]"
+
 subsection{*Basic list processing functions*}
 
-consts
-  filter:: "('a => bool) => 'a list => 'a list"
-  concat:: "'a list list => 'a list"
-  foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
-  foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
-  hd:: "'a list => 'a"
-  tl:: "'a list => 'a list"
-  last:: "'a list => 'a"
-  butlast :: "'a list => 'a list"
-  set :: "'a list => 'a set"
-  map :: "('a=>'b) => ('a list => 'b list)"
-  listsum ::  "'a list => 'a::monoid_add"
-  list_update :: "'a list => nat => 'a => 'a list"
-  take:: "nat => 'a list => 'a list"
-  drop:: "nat => 'a list => 'a list"
-  takeWhile :: "('a => bool) => 'a list => 'a list"
-  dropWhile :: "('a => bool) => 'a list => 'a list"
-  rev :: "'a list => 'a list"
-  zip :: "'a list => 'b list => ('a * 'b) list"
-  upt :: "nat => nat => nat list" ("(1[_..</_'])")
-  remdups :: "'a list => 'a list"
-  remove1 :: "'a => 'a list => 'a list"
-  removeAll :: "'a => 'a list => 'a list"
-  "distinct":: "'a list => bool"
-  replicate :: "nat => 'a => 'a list"
-  splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
+primrec
+  hd :: "'a list \<Rightarrow> 'a" where
+  "hd (x # xs) = x"
+
+primrec
+  tl :: "'a list \<Rightarrow> 'a list" where
+    "tl [] = []"
+  | "tl (x # xs) = xs"
+
+primrec
+  last :: "'a list \<Rightarrow> 'a" where
+  "last (x # xs) = (if xs = [] then x else last xs)"
+
+primrec
+  butlast :: "'a list \<Rightarrow> 'a list" where
+    "butlast []= []"
+  | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
+
+primrec
+  set :: "'a list \<Rightarrow> 'a set" where
+    "set [] = {}"
+  | "set (x # xs) = insert x (set xs)"
+
+primrec
+  map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+    "map f [] = []"
+  | "map f (x # xs) = f x # map f xs"
+
+primrec
+  append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
+    append_Nil:"[] @ ys = ys"
+  | append_Cons: "(x#xs) @ ys = x # xs @ ys"
+
+primrec
+  rev :: "'a list \<Rightarrow> 'a list" where
+    "rev [] = []"
+  | "rev (x # xs) = rev xs @ [x]"
+
+primrec
+  filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    "filter P [] = []"
+  | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
+
+syntax
+  -- {* Special syntax for filter *}
+  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
+
+translations
+  "[x<-xs . P]"== "CONST filter (%x. P) xs"
+
+syntax (xsymbols)
+  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
+syntax (HTML output)
+  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
+
+primrec
+  foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
+    foldl_Nil: "foldl f a [] = a"
+  | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
+
+primrec
+  foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+    "foldr f [] a = a"
+  | "foldr f (x # xs) a = f x (foldr f xs a)"
+
+primrec
+  concat:: "'a list list \<Rightarrow> 'a list" where
+    "concat [] = []"
+  | "concat (x # xs) = x @ concat xs"
+
+primrec (in monoid_add)
+  listsum :: "'a list \<Rightarrow> 'a" where
+    "listsum [] = 0"
+  | "listsum (x # xs) = x + listsum xs"
+
+primrec
+  drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    drop_Nil: "drop n [] = []"
+  | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+
+primrec
+  take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    take_Nil:"take n [] = []"
+  | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+
+primrec
+  nth :: "'a list => nat => 'a" (infixl "!" 100) where
+  nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+
+primrec
+  list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
+    "list_update [] i v = []"
+  | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
 
 nonterminals lupdbinds lupdbind
 
 syntax
-  -- {* list Enumeration *}
-  "@list" :: "args => 'a list"    ("[(_)]")
-
-  -- {* Special syntax for filter *}
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
-
-  -- {* list update *}
   "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   "" :: "lupdbind => lupdbinds"    ("_")
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
 
 translations
-  "[x, xs]" == "x#[xs]"
-  "[x]" == "x#[]"
-  "[x<-xs . P]"== "filter (%x. P) xs"
-
   "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
-  "xs[i:=x]" == "list_update xs i x"
-
-
-syntax (xsymbols)
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
-syntax (HTML output)
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
-
+  "xs[i:=x]" == "CONST list_update xs i x"
+
+primrec
+  takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    "takeWhile P [] = []"
+  | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
+
+primrec
+  dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    "dropWhile P [] = []"
+  | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
+
+primrec
+  zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
+    "zip xs [] = []"
+  | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
+
+primrec 
+  upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
+    upt_0: "[i..<0] = []"
+  | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
+
+primrec
+  distinct :: "'a list \<Rightarrow> bool" where
+    "distinct [] \<longleftrightarrow> True"
+  | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
+
+primrec
+  remdups :: "'a list \<Rightarrow> 'a list" where
+    "remdups [] = []"
+  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
+
+primrec
+  remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    "remove1 x [] = []"
+  | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
+
+primrec
+  removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    "removeAll x [] = []"
+  | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
+
+primrec
+  replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
+    replicate_0: "replicate 0 x = []"
+  | replicate_Suc: "replicate (Suc n) x = x # replicate n x"
 
 text {*
   Function @{text size} is overloaded for all datatypes. Users may
   refer to the list version as @{text length}. *}
 
 abbreviation
-  length :: "'a list => nat" where
-  "length == size"
-
-primrec
-  "hd(x#xs) = x"
-
-primrec
-  "tl([]) = []"
-  "tl(x#xs) = xs"
-
-primrec
-  "last(x#xs) = (if xs=[] then x else last xs)"
-
-primrec
-  "butlast []= []"
-  "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
-
-primrec
-  "set [] = {}"
-  "set (x#xs) = insert x (set xs)"
-
-primrec
-  "map f [] = []"
-  "map f (x#xs) = f(x)#map f xs"
-
-primrec
-  append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
-where
-  append_Nil:"[] @ ys = ys"
-  | append_Cons: "(x#xs) @ ys = x # xs @ ys"
-
-primrec
-  "rev([]) = []"
-  "rev(x#xs) = rev(xs) @ [x]"
-
-primrec
-  "filter P [] = []"
-  "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
-
-primrec
-  foldl_Nil:"foldl f a [] = a"
-  foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
-
-primrec
-  "foldr f [] a = a"
-  "foldr f (x#xs) a = f x (foldr f xs a)"
-
-primrec
-  "concat([]) = []"
-  "concat(x#xs) = x @ concat(xs)"
-
-primrec
-"listsum [] = 0"
-"listsum (x # xs) = x + listsum xs"
-
-primrec
-  drop_Nil:"drop n [] = []"
-  drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
-  -- {*Warning: simpset does not contain this definition, but separate
-       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
-
-primrec
-  take_Nil:"take n [] = []"
-  take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
-  -- {*Warning: simpset does not contain this definition, but separate
-       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
-
-primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
-  nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
-  -- {*Warning: simpset does not contain this definition, but separate
-       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
-
-primrec
-  "[][i:=v] = []"
-  "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
-
-primrec
-  "takeWhile P [] = []"
-  "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
-
-primrec
-  "dropWhile P [] = []"
-  "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
-
-primrec
-  "zip xs [] = []"
-  zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
-  -- {*Warning: simpset does not contain this definition, but separate
-       theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
-
-primrec
-  upt_0: "[i..<0] = []"
-  upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
-
-primrec
-  "distinct [] = True"
-  "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
-
-primrec
-  "remdups [] = []"
-  "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
-
-primrec
-  "remove1 x [] = []"
-  "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
-
-primrec
-  "removeAll x [] = []"
-  "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
-
-primrec
-  replicate_0: "replicate 0 x = []"
-  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
+  length :: "'a list \<Rightarrow> nat" where
+  "length \<equiv> size"
 
 definition
   rotate1 :: "'a list \<Rightarrow> 'a list" where
@@ -210,8 +208,9 @@
   "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
 
 primrec
-  "splice [] ys = ys"
-  "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
+  splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    "splice [] ys = ys"
+  | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"
     -- {*Warning: simpset does not contain the second eqn but a derived one. *}
 
 text{*
@@ -2435,8 +2434,8 @@
   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
 
 translations -- {* Beware of argument permutation! *}
-  "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
-  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
+  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
 
 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   by (induct xs) (simp_all add: left_distrib)
@@ -3532,10 +3531,9 @@
 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
 @{term A} and tail drawn from @{term Xs}.*}
 
-constdefs
-  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
-  "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
-declare set_Cons_def [code del]
+definition
+  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
+  [code del]: "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
 
 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
 by (auto simp add: set_Cons_def)
@@ -3543,10 +3541,10 @@
 text{*Yields the set of lists, all of the same length as the argument and
 with elements drawn from the corresponding element of the argument.*}
 
-consts  listset :: "'a set list \<Rightarrow> 'a list set"
 primrec
-   "listset []    = {[]}"
-   "listset(A#As) = set_Cons A (listset As)"
+  listset :: "'a set list \<Rightarrow> 'a list set" where
+     "listset [] = {[]}"
+  |  "listset (A # As) = set_Cons A (listset As)"
 
 
 subsection{*Relations on Lists*}
@@ -3555,26 +3553,21 @@
 
 text{*These orderings preserve well-foundedness: shorter lists 
   precede longer lists. These ordering are not used in dictionaries.*}
-
-consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
-        --{*The lexicographic ordering for lists of the specified length*}
-primrec
-  "lexn r 0 = {}"
-  "lexn r (Suc n) =
-    (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
-    {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
-
-constdefs
-  lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
-    "lex r == \<Union>n. lexn r n"
-        --{*Holds only between lists of the same length*}
-
-  lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
-    "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
-        --{*Compares lists by their length and then lexicographically*}
-
-declare lex_def [code del]
-
+        
+primrec -- {*The lexicographic ordering for lists of the specified length*}
+  lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
+    "lexn r 0 = {}"
+  | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
+      {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
+
+definition
+  lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
+  [code del]: "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
+
+definition
+  lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
+  [code del]: "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
+        -- {*Compares lists by their length and then lexicographically*}
 
 lemma wf_lexn: "wf r ==> wf (lexn r n)"
 apply (induct n, simp, simp)
@@ -3645,11 +3638,10 @@
     This ordering does \emph{not} preserve well-foundedness.
      Author: N. Voelker, March 2005. *} 
 
-constdefs 
-  lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
-  "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
+definition
+  lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
+  [code del]: "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
-declare lexord_def [code del]
 
 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
 by (unfold lexord_def, induct_tac y, auto) 
diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Map.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -51,10 +51,6 @@
   map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
   "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"
 
-consts
-  map_of :: "('a * 'b) list => 'a ~=> 'b"
-  map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
-
 nonterminals
   maplets maplet
 
@@ -73,25 +69,27 @@
 translations
   "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
   "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
-  "_MapUpd m (_maplets x y)"    == "map_upds m x y"
   "_Map ms"                     == "_MapUpd (CONST empty) ms"
   "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
   "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
 
 primrec
-  "map_of [] = empty"
-  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
+  map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
+    "map_of [] = empty"
+  | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
 
-declare map_of.simps [code del]
+definition
+  map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where
+  "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
+
+translations
+  "_MapUpd m (_maplets x y)"    == "CONST map_upds m x y"
 
 lemma map_of_Cons_code [code]: 
   "map_of [] k = None"
   "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
   by simp_all
 
-defs
-  map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
-
 
 subsection {* @{term [source] empty} *}
 
diff -r 3e80eab831a1 -r 156925dd67af src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOLCF/Fix.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -12,12 +12,9 @@
 
 subsection {* Iteration *}
 
-consts
-  iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)"
-
-primrec
-  "iterate 0 = (\<Lambda> F x. x)"
-  "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
+primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
+    "iterate 0 = (\<Lambda> F x. x)"
+  | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
 
 text {* Derive inductive properties of iterate from primitive recursion *}
 
diff -r 3e80eab831a1 -r 156925dd67af src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOLCF/Up.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -17,12 +17,9 @@
 syntax (xsymbols)
   "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
 
-consts
-  Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
-
-primrec
-  "Ifup f Ibottom = \<bottom>"
-  "Ifup f (Iup x) = f\<cdot>x"
+primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
+    "Ifup f Ibottom = \<bottom>"
+ |  "Ifup f (Iup x) = f\<cdot>x"
 
 subsection {* Ordering on lifted cpo *}
 
diff -r 3e80eab831a1 -r 156925dd67af src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOLCF/ex/Stream.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -550,8 +550,7 @@
 (* ----------------------------------------------------------------------- *)
 
 lemma i_rt_UU [simp]: "i_rt n UU = UU"
-apply (simp add: i_rt_def)
-by (rule iterate.induct,auto)
+  by (induct n) (simp_all add: i_rt_def)
 
 lemma i_rt_0 [simp]: "i_rt 0 s = s"
 by (simp add: i_rt_def)