Added function `replicate' and lemmas map_cong and set_replicate.
--- a/src/HOL/List.ML Tue Aug 05 16:14:23 1997 +0200
+++ b/src/HOL/List.ML Tue Aug 05 16:21:45 1997 +0200
@@ -196,6 +196,16 @@
by (ALLGOALS Asm_simp_tac);
qed "rev_map";
+(* a congruence rule for map: *)
+goal thy
+ "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
+by(rtac impI 1);
+by(hyp_subst_tac 1);
+by(induct_tac "ys" 1);
+by(ALLGOALS Asm_simp_tac);
+val lemma = result();
+bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
+
(** rev **)
section "rev";
@@ -617,3 +627,15 @@
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
qed_spec_mp"set_of_list_take_whileD";
+(** replicate **)
+section "replicate";
+
+goal thy "set(replicate (Suc n) x) = {x}";
+by(induct_tac "n" 1);
+by(ALLGOALS Asm_full_simp_tac);
+val lemma = result();
+
+goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";
+by(fast_tac (!claset addSDs [not0_implies_Suc] addSIs [lemma]) 1);
+qed "set_replicate";
+Addsimps [set_replicate];
--- a/src/HOL/List.thy Tue Aug 05 16:14:23 1997 +0200
+++ b/src/HOL/List.thy Tue Aug 05 16:21:45 1997 +0200
@@ -26,6 +26,7 @@
dropWhile :: ('a => bool) => 'a list => 'a list
tl,ttl :: 'a list => 'a list
rev :: 'a list => 'a list
+ replicate :: nat => 'a => 'a list
syntax
(* list Enumeration *)
@@ -109,6 +110,9 @@
primrec dropWhile list
"dropWhile P [] = []"
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
+primrec replicate nat
+replicate_0 "replicate 0 x = []"
+replicate_Suc "replicate (Suc n) x = x # replicate n x"
end