dropped some old primrecs and some constdefs
authorhaftmann
Sat Jan 16 17:15:28 2010 +0100 (2010-01-16)
changeset 34941156925dd67af
parent 34940 3e80eab831a1
child 34942 d62eddd9e253
dropped some old primrecs and some constdefs
src/HOL/Deriv.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOLCF/Fix.thy
src/HOLCF/Up.thy
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOL/Deriv.thy	Sat Jan 16 17:15:27 2010 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Sat Jan 16 17:15:28 2010 +0100
     1.3 @@ -19,14 +19,13 @@
     1.4            ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
     1.5    "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
     1.6  
     1.7 -consts
     1.8 -  Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
     1.9  primrec
    1.10 -  "Bolzano_bisect P a b 0 = (a,b)"
    1.11 -  "Bolzano_bisect P a b (Suc n) =
    1.12 -      (let (x,y) = Bolzano_bisect P a b n
    1.13 -       in if P(x, (x+y)/2) then ((x+y)/2, y)
    1.14 -                            else (x, (x+y)/2))"
    1.15 +  Bolzano_bisect :: "(real \<times> real \<Rightarrow> bool) \<Rightarrow> real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real \<times> real" where
    1.16 +  "Bolzano_bisect P a b 0 = (a, b)"
    1.17 +  | "Bolzano_bisect P a b (Suc n) =
    1.18 +      (let (x, y) = Bolzano_bisect P a b n
    1.19 +       in if P (x, (x+y) / 2) then ((x+y)/2, y)
    1.20 +                              else (x, (x+y)/2))"
    1.21  
    1.22  
    1.23  subsection {* Derivatives *}
     2.1 --- a/src/HOL/Library/Coinductive_List.thy	Sat Jan 16 17:15:27 2010 +0100
     2.2 +++ b/src/HOL/Library/Coinductive_List.thy	Sat Jan 16 17:15:28 2010 +0100
     2.3 @@ -53,15 +53,14 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 -consts
     2.8 +primrec
     2.9    LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
    2.10 -    'a \<Rightarrow> 'b Datatype.item"
    2.11 -primrec
    2.12 -  "LList_corec_aux 0 f x = {}"
    2.13 -  "LList_corec_aux (Suc k) f x =
    2.14 -    (case f x of
    2.15 -      None \<Rightarrow> NIL
    2.16 -    | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
    2.17 +    'a \<Rightarrow> 'b Datatype.item" where
    2.18 +    "LList_corec_aux 0 f x = {}"
    2.19 +  | "LList_corec_aux (Suc k) f x =
    2.20 +      (case f x of
    2.21 +        None \<Rightarrow> NIL
    2.22 +      | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
    2.23  
    2.24  definition "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
    2.25  
     3.1 --- a/src/HOL/Library/Infinite_Set.thy	Sat Jan 16 17:15:27 2010 +0100
     3.2 +++ b/src/HOL/Library/Infinite_Set.thy	Sat Jan 16 17:15:28 2010 +0100
     3.3 @@ -530,11 +530,9 @@
     3.4    The set's element type must be wellordered (e.g. the natural numbers).
     3.5  *}
     3.6  
     3.7 -consts
     3.8 -  enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
     3.9 -primrec
    3.10 -  enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
    3.11 -  enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
    3.12 +primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
    3.13 +    enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
    3.14 +  | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
    3.15  
    3.16  lemma enumerate_Suc':
    3.17      "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
     4.1 --- a/src/HOL/Library/Nested_Environment.thy	Sat Jan 16 17:15:27 2010 +0100
     4.2 +++ b/src/HOL/Library/Nested_Environment.thy	Sat Jan 16 17:15:28 2010 +0100
     4.3 @@ -43,18 +43,16 @@
     4.4    @{term None}.
     4.5  *}
     4.6  
     4.7 -consts
     4.8 +primrec
     4.9    lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
    4.10 -  lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
    4.11 -
    4.12 -primrec (lookup)
    4.13 -  "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    4.14 -  "lookup (Env b es) xs =
    4.15 -    (case xs of
    4.16 -      [] => Some (Env b es)
    4.17 -    | y # ys => lookup_option (es y) ys)"
    4.18 -  "lookup_option None xs = None"
    4.19 -  "lookup_option (Some e) xs = lookup e xs"
    4.20 +  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
    4.21 +    "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    4.22 +  | "lookup (Env b es) xs =
    4.23 +      (case xs of
    4.24 +        [] => Some (Env b es)
    4.25 +      | y # ys => lookup_option (es y) ys)"
    4.26 +  | "lookup_option None xs = None"
    4.27 +  | "lookup_option (Some e) xs = lookup e xs"
    4.28  
    4.29  hide const lookup_option
    4.30  
    4.31 @@ -76,7 +74,7 @@
    4.32      | Some e => lookup e xs)"
    4.33    by (cases "es x") simp_all
    4.34  
    4.35 -lemmas lookup.simps [simp del]
    4.36 +lemmas lookup_lookup_option.simps [simp del]
    4.37    and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
    4.38  
    4.39  theorem lookup_eq:
    4.40 @@ -247,24 +245,22 @@
    4.41    environment is left unchanged.
    4.42  *}
    4.43  
    4.44 -consts
    4.45 +primrec
    4.46    update :: "'c list => ('a, 'b, 'c) env option
    4.47      => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
    4.48 -  update_option :: "'c list => ('a, 'b, 'c) env option
    4.49 -    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
    4.50 -
    4.51 -primrec (update)
    4.52 -  "update xs opt (Val a) =
    4.53 -    (if xs = [] then (case opt of None => Val a | Some e => e)
    4.54 -    else Val a)"
    4.55 -  "update xs opt (Env b es) =
    4.56 -    (case xs of
    4.57 -      [] => (case opt of None => Env b es | Some e => e)
    4.58 -    | y # ys => Env b (es (y := update_option ys opt (es y))))"
    4.59 -  "update_option xs opt None =
    4.60 -    (if xs = [] then opt else None)"
    4.61 -  "update_option xs opt (Some e) =
    4.62 -    (if xs = [] then opt else Some (update xs opt e))"
    4.63 +  and update_option :: "'c list => ('a, 'b, 'c) env option
    4.64 +    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
    4.65 +    "update xs opt (Val a) =
    4.66 +      (if xs = [] then (case opt of None => Val a | Some e => e)
    4.67 +      else Val a)"
    4.68 +  | "update xs opt (Env b es) =
    4.69 +      (case xs of
    4.70 +        [] => (case opt of None => Env b es | Some e => e)
    4.71 +      | y # ys => Env b (es (y := update_option ys opt (es y))))"
    4.72 +  | "update_option xs opt None =
    4.73 +      (if xs = [] then opt else None)"
    4.74 +  | "update_option xs opt (Some e) =
    4.75 +      (if xs = [] then opt else Some (update xs opt e))"
    4.76  
    4.77  hide const update_option
    4.78  
    4.79 @@ -294,7 +290,7 @@
    4.80        | Some e => Some (update (y # ys) opt e))))"
    4.81    by (cases "es x") simp_all
    4.82  
    4.83 -lemmas update.simps [simp del]
    4.84 +lemmas update_update_option.simps [simp del]
    4.85    and update_simps [simp] = update_nil_none update_nil_some
    4.86      update_cons_val update_cons_nil_env update_cons_cons_env
    4.87  
     5.1 --- a/src/HOL/Library/Ramsey.thy	Sat Jan 16 17:15:27 2010 +0100
     5.2 +++ b/src/HOL/Library/Ramsey.thy	Sat Jan 16 17:15:28 2010 +0100
     5.3 @@ -12,13 +12,10 @@
     5.4  
     5.5  subsubsection {* ``Axiom'' of Dependent Choice *}
     5.6  
     5.7 -consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
     5.8 +primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
     5.9    --{*An integer-indexed chain of choices*}
    5.10 -primrec
    5.11 -  choice_0:   "choice P r 0 = (SOME x. P x)"
    5.12 -
    5.13 -  choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
    5.14 -
    5.15 +    choice_0:   "choice P r 0 = (SOME x. P x)"
    5.16 +  | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
    5.17  
    5.18  lemma choice_n: 
    5.19    assumes P0: "P x0"
     6.1 --- a/src/HOL/Library/Word.thy	Sat Jan 16 17:15:27 2010 +0100
     6.2 +++ b/src/HOL/Library/Word.thy	Sat Jan 16 17:15:28 2010 +0100
     6.3 @@ -43,11 +43,21 @@
     6.4      "bitval \<zero> = 0"
     6.5    | "bitval \<one> = 1"
     6.6  
     6.7 -consts
     6.8 -  bitnot :: "bit => bit"
     6.9 -  bitand :: "bit => bit => bit" (infixr "bitand" 35)
    6.10 -  bitor  :: "bit => bit => bit" (infixr "bitor"  30)
    6.11 -  bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
    6.12 +primrec bitnot :: "bit => bit" where
    6.13 +    bitnot_zero: "(bitnot \<zero>) = \<one>"
    6.14 +  | bitnot_one : "(bitnot \<one>)  = \<zero>"
    6.15 +
    6.16 +primrec bitand :: "bit => bit => bit" (infixr "bitand" 35) where
    6.17 +    bitand_zero: "(\<zero> bitand y) = \<zero>"
    6.18 +  | bitand_one:  "(\<one> bitand y) = y"
    6.19 +
    6.20 +primrec bitor  :: "bit => bit => bit" (infixr "bitor"  30) where
    6.21 +    bitor_zero: "(\<zero> bitor y) = y"
    6.22 +  | bitor_one:  "(\<one> bitor y) = \<one>"
    6.23 +
    6.24 +primrec bitxor :: "bit => bit => bit" (infixr "bitxor" 30) where
    6.25 +    bitxor_zero: "(\<zero> bitxor y) = y"
    6.26 +  | bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
    6.27  
    6.28  notation (xsymbols)
    6.29    bitnot ("\<not>\<^sub>b _" [40] 40) and
    6.30 @@ -61,22 +71,6 @@
    6.31    bitor  (infixr "\<or>\<^sub>b" 30) and
    6.32    bitxor (infixr "\<oplus>\<^sub>b" 30)
    6.33  
    6.34 -primrec
    6.35 -  bitnot_zero: "(bitnot \<zero>) = \<one>"
    6.36 -  bitnot_one : "(bitnot \<one>)  = \<zero>"
    6.37 -
    6.38 -primrec
    6.39 -  bitand_zero: "(\<zero> bitand y) = \<zero>"
    6.40 -  bitand_one:  "(\<one> bitand y) = y"
    6.41 -
    6.42 -primrec
    6.43 -  bitor_zero: "(\<zero> bitor y) = y"
    6.44 -  bitor_one:  "(\<one> bitor y) = \<one>"
    6.45 -
    6.46 -primrec
    6.47 -  bitxor_zero: "(\<zero> bitxor y) = y"
    6.48 -  bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
    6.49 -
    6.50  lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
    6.51    by (cases b) simp_all
    6.52  
    6.53 @@ -244,11 +238,9 @@
    6.54    finally show "bv_extend n b w = bv_extend n b (b#w)" .
    6.55  qed
    6.56  
    6.57 -consts
    6.58 -  rem_initial :: "bit => bit list => bit list"
    6.59 -primrec
    6.60 -  "rem_initial b [] = []"
    6.61 -  "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
    6.62 +primrec rem_initial :: "bit => bit list => bit list" where
    6.63 +    "rem_initial b [] = []"
    6.64 +  | "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
    6.65  
    6.66  lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
    6.67    by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
    6.68 @@ -808,14 +800,12 @@
    6.69  
    6.70  subsection {* Signed Vectors *}
    6.71  
    6.72 -consts
    6.73 -  norm_signed :: "bit list => bit list"
    6.74 -primrec
    6.75 -  norm_signed_Nil: "norm_signed [] = []"
    6.76 -  norm_signed_Cons: "norm_signed (b#bs) =
    6.77 -    (case b of
    6.78 -      \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
    6.79 -    | \<one> => b#rem_initial b bs)"
    6.80 +primrec norm_signed :: "bit list => bit list" where
    6.81 +    norm_signed_Nil: "norm_signed [] = []"
    6.82 +  | norm_signed_Cons: "norm_signed (b#bs) =
    6.83 +      (case b of
    6.84 +        \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
    6.85 +      | \<one> => b#rem_initial b bs)"
    6.86  
    6.87  lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
    6.88    by simp
    6.89 @@ -1005,7 +995,7 @@
    6.90  proof (rule bit_list_cases [of w],simp_all)
    6.91    fix xs
    6.92    show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
    6.93 -  proof (simp add: norm_signed_list_def,auto)
    6.94 +  proof (simp add: norm_signed_def,auto)
    6.95      assume "norm_unsigned xs = []"
    6.96      hence xx: "rem_initial \<zero> xs = []"
    6.97        by (simp add: norm_unsigned_def)
    6.98 @@ -2232,12 +2222,10 @@
    6.99  lemma "nat_to_bv (number_of Int.Pls) = []"
   6.100    by simp
   6.101  
   6.102 -consts
   6.103 -  fast_bv_to_nat_helper :: "[bit list, int] => int"
   6.104 -primrec
   6.105 -  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
   6.106 -  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
   6.107 -    fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
   6.108 +primrec fast_bv_to_nat_helper :: "[bit list, int] => int" where
   6.109 +    fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
   6.110 +  | fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
   6.111 +      fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
   6.112  
   6.113  declare fast_bv_to_nat_helper.simps [code del]
   6.114  
     7.1 --- a/src/HOL/List.thy	Sat Jan 16 17:15:27 2010 +0100
     7.2 +++ b/src/HOL/List.thy	Sat Jan 16 17:15:28 2010 +0100
     7.3 @@ -13,184 +13,182 @@
     7.4      Nil    ("[]")
     7.5    | Cons 'a  "'a list"    (infixr "#" 65)
     7.6  
     7.7 +syntax
     7.8 +  -- {* list Enumeration *}
     7.9 +  "@list" :: "args => 'a list"    ("[(_)]")
    7.10 +
    7.11 +translations
    7.12 +  "[x, xs]" == "x#[xs]"
    7.13 +  "[x]" == "x#[]"
    7.14 +
    7.15  subsection{*Basic list processing functions*}
    7.16  
    7.17 -consts
    7.18 -  filter:: "('a => bool) => 'a list => 'a list"
    7.19 -  concat:: "'a list list => 'a list"
    7.20 -  foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
    7.21 -  foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
    7.22 -  hd:: "'a list => 'a"
    7.23 -  tl:: "'a list => 'a list"
    7.24 -  last:: "'a list => 'a"
    7.25 -  butlast :: "'a list => 'a list"
    7.26 -  set :: "'a list => 'a set"
    7.27 -  map :: "('a=>'b) => ('a list => 'b list)"
    7.28 -  listsum ::  "'a list => 'a::monoid_add"
    7.29 -  list_update :: "'a list => nat => 'a => 'a list"
    7.30 -  take:: "nat => 'a list => 'a list"
    7.31 -  drop:: "nat => 'a list => 'a list"
    7.32 -  takeWhile :: "('a => bool) => 'a list => 'a list"
    7.33 -  dropWhile :: "('a => bool) => 'a list => 'a list"
    7.34 -  rev :: "'a list => 'a list"
    7.35 -  zip :: "'a list => 'b list => ('a * 'b) list"
    7.36 -  upt :: "nat => nat => nat list" ("(1[_..</_'])")
    7.37 -  remdups :: "'a list => 'a list"
    7.38 -  remove1 :: "'a => 'a list => 'a list"
    7.39 -  removeAll :: "'a => 'a list => 'a list"
    7.40 -  "distinct":: "'a list => bool"
    7.41 -  replicate :: "nat => 'a => 'a list"
    7.42 -  splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    7.43 -
    7.44 +primrec
    7.45 +  hd :: "'a list \<Rightarrow> 'a" where
    7.46 +  "hd (x # xs) = x"
    7.47 +
    7.48 +primrec
    7.49 +  tl :: "'a list \<Rightarrow> 'a list" where
    7.50 +    "tl [] = []"
    7.51 +  | "tl (x # xs) = xs"
    7.52 +
    7.53 +primrec
    7.54 +  last :: "'a list \<Rightarrow> 'a" where
    7.55 +  "last (x # xs) = (if xs = [] then x else last xs)"
    7.56 +
    7.57 +primrec
    7.58 +  butlast :: "'a list \<Rightarrow> 'a list" where
    7.59 +    "butlast []= []"
    7.60 +  | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
    7.61 +
    7.62 +primrec
    7.63 +  set :: "'a list \<Rightarrow> 'a set" where
    7.64 +    "set [] = {}"
    7.65 +  | "set (x # xs) = insert x (set xs)"
    7.66 +
    7.67 +primrec
    7.68 +  map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    7.69 +    "map f [] = []"
    7.70 +  | "map f (x # xs) = f x # map f xs"
    7.71 +
    7.72 +primrec
    7.73 +  append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
    7.74 +    append_Nil:"[] @ ys = ys"
    7.75 +  | append_Cons: "(x#xs) @ ys = x # xs @ ys"
    7.76 +
    7.77 +primrec
    7.78 +  rev :: "'a list \<Rightarrow> 'a list" where
    7.79 +    "rev [] = []"
    7.80 +  | "rev (x # xs) = rev xs @ [x]"
    7.81 +
    7.82 +primrec
    7.83 +  filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    7.84 +    "filter P [] = []"
    7.85 +  | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
    7.86 +
    7.87 +syntax
    7.88 +  -- {* Special syntax for filter *}
    7.89 +  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
    7.90 +
    7.91 +translations
    7.92 +  "[x<-xs . P]"== "CONST filter (%x. P) xs"
    7.93 +
    7.94 +syntax (xsymbols)
    7.95 +  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    7.96 +syntax (HTML output)
    7.97 +  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    7.98 +
    7.99 +primrec
   7.100 +  foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
   7.101 +    foldl_Nil: "foldl f a [] = a"
   7.102 +  | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
   7.103 +
   7.104 +primrec
   7.105 +  foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   7.106 +    "foldr f [] a = a"
   7.107 +  | "foldr f (x # xs) a = f x (foldr f xs a)"
   7.108 +
   7.109 +primrec
   7.110 +  concat:: "'a list list \<Rightarrow> 'a list" where
   7.111 +    "concat [] = []"
   7.112 +  | "concat (x # xs) = x @ concat xs"
   7.113 +
   7.114 +primrec (in monoid_add)
   7.115 +  listsum :: "'a list \<Rightarrow> 'a" where
   7.116 +    "listsum [] = 0"
   7.117 +  | "listsum (x # xs) = x + listsum xs"
   7.118 +
   7.119 +primrec
   7.120 +  drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.121 +    drop_Nil: "drop n [] = []"
   7.122 +  | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
   7.123 +  -- {*Warning: simpset does not contain this definition, but separate
   7.124 +       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   7.125 +
   7.126 +primrec
   7.127 +  take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.128 +    take_Nil:"take n [] = []"
   7.129 +  | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
   7.130 +  -- {*Warning: simpset does not contain this definition, but separate
   7.131 +       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   7.132 +
   7.133 +primrec
   7.134 +  nth :: "'a list => nat => 'a" (infixl "!" 100) where
   7.135 +  nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
   7.136 +  -- {*Warning: simpset does not contain this definition, but separate
   7.137 +       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   7.138 +
   7.139 +primrec
   7.140 +  list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   7.141 +    "list_update [] i v = []"
   7.142 +  | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
   7.143  
   7.144  nonterminals lupdbinds lupdbind
   7.145  
   7.146  syntax
   7.147 -  -- {* list Enumeration *}
   7.148 -  "@list" :: "args => 'a list"    ("[(_)]")
   7.149 -
   7.150 -  -- {* Special syntax for filter *}
   7.151 -  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
   7.152 -
   7.153 -  -- {* list update *}
   7.154    "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   7.155    "" :: "lupdbind => lupdbinds"    ("_")
   7.156    "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   7.157    "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
   7.158  
   7.159  translations
   7.160 -  "[x, xs]" == "x#[xs]"
   7.161 -  "[x]" == "x#[]"
   7.162 -  "[x<-xs . P]"== "filter (%x. P) xs"
   7.163 -
   7.164    "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
   7.165 -  "xs[i:=x]" == "list_update xs i x"
   7.166 -
   7.167 -
   7.168 -syntax (xsymbols)
   7.169 -  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   7.170 -syntax (HTML output)
   7.171 -  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   7.172 -
   7.173 +  "xs[i:=x]" == "CONST list_update xs i x"
   7.174 +
   7.175 +primrec
   7.176 +  takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.177 +    "takeWhile P [] = []"
   7.178 +  | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
   7.179 +
   7.180 +primrec
   7.181 +  dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.182 +    "dropWhile P [] = []"
   7.183 +  | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
   7.184 +
   7.185 +primrec
   7.186 +  zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   7.187 +    "zip xs [] = []"
   7.188 +  | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
   7.189 +  -- {*Warning: simpset does not contain this definition, but separate
   7.190 +       theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
   7.191 +
   7.192 +primrec 
   7.193 +  upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
   7.194 +    upt_0: "[i..<0] = []"
   7.195 +  | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
   7.196 +
   7.197 +primrec
   7.198 +  distinct :: "'a list \<Rightarrow> bool" where
   7.199 +    "distinct [] \<longleftrightarrow> True"
   7.200 +  | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
   7.201 +
   7.202 +primrec
   7.203 +  remdups :: "'a list \<Rightarrow> 'a list" where
   7.204 +    "remdups [] = []"
   7.205 +  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
   7.206 +
   7.207 +primrec
   7.208 +  remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.209 +    "remove1 x [] = []"
   7.210 +  | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
   7.211 +
   7.212 +primrec
   7.213 +  removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.214 +    "removeAll x [] = []"
   7.215 +  | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
   7.216 +
   7.217 +primrec
   7.218 +  replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   7.219 +    replicate_0: "replicate 0 x = []"
   7.220 +  | replicate_Suc: "replicate (Suc n) x = x # replicate n x"
   7.221  
   7.222  text {*
   7.223    Function @{text size} is overloaded for all datatypes. Users may
   7.224    refer to the list version as @{text length}. *}
   7.225  
   7.226  abbreviation
   7.227 -  length :: "'a list => nat" where
   7.228 -  "length == size"
   7.229 -
   7.230 -primrec
   7.231 -  "hd(x#xs) = x"
   7.232 -
   7.233 -primrec
   7.234 -  "tl([]) = []"
   7.235 -  "tl(x#xs) = xs"
   7.236 -
   7.237 -primrec
   7.238 -  "last(x#xs) = (if xs=[] then x else last xs)"
   7.239 -
   7.240 -primrec
   7.241 -  "butlast []= []"
   7.242 -  "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
   7.243 -
   7.244 -primrec
   7.245 -  "set [] = {}"
   7.246 -  "set (x#xs) = insert x (set xs)"
   7.247 -
   7.248 -primrec
   7.249 -  "map f [] = []"
   7.250 -  "map f (x#xs) = f(x)#map f xs"
   7.251 -
   7.252 -primrec
   7.253 -  append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
   7.254 -where
   7.255 -  append_Nil:"[] @ ys = ys"
   7.256 -  | append_Cons: "(x#xs) @ ys = x # xs @ ys"
   7.257 -
   7.258 -primrec
   7.259 -  "rev([]) = []"
   7.260 -  "rev(x#xs) = rev(xs) @ [x]"
   7.261 -
   7.262 -primrec
   7.263 -  "filter P [] = []"
   7.264 -  "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
   7.265 -
   7.266 -primrec
   7.267 -  foldl_Nil:"foldl f a [] = a"
   7.268 -  foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
   7.269 -
   7.270 -primrec
   7.271 -  "foldr f [] a = a"
   7.272 -  "foldr f (x#xs) a = f x (foldr f xs a)"
   7.273 -
   7.274 -primrec
   7.275 -  "concat([]) = []"
   7.276 -  "concat(x#xs) = x @ concat(xs)"
   7.277 -
   7.278 -primrec
   7.279 -"listsum [] = 0"
   7.280 -"listsum (x # xs) = x + listsum xs"
   7.281 -
   7.282 -primrec
   7.283 -  drop_Nil:"drop n [] = []"
   7.284 -  drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
   7.285 -  -- {*Warning: simpset does not contain this definition, but separate
   7.286 -       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   7.287 -
   7.288 -primrec
   7.289 -  take_Nil:"take n [] = []"
   7.290 -  take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
   7.291 -  -- {*Warning: simpset does not contain this definition, but separate
   7.292 -       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   7.293 -
   7.294 -primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
   7.295 -  nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
   7.296 -  -- {*Warning: simpset does not contain this definition, but separate
   7.297 -       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   7.298 -
   7.299 -primrec
   7.300 -  "[][i:=v] = []"
   7.301 -  "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
   7.302 -
   7.303 -primrec
   7.304 -  "takeWhile P [] = []"
   7.305 -  "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
   7.306 -
   7.307 -primrec
   7.308 -  "dropWhile P [] = []"
   7.309 -  "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
   7.310 -
   7.311 -primrec
   7.312 -  "zip xs [] = []"
   7.313 -  zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
   7.314 -  -- {*Warning: simpset does not contain this definition, but separate
   7.315 -       theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
   7.316 -
   7.317 -primrec
   7.318 -  upt_0: "[i..<0] = []"
   7.319 -  upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
   7.320 -
   7.321 -primrec
   7.322 -  "distinct [] = True"
   7.323 -  "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
   7.324 -
   7.325 -primrec
   7.326 -  "remdups [] = []"
   7.327 -  "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
   7.328 -
   7.329 -primrec
   7.330 -  "remove1 x [] = []"
   7.331 -  "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
   7.332 -
   7.333 -primrec
   7.334 -  "removeAll x [] = []"
   7.335 -  "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
   7.336 -
   7.337 -primrec
   7.338 -  replicate_0: "replicate 0 x = []"
   7.339 -  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
   7.340 +  length :: "'a list \<Rightarrow> nat" where
   7.341 +  "length \<equiv> size"
   7.342  
   7.343  definition
   7.344    rotate1 :: "'a list \<Rightarrow> 'a list" where
   7.345 @@ -210,8 +208,9 @@
   7.346    "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   7.347  
   7.348  primrec
   7.349 -  "splice [] ys = ys"
   7.350 -  "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
   7.351 +  splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   7.352 +    "splice [] ys = ys"
   7.353 +  | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"
   7.354      -- {*Warning: simpset does not contain the second eqn but a derived one. *}
   7.355  
   7.356  text{*
   7.357 @@ -2435,8 +2434,8 @@
   7.358    "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   7.359  
   7.360  translations -- {* Beware of argument permutation! *}
   7.361 -  "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
   7.362 -  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
   7.363 +  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   7.364 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   7.365  
   7.366  lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   7.367    by (induct xs) (simp_all add: left_distrib)
   7.368 @@ -3532,10 +3531,9 @@
   7.369  text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
   7.370  @{term A} and tail drawn from @{term Xs}.*}
   7.371  
   7.372 -constdefs
   7.373 -  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
   7.374 -  "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
   7.375 -declare set_Cons_def [code del]
   7.376 +definition
   7.377 +  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
   7.378 +  [code del]: "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
   7.379  
   7.380  lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
   7.381  by (auto simp add: set_Cons_def)
   7.382 @@ -3543,10 +3541,10 @@
   7.383  text{*Yields the set of lists, all of the same length as the argument and
   7.384  with elements drawn from the corresponding element of the argument.*}
   7.385  
   7.386 -consts  listset :: "'a set list \<Rightarrow> 'a list set"
   7.387  primrec
   7.388 -   "listset []    = {[]}"
   7.389 -   "listset(A#As) = set_Cons A (listset As)"
   7.390 +  listset :: "'a set list \<Rightarrow> 'a list set" where
   7.391 +     "listset [] = {[]}"
   7.392 +  |  "listset (A # As) = set_Cons A (listset As)"
   7.393  
   7.394  
   7.395  subsection{*Relations on Lists*}
   7.396 @@ -3555,26 +3553,21 @@
   7.397  
   7.398  text{*These orderings preserve well-foundedness: shorter lists 
   7.399    precede longer lists. These ordering are not used in dictionaries.*}
   7.400 -
   7.401 -consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
   7.402 -        --{*The lexicographic ordering for lists of the specified length*}
   7.403 -primrec
   7.404 -  "lexn r 0 = {}"
   7.405 -  "lexn r (Suc n) =
   7.406 -    (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
   7.407 -    {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
   7.408 -
   7.409 -constdefs
   7.410 -  lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
   7.411 -    "lex r == \<Union>n. lexn r n"
   7.412 -        --{*Holds only between lists of the same length*}
   7.413 -
   7.414 -  lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
   7.415 -    "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
   7.416 -        --{*Compares lists by their length and then lexicographically*}
   7.417 -
   7.418 -declare lex_def [code del]
   7.419 -
   7.420 +        
   7.421 +primrec -- {*The lexicographic ordering for lists of the specified length*}
   7.422 +  lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
   7.423 +    "lexn r 0 = {}"
   7.424 +  | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
   7.425 +      {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
   7.426 +
   7.427 +definition
   7.428 +  lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   7.429 +  [code del]: "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
   7.430 +
   7.431 +definition
   7.432 +  lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
   7.433 +  [code del]: "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
   7.434 +        -- {*Compares lists by their length and then lexicographically*}
   7.435  
   7.436  lemma wf_lexn: "wf r ==> wf (lexn r n)"
   7.437  apply (induct n, simp, simp)
   7.438 @@ -3645,11 +3638,10 @@
   7.439      This ordering does \emph{not} preserve well-foundedness.
   7.440       Author: N. Voelker, March 2005. *} 
   7.441  
   7.442 -constdefs 
   7.443 -  lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
   7.444 -  "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
   7.445 +definition
   7.446 +  lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   7.447 +  [code del]: "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
   7.448              (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
   7.449 -declare lexord_def [code del]
   7.450  
   7.451  lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
   7.452  by (unfold lexord_def, induct_tac y, auto) 
     8.1 --- a/src/HOL/Map.thy	Sat Jan 16 17:15:27 2010 +0100
     8.2 +++ b/src/HOL/Map.thy	Sat Jan 16 17:15:28 2010 +0100
     8.3 @@ -51,10 +51,6 @@
     8.4    map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
     8.5    "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"
     8.6  
     8.7 -consts
     8.8 -  map_of :: "('a * 'b) list => 'a ~=> 'b"
     8.9 -  map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    8.10 -
    8.11  nonterminals
    8.12    maplets maplet
    8.13  
    8.14 @@ -73,25 +69,27 @@
    8.15  translations
    8.16    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    8.17    "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    8.18 -  "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    8.19    "_Map ms"                     == "_MapUpd (CONST empty) ms"
    8.20    "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    8.21    "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    8.22  
    8.23  primrec
    8.24 -  "map_of [] = empty"
    8.25 -  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    8.26 +  map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
    8.27 +    "map_of [] = empty"
    8.28 +  | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
    8.29  
    8.30 -declare map_of.simps [code del]
    8.31 +definition
    8.32 +  map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where
    8.33 +  "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
    8.34 +
    8.35 +translations
    8.36 +  "_MapUpd m (_maplets x y)"    == "CONST map_upds m x y"
    8.37  
    8.38  lemma map_of_Cons_code [code]: 
    8.39    "map_of [] k = None"
    8.40    "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
    8.41    by simp_all
    8.42  
    8.43 -defs
    8.44 -  map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    8.45 -
    8.46  
    8.47  subsection {* @{term [source] empty} *}
    8.48  
     9.1 --- a/src/HOLCF/Fix.thy	Sat Jan 16 17:15:27 2010 +0100
     9.2 +++ b/src/HOLCF/Fix.thy	Sat Jan 16 17:15:28 2010 +0100
     9.3 @@ -12,12 +12,9 @@
     9.4  
     9.5  subsection {* Iteration *}
     9.6  
     9.7 -consts
     9.8 -  iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)"
     9.9 -
    9.10 -primrec
    9.11 -  "iterate 0 = (\<Lambda> F x. x)"
    9.12 -  "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
    9.13 +primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
    9.14 +    "iterate 0 = (\<Lambda> F x. x)"
    9.15 +  | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
    9.16  
    9.17  text {* Derive inductive properties of iterate from primitive recursion *}
    9.18  
    10.1 --- a/src/HOLCF/Up.thy	Sat Jan 16 17:15:27 2010 +0100
    10.2 +++ b/src/HOLCF/Up.thy	Sat Jan 16 17:15:28 2010 +0100
    10.3 @@ -17,12 +17,9 @@
    10.4  syntax (xsymbols)
    10.5    "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
    10.6  
    10.7 -consts
    10.8 -  Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
    10.9 -
   10.10 -primrec
   10.11 -  "Ifup f Ibottom = \<bottom>"
   10.12 -  "Ifup f (Iup x) = f\<cdot>x"
   10.13 +primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
   10.14 +    "Ifup f Ibottom = \<bottom>"
   10.15 + |  "Ifup f (Iup x) = f\<cdot>x"
   10.16  
   10.17  subsection {* Ordering on lifted cpo *}
   10.18  
    11.1 --- a/src/HOLCF/ex/Stream.thy	Sat Jan 16 17:15:27 2010 +0100
    11.2 +++ b/src/HOLCF/ex/Stream.thy	Sat Jan 16 17:15:28 2010 +0100
    11.3 @@ -550,8 +550,7 @@
    11.4  (* ----------------------------------------------------------------------- *)
    11.5  
    11.6  lemma i_rt_UU [simp]: "i_rt n UU = UU"
    11.7 -apply (simp add: i_rt_def)
    11.8 -by (rule iterate.induct,auto)
    11.9 +  by (induct n) (simp_all add: i_rt_def)
   11.10  
   11.11  lemma i_rt_0 [simp]: "i_rt 0 s = s"
   11.12  by (simp add: i_rt_def)