--- a/src/HOL/Bali/Table.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Bali/Table.thy Thu Jan 21 09:27:57 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Bali/Table.thy
- ID: $Id$
Author: David von Oheimb
*)
header {* Abstract tables and their implementation as lists *}
@@ -41,9 +40,10 @@
syntax
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
+abbreviation
+ "table_of \<equiv> map_of"
+
translations
- "table_of" == "map_of"
-
(type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
(type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
--- a/src/HOL/Deriv.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Deriv.thy Thu Jan 21 09:27:57 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 *}
--- a/src/HOL/Hoare/HoareAbort.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Thu Jan 21 09:27:57 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/HoareAbort.thy
- ID: $Id$
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 2003 TUM
@@ -261,7 +260,7 @@
array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70,65] 61)
translations
"P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
- "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := list_update a i v)"
+ "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
(* reverse translation not possible because of duplicate "a" *)
text{* Note: there is no special syntax for guarded array access. Thus
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Thu Jan 21 09:27:57 2010 +0100
@@ -72,7 +72,7 @@
"_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
"_PAR ps" \<rightleftharpoons> "Parallel ps"
- "_prg_scheme j i k c q" \<rightleftharpoons> "map (\<lambda>i. (Some c, q)) [j..<k]"
+ "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]"
print_translation {*
let
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Thu Jan 21 09:27:57 2010 +0100
@@ -43,7 +43,7 @@
"_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs" ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57)
translations
- "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])"
+ "_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])"
text {* Translations for variables before and after a transition: *}
--- a/src/HOL/Library/Coinductive_List.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Library/Coinductive_List.thy Thu Jan 21 09:27:57 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)"
--- a/src/HOL/Library/Infinite_Set.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Thu Jan 21 09:27:57 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"
--- a/src/HOL/Library/Nested_Environment.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Library/Nested_Environment.thy Thu Jan 21 09:27:57 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
--- a/src/HOL/Library/Ramsey.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Library/Ramsey.thy Thu Jan 21 09:27:57 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"
--- a/src/HOL/Library/Word.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Library/Word.thy Thu Jan 21 09:27:57 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]
--- a/src/HOL/List.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/List.thy Thu Jan 21 09:27:57 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{*
@@ -2434,8 +2433,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)
@@ -3827,10 +3826,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)
@@ -3838,10 +3836,11 @@
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*}
@@ -3849,26 +3848,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)
@@ -3939,11 +3933,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)
--- a/src/HOL/Map.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOL/Map.thy Thu Jan 21 09:27:57 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} *}
--- a/src/HOLCF/Fix.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOLCF/Fix.thy Thu Jan 21 09:27:57 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 *}
--- a/src/HOLCF/Up.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOLCF/Up.thy Thu Jan 21 09:27:57 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 *}
--- a/src/HOLCF/ex/Stream.thy Wed Jan 20 11:54:19 2010 +0100
+++ b/src/HOLCF/ex/Stream.thy Thu Jan 21 09:27:57 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)