Added function `replicate' and lemmas map_cong and set_replicate.
authornipkow
Tue Aug 05 16:21:45 1997 +0200 (1997-08-05)
changeset 3589244daa75f890
parent 3588 e487bf0ed6c4
child 3590 4d307341d0af
Added function `replicate' and lemmas map_cong and set_replicate.
src/HOL/List.ML
src/HOL/List.thy
     1.1 --- a/src/HOL/List.ML	Tue Aug 05 16:14:23 1997 +0200
     1.2 +++ b/src/HOL/List.ML	Tue Aug 05 16:21:45 1997 +0200
     1.3 @@ -196,6 +196,16 @@
     1.4  by (ALLGOALS Asm_simp_tac);
     1.5  qed "rev_map";
     1.6  
     1.7 +(* a congruence rule for map: *)
     1.8 +goal thy
     1.9 + "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
    1.10 +by(rtac impI 1);
    1.11 +by(hyp_subst_tac 1);
    1.12 +by(induct_tac "ys" 1);
    1.13 +by(ALLGOALS Asm_simp_tac);
    1.14 +val lemma = result();
    1.15 +bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
    1.16 +
    1.17  (** rev **)
    1.18  
    1.19  section "rev";
    1.20 @@ -617,3 +627,15 @@
    1.21  by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    1.22  qed_spec_mp"set_of_list_take_whileD";
    1.23  
    1.24 +(** replicate **)
    1.25 +section "replicate";
    1.26 +
    1.27 +goal thy "set(replicate (Suc n) x) = {x}";
    1.28 +by(induct_tac "n" 1);
    1.29 +by(ALLGOALS Asm_full_simp_tac);
    1.30 +val lemma = result();
    1.31 +
    1.32 +goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";
    1.33 +by(fast_tac (!claset addSDs [not0_implies_Suc] addSIs [lemma]) 1);
    1.34 +qed "set_replicate";
    1.35 +Addsimps [set_replicate];
     2.1 --- a/src/HOL/List.thy	Tue Aug 05 16:14:23 1997 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Aug 05 16:21:45 1997 +0200
     2.3 @@ -26,6 +26,7 @@
     2.4    dropWhile   :: ('a => bool) => 'a list => 'a list
     2.5    tl,ttl      :: 'a list => 'a list
     2.6    rev         :: 'a list => 'a list
     2.7 +  replicate   :: nat => 'a => 'a list
     2.8  
     2.9  syntax
    2.10    (* list Enumeration *)
    2.11 @@ -109,6 +110,9 @@
    2.12  primrec dropWhile list
    2.13    "dropWhile P [] = []"
    2.14    "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
    2.15 +primrec replicate nat
    2.16 +replicate_0   "replicate 0 x       = []"
    2.17 +replicate_Suc "replicate (Suc n) x = x # replicate n x"
    2.18  
    2.19  end
    2.20