1.1 --- a/src/HOL/Bali/Table.thy Thu Jan 21 12:18:41 2010 +0100
1.2 +++ b/src/HOL/Bali/Table.thy Thu Jan 21 12:20:28 2010 +0100
1.3 @@ -1,5 +1,4 @@
1.4 (* Title: HOL/Bali/Table.thy
1.5 - ID: $Id$
1.6 Author: David von Oheimb
1.7 *)
1.8 header {* Abstract tables and their implementation as lists *}
1.9 @@ -41,9 +40,10 @@
1.10 syntax
1.11 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
1.12
1.13 +abbreviation
1.14 + "table_of \<equiv> map_of"
1.15 +
1.16 translations
1.17 - "table_of" == "map_of"
1.18 -
1.19 (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
1.20 (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
1.21
2.1 --- a/src/HOL/Deriv.thy Thu Jan 21 12:18:41 2010 +0100
2.2 +++ b/src/HOL/Deriv.thy Thu Jan 21 12:20:28 2010 +0100
2.3 @@ -19,14 +19,13 @@
2.4 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
2.5 "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
2.6
2.7 -consts
2.8 - Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
2.9 primrec
2.10 - "Bolzano_bisect P a b 0 = (a,b)"
2.11 - "Bolzano_bisect P a b (Suc n) =
2.12 - (let (x,y) = Bolzano_bisect P a b n
2.13 - in if P(x, (x+y)/2) then ((x+y)/2, y)
2.14 - else (x, (x+y)/2))"
2.15 + Bolzano_bisect :: "(real \<times> real \<Rightarrow> bool) \<Rightarrow> real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real \<times> real" where
2.16 + "Bolzano_bisect P a b 0 = (a, b)"
2.17 + | "Bolzano_bisect P a b (Suc n) =
2.18 + (let (x, y) = Bolzano_bisect P a b n
2.19 + in if P (x, (x+y) / 2) then ((x+y)/2, y)
2.20 + else (x, (x+y)/2))"
2.21
2.22
2.23 subsection {* Derivatives *}
3.1 --- a/src/HOL/Hoare/HoareAbort.thy Thu Jan 21 12:18:41 2010 +0100
3.2 +++ b/src/HOL/Hoare/HoareAbort.thy Thu Jan 21 12:20:28 2010 +0100
3.3 @@ -1,5 +1,4 @@
3.4 (* Title: HOL/Hoare/HoareAbort.thy
3.5 - ID: $Id$
3.6 Author: Leonor Prensa Nieto & Tobias Nipkow
3.7 Copyright 2003 TUM
3.8
3.9 @@ -261,7 +260,7 @@
3.10 array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70,65] 61)
3.11 translations
3.12 "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
3.13 - "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := list_update a i v)"
3.14 + "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
3.15 (* reverse translation not possible because of duplicate "a" *)
3.16
3.17 text{* Note: there is no special syntax for guarded array access. Thus
4.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Thu Jan 21 12:18:41 2010 +0100
4.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Thu Jan 21 12:20:28 2010 +0100
4.3 @@ -72,7 +72,7 @@
4.4 "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
4.5 "_PAR ps" \<rightleftharpoons> "Parallel ps"
4.6
4.7 - "_prg_scheme j i k c q" \<rightleftharpoons> "map (\<lambda>i. (Some c, q)) [j..<k]"
4.8 + "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]"
4.9
4.10 print_translation {*
4.11 let
5.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Thu Jan 21 12:18:41 2010 +0100
5.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Thu Jan 21 12:20:28 2010 +0100
5.3 @@ -43,7 +43,7 @@
5.4 "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs" ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57)
5.5
5.6 translations
5.7 - "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])"
5.8 + "_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])"
5.9
5.10 text {* Translations for variables before and after a transition: *}
5.11
6.1 --- a/src/HOL/Library/Coinductive_List.thy Thu Jan 21 12:18:41 2010 +0100
6.2 +++ b/src/HOL/Library/Coinductive_List.thy Thu Jan 21 12:20:28 2010 +0100
6.3 @@ -53,15 +53,14 @@
6.4 qed
6.5 qed
6.6
6.7 -consts
6.8 +primrec
6.9 LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
6.10 - 'a \<Rightarrow> 'b Datatype.item"
6.11 -primrec
6.12 - "LList_corec_aux 0 f x = {}"
6.13 - "LList_corec_aux (Suc k) f x =
6.14 - (case f x of
6.15 - None \<Rightarrow> NIL
6.16 - | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
6.17 + 'a \<Rightarrow> 'b Datatype.item" where
6.18 + "LList_corec_aux 0 f x = {}"
6.19 + | "LList_corec_aux (Suc k) f x =
6.20 + (case f x of
6.21 + None \<Rightarrow> NIL
6.22 + | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
6.23
6.24 definition "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
6.25
7.1 --- a/src/HOL/Library/Infinite_Set.thy Thu Jan 21 12:18:41 2010 +0100
7.2 +++ b/src/HOL/Library/Infinite_Set.thy Thu Jan 21 12:20:28 2010 +0100
7.3 @@ -530,11 +530,9 @@
7.4 The set's element type must be wellordered (e.g. the natural numbers).
7.5 *}
7.6
7.7 -consts
7.8 - enumerate :: "'a::wellorder set => (nat => 'a::wellorder)"
7.9 -primrec
7.10 - enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
7.11 - enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
7.12 +primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
7.13 + enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
7.14 + | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
7.15
7.16 lemma enumerate_Suc':
7.17 "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
8.1 --- a/src/HOL/Library/Nested_Environment.thy Thu Jan 21 12:18:41 2010 +0100
8.2 +++ b/src/HOL/Library/Nested_Environment.thy Thu Jan 21 12:20:28 2010 +0100
8.3 @@ -43,18 +43,16 @@
8.4 @{term None}.
8.5 *}
8.6
8.7 -consts
8.8 +primrec
8.9 lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
8.10 - lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
8.11 -
8.12 -primrec (lookup)
8.13 - "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
8.14 - "lookup (Env b es) xs =
8.15 - (case xs of
8.16 - [] => Some (Env b es)
8.17 - | y # ys => lookup_option (es y) ys)"
8.18 - "lookup_option None xs = None"
8.19 - "lookup_option (Some e) xs = lookup e xs"
8.20 + and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
8.21 + "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
8.22 + | "lookup (Env b es) xs =
8.23 + (case xs of
8.24 + [] => Some (Env b es)
8.25 + | y # ys => lookup_option (es y) ys)"
8.26 + | "lookup_option None xs = None"
8.27 + | "lookup_option (Some e) xs = lookup e xs"
8.28
8.29 hide const lookup_option
8.30
8.31 @@ -76,7 +74,7 @@
8.32 | Some e => lookup e xs)"
8.33 by (cases "es x") simp_all
8.34
8.35 -lemmas lookup.simps [simp del]
8.36 +lemmas lookup_lookup_option.simps [simp del]
8.37 and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
8.38
8.39 theorem lookup_eq:
8.40 @@ -247,24 +245,22 @@
8.41 environment is left unchanged.
8.42 *}
8.43
8.44 -consts
8.45 +primrec
8.46 update :: "'c list => ('a, 'b, 'c) env option
8.47 => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
8.48 - update_option :: "'c list => ('a, 'b, 'c) env option
8.49 - => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
8.50 -
8.51 -primrec (update)
8.52 - "update xs opt (Val a) =
8.53 - (if xs = [] then (case opt of None => Val a | Some e => e)
8.54 - else Val a)"
8.55 - "update xs opt (Env b es) =
8.56 - (case xs of
8.57 - [] => (case opt of None => Env b es | Some e => e)
8.58 - | y # ys => Env b (es (y := update_option ys opt (es y))))"
8.59 - "update_option xs opt None =
8.60 - (if xs = [] then opt else None)"
8.61 - "update_option xs opt (Some e) =
8.62 - (if xs = [] then opt else Some (update xs opt e))"
8.63 + and update_option :: "'c list => ('a, 'b, 'c) env option
8.64 + => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
8.65 + "update xs opt (Val a) =
8.66 + (if xs = [] then (case opt of None => Val a | Some e => e)
8.67 + else Val a)"
8.68 + | "update xs opt (Env b es) =
8.69 + (case xs of
8.70 + [] => (case opt of None => Env b es | Some e => e)
8.71 + | y # ys => Env b (es (y := update_option ys opt (es y))))"
8.72 + | "update_option xs opt None =
8.73 + (if xs = [] then opt else None)"
8.74 + | "update_option xs opt (Some e) =
8.75 + (if xs = [] then opt else Some (update xs opt e))"
8.76
8.77 hide const update_option
8.78
8.79 @@ -294,7 +290,7 @@
8.80 | Some e => Some (update (y # ys) opt e))))"
8.81 by (cases "es x") simp_all
8.82
8.83 -lemmas update.simps [simp del]
8.84 +lemmas update_update_option.simps [simp del]
8.85 and update_simps [simp] = update_nil_none update_nil_some
8.86 update_cons_val update_cons_nil_env update_cons_cons_env
8.87
9.1 --- a/src/HOL/Library/Ramsey.thy Thu Jan 21 12:18:41 2010 +0100
9.2 +++ b/src/HOL/Library/Ramsey.thy Thu Jan 21 12:20:28 2010 +0100
9.3 @@ -12,13 +12,10 @@
9.4
9.5 subsubsection {* ``Axiom'' of Dependent Choice *}
9.6
9.7 -consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
9.8 +primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
9.9 --{*An integer-indexed chain of choices*}
9.10 -primrec
9.11 - choice_0: "choice P r 0 = (SOME x. P x)"
9.12 -
9.13 - choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
9.14 -
9.15 + choice_0: "choice P r 0 = (SOME x. P x)"
9.16 + | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
9.17
9.18 lemma choice_n:
9.19 assumes P0: "P x0"
10.1 --- a/src/HOL/Library/Word.thy Thu Jan 21 12:18:41 2010 +0100
10.2 +++ b/src/HOL/Library/Word.thy Thu Jan 21 12:20:28 2010 +0100
10.3 @@ -43,11 +43,21 @@
10.4 "bitval \<zero> = 0"
10.5 | "bitval \<one> = 1"
10.6
10.7 -consts
10.8 - bitnot :: "bit => bit"
10.9 - bitand :: "bit => bit => bit" (infixr "bitand" 35)
10.10 - bitor :: "bit => bit => bit" (infixr "bitor" 30)
10.11 - bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
10.12 +primrec bitnot :: "bit => bit" where
10.13 + bitnot_zero: "(bitnot \<zero>) = \<one>"
10.14 + | bitnot_one : "(bitnot \<one>) = \<zero>"
10.15 +
10.16 +primrec bitand :: "bit => bit => bit" (infixr "bitand" 35) where
10.17 + bitand_zero: "(\<zero> bitand y) = \<zero>"
10.18 + | bitand_one: "(\<one> bitand y) = y"
10.19 +
10.20 +primrec bitor :: "bit => bit => bit" (infixr "bitor" 30) where
10.21 + bitor_zero: "(\<zero> bitor y) = y"
10.22 + | bitor_one: "(\<one> bitor y) = \<one>"
10.23 +
10.24 +primrec bitxor :: "bit => bit => bit" (infixr "bitxor" 30) where
10.25 + bitxor_zero: "(\<zero> bitxor y) = y"
10.26 + | bitxor_one: "(\<one> bitxor y) = (bitnot y)"
10.27
10.28 notation (xsymbols)
10.29 bitnot ("\<not>\<^sub>b _" [40] 40) and
10.30 @@ -61,22 +71,6 @@
10.31 bitor (infixr "\<or>\<^sub>b" 30) and
10.32 bitxor (infixr "\<oplus>\<^sub>b" 30)
10.33
10.34 -primrec
10.35 - bitnot_zero: "(bitnot \<zero>) = \<one>"
10.36 - bitnot_one : "(bitnot \<one>) = \<zero>"
10.37 -
10.38 -primrec
10.39 - bitand_zero: "(\<zero> bitand y) = \<zero>"
10.40 - bitand_one: "(\<one> bitand y) = y"
10.41 -
10.42 -primrec
10.43 - bitor_zero: "(\<zero> bitor y) = y"
10.44 - bitor_one: "(\<one> bitor y) = \<one>"
10.45 -
10.46 -primrec
10.47 - bitxor_zero: "(\<zero> bitxor y) = y"
10.48 - bitxor_one: "(\<one> bitxor y) = (bitnot y)"
10.49 -
10.50 lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
10.51 by (cases b) simp_all
10.52
10.53 @@ -244,11 +238,9 @@
10.54 finally show "bv_extend n b w = bv_extend n b (b#w)" .
10.55 qed
10.56
10.57 -consts
10.58 - rem_initial :: "bit => bit list => bit list"
10.59 -primrec
10.60 - "rem_initial b [] = []"
10.61 - "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
10.62 +primrec rem_initial :: "bit => bit list => bit list" where
10.63 + "rem_initial b [] = []"
10.64 + | "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
10.65
10.66 lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
10.67 by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
10.68 @@ -808,14 +800,12 @@
10.69
10.70 subsection {* Signed Vectors *}
10.71
10.72 -consts
10.73 - norm_signed :: "bit list => bit list"
10.74 -primrec
10.75 - norm_signed_Nil: "norm_signed [] = []"
10.76 - norm_signed_Cons: "norm_signed (b#bs) =
10.77 - (case b of
10.78 - \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
10.79 - | \<one> => b#rem_initial b bs)"
10.80 +primrec norm_signed :: "bit list => bit list" where
10.81 + norm_signed_Nil: "norm_signed [] = []"
10.82 + | norm_signed_Cons: "norm_signed (b#bs) =
10.83 + (case b of
10.84 + \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
10.85 + | \<one> => b#rem_initial b bs)"
10.86
10.87 lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
10.88 by simp
10.89 @@ -1005,7 +995,7 @@
10.90 proof (rule bit_list_cases [of w],simp_all)
10.91 fix xs
10.92 show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
10.93 - proof (simp add: norm_signed_list_def,auto)
10.94 + proof (simp add: norm_signed_def,auto)
10.95 assume "norm_unsigned xs = []"
10.96 hence xx: "rem_initial \<zero> xs = []"
10.97 by (simp add: norm_unsigned_def)
10.98 @@ -2232,12 +2222,10 @@
10.99 lemma "nat_to_bv (number_of Int.Pls) = []"
10.100 by simp
10.101
10.102 -consts
10.103 - fast_bv_to_nat_helper :: "[bit list, int] => int"
10.104 -primrec
10.105 - fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
10.106 - fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
10.107 - fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
10.108 +primrec fast_bv_to_nat_helper :: "[bit list, int] => int" where
10.109 + fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
10.110 + | fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
10.111 + fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
10.112
10.113 declare fast_bv_to_nat_helper.simps [code del]
10.114
11.1 --- a/src/HOL/List.thy Thu Jan 21 12:18:41 2010 +0100
11.2 +++ b/src/HOL/List.thy Thu Jan 21 12:20:28 2010 +0100
11.3 @@ -13,184 +13,182 @@
11.4 Nil ("[]")
11.5 | Cons 'a "'a list" (infixr "#" 65)
11.6
11.7 -subsection{*Basic list processing functions*}
11.8 -
11.9 -consts
11.10 - filter:: "('a => bool) => 'a list => 'a list"
11.11 - concat:: "'a list list => 'a list"
11.12 - foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
11.13 - foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
11.14 - hd:: "'a list => 'a"
11.15 - tl:: "'a list => 'a list"
11.16 - last:: "'a list => 'a"
11.17 - butlast :: "'a list => 'a list"
11.18 - set :: "'a list => 'a set"
11.19 - map :: "('a=>'b) => ('a list => 'b list)"
11.20 - listsum :: "'a list => 'a::monoid_add"
11.21 - list_update :: "'a list => nat => 'a => 'a list"
11.22 - take:: "nat => 'a list => 'a list"
11.23 - drop:: "nat => 'a list => 'a list"
11.24 - takeWhile :: "('a => bool) => 'a list => 'a list"
11.25 - dropWhile :: "('a => bool) => 'a list => 'a list"
11.26 - rev :: "'a list => 'a list"
11.27 - zip :: "'a list => 'b list => ('a * 'b) list"
11.28 - upt :: "nat => nat => nat list" ("(1[_..</_'])")
11.29 - remdups :: "'a list => 'a list"
11.30 - remove1 :: "'a => 'a list => 'a list"
11.31 - removeAll :: "'a => 'a list => 'a list"
11.32 - "distinct":: "'a list => bool"
11.33 - replicate :: "nat => 'a => 'a list"
11.34 - splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
11.35 -
11.36 -
11.37 -nonterminals lupdbinds lupdbind
11.38 -
11.39 syntax
11.40 -- {* list Enumeration *}
11.41 "@list" :: "args => 'a list" ("[(_)]")
11.42
11.43 +translations
11.44 + "[x, xs]" == "x#[xs]"
11.45 + "[x]" == "x#[]"
11.46 +
11.47 +subsection{*Basic list processing functions*}
11.48 +
11.49 +primrec
11.50 + hd :: "'a list \<Rightarrow> 'a" where
11.51 + "hd (x # xs) = x"
11.52 +
11.53 +primrec
11.54 + tl :: "'a list \<Rightarrow> 'a list" where
11.55 + "tl [] = []"
11.56 + | "tl (x # xs) = xs"
11.57 +
11.58 +primrec
11.59 + last :: "'a list \<Rightarrow> 'a" where
11.60 + "last (x # xs) = (if xs = [] then x else last xs)"
11.61 +
11.62 +primrec
11.63 + butlast :: "'a list \<Rightarrow> 'a list" where
11.64 + "butlast []= []"
11.65 + | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
11.66 +
11.67 +primrec
11.68 + set :: "'a list \<Rightarrow> 'a set" where
11.69 + "set [] = {}"
11.70 + | "set (x # xs) = insert x (set xs)"
11.71 +
11.72 +primrec
11.73 + map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
11.74 + "map f [] = []"
11.75 + | "map f (x # xs) = f x # map f xs"
11.76 +
11.77 +primrec
11.78 + append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
11.79 + append_Nil:"[] @ ys = ys"
11.80 + | append_Cons: "(x#xs) @ ys = x # xs @ ys"
11.81 +
11.82 +primrec
11.83 + rev :: "'a list \<Rightarrow> 'a list" where
11.84 + "rev [] = []"
11.85 + | "rev (x # xs) = rev xs @ [x]"
11.86 +
11.87 +primrec
11.88 + filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.89 + "filter P [] = []"
11.90 + | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
11.91 +
11.92 +syntax
11.93 -- {* Special syntax for filter *}
11.94 "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
11.95
11.96 - -- {* list update *}
11.97 +translations
11.98 + "[x<-xs . P]"== "CONST filter (%x. P) xs"
11.99 +
11.100 +syntax (xsymbols)
11.101 + "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
11.102 +syntax (HTML output)
11.103 + "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
11.104 +
11.105 +primrec
11.106 + foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
11.107 + foldl_Nil: "foldl f a [] = a"
11.108 + | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
11.109 +
11.110 +primrec
11.111 + foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
11.112 + "foldr f [] a = a"
11.113 + | "foldr f (x # xs) a = f x (foldr f xs a)"
11.114 +
11.115 +primrec
11.116 + concat:: "'a list list \<Rightarrow> 'a list" where
11.117 + "concat [] = []"
11.118 + | "concat (x # xs) = x @ concat xs"
11.119 +
11.120 +primrec (in monoid_add)
11.121 + listsum :: "'a list \<Rightarrow> 'a" where
11.122 + "listsum [] = 0"
11.123 + | "listsum (x # xs) = x + listsum xs"
11.124 +
11.125 +primrec
11.126 + drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.127 + drop_Nil: "drop n [] = []"
11.128 + | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
11.129 + -- {*Warning: simpset does not contain this definition, but separate
11.130 + theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
11.131 +
11.132 +primrec
11.133 + take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.134 + take_Nil:"take n [] = []"
11.135 + | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
11.136 + -- {*Warning: simpset does not contain this definition, but separate
11.137 + theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
11.138 +
11.139 +primrec
11.140 + nth :: "'a list => nat => 'a" (infixl "!" 100) where
11.141 + nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
11.142 + -- {*Warning: simpset does not contain this definition, but separate
11.143 + theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
11.144 +
11.145 +primrec
11.146 + list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
11.147 + "list_update [] i v = []"
11.148 + | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
11.149 +
11.150 +nonterminals lupdbinds lupdbind
11.151 +
11.152 +syntax
11.153 "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
11.154 "" :: "lupdbind => lupdbinds" ("_")
11.155 "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
11.156 "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
11.157
11.158 translations
11.159 - "[x, xs]" == "x#[xs]"
11.160 - "[x]" == "x#[]"
11.161 - "[x<-xs . P]"== "filter (%x. P) xs"
11.162 -
11.163 "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
11.164 - "xs[i:=x]" == "list_update xs i x"
11.165 -
11.166 -
11.167 -syntax (xsymbols)
11.168 - "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
11.169 -syntax (HTML output)
11.170 - "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
11.171 -
11.172 + "xs[i:=x]" == "CONST list_update xs i x"
11.173 +
11.174 +primrec
11.175 + takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.176 + "takeWhile P [] = []"
11.177 + | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
11.178 +
11.179 +primrec
11.180 + dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.181 + "dropWhile P [] = []"
11.182 + | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
11.183 +
11.184 +primrec
11.185 + zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
11.186 + "zip xs [] = []"
11.187 + | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
11.188 + -- {*Warning: simpset does not contain this definition, but separate
11.189 + theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
11.190 +
11.191 +primrec
11.192 + upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
11.193 + upt_0: "[i..<0] = []"
11.194 + | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
11.195 +
11.196 +primrec
11.197 + distinct :: "'a list \<Rightarrow> bool" where
11.198 + "distinct [] \<longleftrightarrow> True"
11.199 + | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
11.200 +
11.201 +primrec
11.202 + remdups :: "'a list \<Rightarrow> 'a list" where
11.203 + "remdups [] = []"
11.204 + | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
11.205 +
11.206 +primrec
11.207 + remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.208 + "remove1 x [] = []"
11.209 + | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
11.210 +
11.211 +primrec
11.212 + removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.213 + "removeAll x [] = []"
11.214 + | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
11.215 +
11.216 +primrec
11.217 + replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
11.218 + replicate_0: "replicate 0 x = []"
11.219 + | replicate_Suc: "replicate (Suc n) x = x # replicate n x"
11.220
11.221 text {*
11.222 Function @{text size} is overloaded for all datatypes. Users may
11.223 refer to the list version as @{text length}. *}
11.224
11.225 abbreviation
11.226 - length :: "'a list => nat" where
11.227 - "length == size"
11.228 -
11.229 -primrec
11.230 - "hd(x#xs) = x"
11.231 -
11.232 -primrec
11.233 - "tl([]) = []"
11.234 - "tl(x#xs) = xs"
11.235 -
11.236 -primrec
11.237 - "last(x#xs) = (if xs=[] then x else last xs)"
11.238 -
11.239 -primrec
11.240 - "butlast []= []"
11.241 - "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
11.242 -
11.243 -primrec
11.244 - "set [] = {}"
11.245 - "set (x#xs) = insert x (set xs)"
11.246 -
11.247 -primrec
11.248 - "map f [] = []"
11.249 - "map f (x#xs) = f(x)#map f xs"
11.250 -
11.251 -primrec
11.252 - append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
11.253 -where
11.254 - append_Nil:"[] @ ys = ys"
11.255 - | append_Cons: "(x#xs) @ ys = x # xs @ ys"
11.256 -
11.257 -primrec
11.258 - "rev([]) = []"
11.259 - "rev(x#xs) = rev(xs) @ [x]"
11.260 -
11.261 -primrec
11.262 - "filter P [] = []"
11.263 - "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
11.264 -
11.265 -primrec
11.266 - foldl_Nil:"foldl f a [] = a"
11.267 - foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
11.268 -
11.269 -primrec
11.270 - "foldr f [] a = a"
11.271 - "foldr f (x#xs) a = f x (foldr f xs a)"
11.272 -
11.273 -primrec
11.274 - "concat([]) = []"
11.275 - "concat(x#xs) = x @ concat(xs)"
11.276 -
11.277 -primrec
11.278 -"listsum [] = 0"
11.279 -"listsum (x # xs) = x + listsum xs"
11.280 -
11.281 -primrec
11.282 - drop_Nil:"drop n [] = []"
11.283 - drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
11.284 - -- {*Warning: simpset does not contain this definition, but separate
11.285 - theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
11.286 -
11.287 -primrec
11.288 - take_Nil:"take n [] = []"
11.289 - take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
11.290 - -- {*Warning: simpset does not contain this definition, but separate
11.291 - theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
11.292 -
11.293 -primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
11.294 - nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
11.295 - -- {*Warning: simpset does not contain this definition, but separate
11.296 - theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
11.297 -
11.298 -primrec
11.299 - "[][i:=v] = []"
11.300 - "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
11.301 -
11.302 -primrec
11.303 - "takeWhile P [] = []"
11.304 - "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
11.305 -
11.306 -primrec
11.307 - "dropWhile P [] = []"
11.308 - "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
11.309 -
11.310 -primrec
11.311 - "zip xs [] = []"
11.312 - zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
11.313 - -- {*Warning: simpset does not contain this definition, but separate
11.314 - theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
11.315 -
11.316 -primrec
11.317 - upt_0: "[i..<0] = []"
11.318 - upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
11.319 -
11.320 -primrec
11.321 - "distinct [] = True"
11.322 - "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
11.323 -
11.324 -primrec
11.325 - "remdups [] = []"
11.326 - "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
11.327 -
11.328 -primrec
11.329 - "remove1 x [] = []"
11.330 - "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
11.331 -
11.332 -primrec
11.333 - "removeAll x [] = []"
11.334 - "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
11.335 -
11.336 -primrec
11.337 - replicate_0: "replicate 0 x = []"
11.338 - replicate_Suc: "replicate (Suc n) x = x # replicate n x"
11.339 + length :: "'a list \<Rightarrow> nat" where
11.340 + "length \<equiv> size"
11.341
11.342 definition
11.343 rotate1 :: "'a list \<Rightarrow> 'a list" where
11.344 @@ -210,8 +208,9 @@
11.345 "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
11.346
11.347 primrec
11.348 - "splice [] ys = ys"
11.349 - "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
11.350 + splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
11.351 + "splice [] ys = ys"
11.352 + | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"
11.353 -- {*Warning: simpset does not contain the second eqn but a derived one. *}
11.354
11.355 text{*
11.356 @@ -2434,8 +2433,8 @@
11.357 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
11.358
11.359 translations -- {* Beware of argument permutation! *}
11.360 - "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
11.361 - "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
11.362 + "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
11.363 + "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
11.364
11.365 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
11.366 by (induct xs) (simp_all add: left_distrib)
11.367 @@ -3827,10 +3826,9 @@
11.368 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
11.369 @{term A} and tail drawn from @{term Xs}.*}
11.370
11.371 -constdefs
11.372 - set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
11.373 - "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
11.374 -declare set_Cons_def [code del]
11.375 +definition
11.376 + set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
11.377 + [code del]: "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
11.378
11.379 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
11.380 by (auto simp add: set_Cons_def)
11.381 @@ -3838,10 +3836,11 @@
11.382 text{*Yields the set of lists, all of the same length as the argument and
11.383 with elements drawn from the corresponding element of the argument.*}
11.384
11.385 -consts listset :: "'a set list \<Rightarrow> 'a list set"
11.386 primrec
11.387 - "listset [] = {[]}"
11.388 - "listset(A#As) = set_Cons A (listset As)"
11.389 + listset :: "'a set list \<Rightarrow> 'a list set" where
11.390 + "listset [] = {[]}"
11.391 + | "listset (A # As) = set_Cons A (listset As)"
11.392 +
11.393
11.394 subsection{*Relations on Lists*}
11.395
11.396 @@ -3849,26 +3848,21 @@
11.397
11.398 text{*These orderings preserve well-foundedness: shorter lists
11.399 precede longer lists. These ordering are not used in dictionaries.*}
11.400 -
11.401 -consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
11.402 - --{*The lexicographic ordering for lists of the specified length*}
11.403 -primrec
11.404 - "lexn r 0 = {}"
11.405 - "lexn r (Suc n) =
11.406 - (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
11.407 - {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
11.408 -
11.409 -constdefs
11.410 - lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
11.411 - "lex r == \<Union>n. lexn r n"
11.412 - --{*Holds only between lists of the same length*}
11.413 -
11.414 - lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
11.415 - "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
11.416 - --{*Compares lists by their length and then lexicographically*}
11.417 -
11.418 -declare lex_def [code del]
11.419 -
11.420 +
11.421 +primrec -- {*The lexicographic ordering for lists of the specified length*}
11.422 + lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
11.423 + "lexn r 0 = {}"
11.424 + | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
11.425 + {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
11.426 +
11.427 +definition
11.428 + lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
11.429 + [code del]: "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
11.430 +
11.431 +definition
11.432 + lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
11.433 + [code del]: "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
11.434 + -- {*Compares lists by their length and then lexicographically*}
11.435
11.436 lemma wf_lexn: "wf r ==> wf (lexn r n)"
11.437 apply (induct n, simp, simp)
11.438 @@ -3939,11 +3933,10 @@
11.439 This ordering does \emph{not} preserve well-foundedness.
11.440 Author: N. Voelker, March 2005. *}
11.441
11.442 -constdefs
11.443 - lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
11.444 - "lexord r == {(x,y). \<exists> a v. y = x @ a # v \<or>
11.445 +definition
11.446 + lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
11.447 + [code del]: "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
11.448 (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
11.449 -declare lexord_def [code del]
11.450
11.451 lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
11.452 by (unfold lexord_def, induct_tac y, auto)
12.1 --- a/src/HOL/Map.thy Thu Jan 21 12:18:41 2010 +0100
12.2 +++ b/src/HOL/Map.thy Thu Jan 21 12:20:28 2010 +0100
12.3 @@ -51,10 +51,6 @@
12.4 map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50) where
12.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)"
12.6
12.7 -consts
12.8 - map_of :: "('a * 'b) list => 'a ~=> 'b"
12.9 - map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
12.10 -
12.11 nonterminals
12.12 maplets maplet
12.13
12.14 @@ -73,25 +69,27 @@
12.15 translations
12.16 "_MapUpd m (_Maplets xy ms)" == "_MapUpd (_MapUpd m xy) ms"
12.17 "_MapUpd m (_maplet x y)" == "m(x:=Some y)"
12.18 - "_MapUpd m (_maplets x y)" == "map_upds m x y"
12.19 "_Map ms" == "_MapUpd (CONST empty) ms"
12.20 "_Map (_Maplets ms1 ms2)" <= "_MapUpd (_Map ms1) ms2"
12.21 "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
12.22
12.23 primrec
12.24 - "map_of [] = empty"
12.25 - "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
12.26 + map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
12.27 + "map_of [] = empty"
12.28 + | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
12.29
12.30 -declare map_of.simps [code del]
12.31 +definition
12.32 + map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where
12.33 + "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
12.34 +
12.35 +translations
12.36 + "_MapUpd m (_maplets x y)" == "CONST map_upds m x y"
12.37
12.38 lemma map_of_Cons_code [code]:
12.39 "map_of [] k = None"
12.40 "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
12.41 by simp_all
12.42
12.43 -defs
12.44 - map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
12.45 -
12.46
12.47 subsection {* @{term [source] empty} *}
12.48
13.1 --- a/src/HOLCF/Fix.thy Thu Jan 21 12:18:41 2010 +0100
13.2 +++ b/src/HOLCF/Fix.thy Thu Jan 21 12:20:28 2010 +0100
13.3 @@ -12,12 +12,9 @@
13.4
13.5 subsection {* Iteration *}
13.6
13.7 -consts
13.8 - iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)"
13.9 -
13.10 -primrec
13.11 - "iterate 0 = (\<Lambda> F x. x)"
13.12 - "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
13.13 +primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
13.14 + "iterate 0 = (\<Lambda> F x. x)"
13.15 + | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
13.16
13.17 text {* Derive inductive properties of iterate from primitive recursion *}
13.18
14.1 --- a/src/HOLCF/Up.thy Thu Jan 21 12:18:41 2010 +0100
14.2 +++ b/src/HOLCF/Up.thy Thu Jan 21 12:20:28 2010 +0100
14.3 @@ -17,12 +17,9 @@
14.4 syntax (xsymbols)
14.5 "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
14.6
14.7 -consts
14.8 - Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
14.9 -
14.10 -primrec
14.11 - "Ifup f Ibottom = \<bottom>"
14.12 - "Ifup f (Iup x) = f\<cdot>x"
14.13 +primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
14.14 + "Ifup f Ibottom = \<bottom>"
14.15 + | "Ifup f (Iup x) = f\<cdot>x"
14.16
14.17 subsection {* Ordering on lifted cpo *}
14.18
15.1 --- a/src/HOLCF/ex/Stream.thy Thu Jan 21 12:18:41 2010 +0100
15.2 +++ b/src/HOLCF/ex/Stream.thy Thu Jan 21 12:20:28 2010 +0100
15.3 @@ -550,8 +550,7 @@
15.4 (* ----------------------------------------------------------------------- *)
15.5
15.6 lemma i_rt_UU [simp]: "i_rt n UU = UU"
15.7 -apply (simp add: i_rt_def)
15.8 -by (rule iterate.induct,auto)
15.9 + by (induct n) (simp_all add: i_rt_def)
15.10
15.11 lemma i_rt_0 [simp]: "i_rt 0 s = s"
15.12 by (simp add: i_rt_def)