summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 22 Nov 2004 13:52:27 +0100 | |

changeset 15307 | 10dd989282fd |

parent 15306 | 51f3d31e8eea |

child 15308 | 56c830f91b38 |

indentation

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Mon Nov 22 11:54:08 2004 +0100 +++ b/src/HOL/List.thy Mon Nov 22 13:52:27 2004 +0100 @@ -100,93 +100,118 @@ primrec -"hd(x#xs) = x" + "hd(x#xs) = x" + primrec -"tl([]) = []" -"tl(x#xs) = xs" + "tl([]) = []" + "tl(x#xs) = xs" + primrec -"null([]) = True" -"null(x#xs) = False" + "null([]) = True" + "null(x#xs) = False" + primrec -"last(x#xs) = (if xs=[] then x else last xs)" + "last(x#xs) = (if xs=[] then x else last xs)" + primrec -"butlast []= []" -"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" + "butlast []= []" + "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" + primrec -"x mem [] = False" -"x mem (y#ys) = (if y=x then True else x mem ys)" + "x mem [] = False" + "x mem (y#ys) = (if y=x then True else x mem ys)" + primrec -"set [] = {}" -"set (x#xs) = insert x (set xs)" + "set [] = {}" + "set (x#xs) = insert x (set xs)" + primrec -list_all_Nil:"list_all P [] = True" -list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)" -primrec -"map f [] = []" -"map f (x#xs) = f(x)#map f xs" + list_all_Nil:"list_all P [] = True" + list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)" + primrec -append_Nil:"[]@ys = ys" -append_Cons: "(x#xs)@ys = x#(xs@ys)" + "map f [] = []" + "map f (x#xs) = f(x)#map f xs" + primrec -"rev([]) = []" -"rev(x#xs) = rev(xs) @ [x]" + append_Nil:"[]@ys = ys" + append_Cons: "(x#xs)@ys = x#(xs@ys)" + primrec -"filter P [] = []" -"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" + "rev([]) = []" + "rev(x#xs) = rev(xs) @ [x]" + primrec -foldl_Nil:"foldl f a [] = a" -foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" + "filter P [] = []" + "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" + primrec -"foldr f [] a = a" -"foldr f (x#xs) a = f x (foldr f xs a)" + foldl_Nil:"foldl f a [] = a" + foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" + primrec -"concat([]) = []" -"concat(x#xs) = x @ concat(xs)" + "foldr f [] a = a" + "foldr f (x#xs) a = f x (foldr f xs a)" + 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"} *} + "concat([]) = []" + "concat(x#xs) = x @ concat(xs)" + 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"} *} + 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 -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"} *} + 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 -"[][i:=v] = []" -"(x#xs)[i:=v] = -(case i of 0 => v # xs -| Suc j => x # xs[j:=v])" + 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 -"takeWhile P [] = []" -"takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" + "[][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)" + "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"} *} + "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 [])" + 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)" + "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)" + "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)" + "remove1 x [] = []" + "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)" + primrec -replicate_0: "replicate 0 x = []" -replicate_Suc: "replicate (Suc n) x = x # replicate n x" + replicate_0: "replicate 0 x = []" + replicate_Suc: "replicate (Suc n) x = x # replicate n x" + defs rotate1_def: "rotate1 xs == (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])" rotate_def: "rotate n == rotate1 ^ n"