# HG changeset patch
# User nipkow
# Date 870790905 -7200
# Node ID 244daa75f8903cb3f3ab9426273d7913ab34f46c
# Parent  e487bf0ed6c409910d96c64cffa759640a62c8ee
Added function `replicate' and lemmas map_cong and set_replicate.

diff -r e487bf0ed6c4 -r 244daa75f890 src/HOL/List.ML
--- 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];
diff -r e487bf0ed6c4 -r 244daa75f890 src/HOL/List.thy
--- 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